Skip to content

Commit

Permalink
Re-worked CCS example with alpha-equivalent recursion variable
Browse files Browse the repository at this point in the history
  • Loading branch information
@binghe @mn200
binghe authored and mn200 committed Jan 11, 2024
1 parent c4c8009 commit 02061e4
Show file tree
Hide file tree
Showing 30 changed files with 4,408 additions and 3,608 deletions.
38 changes: 19 additions & 19 deletions examples/CCS/BisimulationUptoScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ val _ = new_theory "BisimulationUpto";
(* Define the strong bisimulation relation up to STRONG_EQUIV *)
val STRONG_BISIM_UPTO = new_definition (
"STRONG_BISIM_UPTO",
``STRONG_BISIM_UPTO (Bsm :('a, 'b) simulation) =
``STRONG_BISIM_UPTO (Bsm :'a simulation) =
!E E'.
Bsm E E' ==>
!u. (!E1. TRANS E u E1 ==>
Expand All @@ -45,14 +45,14 @@ val IDENTITY_STRONG_BISIM_UPTO = store_thm (
PURE_ONCE_REWRITE_TAC [STRONG_BISIM_UPTO]
>> rpt STRIP_TAC (* 2 sub-goals *)
>| [ (* goal 1 *)
ASSUME_TAC (REWRITE_RULE [ASSUME ``E:('a, 'b) CCS = E'``]
ASSUME_TAC (REWRITE_RULE [ASSUME ``E:'a CCS = E'``]
(ASSUME ``TRANS E u E1``)) \\
EXISTS_TAC ``E1 :('a, 'b) CCS`` \\
EXISTS_TAC ``E1 :'a CCS`` \\
ASM_REWRITE_TAC [] \\
REWRITE_TAC [IDENTITY_STRONG_BISIM_UPTO_lemma],
(* goal 2 *)
PURE_ONCE_ASM_REWRITE_TAC [] \\
EXISTS_TAC ``E2 :('a, 'b) CCS`` \\
EXISTS_TAC ``E2 :'a CCS`` \\
ASM_REWRITE_TAC [] \\
REWRITE_TAC [IDENTITY_STRONG_BISIM_UPTO_lemma] ]);

Expand Down Expand Up @@ -164,7 +164,7 @@ val STRONG_BISIM_UPTO_THM = store_thm (
>> IMP_RES_TAC STRONG_BISIM_SUBSET_STRONG_EQUIV
>> Suff `Bsm RSUBSET (STRONG_EQUIV O Bsm O STRONG_EQUIV)`
>- ( DISCH_TAC \\
Know `transitive ((RSUBSET) :('a, 'b) simulation -> ('a, 'b) simulation -> bool)`
Know `transitive ((RSUBSET) :'a simulation -> 'a simulation -> bool)`
>- PROVE_TAC [RSUBSET_WeakOrder, WeakOrder] \\
RW_TAC std_ss [transitive_def] >> RES_TAC )
>> KILL_TAC
Expand Down Expand Up @@ -194,7 +194,7 @@ val STRONG_EQUIV_BY_BISIM_UPTO = store_thm (
*)
val WEAK_BISIM_UPTO = new_definition (
"WEAK_BISIM_UPTO",
``WEAK_BISIM_UPTO (Wbsm: ('a, 'b) simulation) =
``WEAK_BISIM_UPTO (Wbsm: 'a simulation) =
!E E'. Wbsm E E' ==>
(!l.
(!E1. TRANS E (label l) E1 ==>
Expand Down Expand Up @@ -260,7 +260,7 @@ val IDENTITY_WEAK_BISIM_UPTO = store_thm (
PURE_ONCE_REWRITE_TAC [WEAK_BISIM_UPTO]
>> rpt STRIP_TAC (* 4 sub-goals here *)
>| [ (* goal 1 (of 4) *)
ASSUME_TAC (REWRITE_RULE [ASSUME ``E :('a, 'b) CCS = E'``]
ASSUME_TAC (REWRITE_RULE [ASSUME ``E :'a CCS = E'``]
(ASSUME ``TRANS E (label l) E1``)) \\
IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\
Q.EXISTS_TAC `E1` >> art [] \\
Expand All @@ -270,7 +270,7 @@ val IDENTITY_WEAK_BISIM_UPTO = store_thm (
Q.EXISTS_TAC `E2` >> art [] \\
REWRITE_TAC [IDENTITY_WEAK_BISIM_UPTO_lemma'],
(* goal 3 (of 4) *)
ASSUME_TAC (REWRITE_RULE [ASSUME ``E :('a, 'b) CCS = E'``]
ASSUME_TAC (REWRITE_RULE [ASSUME ``E :'a CCS = E'``]
(ASSUME ``TRANS E tau E1``)) \\
IMP_RES_TAC ONE_TAU \\
Q.EXISTS_TAC `E1` >> art [] \\
Expand Down Expand Up @@ -585,7 +585,7 @@ val WEAK_BISIM_UPTO_THM = store_thm (
>> IMP_RES_TAC WEAK_BISIM_SUBSET_WEAK_EQUIV
>> Suff `Wbsm RSUBSET (WEAK_EQUIV O Wbsm O WEAK_EQUIV)`
>- ( DISCH_TAC \\
Know `transitive ((RSUBSET) :('a, 'b) simulation -> ('a, 'b) simulation -> bool)`
Know `transitive ((RSUBSET) :'a simulation -> 'a simulation -> bool)`
>- PROVE_TAC [RSUBSET_WeakOrder, WeakOrder] \\
RW_TAC std_ss [transitive_def] >> RES_TAC )
>> KILL_TAC
Expand All @@ -612,7 +612,7 @@ val WEAK_EQUIV_BY_BISIM_UPTO = store_thm (
corrected Definition 5.8 in the ERRATA (1990) of [1]. *)
val WEAK_BISIM_UPTO_ALT = new_definition (
"WEAK_BISIM_UPTO_ALT",
``WEAK_BISIM_UPTO_ALT (Wbsm: ('a, 'b) simulation) =
``WEAK_BISIM_UPTO_ALT (Wbsm: 'a simulation) =
!E E'. Wbsm E E' ==>
(!l.
(!E1. WEAK_TRANS E (label l) E1 ==>
Expand Down Expand Up @@ -779,7 +779,7 @@ val WEAK_BISIM_UPTO_ALT_THM = store_thm (
>> IMP_RES_TAC WEAK_BISIM_SUBSET_WEAK_EQUIV
>> Suff `Wbsm RSUBSET (WEAK_EQUIV O Wbsm O WEAK_EQUIV)`
>- ( DISCH_TAC \\
Know `transitive ((RSUBSET) :('a, 'b) simulation -> ('a, 'b) simulation -> bool)`
Know `transitive ((RSUBSET) :'a simulation -> 'a simulation -> bool)`
>- PROVE_TAC [RSUBSET_WeakOrder, WeakOrder] \\
RW_TAC std_ss [transitive_def] >> RES_TAC )
>> KILL_TAC
Expand All @@ -805,7 +805,7 @@ val WEAK_EQUIV_BY_BISIM_UPTO_ALT = store_thm (
(* this work is now useless *)
val OBS_BISIM_UPTO = new_definition (
"OBS_BISIM_UPTO",
``OBS_BISIM_UPTO (Obsm: ('a, 'b) simulation) =
``OBS_BISIM_UPTO (Obsm: 'a simulation) =
!E E'. Obsm E E' ==>
!u. (!E1. TRANS E u E1 ==>
?E2. WEAK_TRANS E' u E2 /\ (WEAK_EQUIV O Obsm O STRONG_EQUIV) E1 E2) /\
Expand Down Expand Up @@ -833,7 +833,7 @@ val IDENTITY_OBS_BISIM_UPTO = store_thm (
PURE_ONCE_REWRITE_TAC [OBS_BISIM_UPTO]
>> rpt STRIP_TAC (* 2 sub-goals here *)
>| [ (* goal 1 (of 4) *)
ASSUME_TAC (REWRITE_RULE [ASSUME ``E :('a, 'b) CCS = E'``]
ASSUME_TAC (REWRITE_RULE [ASSUME ``E :'a CCS = E'``]
(ASSUME ``TRANS E u E1``)) \\
IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\
Q.EXISTS_TAC `E1` >> art [] \\
Expand Down Expand Up @@ -1195,16 +1195,16 @@ val OBS_CONGR_BY_BISIM_UPTO = store_thm (
>> irule (REWRITE_RULE [RSUBSET] OBS_BISIM_UPTO_THM)
>> Q.EXISTS_TAC `Obsm` >> art []);

val _ = export_theory ();
val _ = html_theory "BisimulationUpto";

(* Bibliography:
*
* [1] Milner, R.: Communication and concurrency. (1989).
.* [2] Gorrieri, R., Versari, C.: Introduction to Concurrency Theory. Springer, Cham (2015).
* [3] Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011).
* [2] Gorrieri, R., Versari, C.: Introduction to Concurrency Theory. Springer, Cham (2015).
* [3] Sangiorgi, D.: Introduction to Bisimulation and Coinduction.
Cambridge University Press (2011).
* [4] Sangiorgi, D., Rutten, J.: Advanced Topics in Bisimulation and Coinduction.
Cambridge University Press (2011).
*)

val _ = export_theory ();
val _ = html_theory "BisimulationUpto";

(* last updated: Aug 5, 2017 *)
21 changes: 4 additions & 17 deletions examples/CCS/CCSLib.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,8 @@ struct

open HolKernel Parse boolLib bossLib;

open hurdUtils;

(******************************************************************************)
(* *)
(* Backward compatibility and utility tactic/tacticals (2019) *)
Expand All @@ -19,15 +21,6 @@ open HolKernel Parse boolLib bossLib;
fun fix ts = MAP_EVERY Q.X_GEN_TAC ts; (* from HOL Light *)
fun unset ts = MAP_EVERY Q.UNABBREV_TAC ts; (* from HOL mizar mode *)
fun take ts = MAP_EVERY Q.EXISTS_TAC ts; (* from HOL mizar mode *)
val Know = Q_TAC KNOW_TAC; (* from util_prob *)
val Suff = Q_TAC SUFF_TAC; (* from util_prob *)
fun K_TAC _ = ALL_TAC; (* from util_prob *)
val KILL_TAC = POP_ASSUM_LIST K_TAC; (* from util_prob *)
fun wrap a = [a]; (* from util_prob *)
val art = ASM_REWRITE_TAC;
val Rewr = DISCH_THEN (REWRITE_TAC o wrap); (* from util_prob *)
val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap);
val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]);

fun PRINT_TAC s gl = (* from cardinalTheory *)
(print ("** " ^ s ^ "\n"); ALL_TAC gl);
Expand All @@ -37,12 +30,6 @@ fun COUNT_TAC tac g = (* from Konrad Slind *)
val _ = print ("subgoals: " ^ Int.toString (List.length sg) ^ "\n")
in res end;

local
val th = prove (``!a b. a /\ (a ==> b) ==> a /\ b``, PROVE_TAC [])
in
val STRONG_CONJ_TAC :tactic = MATCH_MP_TAC th >> CONJ_TAC
end;

fun NDISJ_TAC n = (NTAC n DISJ2_TAC) >> TRY DISJ1_TAC;

(******************************************************************************)
Expand Down Expand Up @@ -124,11 +111,11 @@ fun STRIP_FORALL_RULE f th =

(* The rule EQ_IMP_LR returns the implication from left to right of a given
equational theorem. *)
val EQ_IMP_LR = STRIP_FORALL_RULE (fst o EQ_IMP_RULE);
val EQ_IMP_LR = iffLR; (* STRIP_FORALL_RULE (fst o EQ_IMP_RULE); *)

(* The rule EQ_IMP_RL returns the implication from right to left of a given
equational theorem. *)
val EQ_IMP_RL = STRIP_FORALL_RULE (snd o EQ_IMP_RULE);
val EQ_IMP_RL = iffRL; (* STRIP_FORALL_RULE (snd o EQ_IMP_RULE); *)

(* Functions to get the left and right hand side of the equational conclusion
of a theorem. *)
Expand Down
Loading

0 comments on commit 02061e4

Please sign in to comment.