diff --git a/src/boss/prove_base_assumsScript.sml b/src/boss/prove_base_assumsScript.sml
index 1f54931f3a..3d4fded15b 100644
--- a/src/boss/prove_base_assumsScript.sml
+++ b/src/boss/prove_base_assumsScript.sml
@@ -159,11 +159,216 @@ val TYPE_DEFINITION = add_def(concl TYPE_DEFINITION)
 val ARB_DEF = add_def(concl (REFL``ARB``))
 
 val goalsNet = read_article "hol4-assums.art" reader;
-val goals = Net.listItems goalsNet;
+val goals_unsorted = Net.listItems goalsNet;
 
 val _ = Parse.hide "_";
 
-(* val bool_cases = hd(amatch ``t \/ ~t``); *)
+(* NOTE: By sorting the above goals, the order of goals will be more stable
+   after changes to HOL core theories. -- Chun Tian, 30 nov 2024
+ *)
+fun term_lt t1 t2 = (Term.compare(t1,t2) = LESS);
+fun thm_lt th1 th2 = term_lt (concl th1) (concl th2);
+val goals = sort thm_lt goals_unsorted;
+
+(* NOTE: contents of goals (List.length goals = 96)
+val goals =
+ 1 [|- !t1 t2. ?fn. fn T = t1 /\ fn F = t2,
+ 2  |- !t1 t2. (if T then t1 else t2) = t1 /\ (if F then t1 else t2) = t2,
+ 3  |- !a0 a1 a0' a1'.
+         Data_List_cons a0 a1 = Data_List_cons a0' a1' <=>
+         a0 = a0' /\ a1 = a1',
+ 4  |- !h t.
+         Data_List_last (Data_List_cons h t) =
+         if t = Data_List_nil then h else Data_List_last t,
+ 5  |- !x. (@y. x = y) = x,
+ 6  |- !x. x = x <=> T,
+ 7  |- !x f. ?!fn1.
+         fn1 Data_List_nil = x /\
+         !h t. fn1 (Data_List_cons h t) = f (fn1 t) h t,
+ 8  |- !a1 a0. Data_List_nil <> Data_List_cons a0 a1,
+ 9  |- !m n. Number_Natural_suc m = Number_Natural_suc n ==> m = n,
+ 10 |- !n. Number_Natural_less Number_Natural_zero n ==>
+           !k. k =
+               Number_Natural_plus
+                 (Number_Natural_times (Number_Natural_div k n) n)
+                 (Number_Natural_mod k n) /\
+               Number_Natural_less (Number_Natural_mod k n) n,
+ 11 |- !P Q x x' y y'.
+         (P <=> Q) /\ (Q ==> x = x') /\ (~Q ==> y = y') ==>
+         (if P then x else y) = if Q then x' else y',
+ 12 |- !x x' y y'.
+         (x <=> x') /\ (x' ==> (y <=> y')) ==> (x ==> y <=> x' ==> y'),
+ 13 |- !P P' Q Q'.
+         (Q ==> (P <=> P')) /\ (P' ==> (Q <=> Q')) ==> (P /\ Q <=> P' /\ Q'),
+ 14 |- !t1 t2 t3. t1 /\ t2 /\ t3 <=> (t1 /\ t2) /\ t3,
+ 15 |- !A B C. (B \/ C) /\ A <=> B /\ A \/ C /\ A,
+ 16 |- !A B C. A \/ B \/ C <=> (A \/ B) \/ C,
+ 17 |- !A B C. B /\ C \/ A <=> (B \/ A) /\ (C \/ A),
+ 18 |- !A B. (~(A /\ B) <=> ~A \/ ~B) /\ (~(A \/ B) <=> ~A /\ ~B),
+ 19 |- !t1 t2. (t1 <=> t2) <=> (t1 ==> t2) /\ (t2 ==> t1),
+ 20 |- !A B. (A <=> B \/ A) <=> B ==> A,
+ 21 |- !A B. A \/ B <=> ~A ==> B,
+ 22 |- !t1 t2. (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 <=> t2),
+ 23 |- !t. (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\
+           (t /\ F <=> F) /\ (t /\ t <=> t),
+ 24 |- !t. ((T <=> t) <=> t) /\ ((t <=> T) <=> t) /\ ((F <=> t) <=> ~t) /\
+           ((t <=> F) <=> ~t),
+ 25 |- !t. (T ==> t <=> t) /\ (t ==> T <=> T) /\ (F ==> t <=> T) /\
+           (t ==> t <=> T) /\ (t ==> F <=> ~t),
+ 26 |- !t. (T \/ t <=> T) /\ (t \/ T <=> T) /\ (F \/ t <=> t) /\
+           (t \/ F <=> t) /\ (t \/ t <=> t),
+ 27 |- !t. t ==> F <=> (t <=> F),
+ 28 |- !t. F ==> t,
+ 29 |- !t. ~t ==> t ==> F,
+ 30 |- !t. (t ==> F) ==> ~t,
+ 31 |- !f b x y. f (if b then x else y) = if b then f x else f y,
+ 32 |- !f g M N. M = N /\ (!x. x = N ==> f x = g x) ==> LET f M = LET g N,
+ 33 |- !f g. f = g <=> !x. f x = g x,
+ 34 |- !f g. ?!h.
+         Function_o h Data_Sum_left = f /\ Function_o h Data_Sum_right = g,
+ 35 |- !P t. (!x. x = t ==> P x) ==> $? P,
+ 36 |- !P Q.
+         (Q ==> (!x. P x) <=> !x. Q ==> P x) /\
+         ((!x. P x) /\ Q <=> !x. P x /\ Q) /\
+         (Q /\ (!x. P x) <=> !x. Q /\ P x),
+ 37 |- !P Q.
+         ((?x. P x) ==> Q <=> !x. P x ==> Q) /\
+         ((?x. P x) /\ Q <=> ?x. P x /\ Q) /\
+         (Q /\ (?x. P x) <=> ?x. Q /\ P x),
+ 38 |- !P f. RES_EXISTS P f <=> ?x. x IN P /\ f x,
+ 39 |- !P f.
+         RES_EXISTS_UNIQUE P f <=>
+         (?x::P. f x) /\ !x y::P. f x /\ f y ==> x = y,
+ 40 |- !P f. RES_FORALL P f <=> !x. x IN P ==> f x,
+ 41 |- !P Q. (?x. P x) /\ (!x. P x ==> Q x) ==> Q ($@ P),
+ 42 |- !f. (!x y z. f x (f y z) = f (f x y) z) ==>
+           (!x y. f x y = f y x) ==>
+           !x y z. f x (f y z) = f y (f x z),
+ 43 |- !P. P Data_List_nil /\ (!t. P t ==> !h. P (Data_List_cons h t)) ==>
+           !l. P l,
+ 44 |- ~(t /\ ~t),
+ 45 |- (!x x'. Data_Sum_left x = Data_Sum_left x' <=> x = x') /\
+       !y y'. Data_Sum_right y = Data_Sum_right y' <=> y = y',
+ 46 |- (!x. Data_Option_isNone (Data_Option_some x) <=> F) /\
+       (Data_Option_isNone Data_Option_none <=> T),
+ 47 |- (!x. Data_Option_isSome (Data_Option_some x) <=> T) /\
+       (Data_Option_isSome Data_Option_none <=> F),
+ 48 |- (!x. Data_Sum_isLeft (Data_Sum_left x) <=> T) /\
+       !y. Data_Sum_isLeft (Data_Sum_right y) <=> F,
+ 49 |- (!x. Data_Sum_isRight (Data_Sum_right x) <=> T) /\
+       !y. Data_Sum_isRight (Data_Sum_left y) <=> F,
+ 50 |- (!l. Data_List_append Data_List_nil l = l) /\
+       !h l1 l2.
+         Data_List_append (Data_List_cons h l1) l2 =
+         Data_List_cons h (Data_List_append l1 l2),
+ 51 |- (!n. Number_Natural_plus Number_Natural_zero n = n) /\
+       !m n.
+         Number_Natural_plus (Number_Natural_suc m) n =
+         Number_Natural_suc (Number_Natural_plus m n),
+ 52 |- (!m. Number_Natural_power m Number_Natural_zero =
+            Number_Natural_bit1 Number_Natural_zero) /\
+       !m n.
+         Number_Natural_power m (Number_Natural_suc n) =
+         Number_Natural_times m (Number_Natural_power m n),
+ 53 |- (!n. Number_Natural_times Number_Natural_zero n = Number_Natural_zero) /\
+       !m n.
+         Number_Natural_times (Number_Natural_suc m) n =
+         Number_Natural_plus (Number_Natural_times m n) n,
+ 54 |- (!t. ~~t <=> t) /\ (~T <=> F) /\ (~F <=> T),
+ 55 |- (!f x. Data_Option_map f (Data_Option_some x) = Data_Option_some (f x)) /\
+       !f. Data_Option_map f Data_Option_none = Data_Option_none,
+ 56 |- (!f. Data_List_map f Data_List_nil = Data_List_nil) /\
+       !f h t.
+         Data_List_map f (Data_List_cons h t) =
+         Data_List_cons (f h) (Data_List_map f t),
+ 57 |- (!p m x. x IN p ==> RES_ABSTRACT p m x = m x) /\
+       !p m1 m2.
+         (!x. x IN p ==> m1 x = m2 x) ==>
+         RES_ABSTRACT p m1 = RES_ABSTRACT p m2,
+ 58 |- (!P. Data_List_filter P Data_List_nil = Data_List_nil) /\
+       !P h t.
+         Data_List_filter P (Data_List_cons h t) =
+         if P h then Data_List_cons h (Data_List_filter P t)
+         else Data_List_filter P t,
+ 59 |- (!P. Data_List_all P Data_List_nil <=> T) /\
+       !P h t.
+         Data_List_all P (Data_List_cons h t) <=> P h /\ Data_List_all P t,
+ 60 |- (!P. Data_List_any P Data_List_nil <=> F) /\
+       !P h t.
+         Data_List_any P (Data_List_cons h t) <=> P h \/ Data_List_any P t,
+ 61 |- Data_List_concat Data_List_nil = Data_List_nil /\
+       !h t.
+         Data_List_concat (Data_List_cons h t) =
+         Data_List_append h (Data_List_concat t),
+ 62 |- Data_List_reverse Data_List_nil = Data_List_nil /\
+       !h t.
+         Data_List_reverse (Data_List_cons h t) =
+         Data_List_append (Data_List_reverse t)
+           (Data_List_cons h Data_List_nil),
+ 63 |- Data_List_unzip Data_List_nil =
+       Data_Pair_comma Data_List_nil Data_List_nil /\
+       !x l.
+         Data_List_unzip (Data_List_cons x l) =
+         Data_Pair_comma
+           (Data_List_cons (Data_Pair_fst x)
+              (Data_Pair_fst (Data_List_unzip l)))
+           (Data_List_cons (Data_Pair_snd x)
+              (Data_Pair_snd (Data_List_unzip l))),
+ 64 |- Data_List_length Data_List_nil = Number_Natural_zero /\
+       !h t.
+         Data_List_length (Data_List_cons h t) =
+         Number_Natural_suc (Data_List_length t),
+ 65 |- Number_Natural_factorial Number_Natural_zero =
+       Number_Natural_bit1 Number_Natural_zero /\
+       !n. Number_Natural_factorial (Number_Natural_suc n) =
+           Number_Natural_times (Number_Natural_suc n)
+             (Number_Natural_factorial n),
+ 66 |- (Data_List_null Data_List_nil <=> T) /\
+       !h t. Data_List_null (Data_List_cons h t) <=> F,
+ 67 |- (Number_Natural_even Number_Natural_zero <=> T) /\
+       !n. Number_Natural_even (Number_Natural_suc n) <=>
+           ~Number_Natural_even n,
+ 68 |- (Number_Natural_odd Number_Natural_zero <=> F) /\
+       !n. Number_Natural_odd (Number_Natural_suc n) <=>
+           ~Number_Natural_odd n,
+ 69 |- Data_Unit_unit = @x. T,
+ 70 |- Number_Natural_zero = Number_Natural_zero,
+ 71 |- (?!x. F) <=> F,
+ 72 |- Data_Pair_comma x y = Data_Pair_comma a b <=> x = a /\ y = b,
+ 73 |- Data_Sum_left x = Data_Sum_left y <=> x = y,
+ 74 |- Data_Sum_right x = Data_Sum_right y <=> x = y,
+ 75 |- Function_id = Function_Combinator_s Function_const Function_const,
+ 76 |- Relation_empty = (\x y. F),
+ 77 |- Relation_universe = (\x y. T),
+ 78 |- Number_Natural_bit1 =
+       (\n.
+            Number_Natural_plus n
+              (Number_Natural_plus n (Number_Natural_suc Number_Natural_zero))),
+ 79 |- Number_Natural_max = (\m n. if Number_Natural_less m n then n else m),
+ 80 |- Number_Natural_min = (\m n. if Number_Natural_less m n then m else n),
+ 81 |- Number_Natural_greater = (\m n. Number_Natural_less n m),
+ 82 |- Number_Natural_greatereq = (\m n. Number_Natural_greater m n \/ m = n),
+ 83 |- Number_Natural_less =
+       (\m n. ?P. (!n. P (Number_Natural_suc n) ==> P n) /\ P m /\ ~P n),
+ 84 |- Number_Natural_lesseq = (\m n. Number_Natural_less m n \/ m = n),
+ 85 |- Relation_irreflexive = (\R. !x. ~R x x),
+ 86 |- Relation_reflexive = (\R. !x. R x x),
+ 87 |- Relation_transitive = (\R. !x y z. R x y /\ R y z ==> R x z),
+ 88 |- Relation_wellFounded =
+       (\R. !B. (?w. B w) ==> ?min. B min /\ !b. R b min ==> ~B b),
+ 89 |- Relation_transitiveClosure =
+       (\R a b.
+            !P. (!x y. R x y ==> P x y) /\ (!x y z. P x y /\ P y z ==> P x z) ==>
+                P a b),
+ 90 |- Relation_subrelation = (\R1 R2. !x y. R1 x y ==> R2 x y),
+ 91 |- Relation_intersect = (\R1 R2 x y. R1 x y /\ R2 x y),
+ 92 |- Relation_union = (\R1 R2 x y. R1 x y \/ R2 x y),
+ 93 |- Function_o = (\f g x. f (g x)),
+ 94 |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x,
+ 95 |- (x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w,
+ 96 |- (x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w]: thm list
+ *)
+
 val bool_cases = hd(amatch``(x = T) \/ _``);
 val BOOL_CASES_AX = bool_cases;
 
@@ -202,23 +407,71 @@ val truth = hd(amatch``T``);
 val TRUTH = truth;
 val not_F = hd(amatch``~F``);
 
-(* |- ~(t /\ ~t) *)
-val th1 = store_thm("th1", el 1 goals |> concl,
-  PURE_REWRITE_TAC[not_and,not_not]
-  \\ Q.SPEC_THEN`t`FULL_STRUCT_CASES_TAC bool_cases
-  \\ PURE_REWRITE_TAC[or_T,or_F,not_F]);
+val if_T = hd (amatch ``if T then t1 else t2``);
+val if_F = hd (amatch ``if F then t1 else t2``);
+
+(* |- !t1 t2. ?fn. fn T = t1 /\ fn F = t2 *)
+val th1 = store_thm
+  ("th1", el 1 goals |> concl,
+  rpt gen_tac
+  \\ qexists_tac`\b. if b then t1 else t2`
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ PURE_REWRITE_TAC[if_T,if_F]
+  \\ conj_tac \\ REFL_TAC);
+
+(* |- !t1 t2. (if T then t1 else t2) = t1 /\ (if F then t1 else t2) = t2 *)
+val th2 = store_thm
+  ("th2", el 2 goals |> concl,
+  rpt gen_tac \\ MATCH_ACCEPT_TAC (CONJ (SPEC_ALL if_T) (SPEC_ALL if_F)));
+
+val bool_case_lemma = th2;
+
+val cons_11 = hd (amatch ``Data_List_cons  _ _ = Data_List_cons _ _``);
+
+(* |- !a0 a1 a0' a1'.
+          Data_List_cons a0 a1 = Data_List_cons a0' a1' <=>
+          a0 = a0' /\ a1 = a1'
+ *)
+val th3 = store_thm
+  ("th3", el 3 goals |> concl, MATCH_ACCEPT_TAC cons_11);
+
+val null_eq = hd(amatch``Data_List_null t <=> (_ = Data_List_nil)``);
+val last_cons = hd(amatch``Data_List_last (Data_List_cons h t) = COND _ _ _``);
+
+(* |- !h t.
+          Data_List_last (Data_List_cons h t) =
+          if t = Data_List_nil then h else Data_List_last t
+ *)
+val th4 = store_thm
+  ("th4", el 4 goals |> concl,
+  MATCH_ACCEPT_TAC(PURE_REWRITE_RULE[null_eq]last_cons));
+
+val select_eq = hd(amatch``@y. y = x``)
+
+(* |- !x. (@y. x = y) = x *)
+val th5 = store_thm
+  ("th5", el 5 goals |> concl,
+  CONV_TAC(QUANT_CONV(LAND_CONV(RAND_CONV(ABS_CONV SYM_CONV))))
+  \\ MATCH_ACCEPT_TAC select_eq);
+
+val refl = hd(amatch``!x. x = x``);
+
+(* |- !x. x = x <=> T *)
+val th6 = store_thm
+  ("th6", el 6 goals |> concl,
+  gen_tac \\ MATCH_ACCEPT_TAC(EQT_INTRO(SPEC_ALL refl)));
 
 val ex_unique_thm = hd (amatch``(?!x. p x) <=> _ /\ _``);
 val list_rec = hd(amatch``fn (Data_List_cons h t) = f h t (fn t)``);
 val list_ind = hd(amatch``_ ==> !l:'a Data_List_list. P l``);
 val fun_eq_thm = hd(amatch``(!x. f x = g x) <=> (f = g)``);
 
-(* |- !x f.
-          ?!fn1.
-              fn1 Data_List_nil = x /\
-              !h t. fn1 (Data_List_cons h t) = f (fn1 t) h t
+(* |- !x f. ?!fn1.
+        fn1 Data_List_nil = x /\
+        !h t. fn1 (Data_List_cons h t) = f (fn1 t) h t
  *)
-val th2 = store_thm("th2", el 2 goals |> concl,
+val th7 = store_thm
+  ("th7", el 7 goals |> concl,
   rpt gen_tac
   \\ CONV_TAC(HO_REWR_CONV ex_unique_thm)
   \\ conj_tac >- (
@@ -237,36 +490,41 @@ val th2 = store_thm("th2", el 2 goals |> concl,
   \\ disch_then(SUBST_ALL_TAC o SYM)
   \\ disch_then (MATCH_ACCEPT_TAC));
 
-val o_def = hd(amatch``Function_o = _``);
+val cons_neq_nil = hd(amatch``Data_List_cons _ _ <> Data_List_nil``);
 
-val sum_cases = hd(amatch``(?a. x = Data_Sum_left a) \/ _``);
-val sum_ind = hd(amatch``_ ==> !l:('a,'b) Data_Sum_sum. P l``);
+(* |- !a1 a0. Data_List_nil <> Data_List_cons a0 a1 *)
+val th8 = store_thm
+  ("th8", el 8 goals |> concl, MATCH_ACCEPT_TAC (GSYM cons_neq_nil));
 
-val sum_case_thms = amatch``Data_Sum_case_left_right f g (_ _) = _``;
+val suc_11 = hd(amatch``Number_Natural_suc _ = Number_Natural_suc _``);
+
+(* |- !m n. Number_Natural_suc m = Number_Natural_suc n ==> m = n *)
+val th9 = store_thm
+  ("th9", el 9 goals |> concl,
+  rpt gen_tac \\ MATCH_ACCEPT_TAC (#1 (EQ_IMP_RULE (SPEC_ALL suc_11))));
+
+val less_zero = hd(amatch``Number_Natural_less Number_Natural_zero n <=> _ <> _``);
+val div_mod = hd(amatch``Number_Natural_times (Number_Natural_div k n) n``);
+val less_mod = hd(amatch``Number_Natural_less (Number_Natural_mod _ _)``);
 
-(* |- !f g.
-          ?!h.
-              Function_o h Data_Sum_left = f /\
-              Function_o h Data_Sum_right = g: thm
+(* |- !n.
+          Number_Natural_less Number_Natural_zero n ==>
+          !k. k =
+              Number_Natural_plus
+                (Number_Natural_times (Number_Natural_div k n) n)
+                (Number_Natural_mod k n) /\
+              Number_Natural_less (Number_Natural_mod k n) n
  *)
-val th3 = store_thm("th3", el 3 goals |> concl,
-  rpt gen_tac
-  \\ CONV_TAC(HO_REWR_CONV ex_unique_thm)
-  \\ PURE_REWRITE_TAC[o_def]
-  \\ PURE_REWRITE_TAC[GSYM fun_eq_thm]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ rpt strip_tac
-  >- (
-    qexists_tac`Data_Sum_case_left_right f g`
-    \\ PURE_REWRITE_TAC sum_case_thms
-    \\ PURE_REWRITE_TAC[fun_eq_thm]
-    \\ conj_tac \\ REFL_TAC )
-  \\ Q.ISPEC_THEN`x`FULL_STRUCT_CASES_TAC sum_cases
-  >- (
-    rpt(first_x_assum(qspec_then`a`SUBST_ALL_TAC))
-    \\ REFL_TAC)
-  \\ rpt(first_x_assum(qspec_then`b`SUBST_ALL_TAC))
-  \\ REFL_TAC);
+val th10 = store_thm
+  ("th10", el 10 goals |> concl,
+  PURE_REWRITE_TAC[less_zero]
+  \\ gen_tac
+  \\ disch_then(fn th => (strip_assume_tac (MATCH_MP less_mod th) >>
+       (strip_assume_tac (MATCH_MP div_mod th))))
+  \\ gen_tac
+  \\ first_x_assum(qspec_then`k`SUBST_ALL_TAC)
+  \\ conj_tac >- REFL_TAC
+  \\ first_x_assum(qspec_then`k`ACCEPT_TAC));
 
 val if_T = hd(amatch``(if T then _ else _) = _``);
 val if_F = hd(amatch``(if F then _ else _) = _``);
@@ -275,7 +533,8 @@ val if_F = hd(amatch``(if F then _ else _) = _``);
           (P <=> Q) /\ (Q ==> x = x') /\ (~Q ==> y = y') ==>
           (if P then x else y) = if Q then x' else y'
  *)
-val th4 = store_thm("th4", el 4 goals |> concl,
+val th11 = store_thm
+  ("th11", el 11 goals |> concl,
   rpt gen_tac
   \\ rpt strip_tac
   \\ last_x_assum SUBST_ALL_TAC
@@ -284,6 +543,19 @@ val th4 = store_thm("th4", el 4 goals |> concl,
   \\ first_x_assum match_mp_tac
   \\ PURE_REWRITE_TAC[truth,not_F]);
 
+(* |- !x x' y y'.
+          (x <=> x') /\ (x' ==> (y <=> y')) ==> (x ==> y <=> x' ==> y')
+ *)
+val th12 = store_thm
+  ("th12", el 12 goals |> concl,
+  rpt strip_tac
+  \\ last_x_assum SUBST_ALL_TAC
+  \\ Q.ISPEC_THEN`x'`FULL_STRUCT_CASES_TAC bool_cases
+  \\ pop_assum mp_tac
+  \\ PURE_REWRITE_TAC[T_imp,F_imp]
+  \\ TRY REFL_TAC
+  \\ disch_then ACCEPT_TAC);
+
 val T_and = hd(amatch``T /\ t``);
 val and_T = hd(amatch``t /\ T <=> _``);
 val F_and = hd(amatch``F /\ t``);
@@ -293,7 +565,8 @@ val and_i = hd(amatch``t /\ t``);
 (* |- !P P' Q Q'.
           (Q ==> (P <=> P')) /\ (P' ==> (Q <=> Q')) ==> (P /\ Q <=> P' /\ Q')
  *)
-val th5 = store_thm("th5", el 5 goals |> concl,
+val th13 = store_thm
+  ("th13", el 13 goals |> concl,
   rpt strip_tac
   \\ Q.ISPEC_THEN`Q`FULL_STRUCT_CASES_TAC bool_cases
   \\ Q.ISPEC_THEN`P'`FULL_STRUCT_CASES_TAC bool_cases
@@ -304,261 +577,126 @@ val th5 = store_thm("th5", el 5 goals |> concl,
   \\ disch_then(SUBST_ALL_TAC o EQT_INTRO)
   \\ REFL_TAC);
 
-(* |- !f g M N. M = N /\ (!x. x = N ==> f x = g x) ==> LET f M = LET g N *)
-val th6 = store_thm (* was: LET_CONG *)
-  ("th6", el 6 goals |> concl,
-  rpt strip_tac
-  \\ VAR_EQ_TAC
-  \\ PURE_REWRITE_TAC[LET_DEF]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ first_x_assum match_mp_tac
-  \\ REFL_TAC);
-
-(* |- !x x' y y'.
-          (x <=> x') /\ (x' ==> (y <=> y')) ==> (x ==> y <=> x' ==> y')
- *)
-val th7 = store_thm
-  ("th7", el 7 goals |> concl,
-  rpt strip_tac
-  \\ last_x_assum SUBST_ALL_TAC
-  \\ Q.ISPEC_THEN`x'`FULL_STRUCT_CASES_TAC bool_cases
-  \\ pop_assum mp_tac
-  \\ PURE_REWRITE_TAC[T_imp,F_imp]
-  \\ TRY REFL_TAC
-  \\ disch_then ACCEPT_TAC);
-
-val cons_11 = hd (amatch ``Data_List_cons  _ _ = Data_List_cons _ _``);
-
-(* |- !a0 a1 a0' a1'.
-          Data_List_cons a0 a1 = Data_List_cons a0' a1' <=>
-          a0 = a0' /\ a1 = a1'
- *)
-val th8 = store_thm
-  ("th8", el 8 goals |> concl, MATCH_ACCEPT_TAC cons_11);
-
-val app_if = hd (amatch ``f (if b then x else y) = if b then f x else f y``);
-
-(* |- !f b x y. f (if b then x else y) = if b then f x else f y *)
-val th9 = store_thm
-  ("th9", el 9 goals |> concl, MATCH_ACCEPT_TAC app_if);
-
-val demorgan = hd (amatch``(b \/ a) /\ (c \/ a)``);
-
-(* |- !A B C. B /\ C \/ A <=> (B \/ A) /\ (C \/ A) *)
-val th10 = store_thm
-  ("th10", el 10 goals |> concl, MATCH_ACCEPT_TAC demorgan);
-
-val or_assoc = hd (amatch``(a \/ b) \/ c``);
+val and_assoc = hd (amatch``(a /\ b) /\ c``);
 
-(* |- !A B C. A \/ B \/ C <=> (A \/ B) \/ C *)
-val th11 = store_thm
-  ("th11", el 11 goals |> concl, MATCH_ACCEPT_TAC (GSYM or_assoc));
+(* |- !t1 t2 t3. t1 /\ t2 /\ t3 <=> (t1 /\ t2) /\ t3 *)
+val th14 = store_thm
+  ("th14", el 14 goals |> concl, MATCH_ACCEPT_TAC (GSYM and_assoc));
 
 val or_distrib_and = hd (amatch``(b \/ c) /\ a <=> _``);
 
 (* |- !A B C. (B \/ C) /\ A <=> B /\ A \/ C /\ A *)
-val th12 = store_thm
-  ("th12", el 12 goals |> concl, MATCH_ACCEPT_TAC or_distrib_and);
+val th15 = store_thm
+  ("th15", el 15 goals |> concl, MATCH_ACCEPT_TAC or_distrib_and);
 
-val and_assoc = hd (amatch``(a /\ b) /\ c``);
+val or_assoc = hd (amatch``(a \/ b) \/ c``);
 
-(* |- !t1 t2 t3. t1 /\ t2 /\ t3 <=> (t1 /\ t2) /\ t3 *)
-val th13 = store_thm
-  ("th13", el 13 goals |> concl, MATCH_ACCEPT_TAC (GSYM and_assoc));
+(* |- !A B C. A \/ B \/ C <=> (A \/ B) \/ C *)
+val th16 = store_thm
+  ("th16", el 16 goals |> concl, MATCH_ACCEPT_TAC (GSYM or_assoc));
 
-val if_T = hd (amatch ``if T then t1 else t2``);
-val if_F = hd (amatch ``if F then t1 else t2``);
+val demorgan = hd (amatch``(b \/ a) /\ (c \/ a)``);
 
-(* |- !t1 t2. ?fn. fn T = t1 /\ fn F = t2 *)
-val th14 = store_thm
-  ("th14", el 14 goals |> concl,
-  rpt gen_tac
-  \\ qexists_tac`\b. if b then t1 else t2`
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ PURE_REWRITE_TAC[if_T,if_F]
-  \\ conj_tac \\ REFL_TAC);
+(* |- !A B C. B /\ C \/ A <=> (B \/ A) /\ (C \/ A) *)
+val th17 = store_thm
+  ("th17", el 17 goals |> concl, MATCH_ACCEPT_TAC demorgan);
 
 val not_or = hd(amatch``~(_ \/ _)``);
 
 (* |- !A B. (~(A /\ B) <=> ~A \/ ~B) /\ (~(A \/ B) <=> ~A /\ ~B) *)
-val th15 = store_thm
-  ("th15", el 15 goals |> concl,
+val th18 = store_thm
+  ("th18", el 18 goals |> concl,
   rpt gen_tac
   \\ PURE_REWRITE_TAC[not_and,not_or]
   \\ conj_tac \\ REFL_TAC);
 
-val and_ex = hd(amatch``p /\ (?x. _) <=> ?x. p /\ _``);
-val ex_and = hd(amatch``(?x. _) /\ p <=> ?x. _ /\ p``);
-val ex_imp = hd(amatch``((?x. _) ==> _) <=> _``);
-
-(* |- !P Q.
-          ((?x. P x) ==> Q <=> !x. P x ==> Q) /\
-          ((?x. P x) /\ Q <=> ?x. P x /\ Q) /\
-          (Q /\ (?x. P x) <=> ?y. Q /\ P y)
- *)
-val th16 = store_thm
-  ("th16", el 16 goals |> concl,
+(* |- !t1 t2. (t1 <=> t2) <=> (t1 ==> t2) /\ (t2 ==> t1) *)
+val th19 = store_thm
+  ("th19", el 19 goals |> concl,
   rpt gen_tac
-  \\ PURE_REWRITE_TAC[and_ex,ex_and,ex_imp]
-  \\ rpt conj_tac \\ REFL_TAC);
+  \\ Q.ISPEC_THEN`t1`FULL_STRUCT_CASES_TAC bool_cases
+  \\ PURE_REWRITE_TAC[T_iff,F_iff,T_imp,F_imp,imp_T,imp_F,and_T,T_and]
+  \\ REFL_TAC);
 
-val and_all = hd(amatch``p /\ (!x. _) <=> !x. p /\ _``);
-val all_and = hd(amatch``(!x. _) /\ p <=> !x. _ /\ p``);
-val all_imp = hd(amatch``((!x. _) ==> _) <=> _``);
-val imp_all = hd(amatch``(_ ==> (!x. _)) <=> _``);
+val eq_imp_thm = th19;
 
-(* |- !P Q.
-          (Q ==> (!x. P x) <=> !x. Q ==> P x) /\
-          ((!x. P x) /\ Q <=> !x. P x /\ Q) /\
-          (Q /\ (!x. P x) <=> !x. Q /\ P x)
- *)
-val th17 = store_thm
-  ("th17", el 17 goals |> concl,
+(* |- !A B. (A <=> B \/ A) <=> B ==> A *)
+val th20 = store_thm
+  ("th20", el 20 goals |> concl,
   rpt gen_tac
-  \\ PURE_REWRITE_TAC[and_all,all_and,all_imp,imp_all]
-  \\ rpt conj_tac \\ REFL_TAC);
-
-(* |- !t1 t2. (if T then t1 else t2) = t1 /\ (if F then t1 else t2) = t2
- *)
-val th18 = store_thm
-  ("th18", el 18 goals |> concl,
-  rpt gen_tac \\ MATCH_ACCEPT_TAC (CONJ (SPEC_ALL if_T) (SPEC_ALL if_F)));
+  \\ Q.ISPEC_THEN`A`FULL_STRUCT_CASES_TAC bool_cases
+  \\ PURE_REWRITE_TAC[T_iff,or_T,F_iff,or_F,imp_T,imp_F]
+  \\ REFL_TAC);
 
-val forall_eq = hd(amatch``!x. (x = t) ==> _``);
-val forall_eq2 = hd(amatch``!x. (t = x) ==> _``);
+(* |- !A B. A \/ B <=> ~A ==> B (DISJ_EQ_IMP) *)
+val th21 = save_thm
+  ("th21", (* this forward proof comes from boolScript.sml *)
+  let
+    val lemma = not_not |> SPEC ``A:bool``
+  in
+    IMP_DISJ_THM
+    |> SPECL [``~A:bool``,``B:bool``]
+    |> SYM
+    |> CONV_RULE
+      ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV)
+         (fn tm => lemma))
+    |> GENL [``A:bool``,``B:bool``]
+  end);
 
-val ex_def = hd(amatch``$? = _``);
-val select_ax = hd(amatch ``p t ==> p ($@ p)``);
+val _ = if concl th21 ~~ concl (el 21 goals) then ()
+        else raise ERR "th21" "assumptions changed";
 
-(* |- !P t. (!x. x = t ==> P x) ==> $? P *)
-val th19 = store_thm
-  ("th19", el 19 goals |> concl,
-  PURE_REWRITE_TAC[forall_eq,ex_def]
+(* |- !t1 t2. (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 <=> t2) *)
+val th22 = store_thm
+  ("th22", el 22 goals |> concl,
+  rpt strip_tac
+  \\ Q.ISPEC_THEN ‘t1’ mp_tac bool_cases
+  \\ PURE_REWRITE_TAC[or_def]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ MATCH_ACCEPT_TAC select_ax);
+  \\ disch_then(qspec_then ‘t1 = t2’ mp_tac)
+  \\ PURE_REWRITE_TAC[iff_T,iff_F,and_imp_intro]
+  \\ disch_then match_mp_tac
+  \\ conj_tac
+  \\ TRY (disch_then(SUBST_ALL_TAC o EQF_INTRO))
+  \\ TRY (disch_then(SUBST_ALL_TAC o EQT_INTRO))
+  \\ rpt (pop_assum mp_tac)
+  \\ PURE_REWRITE_TAC[T_imp,T_iff,imp_T,F_imp,F_iff,imp_F]
+  \\ disch_then ACCEPT_TAC);
 
-val eta_ax = hd(amatch``!f. (\x. f x) = f``);
+val imp_antisym_ax = th22;
 
-(* |- !P Q. (?x. P x) /\ (!x. P x ==> Q x) ==> Q ($@ P) *)
-val th20 = store_thm
-  ("th20", el 20 goals |> concl,
-  PURE_REWRITE_TAC[ex_def]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ rpt strip_tac
-  \\ first_x_assum match_mp_tac
-  \\ CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV (GSYM eta_ax))))
-  \\ first_x_assum ACCEPT_TAC);
-
-(* |- !t1 t2. (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 <=> t2) *)
-val th21 = store_thm
-  ("th21", el 21 goals |> concl,
-  rpt strip_tac
-  \\ Q.ISPEC_THEN`t1`mp_tac bool_cases
-  \\ PURE_REWRITE_TAC[or_def]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ disch_then(qspec_then`t1 = t2`mp_tac)
-  \\ PURE_REWRITE_TAC[iff_T,iff_F,and_imp_intro]
-  \\ disch_then match_mp_tac
-  \\ conj_tac
-  \\ TRY (disch_then(SUBST_ALL_TAC o EQF_INTRO))
-  \\ TRY (disch_then(SUBST_ALL_TAC o EQT_INTRO))
-  \\ rpt (pop_assum mp_tac)
-  \\ PURE_REWRITE_TAC[T_imp,T_iff,imp_T,F_imp,F_iff,imp_F]
-  \\ disch_then ACCEPT_TAC);
-
-val imp_antisym_ax = th21;
-
-val suc_11 = hd(amatch``Number_Natural_suc _ = Number_Natural_suc _``);
-
-(* |- !m n. Number_Natural_suc m = Number_Natural_suc n ==> m = n *)
-val th22 = store_thm
-  ("th22", el 22 goals |> concl,
-  rpt gen_tac \\ MATCH_ACCEPT_TAC (#1 (EQ_IMP_RULE (SPEC_ALL suc_11))));
-
-val null_eq = hd(amatch``Data_List_null t <=> (_ = Data_List_nil)``);
-val last_cons = hd(amatch``Data_List_last (Data_List_cons h t) = COND _ _ _``);
-
-(* |- !h t.
-          Data_List_last (Data_List_cons h t) =
-          if t = Data_List_nil then h else Data_List_last t
+(* |- !t. (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\
+          (t /\ F <=> F) /\ (t /\ t <=> t)
  *)
 val th23 = store_thm
   ("th23", el 23 goals |> concl,
-  MATCH_ACCEPT_TAC(PURE_REWRITE_RULE[null_eq]last_cons));
-
-(* NOTE: The following 3 theorems are proved later under different names.
+  gen_tac
+  \\ conj_tac >- MATCH_ACCEPT_TAC T_and
+  \\ conj_tac >- MATCH_ACCEPT_TAC and_T
+  \\ conj_tac >- MATCH_ACCEPT_TAC F_and
+  \\ conj_tac >- MATCH_ACCEPT_TAC and_F
+  \\ MATCH_ACCEPT_TAC and_i);
 
-th24: |- !P f. RES_EXISTS_UNIQUE P f <=> (?x::P. f x) /\ !x y::P. f x /\ f y ==> x = y
-th25: |- !P f. RES_FORALL P f <=> !x. x IN P ==> f x
-th26: |- !P f. RES_EXISTS P f <=> ?x. x IN P /\ f x
+val AND_CLAUSES = th23;
 
+(* |- !t. ((T <=> t) <=> t) /\ ((t <=> T) <=> t) /\ ((F <=> t) <=> ~t) /\
+          ((t <=> F) <=> ~t)   (EQ_CLAUSES)
  *)
+val th24 = store_thm
+  ("th24", el 24 goals |> concl,
+  gen_tac
+  \\ conj_tac >- MATCH_ACCEPT_TAC T_iff
+  \\ conj_tac >- MATCH_ACCEPT_TAC iff_T
+  \\ conj_tac >- MATCH_ACCEPT_TAC F_iff
+  \\ MATCH_ACCEPT_TAC iff_F);
 
-(* |- !t1 t2. (t1 <=> t2) <=> (t1 ==> t2) /\ (t2 ==> t1) *)
-val th27 = store_thm
-  ("th27", el 27 goals |> concl,
-  rpt gen_tac
-  \\ Q.ISPEC_THEN`t1`FULL_STRUCT_CASES_TAC bool_cases
-  \\ PURE_REWRITE_TAC[T_iff,F_iff,T_imp,F_imp,imp_T,imp_F,and_T,T_and]
-  \\ REFL_TAC);
-
-val eq_imp_thm = th27;
-
-val ext = hd(amatch``(!x. f x = g x) <=> _``);
-
-(* |- !f g. f = g <=> !x. f x = g x *)
-val th28 = store_thm
-  ("th28", el 28 goals |> concl, MATCH_ACCEPT_TAC (GSYM ext));
-
-(* |- !A B. (A <=> B \/ A) <=> B ==> A *)
-val th29 = store_thm
-  ("th29", el 29 goals |> concl,
-  rpt gen_tac
-  \\ Q.ISPEC_THEN`A`FULL_STRUCT_CASES_TAC bool_cases
-  \\ PURE_REWRITE_TAC[T_iff,or_T,F_iff,or_F,imp_T,imp_F]
-  \\ REFL_TAC);
-
-val not_T = hd(amatch``~T``);
-
-(* |- !A B. A ==> B <=> ~A \/ B *)
-val IMP_DISJ_THM = store_thm
-  ("IMP_DISJ_THM", concl boolTheory.IMP_DISJ_THM,
-  rpt gen_tac
-  \\ qspec_then`A`FULL_STRUCT_CASES_TAC bool_cases
-  \\ PURE_REWRITE_TAC[T_imp,not_T,F_imp,not_F,F_or,T_or]
-  \\ REFL_TAC);
-
-(* |- !A B. A \/ B <=> ~A ==> B (DISJ_EQ_IMP) *)
-val th30 = save_thm
-  ("th30", (* this proof is from boolScript.sml *)
-  let
-    val lemma = not_not |> SPEC ``A:bool``
-  in
-    IMP_DISJ_THM
-    |> SPECL [``~A:bool``,``B:bool``]
-    |> SYM
-    |> CONV_RULE
-      ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV)
-         (fn tm => lemma))
-    |> GENL [``A:bool``,``B:bool``]
-  end);
-
-val _ = if concl th30 ~~ concl (el 30 goals) then ()
-        else raise ERR "th30" "assumptions changed";
-
-val cons_neq_nil = hd(amatch``Data_List_cons _ _ <> Data_List_nil``);
-
-(* |- !a1 a0. Data_List_nil <> Data_List_cons a0 a1 *)
-val th31 = store_thm
-  ("th31", el 31 goals |> concl, MATCH_ACCEPT_TAC (GSYM cons_neq_nil));
-
-val some_neq_none = hd(amatch``_ <> Data_Option_none``);
+val EQ_CLAUSES = th24;
 
 (* |- !t. (T ==> t <=> t) /\ (t ==> T <=> T) /\ (F ==> t <=> T) /\
           (t ==> t <=> T) /\ (t ==> F <=> ~t)
  *)
-val th32 = store_thm
-  ("th32", el 32 goals |> concl,
+val th25 = store_thm
+  ("th25", el 25 goals |> concl,
   gen_tac
   \\ conj_tac >- MATCH_ACCEPT_TAC T_imp
   \\ conj_tac >- MATCH_ACCEPT_TAC imp_T
@@ -566,13 +704,13 @@ val th32 = store_thm
   \\ conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL imp_i))
   \\ MATCH_ACCEPT_TAC imp_F);
 
-val IMP_CLAUSES = th32;
+val IMP_CLAUSES = th25;
 
 (* |- !t. (T \/ t <=> T) /\ (t \/ T <=> T) /\ (F \/ t <=> t) /\
           (t \/ F <=> t) /\ (t \/ t <=> t)
  *)
-val th33 = store_thm
-  ("th33", el 33 goals |> concl,
+val th26 = store_thm
+  ("th26", el 26 goals |> concl,
   gen_tac
   \\ conj_tac >- MATCH_ACCEPT_TAC T_or
   \\ conj_tac >- MATCH_ACCEPT_TAC or_T
@@ -580,55 +718,139 @@ val th33 = store_thm
   \\ conj_tac >- MATCH_ACCEPT_TAC or_F
   \\ MATCH_ACCEPT_TAC or_i);
 
-val OR_CLAUSES = th33;
+val OR_CLAUSES = th26;
 
-(* |- !t. (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\
-          (t /\ F <=> F) /\ (t /\ t <=> t)
+(* |- !t. t ==> F <=> (t <=> F) *)
+val th27 = store_thm
+  ("th27", el 27 goals |> concl,
+  PURE_REWRITE_TAC[imp_F, iff_F]
+  \\ gen_tac \\ REFL_TAC);
+
+(* |- !t. F ==> t *)
+val th28 = store_thm
+  ("th28", el 28 goals |> concl,
+  MATCH_ACCEPT_TAC(EQT_ELIM(SPEC_ALL F_imp)));
+
+(* |- !t. ~t ==> t ==> F (boolTheory.F_IMP) *)
+val th29 = store_thm
+  ("th29", el 29 goals |> concl,
+  imp_F |> SPEC_ALL |> EQ_IMP_RULE |> #2 |> MATCH_ACCEPT_TAC);
+
+(* |- !t. (t ==> F) ==> ~t *)
+val th30 = store_thm
+  ("th30", el 30 goals |> concl,
+  imp_F |> SPEC_ALL |> EQ_IMP_RULE |> #1 |> MATCH_ACCEPT_TAC);
+
+val app_if = hd (amatch ``f (if b then x else y) = if b then f x else f y``);
+
+(* |- !f b x y. f (if b then x else y) = if b then f x else f y *)
+val th31 = store_thm
+  ("th31", el 31 goals |> concl, MATCH_ACCEPT_TAC app_if);
+
+(* |- !f g M N. M = N /\ (!x. x = N ==> f x = g x) ==> LET f M = LET g N *)
+val th32 = store_thm (* was: LET_CONG *)
+  ("th32", el 32 goals |> concl,
+  rpt strip_tac
+  \\ VAR_EQ_TAC
+  \\ PURE_REWRITE_TAC[LET_DEF]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ first_x_assum match_mp_tac
+  \\ REFL_TAC);
+
+val ext = hd(amatch``(!x. f x = g x) <=> _``);
+
+(* |- !f g. f = g <=> !x. f x = g x *)
+val th33 = store_thm
+  ("th33", el 33 goals |> concl, MATCH_ACCEPT_TAC (GSYM ext));
+
+val o_def = hd(amatch``Function_o = _``);
+
+val sum_cases = hd(amatch``(?a. x = Data_Sum_left a) \/ _``);
+val sum_ind = hd(amatch``_ ==> !l:('a,'b) Data_Sum_sum. P l``);
+val sum_case_thms = amatch``Data_Sum_case_left_right f g (_ _) = _``;
+
+(* |- !f g. ?!h. Function_o h Data_Sum_left = f /\
+                 Function_o h Data_Sum_right = g
  *)
 val th34 = store_thm
   ("th34", el 34 goals |> concl,
-  gen_tac
-  \\ conj_tac >- MATCH_ACCEPT_TAC T_and
-  \\ conj_tac >- MATCH_ACCEPT_TAC and_T
-  \\ conj_tac >- MATCH_ACCEPT_TAC F_and
-  \\ conj_tac >- MATCH_ACCEPT_TAC and_F
-  \\ MATCH_ACCEPT_TAC and_i);
+  rpt gen_tac
+  \\ CONV_TAC(HO_REWR_CONV ex_unique_thm)
+  \\ PURE_REWRITE_TAC[o_def]
+  \\ PURE_REWRITE_TAC[GSYM fun_eq_thm]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ rpt strip_tac
+  >- ( qexists_tac`Data_Sum_case_left_right f g`
+    \\ PURE_REWRITE_TAC sum_case_thms
+    \\ PURE_REWRITE_TAC[fun_eq_thm]
+    \\ conj_tac \\ REFL_TAC )
+  \\ Q.ISPEC_THEN`x`FULL_STRUCT_CASES_TAC sum_cases
+  >- ( rpt(first_x_assum(qspec_then`a`SUBST_ALL_TAC))
+    \\ REFL_TAC)
+  \\ rpt(first_x_assum(qspec_then`b`SUBST_ALL_TAC))
+  \\ REFL_TAC);
 
-val AND_CLAUSES = th34;
+val forall_eq = hd(amatch``!x. (x = t) ==> _``);
+val forall_eq2 = hd(amatch``!x. (t = x) ==> _``);
 
-(* |- !t. ((T <=> t) <=> t) /\ ((t <=> T) <=> t) /\ ((F <=> t) <=> ~t) /\
-          ((t <=> F) <=> ~t)   (EQ_CLAUSES)
- *)
+val ex_def = hd(amatch``$? = _``);
+val select_ax = hd(amatch ``p t ==> p ($@ p)``);
+
+(* |- !P t. (!x. x = t ==> P x) ==> $? P *)
 val th35 = store_thm
   ("th35", el 35 goals |> concl,
-  gen_tac
-  \\ conj_tac >- MATCH_ACCEPT_TAC T_iff
-  \\ conj_tac >- MATCH_ACCEPT_TAC iff_T
-  \\ conj_tac >- MATCH_ACCEPT_TAC F_iff
-  \\ MATCH_ACCEPT_TAC iff_F);
-
-val EQ_CLAUSES = th35;
+  PURE_REWRITE_TAC[forall_eq,ex_def]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ MATCH_ACCEPT_TAC select_ax);
 
-val select_eq = hd(amatch``@y. y = x``)
+val and_all = hd(amatch``p /\ (!x. _) <=> !x. p /\ _``);
+val all_and = hd(amatch``(!x. _) /\ p <=> !x. _ /\ p``);
+val all_imp = hd(amatch``((!x. _) ==> _) <=> _``);
+val imp_all = hd(amatch``(_ ==> (!x. _)) <=> _``);
 
-(* |- !x. (@y. x = y) = x *)
+(* |- !P Q.
+          (Q ==> (!x. P x) <=> !x. Q ==> P x) /\
+          ((!x. P x) /\ Q <=> !x. P x /\ Q) /\
+          (Q /\ (!x. P x) <=> !x. Q /\ P x)
+ *)
 val th36 = store_thm
   ("th36", el 36 goals |> concl,
-  CONV_TAC(QUANT_CONV(LAND_CONV(RAND_CONV(ABS_CONV SYM_CONV))))
-  \\ MATCH_ACCEPT_TAC select_eq);
+  rpt gen_tac
+  \\ PURE_REWRITE_TAC[and_all,all_and,all_imp,imp_all]
+  \\ rpt conj_tac \\ REFL_TAC);
 
-(* |- !t. t ==> F <=> (t <=> F) *)
+val and_ex = hd(amatch``p /\ (?x. _) <=> ?x. p /\ _``);
+val ex_and = hd(amatch``(?x. _) /\ p <=> ?x. _ /\ p``);
+val ex_imp = hd(amatch``((?x. _) ==> _) <=> _``);
+
+(* |- !P Q.
+          ((?x. P x) ==> Q <=> !x. P x ==> Q) /\
+          ((?x. P x) /\ Q <=> ?x. P x /\ Q) /\
+          (Q /\ (?x. P x) <=> ?y. Q /\ P y)
+ *)
 val th37 = store_thm
   ("th37", el 37 goals |> concl,
-  PURE_REWRITE_TAC[imp_F, iff_F]
-  \\ gen_tac \\ REFL_TAC);
+  rpt gen_tac
+  \\ PURE_REWRITE_TAC[and_ex,ex_and,ex_imp]
+  \\ rpt conj_tac \\ REFL_TAC);
 
-val refl = hd(amatch``!x. x = x``);
+(* NOTE: The following 3 theorems/goals will be proved later under different names.
+th38: |- !P f. RES_EXISTS P f <=> ?x. x IN P /\ f x
+th39: |- !P f. RES_EXISTS_UNIQUE P f <=> (?x::P. f x) /\ !x y::P. f x /\ f y ==> x = y
+th40: |- !P f. RES_FORALL P f <=> !x. x IN P ==> f x
+ *)
 
-(* |- !x. x = x <=> T *)
-val th38 = store_thm
-  ("th38", el 38 goals |> concl,
-  gen_tac \\ MATCH_ACCEPT_TAC(EQT_INTRO(SPEC_ALL refl)));
+val eta_ax = hd(amatch``!f. (\x. f x) = f``);
+
+(* |- !P Q. (?x. P x) /\ (!x. P x ==> Q x) ==> Q ($@ P) *)
+val th41 = store_thm
+  ("th41", el 41 goals |> concl,
+  PURE_REWRITE_TAC[ex_def]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ rpt strip_tac
+  \\ first_x_assum match_mp_tac
+  \\ CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV (GSYM eta_ax))))
+  \\ first_x_assum ACCEPT_TAC);
 
 val eq_trans = hd(amatch``(x = y) /\ (y = z) ==> _``);
 
@@ -637,247 +859,190 @@ val eq_trans = hd(amatch``(x = y) /\ (y = z) ==> _``);
           (!x y. f x y = f y x) ==>
           !x y z. f x (f y z) = f y (f x z)
  *)
-val th39 = store_thm
-  ("th39", el 39 goals |> concl,
+val th42 = store_thm
+  ("th42", el 42 goals |> concl,
   rpt strip_tac
-  \\ first_assum(qspecl_then[`x`,`y`,`z`]SUBST_ALL_TAC)
-  \\ last_assum(qspecl_then[`f x y`,`z`]SUBST_ALL_TAC)
-  \\ first_assum(qspecl_then[`z`,`x`,`y`]SUBST_ALL_TAC)
-  \\ last_assum(qspecl_then[`f z x`,`y`]SUBST_ALL_TAC)
+  \\ first_assum(qspecl_then[`x`,`y`,`z`] SUBST_ALL_TAC)
+  \\ last_assum(qspecl_then[`f x y`,`z`] SUBST_ALL_TAC)
+  \\ first_assum(qspecl_then[`z`,`x`,`y`] SUBST_ALL_TAC)
+  \\ last_assum(qspecl_then[`f z x`,`y`] SUBST_ALL_TAC)
   \\ AP_TERM_TAC
-  \\ last_assum(qspecl_then[`z`,`x`]ACCEPT_TAC));
+  \\ last_assum(qspecl_then[`z`,`x`] ACCEPT_TAC));
 
-val less_zero = hd(amatch``Number_Natural_less Number_Natural_zero n <=> _ <> _``);
-val div_mod = hd(amatch``Number_Natural_times (Number_Natural_div k n) n``);
-val less_mod = hd(amatch``Number_Natural_less (Number_Natural_mod _ _)``);
+val list_ind = hd(amatch``_ ==> !(l:'a Data_List_list). P l``);
 
-(* |- !n.
-          Number_Natural_less Number_Natural_zero n ==>
-          !k. k =
-              Number_Natural_plus
-                (Number_Natural_times (Number_Natural_div k n) n)
-                (Number_Natural_mod k n) /\
-              Number_Natural_less (Number_Natural_mod k n) n
+(* |- !P. P Data_List_nil /\ (!t. P t ==> !h. P (Data_List_cons h t)) ==>
+          !l. P l
  *)
-val th40 = store_thm
-  ("th40", el 40 goals |> concl,
-  PURE_REWRITE_TAC[less_zero]
-  \\ gen_tac
-  \\ disch_then(fn th => (strip_assume_tac (MATCH_MP less_mod th) >>
-       (strip_assume_tac (MATCH_MP div_mod th))))
-  \\ gen_tac
-  \\ first_x_assum(qspec_then`k`SUBST_ALL_TAC)
-  \\ conj_tac >- REFL_TAC
-  \\ first_x_assum(qspec_then`k`ACCEPT_TAC));
-
-val list_ind = hd(amatch``_ ==> !(l:'a Data_List_list). P l``);
-
-(* |- !P. P Data_List_nil /\ (!t. P t ==> !h. P (Data_List_cons h t)) ==>
-          !l. P l
- *)
-val th41 = store_thm
-  ("th41", el 41 goals |> concl,
+val th43 = store_thm
+  ("th43", el 43 goals |> concl,
   rpt strip_tac
   \\ match_mp_tac list_ind
   \\ conj_tac >- first_assum ACCEPT_TAC
   \\ rpt strip_tac \\ res_tac
   \\ first_assum MATCH_ACCEPT_TAC);
 
-(* |- !t. (t ==> F) ==> ~t *)
-val th42 = store_thm
-  ("th42", el 42 goals |> concl,
-  imp_F |> SPEC_ALL |> EQ_IMP_RULE |> #1 |> MATCH_ACCEPT_TAC);
-
-(* |- !t. ~t ==> t ==> F (boolTheory.F_IMP) *)
-val th43 = store_thm
-  ("th43", el 43 goals |> concl,
-  imp_F |> SPEC_ALL |> EQ_IMP_RULE |> #2 |> MATCH_ACCEPT_TAC);
-
-(* |- !t. F ==> t *)
+(* |- ~(t /\ ~t) *)
 val th44 = store_thm
   ("th44", el 44 goals |> concl,
-  MATCH_ACCEPT_TAC(EQT_ELIM(SPEC_ALL F_imp)));
+  PURE_REWRITE_TAC[not_and,not_not]
+  \\ Q.SPEC_THEN`t`FULL_STRUCT_CASES_TAC bool_cases
+  \\ PURE_REWRITE_TAC[or_T,or_F,not_F]);
 
-(* |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x'. Q x' *)
+val left_11 = hd(amatch``Data_Sum_left _ = Data_Sum_left _``);
+val right_11 = hd(amatch``Data_Sum_right _ = Data_Sum_right _``);
+
+(* |- (!x x'. Data_Sum_left x = Data_Sum_left x' <=> x = x') /\
+      !y y'. Data_Sum_right y = Data_Sum_right y' <=> y = y'
+ *)
 val th45 = store_thm
   ("th45", el 45 goals |> concl,
-  rpt strip_tac
-  \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
-  \\ qexists_tac`x`
-  \\ first_assum ACCEPT_TAC);
+    conj_tac
+ >| [ MATCH_ACCEPT_TAC left_11,
+      MATCH_ACCEPT_TAC right_11 ]);
 
-(* |- (!x. P x ==> Q x) ==> (!x. P x) ==> !x. Q x
-val th43 = store_thm
-  ("th43", el 46 goals |> concl,
-  rpt strip_tac
-  \\ first_x_assum match_mp_tac
-  \\ first_x_assum(qspec_then`x`ACCEPT_TAC));
- *)
+val isNone_some = hd(amatch``Data_Option_isNone (Data_Option_some _)``);
+val isNone_none = hd(amatch``Data_Option_isNone (Data_Option_none)``);
 
-(* |- (x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w *)
+(* |- (!x. Data_Option_isNone (Data_Option_some x) <=> F) /\
+      (Data_Option_isNone Data_Option_none <=> T)
+ *)
 val th46 = store_thm
   ("th46", el 46 goals |> concl,
-  rpt strip_tac
-  \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
-  \\ TRY (disj1_tac >> first_assum ACCEPT_TAC)
-  \\ TRY (disj2_tac >> first_assum ACCEPT_TAC));
+    conj_tac
+ >| [ MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL isNone_some)),
+      MATCH_ACCEPT_TAC (EQT_INTRO isNone_none) ]);
 
-(* |- (x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w *)
+val isSome_some = hd(amatch``Data_Option_isSome (Data_Option_some _)``);
+val isSome_none = hd(amatch``Data_Option_isSome (Data_Option_none)``);
+
+(* |- (!x. Data_Option_isSome (Data_Option_some x) <=> T) /\
+      (Data_Option_isSome Data_Option_none <=> F)
+ *)
 val th47 = store_thm
   ("th47", el 47 goals |> concl,
-   rpt strip_tac
-  \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
-  \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
-  \\ first_assum ACCEPT_TAC);
+    conj_tac
+ >| [ MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL isSome_some)),
+      MATCH_ACCEPT_TAC (EQF_INTRO isSome_none) ]);
 
-val unpair = hd(amatch``Data_Pair_comma (Data_Pair_fst _) _``);
-val unzip_nil = hd(amatch``Data_List_unzip Data_List_nil``);
-val unzip_cons = hd(amatch``Data_List_unzip (Data_List_cons _ _)``);
+val isLeft_right = hd(amatch``Data_Sum_isLeft (Data_Sum_right _)``);
+val isLeft_left = hd(amatch``Data_Sum_isLeft (Data_Sum_left _)``);
 
-(* |- Data_List_unzip Data_List_nil =
-      Data_Pair_comma Data_List_nil Data_List_nil /\
-      !x l.
-          Data_List_unzip (Data_List_cons x l) =
-          Data_Pair_comma
-            (Data_List_cons (Data_Pair_fst x)
-               (Data_Pair_fst (Data_List_unzip l)))
-            (Data_List_cons (Data_Pair_snd x)
-               (Data_Pair_snd (Data_List_unzip l)))
+(* |- (!x. Data_Sum_isLeft (Data_Sum_left x) <=> T) /\
+      !y. Data_Sum_isLeft (Data_Sum_right y) <=> F
  *)
 val th48 = store_thm
   ("th48", el 48 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC unzip_nil
-  \\ PURE_REWRITE_TAC[unzip_cons]
-  \\ rpt gen_tac
-  \\ conj_tac
-  \\ MATCH_ACCEPT_TAC(GSYM unpair));
+    conj_tac
+ >| [ PURE_REWRITE_TAC [iff_T] >> MATCH_ACCEPT_TAC isLeft_left,
+      PURE_REWRITE_TAC [iff_F] >> MATCH_ACCEPT_TAC isLeft_right ]);
 
-val reverse_nil = hd(amatch``Data_List_reverse Data_List_nil``);
-val reverse_cons = hd(amatch``Data_List_reverse (Data_List_cons _ _)``);
+val isRight_right = hd(amatch``Data_Sum_isRight (Data_Sum_right _)``);
+val isRight_left = hd(amatch``Data_Sum_isRight (Data_Sum_left _)``);
 
-(* |- Data_List_reverse Data_List_nil = Data_List_nil /\
-      !h t.
-          Data_List_reverse (Data_List_cons h t) =
-          Data_List_append (Data_List_reverse t)
-            (Data_List_cons h Data_List_nil)
+(* |- (!x. Data_Sum_isRight (Data_Sum_right x)) /\
+      !y. ~Data_Sum_isRight (Data_Sum_left y)
  *)
 val th49 = store_thm
   ("th49", el 49 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC reverse_nil
-  \\ MATCH_ACCEPT_TAC reverse_cons);
+    conj_tac
+ >| [ PURE_REWRITE_TAC [iff_T] >> MATCH_ACCEPT_TAC isRight_right,
+      PURE_REWRITE_TAC [iff_F] >> MATCH_ACCEPT_TAC isRight_left ]);
 
-val concat_nil = hd(amatch``Data_List_concat Data_List_nil``);
-val concat_cons = hd(amatch``Data_List_concat (Data_List_cons _ _)``);
+val append_nil = hd(amatch``Data_List_append Data_List_nil``);
+val append_cons =
+    hd(amatch ``Data_List_append (Data_List_cons _ _) _ =
+                Data_List_cons _ (_ _ _)``);
 
-(* |- Data_List_concat Data_List_nil = Data_List_nil /\
-      !h t.
-          Data_List_concat (Data_List_cons h t) =
-          Data_List_append h (Data_List_concat t)
+(* |- (!l. Data_List_append Data_List_nil l = l) /\
+      !h l1 l2.
+          Data_List_append (Data_List_cons h l1) l2 =
+          Data_List_cons h (Data_List_append l1 l2)
  *)
 val th50 = store_thm
   ("th50", el 50 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC concat_nil
-  \\ MATCH_ACCEPT_TAC concat_cons);
+  conj_tac >- MATCH_ACCEPT_TAC append_nil
+  \\ MATCH_ACCEPT_TAC append_cons);
 
-val fact_zero = hd(amatch``Number_Natural_factorial Number_Natural_zero``);
-val fact_suc = hd(amatch``Number_Natural_factorial (Number_Natural_suc _)``);
+val plus_zero = hd(amatch``Number_Natural_plus _ Number_Natural_zero``);
+val plus_suc = hd(amatch``Number_Natural_plus _ (Number_Natural_suc _)``);
+val plus_comm = hd(amatch``Number_Natural_plus x y = Number_Natural_plus y x``);
 
-(* |- Number_Natural_factorial Number_Natural_zero =
-      Number_Natural_bit1 Number_Natural_zero /\
-      !n.
-          Number_Natural_factorial (Number_Natural_suc n) =
-          Number_Natural_times (Number_Natural_suc n)
-            (Number_Natural_factorial n)
+(* |- (!n. Number_Natural_plus Number_Natural_zero n = n) /\
+      !m n. Number_Natural_plus (Number_Natural_suc m) n =
+            Number_Natural_suc (Number_Natural_plus m n)
  *)
 val th51 = store_thm
   ("th51", el 51 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC fact_zero
-  \\ MATCH_ACCEPT_TAC fact_suc);
+  conj_tac >- MATCH_ACCEPT_TAC (PURE_ONCE_REWRITE_RULE[plus_comm]plus_zero)
+  \\ MATCH_ACCEPT_TAC (PURE_ONCE_REWRITE_RULE[plus_comm]plus_suc));
 
-val length_nil = hd(amatch``Data_List_length Data_List_nil``);
-val length_cons = hd(amatch``Data_List_length (Data_List_cons _ _)``);
+val power_zero = hd(amatch``Number_Natural_power _ Number_Natural_zero``);
+val power_suc = hd(amatch``Number_Natural_power _ (Number_Natural_suc _)``);
 
-(* |- Data_List_length Data_List_nil = Number_Natural_zero /\
-      !h t.
-          Data_List_length (Data_List_cons h t) =
-          Number_Natural_suc (Data_List_length t)
+(* |- (!m. Number_Natural_power m Number_Natural_zero =
+           Number_Natural_bit1 Number_Natural_zero) /\
+      !m n. Number_Natural_power m (Number_Natural_suc n) =
+            Number_Natural_times m (Number_Natural_power m n)
  *)
 val th52 = store_thm
   ("th52", el 52 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC length_nil
-  \\ MATCH_ACCEPT_TAC length_cons);
-
-fun EQT_ELIM th = EQ_MP (SYM th) truth;
-
-fun EQF_ELIM th =
-   let
-      val (lhs, rhs) = dest_eq (concl th)
-      val _ = assert Feq rhs
-   in
-      NOT_INTRO (DISCH lhs (EQ_MP th (ASSUME lhs)))
-   end;
+  conj_tac >- MATCH_ACCEPT_TAC power_zero
+  \\ MATCH_ACCEPT_TAC power_suc);
 
-val null_nil = hd(amatch``Data_List_null Data_List_nil``);
-val null_cons = hd(amatch``Data_List_null (Data_List_cons _ _)``);
+val times_comm = hd(amatch``Number_Natural_times x y = Number_Natural_times y x``);
+val times_zero = hd(amatch``Number_Natural_times _ Number_Natural_zero``);
+val times_suc = hd(amatch``Number_Natural_times _ (Number_Natural_suc _)``);
+val times_zero_comm = PURE_ONCE_REWRITE_RULE [times_comm] times_zero;
 
-(* |- (Data_List_null Data_List_nil <=> T) /\
-      !h t. Data_List_null (Data_List_cons h t) <=> F
+(* |- (!n. Number_Natural_times Number_Natural_zero n = Number_Natural_zero) /\
+      !m n.
+          Number_Natural_times (Number_Natural_suc m) n =
+          Number_Natural_plus (Number_Natural_times m n) n
  *)
 val th53 = store_thm
   ("th53", el 53 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO null_nil)
-  \\ MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL null_cons)));
-
-val odd_nil = hd(amatch``Number_Natural_odd Number_Natural_zero``);
-val odd_cons = hd(amatch``Number_Natural_odd (Number_Natural_suc _)``);
+  conj_tac >- MATCH_ACCEPT_TAC times_zero_comm
+  \\ MATCH_ACCEPT_TAC
+      (PURE_ONCE_REWRITE_RULE[plus_comm](PURE_ONCE_REWRITE_RULE[times_comm]times_suc)));
 
-(* |- (Number_Natural_odd Number_Natural_zero <=> F) /\
-      !n. Number_Natural_odd (Number_Natural_suc n) <=> ~Number_Natural_odd n
- *)
+(* |- (!t. ~~t <=> t) /\ (~T <=> F) /\ (~F <=> T) *)
 val th54 = store_thm
   ("th54", el 54 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO odd_nil)
-  \\ MATCH_ACCEPT_TAC odd_cons);
+  PURE_REWRITE_TAC[not_not,iff_F,iff_T,truth,not_F,and_T]
+  \\ gen_tac \\ REFL_TAC);
 
-val even_nil = hd(amatch``Number_Natural_even Number_Natural_zero``);
-val even_cons = hd(amatch``Number_Natural_even (Number_Natural_suc _)``);
+val NOT_CLAUSES = th54;
 
-(* |- (Number_Natural_even Number_Natural_zero <=> T) /\
-      !n. Number_Natural_even (Number_Natural_suc n) <=> ~Number_Natural_even n
+val map_none = hd(amatch``Data_Option_map _ Data_Option_none = _``)
+val map_some = hd(amatch``Data_Option_map _ (Data_Option_some _) = _``)
+
+(* |- (!f x. Data_Option_map f (Data_Option_some x) = Data_Option_some (f x)) /\
+      !f. Data_Option_map f Data_Option_none = Data_Option_none
  *)
 val th55 = store_thm
   ("th55", el 55 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO even_nil)
-  \\ MATCH_ACCEPT_TAC even_cons);
-
-val left_11 = hd(amatch``Data_Sum_left _ = Data_Sum_left _``);
-val right_11 = hd(amatch``Data_Sum_right _ = Data_Sum_right _``);
-
-(* NOTE:
+  conj_tac >- MATCH_ACCEPT_TAC map_some
+  \\ MATCH_ACCEPT_TAC map_none);
 
-th56 |- (!p m x. x IN p ==> RES_ABSTRACT p m x = m x) /\
-         !p m1 m2. (!x. x IN p ==> m1 x = m2 x) ==> RES_ABSTRACT p m1 = RES_ABSTRACT p m2
- *)
+val map_nil = hd(amatch``Data_List_map _ Data_List_nil``);
+val map_cons = hd(amatch``Data_List_map _ (Data_List_cons _ _)``);
 
-(* |- (!x x'. Data_Sum_left x = Data_Sum_left x' <=> x = x') /\
-      !y y'. Data_Sum_right y = Data_Sum_right y' <=> y = y'
+(* |- (!f. Data_List_map f Data_List_nil = Data_List_nil) /\
+      !f h t.
+          Data_List_map f (Data_List_cons h t) =
+          Data_List_cons (f h) (Data_List_map f t)
  *)
-val th57 = store_thm
-  ("th57", el 57 goals |> concl,
-    conj_tac
- >| [ MATCH_ACCEPT_TAC left_11,
-      MATCH_ACCEPT_TAC right_11 ]);
+val th56 = store_thm
+  ("th56", el 56 goals |> concl,
+  conj_tac >- MATCH_ACCEPT_TAC map_nil
+  \\ MATCH_ACCEPT_TAC map_cons);
 
-val map_none = hd(amatch``Data_Option_map _ Data_Option_none = _``)
-val map_some = hd(amatch``Data_Option_map _ (Data_Option_some _) = _``)
+(* NOTE: This theorem will be proved later under a different name.
 
-(* |- (!f x. Data_Option_map f (Data_Option_some x) = Data_Option_some (f x)) /\
-      !f. Data_Option_map f Data_Option_none = Data_Option_none
+th57 |- (!p m x. x IN p ==> RES_ABSTRACT p m x = m x) /\
+         !p m1 m2. (!x. x IN p ==> m1 x = m2 x) ==> RES_ABSTRACT p m1 = RES_ABSTRACT p m2
  *)
-val th58 = store_thm
-  ("th58", el 58 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC map_some
-  \\ MATCH_ACCEPT_TAC map_none);
 
 val filter_nil = hd(amatch``Data_List_filter _ Data_List_nil``);
 val filter_cons = hd(amatch``Data_List_filter _ (Data_List_cons _ _)``);
@@ -888,23 +1053,22 @@ val filter_cons = hd(amatch``Data_List_filter _ (Data_List_cons _ _)``);
           if P h then Data_List_cons h (Data_List_filter P t)
           else Data_List_filter P t
  *)
-val th59 = store_thm
-  ("th59", el 59 goals |> concl,
+val th58 = store_thm
+  ("th58", el 58 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC filter_nil
   \\ MATCH_ACCEPT_TAC filter_cons);
 
-val map_nil = hd(amatch``Data_List_map _ Data_List_nil``);
-val map_cons = hd(amatch``Data_List_map _ (Data_List_cons _ _)``);
+val all_nil = hd(amatch``Data_List_all _ Data_List_nil``);
+val all_cons = hd(amatch``Data_List_all _ (Data_List_cons _ _)``);
 
-(* |- (!f. Data_List_map f Data_List_nil = Data_List_nil) /\
-      !f h t.
-          Data_List_map f (Data_List_cons h t) =
-          Data_List_cons (f h) (Data_List_map f t)
+(* |- (!P. Data_List_all P Data_List_nil <=> T) /\
+      !P h t.
+          Data_List_all P (Data_List_cons h t) <=> P h /\ Data_List_all P t
  *)
-val th60 = store_thm
-  ("th60", el 60 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC map_nil
-  \\ MATCH_ACCEPT_TAC map_cons);
+val th59 = store_thm
+  ("th59", el 59 goals |> concl,
+  conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL all_nil))
+  \\ MATCH_ACCEPT_TAC all_cons);
 
 val any_nil = hd(amatch``Data_List_any _ Data_List_nil``);
 val any_cons = hd(amatch``Data_List_any _ (Data_List_cons _ _)``);
@@ -913,202 +1077,292 @@ val any_cons = hd(amatch``Data_List_any _ (Data_List_cons _ _)``);
       !P h t.
           Data_List_any P (Data_List_cons h t) <=> P h \/ Data_List_any P t
  *)
-val th61 = store_thm
-  ("th61", el 61 goals |> concl,
+val th60 = store_thm
+  ("th60", el 60 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL any_nil))
   \\ MATCH_ACCEPT_TAC any_cons);
 
-val all_nil = hd(amatch``Data_List_all _ Data_List_nil``);
-val all_cons = hd(amatch``Data_List_all _ (Data_List_cons _ _)``);
+val concat_nil = hd(amatch``Data_List_concat Data_List_nil``);
+val concat_cons = hd(amatch``Data_List_concat (Data_List_cons _ _)``);
 
-(* |- (!P. Data_List_all P Data_List_nil <=> T) /\
-      !P h t.
-          Data_List_all P (Data_List_cons h t) <=> P h /\ Data_List_all P t
+(* |- Data_List_concat Data_List_nil = Data_List_nil /\
+      !h t.
+          Data_List_concat (Data_List_cons h t) =
+          Data_List_append h (Data_List_concat t)
+ *)
+val th61 = store_thm
+  ("th61", el 61 goals |> concl,
+  conj_tac >- MATCH_ACCEPT_TAC concat_nil
+  \\ MATCH_ACCEPT_TAC concat_cons);
+
+val reverse_nil = hd(amatch``Data_List_reverse Data_List_nil``);
+val reverse_cons = hd(amatch``Data_List_reverse (Data_List_cons _ _)``);
+
+(* |- Data_List_reverse Data_List_nil = Data_List_nil /\
+      !h t.
+          Data_List_reverse (Data_List_cons h t) =
+          Data_List_append (Data_List_reverse t)
+            (Data_List_cons h Data_List_nil)
  *)
 val th62 = store_thm
   ("th62", el 62 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL all_nil))
-  \\ MATCH_ACCEPT_TAC all_cons);
+  conj_tac >- MATCH_ACCEPT_TAC reverse_nil
+  \\ MATCH_ACCEPT_TAC reverse_cons);
 
-val append_nil = hd(amatch``Data_List_append Data_List_nil``);
-val append_cons =
-    hd(amatch ``Data_List_append (Data_List_cons _ _) _ =
-                Data_List_cons _ (_ _ _)``);
+val unpair = hd(amatch``Data_Pair_comma (Data_Pair_fst _) _``);
+val unzip_nil = hd(amatch``Data_List_unzip Data_List_nil``);
+val unzip_cons = hd(amatch``Data_List_unzip (Data_List_cons _ _)``);
 
-(* |- (!l. Data_List_append Data_List_nil l = l) /\
-      !l1 l2 h.
-          Data_List_append (Data_List_cons h l1) l2 =
-          Data_List_cons h (Data_List_append l1 l2)
+(* |- Data_List_unzip Data_List_nil =
+      Data_Pair_comma Data_List_nil Data_List_nil /\
+      !x l.
+          Data_List_unzip (Data_List_cons x l) =
+          Data_Pair_comma
+            (Data_List_cons (Data_Pair_fst x)
+               (Data_Pair_fst (Data_List_unzip l)))
+            (Data_List_cons (Data_Pair_snd x)
+               (Data_Pair_snd (Data_List_unzip l)))
  *)
 val th63 = store_thm
   ("th63", el 63 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC append_nil
-  \\ MATCH_ACCEPT_TAC append_cons);
+  conj_tac >- MATCH_ACCEPT_TAC unzip_nil
+  \\ PURE_REWRITE_TAC[unzip_cons]
+  \\ rpt gen_tac
+  \\ conj_tac
+  \\ MATCH_ACCEPT_TAC(GSYM unpair));
 
-val power_zero = hd(amatch``Number_Natural_power _ Number_Natural_zero``);
-val power_suc = hd(amatch``Number_Natural_power _ (Number_Natural_suc _)``);
+val length_nil = hd(amatch``Data_List_length Data_List_nil``);
+val length_cons = hd(amatch``Data_List_length (Data_List_cons _ _)``);
 
-(* |- (!m.
-           Number_Natural_power m Number_Natural_zero =
-           Number_Natural_bit1 Number_Natural_zero) /\
-      !m n.
-          Number_Natural_power m (Number_Natural_suc n) =
-          Number_Natural_times m (Number_Natural_power m n)
+(* |- Data_List_length Data_List_nil = Number_Natural_zero /\
+      !h t.
+          Data_List_length (Data_List_cons h t) =
+          Number_Natural_suc (Data_List_length t)
  *)
 val th64 = store_thm
   ("th64", el 64 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC power_zero
-  \\ MATCH_ACCEPT_TAC power_suc);
+  conj_tac >- MATCH_ACCEPT_TAC length_nil
+  \\ MATCH_ACCEPT_TAC length_cons);
 
-val times_comm = hd(amatch``Number_Natural_times x y = Number_Natural_times y x``);
-val plus_comm = hd(amatch``Number_Natural_plus x y = Number_Natural_plus y x``);
-val times_zero = hd(amatch``Number_Natural_times _ Number_Natural_zero``);
-val times_suc = hd(amatch``Number_Natural_times _ (Number_Natural_suc _)``);
-val times_zero_comm = PURE_ONCE_REWRITE_RULE [times_comm] times_zero;
+val fact_zero = hd(amatch``Number_Natural_factorial Number_Natural_zero``);
+val fact_suc = hd(amatch``Number_Natural_factorial (Number_Natural_suc _)``);
 
-(* |- (!n. Number_Natural_times Number_Natural_zero n = Number_Natural_zero) /\
-      !m n.
-          Number_Natural_times (Number_Natural_suc m) n =
-          Number_Natural_plus (Number_Natural_times m n) n
+(* |- Number_Natural_factorial Number_Natural_zero =
+      Number_Natural_bit1 Number_Natural_zero /\
+      !n.
+          Number_Natural_factorial (Number_Natural_suc n) =
+          Number_Natural_times (Number_Natural_suc n)
+            (Number_Natural_factorial n)
  *)
 val th65 = store_thm
   ("th65", el 65 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC times_zero_comm
-  \\ MATCH_ACCEPT_TAC
-      (PURE_ONCE_REWRITE_RULE[plus_comm](PURE_ONCE_REWRITE_RULE[times_comm]times_suc)));
+  conj_tac >- MATCH_ACCEPT_TAC fact_zero
+  \\ MATCH_ACCEPT_TAC fact_suc);
 
-val plus_zero = hd(amatch``Number_Natural_plus _ Number_Natural_zero``);
-val plus_suc = hd(amatch``Number_Natural_plus _ (Number_Natural_suc _)``);
+val null_nil = hd(amatch``Data_List_null Data_List_nil``);
+val null_cons = hd(amatch``Data_List_null (Data_List_cons _ _)``);
 
-(* |- (!n. Number_Natural_plus Number_Natural_zero n = n) /\
-      !m n.
-          Number_Natural_plus (Number_Natural_suc m) n =
-          Number_Natural_suc (Number_Natural_plus m n)
+(* |- (Data_List_null Data_List_nil <=> T) /\
+      !h t. Data_List_null (Data_List_cons h t) <=> F
  *)
 val th66 = store_thm
   ("th66", el 66 goals |> concl,
-  conj_tac >- MATCH_ACCEPT_TAC (PURE_ONCE_REWRITE_RULE[plus_comm]plus_zero)
-  \\ MATCH_ACCEPT_TAC (PURE_ONCE_REWRITE_RULE[plus_comm]plus_suc));
+  conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO null_nil)
+  \\ MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL null_cons)));
 
-(* |- (!t. ~~t <=> t) /\ (~T <=> F) /\ (~F <=> T) *)
+val even_nil = hd(amatch``Number_Natural_even Number_Natural_zero``);
+val even_cons = hd(amatch``Number_Natural_even (Number_Natural_suc _)``);
+
+(* |- (Number_Natural_even Number_Natural_zero <=> T) /\
+      !n. Number_Natural_even (Number_Natural_suc n) <=> ~Number_Natural_even n
+ *)
 val th67 = store_thm
   ("th67", el 67 goals |> concl,
-  PURE_REWRITE_TAC[not_not,iff_F,iff_T,truth,not_F,and_T]
-  \\ gen_tac \\ REFL_TAC);
-
-val NOT_CLAUSES = th67;
+  conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO even_nil)
+  \\ MATCH_ACCEPT_TAC even_cons);
 
-val isRight_right = hd(amatch``Data_Sum_isRight (Data_Sum_right _)``);
-val isRight_left = hd(amatch``Data_Sum_isRight (Data_Sum_left _)``);
+val odd_nil = hd(amatch``Number_Natural_odd Number_Natural_zero``);
+val odd_cons = hd(amatch``Number_Natural_odd (Number_Natural_suc _)``);
 
-(* |- (!x. Data_Sum_isRight (Data_Sum_right x)) /\
-      !y. ~Data_Sum_isRight (Data_Sum_left y)
+(* |- (Number_Natural_odd Number_Natural_zero <=> F) /\
+      !n. Number_Natural_odd (Number_Natural_suc n) <=> ~Number_Natural_odd n
  *)
 val th68 = store_thm
   ("th68", el 68 goals |> concl,
-    conj_tac
- >| [ PURE_REWRITE_TAC [iff_T] >> MATCH_ACCEPT_TAC isRight_right,
-      PURE_REWRITE_TAC [iff_F] >> MATCH_ACCEPT_TAC isRight_left ]);
+  conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO odd_nil)
+  \\ MATCH_ACCEPT_TAC odd_cons);
 
-val isLeft_right = hd(amatch``Data_Sum_isLeft (Data_Sum_right _)``);
-val isLeft_left = hd(amatch``Data_Sum_isLeft (Data_Sum_left _)``);
+val one_thm = hd(amatch``_ = Data_Unit_unit``);
 
-(* |- (!x. Data_Sum_isLeft (Data_Sum_left x) <=> T) /\
-      !y. Data_Sum_isLeft (Data_Sum_right y) <=> F
- *)
+(* |- Data_Unit_unit = @x. T *)
 val th69 = store_thm
   ("th69", el 69 goals |> concl,
-    conj_tac
- >| [ PURE_REWRITE_TAC [iff_T] >> MATCH_ACCEPT_TAC isLeft_left,
-      PURE_REWRITE_TAC [iff_F] >> MATCH_ACCEPT_TAC isLeft_right ]);
-
-val isSome_some = hd(amatch``Data_Option_isSome (Data_Option_some _)``);
-val isSome_none = hd(amatch``Data_Option_isSome (Data_Option_none)``);
+  PURE_ONCE_REWRITE_TAC[one_thm] \\ REFL_TAC);
 
-(* |- (!x. Data_Option_isSome (Data_Option_some x) <=> T) /\
-      (Data_Option_isSome Data_Option_none <=> F)
- *)
+(* |- Number_Natural_zero = Number_Natural_zero *)
 val th70 = store_thm
   ("th70", el 70 goals |> concl,
-    conj_tac
- >| [ MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL isSome_some)),
-      MATCH_ACCEPT_TAC (EQF_INTRO isSome_none) ]);
+  REFL_TAC);
 
-val isNone_some = hd(amatch``Data_Option_isNone (Data_Option_some _)``);
-val isNone_none = hd(amatch``Data_Option_isNone (Data_Option_none)``);
+val exists_simp = hd(amatch “(?x. t) <=> t”);
 
-(* |- (!x. Data_Option_isNone (Data_Option_some x) <=> F) /\
-      (Data_Option_isNone Data_Option_none <=> T)
- *)
+(* |- (?!x. F) <=> F *)
 val th71 = store_thm
   ("th71", el 71 goals |> concl,
-    conj_tac
- >| [ MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL isNone_some)),
-      MATCH_ACCEPT_TAC (EQT_INTRO isNone_none) ]);
+  PURE_REWRITE_TAC [BETA_RULE (SPEC “\x:'a. F” ex_unique_thm)] \\
+  PURE_REWRITE_TAC [SPEC “F” exists_simp, F_and] \\
+  REFL_TAC);
 
-val tc_def           = hd(amatch``!x. Relation_transitiveClosure x = _``);
-val bigIntersect_thm = hd(amatch``Relation_bigIntersect a b c <=> _``);
-val mem_fromPred     = hd(amatch``Set_member r (Set_fromPredicate _)``);
-val subrelation_thm  = hd(amatch``Relation_subrelation x s <=> !x y. _``);
-val transitive_thm   = hd(amatch``Relation_transitive s <=> _``);
+val comma_11 = hd(amatch``Data_Pair_comma _ _ = Data_Pair_comma _ _``);
 
-(* |- Relation_transitiveClosure =
-      (\R a b.
-           !P. (!x y. R x y ==> P x y) /\ (!x y z. P x y /\ P y z ==> P x z) ==>
-               P a b)
- *)
+(* |- Data_Pair_comma x y = Data_Pair_comma a b <=> x = a /\ y = b *)
 val th72 = store_thm
   ("th72", el 72 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm]
-  \\ PURE_REWRITE_TAC[tc_def,bigIntersect_thm,mem_fromPred]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ Ho_Rewrite.PURE_REWRITE_TAC[ex_imp]
-  \\ PURE_REWRITE_TAC[subrelation_thm,transitive_thm]
-  \\ PURE_ONCE_REWRITE_TAC[GSYM and_imp_intro]
-  \\ Ho_Rewrite.PURE_REWRITE_TAC[forall_eq2]
-  \\ rpt gen_tac
-  \\ PURE_REWRITE_TAC[GSYM and_imp_intro]
-  \\ REFL_TAC);
-
-val wellFounded_thm = hd(amatch``Relation_wellFounded r <=> !p. (?x. _) ==> _``);
+  MATCH_ACCEPT_TAC comma_11);
 
-(* |- Relation_wellFounded =
-      (\R. !B. (?w. B w) ==> ?min. B min /\ !b. R b min ==> ~B b)
- *)
+(* |- Data_Sum_left x = Data_Sum_left y <=> x = y *)
 val th73 = store_thm
   ("th73", el 73 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm]
-  \\ PURE_REWRITE_TAC[wellFounded_thm]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ gen_tac \\ REFL_TAC);
+  MATCH_ACCEPT_TAC left_11);
 
-(* |- !A. A ==> ~A ==> F *)
-val F_IMP2 = store_thm
-  ("F_IMP2", “!A. A ==> ~A ==> F”,
-  PURE_REWRITE_TAC[GSYM imp_F]
-  \\ gen_tac
-  \\ disch_then(fn th => disch_then(ACCEPT_TAC o C MP th)));
+(* |- Data_Sum_right x = Data_Sum_right y <=> x = y *)
+val th74 = store_thm
+  ("th74", el 74 goals |> concl,
+  MATCH_ACCEPT_TAC right_11);
+
+val skk = hd(amatch``Function_Combinator_s _ _ = Function_id``);
+
+(* |- Function_id = Function_Combinator_s Function_const Function_const *)
+val th75 = store_thm
+  ("th75", el 75 goals |> concl,
+  PURE_REWRITE_TAC[skk] \\ REFL_TAC);
+
+val empty_thm = hd(amatch``Relation_empty _ _``);
+
+(* |- Relation_empty = (\x y. F) *)
+val th76 = store_thm
+  ("th76", el 76 goals |> concl,
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,EQF_INTRO (SPEC_ALL empty_thm)]
+  \\ CONV_TAC (DEPTH_CONV BETA_CONV)
+  \\ rpt gen_tac \\ REFL_TAC);
+
+val universe_thm = hd(amatch``Relation_universe _ _``);
+
+(* |- Relation_universe = (\x y. T) *)
+val th77 = store_thm
+  ("th77", el 77 goals |> concl,
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,EQT_INTRO(SPEC_ALL universe_thm)]
+  \\ CONV_TAC (DEPTH_CONV BETA_CONV)
+  \\ rpt gen_tac \\ REFL_TAC);
+
+val bit1_thm = hd(amatch``Number_Natural_bit1 _ = _``);
+val bit0_suc = hd(amatch``Number_Natural_bit0 _ = _ _``);
+val bit0_zero = hd(amatch``Number_Natural_bit0 Number_Natural_zero``);
+val plus_zero = hd(amatch``Number_Natural_plus Number_Natural_zero _``);
+val plus_suc = hd(amatch``Number_Natural_plus _ (Number_Natural_suc _)``);
+val plus_suc1 = hd(amatch``Number_Natural_plus (Number_Natural_suc _) _``);
 
