diff --git a/examples/formal-languages/pi-calculus/open_bisimulationScript.sml b/examples/formal-languages/pi-calculus/open_bisimulationScript.sml index 2734f7ce14..2827147953 100644 --- a/examples/formal-languages/pi-calculus/open_bisimulationScript.sml +++ b/examples/formal-languages/pi-calculus/open_bisimulationScript.sml @@ -7,12 +7,83 @@ open HolKernel Parse boolLib bossLib; -open pred_setTheory pi_agentTheory stringTheory relationTheory; +open pred_setTheory relationTheory; + +open pi_agentTheory; val _ = new_theory "open_bisimulation"; +Type dist[pp] = “:string -> string -> bool” + Definition distinction_def : - distinction (d :string -> string -> bool) <=> symmetric d /\ irreflexive d + distinction (D :dist) <=> symmetric D /\ irreflexive D +End + +Inductive TRANS : +[TAU] + !P. TRANS (Tau P) (TauR P) +[INPUT] + !a x P. Name x <> a ==> TRANS (Input a x P) (InputR a x P) +[OUTPUT] + !a b P. TRANS (Output a b P) (FreeOutput a b P) +[MATCH] + !P R b. TRANS P R ==> TRANS (Match (Name b) (Name b) P) R +[MISMACH] + !P R a b. TRANS P R /\ a <> b ==> TRANS (Mismatch (Name a) (Name b) P) R +[OPEN] + !P x z P'. TRANS P (FreeOutput x (Name z) P') /\ x <> Name z ==> + TRANS (Res z P) (BoundOutput x z P') +[SUM1] + !P Q R. TRANS P R ==> TRANS (Sum P Q) R +[SUM2] + !P Q R. TRANS Q R ==> TRANS (Sum P Q) R +[PAR1B] + !P Q R. TRANS P (InputR a x Q) /\ x # P /\ x # Q /\ Name x <> a ==> + TRANS (Par P R) (InputR a x (Par Q R)) +[PAR1BO] + !P Q R. TRANS P (BoundOutput a x Q) /\ x # P /\ x # Q /\ Name x <> a ==> + TRANS (Par P R) (BoundOutput a x (Par Q R)) +[PAR1F] + !P Q R. TRANS P (FreeOutput a b Q) ==> + TRANS (Par P R) (FreeOutput a b (Par Q R)) +[PAR1T] + !P Q R. TRANS P (TauR Q) ==> TRANS (Par P R) (TauR (Par Q R)) +End + +Inductive DTRANS : +[DTAU] + !D P. DTRANS (D :dist) (Tau P) (TauR P) +[DINPUT] + !D a x P. Name x <> a ==> DTRANS D (Input a x P) (InputR a x P) +[DOUTPUT] + !D a b P. DTRANS D (Output a b P) (FreeOutput a b P) +[DMATCH] + !D P R b. DTRANS D P R ==> + DTRANS D (Match (Name b) (Name b) P) R +[DMISMACH] + !D P R a b. distinction D /\ D a b /\ DTRANS D P R ==> + DTRANS D (Mismatch (Name a) (Name b) P) R +[DOPEN] + !D D' P x z Q. + DTRANS D' P (FreeOutput x (Name z) Q) /\ x <> Name z /\ + distinction D /\ z NOTIN (RDOM D) /\ + D' = D RUNION SC (\x y. x = z /\ y IN FV (Res z P)) ==> + DTRANS D (Res z P) (BoundOutput x z Q) +[DSUM1] + !D P Q R. DTRANS D P R ==> DTRANS D (Sum P Q) R +[DSUM2] + !D P Q R. DTRANS D Q R ==> DTRANS D (Sum P Q) R +[DPAR1B] + !D P Q R. DTRANS D P (InputR a x Q) /\ x # P /\ x # Q /\ Name x <> a ==> + DTRANS D (Par P R) (InputR a x (Par Q R)) +[DPAR1BO] + !D P Q R. DTRANS D P (BoundOutput a x Q) /\ x # P /\ x # Q /\ Name x <> a ==> + DTRANS D (Par P R) (BoundOutput a x (Par Q R)) +[DPAR1F] + !D P Q R. DTRANS D P (FreeOutput a b Q) ==> + DTRANS D (Par P R) (FreeOutput a b (Par Q R)) +[DPAR1T] + !D P Q R. DTRANS D P (TauR Q) ==> DTRANS D (Par P R) (TauR (Par Q R)) End val _ = export_theory (); diff --git a/examples/formal-languages/pi-calculus/pi_agentScript.sml b/examples/formal-languages/pi-calculus/pi_agentScript.sml index 4cf958783d..a15ddd1bc5 100644 --- a/examples/formal-languages/pi-calculus/pi_agentScript.sml +++ b/examples/formal-languages/pi-calculus/pi_agentScript.sml @@ -42,9 +42,9 @@ val _ = new_theory "pi_agent"; | Sum pi pi (* P + Q *) | Par pi pi (* P | Q *) | Res 'bound pi (* nu x. P *) - residual = Residual pi + residual = TauR pi | FreeOutput name name pi - | InputResidual name 'bound pi + | InputR name 'bound pi | BoundOutput name 'bound pi End @@ -318,19 +318,19 @@ val Res_termP = prove( match_mp_tac glam >> srw_tac [][genind_term_REP1]); val Res_t = defined_const Res_def; -(* (Tau) Residual *) -val Residual_t = mk_var("Residual", “:^newty1 -> ^newty2”); -val Residual_def = new_definition( - "Residual_def", - “^Residual_t P = ^term_ABS_t2 (GLAM ARB (INL ()) [] [^term_REP_t1 P])”); -val Residual_tm = Residual_def |> concl |> strip_forall |> snd |> rhs |> rand; -val Residual_termP = prove( +(* TauR *) +val TauR_t = mk_var("TauR", “:^newty1 -> ^newty2”); +val TauR_def = new_definition( + "TauR_def", + “^TauR_t P = ^term_ABS_t2 (GLAM ARB (INL ()) [] [^term_REP_t1 P])”); +val TauR_tm = TauR_def |> concl |> strip_forall |> snd |> rhs |> rand; +val TauR_termP = prove( mk_comb(termP1, Tau_tm), match_mp_tac glam >> srw_tac [][genind_term_REP1]); -val Residual_t = defined_const Residual_def; -val Residual_def' = prove( - “^term_ABS_t2 ^Residual_tm = ^Residual_t P”, - srw_tac [][Residual_def, GLAM_NIL_EQ, term_ABS_pseudo11_2, Residual_termP]); +val TauR_t = defined_const TauR_def; +val TauR_def' = prove( + “^term_ABS_t2 ^TauR_tm = ^TauR_t P”, + srw_tac [][TauR_def, GLAM_NIL_EQ, term_ABS_pseudo11_2, TauR_termP]); (* Bound output (residual) *) val BoundOutput_t = mk_var("BoundOutput", “:^newty0 -> string -> ^newty1 -> ^newty2”); @@ -346,26 +346,27 @@ val BoundOutput_termP = prove( val BoundOutput_t = defined_const BoundOutput_def; val BoundOutput_def' = prove( “^term_ABS_t2 ^BoundOutput_tm = ^BoundOutput_t a x P”, - srw_tac [][BoundOutput_def, GLAM_NIL_EQ, term_ABS_pseudo11_1, BoundOutput_termP]); + srw_tac [][BoundOutput_def, GLAM_NIL_EQ, (* term_ABS_pseudo11_2, *) + BoundOutput_termP]); (* Input residual *) -val InputResidual_t = mk_var("InputResidual", +val InputR_t = mk_var("InputR", “:^newty0 -> string -> ^newty1 -> ^newty2”); -val InputResidual_def = new_definition( - "InputResidual_def", - “^InputResidual_t a x P = ^term_ABS_t2 (GLAM x (INR (INR (INL ()))) +val InputR_def = new_definition( + "InputR_def", + “^InputR_t a x P = ^term_ABS_t2 (GLAM x (INR (INR (INL ()))) [^term_REP_t1 P] [^term_REP_t0 a])”); -val InputResidual_tm = - InputResidual_def |> concl |> strip_forall |> snd |> rhs |> rand; -val InputResidual_termP = prove( - mk_comb(termP2, InputResidual_tm), +val InputR_tm = + InputR_def |> concl |> strip_forall |> snd |> rhs |> rand; +val InputR_termP = prove( + mk_comb(termP2, InputR_tm), match_mp_tac glam >> srw_tac [][genind_term_REP0, genind_term_REP1]); -val InputResidual_t = defined_const InputResidual_def; -val InputResidual_def' = prove( - “^term_ABS_t2 ^InputResidual_tm = ^InputResidual_t a x P”, - srw_tac [][InputResidual_def, GLAM_NIL_EQ, term_ABS_pseudo11_1, - InputResidual_termP]); +val InputR_t = defined_const InputR_def; +val InputR_def' = prove( + “^term_ABS_t2 ^InputR_tm = ^InputR_t a x P”, + srw_tac [][InputR_def, GLAM_NIL_EQ, (* term_ABS_pseudo11_1, *) + InputR_termP]); (* Free output (residual) *) val FreeOutput_t = mk_var("FreeOutput", “:^newty0 -> ^newty0 -> ^newty1 -> ^newty2”); @@ -382,7 +383,8 @@ val FreeOutput_termP = prove( val FreeOutput_t = defined_const FreeOutput_def; val FreeOutput_def' = prove( “^term_ABS_t2 ^FreeOutput_tm = ^FreeOutput_t a b P”, - srw_tac [][FreeOutput_def, GLAM_NIL_EQ, term_ABS_pseudo11_1, FreeOutput_termP]); + srw_tac [][FreeOutput_def, GLAM_NIL_EQ, (* term_ABS_pseudo11_1, *) + FreeOutput_termP]); (* ---------------------------------------------------------------------- tpm - permutation of pi-calculus binding variables @@ -406,7 +408,8 @@ val {tpm_thm, term_REP_tpm, t_pmact_t, tpm_t} = term_ABS_t = term_ABS_t1, absrep_id = absrep_id1, repabs_pseudo_id = repabs_pseudo_id1, - cons_info = cons_info, newty = newty1, + cons_info = cons_info, + newty = newty1, genind_term_REP = genind_term_REP1}; Theorem tpm_eqr : @@ -427,19 +430,24 @@ Proof SRW_TAC [][GSYM pmact_decompose] QED +(* ---------------------------------------------------------------------- + npm - permutation of pi-calculus names + ---------------------------------------------------------------------- *) + val ncons_info = [{con_termP = Name_termP, con_def = Name_def}]; -val tpm_name_pfx = "n"; +val npm_name_pfx = "n"; val {tpm_thm = npm_thm, term_REP_tpm = term_REP_npm, t_pmact_t = n_pmact_t, tpm_t = npm_t} = - define_permutation {name_pfx = tpm_name_pfx, name = tyname0, + define_permutation {name_pfx = npm_name_pfx, name = tyname0, term_REP_t = term_REP_t0, term_ABS_t = term_ABS_t0, absrep_id = absrep_id0, repabs_pseudo_id = repabs_pseudo_id0, - cons_info = ncons_info, newty = newty0, + cons_info = ncons_info, + newty = newty0, genind_term_REP = genind_term_REP0}; Theorem npm_eqr : @@ -460,6 +468,50 @@ Proof SRW_TAC [][GSYM pmact_decompose] QED +(* ---------------------------------------------------------------------- + rpm - permutation of pi-calculus residuals + ---------------------------------------------------------------------- + +val rcons_info = + [{con_termP = TauR_termP, con_def = SYM TauR_def'}, + {con_termP = BoundOutput_termP, con_def = SYM BoundOutput_def'}, + {con_termP = InputR_termP, con_def = SYM InputR_def'}, + {con_termP = FreeOutput_termP, con_def = SYM FreeOutput_def'}]; + +val rpm_name_pfx = "r"; + +val {tpm_thm = rpm_thm, + term_REP_tpm = term_REP_rpm, + t_pmact_t = r_pmact_t, + tpm_t = rpm_t} = + define_permutation {name_pfx = rpm_name_pfx, name = tyname2, + term_REP_t = term_REP_t2, + term_ABS_t = term_ABS_t2, + absrep_id = absrep_id2, + repabs_pseudo_id = repabs_pseudo_id2, + cons_info = rcons_info, + newty = newty2, + genind_term_REP = genind_term_REP2}; + +Theorem npm_eqr : + t = npm pi u <=> npm (REVERSE pi) t = (u :name) +Proof + METIS_TAC [pmact_inverse] +QED + +Theorem npm_eql : + npm pi t = u <=> t = npm (REVERSE pi) (u :name) +Proof + simp[npm_eqr] +QED + +Theorem npm_CONS : + npm ((x,y)::pi) (t :name) = npm [(x,y)] (npm pi t) +Proof + SRW_TAC [][GSYM pmact_decompose] +QED + *) + (* ---------------------------------------------------------------------- support (supp) and fn (for type :name) ---------------------------------------------------------------------- *) @@ -593,6 +645,75 @@ Theorem FV_tpm[simp] = “x IN FV (tpm p (t :pi))” |> REWRITE_CONV [perm_supp, pmact_IN] |> GEN_ALL +(* ---------------------------------------------------------------------- + support (supp) and fv (for type :residual) + ---------------------------------------------------------------------- + +val term_REP_eqv = prove( + “support (fn_pmact ^t_pmact_t gt_pmact) ^term_REP_t2 {}”, + srw_tac [][support_def, fnpm_def, FUN_EQ_THM, term_REP_tpm, pmact_sing_inv]); + +val supp_term_REP = prove( + “supp (fn_pmact ^t_pmact_t gt_pmact) ^term_REP_t1 = {}”, + REWRITE_TAC [GSYM SUBSET_EMPTY] + >> MATCH_MP_TAC (GEN_ALL supp_smallest) + >> srw_tac [][term_REP_eqv]); + +val tpm_def' = + term_REP_tpm |> AP_TERM term_ABS_t1 |> PURE_REWRITE_RULE [absrep_id1]; + +val t = mk_var("t", newty1); + +val supp_tpm_support = prove( + “support ^t_pmact_t ^t (supp gt_pmact (^term_REP_t1 ^t))”, + srw_tac [][support_def, tpm_def', supp_fresh, absrep_id1]); + +val supp_tpm_apart = prove( + “x IN supp gt_pmact (^term_REP_t1 ^t) /\ y NOTIN supp gt_pmact (^term_REP_t1 ^t) + ==> ^tpm_t [(x,y)] ^t <> ^t”, + srw_tac [][tpm_def'] + >> DISCH_THEN (MP_TAC o AP_TERM term_REP_t1) + >> srw_tac [][repabs_pseudo_id1, genind_gtpm_eqn, genind_term_REP1, supp_apart]); + +val supp_tpm = prove( + “supp ^t_pmact_t ^t = supp gt_pmact (^term_REP_t1 ^t)”, + match_mp_tac (GEN_ALL supp_unique_apart) + >> srw_tac [][supp_tpm_support, supp_tpm_apart, FINITE_GFV]); + +val _ = overload_on ("FV", “supp ^t_pmact_t”); + +val _ = set_fixity "#" (Infix(NONASSOC, 450)); +val _ = overload_on ("#", “\v (P :pi). v NOTIN FV P”); + +Theorem FINITE_FV[simp] : + FINITE (FV (t :pi)) +Proof + srw_tac [][supp_tpm, FINITE_GFV] +QED + +Theorem FV_EMPTY : + FV t = {} <=> !v. v NOTIN FV (t :pi) +Proof + SIMP_TAC (srw_ss()) [EXTENSION] +QED + +fun supp_clause {con_termP, con_def} = let + val t = mk_comb(“supp ^t_pmact_t”, lhand (concl (SPEC_ALL con_def))) +in + t |> REWRITE_CONV [supp_tpm, con_def, MATCH_MP repabs_pseudo_id1 con_termP, + GFV_thm] + |> REWRITE_RULE [supp_listpm, EMPTY_DELETE, UNION_EMPTY] + |> REWRITE_RULE [GSYM supp_tpm, GSYM supp_npm] + |> GEN_ALL +end + +Theorem FV_thm[simp] = LIST_CONJ (map supp_clause cons_info) + +Theorem FV_tpm[simp] = “x IN FV (tpm p (t :pi))” + |> REWRITE_CONV [perm_supp, pmact_IN] + |> GEN_ALL + *) + (* ---------------------------------------------------------------------- term induction ---------------------------------------------------------------------- *)