Add subtree_equiv_imp_subtree_equiv'

examples/lambda/barendregt/boehmScript.sml

@@ -2859,7 +2859,7 @@ Definition is_ready_def :
                    ?N. M -h->* N /\ hnf N /\ ~is_abs N /\ head_original N
 End
 
-Definition is_ready' :
+Definition is_ready'_def :
     is_ready' M <=> is_ready M /\ solvable M
 End
 
@@ -2902,7 +2902,7 @@ Theorem is_ready_alt' :
                         ?y Ns. M -h->* VAR y @* Ns /\ EVERY (\e. y # e) Ns
 Proof
  (* NOTE: this proof relies on the new [NOT_AND'] in boolSimps.BOOL_ss *)
-    rw [is_ready', is_ready_alt, RIGHT_AND_OVER_OR]
+    rw [is_ready'_def, is_ready_alt, RIGHT_AND_OVER_OR]
  >> REWRITE_TAC [Once CONJ_COMM]
 QED
 
@@ -4951,7 +4951,7 @@ Proof
    *)
      MATCH_MP_TAC principle_hnf_denude_thm >> rw [])
  >> DISCH_TAC
- >> simp [is_ready', GSYM CONJ_ASSOC]
+ >> simp [is_ready'_def, GSYM CONJ_ASSOC]
  (* extra subgoal: solvable (apply (p3 ++ p2 ++ p1) M) *)
  >> ONCE_REWRITE_TAC [TAUT ‘P /\ Q /\ R <=> Q /\ P /\ R’]
  >> CONJ_ASM1_TAC

examples/lambda/barendregt/lameta_completeScript.sml

@@ -7,7 +7,8 @@
 
 open HolKernel Parse boolLib bossLib;
 
-open hurdUtils arithmeticTheory pred_setTheory listTheory rich_listTheory;
+open hurdUtils arithmeticTheory pred_setTheory listTheory rich_listTheory
+     ltreeTheory llistTheory;
 
 open termTheory basic_swapTheory appFOLDLTheory chap2Theory chap3Theory
      horeductionTheory solvableTheory head_reductionTheory head_reductionLib
@@ -30,14 +31,39 @@ val _ = hide "C";
 val _ = hide "W";
 val _ = hide "Y";
 
+(* NOTE: what we know so far about subterm_equiv and subterm_equiv':
+  1. subterm_equiv X (apply pi M) (apply pi N) p r ==> subtree_equiv' X M N p r
+  2. subterm_equiv X M N p r ==> subterm_equiv X (apply pi M) (apply pi N) p r
+  3. subterm_equiv X M N p r ==> subterm_equiv' X M N p r
+ *)
+Theorem subtree_equiv_imp_subtree_equiv' :
+    !X M N p r. FINITE X /\ FV M UNION FV N SUBSET X UNION RANK r /\
+                subtree_equiv X M N p r ==> subtree_equiv' X M N p r
+Proof
+    RW_TAC std_ss [subtree_equiv_def, subtree_equiv'_def]
+ >> POP_ASSUM MP_TAC
+ >> Cases_on ‘p’ >> fs [] >> T_TAC
+ >- simp [ltree_equiv_imp_ltree_equiv']
+ >> reverse (Cases_on ‘solvable M’)
+ >- simp [BT_of_unsolvables, ltree_el]
+ >> reverse (Cases_on ‘solvable N’)
+ >- simp [BT_of_unsolvables, ltree_el]
+ >> Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold]) ‘BT' X M r’
+ >> Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold]) ‘BT' X N r’
+ >> simp [ltree_el_def, LMAP_fromList, LNTH_fromList, GSYM BT_def]
+ >> Cases_on ‘h < LENGTH l’
+ >> Cases_on ‘h < LENGTH l'’
+ >> simp [ltree_equiv_imp_ltree_equiv']
+QED
+
 (* Definition 10.3.10 (iii) and (iv) [1, p.251]
 
    NOTE: The purpose of X is to make sure all terms in Ms share the same excluded
          set (and thus perhaps also the same initial binding list).
  *)
 Definition agree_upto_def :
     agree_upto X Ms p r <=>
-      !M N q. MEM M Ms /\ MEM N Ms /\ q <<= p ==> subtree_equiv X M N q r
+    !M N q. MEM M Ms /\ MEM N Ms /\ q <<= p ==> subtree_equiv X M N q r
 End
 
 (* NOTE: subterm_equiv_lemma and this theorem together implies the original
@@ -60,34 +86,38 @@ Theorem agree_upto_lemma :
        FINITE X /\ p <> [] /\ 0 < r /\ Ms <> [] /\
        BIGUNION (IMAGE FV (set Ms)) SUBSET X UNION RANK r /\
        EVERY (\M. subterm X M p r <> NONE) Ms ==>
-      ?pi. Boehm_transform pi /\ EVERY is_ready' (MAP (apply pi) Ms) /\
-          (agree_upto X Ms p r ==> agree_upto X (MAP (apply pi) Ms) p r) /\
-          !M N. MEM M Ms /\ MEM N Ms /\
-                subtree_equiv X (apply pi M) (apply pi N) p r ==>
-                subtree_equiv' X M N p r
+       ?pi. Boehm_transform pi /\ EVERY is_ready' (MAP (apply pi) Ms) /\
+            (agree_upto X Ms p r ==> agree_upto X (MAP (apply pi) Ms) p r) /\
+            !M N. MEM M Ms /\ MEM N Ms /\
+                  subtree_equiv X (apply pi M) (apply pi N) p r ==>
+                  subtree_equiv' X M N p r
 Proof
     rpt GEN_TAC
  >> DISCH_THEN (MP_TAC o (MATCH_MP subterm_equiv_lemma))
  >> rpt STRIP_TAC
- >> Q.EXISTS_TAC ‘pi’ >> rw []
+ >> Q.EXISTS_TAC ‘pi’
+ >> RW_TAC std_ss []
  >> MATCH_MP_TAC subterm_equiv_imp_agree_upto >> art []
 QED
 
-(*
 (* Definition 10.3.10 (ii) [1, p.251] *)
 Definition is_faithful_def :
-    is_faithful X M p Ns pi <=>
-      (!X M. MEM M Ns ==>
-            (solvable (apply pi M) <=> ltree_lookup (BT X M) p <> NONE)) /\
-       !M N. MEM M Ns /\ MEM N Ns ==>
-            (subtree_equiv X M N p r <=> equivalent (apply pi M) (apply pi N))
+    is_faithful p X Ms pi r <=>
+      (!M.   MEM M Ms ==>
+            (solvable (apply pi M) <=> p IN ltree_paths (BT' X M r))) /\
+       !M N. MEM M Ms /\ MEM N Ms ==>
+            (subtree_equiv X M N p r <=>
+             equivalent (apply pi M) (apply pi N))
 End
 
+Overload faithful = “is_faithful []”
+
+(*
 Theorem is_faithful_two :
     !p M N pi.
-       is_faithful p [M; N] pi <=>
-      (!X. solvable (apply pi M) <=> ltree_lookup (BT X M) p) <> NONE) /\
-      (!X. solvable (apply pi N) <=> ltree_lookup (BT X N) p) <> NONE) /\
+       is_faithful [M; N] p pi <=>
+      (!X. solvable (apply pi M) <=> M IN ltree_paths (BT' X M 0)) /\
+      (!X. solvable (apply pi N) <=> N IN ltree_paths (BT' X N 0)) /\
       (subtree_equiv p M N <=> equivalent (apply pi M) (apply pi N))
 Proof
     rw [is_faithful_def]
@@ -98,17 +128,21 @@ Proof
  >- rw [Once subtree_equiv_comm]
  >> rw [Once equivalent_comm]
 QED
+ *)
 
 (* Proposition 10.3.13 [1, p.253] *)
 Theorem agree_upto_thm :
-    !Ns p. agree_upto p Ns ==> ?pi. Boehm_transform pi /\ is_faithful p Ns pi
+    !X Ms p r.
+       FINITE X /\
+       BIGUNION (IMAGE FV (set Ms)) SUBSET X UNION RANK r /\
+       agree_upto X Ms p r ==>
+       ?pi. Boehm_transform pi /\ is_faithful p X Ms pi r
 Proof
     cheat
 QED
-*)
 
 (*---------------------------------------------------------------------------*
- *  Separability of terms
+ *  Separability of lambda terms
  *---------------------------------------------------------------------------*)
 
 Theorem separability_lemma0_case2[local] :