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()