-val less_thm     = hd(amatch``Number_Natural_less _ _ <=> ?x. _``);
-val less_refl    = hd(amatch``Number_Natural_less x x``);
-val less_zero    = hd(amatch``~(Number_Natural_less _ (Number_Natural_zero))``);
-val less_suc_suc = hd(amatch``Number_Natural_less (Number_Natural_suc _) b``);
-val less_suc     = hd(amatch``Number_Natural_less n (Number_Natural_suc n)``);
-val less_trans   = hd(amatch``Number_Natural_less x y /\ Number_Natural_less y z ==> _``);
 val num_cases    = hd(amatch``(n = Number_Natural_zero) \/ ?n. _``);
 val num_ind      = hd(amatch``_ ==> !n. P (n:Number_Natural_natural)``);
 val num_less_ind = hd(amatch``(!x. _ ==> _) ==> !n. P (n:Number_Natural_natural)``);
+
+(* |- Number_Natural_bit1 =
+      (\n.
+           Number_Natural_plus n
+             (Number_Natural_plus n (Number_Natural_suc Number_Natural_zero)))
+ *)
+val th78 = store_thm
+  ("th78", el 78 goals |> concl,
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,bit1_thm,plus_suc]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ gen_tac
+  \\ AP_TERM_TAC
+  \\ qid_spec_tac`x`
+  \\ ho_match_mp_tac num_ind
+  \\ PURE_REWRITE_TAC[bit0_zero,bit0_suc,plus_zero,plus_suc1]
+  \\ conj_tac >- REFL_TAC
+  \\ gen_tac
+  \\ disch_then SUBST_ALL_TAC
+  \\ PURE_REWRITE_TAC[plus_suc]
+  \\ REFL_TAC);
+
+val max_thm = hd(amatch``Number_Natural_max _ _ = COND _ _ _``);
+val if_id   = hd(amatch``if _ then x else x``);
+val less_or_eq   = hd(amatch``Number_Natural_lesseq _ _ <=> (Number_Natural_less _ _) \/ _``);
+
+(* |- Number_Natural_max = (\m n. if Number_Natural_less m n then n else m) *)
+val th79 = store_thm
+  ("th79", el 79 goals |> concl,
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,max_thm,less_or_eq]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ rpt gen_tac
+  \\ qspec_then`x = x'`strip_assume_tac bool_cases
+  \\ first_assum SUBST1_TAC
+  \\ PURE_REWRITE_TAC[or_F,or_T,if_T]
+  \\ TRY REFL_TAC
+  \\ pop_assum(SUBST1_TAC o EQT_ELIM)
+  \\ PURE_REWRITE_TAC[if_id]
+  \\ REFL_TAC);
+
+val min_thm = hd(amatch``Number_Natural_min _ _ = COND _ _ _``);
+
+(* |- Number_Natural_min = (\m n. if Number_Natural_less m n then m else n) *)
+val th80 = store_thm
+  ("th80", el 80 goals |> concl,
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,min_thm,less_or_eq]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ rpt gen_tac
+  \\ qspec_then`x = x'`strip_assume_tac bool_cases
+  \\ first_assum SUBST1_TAC
+  \\ PURE_REWRITE_TAC[or_F,or_T,if_T]
+  \\ TRY REFL_TAC
+  \\ pop_assum(SUBST1_TAC o EQT_ELIM)
+  \\ PURE_REWRITE_TAC[if_id]
+  \\ REFL_TAC);
+
+val greater_thm   = hd(amatch``Number_Natural_greater _ _ = _``);
+
+(* |- Number_Natural_greater = (\m n. Number_Natural_less n m) *)
+val th81 = store_thm
+  ("th81", el 81 goals |> concl,
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,greater_thm]
+  \\ CONV_TAC (DEPTH_CONV BETA_CONV)
+  \\ rpt gen_tac \\ REFL_TAC);
+
+val greatereq_thm = hd(amatch``Number_Natural_greatereq _ _``);
+
+(* |- Number_Natural_greatereq = (\m n. Number_Natural_greater m n \/ m = n) *)
+val th82 = store_thm
+  ("th82", el 82 goals |> concl,
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,greatereq_thm,less_or_eq,greater_thm]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ rpt gen_tac
+  \\ CONV_TAC(RAND_CONV(ONCE_DEPTH_CONV SYM_CONV))
+  \\ REFL_TAC);
+
+val less_thm     = hd(amatch``Number_Natural_less _ _ <=> ?x. _``);
+val less_refl    = hd(amatch``Number_Natural_less x x``);
+val less_zero    = hd(amatch``~(Number_Natural_less _ (Number_Natural_zero))``);
+val less_suc_suc = hd(amatch``Number_Natural_less (Number_Natural_suc _) b``);
+val less_suc     = hd(amatch``Number_Natural_less n (Number_Natural_suc n)``);
+val less_trans   = hd(amatch``Number_Natural_less x y /\ Number_Natural_less y z ==> _``);
 val not_less     = hd(amatch``~(Number_Natural_less _ _) <=> _``);
 val less_lesseq  = hd(amatch``Number_Natural_less m (Number_Natural_suc n) <=>
                               Number_Natural_lesseq m n``);
