Skip to content

Commit

Permalink
Stage work on D-transitions
Browse files Browse the repository at this point in the history
  • Loading branch information
@binghe
binghe committed Mar 2, 2025
1 parent 4779040 commit 95db595
Show file tree
Hide file tree
Showing 2 changed files with 226 additions and 34 deletions.
75 changes: 73 additions & 2 deletions examples/formal-languages/pi-calculus/open_bisimulationScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ();
Expand Down
185 changes: 153 additions & 32 deletions examples/formal-languages/pi-calculus/pi_agentScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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”);
Expand All @@ -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”);
Expand All @@ -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
Expand All @@ -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 :
Expand All @@ -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 :
Expand All @@ -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)
---------------------------------------------------------------------- *)
Expand Down Expand Up @@ -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
---------------------------------------------------------------------- *)
Expand Down

0 comments on commit 95db595

Please sign in to comment.