From ef22441e35fb589b9cb17f4c13dc045938d35596 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Tue, 9 Jan 2024 22:11:02 +1100 Subject: [PATCH] More additions (REC, I_def, I_NO_TRANS, etc.) --- examples/CCS/CCSConv.sml | 20 ++- examples/CCS/CCSScript.sml | 138 ++++++++++++++---- examples/CCS/MultivariateScript.sml | 9 +- examples/CCS/StrongLawsScript.sml | 213 ++++++++++++++++------------ 4 files changed, 247 insertions(+), 133 deletions(-) diff --git a/examples/CCS/CCSConv.sml b/examples/CCS/CCSConv.sml index 0620380d6d..18260eab89 100644 --- a/examples/CCS/CCSConv.sml +++ b/examples/CCS/CCSConv.sml @@ -1,7 +1,11 @@ -(* - * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) - * Copyright 2016-2017 University of Bologna (Author: Chun Tian) - *) +(* ========================================================================== *) +(* FILE : StrongLawsScript.sml *) +(* DESCRIPTION : Laws of strong equivalence (STRONG_EQUIV) *) +(* *) +(* COPYRIGHTS : 1991-1995 University of Cambridge, UK (Monica Nesi) *) +(* 2016-2017 University of Bologna, Italy (Chun Tian) *) +(* 2023-2024 The Australian National University (Chun Tian) *) +(******************************************************************************) structure CCSConv :> CCSConv = struct @@ -535,7 +539,11 @@ fun CCS_TRANS_CONV tm = val thmS = SIMP_CONV (srw_ss ()) [CCS_Subst_def] ``CCS_Subst ^P ^tm ^X``; val thm = CCS_TRANS_CONV (rconcl thmS) in - GEN_ALL (REWRITE_CONV [TRANS_REC_EQ, thmS, thm] ``TRANS ^tm u E``) + (* NOTE: for the new [REC], CCS_distinct' can be used to eliminate the + extra ‘E <> var X’ generated by TRANS_REC_EQ. + *) + GEN_ALL (REWRITE_CONV [TRANS_REC_EQ, CCS_distinct', thmS, thm] + ``TRANS ^tm u E``) end (* val (X, P) *) else (* no need to distinguish on (rconcl thm) *) failwith "CCS_TRANS_CONV"; @@ -559,5 +567,3 @@ end; (* local *) (* moved to selftest.sml *) end (* struct *) - -(* last updated: May 15, 2017 *) diff --git a/examples/CCS/CCSScript.sml b/examples/CCS/CCSScript.sml index 10b17bb300..ad87212957 100644 --- a/examples/CCS/CCSScript.sml +++ b/examples/CCS/CCSScript.sml @@ -15,6 +15,8 @@ open pred_setTheory pred_setLib relationTheory optionTheory listTheory CCSLib open generic_termsTheory binderLib nomsetTheory nomdatatype; +local open termTheory; in end; (* for SUB's syntax only *) + val _ = new_theory "CCS"; val set_ss = std_ss ++ PRED_SET_ss; @@ -803,10 +805,6 @@ Theorem parameter_tm_recursion = ‘dpm’ |-> ‘apm’] |> CONV_RULE (REDEPTH_CONV sort_uvars) -val FORALL_ONE = oneTheory.FORALL_ONE; -val FORALL_ONE_FN = oneTheory.FORALL_ONE_FN; -val EXISTS_ONE_FN = oneTheory.EXISTS_ONE_FN; - Theorem tm_recursion = parameter_tm_recursion |> Q.INST_TYPE [‘:'q’ |-> ‘:unit’] @@ -819,8 +817,8 @@ Theorem tm_recursion = ‘rs’ |-> ‘\r L t u. rsu (r()) L t’, ‘rl’ |-> ‘\r t rf u. rlu (r()) t rf’, ‘re’ |-> ‘\r v t u. reu (r()) v t’] - |> SIMP_RULE (srw_ss()) [FORALL_ONE, FORALL_ONE_FN, EXISTS_ONE_FN, - fnpm_def] + |> SIMP_RULE (srw_ss()) [oneTheory.FORALL_ONE, oneTheory.FORALL_ONE_FN, + oneTheory.EXISTS_ONE_FN, fnpm_def] |> SIMP_RULE (srw_ss() ++ CONJ_ss) [supp_unitfn] |> Q.INST [‘vru’ |-> ‘vr’, ‘nlu’ |-> ‘nl’, @@ -1009,14 +1007,7 @@ val subst_exists = val SUB_DEF = new_specification("SUB_DEF", ["SUB"], subst_exists); -val _ = add_rule {term_name = "SUB", fixity = Closefix, - pp_elements = [TOK "[", TM, TOK "/", TM, TOK "]"], - paren_style = OnlyIfNecessary, - block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2))}; - -val _ = TeX_notation { hol = "[", TeX = ("\\ensuremath{[}", 1) }; -val _ = TeX_notation { hol = "/", TeX = ("\\ensuremath{/}", 1) }; -val _ = TeX_notation { hol = "]", TeX = ("\\ensuremath{]}", 1) }; +Overload SUB = “SUB”; (* use the syntax already defined in termTheory *) val SUB_THMv = prove( “([N/x](var x) = (N :'a CCS)) /\ (x <> y ==> [N/y](var x) = var x)”, @@ -1737,6 +1728,8 @@ Type transition[pp] = “:'a CCS -> 'a Action -> 'a CCS -> bool” (* Inductive definition of the transition relation TRANS for CCS. TRANS: CCS -> Action -> CCS -> bool + + NOTE: added ‘E <> var X’ into [REC] to prove I_NO_TRANS (see below). *) Inductive TRANS : (!E u. TRANS (prefix u E) u E) /\ (* PREFIX *) @@ -1751,7 +1744,7 @@ Inductive TRANS : ==> TRANS (restr L E) u (restr L E')) /\ (* RESTR *) (!E u E' rf. TRANS E u E' ==> TRANS (relab E rf) (relabel rf u) (relab E' rf)) /\ (* RELABELING *) - (!E u X E1. TRANS (CCS_Subst E (rec X E) X) u E1 + (!E u X E1. TRANS (CCS_Subst E (rec X E) X) u E1 /\ E <> var X ==> TRANS (rec X E) u E1) (* REC *) End @@ -1798,10 +1791,77 @@ QED (* An recursion variable has no transition. !X u E. ~TRANS (var X) u E *) -val VAR_NO_TRANS = save_thm ("VAR_NO_TRANS", +Theorem VAR_NO_TRANS = Q.GENL [`X`, `u`, `E`] (REWRITE_RULE [CCS_distinct', CCS_one_one] - (Q.SPECL [`var X`, `u`, `E`] TRANS_cases))); + (Q.SPECL [`var X`, `u`, `E`] TRANS_cases)) + +val _ = hide "I"; + +(* cf. chap2Theory (examples/lambda/barendregt) *) +Definition I_def : + I = rec "x" (var "x") +End + +Theorem FV_I[simp] : + FV I = {} +Proof + SRW_TAC [][I_def] +QED + +Theorem I_thm : + !X. I = rec X (var X) +Proof + Q.X_GEN_TAC ‘x’ + >> REWRITE_TAC [I_def, Once EQ_SYM_EQ] + >> Cases_on ‘x = "x"’ >- rw [] + >> qabbrev_tac ‘u = var x’ + >> qabbrev_tac ‘y = "x"’ + >> ‘y NOTIN FV u’ by rw [Abbr ‘u’] + >> Know ‘rec x u = rec y ([var y/x] u)’ + >- (MATCH_MP_TAC SIMPLE_ALPHA >> art []) + >> Rewr' + >> Suff ‘[var y/x] u = var y’ >- rw [] + >> rw [Abbr ‘u’] +QED + +Theorem SUB_I[simp] : + [N/v] I = I +Proof + rw [lemma14b] +QED + +Theorem ssub_I : + ssub fm I = I +Proof + rw [ssub_value] +QED + +Theorem I_cases : + I = rec Y P ==> P = var Y +Proof + rw [I_def] + >> qabbrev_tac ‘X = "x"’ + >> Cases_on ‘X = Y’ >> fs [rec_eq_thm] +QED + +(* NOTE: This proof is only possible under the modified [REC] *) +Theorem REC_VAR_NO_TRANS : + !X u E. ~TRANS (rec X (var X)) u E +Proof + rw [Once TRANS_cases, CCS_Subst] + >> DISJ2_TAC + >> fs [GSYM I_thm, I_cases] +QED + +(* |- !u E. ~(I --u-> E) *) +Theorem I_NO_TRANS = REWRITE_RULE [GSYM I_thm] REC_VAR_NO_TRANS + +(******************************************************************************) +(* *) +(* The transitions of prefixed term *) +(* *) +(******************************************************************************) (* !u E u' E'. TRANS (prefix u E) u' E' <=> (u' = u) /\ (E' = E) *) Theorem TRANS_PREFIX_EQ = @@ -2164,31 +2224,52 @@ val REC_cases_EQ = save_thm val REC_cases = save_thm ("REC_cases", EQ_IMP_LR REC_cases_EQ); +Theorem VAR_lemma[local] : + X # P ==> var X = [var X/Y] P ==> X <> Y ==> P = var Y +Proof + MP_TAC (Q.SPEC ‘P’ CCS_cases) >> rw [] + >> fs [] (* 3 subgoals left *) + >| [ (* goal 1 (of 3) *) + rename1 ‘Z = Y’ >> CCONTR_TAC >> fs [SUB_THM], + (* goal 2 (of 3) *) + rename1 ‘var X = [var X/Y] (rec Z E)’ \\ + Q_TAC (NEW_TAC "Z'") ‘{X;Y;Z} UNION FV E’ \\ + Know ‘rec Z E = rec Z' ([var Z'/Z] E)’ + >- (MATCH_MP_TAC SIMPLE_ALPHA >> art []) \\ + DISCH_THEN (fs o wrap), + (* goal 3 (of 3) *) + Q.PAT_X_ASSUM ‘X = X'’ (fs o wrap o SYM) \\ + Q_TAC (NEW_TAC "Z") ‘{X;Y} UNION FV E’ \\ + Know ‘rec X E = rec Z ([var Z/X] E)’ + >- (MATCH_MP_TAC SIMPLE_ALPHA >> art []) \\ + DISCH_THEN (fs o wrap) ] +QED + Theorem TRANS_REC_EQ : - !X E u E'. TRANS (rec X E) u E' <=> TRANS (CCS_Subst E (rec X E) X) u E' + !X E u E'. TRANS (rec X E) u E' <=> TRANS (CCS_Subst E (rec X E) X) u E' /\ E <> var X Proof rpt GEN_TAC >> reverse EQ_TAC >- PURE_ONCE_REWRITE_TAC [REC] >> PURE_ONCE_REWRITE_TAC [REC_cases_EQ] - >> rpt STRIP_TAC + >> STRIP_TAC + >> rename1 ‘rec X E = rec Y P’ >> fs [rec_eq_thm, CCS_Subst] - >> rename1 ‘X <> Y’ - >> rename1 ‘X # P’ - (* stage work *) - >> rw [fresh_tpm_subst] + >> Q.PAT_X_ASSUM ‘E = _’ K_TAC + >> simp [fresh_tpm_subst] >> Q.ABBREV_TAC ‘E = [var X/Y] P’ >> Know ‘rec X E = rec Y ([var Y/X] E)’ >- (MATCH_MP_TAC SIMPLE_ALPHA \\ rw [Abbr ‘E’, FV_SUB]) >> Rewr' - >> rw [Abbr ‘E’] + >> simp [Abbr ‘E’] >> Know ‘[var Y/X] ([var X/Y] P) = P’ >- (MATCH_MP_TAC lemma15b >> art []) >> Rewr' - >> Suff ‘[rec Y P/X] ([var X/Y] P) = [rec Y P/Y] P’ - >- rw [] - >> MATCH_MP_TAC lemma15a >> art [] + >> Know ‘[rec Y P/X] ([var X/Y] P) = [rec Y P/Y] P’ + >- (MATCH_MP_TAC lemma15a >> art []) + >> Rewr' >> art [] + >> METIS_TAC [VAR_lemma] QED val TRANS_REC = save_thm ("TRANS_REC", EQ_IMP_LR TRANS_REC_EQ); @@ -2201,8 +2282,7 @@ Proof >> TRY (ASM_SET_TAC []) (* 1 - 6 *) >> MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC `FV (CCS_Subst E (rec X E) X)` - >> POP_ASSUM (REWRITE_TAC o wrap) - >> REWRITE_TAC [FV_SUBSET_REC'] + >> ASM_REWRITE_TAC [FV_SUBSET_REC'] QED Theorem TRANS_PROC : diff --git a/examples/CCS/MultivariateScript.sml b/examples/CCS/MultivariateScript.sml index 0cf0c9fc41..2175fa6d56 100644 --- a/examples/CCS/MultivariateScript.sml +++ b/examples/CCS/MultivariateScript.sml @@ -3028,7 +3028,7 @@ Proof >> fs [CCS_equation_def, CCS_solution_def, EVERY_MEM, LIST_REL_EL_EQN] QED -(* THE FINAL THEOREM (Theorem 3.13 of [3], full version) *) +(* THE FINAL THEOREM (Theorem 3.16 of [3]) *) Theorem unique_solution_of_rooted_contractions : !Xs Es Ps Qs. CCS_equation Xs Es /\ EVERY (weakly_guarded Xs) Es /\ @@ -3100,11 +3100,8 @@ val _ = html_theory "Multivariate"; solutions." ACM Transactions on Computational Logic (TOCL) 18.1 (2017): 4. (DOI: 10.1145/2971339) - [3] Tian, Chun, and Davide Sangiorgi. "Unique Solutions of - Contractions, CCS, and their HOL Formalisation." Combined 25th - International Workshop on Expressiveness in Concurrency and 15th - Workshop on Structural Operational Semantics (EXPRESS/SOS - 2018). Vol. 276. No. 4. 2018. (DOI: 10.4204/EPTCS.276.10) + [3] C. Tian and D. Sangiorgi, “Unique solutions of contractions, CCS, and + their HOL formalisation,” Inf. Comput., vol. 275, p. 104606, Dec. 2020. [4] Gorrieri, R., Versari, C.: Introduction to Concurrency Theory. Springer, Cham (2015). diff --git a/examples/CCS/StrongLawsScript.sml b/examples/CCS/StrongLawsScript.sml index 0fd54a4335..4f4d5fb40a 100644 --- a/examples/CCS/StrongLawsScript.sml +++ b/examples/CCS/StrongLawsScript.sml @@ -1,8 +1,12 @@ -(* - * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) - * Copyright 2016-2017 University of Bologna (Author: Chun Tian) - * Copyright 2019 Fondazione Bruno Kessler, Italy (Author: Chun Tian) - *) +(* ========================================================================== *) +(* FILE : StrongLawsScript.sml *) +(* DESCRIPTION : Laws of strong equivalence (STRONG_EQUIV) *) +(* *) +(* COPYRIGHTS : 1991-1995 University of Cambridge, UK (Monica Nesi) *) +(* 2016-2017 University of Bologna, Italy (Chun Tian) *) +(* 2018-2019 Fondazione Bruno Kessler, Italy (Chun Tian) *) +(* 2023-2024 The Australian National University (Chun Tian) *) +(******************************************************************************) open HolKernel Parse boolLib bossLib; @@ -11,7 +15,6 @@ open pred_setTheory prim_recTheory arithmeticTheory relationTheory; open CCSLib CCSTheory StrongEQTheory StrongEQLib; val _ = new_theory "StrongLaws"; -val _ = temp_loose_equality (); (******************************************************************************) (* *) @@ -1105,20 +1108,24 @@ val STRONG_RELAB_PREFIX = store_thm ( If A := P, then A ~ P where A is ‘rec X E’, P is ‘CCS_Subst E (rec X E) X’ (instead of just E) + + NOTE: this proof has been fixed due to changed [REC]. --binghe, 9 gen 2024 *) Theorem STRONG_UNFOLDING : !X E. STRONG_EQUIV (rec X E) (CCS_Subst E (rec X E) X) Proof rpt GEN_TAC + >> Cases_on ‘E = var X’ >- rw [] >> PURE_ONCE_REWRITE_TAC [STRONG_EQUIV] - >> EXISTS_TAC - ``\x y. (x = y) \/ - (?Y E'. (x = rec Y E') /\ (y = CCS_Subst E' (rec Y E') Y))`` + >> Q.EXISTS_TAC + ‘\x y. x = y \/ + ?Y E'. x = rec Y E' /\ y = CCS_Subst E' (rec Y E') Y /\ E' <> var Y’ >> CONJ_TAC (* 2 sub-goals here *) >| [ (* goal 1 (of 2) *) BETA_TAC >> DISJ2_TAC \\ qexistsl_tac [‘X’, ‘E’] >> rw [], (* goal 2 (of 2) *) + POP_ASSUM K_TAC \\ PURE_ONCE_REWRITE_TAC [STRONG_BISIM] >> BETA_TAC \\ rpt STRIP_TAC >| (* 4 sub-goals here *) [ (* goal 2.1 (of 4) *) @@ -1142,11 +1149,11 @@ QED (* Prove the theorem STRONG_PREF_REC_EQUIV: |- ∀u s v. u..rec s (v..u..var s) ~ rec s (u..v..var s): *) -val STRONG_PREF_REC_EQUIV = store_thm ( - "STRONG_PREF_REC_EQUIV", - ``!(u :'a Action) s v. +Theorem STRONG_PREF_REC_EQUIV : + !(u :'a Action) s v. STRONG_EQUIV (prefix u (rec s (prefix v (prefix u (var s))))) - (rec s (prefix u (prefix v (var s))))``, + (rec s (prefix u (prefix v (var s)))) +Proof rpt GEN_TAC >> PURE_ONCE_REWRITE_TAC [STRONG_EQUIV] >> EXISTS_TAC @@ -1157,66 +1164,61 @@ val STRONG_PREF_REC_EQUIV = store_thm ( (x = rec s' (prefix v' (prefix u' (var s')))) /\ (y = prefix v' (rec s' (prefix u' (prefix v' (var s')))))`` >> CONJ_TAC (* 2 sub-goals *) - >| [ (* goal 1 (of 2) *) - BETA_TAC \\ - take [`u`, `v`, `s`] >> REWRITE_TAC [], - (* goal 2 (of 2) *) - PURE_ONCE_REWRITE_TAC [STRONG_BISIM] \\ - BETA_TAC \\ - rpt STRIP_TAC >| (* 4 sub-goals *) - [ (* goal 2.1 (of 4) *) - ASSUME_TAC + >- (BETA_TAC >> take [`u`, `v`, `s`] >> REWRITE_TAC []) + >> PURE_ONCE_REWRITE_TAC [STRONG_BISIM] + >> BETA_TAC + >> rpt STRIP_TAC (* 4 sub-goals *) + >| [ (* goal 1 (of 4) *) + ASSUME_TAC (REWRITE_RULE [ASSUME ``E = prefix u' (rec s' (prefix v' (prefix u' (var s'))))``] - (ASSUME ``TRANS E u E1``)) \\ - IMP_RES_TAC TRANS_PREFIX \\ - EXISTS_TAC ``prefix (v' :'a Action) (rec s' (prefix u' (prefix v' (var s'))))`` \\ - CONJ_TAC >| (* 2 sub-goals here *) - [ (* goal 2.1.1 (of 2) *) - art [] \\ - MATCH_MP_TAC REC \\ - REWRITE_TAC [CCS_Subst_def, PREFIX], - (* goal 2.1.2 (of 2) *) - take [`u'`, `v'`, `s'`] >> art [] ], - (* goal 2.2 (of 4) *) - ASSUME_TAC (REWRITE_RULE + (ASSUME ``TRANS E u E1``)) >> fs [] \\ + IMP_RES_TAC TRANS_PREFIX \\ + EXISTS_TAC ``prefix (v' :'a Action) (rec s' (prefix u' (prefix v' (var s'))))`` \\ + CONJ_TAC >| (* 2 sub-goals here *) + [ (* goal 1.1 (of 2) *) + art [] >> MATCH_MP_TAC REC >> rw [CCS_Subst_def, PREFIX], + (* goal 1.2 (of 2) *) + take [`u'`, `v'`, `s'`] >> art [] ], + (* goal 2 (of 4) *) + ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = rec s' (prefix u' (prefix v' (var s')))``, TRANS_REC_EQ, CCS_Subst_def] - (ASSUME ``TRANS E' u E2``)) \\ - IMP_RES_TAC TRANS_PREFIX \\ - EXISTS_TAC ``rec s' (prefix v' (prefix u (var s')))`` \\ - CONJ_TAC >| (* 2 sub-goals here, first one is easy *) - [ (* goal 2.2.1 (of 2) *) - art [PREFIX], - (* goal 2.2.2 (of 2) *) - take [`u`, `v'`, `s'`] >> art - [REWRITE_RULE [ASSUME ``u' :'a Action = u``] + (ASSUME ``TRANS E' u E2``)) >> fs [] \\ + IMP_RES_TAC TRANS_PREFIX \\ + EXISTS_TAC ``rec s' (prefix v' (prefix u (var s')))`` \\ + CONJ_TAC >| (* 2 sub-goals here, first one is easy *) + [ (* goal 2.1 (of 2) *) + art [PREFIX], + (* goal 2.2 (of 2) *) + take [`u`, `v'`, `s'`] \\ + art [REWRITE_RULE [ASSUME ``u' :'a Action = u``] (ASSUME ``E2 = prefix v' (rec s' (prefix u' (prefix v' (var s'))))``)] ], - (* goal 2.3 (of 4) *) - ASSUME_TAC (REWRITE_RULE - [ASSUME ``E = rec s' (prefix v' (prefix u' (var s')))``, - TRANS_REC_EQ, CCS_Subst_def] - (ASSUME ``TRANS E u E1``)) \\ - IMP_RES_TAC TRANS_PREFIX \\ - EXISTS_TAC ``rec s' (prefix u' (prefix v' (var s')))`` \\ - CONJ_TAC >| (* 2 sub-goals here, first one is easy *) - [ (* goal 2.3.1 (of 2) *) - art [PREFIX], - (* goal 2.3.2 (of 2) *) - take [`u'`, `v'`, `s'`] >> art [] ], - (* goal 2.4 (of 4) *) - ASSUME_TAC (REWRITE_RULE - [ASSUME ``E' = prefix v' (rec s' (prefix u' (prefix v' (var s'))))``] - (ASSUME ``TRANS E' u E2``)) \\ - IMP_RES_TAC TRANS_PREFIX \\ - EXISTS_TAC ``prefix (u' :'a Action) - (rec s' (prefix v' (prefix u' (var s'))))`` \\ - CONJ_TAC >| (* 2 sub-goals here *) - [ (* goal 2.4.1 (of 2) *) - art [] \\ - MATCH_MP_TAC REC >> REWRITE_TAC [CCS_Subst_def, PREFIX], - (* goal 2.4.2 (of 2) *) - take [`u'`, `v'`, `s'`] >> art [] ] ] ]); + (* goal 3 (of 4) *) + ASSUME_TAC (REWRITE_RULE + [ASSUME ``E = rec s' (prefix v' (prefix u' (var s')))``, + TRANS_REC_EQ, CCS_Subst_def] + (ASSUME ``TRANS E u E1``)) >> fs [] \\ + IMP_RES_TAC TRANS_PREFIX \\ + EXISTS_TAC ``rec s' (prefix u' (prefix v' (var s')))`` \\ + CONJ_TAC >| (* 2 sub-goals here, first one is easy *) + [ (* goal 3.1 (of 2) *) + art [PREFIX], + (* goal 3.2 (of 2) *) + take [`u'`, `v'`, `s'`] >> art [] ], + (* goal 4 (of 4) *) + ASSUME_TAC (REWRITE_RULE + [ASSUME ``E' = prefix v' (rec s' (prefix u' (prefix v' (var s'))))``] + (ASSUME ``TRANS E' u E2``)) >> fs [] \\ + IMP_RES_TAC TRANS_PREFIX \\ + EXISTS_TAC ``prefix (u' :'a Action) + (rec s' (prefix v' (prefix u' (var s'))))`` \\ + CONJ_TAC >| (* 2 sub-goals here *) + [ (* goal 4.1 (of 2) *) + art [] >> MATCH_MP_TAC REC >> rw [CCS_Subst_def, PREFIX], + (* goal 4.2 (of 2) *) + take [`u'`, `v'`, `s'`] >> art [] ] ] +QED (* Prove the theorem STRONG_REC_ACT2: |- ∀s u. rec s (u..u..var s) ~ rec s (u..var s) @@ -1245,52 +1247,79 @@ Proof ASSUME_TAC (REWRITE_RULE [ASSUME ``E = rec s' (prefix u' (prefix u' (var s')))``, TRANS_REC_EQ, CCS_Subst_def] - (ASSUME ``TRANS E u E1``)) \\ + (ASSUME ``TRANS E u E1``)) >> fs [] \\ IMP_RES_TAC TRANS_PREFIX >> EXISTS_TAC ``E' :'a CCS`` \\ CONJ_TAC >| (* 2 sub-goals here *) [ (* goal 2.1.1 (of 2) *) - ASM_REWRITE_TAC [] \\ - MATCH_MP_TAC REC >> REWRITE_TAC [CCS_Subst_def, PREFIX], + art [] >> MATCH_MP_TAC REC >> rw [CCS_Subst_def, PREFIX], (* goal 2.1.2 (of 2) *) qexistsl_tac [‘s'’, ‘u'’] >> art [] ], (* goal 2.2 (of 4) *) ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = rec s'(prefix u'(var s'))``, TRANS_REC_EQ, CCS_Subst_def] - (ASSUME ``TRANS E' u E2``)) \\ + (ASSUME ``TRANS E' u E2``)) >> fs [] \\ IMP_RES_TAC TRANS_PREFIX \\ EXISTS_TAC ``prefix (u' :'a Action) E`` \\ CONJ_TAC >| (* 2 sub-goals here *) [ (* goal 2.2.1 (of 2) *) - ASM_REWRITE_TAC [] \\ - MATCH_MP_TAC REC >> REWRITE_TAC [CCS_Subst_def, PREFIX], + art [] >> MATCH_MP_TAC REC >> rw [CCS_Subst_def, PREFIX], (* goal 2.2.2 (of 2) *) qexistsl_tac [‘s'’, ‘u'’] >> art [] ], (* goal 2.3 (of 4) *) ASSUME_TAC (REWRITE_RULE [ASSUME ``E = prefix u' (rec s' (prefix u' (prefix u' (var s'))))``] - (ASSUME ``TRANS E u E1``)) \\ + (ASSUME ``TRANS E u E1``)) >> fs [] \\ IMP_RES_TAC TRANS_PREFIX >> EXISTS_TAC ``E' :'a CCS`` \\ CONJ_TAC >| (* 2 sub-goals here *) [ (* goal 2.3.1 (of 2) *) - ASM_REWRITE_TAC [] \\ - MATCH_MP_TAC REC \\ - REWRITE_TAC [CCS_Subst_def, PREFIX], + art [] >> MATCH_MP_TAC REC >> rw [CCS_Subst_def, PREFIX], (* goal 2.3.2 (of 2) *) qexistsl_tac [‘s'’, ‘u'’] >> art [] ], (* goal 2.4 (of 4) *) ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = rec s' (prefix u' (var s'))``, TRANS_REC_EQ, CCS_Subst_def] - (ASSUME ``TRANS E' u E2``)) \\ + (ASSUME ``TRANS E' u E2``)) >> fs [] \\ IMP_RES_TAC TRANS_PREFIX \\ EXISTS_TAC ``rec s' (prefix u' (prefix u' (var s')))`` \\ CONJ_TAC >| (* 2 sub-goals here, first one is easy *) [ (* goal 2.4.1 (of 2) *) - ASM_REWRITE_TAC [PREFIX], + art [PREFIX], (* goal 2.4.2 (of 2) *) qexistsl_tac [‘s'’, ‘u'’] >> art [] ] ] ] QED +(******************************************************************************) +(* *) +(* The strong laws for the redundant recursion operators *) +(* *) +(******************************************************************************) + +Theorem STRONG_EQUIV_REC_ELIM : + !X E. X # E ==> STRONG_EQUIV (rec X E) E +Proof + rw [Once PROPERTY_STAR] + >| [ (* goal 1 (of 2) *) + fs [TRANS_REC_EQ, CCS_Subst] \\ + Know ‘[rec X E/X] E = E’ + >- (MATCH_MP_TAC lemma14b >> art []) \\ + DISCH_THEN (fs o wrap) \\ + Q.EXISTS_TAC ‘E1’ >> rw [], + (* goal 2 (of 2) *) + Q.EXISTS_TAC ‘E2’ >> reverse (rw [TRANS_REC_EQ, CCS_Subst]) + >- (CCONTR_TAC >> fs [VAR_NO_TRANS]) \\ + Know ‘[rec X E/X] E = E’ + >- (MATCH_MP_TAC lemma14b >> art []) >> rw [] ] +QED + +Theorem STRONG_EQUIV_REC_REC_ELIM : + !X E. STRONG_EQUIV (rec X (rec X E)) (rec X E) +Proof + rpt GEN_TAC + >> MATCH_MP_TAC STRONG_EQUIV_REC_ELIM + >> rw [] +QED + (******************************************************************************) (* *) (* The strong laws for the parallel operator in the general form *) @@ -1399,7 +1428,7 @@ val [ALL_SYNC_BASE, ALL_SYNC_INDUCT] = |- !m n. m < (SUC n) = m <= n *) val LESS_SUC_LESS_EQ' = Q.prove ( - `!m n. m < SUC n = m <= n`, + `!m n. m < SUC n <=> m <= n`, REWRITE_TAC [LESS_EQ, LESS_EQ_MONO]); (* |- ∀n m. m < SUC n ⇒ m ≤ n @@ -1420,9 +1449,9 @@ val LESS_EQ_LESS_EQ_SUC = Q.prove ( >> IMP_RES_TAC LESS_EQ_IMP_LESS_SUC >> IMP_RES_TAC LESS_IMP_LESS_OR_EQ); -val SIGMA_TRANS_THM_EQ = store_thm ( - "SIGMA_TRANS_THM_EQ", - ``!n f (u :'a Action) E. TRANS (SIGMA f n) u E = (?k. k <= n /\ TRANS (f k) u E)``, +Theorem SIGMA_TRANS_THM_EQ : + !n f (u :'a Action) E. TRANS (SIGMA f n) u E <=> ?k. k <= n /\ TRANS (f k) u E +Proof Induct (* 2 sub-goals here *) >| [ (* goal 1 (of 2) *) rpt GEN_TAC \\ @@ -1461,7 +1490,8 @@ val SIGMA_TRANS_THM_EQ = store_thm ( (* goal 2.2.2 (of 2) *) DISJ2_TAC \\ REWRITE_TAC [REWRITE_RULE [ASSUME ``k = SUC n``] - (ASSUME ``TRANS ((f: num -> 'a CCS) k) u E``)] ] ] ]); + (ASSUME ``TRANS ((f: num -> 'a CCS) k) u E``)] ] ] ] +QED (* SIGMA_TRANS_THM = |- ∀u n f E. SIGMA f n --u-> E ⇒ ∃k. k ≤ n ∧ f k --u-> E @@ -1469,12 +1499,12 @@ val SIGMA_TRANS_THM_EQ = store_thm ( val SIGMA_TRANS_THM = save_thm ( "SIGMA_TRANS_THM", EQ_IMP_LR SIGMA_TRANS_THM_EQ); -val SYNC_TRANS_THM_EQ = store_thm ( - "SYNC_TRANS_THM_EQ", - ``!m (u :'a Action) P f v Q. TRANS (SYNC u P f m) v Q = - (?j l. j <= m /\ +Theorem SYNC_TRANS_THM_EQ : + !m (u :'a Action) P f v Q. TRANS (SYNC u P f m) v Q <=> + ?j l. j <= m /\ (u = label l) /\ (PREF_ACT (f j) = label (COMPL l)) /\ - (v = tau) /\ (Q = par P (PREF_PROC (f j))))``, + (v = tau) /\ (Q = par P (PREF_PROC (f j))) +Proof Induct_on `m` (* 2 sub-goals here *) >| [ (* goal 1 (of 2) *) rpt GEN_TAC \\ @@ -1637,7 +1667,8 @@ val SYNC_TRANS_THM_EQ = store_thm ( CHECK_ASSUME_TAC (REWRITE_RULE [ASSUME ``x = COMPL (l :'a Label)``, COMPL_COMPL_LAB, ASSUME ``x' :'a Label = l``] - (ASSUME ``~(x' = COMPL (x :'a Label))``)) ] ] ] ] ] ); + (ASSUME ``~(x' = COMPL (x :'a Label))``)) ] ] ] ] ] +QED (* SYNC_TRANS_THM = |- ∀v u m f Q P.