-val less_or_eq   = hd(amatch``Number_Natural_lesseq _ _ <=> (Number_Natural_less _ _) \/ _``);
 val trichotomy   = hd(amatch``_ \/ _ \/ (_ = _)``);
 
+(* |- !A. A ==> ~A ==> F *)
+val F_IMP2 = store_thm
+  ("F_IMP2", “!A. A ==> ~A ==> F”,
+  PURE_REWRITE_TAC[GSYM imp_F]
+  \\ gen_tac
+  \\ disch_then(fn th => disch_then(ACCEPT_TAC o C MP th)));
+
 (* |- Number_Natural_less =
       (\m n. ?P. (!n. P (Number_Natural_suc n) ==> P n) /\ P m /\ ~P n)
  *)
-val th74 = store_thm
-  ("th74", el 74 goals |> concl,
+val th83 = store_thm
+  ("th83", el 83 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm]
   \\ qx_genl_tac[`a`,`b`]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
@@ -1143,8 +1397,10 @@ val th74 = store_thm
       \\ ntac 2 strip_tac
       \\ CONV_TAC(REWR_CONV F_imp))
     \\ rpt strip_tac
-    \\ `P a` by (first_x_assum(fn th => (first_x_assum match_mp_tac \\ first_assum ACCEPT_TAC)))
-    \\ `!n. Number_Natural_less n a ==> P n` by (first_x_assum match_mp_tac \\ first_assum ACCEPT_TAC)
+    \\ `P a` by (first_x_assum(fn th => (first_x_assum match_mp_tac \\
+                                         first_assum ACCEPT_TAC)))
+    \\ `!n. Number_Natural_less n a ==> P n`
+           by (first_x_assum match_mp_tac \\ first_assum ACCEPT_TAC)
     \\ first_x_assum(assume_tac o CONV_RULE(REWR_CONV less_lesseq))
     \\ first_x_assum(strip_assume_tac o CONV_RULE(REWR_CONV less_or_eq))
     >- (
@@ -1164,126 +1420,18 @@ val th74 = store_thm
   \\ first_x_assum(fn th => (first_x_assum(mp_tac o EQ_MP th)))
   \\ PURE_REWRITE_TAC[F_imp]);
 
