Skip to content

Commit

Permalink
Minor cleanups (pi_agent)
Browse files Browse the repository at this point in the history
  • Loading branch information
@binghe
binghe committed Mar 2, 2025
1 parent 95db595 commit a80b821
Show file tree
Hide file tree
Showing 2 changed files with 47 additions and 29 deletions.
28 changes: 28 additions & 0 deletions examples/formal-languages/pi-calculus/open_bisimulationScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,34 @@ open pi_agentTheory;

val _ = new_theory "open_bisimulation";

(* ----------------------------------------------------------------------
Pi-calculus as a nominal datatype in HOL4
HOL4 syntax ('free and 'bound are special type variables (alias of string)
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 *)
| Res 'bound pi (* nu x. P *)
residual = TauR pi
| InputR name 'bound pi
| FreeOutput name name pi
| BoundOutput name 'bound pi
End
NOTE: Replication ("!") is not supported.
---------------------------------------------------------------------- *)

Type dist[pp] = “:string -> string -> bool”

Definition distinction_def :
Expand Down
48 changes: 19 additions & 29 deletions examples/formal-languages/pi-calculus/pi_agentScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,22 +17,9 @@ val _ = new_theory "pi_agent";
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 *)
Expand All @@ -42,9 +29,10 @@ val _ = new_theory "pi_agent";
| Sum pi pi (* P + Q *)
| Par pi pi (* P | Q *)
| Res 'bound pi (* nu x. P *)
residual = TauR pi
| FreeOutput name name pi
| InputR name 'bound pi
| FreeOutput name name pi
| BoundOutput name 'bound pi
End
Expand Down Expand Up @@ -161,8 +149,8 @@ val Name_t = mk_var("Name", “:string -> ^newty0”);
val Name_def = new_definition(
"Name_def", “^Name_t s = ^term_ABS_t0 (GVAR s ())”);
val Name_termP = prove(
mk_comb(termP0, Name_def |> SPEC_ALL |> concl |> rhs |> rand),
srw_tac [][genind_rules]);
mk_comb(termP0, Name_def |> SPEC_ALL |> concl |> rhs |> rand),
srw_tac [][genind_rules]);
val Name_t = defined_const Name_def;

