From cbc649ca223d6287eb9662be83bfe37422d0ccad Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 13:53:25 +0000
Subject: [PATCH 01/19] Add bool_to_bit

---
 src/num/theories/arithmeticScript.sml | 35 +++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/src/num/theories/arithmeticScript.sml b/src/num/theories/arithmeticScript.sml
index 9ca58af265..f951878444 100644
--- a/src/num/theories/arithmeticScript.sml
+++ b/src/num/theories/arithmeticScript.sml
@@ -224,6 +224,11 @@ val NRC = new_recursive_definition {
   def = “(NRC R 0 x y = (x = y)) /\
           (NRC R (SUC n) x y = ?z. R x z /\ NRC R n z y)”};
 
+val bool_to_bit_def = new_definition(
+  "bool_to_bit_def",
+  “bool_to_bit b = if b then 1 else 0”
+);
+
 val _ = overload_on ("RELPOW", “NRC”)
 val _ = overload_on ("NRC", “NRC”)
 
@@ -4997,4 +5002,34 @@ val MOD_EXP = store_thm(
   `_ = (a * a ** m) MOD n` by rw[MOD_TIMES2] >>
   rw[EXP]);
 
+Theorem ODD_bool_to_bit[simp]:
+  ODD (bool_to_bit b) = b /\
+  ODD (1 - bool_to_bit b) = ~b
+Proof
+  rw[bool_to_bit_def, ODD, ONE, SUB_MONO_EQ, SUB_0]
+QED
+
+Theorem bool_to_bit_neq_add:
+  bool_to_bit (x <> y) =
+  (bool_to_bit x + bool_to_bit y) MOD 2
+Proof
+  reverse(rw[bool_to_bit_def, ADD_0, ADD])
+  >- (
+    rw[ONE, ADD] \\ rw[GSYM TWO, GSYM ONE]
+    \\ irule EQ_SYM
+    \\ irule (DIVMOD_ID |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL)
+    \\ rw[TWO, LESS_0] )
+  \\ irule EQ_SYM
+  \\ irule ONE_MOD
+  \\ rw[ONE, TWO, LESS_MONO, LESS_0]
+QED
+
+Theorem bool_to_bit_MOD_2[simp]:
+  bool_to_bit x MOD 2 = bool_to_bit x
+Proof
+  rw[bool_to_bit_def]
+  \\ irule ONE_MOD
+  \\ rw[ONE, TWO, LESS_MONO, LESS_0]
+QED
+
 val _ = export_theory()

From 04845565df9c260c11060ff70c459ded78440c71 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 13:53:36 +0000
Subject: [PATCH 02/19] Prove more theorems about chunks

---
 src/list/src/rich_listScript.sml | 195 +++++++++++++++++++++++++++++++
 1 file changed, 195 insertions(+)

diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
index 124bea3e0f..1e33608e1b 100644
--- a/src/list/src/rich_listScript.sml
+++ b/src/list/src/rich_listScript.sml
@@ -3189,6 +3189,201 @@ Proof
   \\ Cases_on`q` \\ fs[ADD1]
 QED
 