-(* |- Relation_transitive = (\R. !x y z. R x y /\ R y z ==> R x z) *)
-val th75 = store_thm
-  ("th75", el 75 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,transitive_thm]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ gen_tac \\ REFL_TAC);
-
-(* |- Relation_subrelation = (\R1 R2. !x y. R1 x y ==> R2 x y) *)
-val th76 = store_thm
-  ("th76", el 76 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,subrelation_thm]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ rpt gen_tac \\ REFL_TAC);
-
-val union_thm = hd(amatch``Relation_union r s = _``);
-val fromSet_thm = hd(amatch``Relation_fromSet _ _ _``);
-val mem_union = hd(amatch``Set_member _ (Set_union _ _) <=> _``);
-val mem_toSet = hd(amatch``Set_member _ (Relation_toSet _)``);
-
-(* |- Relation_union = (\R1 R2 x y. R1 x y \/ R2 x y) *)
-val th77 = store_thm
-  ("th77", el 77 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,union_thm,fromSet_thm,mem_union,mem_toSet]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ rpt gen_tac \\ REFL_TAC);
-
-val intersect_thm = hd(amatch``Relation_intersect x y = _``);
-val mem_inter     = hd(amatch``Set_member _ (Set_intersect _ _)``);
-
-(* |- Relation_intersect = (\R1 R2 x y. R1 x y /\ R2 x y) *)
-val th78 = store_thm
-  ("th78", el 78 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,intersect_thm,fromSet_thm,mem_inter,mem_toSet]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ rpt gen_tac \\ REFL_TAC);
-
-val greatereq_thm = hd(amatch``Number_Natural_greatereq _ _``);
-val greater_thm   = hd(amatch``Number_Natural_greater _ _ = _``);
-
-(* |- Number_Natural_greatereq = (\m n. Number_Natural_greater m n \/ m = n) *)
-val th79 = store_thm
-  ("th79", el 79 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,greatereq_thm,less_or_eq,greater_thm]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ rpt gen_tac
-  \\ CONV_TAC(RAND_CONV(ONCE_DEPTH_CONV SYM_CONV))
-  \\ REFL_TAC);
-
 (* |- Number_Natural_lesseq = (\m n. Number_Natural_less m n \/ m = n) *)
