From a21684dfc0e9c218f6b171867643c9d3287b50c8 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Thu, 14 Mar 2024 19:05:56 +1100 Subject: [PATCH] [lambda] Boehm_out_lemma (Proposition 10.3.7 (i) [1, p.248]) --- examples/lambda/barendregt/boehmScript.sml | 283 +++++++++++++++++---- examples/lambda/basics/termScript.sml | 41 ++- 2 files changed, 271 insertions(+), 53 deletions(-) diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml index e0b9cf2133..c621bb499e 100644 --- a/examples/lambda/barendregt/boehmScript.sml +++ b/examples/lambda/barendregt/boehmScript.sml @@ -92,7 +92,7 @@ Proof >> Q.EXISTS_TAC ‘M2’ >> art [] QED -Theorem tpm_rel_reduce[simp] : +Theorem tpm_rel_tpm[simp] : tpm_rel (tpm pi M) M /\ tpm_rel M (tpm pi M) Proof CONJ_ASM1_TAC @@ -577,8 +577,55 @@ Proof >> PROVE_TAC [] QED +(* NOTE: when subterm X M p = NONE, either 1) M or its subterm is unsolvable, + or 2) p runs out of ltree_paths (BTe X M). If we knew subterm X M p <> NONE + a priori, then p IN ltree_paths (BTe X M) must hold. + *) +Theorem subterm_imp_ltree_paths : + !p X M. FINITE X /\ subterm X M p <> NONE ==> p IN ltree_paths (BTe X M) +Proof + Induct_on ‘p’ >- rw [] + >> rpt GEN_TAC + >> STRIP_TAC + >> POP_ASSUM MP_TAC + >> Cases_on ‘solvable M’ + >> simp [subterm_def, ltree_paths_def, ltree_lookup] + >> qabbrev_tac ‘M0 = principle_hnf M’ + >> qabbrev_tac ‘n = LAMl_size M0’ + >> qabbrev_tac ‘vs = NEWS n (X UNION FV M0)’ + >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’ + >> qabbrev_tac ‘Ms = hnf_children M1’ + >> qabbrev_tac ‘m = hnf_children_size M0’ + >> Know ‘BTe X M = ltree_unfold BT_generator (X,M)’ >- rw [BT_def] + >> simp [Once ltree_unfold, BT_generator_def, LNTH_fromList, EL_MAP] + >> DISCH_THEN K_TAC + >> Know ‘m = LENGTH Ms’ + >- (qunabbrev_tac ‘M1’ \\ + ‘ALL_DISTINCT vs /\ LENGTH vs = n /\ DISJOINT (set vs) (X UNION FV M0)’ + by (rw [Abbr ‘vs’, NEWS_def]) \\ + ‘hnf M0’ by rw [hnf_principle_hnf', Abbr ‘M0’] \\ + Know ‘?y args. M0 = LAMl (TAKE n vs) (VAR y @* args)’ + >- (qunabbrev_tac ‘n’ >> irule (iffLR hnf_cases_shared) >> rw [] \\ + MATCH_MP_TAC DISJOINT_SUBSET \\ + Q.EXISTS_TAC ‘X UNION FV M0’ >> art [] \\ + SET_TAC []) >> STRIP_TAC \\ + ‘TAKE n vs = vs’ by rw [] \\ + POP_ASSUM (REV_FULL_SIMP_TAC std_ss o wrap) \\ + qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’ \\ + Know ‘M1 = VAR y @* args’ + >- (qunabbrev_tac ‘M1’ >> POP_ORW \\ + MATCH_MP_TAC principle_hnf_beta_reduce >> rw [hnf_appstar]) \\ + qunabbrev_tac ‘Ms’ \\ + Rewr' >> simp [hnf_children_hnf] \\ + qunabbrev_tac ‘m’ >> simp []) + >> DISCH_TAC + >> Cases_on ‘h < m’ >> rw [] + >> simp [GSYM BT_def] + >> fs [ltree_paths_def] +QED + (* Lemma 10.1.15 [1, p.222] *) -Theorem BT_subterm_thm : +Theorem BT_subterm_thm_old[local] : !p X M. p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE ==> BT (THE (subterm X M p)) = THE (ltree_lookup (BTe X M) p) Proof @@ -599,6 +646,15 @@ Proof >> rw [ltree_paths_def, ltree_lookup_def, LNTH_fromList, GSYM BT_def, EL_MAP] QED +Theorem BT_subterm_thm : + !p X M. FINITE X /\ subterm X M p <> NONE ==> + BT (THE (subterm X M p)) = THE (ltree_lookup (BTe X M) p) +Proof + rpt STRIP_TAC + >> MATCH_MP_TAC BT_subterm_thm_old >> art [] + >> MATCH_MP_TAC subterm_imp_ltree_paths >> art [] +QED + (* NOTE: This proof shares a lot of tactics with [subterm_tpm_lemma] *) Theorem BT_ltree_lookup_lemma : !p X Y M pi. FINITE X /\ FINITE Y /\ @@ -761,7 +817,7 @@ Proof QED (* The set of ltree paths of BT is unique w.r.t. excluded list *) -Theorem BT_ltree_paths_unique : +Theorem BT_ltree_paths_cong : !X Y M. FINITE X /\ FINITE Y ==> ltree_paths (BTe X M) = ltree_paths (BTe Y M) Proof @@ -1914,13 +1970,13 @@ End Theorem subterm_width_NIL[simp] = cj 1 subterm_width_def Theorem subterm_width_alt : - !X M p. FINITE X /\ - p <> [] /\ p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE ==> + !X M p. FINITE X /\ p <> [] /\ subterm X M p <> NONE ==> subterm_width M p = let Ms = {subterm' X M p' | p' <<= FRONT p} in MAX_SET (IMAGE (hnf_children_size o principle_hnf) Ms) Proof rpt STRIP_TAC + >> ‘p IN ltree_paths (BTe X M)’ by PROVE_TAC [subterm_imp_ltree_paths] >> Cases_on ‘p’ >> rw [subterm_width_def] >> qabbrev_tac ‘p = h::t’ (* preparing for subterm_hnf_children_size_cong *) @@ -1972,12 +2028,12 @@ QED hnf_children_size (principle_hnf (subterm' Y M p) *) Theorem subterm_width_thm : - !X M p p'. FINITE X /\ - p <> [] /\ p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE /\ + !X M p p'. FINITE X /\ p <> [] /\ subterm X M p <> NONE /\ p' <<= FRONT p ==> hnf_children_size (principle_hnf (subterm' X M p')) <= subterm_width M p Proof rpt STRIP_TAC + >> ‘p IN ltree_paths (BTe X M)’ by PROVE_TAC [subterm_imp_ltree_paths] >> Cases_on ‘p’ >> RW_TAC std_ss [subterm_width_def] >> qabbrev_tac ‘p = h::t’ @@ -2012,7 +2068,7 @@ Proof QED (* NOTE: This lemma does not hold without ‘v IN X’. *) -Theorem subterm_subst_cong_lemma[local] : +Theorem subterm_subst_cong_lemma_old[local] : !l X M p. l <<= p /\ FINITE X /\ v IN X /\ p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE /\ P = permutator d /\ subterm_width M p <= d @@ -2114,7 +2170,7 @@ Proof CONJ_TAC >- (MATCH_MP_TAC IMAGE_FINITE \\ ‘{subterm' (X UNION set vs) (EL h args) p' | p' <<= FRONT t} = IMAGE (subterm' (X UNION set vs) (EL h args)) - {p' | p' <<= FRONT t}’ + {p' | p' <<= FRONT t}’ by rw [Once EXTENSION] >> POP_ORW \\ MATCH_MP_TAC IMAGE_FINITE >> rw [FINITE_prefix]) \\ CONJ_TAC >- (‘{hnf_children_size (principle_hnf (subterm' X M p')) | @@ -2535,6 +2591,20 @@ Proof >> simp [Abbr ‘f’, hnf_children_hnf] QED +Theorem subterm_subst_cong_lemma[local] : + !l X M p. l <<= p /\ FINITE X /\ v IN X /\ + subterm X M p <> NONE /\ + P = permutator d /\ subterm_width M p <= d + ==> subterm X ([P/v] M) l <> NONE /\ + tpm_rel (subterm' X ([P/v] M) l) ([P/v] (subterm' X M l)) +Proof + rpt GEN_TAC + >> STRIP_TAC + >> MATCH_MP_TAC subterm_subst_cong_lemma_old + >> Q.EXISTS_TAC ‘p’ >> art [] + >> MATCH_MP_TAC subterm_imp_ltree_paths >> art [] +QED + (* NOTE: ‘y IN X’ must hold to make sure that ‘~MEM y vs’, where ‘set vs’ is disjoint with X, otherwise disaster happens. @@ -2549,7 +2619,7 @@ QED *) Theorem subterm_subst_cong : !p X M y P d. FINITE X /\ y IN X /\ - p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE /\ + subterm X M p <> NONE /\ P = permutator d /\ subterm_width M p <= d ==> subterm X ([P/y] M) p <> NONE /\ tpm_rel (subterm' X ([P/y] M) p) ([P/y] (subterm' X M p)) @@ -2578,48 +2648,20 @@ QED which is impossible if M is not already "is_ready". - NOTE4: The precise forms of Z and Z' in the conclusion, are: - - Z = X UNION FV M UNION set vs - Z' = X UNION FV M - - where vs = NEWS (LAMl_size (principle_hnf M) (X UNION FV M)) = f (X,M) - (vs is function of X and M, assuming M is solvable, otherwise trivial.) - - NOTE5: It's possible that the two terms in the final conclusion: - - 1. subterm' Z (apply pi M) p - 2. fm ' (subterm' Z' M p) - - are not equal, nor are they beta-equivalent, but they differ by a tpm! - - NOTE6: In general ‘apply pi M’ is not solvable even if M is solable (see also - [Boehm_apply_unsolvable], but in this case it is, and this is needed in - [Boehm_out_lemma] when rewriting ‘apply pi M’ to explicit forms using - [is_ready_alt] (assuming M is solvable). The extra conclusion is added: - ‘solvable M ==> solvable (apply pi M)’, which is not provable outside - the proof of this lemma. - - NOTE7: The core textbook proof steps of this lemma is actually in the proof of - [subterm_subst_cong], which has to have a ‘tpm_rel’ in the conclusion. - But the conclusion of the present lemma may still be ‘=’, because ‘tpm’ - may be represent by a ssub (fm), which can be combined with [P/y]. - - NOTE8: Instead of ssub, the conclusion has used ‘ISUB’. This is because later, - in [Boehm_out_lemma], we need to concatenate two ISUBs into a single one, - but there's no clear relationship on their keys. ISUB is straightforward - for this purposes. + NOTE4: Added ‘p IN ltree_paths (BTe X (apply pi M))’ into conclusions for the + needs in the user theorem. *) Theorem Boehm_transform_exists_lemma : - !X M p. FINITE X /\ - p <> [] /\ p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE ==> + !X M p. FINITE X /\ p <> [] /\ subterm X M p <> NONE ==> ?pi. Boehm_transform pi /\ solvable (apply pi M) /\ is_ready (apply pi M) /\ - ?Z v N. Z = X UNION FV M /\ closed N /\ + ?Z v P. Z = X UNION FV M /\ closed P /\ subterm Z (apply pi M) p <> NONE /\ - tpm_rel (subterm' Z (apply pi M) p) ([N/v] (subterm' Z M p)) + tpm_rel (subterm' Z (apply pi M) p) + ([P/v] (subterm' Z M p)) Proof rpt STRIP_TAC + >> ‘p IN ltree_paths (BTe X M)’ by PROVE_TAC [subterm_imp_ltree_paths] >> ‘(!q. q <<= p ==> subterm X M q <> NONE) /\ !q. q <<= FRONT p ==> solvable (subterm' X M q)’ by METIS_TAC [subterm_solvable_lemma] @@ -3008,10 +3050,10 @@ Proof to convert ‘subterm X M (h::t) <> NONE’ to ‘subterm Z M (h::t) <> NONE’. *) - >> CONJ_ASM1_TAC (* t IN ltree_paths ... *) + >> Know ‘t IN ltree_paths (BTe Z N)’ >- (Q.PAT_X_ASSUM ‘h::t IN ltree_paths (BTe X M)’ MP_TAC \\ ‘ltree_paths (BTe X M) = ltree_paths (BTe Y M)’ - by PROVE_TAC [BT_ltree_paths_unique] >> POP_ORW \\ + by PROVE_TAC [BT_ltree_paths_cong] >> POP_ORW \\ simp [ltree_paths_def, ltree_lookup] \\ Know ‘BTe Y M = ltree_unfold BT_generator (Y,M)’ >- rw [BT_def] \\ Q.PAT_X_ASSUM ‘M0 = _’ K_TAC \\ @@ -3021,6 +3063,7 @@ Proof qunabbrev_tac ‘Y’ >> SET_TAC []) >> Rewr' \\ simp [hnf_children_hnf] \\ simp [GSYM BT_def, EL_MAP, hnf_children_hnf]) + >> DISCH_TAC (* stage work *) >> CONJ_ASM1_TAC (* subterm Z N t <> NONE *) >- (Q.PAT_X_ASSUM ‘subterm X M (h::t) <> NONE’ MP_TAC \\ @@ -3103,6 +3146,152 @@ Proof >> MATCH_MP_TAC IS_PREFIX_BUTLAST' >> art [] QED +(* Another version with ‘tpm_rel’ but with ‘ISUB’ + + NOTE: there's also ‘p IN ltree_paths (BTe Z (apply pi M))’ added into + the conclusion, which has to be proved. + *) +Theorem Boehm_transform_exists_lemma' : + !X M p. FINITE X /\ p <> [] /\ subterm X M p <> NONE ==> + ?pi. Boehm_transform pi /\ + solvable (apply pi M) /\ is_ready (apply pi M) /\ + ?Z ss. Z = X UNION FV M /\ + subterm Z (apply pi M) p <> NONE /\ + p IN ltree_paths (BTe Z (apply pi M)) /\ + subterm' Z (apply pi M) p = (subterm' Z M p) ISUB ss +Proof + rpt STRIP_TAC + >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘p’] Boehm_transform_exists_lemma) + >> RW_TAC std_ss [] + >> Q.EXISTS_TAC ‘pi’ >> rw [] + >> POP_ASSUM MP_TAC (* tpm_rel ... *) + >> qabbrev_tac ‘t = [P/v] (subterm' (X UNION FV M) M p)’ + >> rw [tpm_rel_alt] + >> POP_ORW + (* applying tpm_ISUB_exists *) + >> STRIP_ASSUME_TAC (Q.SPECL [‘pi'’, ‘t’] tpm_ISUB_exists) + >> POP_ORW + >> qunabbrev_tac ‘t’ + >> Q.EXISTS_TAC ‘[(P,v)] ++ ss’ + >> rw [GSYM ISUB_APPEND] + (* final goal: p IN ltree_paths (BTe (X UNION FV M) (apply pi M)) *) + >> qabbrev_tac ‘N = apply pi M’ + >> qabbrev_tac ‘Z = X UNION FV M’ + >> MATCH_MP_TAC subterm_imp_ltree_paths >> art [] + >> rw [Abbr ‘Z’] +QED + +(* Proposition 10.3.7 (i) [1, p.248] (Boehm out lemma) + + NOTE: this time the case ‘p = []’ is included, but it's a trvial case. + *) +Theorem Boehm_out_lemma_old[local] : + !p X M. FINITE X /\ p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE ==> + ?pi ss. Boehm_transform pi /\ apply pi M == subterm' X M p ISUB ss +Proof + Induct_on ‘p’ + >- (rw [] >> qexistsl_tac [‘[]’, ‘[]’] >> rw []) + >> rpt STRIP_TAC + >> rename1 ‘subterm X M (h::t) <> NONE’ + >> qabbrev_tac ‘p = h::t’ (* head and tail *) + >> ‘p <> []’ by rw [Abbr ‘p’] + >> ‘(!q. q <<= p ==> subterm X M q <> NONE) /\ + !q. q <<= FRONT p ==> solvable (subterm' X M q)’ + by METIS_TAC [subterm_solvable_lemma] + >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘h::t’] Boehm_transform_exists_lemma') + >> rw [] (* this asserts pi and [P/v] *) + >> rename1 ‘Boehm_transform p0’ + >> qabbrev_tac ‘Z = X UNION FV M’ (* Z is now unique *) + >> ‘FINITE Z’ by rw [Abbr ‘Z’] + >> qabbrev_tac ‘M' = apply p0 M’ + >> ‘?y Ms. M' -h->* VAR y @* Ms /\ EVERY (\e. y # e) Ms’ + by METIS_TAC [is_ready_alt] + >> ‘principle_hnf M' = VAR y @* Ms’ by rw [principle_hnf_thm', hnf_appstar] + (* stage work *) + >> qunabbrev_tac ‘p’ + >> Know ‘h < LENGTH Ms’ + >- (Q.PAT_X_ASSUM ‘subterm Z M' (h::t) <> NONE’ MP_TAC \\ + RW_TAC std_ss [subterm_of_solvables] >> fs []) + >> DISCH_TAC + >> qabbrev_tac ‘m = LENGTH Ms’ + (* NOTE: This is the second ‘=’ of (2) [1, p.249], while the first ‘=’ is + now a tpm_rel in assumptions. *) + >> qabbrev_tac ‘N = EL h Ms’ + (* NOTE: Z is still there when going to subterm, not changed *) + >> Know ‘subterm' Z M' (h::t) = subterm' Z N t /\ subterm Z N t <> NONE’ + >- (Q.PAT_X_ASSUM ‘subterm' Z M' (h::t) = subterm' Z M (h::t) ISUB ss’ K_TAC \\ + Q.PAT_X_ASSUM ‘subterm Z M' (h::t) <> NONE’ MP_TAC \\ + rw [subterm_of_solvables, Abbr ‘N’]) + >> STRIP_TAC + >> Q.PAT_X_ASSUM ‘subterm' Z M' (h::t) = subterm' Z N t’ (fs o wrap) + >> rpt (Q.PAT_X_ASSUM ‘T’ K_TAC) + (* stage work, now define a selector *) + >> qabbrev_tac ‘U = selector h m’ + >> qabbrev_tac ‘p1 = [[U/y]]’ + >> ‘Boehm_transform p1’ by rw [Abbr ‘p1’] + >> qabbrev_tac ‘p10 = p1 ++ p0’ + >> ‘Boehm_transform p10’ by rw [Abbr ‘p10’, Boehm_transform_APPEND] + (* applying properties of selector (U) *) + >> Know ‘apply p10 M == N’ + >- (rw [Abbr ‘p10’, Boehm_apply_APPEND] \\ + MATCH_MP_TAC lameq_TRANS \\ + Q.EXISTS_TAC ‘apply p1 (principle_hnf M')’ \\ + CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong \\ + CONJ_TAC >- art [] \\ + MATCH_MP_TAC lameq_SYM \\ + MATCH_MP_TAC lameq_principle_hnf' >> art []) \\ + rw [Abbr ‘p1’, appstar_SUB] \\ + Know ‘MAP [U/y] Ms = Ms’ + >- (rw [LIST_EQ_REWRITE, EL_MAP] \\ + MATCH_MP_TAC lemma14b \\ + Q.PAT_X_ASSUM ‘EVERY (\e. y # e) Ms’ MP_TAC \\ + rw [EVERY_MEM, MEM_EL] \\ + POP_ASSUM MATCH_MP_TAC >> rename1 ‘i < m’ \\ + Q.EXISTS_TAC ‘i’ >> art []) >> Rewr' \\ + qunabbrevl_tac [‘U’, ‘N’] \\ + MATCH_MP_TAC selector_thm >> rw [Abbr ‘m’]) + >> DISCH_TAC + (* stage work, now using IH *) + >> Q.PAT_X_ASSUM ‘!X M. _’ (MP_TAC o (Q.SPECL [‘Z’, ‘N’])) >> simp [] + >> Know ‘t IN ltree_paths (BTe Z N)’ + >- (Q.PAT_X_ASSUM ‘h::t IN ltree_paths (BTe Z M')’ MP_TAC \\ + simp [ltree_paths_def, ltree_lookup] \\ + Know ‘BTe Z M' = ltree_unfold BT_generator (Z,M')’ >- rw [BT_def] \\ + simp [Once ltree_unfold, BT_generator_def, LNTH_fromList] \\ + rw [GSYM BT_def, EL_MAP, hnf_children_hnf]) + >> RW_TAC std_ss [] + >> rename1 ‘apply p2 N == _’ + >> POP_ASSUM MP_TAC + (* applying subterm_tpm_cong *) + >> Know ‘tpm_rel (subterm' Z M (h::t)) (subterm' X M (h::t))’ + >- (MP_TAC (Q.SPECL [‘h::t’, ‘Z’, ‘X’, ‘M’] subterm_tpm_cong) >> rw []) + >> rw [tpm_rel_alt] + >> qabbrev_tac ‘N' = subterm' X M (h::t)’ + (* applying tpm_ISUB_exists *) + >> STRIP_ASSUME_TAC (Q.SPECL [‘pi’, ‘N'’] tpm_ISUB_exists) + >> Q.PAT_X_ASSUM ‘apply p2 N == _’ MP_TAC + >> Q.PAT_X_ASSUM ‘subterm' Z M (h::t) = tpm pi N'’ (ONCE_REWRITE_TAC o wrap) + >> Q.PAT_X_ASSUM ‘tpm pi N' = N' ISUB ss''’ (ONCE_REWRITE_TAC o wrap) + >> simp [Abbr ‘N'’, ISUB_APPEND] >> DISCH_TAC + (* final stage *) + >> qexistsl_tac [‘p2 ++ p10’, ‘ss'' ++ ss ++ ss'’] + >> CONJ_TAC + >- (MATCH_MP_TAC Boehm_transform_APPEND >> art []) + >> MATCH_MP_TAC lameq_TRANS + >> Q.EXISTS_TAC ‘apply p2 N’ >> art [] + >> rw [Boehm_apply_APPEND] + >> MATCH_MP_TAC Boehm_apply_lameq_cong >> art [] +QED + +Theorem Boehm_out_lemma : + !p X M. FINITE X /\ subterm X M p <> NONE ==> + ?pi ss. Boehm_transform pi /\ apply pi M == subterm' X M p ISUB ss +Proof + rpt STRIP_TAC + >> MATCH_MP_TAC Boehm_out_lemma_old >> art [] + >> MATCH_MP_TAC subterm_imp_ltree_paths >> art [] +QED + (*---------------------------------------------------------------------------* * Separability of terms *---------------------------------------------------------------------------*) diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml index 1530c0b47a..a31897f39e 100644 --- a/examples/lambda/basics/termScript.sml +++ b/examples/lambda/basics/termScript.sml @@ -678,15 +678,10 @@ Definition ISUB_def: ($ISUB t [] = t) /\ ($ISUB t ((s,x)::rst) = $ISUB ([s/x]t) rst) End +val _ = export_rewrites ["ISUB_def"]; val _ = set_fixity "ISUB" (Infixr 501); -Theorem ISUB_NIL[simp] : - t ISUB [] = t -Proof - rw [ISUB_def] -QED - Definition DOM_DEF : (DOM [] = {}) /\ (DOM ((x,y)::rst) = {y} UNION DOM rst) @@ -767,6 +762,40 @@ Proof >> rw [ISUB_def, SUB_VAR] QED +Theorem tpm1_ISUB_exists[local] : + !M x y. ?ss. tpm [(x,y)] M = M ISUB ss +Proof + rpt GEN_TAC + >> Cases_on ‘x # M’ + >- (rw [fresh_tpm_subst] \\ + Q.EXISTS_TAC ‘[(VAR x,y)]’ >> rw []) + >> Cases_on ‘y # M’ + >- (rw [Once pmact_flip_args, fresh_tpm_subst] \\ + Q.EXISTS_TAC ‘[(VAR y,x)]’ >> rw []) + (* stage work *) + >> fs [] + >> Q_TAC (NEW_TAC "z") ‘FV M UNION {x} UNION {y}’ + (* applying swap_eq_3substs *) + >> Q.EXISTS_TAC ‘[(VAR z,x);(VAR x,y);(VAR y,z)]’ + >> rw [swap_eq_3substs] +QED + +Theorem tpm_ISUB_exists : + !pi M. ?ss. tpm pi M = M ISUB ss +Proof + Induct_on ‘pi’ + >- (rw [] >> Q.EXISTS_TAC ‘[]’ >> rw []) + >> rpt GEN_TAC + >> Cases_on ‘h’ + >> rw [Once tpm_CONS] + >> STRIP_ASSUME_TAC (Q.SPECL [‘tpm pi M’, ‘q’, ‘r’] tpm1_ISUB_exists) + >> POP_ORW + >> POP_ASSUM (STRIP_ASSUME_TAC o (Q.SPEC ‘M’)) + >> POP_ORW + >> rw [ISUB_APPEND] + >> Q.EXISTS_TAC ‘ss' ++ ss’ >> rw [] +QED + (* ---------------------------------------------------------------------- RENAMING: a special iterated substitutions like tpm ---------------------------------------------------------------------- *)