optimized agree_upto_lemma

examples/lambda/barendregt/lameta_completeScript.sml

@@ -644,24 +644,6 @@ Proof
       AP_TERM_TAC >> simp [Abbr ‘Qs’] ]
 QED
 
-(* cf. BT_ltree_paths_thm
-
-   M -h->* M0
-  /          \be*
-lameta        +---[lameta_CR] y1 = y2 /\ n1 + m2 = n2 + m1
-  \         /be*
-   N -h->* Ns
-
-   NOTE: Or “FV M UNION FV N SUBSET X UNION RANK r”.
- *)
-Theorem lameta_BT_equivalent_cong :
-    !X M N r. FINITE X /\ FV M UNION FV N SUBSET X /\ lameta M N ==>
-              !p. p IN ltree_paths (BT' X M r) /\
-                  p IN ltree_paths (BT' X N r) ==> subtree_equiv X M N p r
-Proof
-    cheat
-QED
-
 (*---------------------------------------------------------------------------*
  *  BT_paths and BT_valid_paths
  *---------------------------------------------------------------------------*)
@@ -897,7 +879,11 @@ Proof
  >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
 QED
 
-(* Lemma 10.3.11 [1. p.251] *)
+(* Lemma 10.3.11 [1. p.251]
+
+   NOTE: This theorem is weaker than subtree_equiv_lemma, but is tailored to
+   prove [agree_upto_thm].
+ *)
 Theorem agree_upto_lemma :
     !X Ms p r.
        FINITE X /\ Ms <> [] /\ p <> [] /\ 0 < r /\
@@ -907,9 +893,8 @@ Theorem agree_upto_lemma :
            (!M. MEM M Ms ==> is_ready' (apply pi M)) /\
            (!M. MEM M Ms ==> FV (apply pi M) SUBSET X UNION RANK r) /\
            (!M. MEM M Ms ==> p IN ltree_paths (BT' X (apply pi M) r)) /\
-           (!q M. MEM M Ms /\ q <<= p ==>
-                 (solvable (subterm' X M q r) <=>
-                  solvable (subterm' X (apply pi M) q r))) /\
+           (!M. MEM M Ms ==> (solvable (subterm' X M p r) <=>
+                              solvable (subterm' X (apply pi M) p r))) /\
            (agree_upto X Ms p r ==>
             agree_upto X (apply pi Ms) p r) /\
            !M N. MEM M Ms /\ MEM N Ms /\
@@ -1322,10 +1307,6 @@ Proof
  >> ‘subterm X (apply pi' (M i)) p (SUC r) <> NONE’
       by simp [GSYM BT_ltree_paths_thm]
  >> simp []
- >> Q.PAT_X_ASSUM ‘!q M. MEM M Ms /\ q <<= h::p ==> _’
-      (MP_TAC o Q.SPECL [‘h::p’, ‘M (i :num)’])
- >> impl_tac >- simp [EL_MEM, Abbr ‘M’]
- >> Rewr'
  (* applying hreduce_subterm_cong *)
  >> Know ‘subterm X (apply p0 (M i)) (h::p) r =
           subterm X (VAR y @* f i) (h::p) r’
@@ -1359,6 +1340,10 @@ Proof
  >> METIS_TAC []
 QED
 
+(*---------------------------------------------------------------------------*
+ *
+ *---------------------------------------------------------------------------*)
+
 (* Exercise 10.6.9 [1, p.272].
 
    NOTE: the actual statements have ‘has_benf M /\ has_benf N’