From 8b7bca3339196d3d526aa8454d2cf37e501bc2ed Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Sun, 2 Mar 2025 13:41:36 +1100 Subject: [PATCH] renamed pi_agentTheory --- .../pi-calculus/open_bisimulationScript.sml | 6 +- ...i_nominalScript.sml => pi_agentScript.sml} | 61 ++++++++++++------- .../pi-calculus/testScript.sml | 55 ----------------- 3 files changed, 44 insertions(+), 78 deletions(-) rename examples/formal-languages/pi-calculus/{pi_nominalScript.sml => pi_agentScript.sml} (95%) delete mode 100644 examples/formal-languages/pi-calculus/testScript.sml diff --git a/examples/formal-languages/pi-calculus/open_bisimulationScript.sml b/examples/formal-languages/pi-calculus/open_bisimulationScript.sml index 3ee1aad39c..2734f7ce14 100644 --- a/examples/formal-languages/pi-calculus/open_bisimulationScript.sml +++ b/examples/formal-languages/pi-calculus/open_bisimulationScript.sml @@ -7,9 +7,13 @@ open HolKernel Parse boolLib bossLib; -open pred_setTheory pi_nominalTheory; +open pred_setTheory pi_agentTheory stringTheory relationTheory; val _ = new_theory "open_bisimulation"; +Definition distinction_def : + distinction (d :string -> string -> bool) <=> symmetric d /\ irreflexive d +End + val _ = export_theory (); val _ = html_theory "open_bisimulation"; diff --git a/examples/formal-languages/pi-calculus/pi_nominalScript.sml b/examples/formal-languages/pi-calculus/pi_agentScript.sml similarity index 95% rename from examples/formal-languages/pi-calculus/pi_nominalScript.sml rename to examples/formal-languages/pi-calculus/pi_agentScript.sml index be96ff6840..2f78bc17d7 100644 --- a/examples/formal-languages/pi-calculus/pi_nominalScript.sml +++ b/examples/formal-languages/pi-calculus/pi_agentScript.sml @@ -1,6 +1,6 @@ (* ========================================================================== *) -(* FILE : pi_nominalScript.sml *) -(* DESCRIPTION : Nominal type for pi-calculus *) +(* FILE : pi_agentScript.sml *) +(* DESCRIPTION : Nominal type for process (agent) of pi-calculus *) (* *) (* Copyright 2025 The Australian National University (Author: Chun Tian) *) (* ========================================================================== *) @@ -9,27 +9,42 @@ open HolKernel Parse boolLib bossLib; open pred_setTheory generic_termsTheory binderLib nomsetTheory nomdatatype; -val _ = new_theory "pi_nominal"; +val _ = new_theory "pi_agent"; (* ---------------------------------------------------------------------- - Pi-calculus as a nominal datatype in HOL4 - - [type 0] - name := Name string - - [type 1] - pi := Nil - | Tau pi - | Input name "<> pi" a(x). P (x is the binding variable) - | Output name name pi \bar{a}b. P - | Match name name pi [a == b] P - | Mismatch name name pi [a != b] P - | Sum pi pi P + Q - | Par pi pi P || Q - | Restr "<> pi" nu x. P - | Var string (unused, to be deleted) - - NOTE: Replication ("!") is not supported. + Pi-calculus as a nominal datatype in HOL4 + + HOL4 syntax ('free and 'bound are special type variables (alias of string) + + Nominal_datatype : + term = VAR 'free | LAM 'bound term | APP term term + End + + Nomimal_datatype : + CCS = nil + | var 'free + | prefix ('a Action) CCS + | sum CCS CCS + | par CCS CCS + | restr ('a Label set) CCS + | relab CCS ('a Relabeling) + | rec 'bound CCS + End + + Nominal_datatype : + name = Name 'free + pi = Nil (* 0 *) + | Tau pi (* tau.P *) + | Input name 'bound pi (* a(x).P *) + | Output name name pi (* {a}b.P *) + | Match name name pi (* [a == b] P *) + | Mismatch name name pi (* [a <> b] P *) + | Sum pi pi (* P + Q *) + | Par pi pi (* P | Q *) + | Restr 'bound pi (* nu x. P *) + End + + NOTE: Replication ("!") is not supported. ---------------------------------------------------------------------- *) val tyname0 = "name"; @@ -124,7 +139,7 @@ val Name_termP = prove( srw_tac [][genind_rules]); val Name_t = defined_const Name_def; -(* "Var" of type 1 (:pi), functions as Nil *) +(* "Var" of type 1 (:pi) *) val Var_t = mk_var("Var", “:string -> ^newty1”); val Var_def = new_definition( "Var_def", “^Var_t s = ^term_ABS_t1 (GVAR s ())”); @@ -490,6 +505,7 @@ Theorem FV_tpm[simp] = “x IN FV (tpm p (t :pi))” term induction ---------------------------------------------------------------------- *) +(* fun genit th = let val (_, args) = strip_comb (concl th) val (tm, x) = case args of [x,y] => (x,y) | _ => raise Fail "Bind" @@ -566,6 +582,7 @@ Theorem tpm_ALPHA : Proof SRW_TAC [boolSimps.CONJ_ss][rec_eq_thm, pmact_flip_args] QED + *) (* ---------------------------------------------------------------------- Pi-term recursion diff --git a/examples/formal-languages/pi-calculus/testScript.sml b/examples/formal-languages/pi-calculus/testScript.sml deleted file mode 100644 index 8bffde384c..0000000000 --- a/examples/formal-languages/pi-calculus/testScript.sml +++ /dev/null @@ -1,55 +0,0 @@ -open HolKernel Parse boolLib bossLib; - -open pred_setTheory generic_termsTheory binderLib nomsetTheory nomdatatype; - -val _ = new_theory "test"; - -(* ---------------------------------------------------------------------- - [type 0] - name := Name string - - [type 1] - pi := Nil - | Input name "<> pi" - ---------------------------------------------------------------------- *) - -val tyname0 = "name"; -val tyname1 = "pi"; - -val gvar_rep_t = “:unit”; -val u_tm = mk_var("u", gvar_rep_t); -val vp = “(\n ^u_tm. n = 0 \/ n = 1)”; - -val glam_rep_t = “:unit + unit”; -val d_tm = mk_var("d", glam_rep_t); -val lp = - “(\n ^d_tm tns uns. - n = 1 /\ ISL d /\ tns = [] ∧ uns = [] \/ - n = 1 /\ ISR d /\ tns = [1] ∧ uns = [0] - )”; - -(* type 0 (:name) *) -val {term_ABS_pseudo11 = term_ABS_pseudo11_0, - term_REP_11 = term_REP_11_0, - genind_term_REP = genind_term_REP0, - genind_exists = genind_exists0, - termP = termP0, - absrep_id = absrep_id0, - repabs_pseudo_id = repabs_pseudo_id0, - term_REP_t = term_REP_t0, - term_ABS_t = term_ABS_t0, - newty = newty0, ...} = new_type_step1 tyname0 0 {vp = vp, lp = lp}; - -(* type 1 (:pi) *) -val {term_ABS_pseudo11 = term_ABS_pseudo11_1, - term_REP_11 = term_REP_11_1, - genind_term_REP = genind_term_REP1, - genind_exists = genind_exists1, - termP = termP1, - absrep_id = absrep_id1, - repabs_pseudo_id = repabs_pseudo_id1, - term_REP_t = term_REP_t1, - term_ABS_t = term_ABS_t1, - newty = newty1, ...} = new_type_step1 tyname1 1 {vp = vp, lp = lp}; - -val _ = export_theory ();