From fbdc8f631085370c871c50b58817d2e5b679eb88 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Thu, 11 Jan 2024 17:47:34 +1100 Subject: [PATCH] Reverted [REC]; re-worked REC_VAR_NO_TRANS (and I_NO_TRANS) by methods of Ian Shillito --- examples/CCS/CCSConv.sml | 7 +- examples/CCS/CCSScript.sml | 243 +++++++++++++++++++++------- examples/CCS/ExampleScript.sml | 22 +-- examples/CCS/MultivariateScript.sml | 6 +- examples/CCS/StrongLawsScript.sml | 18 +-- 5 files changed, 205 insertions(+), 91 deletions(-) diff --git a/examples/CCS/CCSConv.sml b/examples/CCS/CCSConv.sml index 18260eab89..29d88e3f8d 100644 --- a/examples/CCS/CCSConv.sml +++ b/examples/CCS/CCSConv.sml @@ -4,7 +4,6 @@ (* *) (* 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 = @@ -539,11 +538,7 @@ 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 - (* 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``) + GEN_ALL (REWRITE_CONV [TRANS_REC_EQ, thmS, thm] ``TRANS ^tm u E``) end (* val (X, P) *) else (* no need to distinguish on (rconcl thm) *) failwith "CCS_TRANS_CONV"; diff --git a/examples/CCS/CCSScript.sml b/examples/CCS/CCSScript.sml index ad87212957..7fc197a6d2 100644 --- a/examples/CCS/CCSScript.sml +++ b/examples/CCS/CCSScript.sml @@ -1013,7 +1013,7 @@ val SUB_THMv = prove( “([N/x](var x) = (N :'a CCS)) /\ (x <> y ==> [N/y](var x) = var x)”, SRW_TAC [][SUB_DEF]); -val SUB_COMM = prove( +Theorem SUB_COMM = prove( “!N x x' y (t :'a CCS). x' <> x /\ x' # N ∧ y <> x /\ y # N ==> (tpm [(x',y)] ([N/x] t) = [N/x] (tpm [(x',y)] t))”, @@ -1728,8 +1728,6 @@ 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 *) @@ -1744,7 +1742,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 <> var X + (!E u X E1. TRANS (CCS_Subst E (rec X E) X) u E1 ==> TRANS (rec X E) u E1) (* REC *) End @@ -1765,6 +1763,9 @@ val [PREFIX, SUM1, SUM2, PAR1, PAR2, PAR3, RESTR, RELABELING, REC] = "RELABELING", "REC"], CONJUNCTS TRANS_rules)); +(* Use SUB instead of CCS_Subst *) +Theorem REC' = REWRITE_RULE [CCS_Subst] REC + val TRANS_IND = save_thm ("TRANS_IND", TRANS_ind |> (Q.SPEC `P`) |> GEN_ALL); @@ -1792,15 +1793,19 @@ QED !X u E. ~TRANS (var X) u E *) Theorem VAR_NO_TRANS = - Q.GENL [`X`, `u`, `E`] - (REWRITE_RULE [CCS_distinct', CCS_one_one] - (Q.SPECL [`var X`, `u`, `E`] TRANS_cases)) + TRANS_cases |> Q.SPECL [`var X`, `u`, `E`] + |> REWRITE_RULE [CCS_distinct', CCS_one_one] + |> Q.GENL [`X`, `u`, `E`] + +(*---------------------------------------------------------------------------* + * The "I combinator" of CCS + *---------------------------------------------------------------------------*) val _ = hide "I"; (* cf. chap2Theory (examples/lambda/barendregt) *) Definition I_def : - I = rec "x" (var "x") + I = rec "s" (var "s") End Theorem FV_I[simp] : @@ -1812,17 +1817,8 @@ 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’] + rw [I_def, Once EQ_SYM_EQ] + >> Cases_on ‘X = "s"’ >> rw [rec_eq_thm] QED Theorem SUB_I[simp] : @@ -1838,24 +1834,149 @@ Proof QED Theorem I_cases : - I = rec Y P ==> P = var Y + !Y P. 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 +(* TRANSn is the labelled version of TRANS. *) +Inductive TRANSn : + (!E u. TRANSn 0 (prefix u E) u E) /\ + (!n E u E1 E'. TRANSn n E u E1 ==> TRANSn (SUC n) (sum E E') u E1) /\ + (!n E u E1 E'. TRANSn n E u E1 ==> TRANSn (SUC n) (sum E' E) u E1) /\ + (!n E u E1 E'. TRANSn n E u E1 ==> TRANSn (SUC n) (par E E') u (par E1 E')) /\ + (!n E u E1 E'. TRANSn n E u E1 ==> TRANSn (SUC n) (par E' E) u (par E' E1)) /\ + (!n E l E1 E' E2. TRANSn n E (label l) E1 /\ TRANSn n' E' (label (COMPL l)) E2 + ==> TRANSn (SUC (MAX n n')) (par E E') tau (par E1 E2)) /\ + (!n E u E' l L. TRANSn n E u E' /\ ((u = tau) \/ + ((u = label l) /\ l NOTIN L /\ (COMPL l) NOTIN L)) + ==> TRANSn (SUC n) (restr L E) u (restr L E')) /\ + (!n E u E' rf. TRANSn n E u E' + ==> TRANSn (SUC n) (relab E rf) (relabel rf u) (relab E' rf)) /\ + (!n E u X E1. TRANSn n (CCS_Subst E (rec X E) X) u E1 + ==> TRANSn (SUC n) (rec X E) u E1) +End + +(* The rules for the transition relation TRANS as individual theorems. *) +val [PREFIXn, SUM1n, SUM2n, PAR1n, PAR2n, PAR3n, RESTRn, RELABELINGn, RECn] = + map save_thm + (combine (["PREFIXn", "SUM1n", "SUM2n", "PAR1n", "PAR2n", "PAR3n", + "RESTRn", "RELABELINGn", "RECn"], + CONJUNCTS TRANSn_rules)); + +Theorem TRANS0_cases : + !E u E0. TRANSn 0 E u E0 <=> E = prefix u E0 +Proof + rw [Once TRANSn_cases] +QED + +Theorem RECn_cases_EQ = + TRANSn_cases |> Q.SPECL [‘n’, `rec X E`] + |> REWRITE_RULE [CCS_distinct', CCS_one_one] + |> Q.SPECL [`u`, `E'`] + |> Q.GENL [‘n’, `X`, `E`, `u`, `E'`] + +Theorem RECn_cases = EQ_IMP_LR RECn_cases_EQ + +Theorem TRANS0_REC_EQ : + !X E u E'. TRANSn 0 (rec X E) u E' <=> F Proof - rw [Once TRANS_cases, CCS_Subst] - >> DISJ2_TAC - >> fs [GSYM I_thm, I_cases] + rw [TRANS0_cases] +QED + +Theorem TRANSn_REC_EQ : + !n X E u E'. TRANSn (SUC n) (rec X E) u E' <=> + TRANSn n (CCS_Subst E (rec X E) X) u E' +Proof + rpt GEN_TAC + >> reverse EQ_TAC + >- PURE_ONCE_REWRITE_TAC [RECn] + >> PURE_ONCE_REWRITE_TAC [RECn_cases_EQ] + >> rpt STRIP_TAC + >> fs [rec_eq_thm, CCS_Subst] + >> rename1 ‘X <> Y’ + >> rename1 ‘X # P’ + >> Q.PAT_X_ASSUM ‘n = n'’ (fs o wrap o SYM) + (* stage work *) + >> rw [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’] + >> 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 [] QED -(* |- !u E. ~(I --u-> E) *) -Theorem I_NO_TRANS = REWRITE_RULE [GSYM I_thm] REC_VAR_NO_TRANS +Theorem TRANSn_REC_EQ' = REWRITE_RULE [CCS_Subst] TRANSn_REC_EQ + +Theorem I_NO_TRANSn_lemma[local] : + !X u E n. ~TRANSn n (rec X (var X)) u E +Proof + Induct_on ‘n’ + >- rw [TRANS0_REC_EQ] + >> rw [TRANSn_REC_EQ'] +QED + +(* |- !u E n. ~TRANSn n I u E *) +Theorem I_NO_TRANSn = REWRITE_RULE [GSYM I_thm] I_NO_TRANSn_lemma + +Theorem TRANS_imp_TRANSn : + !E u E'. TRANS E u E' ==> ?n. TRANSn n E u E' +Proof + HO_MATCH_MP_TAC TRANS_ind >> rw [] (* 10 subgoals *) + >- (Q.EXISTS_TAC ‘0’ >> rw [PREFIXn]) + >- (Q.EXISTS_TAC ‘SUC n’ >> rw [SUM1n]) + >- (Q.EXISTS_TAC ‘SUC n’ >> rw [SUM2n]) + >- (Q.EXISTS_TAC ‘SUC n’ >> rw [PAR1n]) + >- (Q.EXISTS_TAC ‘SUC n’ >> rw [PAR2n]) + >- (Q.EXISTS_TAC ‘SUC (MAX n n')’ \\ + MATCH_MP_TAC PAR3n >> Q.EXISTS_TAC ‘l’ >> rw []) + >- (Q.EXISTS_TAC ‘SUC n’ >> rw [RESTRn]) + >- (Q.EXISTS_TAC ‘SUC n’ >> rw [RESTRn]) + >- (Q.EXISTS_TAC ‘SUC n’ >> rw [RELABELINGn]) + >> (Q.EXISTS_TAC ‘SUC n’ >> rw [RECn]) +QED + +Theorem TRANSn_imp_TRANS : + !n E u E'. TRANSn n E u E' ==> TRANS E u E' +Proof + HO_MATCH_MP_TAC TRANSn_ind >> rw [] (* 10 subgoals *) + >- (rw [PREFIX]) + >- (rw [SUM1]) + >- (rw [SUM2]) + >- (rw [PAR1]) + >- (rw [PAR2]) + >- (MATCH_MP_TAC PAR3 >> Q.EXISTS_TAC ‘l’ >> rw []) + >- (rw [RESTR]) + >- (rw [RESTR]) + >- (rw [RELABELING]) + >> (rw [REC]) +QED + +Theorem TRANS_iff_TRANSn : + !E u E'. TRANS E u E' <=> ?n. TRANSn n E u E' +Proof + rpt GEN_TAC >> EQ_TAC + >- rw [TRANS_imp_TRANSn] + >> STRIP_TAC + >> MATCH_MP_TAC TRANSn_imp_TRANS + >> Q.EXISTS_TAC ‘n’ >> art [] +QED + +(* NOTE: This proof method based on ‘TRANSn’ is learnt from Ian Shillito. *) +Theorem I_NO_TRANS : + !X u E. ~TRANS I u E +Proof + rw [TRANS_iff_TRANSn, I_NO_TRANSn] +QED (******************************************************************************) (* *) @@ -2224,56 +2345,57 @@ 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' /\ E <> var X + !X E u E'. TRANS (rec X E) u E' <=> TRANS (CCS_Subst E (rec X E) X) u E' Proof rpt GEN_TAC >> reverse EQ_TAC >- PURE_ONCE_REWRITE_TAC [REC] >> PURE_ONCE_REWRITE_TAC [REC_cases_EQ] - >> STRIP_TAC - >> rename1 ‘rec X E = rec Y P’ + >> rpt STRIP_TAC >> fs [rec_eq_thm, CCS_Subst] - >> Q.PAT_X_ASSUM ‘E = _’ K_TAC - >> simp [fresh_tpm_subst] + >> rename1 ‘X <> Y’ + >> rename1 ‘X # P’ + (* stage work *) + >> rw [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' - >> simp [Abbr ‘E’] + >> rw [Abbr ‘E’] >> Know ‘[var Y/X] ([var X/Y] P) = P’ >- (MATCH_MP_TAC lemma15b >> art []) >> Rewr' - >> 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] + >> Suff ‘[rec Y P/X] ([var X/Y] P) = [rec Y P/Y] P’ + >- rw [] + >> MATCH_MP_TAC lemma15a >> art [] QED -val TRANS_REC = save_thm ("TRANS_REC", EQ_IMP_LR TRANS_REC_EQ); +(* |- !X E u E'. rec X E --u-> E' <=> [rec X E/X] E --u-> E' *) +Theorem TRANS_REC_EQ' = REWRITE_RULE [CCS_Subst] TRANS_REC_EQ + +(* |- !X E u E'. rec X E --u-> E' ==> CCS_Subst E (rec X E) X --u-> E' *) +Theorem TRANS_REC = EQ_IMP_LR TRANS_REC_EQ +(* |- !X E u E'. rec X E --u-> E' ==> [rec X E/X] E --u-> E' *) +Theorem TRANS_REC' = EQ_IMP_LR TRANS_REC_EQ' + +Theorem REC_VAR_NO_TRANS : + !X Y u E. ~TRANS (rec X (var Y)) u E +Proof + rpt GEN_TAC + >> Cases_on ‘X = Y’ + >- rw [GSYM I_thm, I_NO_TRANS] + >> rw [TRANS_REC_EQ', VAR_NO_TRANS] +QED + +(* NOTE: This is the *ONLY* theorem for which the induction principle of + ‘TRANS’ is needed. And this theorem (and the next TRANS_PROC) is only needed + in MultivariateScript.sml (so even the univariate "Unique solution" theorems + do not need this theorem). Thus, if ‘TRANS’ were defined by CoInductive, + "almost all" CCS theorems in this work, still hold. -- Chun Tian, 11 gen 2024 + *) Theorem TRANS_FV : !E u E'. TRANS E u E' ==> FV E' SUBSET (FV E) Proof @@ -2293,6 +2415,7 @@ Proof >> rfs [] QED +(* A modern name after ‘IS_PROC’ has been overloaded on ‘closed’. *) Theorem TRANS_closed = TRANS_PROC (* ---------------------------------------------------------------------- diff --git a/examples/CCS/ExampleScript.sml b/examples/CCS/ExampleScript.sml index 02f97acc4e..64c9436077 100644 --- a/examples/CCS/ExampleScript.sml +++ b/examples/CCS/ExampleScript.sml @@ -1,14 +1,18 @@ -(* - * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) - * Copyright 2016-2017 University of Bologna, Italy (Author: Chun Tian) - * Copyright 2018-2019 Fondazione Bruno Kessler, Italy (Author: Chun Tian) - *) +(* ========================================================================== *) +(* FILE : ExampleScript.sml *) +(* DESCRIPTION : Examples of concrete CCS processes; Some experiments *) +(* *) +(* 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) *) +(******************************************************************************) open HolKernel Parse boolLib bossLib; -open pred_setTheory relationTheory pairTheory sumTheory listTheory; -open prim_recTheory arithmeticTheory combinTheory stringTheory; +open combinTheory pred_setTheory relationTheory pairTheory sumTheory listTheory + arithmeticTheory stringTheory EmitTeX; +(* local theories *) open CCSLib CCSTheory CCSSyntax CCSConv; open StrongEQTheory StrongEQLib StrongLawsTheory; open WeakEQTheory WeakEQLib WeakLawsTheory; @@ -16,11 +20,9 @@ open ObsCongrTheory ObsCongrLib ObsCongrLawsTheory; open CongruenceTheory CoarsestCongrTheory; open TraceTheory ExpansionTheory ContractionTheory; open BisimulationUptoTheory UniqueSolutionsTheory; - open MultivariateTheory; val _ = new_theory "Example"; -val _ = temp_loose_equality (); (* For paper generating purposes, some type abbreviations are disabled *) val _ = disable_tyabbrev_printing "transition"; @@ -127,8 +129,6 @@ QED val _ = export_theory (); val _ = html_theory "Example"; -open EmitTeX; - (* Emit theory books in TeX *) val _ = if (OS.FileSys.isDir "../paper" handle e => false) then diff --git a/examples/CCS/MultivariateScript.sml b/examples/CCS/MultivariateScript.sml index 2175fa6d56..c3ced346b5 100644 --- a/examples/CCS/MultivariateScript.sml +++ b/examples/CCS/MultivariateScript.sml @@ -544,7 +544,7 @@ Proof QED (* A more precise estimation with `set Xs` *) -Theorem FV_SUBSET_BIGUNION_PRO : +Theorem FV_SUBSET_BIGUNION' : !Xs Ps E. ALL_DISTINCT Xs /\ (LENGTH Ps = LENGTH Xs) ==> FV (CCS_SUBST (fromList Xs Ps) E) SUBSET ((FV E) DIFF (set Xs)) UNION BIGUNION (IMAGE FV (set Ps)) @@ -579,7 +579,7 @@ Proof >> Suff `FV (CCS_SUBST (fromList Xs Ps) E) SUBSET {}` >- SET_TAC [] >> Know `FV (CCS_SUBST (fromList Xs Ps) E) SUBSET ((FV E) DIFF (set Xs)) UNION BIGUNION (IMAGE FV (set Ps))` - >- PROVE_TAC [FV_SUBSET_BIGUNION_PRO] + >- PROVE_TAC [FV_SUBSET_BIGUNION'] >> Know `FV E DIFF (set Xs) = {}` >- ASM_SET_TAC [] >> Rewr' >> Know `BIGUNION (IMAGE FV (set Ps)) = {}` >- rw [NOT_IN_EMPTY, IN_BIGUNION_IMAGE, IMAGE_EQ_SING] >> Rewr' @@ -590,7 +590,7 @@ QED "CCS_SUBST_elim" (or "CCS_SUBST_elim"); `LENGTH Ps = LENGTH Xs` is due to the limitation of "MAP_ZIP" *) -Theorem CCS_SUBST_PROC : +Theorem CCS_SUBST_elim_closed : !Xs Ps P. LENGTH Ps = LENGTH Xs /\ IS_PROC P ==> CCS_SUBST (fromList Xs Ps) P = P Proof diff --git a/examples/CCS/StrongLawsScript.sml b/examples/CCS/StrongLawsScript.sml index 4f4d5fb40a..9f6eeb861d 100644 --- a/examples/CCS/StrongLawsScript.sml +++ b/examples/CCS/StrongLawsScript.sml @@ -1108,24 +1108,20 @@ 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] - >> Q.EXISTS_TAC - ‘\x y. x = y \/ - ?Y E'. x = rec Y E' /\ y = CCS_Subst E' (rec Y E') Y /\ E' <> var Y’ + >> EXISTS_TAC + ``\x y. (x = y) \/ + (?Y E'. (x = rec Y E') /\ (y = CCS_Subst E' (rec Y E') 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) *) @@ -1220,6 +1216,8 @@ Proof take [`u'`, `v'`, `s'`] >> art [] ] ] QED +Theorem STRONG_UNFOLDING' = REWRITE_RULE [CCS_Subst] STRONG_UNFOLDING + (* Prove the theorem STRONG_REC_ACT2: |- ∀s u. rec s (u..u..var s) ~ rec s (u..var s) *) @@ -1306,8 +1304,7 @@ Proof 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]) \\ + Q.EXISTS_TAC ‘E2’ >> rw [TRANS_REC_EQ, CCS_Subst] \\ Know ‘[rec X E/X] E = E’ >- (MATCH_MP_TAC lemma14b >> art []) >> rw [] ] QED @@ -1316,8 +1313,7 @@ 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 [] + >> MATCH_MP_TAC STRONG_EQUIV_REC_ELIM >> rw [] QED (******************************************************************************)