(* "Var" of type 1 (:pi)
Expand All @@ -182,7 +170,7 @@ val Nil_def = new_definition(
“^Nil_t = ^term_ABS_t1 (GLAM ARB (INL ()) [] [])”);
val Nil_tm = Nil_def |> concl |> strip_forall |> snd |> rhs |> rand;
val Nil_termP = prove(
“^termP1 ^Nil_tm”,
mk_comb(termP1, Nil_tm),
match_mp_tac glam >> srw_tac [][genind_term_REP1]);
val Nil_t = defined_const Nil_def;
val Nil_def' = prove(
Expand All @@ -196,7 +184,7 @@ val Tau_def = new_definition(
“^Tau_t P = ^term_ABS_t1 (GLAM ARB (INR (INL ())) [] [^term_REP_t1 P])”);
val Tau_tm = Tau_def |> concl |> strip_forall |> snd |> rhs |> rand;
val Tau_termP = prove(
“^termP1 ^Tau_tm”,
mk_comb(termP1, Tau_tm),
match_mp_tac glam >> srw_tac [][genind_term_REP1]);
val Tau_t = defined_const Tau_def;
val Tau_def' = prove(
Expand All @@ -212,7 +200,7 @@ val Input_def = new_definition(
[^term_REP_t0 a])”);
val Input_tm = Input_def |> concl |> strip_forall |> snd |> rhs |> rand;
val Input_termP = prove(
“^termP1 ^Input_tm”,
mk_comb(termP1, Input_tm),
match_mp_tac glam >> srw_tac [][genind_term_REP0,genind_term_REP1]);
val Input_t = defined_const Input_def;
val Input_def' = prove(
Expand All @@ -229,7 +217,7 @@ val Output_def = new_definition(
^term_REP_t1 P])”);
val Output_tm = Output_def |> concl |> strip_forall |> snd |> rhs |> rand;
val Output_termP = prove(
“^termP1 ^Output_tm”,
mk_comb(termP1, Output_tm),
match_mp_tac glam >> srw_tac [][genind_term_REP0,genind_term_REP1]);
val Output_t = defined_const Output_def;
val Output_def' = prove(
Expand All @@ -246,7 +234,7 @@ val Match_def = new_definition(
^term_REP_t1 P])”);
val Match_tm = Match_def |> concl |> strip_forall |> snd |> rhs |> rand;
val Match_termP = prove(
“^termP1 ^Match_tm”,
mk_comb(termP1, Match_tm),
match_mp_tac glam >> srw_tac [][genind_term_REP0,genind_term_REP1]);
val Match_t = defined_const Match_def;
val Match_def' = prove(
Expand All @@ -264,7 +252,7 @@ val Mismatch_def = new_definition(
^term_REP_t1 P])”);
val Mismatch_tm = Mismatch_def |> concl |> strip_forall |> snd |> rhs |> rand;
val Mismatch_termP = prove(
“^termP1 ^Mismatch_tm”,
mk_comb(termP1, Mismatch_tm),
match_mp_tac glam >> srw_tac [][genind_term_REP0,genind_term_REP1]);
val Mismatch_t = defined_const Mismatch_def;
val Mismatch_def' = prove(
Expand All @@ -281,7 +269,7 @@ val Sum_def = new_definition(
^term_REP_t1 Q])”);
val Sum_tm = Sum_def |> concl |> strip_forall |> snd |> rhs |> rand;
val Sum_termP = prove(
“^termP1 ^Sum_tm”,
mk_comb(termP1, Sum_tm),
match_mp_tac glam >> srw_tac [][genind_term_REP1]);
val Sum_t = defined_const Sum_def;
val Sum_def' = prove(
Expand All @@ -298,7 +286,7 @@ val Par_def = new_definition(
^term_REP_t1 Q])”);
val Par_tm = Par_def |> concl |> strip_forall |> snd |> rhs |> rand;
val Par_termP = prove(
“^termP1 ^Par_tm”,
mk_comb(termP1, Par_tm),
match_mp_tac glam >> srw_tac [][genind_term_REP1]);
val Par_t = defined_const Par_def;
val Par_def' = prove(
Expand All @@ -314,7 +302,7 @@ val Res_def = new_definition(
[^term_REP_t1 P] [])”);
val Res_tm = Res_def |> concl |> strip_forall |> snd |> rhs |> rand;
val Res_termP = prove(
“^termP1 ^Res_tm”,
mk_comb (termP1, Res_tm),
match_mp_tac glam >> srw_tac [][genind_term_REP1]);
val Res_t = defined_const Res_def;

Expand All @@ -333,7 +321,8 @@ val TauR_def' = prove(
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”);
val BoundOutput_t =
mk_var("BoundOutput", “:^newty0 -> string -> ^newty1 -> ^newty2”);
val BoundOutput_def = new_definition(
"BoundOutput_def",
“^BoundOutput_t a x P = ^term_ABS_t2 (GLAM x (INR (INL ()))
Expand Down Expand Up @@ -369,7 +358,8 @@ val InputR_def' = prove(
InputR_termP]);

(* Free output (residual) *)
val FreeOutput_t = mk_var("FreeOutput", “:^newty0 -> ^newty0 -> ^newty1 -> ^newty2”);
val FreeOutput_t =
mk_var("FreeOutput", “:^newty0 -> ^newty0 -> ^newty1 -> ^newty2”);
val FreeOutput_def = new_definition(
"FreeOutput_def",
“^FreeOutput_t a b P = ^term_ABS_t2 (GLAM ARB (INR (INR (INR (INL ())))) []
Expand All @@ -378,7 +368,7 @@ val FreeOutput_def = new_definition(
^term_REP_t1 P])”);
val FreeOutput_tm = FreeOutput_def |> concl |> strip_forall |> snd |> rhs |> rand;
val FreeOutput_termP = prove(
“^termP2 ^FreeOutput_tm”,
mk_comb(termP2, FreeOutput_tm),
match_mp_tac glam >> srw_tac [][genind_term_REP0,genind_term_REP1]);
val FreeOutput_t = defined_const FreeOutput_def;
val FreeOutput_def' = prove(
Expand Down

0 comments on commit a80b821

Please sign in to comment.