Executable Specification

[View processes_terms.sig] [View processes_terms.mod]
sig processes_terms.

kind pt type.

%lsc terms
type abs (pt -> pt) -> pt.
type app pt -> pt -> pt.
type subex (pt -> pt) -> pt -> pt.

%pi-calculus terms
type null       pt.
type nu 	(pt -> pt) -> pt.
type par	pt -> pt -> pt.
type out	pt -> pt -> pt.
type out2	pt -> pt -> pt -> pt.
type in		pt -> (pt -> pt) -> pt.
type in2 	pt -> (pt -> pt -> pt) -> pt.
module processes_terms.

Reasoning

[View trans_is_bisimulation.thm]

Click on a command or tactic to see a detailed view of its use.

Specification "processes_terms".

Import "trans". [View trans]
Import "picalc". [View picalc]
Import "lsc". [View lsc]


/*** 1. simulation of beta at a distance by tensor reduction ***/

Theorem lemma_red_tensor_simulates_red_db : forall U V W P Q R2,
   red_db_ker U V W -> trans U P -> trans V Q -> trans W R2
   -> exists R1, nabla b y z,
      red_ker_tensor (P b) (par (out2 b y z) (in y Q)) (R1 y z)
     /\ str_eq (nu (y\R1 y z)) (R2 z).

Theorem red_tensor_simulates_evc_red_db: forall U V P Q2,
   evc_cl red_db U V -> trans U P -> trans V Q2
   -> exists Q1, nabla a, red_tensor (P a) (Q1 a) /\ str_eq (Q2 a) (Q1 a).

/*** 2. simulation of linear substitution by exponential reduction***/

Theorem lemma_red_exp_simulates_red_ls : forall U W V P R Q2, nabla y,
   red_ls_ker W U V -> trans W R -> trans (U y) (P y) -> trans (V y) (Q2 y)
   -> exists Q1, nabla a y, red_ker_exp (P y a) (in y R) (Q1 y a)
      /\ str_eq (Q1 y a)(par (Q2 y a) (in y R)).

Theorem red_exp_simulates_red_ls : forall U V P Q2,
   evc_cl red_ls U V -> trans U P -> trans V Q2
   -> exists Q1, nabla a, red_exp (P a) (Q1 a) /\ str_eq (Q1 a) (Q2 a).

/*** 3. converse simulation of beta at a distance ***/

Theorem lemma_red_db_simulates_red_tensor : forall U V P Q R Q1, nabla a b c,
   trans U P -> trans V R -> red_ker_tensor (out2 b c a) (P b) (Q b a c)
   -> str_eq (par (Q b a c) (in c R)) (Q1 b a c)
   -> exists W Q2, nabla a, red_db_ker U V W
      /\ trans W Q2 /\ str_eq (nu (z2\ nu (Q1 z2 a))) (Q2 a).