-val th80 = store_thm
-  ("th80", el 80 goals |> concl,
+val th84 = store_thm
+  ("th84", el 84 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,less_or_eq]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
 
-val min_thm = hd(amatch``Number_Natural_min _ _ = COND _ _ _``);
-val if_id   = hd(amatch``if _ then x else x``);
-
-(* |- Number_Natural_min = (\m n. if Number_Natural_less m n then m else n) *)
-val th81 = store_thm
-  ("th81", el 81 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,min_thm,less_or_eq]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ rpt gen_tac
-  \\ qspec_then`x = x'`strip_assume_tac bool_cases
-  \\ first_assum SUBST1_TAC
-  \\ PURE_REWRITE_TAC[or_F,or_T,if_T]
-  \\ TRY REFL_TAC
-  \\ pop_assum(SUBST1_TAC o EQT_ELIM)
-  \\ PURE_REWRITE_TAC[if_id]
-  \\ REFL_TAC);
-
-val max_thm = hd(amatch``Number_Natural_max _ _ = COND _ _ _``);
-
-(* |- Number_Natural_max = (\m n. if Number_Natural_less m n then n else m) *)
-val th82 = store_thm
-  ("th82", el 82 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,max_thm,less_or_eq]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ rpt gen_tac
-  \\ qspec_then`x = x'`strip_assume_tac bool_cases
-  \\ first_assum SUBST1_TAC
-  \\ PURE_REWRITE_TAC[or_F,or_T,if_T]
-  \\ TRY REFL_TAC
-  \\ pop_assum(SUBST1_TAC o EQT_ELIM)
-  \\ PURE_REWRITE_TAC[if_id]
-  \\ REFL_TAC);
-
-val bit1_thm = hd(amatch``Number_Natural_bit1 _ = _``);
-val bit0_suc = hd(amatch``Number_Natural_bit0 _ = _ _``);
-val bit0_zero = hd(amatch``Number_Natural_bit0 Number_Natural_zero``);
-val plus_zero = hd(amatch``Number_Natural_plus Number_Natural_zero _``);
-val plus_suc = hd(amatch``Number_Natural_plus _ (Number_Natural_suc _)``);
-val plus_suc1 = hd(amatch``Number_Natural_plus (Number_Natural_suc _) _``);
-
-(* |- Number_Natural_bit1 =
-      (\n.
-           Number_Natural_plus n
-             (Number_Natural_plus n (Number_Natural_suc Number_Natural_zero)))
- *)
-val th83 = store_thm
-  ("th83", el 83 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,bit1_thm,plus_suc]
-  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
-  \\ gen_tac
-  \\ AP_TERM_TAC
-  \\ qid_spec_tac`x`
-  \\ ho_match_mp_tac num_ind
-  \\ PURE_REWRITE_TAC[bit0_zero,bit0_suc,plus_zero,plus_suc1]
-  \\ conj_tac >- REFL_TAC
-  \\ gen_tac
-  \\ disch_then SUBST_ALL_TAC
-  \\ PURE_REWRITE_TAC[plus_suc]
-  \\ REFL_TAC);
-
 val irreflexive_thm = hd(amatch``Relation_irreflexive _ = _``);
 
 (* |- Relation_irreflexive = (\R. !x. ~R x x) *)
