Added fresh_tpm_isub'

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] :

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 :