Added LAMl_ISUB, etc.

binghe · binghe · commit b25fe4710b2c · 2024-11-09T14:57:13.000+11:00
diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
@@ -2796,11 +2796,12 @@ QED
 
 (* Definition 10.3.5 (ii) *)
 Definition head_original_def :
-    head_original M0 = let n = LAMl_size M0;
-                          vs = NEWS n (FV M0);
-                          M1 = principle_hnf (M0 @* MAP VAR vs);
-                       in
-                          EVERY (\e. hnf_headvar M1 # e) (hnf_children M1)
+    head_original M0 =
+       let n = LAMl_size M0;
+          vs = NEWS n (FV M0);
+          M1 = principle_hnf (M0 @* MAP VAR vs)
+        in
+          EVERY (\e. hnf_headvar M1 # e) (hnf_children M1)
 End
 
 (* Definition 10.3.5 (iii)
@@ -2871,9 +2872,9 @@ QED
 Definition subterm_width_def :
     subterm_width M     [] = 0 /\
     subterm_width M (h::p) =
-    MAX_SET (IMAGE (hnf_children_size o principle_hnf)
-                   {subterm' (FV M) M q 0 | q |
-                    q <<= FRONT (h::p) /\ solvable (subterm' (FV M) M q 0)})
+      MAX_SET (IMAGE (hnf_children_size o principle_hnf)
+                     {subterm' (FV M) M q 0 | q |
+                      q <<= FRONT (h::p) /\ solvable (subterm' (FV M) M q 0)})
 End
 
 (* |- subterm_width M [] = 0 *)
@@ -3029,12 +3030,10 @@ Proof
  >> Q.EXISTS_TAC ‘q’ >> rw []
 QED
 
-(* cf. unsolvable_subst *)
 Theorem solvable_subst_permutator :
-    !X M M0 r v P d. FINITE X /\ FV M SUBSET X UNION RANK r /\ v IN X UNION RANK r /\
-                     M0 = principle_hnf M /\
-                     P = permutator d /\ hnf_children_size M0 <= d /\
-                     solvable M ==> solvable ([P/v] M)
+    !X M r P v d. FINITE X /\ FV M SUBSET X UNION RANK r /\ v IN X UNION RANK r /\
+                  P = permutator d /\ hnf_children_size (principle_hnf M) <= d /\
+                  solvable M ==> solvable ([P/v] M)
 Proof
     RW_TAC std_ss []
  >> qabbrev_tac ‘P = permutator d’
@@ -3078,24 +3077,26 @@ Proof
 QED
 
 Theorem solvable_subst_permutator_cong :
-    !X M M0 r v P d. FINITE X /\ FV M SUBSET X UNION RANK r /\ v IN X UNION RANK r /\
-                     M0 = principle_hnf M /\
-                     P = permutator d /\ hnf_children_size M0 <= d ==>
-                    (solvable ([P/v] M) <=> solvable M)
+    !X M r P v d.
+         FINITE X /\ FV M SUBSET X UNION RANK r /\ v IN X UNION RANK r /\
+         P = permutator d /\ hnf_children_size (principle_hnf M) <= d
+     ==> (solvable ([P/v] M) <=> solvable M)
 Proof
     rpt STRIP_TAC
  >> EQ_TAC >- PROVE_TAC [unsolvable_subst]
  >> DISCH_TAC
  >> MATCH_MP_TAC solvable_subst_permutator
- >> qexistsl_tac [‘X’, ‘M0’, ‘r’, ‘d’] >> rw []
+ >> qexistsl_tac [‘X’, ‘r’, ‘d’] >> art []
 QED
 
 (*
-Theorem solvable_permutator_ISUB :
-    !X M M0 r v P d. FINITE X /\ FV M SUBSET X UNION RANK r /\ v IN X UNION RANK r /\
-                     M0 = principle_hnf M /\
-                     P = permutator d /\ hnf_children_size M0 <= d /\
-                     solvable M ==> solvable ([P/v] M)
+Theorem solvable_ISUB_permutator :
+    !X M M0 r ss d.
+         FINITE X /\ FV M SUBSET X UNION RANK r /\
+         M0 = principle_hnf M /\ hnf_children_size M0 <= d /\
+         DOM ss SUBSET X UNION RANK r /\
+        (!P. MEM P (MAP FST ss) ==> P = permutator d) ==>
+         solvable M ==> solvable (M ISUB ss)
 Proof
     RW_TAC std_ss []
  >> qabbrev_tac ‘P = permutator d’
@@ -3109,8 +3110,8 @@ Proof
  >> ‘TAKE n vs = vs’ by rw []
  >> POP_ASSUM (rfs o wrap)
  >> ‘M0 == M’ by rw [Abbr ‘M0’, lameq_principle_hnf']
- >> ‘[P/v] M0 == [P/v] M’ by rw [lameq_sub_cong]
- >> Suff ‘solvable ([P/v] M0)’ >- PROVE_TAC [lameq_solvable_cong]
+ >> ‘M0 ISUB ss == M ISUB ss’ by rw [lameq_isub_cong]
+ >> Suff ‘solvable (M0 ISUB ss)’ >- PROVE_TAC [lameq_solvable_cong]
  >> ‘FV P = {}’ by rw [Abbr ‘P’, FV_permutator]
  >> ‘DISJOINT (set vs) (FV P)’ by rw [DISJOINT_ALT']
  >> Know ‘~MEM v vs’
@@ -3797,7 +3798,7 @@ Proof
   *)
  >> Know ‘solvable ([P/v] M)’
  >- (MATCH_MP_TAC solvable_subst_permutator \\
-     qexistsl_tac [‘X’, ‘M0’, ‘r’, ‘d’] >> simp [])
+     qexistsl_tac [‘X’, ‘r’, ‘d’] >> simp [])
  >> DISCH_TAC
  (* Now we need to know the exact form of ‘principle_hnf ([P/v] M)’.
 
@@ -5445,7 +5446,7 @@ Proof
  >> DISCH_TAC
  >> Know ‘solvable ([P/v] M)’
  >- (MATCH_MP_TAC solvable_subst_permutator \\
-     qexistsl_tac [‘X’,‘M0’, ‘r’, ‘d’] >> simp [] \\
+     qexistsl_tac [‘X’, ‘r’, ‘d’] >> simp [] \\
      MP_TAC (Q.SPECL [‘X’, ‘M’, ‘h::p’, ‘r’] subterm_width_first) \\
      simp [ltree_paths_def])
  >> DISCH_TAC
@@ -6197,7 +6198,7 @@ Proof
  >- (rpt STRIP_TAC \\
      Know ‘MAP (\t. t ISUB ss) (MAP VAR xs) = MAP VAR xs’
      >- (rw [LIST_EQ_REWRITE, EL_MAP] \\
-         MATCH_MP_TAC ISUB_VAR_FRESH >> rw [GSYM DOM_ALT_MAP_SND] \\
+         MATCH_MP_TAC ISUB_VAR_FRESH >> rw [GSYM DOM_ALT] \\
          simp [IN_IMAGE, IN_COUNT, Once DISJ_SYM] \\
          STRONG_DISJ_TAC (* push ‘a < k’ *) \\
          rename1 ‘EL x xs <> y a’ \\
diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml
@@ -5,7 +5,7 @@
 open HolKernel Parse boolLib bossLib BasicProvers;
 
 open pred_setTheory pred_setLib listTheory rich_listTheory finite_mapTheory
-     arithmeticTheory string_numTheory hurdUtils;
+     arithmeticTheory string_numTheory hurdUtils pairTheory;
 
 open basic_swapTheory termTheory nomsetTheory binderLib appFOLDLTheory;
 
@@ -213,6 +213,18 @@ val lameq_sub_cong = save_thm(
   "lameq_sub_cong",
   REWRITE_RULE [GSYM AND_IMP_INTRO] (last (CONJUNCTS lemma2_12)));
 
+Theorem lameq_isub_cong :
+    !ss M N. M == N ==> M ISUB ss == N ISUB ss
+Proof
+    Induct_on ‘ss’
+ >- rw []
+ >> simp [FORALL_PROD]
+ >> qx_genl_tac [‘P’, ‘v’]
+ >> rpt STRIP_TAC
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ >> MATCH_MP_TAC (cj 1 lemma2_12) >> art []
+QED
+
 val lemma2_13 = store_thm( (* p.20 *)
   "lemma2_13",
   ``!c n n'. ctxt c ==> (n == n') ==> (c n == c n')``,
diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
@@ -9,7 +9,7 @@
 open HolKernel Parse boolLib bossLib;
 
 open arithmeticTheory listTheory rich_listTheory pred_setTheory finite_mapTheory
-     hurdUtils listLib;
+     hurdUtils listLib pairTheory;
 
 open termTheory binderLib;
 
@@ -277,6 +277,23 @@ Proof
  >> Induct_on ‘vs’ >> rw []
 QED
 
+Theorem LAMl_ISUB :
+    !ss vs M. DISJOINT (set vs) (FVS ss) /\
+              DISJOINT (set vs) (DOM ss) ==>
+             ((LAMl vs M) ISUB ss = LAMl vs (M ISUB ss))
+Proof
+    Induct_on ‘ss’ >- rw [DOM_DEF, FVS_DEF]
+ >> simp [FORALL_PROD, DOM_ALT]
+ >> qx_genl_tac [‘P’, ‘v’]
+ >> rw [FVS_DEF, DISJOINT_UNION]
+ >> Know ‘[P/v] (LAMl vs M) = LAMl vs ([P/v] M)’
+ >- (MATCH_MP_TAC LAMl_SUB \\
+     simp [Once DISJOINT_SYM])
+ >> Rewr'
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ >> simp [Once DISJOINT_SYM, DOM_ALT]
+QED
+
 (* LAMl_ssub = ssub_LAM + LAMl_SUB *)
 Theorem LAMl_ssub :
     !vs fm t. DISJOINT (FDOM fm) (set vs) /\
diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml
@@ -736,7 +736,7 @@ Definition DOM_DEF :
    (DOM ((x,y)::rst) = {y} UNION DOM rst)
 End
 
-Theorem DOM_ALT_MAP_SND :
+Theorem DOM_ALT :
     !phi. DOM phi = set (MAP SND phi)
 Proof
     Induct_on ‘phi’ >- rw [DOM_DEF]
@@ -821,7 +821,7 @@ Proof
 QED
 
 (* |- !y sub. y NOTIN DOM sub ==> VAR y ISUB sub = VAR y *)
-Theorem ISUB_unchanged = REWRITE_RULE [GSYM DOM_ALT_MAP_SND] ISUB_VAR_FRESH
+Theorem ISUB_unchanged = REWRITE_RULE [GSYM DOM_ALT] ISUB_VAR_FRESH
 
 Theorem tpm1_ISUB_exists[local] :
     !M x y. ?ss. tpm [(x,y)] M = M ISUB ss
