renamed pi_agentTheory

binghe · Mar 2, 2025 · 8b7bca3 · 8b7bca3
1 parent 6f026fe
commit 8b7bca3
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 78 deletions.
diff --git 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/...anguages/pi-calculus/pi_nominalScript.sml → ...-languages/pi-calculus/pi_agentScript.sml b/...anguages/pi-calculus/pi_nominalScript.sml → ...-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 "<<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 "<<name>> 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