-val th84 = store_thm
-  ("th84", el 84 goals |> concl,
+val th85 = store_thm
+  ("th85", el 85 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm, irreflexive_thm]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac
@@ -1292,96 +1440,154 @@ val th84 = store_thm
 val reflexive_thm = hd(amatch``Relation_reflexive _ = _``);
 
 (* |- Relation_reflexive = (\R. !x. R x x) *)
-val th85 = store_thm
-  ("th85", el 85 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm, reflexive_thm]
-  \\ CONV_TAC (DEPTH_CONV BETA_CONV)
-  \\ rpt gen_tac \\ REFL_TAC);
-
-val o_thm = hd(amatch``(Function_o _ _) _ = _``);
-
-(* |- Function_o = (\f g x. f (g x)) *)
 val th86 = store_thm
   ("th86", el 86 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,o_thm]
+  PURE_REWRITE_TAC[GSYM fun_eq_thm, reflexive_thm]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
 
-(* |- Number_Natural_greater = (\m n. Number_Natural_less n m) *)
+val transitive_thm = hd(amatch``Relation_transitive s <=> _``);
+
+(* |- Relation_transitive = (\R. !x y z. R x y /\ R y z ==> R x z) *)
 val th87 = store_thm
   ("th87", el 87 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,greater_thm]