induction on 1. intros. case H1. case H3. case H3. case H7. case H8. apply red_ker_tensor_out2_no_com_case to H9. case H9. case H10. case H10. case H3. exists subex U1 V. exists a\nu (x\par (P3 a x) (in x R)). intros. split. search. search. unfold 20. exists nu (z1\nu (z2\Q1 z2 n1 z1)). split. search. unfold 17. intros. unfold 20. exists nu (z2\par (P3 n1 n2) (in n2 R)). split. backchain str_eq_sym. backchain 0 str_eq_sym. backchain nu_gen. case H3. case H7. permute (n1 n4) H5. apply IH to *H5 *H2 *H8 _. exists subex W V1. exists a\nu (x\par (Q3 x a) (in x Q2)). intros. split. search. search. unfold 20. exists nu (z2\nu (z3\par (nu (z4\par (S z4 z2 n1 z3) (in z4 Q2))) (in z3 R))). split. backchain str_eq_sym. unfold 20. exists nu (z2\nu (z3\nu (z4\par (par (S z4 z2 n1 z3) (in z4 Q2)) (in z3 R)))). split. search. unfold 20. exists nu (z2\nu (z4\nu (z3\par (par (S z4 z2 n1 z3) (in z4 Q2)) (in z3 R)))). split. search. unfold 20. exists nu (z4\nu (z2\nu (z3\par (par (S z4 z2 n1 z3) (in z4 Q2)) (in z3 R)))). split. search. unfold 17. intros. unfold 20. exists nu (z2\nu (z3\par (S n2 z2 n1 z3) (par (in n2 Q2) (in z3 R)))). split. search. unfold 20. exists nu (z2\nu (z3\par (S n2 z2 n1 z3) (par (in z3 R) (in n2 Q2)))). split. search. unfold 20. exists nu (z2\nu (z3\par (par (S n2 z2 n1 z3) (in z3 R)) (in n2 Q2))). split. search. unfold 20. exists nu (z2\par (nu (z3\par (S n2 z2 n1 z3) (in z3 R))) (in n2 Q2)). split. search. unfold 20. exists par (nu (z2\nu (z3\par (S n2 z2 n1 z3) (in z3 R)))) (in n2 Q2). split. search. unfold 18. intros. search. case H8.
Theorem red_db_simulates_red_tensor : forall U P Q1, nabla a, trans U P -> red_tensor (P a) (Q1 a) -> exists V Q2, nabla a, evc_cl red_db U V /\ trans V Q2 /\ str_eq (Q1 a) (Q2 a). /*** 4. convere simulation of linear substitution ***/ Theorem lemma_red_ls_simulates_red_exp : forall P Q R1 U V, nabla x y, trans (U x) (P x) -> trans V Q -> red_ker_exp (P y x) (in y Q) (R1 y x) -> exists W R2, nabla x y, red_ls_ker V U W /\ trans (W y) (R2 y) /\ str_eq (R1 y x) (par (R2 y x) (in y Q)).
induction on 1. intros. case H1. case H3. case H3. search. case H3. case H6. case H7. apply red_ker_exp_no_new_names to H8. apply red_ker_exp_no_new_names to H8. apply IH to H4 H2 _. exists z1\app (W z1) (V1 z1). exists y\a\nu (b\nu (x1\ par (R3 y b) (par (out2 b x1 a) (in x1 (Q1 y))))). intros. split. search. search. clear IH H2 H4 H5 H8 H9 H10. unfold 20. exists nu (b\par (nu (x1\par (R3 n2 b) (par (out2 b x1 n1) (in x1 (Q1 n2))))) (in n2 Q)). split. unfold 20. exists nu (b\nu (x1\par (par (R3 n2 b) (par (out2 b x1 n1) (in x1 (Q1 n2)))) (in n2 Q))). split. unfold 17. intros. unfold 17. intros. unfold 20. exists par (R3 n2 n3) (par (par (out2 n3 n4 n1) (in n4 (Q1 n2))) (in n2 Q)). split. unfold 20. exists par (R3 n2 n3) (par (in n2 Q) (par (out2 n3 n4 n1) (in n4 (Q1 n2)))). split. unfold 20. exists par (par (R3 n2 n3) (in n2 Q)) (par (out2 n3 n4 n1) (in n4 (Q1 n2))). split. unfold 18. search. search. search. search. search. search. case H8. case H9. case H9. case H3. case H3. case H6. apply IH to H4 H2 _. exists z1\subex (z2\W z2 z1) (V1 z1). exists y\a\nu (x\par (R2 x y a) (in x (Q1 y))). intros. split. search. search. clear IH H2 H4 H5 H7 H8 H9. unfold 20. exists nu (x\par (par (R2 x n2 n1) (in x (Q1 n2))) (in n2 Q)). split. unfold 17. intros. unfold 20. exists par (R2 n3 n2 n1) (par (in n3 (Q1 n2)) (in n2 Q)). split. unfold 20. exists par (R2 n3 n2 n1) (par (in n2 Q) (in n3 (Q1 n2))). split. unfold 20. exists par (par (R2 n3 n2 n1) (in n2 Q)) (in n3 (Q1 n2)). split. unfold 18. search. search. search. search. search. case H7.
Theorem red_ls_simulates_red_exp : forall U P Q1, nabla a, trans U P -> red_exp (P a) (Q1 a) -> exists V Q2, nabla a, evc_cl red_ls U V /\ trans V Q2 /\ str_eq (Q1 a) (Q2 a).