From ea8623c1ef089c0952476a68c1ddb41635f9dd1e Mon Sep 17 00:00:00 2001 From: Chun Tian Date: Mon, 4 Nov 2024 16:01:00 +1100 Subject: [PATCH] Added fresh_tpm_isub' --- examples/lambda/basics/appFOLDLScript.sml | 44 ++------- examples/lambda/basics/termScript.sml | 115 ++++++++++++++++++++-- 2 files changed, 115 insertions(+), 44 deletions(-) diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml index 43c4ebbbf4..1fbcf16004 100644 --- a/examples/lambda/basics/appFOLDLScript.sml +++ b/examples/lambda/basics/appFOLDLScript.sml @@ -364,42 +364,14 @@ Proof >> Suff ‘(FEMPTY |++ ZIP (vs, MAP VAR vs')) ' M = M ISUB REVERSE (ZIP (MAP VAR vs', vs))’ >- (Rewr' >> MATCH_MP_TAC LAMl_ALPHA >> art []) - >> rpt (POP_ASSUM MP_TAC) - >> Q.ID_SPEC_TAC ‘vs'’ - >> Q.ID_SPEC_TAC ‘vs’ - >> Induct_on ‘vs’ >- rw [FUPDATE_LIST_THM, ISUB_def] - >> rw [] - >> Cases_on ‘vs'’ >- fs [] - >> fs [] >> rename1 ‘v # M’ - (* RHS rewriting *) - >> REWRITE_TAC [GSYM ISUB_APPEND, GSYM SUB_ISUB_SINGLETON] - (* LHS rewriting *) - >> rw [FUPDATE_LIST_THM] - >> Know ‘(FEMPTY :string |-> term) |+ (h,VAR v) |++ ZIP (vs,MAP VAR t) = - (FEMPTY |++ ZIP (vs,MAP VAR t)) |+ (h,VAR v)’ - >- (MATCH_MP_TAC FUPDATE_FUPDATE_LIST_COMMUTES \\ - rw [MAP_ZIP]) - >> Rewr' - >> qabbrev_tac ‘fm = (FEMPTY :string |-> term) |++ ZIP (vs,MAP VAR t)’ - >> ‘FDOM fm = set vs’ by (rw [Abbr ‘fm’, FDOM_FUPDATE_LIST, MAP_ZIP]) - (* applying ssub_update_apply_SUBST' *) - >> Know ‘(fm |+ (h,VAR v)) ' M = [fm ' (VAR v)/h] (fm ' M)’ - >- (MATCH_MP_TAC ssub_update_apply_SUBST' >> rw [] \\ - ‘fm = fromPairs vs (MAP VAR t)’ by rw [Abbr ‘fm’, fromPairs_def] \\ - POP_ORW \\ - Q.PAT_X_ASSUM ‘MEM k vs’ MP_TAC >> rw [MEM_EL] \\ - Know ‘fromPairs vs (MAP VAR t) ' (EL n vs) = EL n (MAP VAR t)’ - >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\ - rw [EL_MAP] \\ - Q.PAT_X_ASSUM ‘~MEM h t’ MP_TAC >> rw [MEM_EL] \\ - POP_ASSUM (MP_TAC o (Q.SPEC ‘n’)) >> rw []) - >> Rewr' - >> Know ‘fm ' (VAR v) = VAR v’ - >- (MATCH_MP_TAC ssub_14b >> rw [GSYM DISJOINT_DEF]) - >> Rewr' - >> Suff ‘fm ' M = M ISUB REVERSE (ZIP (MAP VAR t,vs))’ >- rw [] - >> qunabbrev_tac ‘fm’ - >> FIRST_X_ASSUM irule >> rw [] + (* applying fromPairs_ISUB *) + >> REWRITE_TAC [GSYM fromPairs_def] + >> MATCH_MP_TAC fromPairs_ISUB + >> fs [DISJOINT_UNION'] + >> rw [EVERY_MEM, MEM_MAP] + >> simp [] + >> Q.PAT_X_ASSUM ‘DISJIOINT (set vs') (set vs)’ MP_TAC + >> rw [DISJOINT_ALT] QED Theorem LAMl_SNOC[simp] : diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml index 3c8d307e72..9fa8b73d9e 100644 --- a/examples/lambda/basics/termScript.sml +++ b/examples/lambda/basics/termScript.sml @@ -884,7 +884,7 @@ QED (* This is a direct generalization of fresh_tpm_subst - NOTE: ‘ALL_DISTINCT xs’ is not assumed, thus ‘REVERSE vs’, etc. is necessary. + NOTE: cf. fresh_tpm_isub' for another version without REVERSE. *) Theorem fresh_tpm_isub : !xs ys t. LENGTH xs = LENGTH ys /\ ALL_DISTINCT ys /\ @@ -1502,16 +1502,48 @@ Proof >> Q.EXISTS_TAC ‘n’ >> art [] QED -Theorem fromPairs_FOLDR' : +Theorem fromPairs_ISUB : !Xs Ps E. ALL_DISTINCT Xs /\ LENGTH Ps = LENGTH Xs /\ EVERY (\p. DISJOINT (set Xs) (FV p)) Ps ==> - (fromPairs Xs Ps) ' E = - FOLDR (\(x,y) e. [y/x] e) E (ZIP (Xs,Ps)) + (fromPairs Xs Ps) ' E = E ISUB REVERSE (ZIP (Ps,Xs)) Proof - rpt STRIP_TAC - >> MATCH_MP_TAC fromPairs_FOLDR >> art [] - >> fs [FEVERY_DEF, EVERY_MEM] - >> RW_TAC std_ss [MEM_ZIP] + Induct_on ‘Xs’ + >- rw [fromPairs_def, FUPDATE_LIST_THM] + >> rw [] + >> Cases_on ‘Ps’ >- fs [] + >> fs [fromPairs_def] >> rename1 ‘v # P’ + (* RHS rewriting *) + >> REWRITE_TAC [GSYM ISUB_APPEND, GSYM SUB_ISUB_SINGLETON] + (* LHS rewriting *) + >> rw [fromPairs_def, FUPDATE_LIST_THM] + >> Know ‘(FEMPTY :string |-> term) |+ (v,P) |++ ZIP (Xs,t) = + (FEMPTY |++ ZIP (Xs,t)) |+ (v,P)’ + >- (MATCH_MP_TAC FUPDATE_FUPDATE_LIST_COMMUTES \\ + rw [MAP_ZIP]) + >> Rewr' + >> qabbrev_tac ‘fm = (FEMPTY :string |-> term) |++ ZIP (Xs,t)’ + >> ‘FDOM fm = set Xs’ by rw [Abbr ‘fm’, FDOM_FUPDATE_LIST, MAP_ZIP] + (* applying ssub_update_apply_SUBST' *) + >> Know ‘(fm |+ (v,P)) ' E = [fm ' P/v] (fm ' E)’ + >- (MATCH_MP_TAC ssub_update_apply_SUBST' >> rw [] \\ + ‘fm = fromPairs Xs t’ by rw [Abbr ‘fm’, fromPairs_def] \\ + POP_ORW \\ + Q.PAT_X_ASSUM ‘MEM k Xs’ MP_TAC >> rw [MEM_EL] \\ + Know ‘fromPairs Xs t ' (EL n Xs) = EL n t’ + >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\ + Q.PAT_X_ASSUM ‘EVERY _ t’ MP_TAC >> rw [EVERY_MEM, MEM_EL] \\ + POP_ASSUM (MP_TAC o (Q.SPEC ‘EL n t’)) \\ + impl_tac >- (Q.EXISTS_TAC ‘n’ >> art []) \\ + rw [DISJOINT_ALT']) + >> Rewr' + >> Know ‘fm ' P = P’ + >- (MATCH_MP_TAC ssub_14b \\ + rw [GSYM DISJOINT_DEF, Once DISJOINT_SYM]) + >> Rewr' + >> Suff ‘fm ' E = E ISUB REVERSE (ZIP (t,Xs))’ >- rw [] + >> qunabbrev_tac ‘fm’ + >> FIRST_X_ASSUM irule >> rw [] + >> fs [EVERY_CONJ] QED Theorem fromPairs_self : @@ -1639,8 +1671,75 @@ Proof >> SET_TAC [] QED +(* If, additionally, ‘ALL_DISTINCT xs /\ DISJOINT (set xs) (set ys)’ holds, + the REVERSE in conclusion can be eliminated. + *) +Theorem fresh_tpm_isub' : + !xs ys t. LENGTH xs = LENGTH ys /\ + ALL_DISTINCT xs /\ ALL_DISTINCT ys /\ + DISJOINT (set xs) (set ys) /\ + DISJOINT (set ys) (FV t) + ==> tpm (ZIP (xs,ys)) t = t ISUB (ZIP (MAP VAR ys, xs)) +Proof + rw [fresh_tpm_isub] + >> qabbrev_tac ‘Ps = MAP VAR ys’ + >> ‘LENGTH Ps = LENGTH ys’ by rw [Abbr ‘Ps’] + >> simp [MAP_REVERSE, GSYM REVERSE_ZIP] + (* applying fromPairs_ISUB *) + >> Know ‘t ISUB REVERSE (ZIP (Ps,xs)) = fromPairs xs Ps ' t’ + >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ + MATCH_MP_TAC fromPairs_ISUB >> art [] \\ + rw [EVERY_MEM, MEM_EL, Abbr ‘Ps’] \\ + simp [EL_MAP] \\ + Q.PAT_X_ASSUM ‘DISJOINT (set xs) (set ys)’ MP_TAC \\ + rw [DISJOINT_ALT'] \\ + POP_ASSUM MATCH_MP_TAC >> simp [EL_MEM]) + >> Rewr' + >> qabbrev_tac ‘xs' = REVERSE xs’ + >> qabbrev_tac ‘Ps' = REVERSE Ps’ + >> ‘xs = REVERSE xs' /\ Ps = REVERSE Ps'’ by rw [Abbr ‘xs'’, Abbr ‘Ps'’] + >> NTAC 2 POP_ORW + >> ‘LENGTH xs' = LENGTH xs /\ LENGTH Ps' = LENGTH Ps’ + by rw [Abbr ‘xs'’, Abbr ‘Ps'’] + >> simp [GSYM REVERSE_ZIP] + >> Know ‘t ISUB REVERSE (ZIP (Ps',xs')) = fromPairs xs' Ps' ' t’ + >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ + MATCH_MP_TAC fromPairs_ISUB >> art [] \\ + CONJ_TAC >- rw [Abbr ‘xs'’, ALL_DISTINCT_REVERSE] \\ + rw [EVERY_MEM, MEM_EL, Abbr ‘Ps'’, Abbr ‘Ps’, Abbr ‘xs'’] \\ + simp [EL_MAP] \\ + Q.PAT_X_ASSUM ‘DISJOINT (set xs) (set ys)’ MP_TAC \\ + rw [DISJOINT_ALT'] \\ + POP_ASSUM MATCH_MP_TAC >> simp [EL_MEM]) + >> Rewr' + >> simp [fromPairs_def, Abbr ‘xs'’, Abbr ‘Ps'’] + >> qabbrev_tac ‘fm = FEMPTY |++ ZIP (xs,Ps)’ + >> qabbrev_tac ‘fm' = FEMPTY |++ ZIP (REVERSE xs,REVERSE Ps)’ + >> Suff ‘fm = fm'’ >- rw [] + >> ‘FDOM fm = set xs /\ FDOM fm' = set xs’ + by rw [Abbr ‘fm’, Abbr ‘fm'’, GSYM fromPairs_def, FDOM_fromPairs, + LIST_TO_SET_REVERSE] + >> rw [fmap_EXT, MEM_EL] + (* applying fromPairs_FAPPLY_EL *) + >> simp [Abbr ‘fm’, Abbr ‘fm'’, GSYM fromPairs_def] + >> Know ‘fromPairs xs Ps ' (EL n xs) = EL n Ps’ + >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> art []) + >> Rewr' + >> qabbrev_tac ‘xs' = REVERSE xs’ + >> qabbrev_tac ‘Ps' = REVERSE Ps’ + >> ‘xs = REVERSE xs' /\ Ps = REVERSE Ps'’ by rw [Abbr ‘xs'’, Abbr ‘Ps'’] + >> NTAC 2 POP_ORW + >> ‘LENGTH xs' = LENGTH xs /\ LENGTH Ps' = LENGTH Ps’ + by rw [Abbr ‘xs'’, Abbr ‘Ps'’] + >> simp [EL_REVERSE, Once EQ_SYM_EQ] + >> MATCH_MP_TAC fromPairs_FAPPLY_EL + >> simp [Abbr ‘xs'’, Abbr ‘Ps'’, ALL_DISTINCT_REVERSE] +QED + (*****************************************************************************) (* Simultaneous substitution given by a function containing infinite keys *) +(* *) +(* NOTE: This definition is not used (it doesn't have finite "support"). *) (*****************************************************************************) Definition fssub_def :