-  \\ CONV_TAC (DEPTH_CONV BETA_CONV)
-  \\ rpt gen_tac \\ REFL_TAC);
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,transitive_thm]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ gen_tac \\ REFL_TAC);
 
-val skk = hd(amatch``Function_Combinator_s _ _ = Function_id``);
+val wellFounded_thm = hd(amatch``Relation_wellFounded r <=> !p. (?x. _) ==> _``);
 
-(* |- Function_id = Function_Combinator_s Function_const Function_const *)
+(* |- Relation_wellFounded =
+      (\R. !B. (?w. B w) ==> ?min. B min /\ !b. R b min ==> ~B b)
+ *)
 val th88 = store_thm
   ("th88", el 88 goals |> concl,
-  PURE_REWRITE_TAC[skk] \\ REFL_TAC);
+  PURE_REWRITE_TAC[GSYM fun_eq_thm]
+  \\ PURE_REWRITE_TAC[wellFounded_thm]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ gen_tac \\ REFL_TAC);
 
-val comma_11 = hd(amatch``Data_Pair_comma _ _ = Data_Pair_comma _ _``);
+val tc_def           = hd(amatch``!x. Relation_transitiveClosure x = _``);
+val bigIntersect_thm = hd(amatch``Relation_bigIntersect a b c <=> _``);
+val mem_fromPred     = hd(amatch``Set_member r (Set_fromPredicate _)``);
+val subrelation_thm  = hd(amatch``Relation_subrelation x s <=> !x y. _``);
 
