Fix breakage

Author: ordinarymath

examples/lambda/barendregt/boehmScript.sml

@@ -1058,7 +1058,7 @@ Proof
  >> reverse (Cases_on ‘solvable M’)
  >- rw [subterm_def, BT_of_unsolvables, ltree_el_def]
  (* stage work *)
- >> rw [subterm_def, BT_def, BT_generator_def, Once ltree_unfold, ltree_el_def]
+ >> simp[subterm_def, BT_def, BT_generator_def, Once ltree_unfold, ltree_el_def]
  >> qabbrev_tac ‘M0 = principle_hnf M’
  >> qabbrev_tac ‘n  = LAMl_size M0’
  >> Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’

examples/lambda/barendregt/normal_orderScript.sml

@@ -188,7 +188,8 @@ val bnf_noposn = store_thm(
   "bnf_noposn",
   ``∀M. bnf M ⇔ (noposn M = NONE)``,
   HO_MATCH_MP_TAC simple_induction THEN
-  SRW_TAC [][] THEN Cases_on `noposn M` THEN SRW_TAC [][])
+  SRW_TAC [][] THEN Cases_on `noposn M` THEN
+  SRW_TAC [][EQ_IMP_THM])
 
 val normorder_noposn = store_thm(
   "normorder_noposn",

src/finite_maps/alist_treeScript.sml

@@ -307,11 +307,10 @@ Theorem is_lookup_far_left:
   !R k k' v. R k k' ==> is_lookup F T R [(k', v)] k NONE
 Proof
   fs [is_lookup_def, sortingTheory.SORTED_EQ, listTheory.MEM_MAP,
-      pairTheory.EXISTS_PROD]
+      pairTheory.EXISTS_PROD,alistTheory.ALOOKUP_NONE,PULL_EXISTS]
   \\ rpt strip_tac
-  \\ Cases_on `ALOOKUP ys k` \\ CASE_TAC \\ fs []
-  \\ metis_tac [alistTheory.ALOOKUP_MEM, relationTheory.irreflexive_def,
-    relationTheory.transitive_def]
+  \\ metis_tac [ relationTheory.irreflexive_def,
+     relationTheory.transitive_def]
 QED
 
 Theorem is_lookup_far_right:

src/pred_set/src/more_theories/cardinalScript.sml

@@ -3178,13 +3178,13 @@ Proof
                  else if (!x. x IN s ==> ISR x) /\ IMAGE OUTR s IN As then
                    SOME (INR (THE (SND p (IMAGE OUTR s))))
                  else NONE’ >>
-  rw[] >> simp[AllCaseEqs(), PULL_EXISTS]
+  rw[] >> simp[PULL_EXISTS]
   >- (metis_tac[THE_DEF, MEMBER_NOT_EMPTY])
   >- (rename [‘s = {}’, ‘s <> IMAGE INL A’] >>
-      pop_assum mp_tac >> rw[]
+      rpt (IF_CASES_TAC >> fs[])
       >- (qpat_x_assum ‘s <> IMAGE INL _’ mp_tac >>
-          csimp[EXTENSION, PULL_EXISTS, sumTheory.INL]) >>
-      first_x_assum $ qspec_then ‘IMAGE OUTR s’ mp_tac >> simp[]) >>
+          rw[CONTRAPOS_THM] >> gvs[]) >>
+      fs[DISJ_EQ_IMP]) >>
   qexists_tac ‘λtup. (OUTL (THE (tup (IMAGE INL A))),
                       (λB. if B IN As then
                              SOME (OUTR (THE (tup (IMAGE INR B))))

src/pred_set/src/more_theories/wellorderScript.sml

@@ -595,15 +595,15 @@ val wo2wo_EQ_NONE = store_thm(
   ``!x. (wo2wo w1 w2 x = NONE) ==>
         !y. (x,y) WIN w1 ==> (wo2wo w1 w2 y = NONE)``,
   ONCE_REWRITE_TAC [wo2wo_thm] >> rw[LET_THM] >>
-  match_mp_tac SUBSET_ANTISYM >> rw[IMAGE_wo2wo_SUBSET] >>
-  match_mp_tac SUBSET_TRANS >>
-  qexists_tac `IMAGE THE (IMAGE (wo2wo w1 w2) (iseg w1 x) DELETE NONE)` >>
-  conj_tac >- (
-    Cases_on`wleast w2 (IMAGE THE (IMAGE (wo2wo w1 w2) (iseg w1 x) DELETE NONE))` >>
-    imp_res_tac wleast_EQ_NONE >> fs[] ) >>
-  simp_tac (srw_ss() ++ DNF_ss) [SUBSET_DEF] >>
-  qsuff_tac `!a. a IN iseg w1 x ==> a IN iseg w1 y` >- metis_tac[] >>
-  rw[iseg_def] >> metis_tac [WIN_TRANS]);
+  fs[IMAGE_wo2wo_SUBSET,SET_EQ_SUBSET]
+  >- (
+    qsuff_tac `elsOf w2 ⊆ IMAGE THE (IMAGE (wo2wo w1 w2) (iseg w1 y) DELETE NONE)` >- fs[] >>
+    MATCH_MP_TAC SUBSET_TRANS >>
+    first_x_assum (irule_at (Pos hd)) >>
+    simp_tac (srw_ss() ++ DNF_ss) [SUBSET_DEF] >>
+    qsuff_tac `!a. a IN iseg w1 x ==> a IN iseg w1 y` >- metis_tac[] >>
+    rw[iseg_def] >> METIS_TAC[WIN_TRANS])
+  >- imp_res_tac wleast_EQ_NONE);
 
 val wo2wo_EQ_SOME_downwards = store_thm(
   "wo2wo_EQ_SOME_downwards",