Rebalanced proofs

examples/lambda/barendregt/boehmScript.sml

@@ -364,6 +364,21 @@ Proof
  >> POP_ASSUM (rfs o wrap)
 QED
 
+(* This proof without other antecedents is based on principle_hnf_hreduce *)
+Theorem hreduce_BT_cong :
+    !X M N r. M -h->* N ==> BT' X M r = BT' X N r
+Proof
+    rpt STRIP_TAC
+ >> ‘M == N’ by PROVE_TAC [hreduces_lameq]
+ >> reverse (Cases_on ‘solvable M’)
+ >- (‘unsolvable N’ by PROVE_TAC [lameq_solvable_cong] \\
+     rw [BT_of_unsolvables])
+ >> ‘solvable N’ by PROVE_TAC [lameq_solvable_cong]
+ >> ‘principle_hnf M = principle_hnf N’ by PROVE_TAC [principle_hnf_hreduce]
+ >> 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’
+QED
+
 Theorem BT_finite_branching :
     !X M r. finite_branching (BT' X M r)
 Proof
@@ -5643,6 +5658,16 @@ Proof
     rw [subtree_equiv_def, Once ltree_equiv_comm]
 QED
 
+Theorem hreduce_subtree_equiv_cong :
+    !X M M' N N' p r. M -h->* M' /\ N -h->* N' ==>
+                     (subtree_equiv X M N p r <=> subtree_equiv X M' N' p r)
+Proof
+    rw [subtree_equiv_def]
+ >> Suff ‘BT' X M r = BT' X M' r /\ BT' X N r = BT' X N' r’
+ >- DISCH_THEN (fs o wrap)
+ >> rw [hreduce_BT_cong]
+QED
+
 (* NOTE: This is the explicit form of the Boehm transform constructed in the
    next lemma. It assumes (at least):
 
@@ -5705,6 +5730,13 @@ QED
    NOTE: This is the LAST theorem of the current theory, because this proof is
    so long. Further results (plus users of this lemma) are to be found in the
    next lameta_completeTheory.
+
+   NOTE: Added the following conclusion for the need of [agree_upto_thm]:
+
+    !q M. MEM M Ms /\ q <<= p ==>
+         (solvable (subterm' X M q r) <=>
+          solvable (subterm' X (apply pi M) q r))
+
  *)
 Theorem subtree_equiv_lemma_explicit :
     !X Ms p r.

examples/lambda/barendregt/lameta_completeScript.sml

@@ -660,31 +660,6 @@ Proof
       AP_TERM_TAC >> simp [Abbr ‘Qs’] ]
 QED
 
-(* This proof without other antecedents is based on principle_hnf_hreduce *)
-Theorem hreduce_BT_cong :
-    !X M N r. M -h->* N ==> BT' X M r = BT' X N r
-Proof
-    rpt STRIP_TAC
- >> ‘M == N’ by PROVE_TAC [hreduces_lameq]
- >> reverse (Cases_on ‘solvable M’)
- >- (‘unsolvable N’ by PROVE_TAC [lameq_solvable_cong] \\
-     rw [BT_of_unsolvables])
- >> ‘solvable N’ by PROVE_TAC [lameq_solvable_cong]
- >> ‘principle_hnf M = principle_hnf N’ by PROVE_TAC [principle_hnf_hreduce]
- >> 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’
-QED
-
-Theorem hreduce_subtree_equiv_cong :
-    !X M M' N N' p r. M -h->* M' /\ N -h->* N' ==>
-                     (subtree_equiv X M N p r <=> subtree_equiv X M' N' p r)
-Proof
-    rw [subtree_equiv_def]
- >> Suff ‘BT' X M r = BT' X M' r /\ BT' X N r = BT' X N' r’
- >- DISCH_THEN (fs o wrap)
- >> rw [hreduce_BT_cong]
-QED
-
 (*---------------------------------------------------------------------------*
  *  BT_paths and BT_valid_paths
  *---------------------------------------------------------------------------*)
@@ -1983,7 +1958,6 @@ Theorem lameta_complete :
 Proof
     rpt STRIP_TAC
  >> ‘has_benf M /\ has_benf N’ by PROVE_TAC [has_benf_has_bnf]
- (* NOTE: the definition of ‘has_benf’ may be wrong *)
  >> ‘?M'. lameta M M' /\ benf M'’ by METIS_TAC [has_benf_def]
  >> ‘?N'. lameta N N' /\ benf N'’ by METIS_TAC [has_benf_def]
  >> Cases_on ‘M' = N'’