-(* |- Data_Pair_comma x y = Data_Pair_comma a b <=> x = a /\ y = b *)
+(* |- Relation_transitiveClosure =
+      (\R a b.
+           !P. (!x y. R x y ==> P x y) /\ (!x y z. P x y /\ P y z ==> P x z) ==>
+               P a b)
+ *)
 val th89 = store_thm
   ("th89", el 89 goals |> concl,
-  MATCH_ACCEPT_TAC comma_11);
+  PURE_REWRITE_TAC[GSYM fun_eq_thm]
+  \\ PURE_REWRITE_TAC[tc_def,bigIntersect_thm,mem_fromPred]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ Ho_Rewrite.PURE_REWRITE_TAC[ex_imp]
+  \\ PURE_REWRITE_TAC[subrelation_thm,transitive_thm]
+  \\ PURE_ONCE_REWRITE_TAC[GSYM and_imp_intro]
+  \\ Ho_Rewrite.PURE_REWRITE_TAC[forall_eq2]
+  \\ rpt gen_tac
+  \\ PURE_REWRITE_TAC[GSYM and_imp_intro]
+  \\ REFL_TAC);
 
-(* |- Data_Sum_right x = Data_Sum_right y <=> x = y *)
+(* |- Relation_subrelation = (\R1 R2. !x y. R1 x y ==> R2 x y) *)
 val th90 = store_thm
   ("th90", el 90 goals |> concl,
-  MATCH_ACCEPT_TAC right_11);
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,subrelation_thm]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ rpt gen_tac \\ REFL_TAC);
 
-(* |- Data_Sum_left x = Data_Sum_left y <=> x = y *)
+val fromSet_thm = hd(amatch``Relation_fromSet _ _ _``);
+val intersect_thm = hd(amatch``Relation_intersect x y = _``);
+val union_thm = hd(amatch``Relation_union r s = _``);
+val mem_inter = hd(amatch``Set_member _ (Set_intersect _ _)``);
+val mem_union = hd(amatch``Set_member _ (Set_union _ _) <=> _``);
+val mem_toSet = hd(amatch``Set_member _ (Relation_toSet _)``);
+
+(* |- Relation_intersect = (\R1 R2 x y. R1 x y /\ R2 x y) *)
 val th91 = store_thm
   ("th91", el 91 goals |> concl,
-  MATCH_ACCEPT_TAC left_11);
-
-(* |- (?!x. P x) <=> (?x. P x) /\ !x y. P x /\ P y ==> x = y
-val th89 = store_thm
-  ("th89", el 89 goals |> concl,
-  MATCH_ACCEPT_TAC ex_unique_thm);
- *)
-
-val exists_simp = hd(amatch “(?x. t) <=> t”);
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,intersect_thm,fromSet_thm,mem_inter,mem_toSet]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ rpt gen_tac \\ REFL_TAC);
 
-(* |- (?!x. F) <=> F *)
+(* |- Relation_union = (\R1 R2 x y. R1 x y \/ R2 x y) *)
 val th92 = store_thm
   ("th92", el 92 goals |> concl,
-  PURE_REWRITE_TAC [BETA_RULE (SPEC “\x:'a. F” ex_unique_thm)] \\
-  PURE_REWRITE_TAC [SPEC “F” exists_simp, F_and] \\
-  REFL_TAC);
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,union_thm,fromSet_thm,mem_union,mem_toSet]
+  \\ CONV_TAC(DEPTH_CONV BETA_CONV)
+  \\ rpt gen_tac \\ REFL_TAC);
 
-val one_thm = hd(amatch``_ = Data_Unit_unit``);
+val o_thm = hd(amatch``(Function_o _ _) _ = _``);
 
-(* |- Data_Unit_unit = @x. T *)
+(* |- Function_o = (\f g x. f (g x)) *)
 val th93 = store_thm
   ("th93", el 93 goals |> concl,
-  PURE_ONCE_REWRITE_TAC[one_thm] \\ REFL_TAC);
-
-val universe_thm = hd(amatch``Relation_universe _ _``);
+  PURE_REWRITE_TAC[GSYM fun_eq_thm,o_thm]
+  \\ CONV_TAC (DEPTH_CONV BETA_CONV)
+  \\ rpt gen_tac \\ REFL_TAC);
 
-(* |- Relation_universe = (\x y. T) *)
+(* |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x'. Q x' *)
 val th94 = store_thm
   ("th94", el 94 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,EQT_INTRO(SPEC_ALL universe_thm)]
-  \\ CONV_TAC (DEPTH_CONV BETA_CONV)
-  \\ rpt gen_tac \\ REFL_TAC);
+  rpt strip_tac
+  \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
+  \\ qexists_tac`x`
+  \\ first_assum ACCEPT_TAC);
 
-val empty_thm = hd(amatch``Relation_empty _ _``);
+(* |- (!x. P x ==> Q x) ==> (!x. P x) ==> !x. Q x
+val th94' = store_thm
+  ("th94'", el ?? goals |> concl,
+  rpt strip_tac
+  \\ first_x_assum match_mp_tac
+  \\ first_x_assum(qspec_then`x`ACCEPT_TAC));
+ *)
 
-(* |- Relation_empty = (\x y. F) *)
+(* |- (x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w *)
 val th95 = store_thm
   ("th95", el 95 goals |> concl,
-  PURE_REWRITE_TAC[GSYM fun_eq_thm,EQF_INTRO (SPEC_ALL empty_thm)]
-  \\ CONV_TAC (DEPTH_CONV BETA_CONV)
-  \\ rpt gen_tac \\ REFL_TAC);
+   rpt strip_tac
+  \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
+  \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
+  \\ first_assum ACCEPT_TAC);
 
-(* |- Number_Natural_zero = Number_Natural_zero *)
+(* |- (x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w *)
 val th96 = store_thm
   ("th96", el 96 goals |> concl,
-  REFL_TAC);
+  rpt strip_tac
+  \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
+  \\ TRY (disj1_tac >> first_assum ACCEPT_TAC)
+  \\ TRY (disj2_tac >> first_assum ACCEPT_TAC));
+
+val not_T = hd(amatch``~T``);
+
+(* |- !A B. A ==> B <=> ~A \/ B *)
+val IMP_DISJ_THM = store_thm
+  ("IMP_DISJ_THM", concl boolTheory.IMP_DISJ_THM,
+  rpt gen_tac
+  \\ qspec_then`A`FULL_STRUCT_CASES_TAC bool_cases
+  \\ PURE_REWRITE_TAC[T_imp,not_T,F_imp,not_F,F_or,T_or]
+  \\ REFL_TAC);
+
+(* This is no more needed
+val some_neq_none = hd(amatch``_ <> Data_Option_none``);
+ *)
+
+fun EQT_ELIM th = EQ_MP (SYM th) truth;
+
+fun EQF_ELIM th =
+   let
+      val (lhs, rhs) = dest_eq (concl th)
+      val _ = assert Feq rhs
+   in
+      NOT_INTRO (DISCH lhs (EQ_MP th (ASSUME lhs)))
+   end;
+
+(* |- (?!x. P x) <=> (?x. P x) /\ !x y. P x /\ P y ==> x = y
+val th89 = store_thm
+  ("th89", el ?? goals |> concl,
+  MATCH_ACCEPT_TAC ex_unique_thm);
+ *)
 
 (* Now raise an error if the above th96 is not the last one *)
 val _ = if List.length goals <> 96 then
@@ -1431,7 +1637,7 @@ val BOOL_EQ_DISTINCT = store_thm("BOOL_EQ_DISTINCT", concl boolTheory.BOOL_EQ_DI
  *)
 val bool_case_thm = store_thm
   ("bool_case_thm", concl boolTheory.bool_case_thm,
-  PURE_REWRITE_TAC[th18]
+  PURE_REWRITE_TAC[bool_case_lemma]
   \\ conj_tac \\ rpt gen_tac \\ REFL_TAC);
 
 val forall_bool = hd(amatch``(!b:bool. P b) <=> _``)