+Theorem chunks_append_divides:
+  !n l1 l2.
+    0 < n /\ divides n (LENGTH l1) /\ ~NULL l1 /\ ~NULL l2 ==>
+    chunks n (l1 ++ l2) = chunks n l1 ++ chunks n l2
+Proof
+  HO_MATCH_MP_TAC chunks_ind
+  \\ rw[dividesTheory.divides_def, PULL_EXISTS]
+  \\ simp[Once chunks_def]
+  \\ Cases_on`q=0` \\ fs[] \\ rfs[]
+  \\ IF_CASES_TAC
+  >- ( Cases_on`q` \\ fs[ADD1, LEFT_ADD_DISTRIB] \\ fs[LESS_OR_EQ] )
+  \\ simp[DROP_APPEND, TAKE_APPEND]
+  \\ Q.MATCH_GOALSUB_ABBREV_TAC`lhs = _`
+  \\ simp[Once chunks_def]
+  \\ Cases_on`q = 1` \\ fs[]
+  >- (
+    simp[Abbr`lhs`]
+    \\ fs[NOT_LESS_EQUAL]
+    \\ simp[DROP_LENGTH_TOO_LONG])
+  \\ simp[Abbr`lhs`]
+  \\ `n - n * q = 0` by simp[]
+  \\ simp[]
+  \\ first_x_assum irule
+  \\ simp[NULL_EQ]
+  \\ qexists_tac`q - 1`
+  \\ simp[]
+QED
+
+Theorem chunks_length:
+  chunks (LENGTH ls) ls = [ls]
+Proof
+  rw[Once chunks_def]
+QED
+
+Theorem chunks_not_nil[simp]:
+  !n ls. chunks n ls <> []
+Proof
+  HO_MATCH_MP_TAC chunks_ind
+  \\ rw[]
+  \\ rw[Once chunks_def]
+QED
+
+Theorem LENGTH_chunks:
+  !n ls. 0 < n ∧ ¬NULL ls ==>
+    LENGTH (chunks n ls) =
+    LENGTH ls DIV n + (bool_to_bit $ ~divides n (LENGTH ls))
+Proof
+  HO_MATCH_MP_TAC chunks_ind
+  \\ rw[]
+  \\ rw[Once chunks_def, dividesTheory.DIV_EQUAL_0, bool_to_bit_def,
+        dividesTheory.divides_def]
+  \\ fs[LESS_OR_EQ, ADD1, NULL_EQ, bool_to_bit_def] \\ rfs[]
+  \\ rw[]
+  \\ fs[dividesTheory.divides_def, dividesTheory.SUB_DIV]
+  \\ rfs[]
+  >- (
+    Cases_on`LENGTH ls DIV n = 0` >- rfs[dividesTheory.DIV_EQUAL_0]
+    \\ simp[] )
+  >- (
+    Cases_on`q` \\ fs[MULT_SUC]
+    \\ Q.MATCH_ASMSUB_RENAME_TAC`n + n * p`
+    \\ first_x_assum(Q.SPEC_THEN`2 + p`mp_tac)
+    \\ simp[LEFT_ADD_DISTRIB] )
+  >- (
+    first_x_assum(Q.SPEC_THEN`PRE q`mp_tac)
+    \\ Cases_on`q` \\ fs[MULT_SUC] )
+  \\ Cases_on`q` \\ fs[MULT_SUC]
+  \\ simp[ADD_DIV_RWT]
+QED
+
+Theorem EL_chunks:
+  ∀k ls n.
+  n < LENGTH (chunks k ls) /\ 0 < k /\ ~NULL ls ==>
+  EL n (chunks k ls) = TAKE k (DROP (n * k) ls)
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[NULL_EQ]
+  \\ Q.PAT_X_ASSUM`_ < LENGTH _ `mp_tac
+  \\ rw[Once chunks_def] \\ fs[]
+  \\ rw[Once chunks_def]
+  \\ Q.MATCH_GOALSUB_RENAME_TAC`EL m _`
+  \\ Cases_on`m` \\ fs[]
+  \\ pop_assum mp_tac
+  \\ dep_rewrite.DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ simp[NULL_EQ]
+  \\ strip_tac
+  \\ dep_rewrite.DEP_REWRITE_TAC[DROP_DROP]
+  \\ simp[MULT_SUC]
+  \\ Q.MATCH_GOALSUB_RENAME_TAC`k + k * m <= _`
+  \\ `k * m <= LENGTH ls - k` suffices_by simp[]
+  \\ `m <= (LENGTH ls - k) DIV k` suffices_by simp[X_LE_DIV]
+  \\ fs[bool_to_bit_def]
+  \\ pop_assum mp_tac \\ rw[]
+QED
+
+Theorem chunks_MAP:
+  !n ls. chunks n (MAP f ls) = MAP (MAP f) (chunks n ls)
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[]
+  \\ rw[Once chunks_def]
+  >- rw[Once chunks_def]
+  >- rw[Once chunks_def]
+  \\ fs[]
+  \\ simp[GSYM MAP_DROP]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ simp[MAP_TAKE]
+QED
+
+Theorem chunks_ZIP:
+  !n ls l2. LENGTH ls = LENGTH l2 ==>
+  chunks n (ZIP (ls, l2)) = MAP ZIP (ZIP (chunks n ls, chunks n l2))
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[]
+  \\ rw[Once chunks_def]
+  >- ( rw[Once chunks_def] \\ rw[Once chunks_def] )
+  >- rw[Once chunks_def]
+  \\ fs[]
+  \\ simp[GSYM ZIP_DROP]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ CONV_TAC(PATH_CONV"rrrr"(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ simp[ZIP_TAKE]
+QED
+
+Theorem chunks_TAKE:
+  !n ls m. divides n m /\ 0 < m ==>
+    chunks n (TAKE m ls) = TAKE (m DIV n) (chunks n ls)
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ rw[]
+  >- (
+    rw[Once chunks_def] \\ fs[LENGTH_TAKE_EQ]
+    \\ fs[dividesTheory.divides_def]
+    \\ BasicProvers.VAR_EQ_TAC
+    \\ Q.MATCH_GOALSUB_RENAME_TAC`n * m`
+    \\ fs[ZERO_LESS_MULT]
+    \\ `n <= n * m` by simp[LE_MULT_CANCEL_LBARE]
+    \\ dep_rewrite.DEP_REWRITE_TAC[TAKE_LENGTH_TOO_LONG]
+    \\ simp[MULT_DIV] )
+  >- fs[dividesTheory.divides_def]
+  \\ fs[]
+  \\ simp[Once chunks_def, LENGTH_TAKE_EQ]
+  \\ `n <= m` by (
+    rfs[dividesTheory.divides_def] \\ rw[]
+    \\ fs[ZERO_LESS_MULT] )
+  \\ IF_CASES_TAC
+  >- (
+    pop_assum mp_tac \\ rw[]
+    \\ `m = n` by fs[] \\ rw[] )
+  \\ fs[TAKE_TAKE, DROP_TAKE]
+  \\ first_x_assum(Q.SPEC_THEN`m - n`mp_tac)
+  \\ simp[]
+  \\ impl_keep_tac >- (
+    fs[dividesTheory.divides_def]
+    \\ qexists_tac`q - 1`
+    \\ simp[LEFT_SUB_DISTRIB] )
+  \\ rw[]
+  \\ `m DIV n <> 0` by fs[dividesTheory.DIV_EQUAL_0]
+  \\ Cases_on`m DIV n` \\ fs[TAKE_TAKE_MIN]
+  \\ `MIN n m = n` by fs[MIN_DEF] \\ rw[]
+  \\ simp[dividesTheory.SUB_DIV]
+QED
+
+Definition chunks_tr_aux_def:
+  chunks_tr_aux n ls acc =
+    if LENGTH ls <= SUC n then REVERSE $ ls :: acc
+    else chunks_tr_aux n (DROP (SUC n) ls) (TAKE (SUC n) ls :: acc)
+Termination
+  WF_REL_TAC`measure $ LENGTH o FST o SND`
+  \\ rw[LENGTH_DROP]
+End
+
+Definition chunks_tr_def:
+  chunks_tr n ls = if n = 0 then [ls] else chunks_tr_aux (n - 1) ls []
+End
+
+Theorem chunks_tr_aux_thm:
+  !n ls acc.
+    chunks_tr_aux n ls acc =
+    REVERSE acc ++ chunks (SUC n) ls
+Proof
+  HO_MATCH_MP_TAC chunks_tr_aux_ind
+  \\ rw[]
+  \\ rw[Once chunks_tr_aux_def]
+  >- rw[Once chunks_def]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ rw[]
+QED
+
+Theorem chunks_tr_thm:
+  chunks_tr = chunks
+Proof
+  simp[FUN_EQ_THM, chunks_tr_def]
+  \\ Cases \\ rw[chunks_tr_aux_thm]
+QED
+
 (*---------------------------------------------------------------------------*)
 (* Various lemmas from the CakeML project https://cakeml.org                 *)
 (*---------------------------------------------------------------------------*)

From 9c5d06bd8e5bbcc9abd6cf6fed3afd6a1c3883b3 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 14:09:45 +0000
Subject: [PATCH 03/19] Fix some Unicode violations

---
 src/list/src/rich_listScript.sml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
index 1e33608e1b..092d1e2cec 100644
--- a/src/list/src/rich_listScript.sml
+++ b/src/list/src/rich_listScript.sml
@@ -3232,7 +3232,7 @@ Proof
 QED
 
 Theorem LENGTH_chunks:
-  !n ls. 0 < n ∧ ¬NULL ls ==>
+  !n ls. 0 < n /\ ~NULL ls ==>
     LENGTH (chunks n ls) =
     LENGTH ls DIV n + (bool_to_bit $ ~divides n (LENGTH ls))
 Proof
@@ -3260,7 +3260,7 @@ Proof
 QED
 
 Theorem EL_chunks:
-  ∀k ls n.
+  !k ls n.
   n < LENGTH (chunks k ls) /\ 0 < k /\ ~NULL ls ==>
   EL n (chunks k ls) = TAKE k (DROP (n * k) ls)
 Proof

From aa170a503f19bdcb8ba51a067c3c84591ee2f468 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 14:28:49 +0000
Subject: [PATCH 04/19] Add some theorems about dropWhile

---
 src/list/src/listScript.sml      | 10 ++++++++++
 src/list/src/rich_listScript.sml | 22 +++++++++++++++++++++-
 2 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/src/list/src/listScript.sml b/src/list/src/listScript.sml
index 84a465bb0d..e728fddbe0 100644
--- a/src/list/src/listScript.sml
+++ b/src/list/src/listScript.sml
@@ -4734,6 +4734,16 @@ val EL_LENGTH_dropWhile_REVERSE = Q.store_thm("EL_LENGTH_dropWhile_REVERSE",
    >> fs [NOT_EVERY, dropWhile_APPEND_EXISTS, arithmeticTheory.ADD1])
 end
 
+Theorem dropWhile_id:
+ (dropWhile P ls = ls) <=> NULL ls \/ ~P(HD ls)
+Proof
+  Cases_on`ls` \\ rw[dropWhile_def, NULL]
+  \\ disch_then(mp_tac o Q.AP_TERM`LENGTH`)
+  \\ Q.MATCH_GOALSUB_RENAME_TAC`dropWhile P l`
+  \\ Q.SPECL_THEN[`P`,`l`]mp_tac LENGTH_dropWhile_LESS_EQ
+  \\ simp[]
+QED
+
 val IMP_EVERY_LUPDATE = store_thm("IMP_EVERY_LUPDATE",
   “!xs h i. P h /\ EVERY P xs ==> EVERY P (LUPDATE h i xs)”,
   Induct THEN fs [LUPDATE_def] THEN REPEAT STRIP_TAC
diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
index 092d1e2cec..08638478e9 100644
--- a/src/list/src/rich_listScript.sml
+++ b/src/list/src/rich_listScript.sml
@@ -8,7 +8,7 @@ open HolKernel Parse boolLib BasicProvers;
 open numLib metisLib simpLib combinTheory arithmeticTheory prim_recTheory
      pred_setTheory listTheory pairTheory markerLib TotalDefn;
 
-local open listSimps pred_setSimps in end;
+local open listSimps pred_setSimps dep_rewrite in end;
 
 val FILTER_APPEND = FILTER_APPEND_DISTRIB
 val REVERSE = REVERSE_SNOC_DEF
@@ -3783,6 +3783,26 @@ Proof
 QED
 (* END more lemmas of IS_SUFFIX *)
 
+Theorem IS_SUFFIX_dropWhile:
+  IS_SUFFIX ls (dropWhile P ls)
+Proof
+  Induct_on`ls`
+  \\ rw[IS_SUFFIX_CONS]
+QED
+
+Theorem LENGTH_dropWhile_id:
+  (LENGTH (dropWhile P ls) = LENGTH ls) <=> (dropWhile P ls = ls)
+Proof
+  rw[EQ_IMP_THM]
+  \\ rw[dropWhile_id]
+  \\ Cases_on`ls` \\ fs[]
+  \\ strip_tac \\ fs[]
+  \\ `IS_SUFFIX t (dropWhile P t)` by simp[IS_SUFFIX_dropWhile]
+  \\ fs[IS_SUFFIX_APPEND]
+  \\ `LENGTH t = LENGTH l + LENGTH (dropWhile P t)` by metis_tac[LENGTH_APPEND]
+  \\ fs[]
+QED
+
 Theorem nub_GENLIST:
   nub (GENLIST f n) =
     MAP f (FILTER (\i. !j. (i < j) /\ (j < n) ==> f i <> f j) (COUNT_LIST n))

From c46c51b6aabab5c6db77225bc783b8573086d0ee Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 14:35:04 +0000
Subject: [PATCH 05/19] Add LENGTH_word_to_bin_list_bound

---
 src/n-bit/wordsScript.sml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
index 7d17c753b9..fe73361758 100644
--- a/src/n-bit/wordsScript.sml
+++ b/src/n-bit/wordsScript.sml
@@ -5060,6 +5060,18 @@ QED
 Theorem CARD_WORD = CARD_CART_UNIV |> INST_TYPE [alpha |-> bool]
                                    |> SIMP_RULE bool_ss [CARD_BOOL,FINITE_BOOL]
 
+(* -------------------------------------------------------------------------
+    Theorems about word_to_bin_list
+   ------------------------------------------------------------------------- *)
+
+Theorem LENGTH_word_to_bin_list_bound:
+  LENGTH (word_to_bin_list (w:'a word)) <= (dimindex (:'a))
+Proof
+  rw[word_to_bin_list_def, w2l_def, LENGTH_n2l]
+  \\ Cases_on`w` \\ simp[]
+  \\ fs[dimword_def, GSYM LESS_EQ, LOG2_def, logrootTheory.LT_EXP_LOG]
+QED
+
 (* -------------------------------------------------------------------------
     Create a few word sizes
    ------------------------------------------------------------------------- *)

From eebff12797bfd2990083b2b6070ac77fd05dd89e Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 15:06:25 +0000
Subject: [PATCH 06/19] Prove word_from_bin_list rol and ror

---
 src/n-bit/wordsScript.sml | 55 ++++++++++++++++++++++++++++++++++++++-
 1 file changed, 54 insertions(+), 1 deletion(-)

diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
index fe73361758..2c4ccd0d56 100644
--- a/src/n-bit/wordsScript.sml
+++ b/src/n-bit/wordsScript.sml
@@ -5061,7 +5061,7 @@ Theorem CARD_WORD = CARD_CART_UNIV |> INST_TYPE [alpha |-> bool]
                                    |> SIMP_RULE bool_ss [CARD_BOOL,FINITE_BOOL]
 
 (* -------------------------------------------------------------------------
-    Theorems about word_to_bin_list
+    Theorems about word_{to,from}_bin_list
    ------------------------------------------------------------------------- *)
 
 Theorem LENGTH_word_to_bin_list_bound:
@@ -5072,6 +5072,59 @@ Proof
   \\ fs[dimword_def, GSYM LESS_EQ, LOG2_def, logrootTheory.LT_EXP_LOG]
 QED
 
+Theorem word_from_bin_list_ror:
+  x < dimindex(:'a) /\ LENGTH ls = dimindex(:'a)
+  ==>
+  word_ror (word_from_bin_list ls : 'a word) x =
+  word_from_bin_list (DROP x ls ++ TAKE x ls)
+Proof
+  rw[word_from_bin_list_def, l2w_def]
+  \\ Cases_on`x = 0` \\ gs[SHIFT_ZERO]
+  \\ rw[word_ror_n2w, l2n_APPEND]
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ qspecl_then[`x`,`ls`](mp_tac o SYM) listTheory.TAKE_DROP
+  \\ disch_then(SUBST1_TAC o Q.AP_TERM`l2n 2`)
+  \\ rewrite_tac[l2n_APPEND]
+  \\ simp[]
+  \\ qmatch_goalsub_abbrev_tac`BITS _ _ (2 ** x * ld + lt)`
+  \\ qspecl_then[`x - 1`,`0`,`ld`,`lt`]mp_tac BITS_SUM2
+  \\ simp[ADD1]
+  \\ disch_then kall_tac
+  \\ qspecl_then[`x-1`,`lt`]mp_tac BITS_ZEROL
+  \\ simp[ADD1]
+  \\ impl_keep_tac
+  >- (
+    qspecl_then[`TAKE x ls`,`2`]mp_tac l2n_lt
+    \\ simp[] )
+  \\ simp[]
+  \\ disch_then kall_tac
+  \\ simp_tac std_ss [Once ADD_COMM, SimpRHS]
+  \\ qmatch_goalsub_abbrev_tac`BITS h x`
+  \\ qspecl_then[`h`,`x`,`ld`,`lt`]mp_tac BITS_SUM
+  \\ simp[] \\ disch_then kall_tac
+  \\ DEP_REWRITE_TAC[BITS_ZERO4]
+  \\ simp[Abbr`h`]
+  \\ DEP_REWRITE_TAC[BITS_ZEROL]
+  \\ qspecl_then[`DROP x ls`,`2`]mp_tac l2n_lt
+  \\ simp[ADD1]
+QED
+
+Theorem word_from_bin_list_rol:
+  x < dimindex(:'a) /\ LENGTH ls = dimindex(:'a)
+  ==>
+  word_rol (word_from_bin_list ls : 'a word) x =
+  word_from_bin_list (LASTN x ls ++ BUTLASTN x ls)
+Proof
+  rw[word_rol_def]
+  \\ Cases_on`x=0`
+  >- (
+    rw[rich_listTheory.LASTN, rich_listTheory.BUTLASTN]
+    \\ ONCE_REWRITE_TAC[GSYM ROR_MOD]
+    \\ rw[SHIFT_ZERO] )
+  \\ DEP_REWRITE_TAC[word_from_bin_list_ror]
+  \\ simp[rich_listTheory.LASTN_DROP, rich_listTheory.BUTLASTN_TAKE]
+QED
+
 (* -------------------------------------------------------------------------
     Create a few word sizes
    ------------------------------------------------------------------------- *)

From ae219da1dee3382e1e6fb111b318fbd2038e82dd Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 15:58:26 +0000
Subject: [PATCH 07/19] Prove word_from_bin_list_and

---
 src/list/src/numposrepScript.sml      | 16 ++++++++++++++
 src/n-bit/wordsScript.sml             | 31 +++++++++++++++++++++++++++
 src/num/extra_theories/bitScript.sml  |  6 ++++++
 src/num/theories/arithmeticScript.sml | 13 +++++++++++
 4 files changed, 66 insertions(+)

diff --git a/src/list/src/numposrepScript.sml b/src/list/src/numposrepScript.sml
index 3446fa2dd1..afe4c56dfe 100644
--- a/src/list/src/numposrepScript.sml
+++ b/src/list/src/numposrepScript.sml
@@ -422,4 +422,20 @@ val l2n_11 = Q.store_thm("l2n_11",
         \\ NTAC 2 (POP_ASSUM SUBST1_TAC)
         \\ FULL_SIMP_TAC (srw_ss()) [l2n_APPEND]]);
 
+Theorem BITWISE_l2n_2:
+  LENGTH l1 = LENGTH l2 ==>
+  BITWISE (LENGTH l1) op (l2n 2 l1) (l2n 2 l2) =
+  l2n 2 (MAP2 (\x y. bool_to_bit $ op (ODD x) (ODD y)) l1 l2)
+Proof
+  Q.ID_SPEC_TAC`l2`
+  \\ Induct_on`l1`
+  \\ simp[BITWISE_EVAL]
+  >- simp[BITWISE_def, l2n_def]
+  \\ Q.X_GEN_TAC`b`
+  \\ Cases \\ fs[BITWISE_EVAL]
+  \\ strip_tac
+  \\ fs[l2n_def]
+  \\ simp[SBIT_def, ODD_ADD, ODD_MULT, GSYM bool_to_bit_def]
+QED
+
 val _ = export_theory()
diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
index 2c4ccd0d56..4922e6dee6 100644
--- a/src/n-bit/wordsScript.sml
+++ b/src/n-bit/wordsScript.sml
@@ -5125,6 +5125,37 @@ Proof
   \\ simp[rich_listTheory.LASTN_DROP, rich_listTheory.BUTLASTN_TAKE]
 QED
 
+Theorem word_from_bin_list_and:
+  LENGTH l1 = dimindex(:'a) /\
+  LENGTH l2 = dimindex(:'a)
+  ==>
+  word_from_bin_list l1 && word_from_bin_list l2 : 'a word =
+  word_from_bin_list (MAP2 (\x y. bool_to_bit $ (ODD x /\ ODD y)) l1 l2)
+Proof
+  rw[word_from_bin_list_def, l2w_def, word_and_n2w]
+  \\ qmatch_goalsub_abbrev_tac`BITWISE n`
+  \\ qmatch_goalsub_abbrev_tac`a MOD d = b MOD d`
+  \\ `d = 2 ** n`
+  by simp[Abbr`d`, Abbr`n`, dimword_def]
+  \\ `a < d` by (
+    pop_assum SUBST1_TAC
+    \\ qunabbrev_tac`a`
+    \\ irule BITWISE_LT_2EXP )
+  \\ `b < d`
+  by (
+    qunabbrev_tac`b`
+    \\ qmatch_goalsub_abbrev_tac`l2n 2 ls`
+    \\ `n = LENGTH ls` by simp[Abbr`ls`]
+    \\ qunabbrev_tac`d`
+    \\ qpat_x_assum`_ = 2 ** _`SUBST1_TAC
+    \\ pop_assum SUBST1_TAC
+    \\ irule l2n_lt \\ simp[] )
+  \\ simp[]
+  \\ unabbrev_all_tac
+  \\ DEP_REWRITE_TAC[GSYM BITWISE_l2n_2]
+  \\ simp[]
+QED
+
 (* -------------------------------------------------------------------------
     Create a few word sizes
    ------------------------------------------------------------------------- *)
diff --git a/src/num/extra_theories/bitScript.sml b/src/num/extra_theories/bitScript.sml
index 8ff867a02a..609f2134c6 100644
--- a/src/num/extra_theories/bitScript.sml
+++ b/src/num/extra_theories/bitScript.sml
@@ -381,6 +381,12 @@ val NOT_MOD2_LEM2 = Q.store_thm("NOT_MOD2_LEM2",
 val ODD_MOD2_LEM = Q.store_thm("ODD_MOD2_LEM",
    `!n. ODD n = ((n MOD 2) = 1)`, RW_TAC arith_ss [ODD_EVEN, MOD_2])
 
+Theorem ODD_MOD_2[simp]:
+  ODD (x MOD 2) = ODD x
+Proof
+  RW_TAC arith_ss [ODD_MOD2_LEM]
+QED
+
 (* ------------------------------------------------------------------------- *)
 
 val DIV_MULT_THM = Q.store_thm("DIV_MULT_THM",
diff --git a/src/num/theories/arithmeticScript.sml b/src/num/theories/arithmeticScript.sml
index f951878444..5d7c49a333 100644
--- a/src/num/theories/arithmeticScript.sml
+++ b/src/num/theories/arithmeticScript.sml
@@ -2967,6 +2967,19 @@ Proof
  >> PROVE_TAC []
 QED
 
+Theorem MOD_DIV_SAME[simp]:
+  0 < y ==> x MOD y DIV y = 0
+Proof
+  strip_tac
+  \\ Cases_on`y=1` \\ fs[DIV_1, MOD_1]
+  \\ `1 < y` by (
+    simp[ONE, SUC_LT]
+    \\ Cases_on`y` \\ fs[NOT_LESS_0, ONE]
+    \\ drule (NOT_LT_ZERO_EQ_ZERO |> GSYM |> SPEC_ALL |> iffRL |> CONTRAPOS)
+    \\ rw[] )
+  \\ rw[DIV_EQ_0, MOD_LESS]
+QED
+
 (* ------------------------------------------------------------------------ *)
 (* Some miscellaneous lemmas (from transc.ml)                               *)
 (* ------------------------------------------------------------------------ *)

From afdcb4a2d54201f48401900c939980727dd0d1cc Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 16:22:04 +0000
Subject: [PATCH 08/19] Prove word_from_bin_list_not

---
 src/list/src/numposrepScript.sml | 61 ++++++++++++++++++++++++++++++++
 src/n-bit/wordsScript.sml        | 42 ++++++++++++++++++++++
 2 files changed, 103 insertions(+)

diff --git a/src/list/src/numposrepScript.sml b/src/list/src/numposrepScript.sml
index afe4c56dfe..0e36457194 100644
--- a/src/list/src/numposrepScript.sml
+++ b/src/list/src/numposrepScript.sml
@@ -438,4 +438,65 @@ Proof
   \\ simp[SBIT_def, ODD_ADD, ODD_MULT, GSYM bool_to_bit_def]
 QED
 
+Theorem l2n_2_neg:
+  !ls.
+  EVERY ($> 2) ls ==>
+  2 ** LENGTH ls - SUC (l2n 2 ls) = l2n 2 (MAP (\x. 1 - x) ls)
+Proof
+  Induct
+  \\ rw[l2n_def]
+  \\ fs[EXP, ADD1]
+  \\ first_x_assum(CHANGED_TAC o SUBST1_TAC o SYM)
+  \\ simp[LEFT_SUB_DISTRIB, LEFT_ADD_DISTRIB, SUB_RIGHT_ADD]
+  \\ Q.SPECL_THEN[`ls`,`2`]mp_tac l2n_lt
+  \\ simp[]
+QED
+
+Theorem l2n_max:
+  0 < b ==>
+  !ls. (l2n b ls = b ** (LENGTH ls) - 1) <=>
+       (EVERY ((=) (b - 1) o flip $MOD b) ls)
+Proof
+  strip_tac
+  \\ Induct
+  \\ rw[l2n_def]
+  \\ rw[EXP]
+  \\ Q.MATCH_GOALSUB_ABBREV_TAC`b * l + a`
+  \\ Q.MATCH_GOALSUB_ABBREV_TAC`b ** n`
+  \\ fs[EQ_IMP_THM]
+  \\ conj_tac
+  >- (
+    strip_tac
+    \\ Cases_on`n=0` \\ fs[] >- (fs[Abbr`n`] \\ rw[])
+    \\ `0 < b * b ** n` by simp[]
+    \\ `a + b * l + 1 = b * b ** n` by simp[]
+    \\ `(b * b ** n) DIV b = b ** n` by simp[MULT_TO_DIV]
+    \\ `(b * l + (a + 1)) DIV b = b ** n` by fs[]
+    \\ `(b * l) MOD b = 0` by simp[]
+    \\ `(b * l + (a + 1)) DIV b = (b * l) DIV b + (a + 1) DIV b`
+    by ( irule ADD_DIV_RWT \\ simp[] )
+    \\ pop_assum SUBST_ALL_TAC
+    \\ `(a + 1) DIV b = if a = b - 1 then 1 else 0`
+    by (
+      rw[]
+      \\ `a + 1 < b` suffices_by rw[DIV_EQ_0]
+      \\ simp[Abbr`a`]
+      \\ `h MOD b < b - 1` suffices_by simp[]
+      \\ `h MOD b < b` by simp[]
+      \\ fs[] )
+    \\ `b * l DIV b = l` by simp[MULT_TO_DIV]
+    \\ pop_assum SUBST_ALL_TAC
+    \\ pop_assum SUBST_ALL_TAC
+    \\ `l < b ** n` by ( map_every Q.UNABBREV_TAC[`l`,`n`]
+                         \\ irule l2n_lt \\ simp[] )
+    \\ Cases_on`a = b - 1` \\ fs[] )
+  \\ strip_tac
+  \\ rewrite_tac[LEFT_SUB_DISTRIB]
+  \\ Q.PAT_X_ASSUM`_ = a`(SUBST1_TAC o SYM)
+  \\ fs[SUB_LEFT_ADD] \\ rw[]
+  \\ Cases_on`n=0` \\ fs[]
+  \\ `b ** n <= b ** 0` by simp[]
+  \\ fs[EXP_BASE_LE_IFF]
+QED
+
 val _ = export_theory()
diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
index 4922e6dee6..7e83f0db5b 100644
--- a/src/n-bit/wordsScript.sml
+++ b/src/n-bit/wordsScript.sml
@@ -5156,6 +5156,48 @@ Proof
   \\ simp[]
 QED
 
+Theorem word_from_bin_list_not:
+  LENGTH ls = dimindex(:'a) /\ EVERY ($> 2) ls ==>
+  ~word_from_bin_list ls : 'a word =
+  word_from_bin_list (MAP (\x. 1 - x) ls)
+Proof
+  rw[word_from_bin_list_def, l2w_def]
+  \\ rewrite_tac[word_1comp_n2w]
+  \\ Cases_on`l2n 2 ls = dimword(:'a) - 1`
+  >- (
+    mp_then Any (qspec_then`ls`mp_tac)
+      l2n_max (SIMP_CONV(srw_ss())[]``0 < 2n`` |> EQT_ELIM)
+    \\ `dimword (:'a) = 2 ** LENGTH ls` by simp[dimword_def]
+    \\ first_assum (SUBST_ALL_TAC o SYM)
+    \\ pop_assum kall_tac
+    \\ pop_assum SUBST_ALL_TAC
+    \\ simp[ADD1, ZERO_LT_dimword]
+    \\ strip_tac
+    \\ qmatch_goalsub_abbrev_tac`A MOD N = 0`
+    \\ `A = 0` suffices_by rw[]
+    \\ rw[Abbr`A`, l2n_eq_0]
+    \\ gs[listTheory.EVERY_MAP, listTheory.EVERY_MEM]
+    \\ rw[]
+    \\ `2 > x` by simp[]
+    \\ `x < 2` by simp[]
+    \\ pop_assum mp_tac
+    \\ `x MOD 2 = 1` by simp[]
+    \\ rewrite_tac[NUMERAL_LESS_THM]
+    \\ strip_tac \\ fs[] )
+  \\ `SUC (l2n 2 ls) < dimword(:'a)`
+  by (
+    qspecl_then[`ls`,`2`]mp_tac l2n_lt
+    \\ gs[dimword_def] )
+  \\ qmatch_goalsub_abbrev_tac`_ = n2w $ l2n 2 l1`
+  \\ `l2n 2 l1 < dimword(:'a)`
+  by (
+    qspecl_then[`l1`,`2`]mp_tac l2n_lt
+    \\ gs[dimword_def, Abbr`l1`] )
+  \\ simp[Abbr`l1`]
+  \\ drule l2n_2_neg
+  \\ simp[dimword_def]
+QED
+
 (* -------------------------------------------------------------------------
     Create a few word sizes
    ------------------------------------------------------------------------- *)

From 5ae53ad0f07b18c456de93906c009d5db1a22c07 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 18:35:14 +0000
Subject: [PATCH 09/19] Add some theorems about l2w and w2l

---
 src/list/src/numposrepScript.sml |  8 ++++++++
 src/n-bit/wordsScript.sml        | 23 +++++++++++++++++++++++
 2 files changed, 31 insertions(+)

diff --git a/src/list/src/numposrepScript.sml b/src/list/src/numposrepScript.sml
index 0e36457194..773f7b2b8d 100644
--- a/src/list/src/numposrepScript.sml
+++ b/src/list/src/numposrepScript.sml
@@ -499,4 +499,12 @@ Proof
   \\ fs[EXP_BASE_LE_IFF]
 QED
 
+Theorem l2n_PAD_RIGHT_0[simp]:
+  0 < b ==> l2n b (PAD_RIGHT 0 h ls) = l2n b ls
+Proof
+  Induct_on`ls` \\ rw[l2n_def, PAD_RIGHT, l2n_eq_0, EVERY_GENLIST]
+  \\ fs[PAD_RIGHT, l2n_APPEND]
+  \\ fs[l2n_eq_0, EVERY_GENLIST]
+QED
+
 val _ = export_theory()
diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
index 7e83f0db5b..fc3c309a45 100644
--- a/src/n-bit/wordsScript.sml
+++ b/src/n-bit/wordsScript.sml
@@ -5060,6 +5060,29 @@ QED
 Theorem CARD_WORD = CARD_CART_UNIV |> INST_TYPE [alpha |-> bool]
                                    |> SIMP_RULE bool_ss [CARD_BOOL,FINITE_BOOL]
 
+Theorem MEM_w2l_less:
+  1 < b /\ MEM x (w2l b w) ==> x < b
+Proof
+  Cases_on`w`
+  \\ rw[w2l_def]
+  \\ rpt $ pop_assum mp_tac
+  \\ map_every qid_spec_tac [`x`,`n`,`b`]
+  \\ recInduct n2l_ind
+  \\ rw[]
+  \\ pop_assum mp_tac
+  \\ rw[Once n2l_def]
+  >- ( irule MOD_LESS \\ gs[] )
+  \\ first_x_assum irule
+  \\ gs[DIV_LT_X]
+  \\ Cases_on`b` \\ gs[MULT]
+QED
+
+Theorem l2w_PAD_RIGHT_0[simp]:
+  0 < b ==> l2w b (PAD_RIGHT 0 h ls) = l2w b ls
+Proof
+  rw[l2w_def]
+QED
+
 (* -------------------------------------------------------------------------
     Theorems about word_{to,from}_bin_list
    ------------------------------------------------------------------------- *)

From 5fb53e44ac0cd0562e366c3decf347905a3e70b5 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 18:43:19 +0000
Subject: [PATCH 10/19] Prove BITWISE_COMM and BITWISE_AND_0

---
 src/num/extra_theories/bitScript.sml | 34 ++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/src/num/extra_theories/bitScript.sml b/src/num/extra_theories/bitScript.sml
index 609f2134c6..8b91f3c0ac 100644
--- a/src/num/extra_theories/bitScript.sml
+++ b/src/num/extra_theories/bitScript.sml
@@ -1526,4 +1526,38 @@ Proof
   simp_tac std_ss []
 QED
 
+Theorem BITWISE_COMM:
+  (!m. m <= n ==> op (BIT m x) (BIT m y) = op (BIT m y) (BIT m x))
+  ==> BITWISE n op x y = BITWISE n op y x
+Proof
+  Induct_on`n`
+  \\ SRW_TAC[][BITWISE_def]
+  \\ first_assum(Q.SPEC_THEN`n`mp_tac)
+  \\ impl_tac >- SRW_TAC[][]
+  \\ disch_then SUBST1_TAC
+  \\ simp[]
+  \\ first_x_assum irule
+  \\ SRW_TAC[][]
+  \\ first_x_assum irule
+  \\ simp[]
+QED
+
+Triviality BITWISE_AND_0_lemma:
+  BITWISE w $/\ x 0 = 0
+Proof
+  Q.ID_SPEC_TAC`x`
+  \\ Induct_on`w`
+  \\ SRW_TAC[][BITWISE_def, SBIT_def, BIT_ZERO]
+QED
+
+Theorem BITWISE_AND_0[simp]:
+  BITWISE w $/\ x 0 = 0 /\
+  BITWISE w $/\ 0 x = 0
+Proof
+  Q.SPECL_THEN[`$/\`,`0`,`x`,`w`]mp_tac(Q.GENL[`op`,`x`,`y`,`n`]BITWISE_COMM)
+  \\ impl_tac >- SRW_TAC[][BIT_ZERO]
+  \\ disch_then SUBST1_TAC
+  \\ SRW_TAC[][BITWISE_AND_0_lemma]
+QED
+
 val _ = export_theory()

From db909049b5ea08b252d8ab39a6fca6892bc094c3 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 18:49:56 +0000
Subject: [PATCH 11/19] Prove word_and_lsl_eq_0

---
 src/n-bit/wordsScript.sml            |  9 +++++++++
 src/num/extra_theories/bitScript.sml | 17 +++++++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
index fc3c309a45..0d2a7c4223 100644
--- a/src/n-bit/wordsScript.sml
+++ b/src/n-bit/wordsScript.sml
@@ -5083,6 +5083,15 @@ Proof
   rw[l2w_def]
 QED
 
+Theorem word_and_lsl_eq_0:
+  w2n w1 < 2 ** n ==> w1 && w2 << n = 0w
+Proof
+  Cases_on`w1` \\ Cases_on`w2`
+  \\ rw[word_and_n2w, word_lsl_n2w]
+  \\ drule BITWISE_AND_SHIFT_EQ_0
+  \\ simp[]
+QED
+
 (* -------------------------------------------------------------------------
     Theorems about word_{to,from}_bin_list
    ------------------------------------------------------------------------- *)
diff --git a/src/num/extra_theories/bitScript.sml b/src/num/extra_theories/bitScript.sml
index 8b91f3c0ac..3302624813 100644
--- a/src/num/extra_theories/bitScript.sml
+++ b/src/num/extra_theories/bitScript.sml
@@ -1560,4 +1560,21 @@ Proof
   \\ SRW_TAC[][BITWISE_AND_0_lemma]
 QED
 
+Theorem BITWISE_AND_SHIFT_EQ_0:
+  !w x y n.
+  x < 2 ** n ==>
+  BITWISE w $/\ x (y * 2 ** n) = 0
+Proof
+  Induct \\ SRW_TAC[][BITWISE_def, SBIT_def]
+  \\ strip_tac
+  \\ Cases_on`w < n`
+  >- ( drule BIT_SHIFT_THM3 \\ simp[]
+       \\ Q.EXISTS_TAC`y` \\ simp[])
+  \\ FULL_SIMP_TAC(srw_ss())[NOT_LESS]
+  \\ drule TWOEXP_MONO2 \\ strip_tac
+  \\ `x < 2 ** w` by METIS_TAC[LESS_LESS_EQ_TRANS]
+  \\ drule NOT_BIT_GT_TWOEXP
+  \\ simp[]
+QED
+
 val _ = export_theory()

From 4e16bd3b331c521cff62afc5004a100fdf048368 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 23:33:53 +0000
Subject: [PATCH 12/19] Attempt to fix OpenTheory base vs HOL4

---
 src/boss/prove_base_assumsScript.sml | 173 +++++++++++++--------------
 1 file changed, 85 insertions(+), 88 deletions(-)

diff --git a/src/boss/prove_base_assumsScript.sml b/src/boss/prove_base_assumsScript.sml
index 3d4fded15b..71d4be7806 100644
--- a/src/boss/prove_base_assumsScript.sml
+++ b/src/boss/prove_base_assumsScript.sml
@@ -222,80 +222,80 @@ val goals =
  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.
+ 32 |- !f g. f = g <=> !x. f x = g x,
+ 33 |- !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.
+ 34 |- !P t. (!x. x = t ==> P x) ==> $? P,
+ 35 |- !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.
+ 36 |- !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.
+ 37 |- !P f. RES_EXISTS P f <=> ?x. x IN P /\ f x,
+ 38 |- !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) ==>
+ 39 |- !P f. RES_FORALL P f <=> !x. x IN P ==> f x,
+ 40 |- !P Q. (?x. P x) /\ (!x. P x ==> Q x) ==> Q ($@ P),
+ 41 |- !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)) ==>
+ 42 |- !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') /\
+ 43 |- ~(t /\ ~t),
+ 44 |- (!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) /\
+ 45 |- (!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) /\
+ 46 |- (!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) /\
+ 47 |- (!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) /\
+ 48 |- (!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) /\
+ 49 |- (!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) /\
+ 50 |- (!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 =
+ 51 |- (!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) /\
+ 52 |- (!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)) /\
+ 53 |- (!t. ~~t <=> t) /\ (~T <=> F) /\ (~F <=> T),
+ 54 |- (!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) /\
+ 55 |- (!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) /\
+ 56 |- (!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) /\
+ 57 |- (!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) /\
+ 58 |- (!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) /\
+ 59 |- (!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,
+ 60 |- (T <> F) /\ (F <> T)
  61 |- Data_List_concat Data_List_nil = Data_List_nil /\
        !h t.
          Data_List_concat (Data_List_cons h t) =
@@ -747,21 +747,11 @@ val app_if = hd (amatch ``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 th32 = store_thm
+  ("th32", el 32 goals |> concl, MATCH_ACCEPT_TAC (GSYM ext));
 
 val o_def = hd(amatch``Function_o = _``);
 
@@ -772,8 +762,8 @@ 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,
+val th33 = store_thm
+  ("th33", el 33 goals |> concl,
   rpt gen_tac
   \\ CONV_TAC(HO_REWR_CONV ex_unique_thm)
   \\ PURE_REWRITE_TAC[o_def]
@@ -797,8 +787,8 @@ 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,
+val th34 = store_thm
+  ("th34", el 34 goals |> concl,
   PURE_REWRITE_TAC[forall_eq,ex_def]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ MATCH_ACCEPT_TAC select_ax);
@@ -813,8 +803,8 @@ val imp_all = hd(amatch``(_ ==> (!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,
+val th35 = store_thm
+  ("th35", el 35 goals |> concl,
   rpt gen_tac
   \\ PURE_REWRITE_TAC[and_all,all_and,all_imp,imp_all]
   \\ rpt conj_tac \\ REFL_TAC);
@@ -828,8 +818,8 @@ val ex_imp = hd(amatch``((?x. _) ==> _) <=> _``);
           ((?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,
+val th36 = store_thm
+  ("th36", el 36 goals |> concl,
   rpt gen_tac
   \\ PURE_REWRITE_TAC[and_ex,ex_and,ex_imp]
   \\ rpt conj_tac \\ REFL_TAC);
@@ -843,8 +833,8 @@ th40: |- !P f. RES_FORALL P f <=> !x. x IN P ==> f x
 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,
+val th40 = store_thm
+  ("th40", el 40 goals |> concl,
   PURE_REWRITE_TAC[ex_def]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt strip_tac
@@ -859,8 +849,8 @@ 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 th42 = store_thm
-  ("th42", el 42 goals |> concl,
+val th41 = store_thm
+  ("th41", el 41 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)
@@ -874,8 +864,8 @@ 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 th43 = store_thm
-  ("th43", el 43 goals |> concl,
+val th42 = store_thm
+  ("th42", el 42 goals |> concl,
   rpt strip_tac
   \\ match_mp_tac list_ind
   \\ conj_tac >- first_assum ACCEPT_TAC
@@ -883,8 +873,8 @@ val th43 = store_thm
   \\ first_assum MATCH_ACCEPT_TAC);
 
 (* |- ~(t /\ ~t) *)
-val th44 = store_thm
-  ("th44", el 44 goals |> concl,
+val th43 = store_thm
+  ("th43", el 43 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]);
@@ -895,8 +885,8 @@ 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,
+val th44 = store_thm
+  ("th44", el 44 goals |> concl,
     conj_tac
  >| [ MATCH_ACCEPT_TAC left_11,
       MATCH_ACCEPT_TAC right_11 ]);
@@ -907,8 +897,8 @@ val isNone_none = hd(amatch``Data_Option_isNone (Data_Option_none)``);
 (* |- (!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,
+val th45 = store_thm
+  ("th45", el 45 goals |> concl,
     conj_tac
  >| [ MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL isNone_some)),
       MATCH_ACCEPT_TAC (EQT_INTRO isNone_none) ]);
@@ -919,8 +909,8 @@ 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,
+val th46 = store_thm
+  ("th46", el 46 goals |> concl,
     conj_tac
  >| [ MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL isSome_some)),
       MATCH_ACCEPT_TAC (EQF_INTRO isSome_none) ]);
@@ -931,8 +921,8 @@ val isLeft_left = hd(amatch``Data_Sum_isLeft (Data_Sum_left _)``);
 (* |- (!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,
+val th47 = store_thm
+  ("th47", el 47 goals |> concl,
     conj_tac
  >| [ PURE_REWRITE_TAC [iff_T] >> MATCH_ACCEPT_TAC isLeft_left,
       PURE_REWRITE_TAC [iff_F] >> MATCH_ACCEPT_TAC isLeft_right ]);
@@ -943,8 +933,8 @@ val isRight_left = hd(amatch``Data_Sum_isRight (Data_Sum_left _)``);
 (* |- (!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,
+val th48 = store_thm
+  ("th48", el 48 goals |> concl,
     conj_tac
  >| [ PURE_REWRITE_TAC [iff_T] >> MATCH_ACCEPT_TAC isRight_right,
       PURE_REWRITE_TAC [iff_F] >> MATCH_ACCEPT_TAC isRight_left ]);
@@ -959,8 +949,8 @@ val append_cons =
           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,
+val th49 = store_thm
+  ("th49", el 49 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC append_nil
   \\ MATCH_ACCEPT_TAC append_cons);
 
@@ -972,8 +962,8 @@ val plus_comm = hd(amatch``Number_Natural_plus x y = Number_Natural_plus y x``);
       !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,
+val th50 = store_thm
+  ("th50", el 50 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));
 
@@ -985,8 +975,8 @@ val power_suc = hd(amatch``Number_Natural_power _ (Number_Natural_suc _)``);
       !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,
+val th51 = store_thm
+  ("th51", el 51 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC power_zero
   \\ MATCH_ACCEPT_TAC power_suc);
 
@@ -1000,19 +990,19 @@ val times_zero_comm = PURE_ONCE_REWRITE_RULE [times_comm] times_zero;
           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,
+val th52 = store_thm
+  ("th52", el 52 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)));
 
 (* |- (!t. ~~t <=> t) /\ (~T <=> F) /\ (~F <=> T) *)
-val th54 = store_thm
-  ("th54", el 54 goals |> concl,
+val th53 = store_thm
+  ("th53", el 53 goals |> concl,
   PURE_REWRITE_TAC[not_not,iff_F,iff_T,truth,not_F,and_T]
   \\ gen_tac \\ REFL_TAC);
 
-val NOT_CLAUSES = th54;
+val NOT_CLAUSES = th53;
 
 val map_none = hd(amatch``Data_Option_map _ Data_Option_none = _``)
 val map_some = hd(amatch``Data_Option_map _ (Data_Option_some _) = _``)
@@ -1020,8 +1010,8 @@ 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,
+val th54 = store_thm
+  ("th54", el 54 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC map_some
   \\ MATCH_ACCEPT_TAC map_none);
 
@@ -1033,8 +1023,8 @@ val map_cons = hd(amatch``Data_List_map _ (Data_List_cons _ _)``);
           Data_List_map f (Data_List_cons h t) =
           Data_List_cons (f h) (Data_List_map f t)
  *)
-val th56 = store_thm
-  ("th56", el 56 goals |> concl,
+val th55 = store_thm
+  ("th55", el 55 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC map_nil
   \\ MATCH_ACCEPT_TAC map_cons);
 
@@ -1053,8 +1043,8 @@ 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 th58 = store_thm
-  ("th58", el 58 goals |> concl,
+val th57 = store_thm
+  ("th57", el 57 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC filter_nil
   \\ MATCH_ACCEPT_TAC filter_cons);
 
@@ -1065,8 +1055,8 @@ val all_cons = hd(amatch``Data_List_all _ (Data_List_cons _ _)``);
       !P h t.
           Data_List_all P (Data_List_cons h t) <=> P h /\ Data_List_all 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 (EQT_INTRO (SPEC_ALL all_nil))
   \\ MATCH_ACCEPT_TAC all_cons);
 
@@ -1077,14 +1067,21 @@ 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 th60 = store_thm
-  ("th60", el 60 goals |> concl,
+val th59 = store_thm
+  ("th59", el 59 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL any_nil))
   \\ MATCH_ACCEPT_TAC any_cons);
 
 val concat_nil = hd(amatch``Data_List_concat Data_List_nil``);
 val concat_cons = hd(amatch``Data_List_concat (Data_List_cons _ _)``);
 
+(* |- (T <> F) /\ (F <> T) *)
+val th60 = store_thm
+  ("th60",  el 60 goals |> concl,
+  PURE_REWRITE_TAC[eq_imp_thm, not_and, imp_F, not_not]
+  \\ conj_tac >|[disj1_tac, disj2_tac]
+  \\ ACCEPT_TAC truth);
+
 (* |- Data_List_concat Data_List_nil = Data_List_nil /\
       !h t.
           Data_List_concat (Data_List_cons h t) =

From 4640431ba7d5b26dce8ef608bf1330ab2d2faf2e Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Mon, 16 Dec 2024 08:42:22 +0000
Subject: [PATCH 13/19] Remove unneeded inline proof about BITWISE /\ 0

---
 src/num/theories/cv_compute/automation/cv_primScript.sml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/num/theories/cv_compute/automation/cv_primScript.sml b/src/num/theories/cv_compute/automation/cv_primScript.sml
index 3df66869bc..eb7085391e 100644
--- a/src/num/theories/cv_compute/automation/cv_primScript.sml
+++ b/src/num/theories/cv_compute/automation/cv_primScript.sml
@@ -1239,9 +1239,6 @@ Proof
   \\ completeInduct_on ‘m’
   \\ simp [Once cv_word_and_loop_def]
   \\ Cases_on ‘m = 0’ \\ fs [wordsTheory.WORD_AND_CLAUSES]
-  >-
-   (qsuff_tac ‘!l n. BITWISE l $/\ 0 n = 0’ >- fs []
-    \\ Induct \\ fs [BITWISE])
   \\ gvs [PULL_FORALL,AND_IMP_INTRO] \\ rw []
   \\ Cases_on ‘l’ \\ gvs []
   \\ rename [‘n < 2 ** SUC l’]

From 6081abef0029f7c28da07b9baafa4dc3acb084e6 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Mon, 16 Dec 2024 16:20:12 +0000
Subject: [PATCH 14/19] Revert "Attempt to fix OpenTheory base vs HOL4"

This reverts commit 4e16bd3b331c521cff62afc5004a100fdf048368.
---
 src/boss/prove_base_assumsScript.sml | 173 ++++++++++++++-------------
 1 file changed, 88 insertions(+), 85 deletions(-)

diff --git a/src/boss/prove_base_assumsScript.sml b/src/boss/prove_base_assumsScript.sml
index 71d4be7806..3d4fded15b 100644
--- a/src/boss/prove_base_assumsScript.sml
+++ b/src/boss/prove_base_assumsScript.sml
@@ -222,80 +222,80 @@ val goals =
  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. f = g <=> !x. f x = g x,
- 33 |- !f g. ?!h.
+ 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,
- 34 |- !P t. (!x. x = t ==> P x) ==> $? P,
- 35 |- !P Q.
+ 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),
- 36 |- !P Q.
+ 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),
- 37 |- !P f. RES_EXISTS P f <=> ?x. x IN P /\ f x,
- 38 |- !P f.
+ 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,
- 39 |- !P f. RES_FORALL P f <=> !x. x IN P ==> f x,
- 40 |- !P Q. (?x. P x) /\ (!x. P x ==> Q x) ==> Q ($@ P),
- 41 |- !f. (!x y z. f x (f y z) = f (f x y) z) ==>
+ 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),
- 42 |- !P. P Data_List_nil /\ (!t. P t ==> !h. P (Data_List_cons h t)) ==>
+ 43 |- !P. P Data_List_nil /\ (!t. P t ==> !h. P (Data_List_cons h t)) ==>
            !l. P l,
- 43 |- ~(t /\ ~t),
- 44 |- (!x x'. Data_Sum_left x = Data_Sum_left x' <=> x = x') /\
+ 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',
- 45 |- (!x. Data_Option_isNone (Data_Option_some x) <=> F) /\
+ 46 |- (!x. Data_Option_isNone (Data_Option_some x) <=> F) /\
        (Data_Option_isNone Data_Option_none <=> T),
- 46 |- (!x. Data_Option_isSome (Data_Option_some x) <=> T) /\
+ 47 |- (!x. Data_Option_isSome (Data_Option_some x) <=> T) /\
        (Data_Option_isSome Data_Option_none <=> F),
- 47 |- (!x. Data_Sum_isLeft (Data_Sum_left x) <=> T) /\
+ 48 |- (!x. Data_Sum_isLeft (Data_Sum_left x) <=> T) /\
        !y. Data_Sum_isLeft (Data_Sum_right y) <=> F,
- 48 |- (!x. Data_Sum_isRight (Data_Sum_right x) <=> T) /\
+ 49 |- (!x. Data_Sum_isRight (Data_Sum_right x) <=> T) /\
        !y. Data_Sum_isRight (Data_Sum_left y) <=> F,
- 49 |- (!l. Data_List_append Data_List_nil l = l) /\
+ 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),
- 50 |- (!n. Number_Natural_plus Number_Natural_zero n = n) /\
+ 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),
- 51 |- (!m. Number_Natural_power m Number_Natural_zero =
+ 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),
- 52 |- (!n. Number_Natural_times Number_Natural_zero n = Number_Natural_zero) /\
+ 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,
- 53 |- (!t. ~~t <=> t) /\ (~T <=> F) /\ (~F <=> T),
- 54 |- (!f x. Data_Option_map f (Data_Option_some x) = Data_Option_some (f x)) /\
+ 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,
- 55 |- (!f. Data_List_map f Data_List_nil = Data_List_nil) /\
+ 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),
- 56 |- (!p m x. x IN p ==> RES_ABSTRACT p m x = m x) /\
+ 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,
- 57 |- (!P. Data_List_filter P Data_List_nil = Data_List_nil) /\
+ 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,
- 58 |- (!P. Data_List_all P Data_List_nil <=> 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,
- 59 |- (!P. Data_List_any P Data_List_nil <=> F) /\
+ 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,
- 60 |- (T <> F) /\ (F <> T)
  61 |- Data_List_concat Data_List_nil = Data_List_nil /\
        !h t.
          Data_List_concat (Data_List_cons h t) =
@@ -747,11 +747,21 @@ val app_if = hd (amatch ``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 th32 = store_thm
-  ("th32", el 32 goals |> concl, MATCH_ACCEPT_TAC (GSYM ext));
+val th33 = store_thm
+  ("th33", el 33 goals |> concl, MATCH_ACCEPT_TAC (GSYM ext));
 
 val o_def = hd(amatch``Function_o = _``);
 
@@ -762,8 +772,8 @@ 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 th33 = store_thm
-  ("th33", el 33 goals |> concl,
+val th34 = store_thm
+  ("th34", el 34 goals |> concl,
   rpt gen_tac
   \\ CONV_TAC(HO_REWR_CONV ex_unique_thm)
   \\ PURE_REWRITE_TAC[o_def]
@@ -787,8 +797,8 @@ val ex_def = hd(amatch``$? = _``);
 val select_ax = hd(amatch ``p t ==> p ($@ p)``);
 
 (* |- !P t. (!x. x = t ==> P x) ==> $? P *)
-val th34 = store_thm
-  ("th34", el 34 goals |> concl,
+val th35 = store_thm
+  ("th35", el 35 goals |> concl,
   PURE_REWRITE_TAC[forall_eq,ex_def]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ MATCH_ACCEPT_TAC select_ax);
@@ -803,8 +813,8 @@ val imp_all = hd(amatch``(_ ==> (!x. _)) <=> _``);
           ((!x. P x) /\ Q <=> !x. P x /\ Q) /\
           (Q /\ (!x. P x) <=> !x. Q /\ P x)
  *)
-val th35 = store_thm
-  ("th35", el 35 goals |> concl,
+val th36 = store_thm
+  ("th36", el 36 goals |> concl,
   rpt gen_tac
   \\ PURE_REWRITE_TAC[and_all,all_and,all_imp,imp_all]
   \\ rpt conj_tac \\ REFL_TAC);
@@ -818,8 +828,8 @@ val ex_imp = hd(amatch``((?x. _) ==> _) <=> _``);
           ((?x. P x) /\ Q <=> ?x. P x /\ Q) /\
           (Q /\ (?x. P x) <=> ?y. Q /\ P y)
  *)
-val th36 = store_thm
-  ("th36", el 36 goals |> concl,
+val th37 = store_thm
+  ("th37", el 37 goals |> concl,
   rpt gen_tac
   \\ PURE_REWRITE_TAC[and_ex,ex_and,ex_imp]
   \\ rpt conj_tac \\ REFL_TAC);
@@ -833,8 +843,8 @@ th40: |- !P f. RES_FORALL P f <=> !x. x IN P ==> f x
 val eta_ax = hd(amatch``!f. (\x. f x) = f``);
 
 (* |- !P Q. (?x. P x) /\ (!x. P x ==> Q x) ==> Q ($@ P) *)
-val th40 = store_thm
-  ("th40", el 40 goals |> concl,
+val th41 = store_thm
+  ("th41", el 41 goals |> concl,
   PURE_REWRITE_TAC[ex_def]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt strip_tac
@@ -849,8 +859,8 @@ 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 th41 = store_thm
-  ("th41", el 41 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)
@@ -864,8 +874,8 @@ 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 th42 = store_thm
-  ("th42", el 42 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
@@ -873,8 +883,8 @@ val th42 = store_thm
   \\ first_assum MATCH_ACCEPT_TAC);
 
 (* |- ~(t /\ ~t) *)
-val th43 = store_thm
-  ("th43", el 43 goals |> concl,
+val th44 = store_thm
+  ("th44", el 44 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]);
@@ -885,8 +895,8 @@ 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 th44 = store_thm
-  ("th44", el 44 goals |> concl,
+val th45 = store_thm
+  ("th45", el 45 goals |> concl,
     conj_tac
  >| [ MATCH_ACCEPT_TAC left_11,
       MATCH_ACCEPT_TAC right_11 ]);
@@ -897,8 +907,8 @@ val isNone_none = hd(amatch``Data_Option_isNone (Data_Option_none)``);
 (* |- (!x. Data_Option_isNone (Data_Option_some x) <=> F) /\
       (Data_Option_isNone Data_Option_none <=> T)
  *)
-val th45 = store_thm
-  ("th45", el 45 goals |> concl,
+val th46 = store_thm
+  ("th46", el 46 goals |> concl,
     conj_tac
  >| [ MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL isNone_some)),
       MATCH_ACCEPT_TAC (EQT_INTRO isNone_none) ]);
@@ -909,8 +919,8 @@ 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 th46 = store_thm
-  ("th46", el 46 goals |> concl,
+val th47 = store_thm
+  ("th47", el 47 goals |> concl,
     conj_tac
  >| [ MATCH_ACCEPT_TAC (EQT_INTRO (SPEC_ALL isSome_some)),
       MATCH_ACCEPT_TAC (EQF_INTRO isSome_none) ]);
@@ -921,8 +931,8 @@ val isLeft_left = hd(amatch``Data_Sum_isLeft (Data_Sum_left _)``);
 (* |- (!x. Data_Sum_isLeft (Data_Sum_left x) <=> T) /\
       !y. Data_Sum_isLeft (Data_Sum_right y) <=> F
  *)
-val th47 = store_thm
-  ("th47", el 47 goals |> concl,
+val th48 = store_thm
+  ("th48", el 48 goals |> concl,
     conj_tac
  >| [ PURE_REWRITE_TAC [iff_T] >> MATCH_ACCEPT_TAC isLeft_left,
       PURE_REWRITE_TAC [iff_F] >> MATCH_ACCEPT_TAC isLeft_right ]);
@@ -933,8 +943,8 @@ val isRight_left = hd(amatch``Data_Sum_isRight (Data_Sum_left _)``);
 (* |- (!x. Data_Sum_isRight (Data_Sum_right x)) /\
       !y. ~Data_Sum_isRight (Data_Sum_left y)
  *)
-val th48 = store_thm
-  ("th48", el 48 goals |> concl,
+val th49 = store_thm
+  ("th49", el 49 goals |> concl,
     conj_tac
  >| [ PURE_REWRITE_TAC [iff_T] >> MATCH_ACCEPT_TAC isRight_right,
       PURE_REWRITE_TAC [iff_F] >> MATCH_ACCEPT_TAC isRight_left ]);
@@ -949,8 +959,8 @@ val append_cons =
           Data_List_append (Data_List_cons h l1) l2 =
           Data_List_cons h (Data_List_append l1 l2)
  *)
-val th49 = store_thm
-  ("th49", el 49 goals |> concl,
+val th50 = store_thm
+  ("th50", el 50 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC append_nil
   \\ MATCH_ACCEPT_TAC append_cons);
 
@@ -962,8 +972,8 @@ val plus_comm = hd(amatch``Number_Natural_plus x y = Number_Natural_plus y x``);
       !m n. Number_Natural_plus (Number_Natural_suc m) n =
             Number_Natural_suc (Number_Natural_plus m n)
  *)
-val th50 = store_thm
-  ("th50", el 50 goals |> concl,
+val th51 = store_thm
+  ("th51", el 51 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));
 
@@ -975,8 +985,8 @@ val power_suc = hd(amatch``Number_Natural_power _ (Number_Natural_suc _)``);
       !m n. Number_Natural_power m (Number_Natural_suc n) =
             Number_Natural_times m (Number_Natural_power m n)
  *)
-val th51 = store_thm
-  ("th51", el 51 goals |> concl,
+val th52 = store_thm
+  ("th52", el 52 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC power_zero
   \\ MATCH_ACCEPT_TAC power_suc);
 
@@ -990,19 +1000,19 @@ val times_zero_comm = PURE_ONCE_REWRITE_RULE [times_comm] times_zero;
           Number_Natural_times (Number_Natural_suc m) n =
           Number_Natural_plus (Number_Natural_times m n) n
  *)
-val th52 = store_thm
-  ("th52", el 52 goals |> concl,
+val th53 = store_thm
+  ("th53", el 53 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)));
 
 (* |- (!t. ~~t <=> t) /\ (~T <=> F) /\ (~F <=> T) *)
-val th53 = store_thm
-  ("th53", el 53 goals |> concl,
+val th54 = store_thm
+  ("th54", el 54 goals |> concl,
   PURE_REWRITE_TAC[not_not,iff_F,iff_T,truth,not_F,and_T]
   \\ gen_tac \\ REFL_TAC);
 
-val NOT_CLAUSES = th53;
+val NOT_CLAUSES = th54;
 
 val map_none = hd(amatch``Data_Option_map _ Data_Option_none = _``)
 val map_some = hd(amatch``Data_Option_map _ (Data_Option_some _) = _``)
@@ -1010,8 +1020,8 @@ 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 th54 = store_thm
-  ("th54", el 54 goals |> concl,
+val th55 = store_thm
+  ("th55", el 55 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC map_some
   \\ MATCH_ACCEPT_TAC map_none);
 
@@ -1023,8 +1033,8 @@ val map_cons = hd(amatch``Data_List_map _ (Data_List_cons _ _)``);
           Data_List_map f (Data_List_cons h t) =
           Data_List_cons (f h) (Data_List_map f t)
  *)
-val th55 = store_thm
-  ("th55", el 55 goals |> concl,
+val th56 = store_thm
+  ("th56", el 56 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC map_nil
   \\ MATCH_ACCEPT_TAC map_cons);
 
@@ -1043,8 +1053,8 @@ 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 th57 = store_thm
-  ("th57", el 57 goals |> concl,
+val th58 = store_thm
+  ("th58", el 58 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC filter_nil
   \\ MATCH_ACCEPT_TAC filter_cons);
 
@@ -1055,8 +1065,8 @@ val all_cons = hd(amatch``Data_List_all _ (Data_List_cons _ _)``);
       !P h t.
           Data_List_all P (Data_List_cons h t) <=> P h /\ Data_List_all P t
  *)
-val th58 = store_thm
-  ("th58", el 58 goals |> concl,
+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);
 
@@ -1067,21 +1077,14 @@ 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 th59 = store_thm
-  ("th59", el 59 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 concat_nil = hd(amatch``Data_List_concat Data_List_nil``);
 val concat_cons = hd(amatch``Data_List_concat (Data_List_cons _ _)``);
 
-(* |- (T <> F) /\ (F <> T) *)
-val th60 = store_thm
-  ("th60",  el 60 goals |> concl,
-  PURE_REWRITE_TAC[eq_imp_thm, not_and, imp_F, not_not]
-  \\ conj_tac >|[disj1_tac, disj2_tac]
-  \\ ACCEPT_TAC truth);
-
 (* |- Data_List_concat Data_List_nil = Data_List_nil /\
       !h t.
           Data_List_concat (Data_List_cons h t) =

From f7257e64972903c06f70a3339b35926eed169562 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Tue, 17 Dec 2024 21:18:17 +0000
Subject: [PATCH 15/19] Prove a new opentheory bridge assumption

---
 src/boss/prove_base_assumsScript.sml | 226 ++++++++++++++-------------
 1 file changed, 117 insertions(+), 109 deletions(-)

diff --git a/src/boss/prove_base_assumsScript.sml b/src/boss/prove_base_assumsScript.sml
index 3d4fded15b..becf3079c7 100644
--- a/src/boss/prove_base_assumsScript.sml
+++ b/src/boss/prove_base_assumsScript.sml
@@ -296,16 +296,17 @@ val goals =
  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 /\
+ 61 |- (T <> F) /\ (F <> T)
+ 62 |- 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 /\
+ 63 |- 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 =
+ 64 |- 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) =
@@ -314,59 +315,59 @@ val goals =
               (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 /\
+ 65 |- 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 =
+ 66 |- 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) /\
+ 67 |- (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) /\
+ 68 |- (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) /\
+ 69 |- (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 =
+ 70 |- Data_Unit_unit = @x. T,
+ 71 |- Number_Natural_zero = Number_Natural_zero,
+ 72 |- (?!x. F) <=> F,
+ 73 |- Data_Pair_comma x y = Data_Pair_comma a b <=> x = a /\ y = b,
+ 74 |- Data_Sum_left x = Data_Sum_left y <=> x = y,
+ 75 |- Data_Sum_right x = Data_Sum_right y <=> x = y,
+ 76 |- Function_id = Function_Combinator_s Function_const Function_const,
+ 77 |- Relation_empty = (\x y. F),
+ 78 |- Relation_universe = (\x y. T),
+ 79 |- 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 =
+ 80 |- Number_Natural_max = (\m n. if Number_Natural_less m n then n else m),
+ 81 |- Number_Natural_min = (\m n. if Number_Natural_less m n then m else n),
+ 82 |- Number_Natural_greater = (\m n. Number_Natural_less n m),
+ 83 |- Number_Natural_greatereq = (\m n. Number_Natural_greater m n \/ m = n),
+ 84 |- 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 =
+ 85 |- Number_Natural_lesseq = (\m n. Number_Natural_less m n \/ m = n),
+ 86 |- Relation_irreflexive = (\R. !x. ~R x x),
+ 87 |- Relation_reflexive = (\R. !x. R x x),
+ 88 |- Relation_transitive = (\R. !x y z. R x y /\ R y z ==> R x z),
+ 89 |- Relation_wellFounded =
        (\R. !B. (?w. B w) ==> ?min. B min /\ !b. R b min ==> ~B b),
- 89 |- Relation_transitiveClosure =
+ 90 |- 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
+ 91 |- Relation_subrelation = (\R1 R2. !x y. R1 x y ==> R2 x y),
+ 92 |- Relation_intersect = (\R1 R2 x y. R1 x y /\ R2 x y),
+ 93 |- Relation_union = (\R1 R2 x y. R1 x y \/ R2 x y),
+ 94 |- Function_o = (\f g x. f (g x)),
+ 95 |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x,
+ 96 |- (x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w,
+ 97 |- (x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w]: thm list
  *)
 
 val bool_cases = hd(amatch``(x = T) \/ _``);
@@ -1085,13 +1086,20 @@ val th60 = store_thm
 val concat_nil = hd(amatch``Data_List_concat Data_List_nil``);
 val concat_cons = hd(amatch``Data_List_concat (Data_List_cons _ _)``);
 
+(* |- (T <> F) /\ (F <> T) *)
+val th61 = store_thm
+  ("th61",  el 61 goals |> concl,
+  PURE_REWRITE_TAC[eq_imp_thm, not_and, imp_F, not_not]
+  \\ conj_tac >|[disj1_tac, disj2_tac]
+  \\ ACCEPT_TAC truth);
+
 (* |- 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,
+val th62 = store_thm
+  ("th62", el 62 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC concat_nil
   \\ MATCH_ACCEPT_TAC concat_cons);
 
@@ -1104,8 +1112,8 @@ val reverse_cons = hd(amatch``Data_List_reverse (Data_List_cons _ _)``);
           Data_List_append (Data_List_reverse t)
             (Data_List_cons h Data_List_nil)
  *)
-val th62 = store_thm
-  ("th62", el 62 goals |> concl,
+val th63 = store_thm
+  ("th63", el 63 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC reverse_nil
   \\ MATCH_ACCEPT_TAC reverse_cons);
 
@@ -1123,8 +1131,8 @@ val unzip_cons = hd(amatch``Data_List_unzip (Data_List_cons _ _)``);
             (Data_List_cons (Data_Pair_snd x)
                (Data_Pair_snd (Data_List_unzip l)))
  *)
-val th63 = store_thm
-  ("th63", el 63 goals |> concl,
+val th64 = store_thm
+  ("th64", el 64 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC unzip_nil
   \\ PURE_REWRITE_TAC[unzip_cons]
   \\ rpt gen_tac
@@ -1139,8 +1147,8 @@ val length_cons = hd(amatch``Data_List_length (Data_List_cons _ _)``);
           Data_List_length (Data_List_cons h t) =
           Number_Natural_suc (Data_List_length t)
  *)
-val th64 = store_thm
-  ("th64", el 64 goals |> concl,
+val th65 = store_thm
+  ("th65", el 65 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC length_nil
   \\ MATCH_ACCEPT_TAC length_cons);
 
@@ -1154,8 +1162,8 @@ val fact_suc = hd(amatch``Number_Natural_factorial (Number_Natural_suc _)``);
           Number_Natural_times (Number_Natural_suc n)
             (Number_Natural_factorial n)
  *)
-val th65 = store_thm
-  ("th65", el 65 goals |> concl,
+val th66 = store_thm
+  ("th66", el 66 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC fact_zero
   \\ MATCH_ACCEPT_TAC fact_suc);
 
@@ -1165,8 +1173,8 @@ val null_cons = hd(amatch``Data_List_null (Data_List_cons _ _)``);
 (* |- (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,
+val th67 = store_thm
+  ("th67", el 67 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO null_nil)
   \\ MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL null_cons)));
 
@@ -1176,8 +1184,8 @@ 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,
+val th68 = store_thm
+  ("th68", el 68 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO even_nil)
   \\ MATCH_ACCEPT_TAC even_cons);
 
@@ -1187,28 +1195,28 @@ val odd_cons = hd(amatch``Number_Natural_odd (Number_Natural_suc _)``);
 (* |- (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,
+val th69 = store_thm
+  ("th69", el 69 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO odd_nil)
   \\ MATCH_ACCEPT_TAC odd_cons);
 
 val one_thm = hd(amatch``_ = Data_Unit_unit``);
 
 (* |- Data_Unit_unit = @x. T *)
-val th69 = store_thm
-  ("th69", el 69 goals |> concl,
+val th70 = store_thm
+  ("th70", el 70 goals |> concl,
   PURE_ONCE_REWRITE_TAC[one_thm] \\ REFL_TAC);
 
 (* |- Number_Natural_zero = Number_Natural_zero *)
-val th70 = store_thm
-  ("th70", el 70 goals |> concl,
+val th71 = store_thm
+  ("th71", el 71 goals |> concl,
   REFL_TAC);
 
 val exists_simp = hd(amatch “(?x. t) <=> t”);
 
 (* |- (?!x. F) <=> F *)
-val th71 = store_thm
-  ("th71", el 71 goals |> concl,
+val th72 = store_thm
+  ("th72", el 72 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);
@@ -1216,32 +1224,32 @@ val th71 = store_thm
 val comma_11 = hd(amatch``Data_Pair_comma _ _ = Data_Pair_comma _ _``);
 
 (* |- Data_Pair_comma x y = Data_Pair_comma a b <=> x = a /\ y = b *)
-val th72 = store_thm
-  ("th72", el 72 goals |> concl,
+val th73 = store_thm
+  ("th73", el 73 goals |> concl,
   MATCH_ACCEPT_TAC comma_11);
 
 (* |- Data_Sum_left x = Data_Sum_left y <=> x = y *)
-val th73 = store_thm
-  ("th73", el 73 goals |> concl,
+val th74 = store_thm
+  ("th74", el 74 goals |> concl,
   MATCH_ACCEPT_TAC left_11);
 
 (* |- Data_Sum_right x = Data_Sum_right y <=> x = y *)
-val th74 = store_thm
-  ("th74", el 74 goals |> concl,
+val th75 = store_thm
+  ("th75", el 75 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,
+val th76 = store_thm
+  ("th76", el 76 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,
+val th77 = store_thm
+  ("th77", el 77 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);
@@ -1249,8 +1257,8 @@ val th76 = store_thm
 val universe_thm = hd(amatch``Relation_universe _ _``);
 
 (* |- Relation_universe = (\x y. T) *)
-val th77 = store_thm
-  ("th77", el 77 goals |> concl,
+val th78 = store_thm
+  ("th78", el 78 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);
@@ -1271,8 +1279,8 @@ val num_less_ind = hd(amatch``(!x. _ ==> _) ==> !n. P (n:Number_Natural_natural)
            Number_Natural_plus n
              (Number_Natural_plus n (Number_Natural_suc Number_Natural_zero)))
  *)
-val th78 = store_thm
-  ("th78", el 78 goals |> concl,
+val th79 = store_thm
+  ("th79", el 79 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,bit1_thm,plus_suc]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ gen_tac
@@ -1291,8 +1299,8 @@ 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,
+val th80 = store_thm
+  ("th80", el 80 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,max_thm,less_or_eq]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac
@@ -1307,8 +1315,8 @@ val th79 = store_thm
 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,
+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
@@ -1323,8 +1331,8 @@ val th80 = store_thm
 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,
+val th82 = store_thm
+  ("th82", el 82 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,greater_thm]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1332,8 +1340,8 @@ val th81 = store_thm
 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,
+val th83 = store_thm
+  ("th83", el 83 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
@@ -1361,8 +1369,8 @@ val F_IMP2 = store_thm
 (* |- Number_Natural_less =
       (\m n. ?P. (!n. P (Number_Natural_suc n) ==> P n) /\ P m /\ ~P n)
  *)
-val th83 = store_thm
-  ("th83", el 83 goals |> concl,
+val th84 = store_thm
+  ("th84", el 84 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm]
   \\ qx_genl_tac[`a`,`b`]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
@@ -1421,8 +1429,8 @@ val th83 = store_thm
   \\ PURE_REWRITE_TAC[F_imp]);
 
 (* |- Number_Natural_lesseq = (\m n. Number_Natural_less m n \/ m = n) *)
-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,less_or_eq]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1430,8 +1438,8 @@ val th84 = store_thm
 val irreflexive_thm = hd(amatch``Relation_irreflexive _ = _``);
 
 (* |- Relation_irreflexive = (\R. !x. ~R x x) *)
-val th85 = store_thm
-  ("th85", el 85 goals |> concl,
+val th86 = store_thm
+  ("th86", el 86 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm, irreflexive_thm]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac
@@ -1440,8 +1448,8 @@ val th85 = store_thm
 val reflexive_thm = hd(amatch``Relation_reflexive _ = _``);
 
 (* |- Relation_reflexive = (\R. !x. R x x) *)
-val th86 = store_thm
-  ("th86", el 86 goals |> concl,
+val th87 = store_thm
+  ("th87", el 87 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm, reflexive_thm]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1449,8 +1457,8 @@ val th86 = store_thm
 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,
+val th88 = store_thm
+  ("th88", el 88 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,transitive_thm]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ gen_tac \\ REFL_TAC);
@@ -1460,8 +1468,8 @@ val wellFounded_thm = hd(amatch``Relation_wellFounded r <=> !p. (?x. _) ==> _``)
 (* |- 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,
+val th89 = store_thm
+  ("th89", el 89 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm]
   \\ PURE_REWRITE_TAC[wellFounded_thm]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
@@ -1477,8 +1485,8 @@ val subrelation_thm  = hd(amatch``Relation_subrelation x s <=> !x y. _``);
            !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,
+val th90 = store_thm
+  ("th90", el 90 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm]
   \\ PURE_REWRITE_TAC[tc_def,bigIntersect_thm,mem_fromPred]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
@@ -1491,8 +1499,8 @@ val th89 = store_thm
   \\ REFL_TAC);
 
 (* |- Relation_subrelation = (\R1 R2. !x y. R1 x y ==> R2 x y) *)
-val th90 = store_thm
-  ("th90", el 90 goals |> concl,
+val th91 = store_thm
+  ("th91", el 91 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,subrelation_thm]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1505,15 +1513,15 @@ 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,
+val th92 = store_thm
+  ("th92", el 92 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);
 
 (* |- Relation_union = (\R1 R2 x y. R1 x y \/ R2 x y) *)
-val th92 = store_thm
-  ("th92", el 92 goals |> concl,
+val th93 = store_thm
+  ("th93", el 93 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);
@@ -1521,15 +1529,15 @@ val th92 = store_thm
 val o_thm = hd(amatch``(Function_o _ _) _ = _``);
 
 (* |- Function_o = (\f g x. f (g x)) *)
-val th93 = store_thm
-  ("th93", el 93 goals |> concl,
+val th94 = store_thm
+  ("th94", el 94 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,o_thm]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
 
 (* |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x'. Q x' *)
-val th94 = store_thm
-  ("th94", el 94 goals |> concl,
+val th95 = store_thm
+  ("th95", el 95 goals |> concl,
   rpt strip_tac
   \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
   \\ qexists_tac`x`
@@ -1544,16 +1552,16 @@ val th94' = store_thm
  *)
 
 (* |- (x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w *)
-val th95 = store_thm
-  ("th95", el 95 goals |> concl,
+val th96 = store_thm
+  ("th96", el 96 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);
 
 (* |- (x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w *)
-val th96 = store_thm
-  ("th96", el 96 goals |> concl,
+val th97 = store_thm
+  ("th97", el 97 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)
@@ -1590,7 +1598,7 @@ val th89 = store_thm
  *)
 
 (* Now raise an error if the above th96 is not the last one *)
-val _ = if List.length goals <> 96 then
+val _ = if List.length goals <> 97 then
             (raise ERR "-" "assumptions changed")
         else ();
 

From b9dead17aa52b0ed17c5aa6897fb9ce1f775fe88 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 18 Dec 2024 08:17:02 +0000
Subject: [PATCH 16/19] Remove redundant proof of BOOL_EQ_DISTINCT

---
 src/boss/prove_base_assumsScript.sml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/boss/prove_base_assumsScript.sml b/src/boss/prove_base_assumsScript.sml
index becf3079c7..773521713f 100644
--- a/src/boss/prove_base_assumsScript.sml
+++ b/src/boss/prove_base_assumsScript.sml
@@ -1089,9 +1089,7 @@ val concat_cons = hd(amatch``Data_List_concat (Data_List_cons _ _)``);
 (* |- (T <> F) /\ (F <> T) *)
 val th61 = store_thm
   ("th61",  el 61 goals |> concl,
-  PURE_REWRITE_TAC[eq_imp_thm, not_and, imp_F, not_not]
-  \\ conj_tac >|[disj1_tac, disj2_tac]
-  \\ ACCEPT_TAC truth);
+  PURE_REWRITE_TAC[iff_F,not_not,iff_T,not_F,and_T]);
 
 (* |- Data_List_concat Data_List_nil = Data_List_nil /\
       !h t.
@@ -1637,8 +1635,7 @@ val LET_RAND = store_thm("LET_RAND", concl boolTheory.LET_RAND,
   \\ REFL_TAC)
 
 (* |- (T <=/=> F) /\ (F <=/=> T) *)
-val BOOL_EQ_DISTINCT = store_thm("BOOL_EQ_DISTINCT", concl boolTheory.BOOL_EQ_DISTINCT,
-  PURE_REWRITE_TAC[iff_F,not_not,iff_T,not_F,and_T]);
+val BOOL_EQ_DISTINCT = th61;
 
 (* |- (!t1 t2. (if T then t1 else t2) = t1) /\
       !t1 t2. (if F then t1 else t2) = t2

From 00b7c1dacd59a9af419125d913b00e4d1457e297 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 18 Dec 2024 08:18:35 +0000
Subject: [PATCH 17/19] Make chunks_length a simp

---
 src/list/src/rich_listScript.sml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
index 08638478e9..6a3de4d876 100644
--- a/src/list/src/rich_listScript.sml
+++ b/src/list/src/rich_listScript.sml
@@ -3217,7 +3217,7 @@ Proof
   \\ simp[]
 QED
 
-Theorem chunks_length:
+Theorem chunks_length[simp]:
   chunks (LENGTH ls) ls = [ls]
 Proof
   rw[Once chunks_def]

From 4d1168d952d9bdfcf1f37298ac1f4bd66caaef9e Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 18 Dec 2024 08:20:33 +0000
Subject: [PATCH 18/19] Reorient l2n_2_neg

---
 src/list/src/numposrepScript.sml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/list/src/numposrepScript.sml b/src/list/src/numposrepScript.sml
index 773f7b2b8d..86277ec52f 100644
--- a/src/list/src/numposrepScript.sml
+++ b/src/list/src/numposrepScript.sml
@@ -441,7 +441,7 @@ QED
 Theorem l2n_2_neg:
   !ls.
   EVERY ($> 2) ls ==>
-  2 ** LENGTH ls - SUC (l2n 2 ls) = l2n 2 (MAP (\x. 1 - x) ls)
+  l2n 2 (MAP (\x. 1 - x) ls) = 2 ** LENGTH ls - SUC (l2n 2 ls)
 Proof
   Induct
   \\ rw[l2n_def]

From 8274f79967e22f72947de4d5130fd661860ee3f9 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 18 Dec 2024 08:51:45 +0000
Subject: [PATCH 19/19] Fix proof after reorienting statement

---
 src/list/src/numposrepScript.sml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/list/src/numposrepScript.sml b/src/list/src/numposrepScript.sml
index 86277ec52f..2b5d8bcff3 100644
--- a/src/list/src/numposrepScript.sml
+++ b/src/list/src/numposrepScript.sml
@@ -446,7 +446,6 @@ Proof
   Induct
   \\ rw[l2n_def]
   \\ fs[EXP, ADD1]
-  \\ first_x_assum(CHANGED_TAC o SUBST1_TAC o SYM)
   \\ simp[LEFT_SUB_DISTRIB, LEFT_ADD_DISTRIB, SUB_RIGHT_ADD]
   \\ Q.SPECL_THEN[`ls`,`2`]mp_tac l2n_lt
   \\ simp[]