Re-enable previously disabled proofs

examples/lambda/barendregt/boehmScript.sml

@@ -937,7 +937,6 @@ Proof
  >> qexistsl_tac [‘M’, ‘M0’, ‘n’, ‘m’, ‘vs’, ‘M1’] >> simp []
 QED
 
-(* NOTE: cf. BT_paths M *)
 Theorem BT_ltree_paths_thm :
     !X M p r. FINITE X /\ FV M SUBSET X UNION RANK r ==>
              (p IN ltree_paths (BT' X M r) <=> subterm X M p r <> NONE)
@@ -2326,6 +2325,16 @@ Proof
     RW_TAC std_ss [BT_tpm_thm, ltree_paths_map_cong]
 QED
 
+Theorem BT_ltree_paths_cong :
+    !X Y M r r'. FINITE X /\ FINITE Y /\
+                 FV M SUBSET X UNION RANK r /\
+                 FV M SUBSET Y UNION RANK r'
+             ==> ltree_paths (BT' X M r) = ltree_paths (BT' Y M r')
+Proof
+    rw [Once EXTENSION, BT_ltree_paths_thm]
+ >> MATCH_MP_TAC (cj 1 subterm_tpm_cong) >> art []
+QED
+
 (*---------------------------------------------------------------------------*
  *  Boehm transformations
  *---------------------------------------------------------------------------*)

examples/lambda/barendregt/lameta_completeScript.sml

@@ -8,11 +8,11 @@
 open HolKernel Parse boolLib bossLib;
 
 open hurdUtils arithmeticTheory pred_setTheory listTheory rich_listTheory
-     ltreeTheory llistTheory relationTheory tautLib;
+     ltreeTheory llistTheory relationTheory tautLib topologyTheory;
 
 open termTheory basic_swapTheory appFOLDLTheory chap2Theory chap3Theory NEWLib
      horeductionTheory solvableTheory head_reductionTheory head_reductionLib
-     nomsetTheory standardisationTheory boehmTheory topologyTheory;
+     nomsetTheory standardisationTheory boehmTheory takahashiS3Theory;
 
 (* enable basic monad support *)
 open monadsyntax;
@@ -62,127 +62,6 @@ Definition ltree_subset_def :
            ltree_node (THE (ltree_lookup B p))
 End
 
-(*---------------------------------------------------------------------------*
- *  Boehm trees of beta/eta equivalent terms
- *---------------------------------------------------------------------------*)
-
-(* Proposition 10.1.6 [1, p.219] *)
-Theorem lameq_BT_cong :
-    !X M N r. FINITE X /\ FV M UNION FV N SUBSET X /\ M == N ==>
-              BT' X M r = BT' X N r
-Proof
-    RW_TAC std_ss []
- >> reverse (Cases_on ‘solvable M’)
- >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\
-     rw [BT_of_unsolvables])
- >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong]
- (* applying ltree_bisimulation *)
- >> rw [ltree_bisimulation]
- (* NOTE: ‘solvable P /\ solvable Q’ cannot be added here *)
- >> Q.EXISTS_TAC
-     ‘\x y. ?P Q r. FV P UNION FV Q SUBSET X UNION RANK r /\
-                    P == Q /\ x = BT' X P r /\ y = BT' X Q r’
- >> BETA_TAC
- >> CONJ_TAC
- >- (qexistsl_tac [‘M’, ‘N’, ‘r’] >> simp [] \\
-     Q.PAT_X_ASSUM ‘FV M UNION FV N SUBSET X’ MP_TAC \\
-     Q.PAT_X_ASSUM ‘FINITE X’ MP_TAC \\
-     SET_TAC [])
- (* stage work *)
- >> qx_genl_tac [‘a1’, ‘ts1’, ‘a2’, ‘ts2’] >> STRIP_TAC
- >> qabbrev_tac ‘P0 = principle_hnf P’
- >> qabbrev_tac ‘Q0 = principle_hnf Q’
- >> qabbrev_tac ‘n  = LAMl_size P0’
- >> qabbrev_tac ‘n' = LAMl_size Q0’
- >> qabbrev_tac ‘vs = RNEWS r n  X’
- >> qabbrev_tac ‘vs'= RNEWS r n' X’
- >> qabbrev_tac ‘P1 = principle_hnf (P0 @* MAP VAR vs)’
- >> qabbrev_tac ‘Q1 = principle_hnf (Q0 @* MAP VAR vs')’
- >> qabbrev_tac ‘Ps = hnf_children P1’
- >> qabbrev_tac ‘Qs = hnf_children Q1’
- >> qabbrev_tac ‘y  = hnf_head P1’
- >> qabbrev_tac ‘y' = hnf_head Q1’
- (* applying ltree_unfold *)
- >> Q.PAT_X_ASSUM ‘_ = BT' X Q r’ MP_TAC
- >> simp [BT_def, Once ltree_unfold, BT_generator_def]
- >> Q.PAT_X_ASSUM ‘_ = BT' X P r’ MP_TAC
- >> simp [BT_def, Once ltree_unfold, BT_generator_def]
- >> NTAC 2 STRIP_TAC
- (* easy case: unsolvable P (and Q) *)
- >> reverse (Cases_on ‘solvable P’)
- >- (‘unsolvable Q’ by PROVE_TAC [lameq_solvable_cong] >> fs [] \\
-     rw [llist_rel_def, LLENGTH_MAP])
- (* now both P and Q are solvable *)
- >> ‘solvable Q’ by PROVE_TAC [lameq_solvable_cong]
- >> fs []
- (* applying lameq_principle_hnf_size_eq' *)
- >> Know ‘n = n' /\ vs = vs'’
- >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\
-     qunabbrevl_tac [‘n’, ‘n'’, ‘P0’, ‘Q0’] \\
-     MATCH_MP_TAC lameq_principle_hnf_size_eq' >> art [])
- (* clean up now duplicated abbreviations: n' and vs' *)
- >> qunabbrevl_tac [‘n'’, ‘vs'’]
- >> DISCH_THEN (rfs o wrap o GSYM)
- (* proving y = y' *)
- >> STRONG_CONJ_TAC
- >- (MP_TAC (Q.SPECL [‘r’, ‘X’, ‘P’, ‘Q’, ‘P0’, ‘Q0’, ‘n’, ‘vs’, ‘P1’, ‘Q1’]
-                     lameq_principle_hnf_head_eq) \\
-     simp [GSYM solvable_iff_has_hnf])
- >> DISCH_THEN (rfs o wrap o GSYM)
- >> qunabbrevl_tac [‘y’, ‘y'’]
- (* applying lameq_principle_hnf_thm' *)
- >> MP_TAC (Q.SPECL [‘r’, ‘X’, ‘P’, ‘Q’, ‘P0’, ‘Q0’, ‘n’, ‘vs’, ‘P1’, ‘Q1’]
-                     lameq_principle_hnf_thm)
- >> simp [GSYM solvable_iff_has_hnf]
- >> rw [llist_rel_def, LLENGTH_MAP, EL_MAP]
- >> Cases_on ‘i < LENGTH Ps’ >> fs [LNTH_fromList, EL_MAP]
- >> Q.PAT_X_ASSUM ‘(EL i Ps,SUC r) = z’  (ONCE_REWRITE_TAC o wrap o SYM)
- >> Q.PAT_X_ASSUM ‘(EL i Qs,SUC r) = z'’ (ONCE_REWRITE_TAC o wrap o SYM)
- >> qexistsl_tac [‘EL i Ps’, ‘EL i Qs’, ‘SUC r’] >> simp []
- >> qabbrev_tac ‘n = LAMl_size Q0’
- >> qabbrev_tac ‘m = LENGTH Qs’
- >> CONJ_TAC (* 2 symmetric subgoals *)
- >| [ (* goal 1 (of 2) *)
-      MATCH_MP_TAC subterm_induction_lemma' \\
-      qexistsl_tac [‘P’,‘P0’, ‘n’, ‘m’, ‘vs’, ‘P1’] >> simp [] \\
-      qunabbrev_tac ‘vs’ \\
-      Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’ \\
-     ‘DISJOINT (set vs) (FV P0)’ by METIS_TAC [subterm_disjoint_lemma'] \\
-      Q_TAC (HNF_TAC (“P0 :term”, “vs :string list”,
-                      “y  :string”, “args :term list”)) ‘P1’ \\
-     ‘TAKE (LAMl_size P0) vs = vs’ by rw [] \\
-      POP_ASSUM (rfs o wrap) \\
-      Q.PAT_X_ASSUM ‘LENGTH Ps = m’ (REWRITE_TAC o wrap o SYM) \\
-      AP_TERM_TAC >> simp [Abbr ‘Ps’],
-      (* goal 2 (of 2) *)
-      MATCH_MP_TAC subterm_induction_lemma' \\
-      qexistsl_tac [‘Q’,‘Q0’, ‘n’, ‘m’, ‘vs’, ‘Q1’] >> simp [] \\
-      qunabbrev_tac ‘vs’ \\
-      Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’ \\
-     ‘DISJOINT (set vs) (FV Q0)’ by METIS_TAC [subterm_disjoint_lemma'] \\
-      Q_TAC (HNF_TAC (“Q0 :term”, “vs :string list”,
-                      “y  :string”, “args :term list”)) ‘Q1’ \\
-     ‘TAKE (LAMl_size Q0) vs = vs’ by rw [] \\
-      POP_ASSUM (rfs o wrap) \\
-      qunabbrev_tac ‘m’ \\
-      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
-
 (*---------------------------------------------------------------------------*
  *  An equivalence relation of terms
  *---------------------------------------------------------------------------*)
@@ -675,6 +554,127 @@ Proof
       SET_TAC [] ]
 QED
 
+(*---------------------------------------------------------------------------*
+ *  Boehm trees of beta/eta equivalent terms
+ *---------------------------------------------------------------------------*)
+
+(* Proposition 10.1.6 [1, p.219] *)
+Theorem lameq_BT_cong :
+    !X M N r. FINITE X /\ FV M UNION FV N SUBSET X /\ M == N ==>
+              BT' X M r = BT' X N r
+Proof
+    RW_TAC std_ss []
+ >> reverse (Cases_on ‘solvable M’)
+ >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\
+     rw [BT_of_unsolvables])
+ >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong]
+ (* applying ltree_bisimulation *)
+ >> rw [ltree_bisimulation]
+ (* NOTE: ‘solvable P /\ solvable Q’ cannot be added here *)
+ >> Q.EXISTS_TAC
+     ‘\x y. ?P Q r. FV P UNION FV Q SUBSET X UNION RANK r /\
+                    P == Q /\ x = BT' X P r /\ y = BT' X Q r’
+ >> BETA_TAC
+ >> CONJ_TAC
+ >- (qexistsl_tac [‘M’, ‘N’, ‘r’] >> simp [] \\
+     Q.PAT_X_ASSUM ‘FV M UNION FV N SUBSET X’ MP_TAC \\
+     Q.PAT_X_ASSUM ‘FINITE X’ MP_TAC \\
+     SET_TAC [])
+ (* stage work *)
+ >> qx_genl_tac [‘a1’, ‘ts1’, ‘a2’, ‘ts2’] >> STRIP_TAC
+ >> qabbrev_tac ‘P0 = principle_hnf P’
+ >> qabbrev_tac ‘Q0 = principle_hnf Q’
+ >> qabbrev_tac ‘n  = LAMl_size P0’
+ >> qabbrev_tac ‘n' = LAMl_size Q0’
+ >> qabbrev_tac ‘vs = RNEWS r n  X’
+ >> qabbrev_tac ‘vs'= RNEWS r n' X’
+ >> qabbrev_tac ‘P1 = principle_hnf (P0 @* MAP VAR vs)’
+ >> qabbrev_tac ‘Q1 = principle_hnf (Q0 @* MAP VAR vs')’
+ >> qabbrev_tac ‘Ps = hnf_children P1’
+ >> qabbrev_tac ‘Qs = hnf_children Q1’
+ >> qabbrev_tac ‘y  = hnf_head P1’
+ >> qabbrev_tac ‘y' = hnf_head Q1’
+ (* applying ltree_unfold *)
+ >> Q.PAT_X_ASSUM ‘_ = BT' X Q r’ MP_TAC
+ >> simp [BT_def, Once ltree_unfold, BT_generator_def]
+ >> Q.PAT_X_ASSUM ‘_ = BT' X P r’ MP_TAC
+ >> simp [BT_def, Once ltree_unfold, BT_generator_def]
+ >> NTAC 2 STRIP_TAC
+ (* easy case: unsolvable P (and Q) *)
+ >> reverse (Cases_on ‘solvable P’)
+ >- (‘unsolvable Q’ by PROVE_TAC [lameq_solvable_cong] >> fs [] \\
+     rw [llist_rel_def, LLENGTH_MAP])
+ (* now both P and Q are solvable *)
+ >> ‘solvable Q’ by PROVE_TAC [lameq_solvable_cong]
+ >> fs []
+ (* applying lameq_principle_hnf_size_eq' *)
+ >> Know ‘n = n' /\ vs = vs'’
+ >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\
+     qunabbrevl_tac [‘n’, ‘n'’, ‘P0’, ‘Q0’] \\
+     MATCH_MP_TAC lameq_principle_hnf_size_eq' >> art [])
+ (* clean up now duplicated abbreviations: n' and vs' *)
+ >> qunabbrevl_tac [‘n'’, ‘vs'’]
+ >> DISCH_THEN (rfs o wrap o GSYM)
+ (* proving y = y' *)
+ >> STRONG_CONJ_TAC
+ >- (MP_TAC (Q.SPECL [‘r’, ‘X’, ‘P’, ‘Q’, ‘P0’, ‘Q0’, ‘n’, ‘vs’, ‘P1’, ‘Q1’]
+                     lameq_principle_hnf_head_eq) \\
+     simp [GSYM solvable_iff_has_hnf])
+ >> DISCH_THEN (rfs o wrap o GSYM)
+ >> qunabbrevl_tac [‘y’, ‘y'’]
+ (* applying lameq_principle_hnf_thm' *)
+ >> MP_TAC (Q.SPECL [‘r’, ‘X’, ‘P’, ‘Q’, ‘P0’, ‘Q0’, ‘n’, ‘vs’, ‘P1’, ‘Q1’]
+                     lameq_principle_hnf_thm)
+ >> simp [GSYM solvable_iff_has_hnf]
+ >> rw [llist_rel_def, LLENGTH_MAP, EL_MAP]
+ >> Cases_on ‘i < LENGTH Ps’ >> fs [LNTH_fromList, EL_MAP]
+ >> Q.PAT_X_ASSUM ‘(EL i Ps,SUC r) = z’  (ONCE_REWRITE_TAC o wrap o SYM)
+ >> Q.PAT_X_ASSUM ‘(EL i Qs,SUC r) = z'’ (ONCE_REWRITE_TAC o wrap o SYM)
+ >> qexistsl_tac [‘EL i Ps’, ‘EL i Qs’, ‘SUC r’] >> simp []
+ >> qabbrev_tac ‘n = LAMl_size Q0’
+ >> qabbrev_tac ‘m = LENGTH Qs’
+ >> CONJ_TAC (* 2 symmetric subgoals *)
+ >| [ (* goal 1 (of 2) *)
+      MATCH_MP_TAC subterm_induction_lemma' \\
+      qexistsl_tac [‘P’,‘P0’, ‘n’, ‘m’, ‘vs’, ‘P1’] >> simp [] \\
+      qunabbrev_tac ‘vs’ \\
+      Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’ \\
+     ‘DISJOINT (set vs) (FV P0)’ by METIS_TAC [subterm_disjoint_lemma'] \\
+      Q_TAC (HNF_TAC (“P0 :term”, “vs :string list”,
+                      “y  :string”, “args :term list”)) ‘P1’ \\
+     ‘TAKE (LAMl_size P0) vs = vs’ by rw [] \\
+      POP_ASSUM (rfs o wrap) \\
+      Q.PAT_X_ASSUM ‘LENGTH Ps = m’ (REWRITE_TAC o wrap o SYM) \\
+      AP_TERM_TAC >> simp [Abbr ‘Ps’],
+      (* goal 2 (of 2) *)
+      MATCH_MP_TAC subterm_induction_lemma' \\
+      qexistsl_tac [‘Q’,‘Q0’, ‘n’, ‘m’, ‘vs’, ‘Q1’] >> simp [] \\
+      qunabbrev_tac ‘vs’ \\
+      Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’ \\
+     ‘DISJOINT (set vs) (FV Q0)’ by METIS_TAC [subterm_disjoint_lemma'] \\
+      Q_TAC (HNF_TAC (“Q0 :term”, “vs :string list”,
+                      “y  :string”, “args :term list”)) ‘Q1’ \\
+     ‘TAKE (LAMl_size Q0) vs = vs’ by rw [] \\
+      POP_ASSUM (rfs o wrap) \\
+      qunabbrev_tac ‘m’ \\
+      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)
@@ -689,17 +689,6 @@ QED
  *  BT_paths and BT_valid_paths
  *---------------------------------------------------------------------------*)
 
-(* By subterm_tpm_cong and BT_ltree_paths_thm, etc. *)
-Theorem BT_ltree_paths_cong :
-    !X Y M r r'. FINITE X /\ FINITE Y /\
-                 FV M SUBSET X UNION RANK r /\
-                 FV M SUBSET Y UNION RANK r'
-             ==> ltree_paths (BT' X M r) = ltree_paths (BT' Y M r')
-Proof
-    rw [Once EXTENSION, BT_ltree_paths_thm]
- >> MATCH_MP_TAC (cj 1 subterm_tpm_cong) >> art []
-QED
-
 Definition BT_paths_def :
     BT_paths M = ltree_paths (BT' (FV M) M 0)
 End
@@ -718,7 +707,7 @@ Proof
  >> MATCH_MP_TAC BT_ltree_paths_cong >> simp []
 QED
 
-Theorem IN_BT_paths :
+Theorem BT_paths_eq_subterm_not_none :
     !X M p r. FINITE X /\ FV M SUBSET X UNION RANK r ==>
              (p IN BT_paths M <=> subterm X M p r <> NONE)
 Proof
@@ -1873,7 +1862,7 @@ Proof
  (* stage work *)
  >> ‘?M0. M == M0 /\ hnf M0’ by METIS_TAC [has_hnf_def, solvable_iff_has_hnf]
  >> ‘?vs args y. ALL_DISTINCT vs /\ M0 = LAMl vs (VAR y @* args)’
-       by METIS_TAC [hnf_cases]
+      by METIS_TAC [hnf_cases]
  >> qabbrev_tac ‘as = NEWS (LENGTH args) (FV P)’
  >> qabbrev_tac ‘pi = [LAMl as P/y]::MAP rightctxt (MAP VAR (REVERSE vs))’
  >> Q.EXISTS_TAC ‘pi’
@@ -1903,11 +1892,11 @@ Proof
  >- (irule lameq_sub_cong >> rw [lameq_LAMl_appstar_VAR])
  >> rw [Abbr ‘t’, appstar_SUB]
  >> ‘DISJOINT (set as) (FV P) /\ LENGTH as = LENGTH args’
-       by rw [NEWS_def, Abbr ‘as’]
+      by rw [NEWS_def, Abbr ‘as’]
  >> MATCH_MP_TAC lameq_LAMl_appstar_reduce >> rw []
 QED
 
-(* Theorem 10.4.2 (i) [1, p.256]
+(* Theorem 10.4.2 (i) [1, p.256] *)
 Theorem separability_thm :
     !M N. benf M /\ benf N /\ M <> N ==>
          !P Q. ?pi. Boehm_transform pi /\ apply pi M == P /\ apply pi N == Q
@@ -2042,7 +2031,6 @@ Proof
       (* goal 7 (of 7) *)
       PROVE_TAC [conversion_compatible, compatible_def, absctxt] ]
 QED
-*)
 
 val _ = export_theory ();
 val _ = html_theory "lameta_complete";