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 picalc_str_eq_is_bisimulation.thm]

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

Specification "processes_terms".

Import "picalc". [View picalc]

/*** structural equivalence is bisimulation in the tensor case */

/*lemma */

Theorem red_ker_tensor_str_eq_left_of_par : forall P1 P2 Q R2,
      str_eq P2 P1 -> red_ker_tensor P2 Q R2
      -> exists R1, red_ker_tensor P1 Q R1 /\ str_eq R2 R1.
induction on 1. intros. case H1. search. case H3. apply red_ker_tensor_par_cases to H2. case H4. search. apply red_ker_tensor_null_cases to H5. apply red_ker_tensor_par_cases to H2. case H4. apply red_ker_tensor_null_cases to H5. search. search. search. apply red_ker_tensor_nu_cases to H2. apply red_ker_tensor_null_cases to H4. apply red_ker_tensor_null_cases to H2. apply red_ker_tensor_par_cases to H2. case H4. search. search. apply red_ker_tensor_par_cases to H2. case H4. apply red_ker_tensor_par_cases to H5. case H7. search. search. search. apply red_ker_tensor_par_cases to H2. case H4. search. apply red_ker_tensor_par_cases to H5. case H7. search. search. apply red_ker_tensor_nu_cases to H2. apply red_ker_tensor_par_cases to H4. case H6. apply red_ker_tensor_no_new_names to H7. search. search. apply red_ker_tensor_nu_cases to H2. apply red_ker_tensor_par_cases to H4. case H6. search. apply red_ker_tensor_no_new_names to H7. search. apply red_ker_tensor_par_cases to H2. case H4. search. apply red_ker_tensor_nu_cases to H5. search. apply red_ker_tensor_par_cases to H2. case H4. apply red_ker_tensor_nu_cases to H5. search. search. apply red_ker_tensor_nu_cases to H2. apply red_ker_tensor_nu_cases to H4. search. apply red_ker_tensor_nu_cases to H2. apply IH to H3 H4. search. apply red_ker_tensor_par_cases to H2. case H4. apply IH to H3 H5. search. search. apply red_ker_tensor_par_cases to H2. case H4. search. apply IH to H3 H5. search. apply IH to H3 H2. apply IH to H4 H5. search.
/* proof */ Theorem red_str_eq_delay_tensor : forall P1 P2 Q2, str_eq P2 P1 -> red_tensor P2 Q2 -> exists Q1, red_tensor P1 Q1 /\ str_eq Q2 Q1. /*** structural equivalence is bisimulation in the exponential case */ /* lemma */ Theorem red_ker_exp_str_eq_left_of_par : forall P1 P2 Q R2, str_eq P2 P1 -> red_ker_exp P2 Q R2 -> exists R1, red_ker_exp P1 Q R1 /\ str_eq R2 R1. /* proof */ Theorem red_str_eq_delay_exp : forall P1 P2 Q2, str_eq P2 P1 -> red_exp P2 Q2 -> exists Q1, red_exp P1 Q1 /\ str_eq Q2 Q1.