src/ZF/Integ/Bin.thy
 changeset 13560 d9651081578b parent 12182 3f820a21dcc1 child 13612 55d32e76ef4e
```--- a/src/ZF/Integ/Bin.thy	Thu Sep 05 14:03:03 2002 +0200
+++ b/src/ZF/Integ/Bin.thy	Sat Sep 07 22:04:28 2002 +0200
@@ -3,8 +3,6 @@
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

-Arithmetic on binary integers.
-
The sign Pls stands for an infinite string of leading 0's.
The sign Min stands for an infinite string of leading 1's.

@@ -16,7 +14,9 @@
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
*)

-Bin = Int + Datatype +
+
+theory Bin = Int + Datatype:

consts  bin :: i
datatype
@@ -25,55 +25,54 @@
| Bit ("w: bin", "b: bool")	(infixl "BIT" 90)

syntax
-  "_Int"           :: xnum => i        ("_")
+  "_Int"    :: "xnum => i"        ("_")

consts
-  integ_of  :: i=>i
-  NCons     :: [i,i]=>i
-  bin_succ  :: i=>i
-  bin_pred  :: i=>i
-  bin_minus :: i=>i
-  bin_mult  :: [i,i]=>i
+  integ_of  :: "i=>i"
+  NCons     :: "[i,i]=>i"
+  bin_succ  :: "i=>i"
+  bin_pred  :: "i=>i"
+  bin_minus :: "i=>i"
+  bin_mult  :: "[i,i]=>i"

primrec
-  integ_of_Pls  "integ_of (Pls)     = \$# 0"
-  integ_of_Min  "integ_of (Min)     = \$-(\$#1)"
-  integ_of_BIT  "integ_of (w BIT b) = \$#b \$+ integ_of(w) \$+ integ_of(w)"
+  integ_of_Pls:  "integ_of (Pls)     = \$# 0"
+  integ_of_Min:  "integ_of (Min)     = \$-(\$#1)"
+  integ_of_BIT:  "integ_of (w BIT b) = \$#b \$+ integ_of(w) \$+ integ_of(w)"

(** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)

-  NCons_Pls "NCons (Pls,b)     = cond(b,Pls BIT b,Pls)"
-  NCons_Min "NCons (Min,b)     = cond(b,Min,Min BIT b)"
-  NCons_BIT "NCons (w BIT c,b) = w BIT c BIT b"
+  NCons_Pls: "NCons (Pls,b)     = cond(b,Pls BIT b,Pls)"
+  NCons_Min: "NCons (Min,b)     = cond(b,Min,Min BIT b)"
+  NCons_BIT: "NCons (w BIT c,b) = w BIT c BIT b"

primrec (*successor.  If a BIT, can change a 0 to a 1 without recursion.*)
-  bin_succ_Pls  "bin_succ (Pls)     = Pls BIT 1"
-  bin_succ_Min  "bin_succ (Min)     = Pls"
-  bin_succ_BIT  "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
+  bin_succ_Pls:  "bin_succ (Pls)     = Pls BIT 1"
+  bin_succ_Min:  "bin_succ (Min)     = Pls"
+  bin_succ_BIT:  "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"

primrec (*predecessor*)
-  bin_pred_Pls  "bin_pred (Pls)     = Min"
-  bin_pred_Min  "bin_pred (Min)     = Min BIT 0"
-  bin_pred_BIT  "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
+  bin_pred_Pls:  "bin_pred (Pls)     = Min"
+  bin_pred_Min:  "bin_pred (Min)     = Min BIT 0"
+  bin_pred_BIT:  "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"

primrec (*unary negation*)
-  bin_minus_Pls
+  bin_minus_Pls:
"bin_minus (Pls)       = Pls"
-  bin_minus_Min
+  bin_minus_Min:
"bin_minus (Min)       = Pls BIT 1"
-  bin_minus_BIT
+  bin_minus_BIT:
"bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
bin_minus(w) BIT 0)"

primrec (*sum*)
"bin_adder (Pls)     = (lam w:bin. w)"
"bin_adder (Min)     = (lam w:bin. bin_pred(w))"
(lam w:bin.
bin_case (v BIT x, bin_pred(v BIT x),
@@ -89,19 +88,610 @@
x xor y)"
*)

-defs
+constdefs

primrec
-  bin_mult_Pls
+  bin_mult_Pls:
"bin_mult (Pls,w)     = Pls"
-  bin_mult_Min
+  bin_mult_Min:
"bin_mult (Min,w)     = bin_minus(w)"
-  bin_mult_BIT
+  bin_mult_BIT:
"bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
NCons(bin_mult(v,w),0))"

setup NumeralSyntax.setup

+
+declare bin.intros [simp,TC]
+
+lemma NCons_Pls_0: "NCons(Pls,0) = Pls"
+by simp
+
+lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1"
+by simp
+
+lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0"
+by simp
+
+lemma NCons_Min_1: "NCons(Min,1) = Min"
+by simp
+
+lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b"
+
+lemmas NCons_simps [simp] =
+    NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
+
+
+
+(** Type checking **)
+
+lemma integ_of_type [TC]: "w: bin ==> integ_of(w) : int"
+apply (induct_tac "w")
+done
+
+lemma NCons_type [TC]: "[| w: bin; b: bool |] ==> NCons(w,b) : bin"
+by (induct_tac "w", auto)
+
+lemma bin_succ_type [TC]: "w: bin ==> bin_succ(w) : bin"
+by (induct_tac "w", auto)
+
+lemma bin_pred_type [TC]: "w: bin ==> bin_pred(w) : bin"
+by (induct_tac "w", auto)
+
+lemma bin_minus_type [TC]: "w: bin ==> bin_minus(w) : bin"
+by (induct_tac "w", auto)
+
+(*This proof is complicated by the mutual recursion*)
+     "v: bin ==> ALL w: bin. bin_add(v,w) : bin"
+apply (induct_tac "v")
+apply (rule_tac [3] ballI)
+apply (rename_tac [3] "w'")
+apply (induct_tac [3] "w'")
+done
+
+lemma bin_mult_type [TC]: "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin"
+by (induct_tac "v", auto)
+
+
+subsubsection{*The Carry and Borrow Functions,
+            @{term bin_succ} and @{term bin_pred}*}
+
+(*NCons preserves the integer value of its argument*)
+lemma integ_of_NCons [simp]:
+     "[| w: bin; b: bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)"
+apply (erule bin.cases)
+apply (auto elim!: boolE)
+done
+
+lemma integ_of_succ [simp]:
+     "w: bin ==> integ_of(bin_succ(w)) = \$#1 \$+ integ_of(w)"
+apply (erule bin.induct)
+done
+
+lemma integ_of_pred [simp]:
+     "w: bin ==> integ_of(bin_pred(w)) = \$- (\$#1) \$+ integ_of(w)"
+apply (erule bin.induct)
+done
+
+
+subsubsection{*@{term bin_minus}: Unary Negation of Binary Integers*}
+
+lemma integ_of_minus: "w: bin ==> integ_of(bin_minus(w)) = \$- integ_of(w)"
+apply (erule bin.induct)
+done
+
+
+
+
+apply (erule bin.induct, auto)
+done
+
+
+apply (erule bin.induct, auto)
+done
+
+
+
+     "[| w: bin;  y: bool |]
+      ==> bin_add(v BIT x, w BIT y) =
+          NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"
+
+     "v: bin ==>
+          ALL w: bin. integ_of(bin_add(v,w)) = integ_of(v) \$+ integ_of(w)"
+apply (erule bin.induct, simp, simp)
+apply (rule ballI)
+apply (induct_tac "wa")
+done
+
+(*Subtraction*)
+lemma diff_integ_of_eq:
+     "[| v: bin;  w: bin |]
+      ==> integ_of(v) \$- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))"
+apply (unfold zdiff_def)
+done
+
+
+subsubsection{*@{term bin_mult}: Binary Multiplication*}
+
+lemma integ_of_mult:
+     "[| v: bin;  w: bin |]
+      ==> integ_of(bin_mult(v,w)) = integ_of(v) \$* integ_of(w)"
+apply (induct_tac "v", simp)
+done
+
+
+subsection{*Computations*}
+
+(** extra rules for bin_succ, bin_pred **)
+
+lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0"
+by simp
+
+lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)"
+by simp
+
+lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)"
+by simp
+
+lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1"
+by simp
+
+(** extra rules for bin_minus **)
+
+lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))"
+by simp
+
+lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0"
+by simp
+
+(** extra rules for bin_add **)
+
+lemma bin_add_BIT_11: "w: bin ==> bin_add(v BIT 1, w BIT 1) =
+by simp
+
+lemma bin_add_BIT_10: "w: bin ==> bin_add(v BIT 1, w BIT 0) =
+by simp
+
+lemma bin_add_BIT_0: "[| w: bin;  y: bool |]
+by simp
+
+(** extra rules for bin_mult **)
+
+lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)"
+by simp
+
+lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)"
+by simp
+
+
+(** Simplification rules with integer constants **)
+
+lemma int_of_0: "\$#0 = #0"
+by simp
+
+lemma int_of_succ: "\$# succ(n) = #1 \$+ \$#n"
+
+lemma zminus_0 [simp]: "\$- #0 = #0"
+by simp
+
+lemma zadd_0_intify [simp]: "#0 \$+ z = intify(z)"
+by simp
+
+lemma zadd_0_right_intify [simp]: "z \$+ #0 = intify(z)"
+by simp
+
+lemma zmult_1_intify [simp]: "#1 \$* z = intify(z)"
+by simp
+
+lemma zmult_1_right_intify [simp]: "z \$* #1 = intify(z)"
+by (subst zmult_commute, simp)
+
+lemma zmult_0 [simp]: "#0 \$* z = #0"
+by simp
+
+lemma zmult_0_right [simp]: "z \$* #0 = #0"
+by (subst zmult_commute, simp)
+
+lemma zmult_minus1 [simp]: "#-1 \$* z = \$-z"
+
+lemma zmult_minus1_right [simp]: "z \$* #-1 = \$-z"
+apply (subst zmult_commute)
+apply (rule zmult_minus1)
+done
+
+
+subsection{*Simplification Rules for Comparison of Binary Numbers*}
+text{*Thanks to Norbert Voelker*}
+
+(** Equals (=) **)
+
+lemma eq_integ_of_eq:
+     "[| v: bin;  w: bin |]
+      ==> ((integ_of(v)) = integ_of(w)) <->
+          iszero (integ_of (bin_add (v, bin_minus(w))))"
+apply (unfold iszero_def)
+done
+
+lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))"
+by (unfold iszero_def, simp)
+
+
+lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))"
+apply (unfold iszero_def)
+done
+
+lemma iszero_integ_of_BIT:
+     "[| w: bin; x: bool |]
+      ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"
+apply (unfold iszero_def, simp)
+apply (subgoal_tac "integ_of (w) : int")
+apply typecheck
+apply (drule int_cases)
+apply (subgoal_tac "znegative (\$- \$# succ (n)) <-> znegative (\$# succ (n))")
+ apply (simp (no_asm_use))
+apply simp
+done
+
+lemma iszero_integ_of_0:
+     "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"
+by (simp only: iszero_integ_of_BIT, blast)
+
+lemma iszero_integ_of_1: "w: bin ==> ~ iszero (integ_of (w BIT 1))"
+by (simp only: iszero_integ_of_BIT, blast)
+
+
+
+(** Less-than (<) **)
+
+lemma less_integ_of_eq_neg:
+     "[| v: bin;  w: bin |]
+      ==> integ_of(v) \$< integ_of(w)
+          <-> znegative (integ_of (bin_add (v, bin_minus(w))))"
+apply (unfold zless_def zdiff_def)
+done
+
+lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))"
+by simp
+
+lemma neg_integ_of_Min: "znegative (integ_of(Min))"
+by simp
+
+lemma neg_integ_of_BIT:
+     "[| w: bin; x: bool |]
+      ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"
+apply simp
+apply (subgoal_tac "integ_of (w) : int")
+apply typecheck
+apply (drule int_cases)
+apply (subgoal_tac "\$#1 \$- \$# succ (succ (n #+ n)) = \$- \$# succ (n #+ n) ")
+apply (simp add: equation_zminus int_of_diff [symmetric])
+done
+
+(** Less-than-or-equals (<=) **)
+
+lemma le_integ_of_eq_not_less:
+     "(integ_of(x) \$<= (integ_of(w))) <-> ~ (integ_of(w) \$< (integ_of(x)))"
+by (simp add: not_zless_iff_zle [THEN iff_sym])
+
+
+(*Delete the original rewrites, with their clumsy conditional expressions*)
+declare bin_succ_BIT [simp del]
+        bin_pred_BIT [simp del]
+        bin_minus_BIT [simp del]
+        NCons_Pls [simp del]
+        NCons_Min [simp del]
+        bin_mult_BIT [simp del]
+
+(*Hide the binary representation of integer constants*)
+declare integ_of_Pls [simp del] integ_of_Min [simp del] integ_of_BIT [simp del]
+
+
+lemmas bin_arith_extra_simps =
+     integ_of_minus [symmetric]
+     integ_of_mult [symmetric]
+     bin_succ_1 bin_succ_0
+     bin_pred_1 bin_pred_0
+     bin_minus_1 bin_minus_0
+     diff_integ_of_eq
+     bin_mult_1 bin_mult_0 NCons_simps
+
+
+(*For making a minimal simpset, one must include these default simprules
+  of thy.  Also include simp_thms, or at least (~False)=True*)
+lemmas bin_arith_simps =
+     bin_pred_Pls bin_pred_Min
+     bin_succ_Pls bin_succ_Min
+     bin_minus_Pls bin_minus_Min
+     bin_mult_Pls bin_mult_Min
+     bin_arith_extra_simps
+
+(*Simplification of relational operations*)
+lemmas bin_rel_simps =
+     eq_integ_of_eq iszero_integ_of_Pls nonzero_integ_of_Min
+     iszero_integ_of_0 iszero_integ_of_1
+     less_integ_of_eq_neg
+     not_neg_integ_of_Pls neg_integ_of_Min neg_integ_of_BIT
+     le_integ_of_eq_not_less
+
+declare bin_arith_simps [simp]
+declare bin_rel_simps [simp]
+
+
+(** Simplification of arithmetic when nested to the right **)
+
+     "[| v: bin;  w: bin |]
+      ==> integ_of(v) \$+ (integ_of(w) \$+ z) = (integ_of(bin_add(v,w)) \$+ z)"
+
+lemma mult_integ_of_left [simp]:
+     "[| v: bin;  w: bin |]
+      ==> integ_of(v) \$* (integ_of(w) \$* z) = (integ_of(bin_mult(v,w)) \$* z)"
+
+    "[| v: bin;  w: bin |]
+      ==> integ_of(v) \$+ (integ_of(w) \$- c) = integ_of(bin_add(v,w)) \$- (c)"
+apply (unfold zdiff_def)
+done
+
+     "[| v: bin;  w: bin |]
+      ==> integ_of(v) \$+ (c \$- integ_of(w)) =
+          integ_of (bin_add (v, bin_minus(w))) \$+ (c)"
+apply (subst diff_integ_of_eq [symmetric])
+done
+
+
+(** More for integer constants **)
+
+declare int_of_0 [simp] int_of_succ [simp]
+
+lemma zdiff0 [simp]: "#0 \$- x = \$-x"
+
+lemma zdiff0_right [simp]: "x \$- #0 = intify(x)"
+
+lemma zdiff_self [simp]: "x \$- x = #0"
+
+lemma znegative_iff_zless_0: "k: int ==> znegative(k) <-> k \$< #0"
+
+lemma zero_zless_imp_znegative_zminus: "[|#0 \$< k; k: int|] ==> znegative(\$-k)"
+
+lemma zero_zle_int_of [simp]: "#0 \$<= \$# n"
+by (simp add: not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym])
+
+lemma nat_of_0 [simp]: "nat_of(#0) = 0"
+by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of)
+
+lemma nat_le_int0_lemma: "[| z \$<= \$#0; z: int |] ==> nat_of(z) = 0"
+by (auto simp add: znegative_iff_zless_0 [THEN iff_sym] zle_def zneg_nat_of)
+
+lemma nat_le_int0: "z \$<= \$#0 ==> nat_of(z) = 0"
+apply (subgoal_tac "nat_of (intify (z)) = 0")
+apply (rule_tac [2] nat_le_int0_lemma, auto)
+done
+
+lemma int_of_eq_0_imp_natify_eq_0: "\$# n = #0 ==> natify(n) = 0"
+by (rule not_znegative_imp_zero, auto)
+
+lemma nat_of_zminus_int_of: "nat_of(\$- \$# n) = 0"
+apply (unfold nat_of_def raw_nat_of_def)
+apply (auto dest!: not_znegative_imp_zero natify_int_of_eq
+            iff del: int_of_eq)
+apply (rule the_equality, auto)
+apply (blast intro: int_of_eq_0_imp_natify_eq_0 sym)
+done
+
+lemma int_of_nat_of: "#0 \$<= z ==> \$# nat_of(z) = intify(z)"
+apply (rule not_zneg_nat_of_intify)
+done
+
+declare int_of_nat_of [simp] nat_of_zminus_int_of [simp]
+
+lemma int_of_nat_of_if: "\$# nat_of(z) = (if #0 \$<= z then intify(z) else #0)"
+by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless)
+
+lemma zless_nat_iff_int_zless: "[| m: nat; z: int |] ==> (m < nat_of(z)) <-> (\$#m \$< z)"
+apply (case_tac "znegative (z) ")
+apply (erule_tac [2] not_zneg_nat_of [THEN subst])
+apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans]
+done
+
+
+(** nat_of and zless **)
+
+(*An alternative condition is  \$#0 <= w  *)
+lemma zless_nat_conj_lemma: "\$#0 \$< z ==> (nat_of(w) < nat_of(z)) <-> (w \$< z)"
+apply (rule iff_trans)
+apply (rule zless_int_of [THEN iff_sym])
+apply (auto simp add: int_of_nat_of_if simp del: zless_int_of)
+apply (auto elim: zless_asym simp add: not_zle_iff_zless)
+apply (blast intro: zless_zle_trans)
+done
+
+lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) <-> (\$#0 \$< z & w \$< z)"
+apply (case_tac "\$#0 \$< z")
+apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle)
+done
+
+(*This simprule cannot be added unless we can find a way to make eq_integ_of_eq
+  unconditional!
+  [The condition "True" is a hack to prevent looping.
+    Conditional rewrite rules are tried after unconditional ones, so a rule
+    like eq_nat_number_of will be tried first to eliminate #mm=#nn.]
+  lemma integ_of_reorient [simp]:
+       "True ==> (integ_of(w) = x) <-> (x = integ_of(w))"
+  by auto
+*)
+
+lemma integ_of_minus_reorient [simp]:
+     "(integ_of(w) = \$- x) <-> (\$- x = integ_of(w))"
+by auto
+
+     "(integ_of(w) = x \$+ y) <-> (x \$+ y = integ_of(w))"
+by auto
+
+lemma integ_of_diff_reorient [simp]:
+     "(integ_of(w) = x \$- y) <-> (x \$- y = integ_of(w))"
+by auto
+
+lemma integ_of_mult_reorient [simp]:
+     "(integ_of(w) = x \$* y) <-> (x \$* y = integ_of(w))"
+by auto
+
+ML
+{*
+val bin_pred_Pls = thm "bin_pred_Pls";
+val bin_pred_Min = thm "bin_pred_Min";
+val bin_minus_Pls = thm "bin_minus_Pls";
+val bin_minus_Min = thm "bin_minus_Min";
+
+val NCons_Pls_0 = thm "NCons_Pls_0";
+val NCons_Pls_1 = thm "NCons_Pls_1";
+val NCons_Min_0 = thm "NCons_Min_0";
+val NCons_Min_1 = thm "NCons_Min_1";
+val NCons_BIT = thm "NCons_BIT";
+val NCons_simps = thms "NCons_simps";
+val integ_of_type = thm "integ_of_type";
+val NCons_type = thm "NCons_type";
+val bin_succ_type = thm "bin_succ_type";
+val bin_pred_type = thm "bin_pred_type";
+val bin_minus_type = thm "bin_minus_type";
+val bin_mult_type = thm "bin_mult_type";
+val integ_of_NCons = thm "integ_of_NCons";
+val integ_of_succ = thm "integ_of_succ";
+val integ_of_pred = thm "integ_of_pred";
+val integ_of_minus = thm "integ_of_minus";
+val diff_integ_of_eq = thm "diff_integ_of_eq";
+val integ_of_mult = thm "integ_of_mult";
+val bin_succ_1 = thm "bin_succ_1";
+val bin_succ_0 = thm "bin_succ_0";
+val bin_pred_1 = thm "bin_pred_1";
+val bin_pred_0 = thm "bin_pred_0";
+val bin_minus_1 = thm "bin_minus_1";
+val bin_minus_0 = thm "bin_minus_0";
+val bin_mult_1 = thm "bin_mult_1";
+val bin_mult_0 = thm "bin_mult_0";
+val int_of_0 = thm "int_of_0";
+val int_of_succ = thm "int_of_succ";
+val zminus_0 = thm "zminus_0";
+val zmult_1_intify = thm "zmult_1_intify";
+val zmult_1_right_intify = thm "zmult_1_right_intify";
+val zmult_0 = thm "zmult_0";
+val zmult_0_right = thm "zmult_0_right";
+val zmult_minus1 = thm "zmult_minus1";
+val zmult_minus1_right = thm "zmult_minus1_right";
+val eq_integ_of_eq = thm "eq_integ_of_eq";
+val iszero_integ_of_Pls = thm "iszero_integ_of_Pls";
+val nonzero_integ_of_Min = thm "nonzero_integ_of_Min";
+val iszero_integ_of_BIT = thm "iszero_integ_of_BIT";
+val iszero_integ_of_0 = thm "iszero_integ_of_0";
+val iszero_integ_of_1 = thm "iszero_integ_of_1";
+val less_integ_of_eq_neg = thm "less_integ_of_eq_neg";
+val not_neg_integ_of_Pls = thm "not_neg_integ_of_Pls";
+val neg_integ_of_Min = thm "neg_integ_of_Min";
+val neg_integ_of_BIT = thm "neg_integ_of_BIT";
+val le_integ_of_eq_not_less = thm "le_integ_of_eq_not_less";
+val bin_arith_extra_simps = thms "bin_arith_extra_simps";
+val bin_arith_simps = thms "bin_arith_simps";
+val bin_rel_simps = thms "bin_rel_simps";
+val mult_integ_of_left = thm "mult_integ_of_left";
+val zdiff0 = thm "zdiff0";
+val zdiff0_right = thm "zdiff0_right";
+val zdiff_self = thm "zdiff_self";
+val znegative_iff_zless_0 = thm "znegative_iff_zless_0";
+val zero_zless_imp_znegative_zminus = thm "zero_zless_imp_znegative_zminus";
+val zero_zle_int_of = thm "zero_zle_int_of";
+val nat_of_0 = thm "nat_of_0";
+val nat_le_int0 = thm "nat_le_int0";
+val int_of_eq_0_imp_natify_eq_0 = thm "int_of_eq_0_imp_natify_eq_0";
+val nat_of_zminus_int_of = thm "nat_of_zminus_int_of";
+val int_of_nat_of = thm "int_of_nat_of";
+val int_of_nat_of_if = thm "int_of_nat_of_if";
+val zless_nat_iff_int_zless = thm "zless_nat_iff_int_zless";
+val zless_nat_conj = thm "zless_nat_conj";
+val integ_of_minus_reorient = thm "integ_of_minus_reorient";