# HG changeset patch
# User paulson
# Date 1070550996 -3600
# Node ID e33ffff0123c63559d0fb50ab615d63e49b32be7
# Parent  5efbb548107d491b8bb6a4e64bb508cc3036b96f
further simplifications of the integer development; converting more .ML files
to Isar scripts

diff -r 5efbb548107d -r e33ffff0123c src/HOL/Integ/Int.thy
--- a/src/HOL/Integ/Int.thy	Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/Integ/Int.thy	Thu Dec 04 16:16:36 2003 +0100
@@ -54,75 +54,32 @@
 by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
 
 
-subsection{*Comparison laws*}
-
-(*RING AND FIELD????????????????????????????????????????????????????????????*)
-
-lemma zminus_zless_zminus [simp]: "(- x < - y) = (y < (x::int))"
-by (simp add: zless_def zdiff_def zadd_ac)
-
-lemma zminus_zle_zminus [simp]: "(- x \<le> - y) = (y \<le> (x::int))"
-by (simp add: zle_def)
-
-text{*The next several equations can make the simplifier loop!*}
-
-lemma zless_zminus: "(x < - y) = (y < - (x::int))"
-by (simp add: zless_def zdiff_def zadd_ac)
-
-lemma zminus_zless: "(- x < y) = (- y < (x::int))"
-by (simp add: zless_def zdiff_def zadd_ac)
-
-lemma zle_zminus: "(x \<le> - y) = (y \<le> - (x::int))"
-by (simp add: zle_def zminus_zless)
-
-lemma zminus_zle: "(- x \<le> y) = (- y \<le> (x::int))"
-by (simp add: zle_def zless_zminus)
-
-lemma equation_zminus: "(x = - y) = (y = - (x::int))"
-by auto
-
-lemma zminus_equation: "(- x = y) = (- (y::int) = x)"
-by auto
-
-
 subsection{*nat: magnitide of an integer, as a natural number*}
 
 lemma nat_int [simp]: "nat(int n) = n"
 by (unfold nat_def, auto)
 
-lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
-apply (unfold nat_def)
-apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless)
-done
-
 lemma nat_zero [simp]: "nat 0 = 0"
 apply (unfold Zero_int_def)
 apply (rule nat_int)
 done
 
+lemma neg_nat: "neg z ==> nat z = 0"
+by (unfold nat_def, auto)
+
 lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
 apply (drule not_neg_eq_ge_0 [THEN iffD1])
 apply (drule zle_imp_zless_or_eq)
 apply (auto simp add: zless_iff_Suc_zadd)
 done
 
-lemma neg_nat: "neg z ==> nat z = 0"
-by (unfold nat_def, auto)
-
-lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
-apply (case_tac "neg z")
-apply (erule_tac [2] not_neg_nat [THEN subst])
-apply (auto simp add: neg_nat)
-apply (auto dest: order_less_trans simp add: neg_eq_less_0)
-done
-
 lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
 by (simp add: neg_eq_less_0 zle_def not_neg_nat)
 
 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
 by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
 
-(*An alternative condition is  0 \<le> w  *)
+text{*An alternative condition is @{term "0 \<le> w"} *}
 lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
 apply (subst zless_int [symmetric])
 apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
@@ -137,10 +94,11 @@
 apply (auto simp add: nat_mono_iff linorder_not_less)
 done
 
-
 subsection{*Monotonicity results*}
 
-(*RING AND FIELD?*)
+text{*Most are available in theory @{text Ring_and_Field}, but they are
+      not yet available: we must prove @{text zadd_zless_mono} before we
+      can prove that the integers are a ring.*}
 
 lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))"
 by (simp add: zless_def zdiff_def zadd_ac) 
@@ -181,7 +139,7 @@
 apply (simp add: int_Suc)
 apply (case_tac "n=0")
 apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
-apply (simp_all add: zadd_zmult_distrib zadd_zless_mono int_Suc0_eq_1 order_le_less)
+apply (simp_all add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
 done
 
 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
@@ -191,6 +149,7 @@
 apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
 done
 
+
 text{*The Integers Form an Ordered Ring*}
 instance int :: ordered_ring
 proof
@@ -210,6 +169,39 @@
   show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
 qed
 
+
+subsection{*Comparison laws*}
+
+text{*Legacy bindings: all are in theory @{text Ring_and_Field}.*}
+
+lemma zminus_zless_zminus: "(- x < - y) = (y < (x::int))"
+  by (rule Ring_and_Field.neg_less_iff_less)
+
+lemma zminus_zle_zminus: "(- x \<le> - y) = (y \<le> (x::int))"
+  by (rule Ring_and_Field.neg_le_iff_le)
+
+
+text{*The next several equations can make the simplifier loop!*}
+
+lemma zless_zminus: "(x < - y) = (y < - (x::int))"
+  by (rule Ring_and_Field.less_minus_iff)
+
+lemma zminus_zless: "(- x < y) = (- y < (x::int))"
+  by (rule Ring_and_Field.minus_less_iff)
+
+lemma zle_zminus: "(x \<le> - y) = (y \<le> - (x::int))"
+  by (rule Ring_and_Field.le_minus_iff)
+
+lemma zminus_zle: "(- x \<le> y) = (- y \<le> (x::int))"
+  by (rule Ring_and_Field.minus_le_iff)
+
+lemma equation_zminus: "(x = - y) = (y = - (x::int))"
+  by (rule Ring_and_Field.equation_minus_iff)
+
+lemma zminus_equation: "(- x = y) = (- (y::int) = x)"
+  by (rule Ring_and_Field.minus_equation_iff)
+
+
 subsection{*Lemmas about the Function @{term int} and Orderings*}
 
 lemma negative_zless_0: "- (int (Suc n)) < 0"
@@ -254,6 +246,18 @@
 
 subsection{*Misc Results*}
 
+lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
+apply (unfold nat_def)
+apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless)
+done
+
+lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
+apply (case_tac "neg z")
+apply (erule_tac [2] not_neg_nat [THEN subst])
+apply (auto simp add: neg_nat)
+apply (auto dest: order_less_trans simp add: neg_eq_less_0)
+done
+
 lemma zless_eq_neg: "(w<z) = neg(w-z)"
 by (simp add: zless_def)
 
@@ -350,6 +354,22 @@
 apply (simp add: eq_diff_eq [symmetric])
 done
 
+
+
+text{*A case theorem distinguishing non-negative and negative int*}
+
+lemma negD: "neg x ==> EX n. x = - (int (Suc n))"
+by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd 
+                   diff_eq_eq [symmetric] zdiff_def)
+
+lemma int_cases: 
+     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
+apply (case_tac "neg z")
+apply (fast dest!: negD)
+apply (drule not_neg_nat [symmetric], auto) 
+done
+
+
 (*Legacy ML bindings, but no longer the structure Int.*)
 ML
 {*
@@ -372,61 +392,6 @@
 val not_iszero_1 = thm "not_iszero_1";
 val int_0_less_1 = thm "int_0_less_1";
 val int_0_neq_1 = thm "int_0_neq_1";
-val zadd_cancel_21 = thm "zadd_cancel_21";
-val zadd_cancel_end = thm "zadd_cancel_end";
-
-structure Int_Cancel_Data =
-struct
-  val ss		= HOL_ss
-  val eq_reflection	= eq_reflection
-
-  val sg_ref 		= Sign.self_ref (Theory.sign_of (the_context()))
-  val T		= HOLogic.intT
-  val zero		= Const ("0", HOLogic.intT)
-  val restrict_to_left  = restrict_to_left
-  val add_cancel_21	= zadd_cancel_21
-  val add_cancel_end	= zadd_cancel_end
-  val add_left_cancel	= zadd_left_cancel
-  val add_assoc		= zadd_assoc
-  val add_commute	= zadd_commute
-  val add_left_commute	= zadd_left_commute
-  val add_0		= zadd_0
-  val add_0_right	= zadd_0_right
-
-  val eq_diff_eq	= eq_diff_eq
-  val eqI_rules		= [zless_eqI, zeq_eqI, zle_eqI]
-  fun dest_eqI th = 
-      #1 (HOLogic.dest_bin "op =" HOLogic.boolT
-	      (HOLogic.dest_Trueprop (concl_of th)))
-
-  val diff_def		= zdiff_def
-  val minus_add_distrib	= zminus_zadd_distrib
-  val minus_minus	= zminus_zminus
-  val minus_0		= zminus_0
-  val add_inverses	= [zadd_zminus_inverse, zadd_zminus_inverse2]
-  val cancel_simps	= [zadd_zminus_cancel, zminus_zadd_cancel]
-end;
-
-structure Int_Cancel = Abel_Cancel (Int_Cancel_Data);
-*}
-
-
-text{*A case theorem distinguishing non-negative and negative int*}
-
-lemma negD: "neg x ==> EX n. x = - (int (Suc n))"
-by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd 
-                   diff_eq_eq [symmetric] zdiff_def)
-
-lemma int_cases: 
-     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
-apply (case_tac "neg z")
-apply (fast dest!: negD)
-apply (drule not_neg_nat [symmetric], auto) 
-done
-
-
-ML
-{*
 val zless_eq_neg = thm "zless_eq_neg";
 val eq_eq_iszero = thm "eq_eq_iszero";
 val zle_eq_not_neg = thm "zle_eq_not_neg";
diff -r 5efbb548107d -r e33ffff0123c src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/Integ/NatBin.thy	Thu Dec 04 16:16:36 2003 +0100
@@ -9,33 +9,31 @@
 theory NatBin = IntPower:
 
 text {*
-  This case is simply reduced to that for the non-negative integers.
+  Arithmetic for naturals is reduced to that for the non-negative integers.
 *}
 
 instance nat :: number ..
 
 defs (overloaded)
-  nat_number_of_def: "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
+  nat_number_of_def:
+     "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
 
 
 (** nat (coercion from int to nat) **)
 
-lemma nat_number_of: "nat (number_of w) = number_of w"
-apply (simp (no_asm) add: nat_number_of_def)
-done
-declare nat_number_of [simp] nat_0 [simp] nat_1 [simp]
+declare nat_0 [simp] nat_1 [simp]
+
+lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
+by (simp add: nat_number_of_def)
 
 lemma numeral_0_eq_0: "Numeral0 = (0::nat)"
-apply (simp (no_asm) add: nat_number_of_def)
-done
+by (simp add: nat_number_of_def)
 
 lemma numeral_1_eq_1: "Numeral1 = (1::nat)"
-apply (simp (no_asm) add: nat_1 nat_number_of_def)
-done
+by (simp add: nat_1 nat_number_of_def)
 
 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
-apply (simp (no_asm) add: numeral_1_eq_1)
-done
+by (simp add: numeral_1_eq_1)
 
 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
 apply (unfold nat_number_of_def)
@@ -43,36 +41,36 @@
 done
 
 
-(** Distributive laws for "nat".  The others are in IntArith.ML, but these
-    require div and mod to be defined for type "int".  They also need 
-    some of the lemmas proved just above.**)
+text{*Distributive laws for type @{text nat}.  The others are in theory
+   @{text IntArith}, but these require div and mod to be defined for type
+   "int".  They also need some of the lemmas proved above.*}
 
 lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
 apply (case_tac "0 <= z'")
 apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
-apply (case_tac "z' = 0" , simp (no_asm_simp) add: DIVISION_BY_ZERO)
+apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
 apply (auto elim!: nonneg_eq_int)
 apply (rename_tac m m')
 apply (subgoal_tac "0 <= int m div int m'")
  prefer 2 apply (simp add: numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
-apply (rule inj_int [THEN injD])
-apply (simp (no_asm_simp))
+apply (rule inj_int [THEN injD], simp)
 apply (rule_tac r = "int (m mod m') " in quorem_div)
- prefer 2 apply (force)
-apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int zmult_int)
+ prefer 2 apply force
+apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int 
+                 zmult_int)
 done
 
 (*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
-lemma nat_mod_distrib: "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
-apply (case_tac "z' = 0" , simp (no_asm_simp) add: DIVISION_BY_ZERO)
+lemma nat_mod_distrib:
+     "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
+apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
 apply (auto elim!: nonneg_eq_int)
 apply (rename_tac m m')
 apply (subgoal_tac "0 <= int m mod int m'")
  prefer 2 apply (simp add: nat_less_iff numeral_0_eq_0 pos_mod_sign) 
-apply (rule inj_int [THEN injD])
-apply (simp (no_asm_simp))
+apply (rule inj_int [THEN injD], simp)
 apply (rule_tac q = "int (m div m') " in quorem_mod)
- prefer 2 apply (force)
+ prefer 2 apply force
 apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int zmult_int)
 done
 
@@ -80,7 +78,8 @@
 (** int (coercion from nat to int) **)
 
 (*"neg" is used in rewrite rules for binary comparisons*)
-lemma int_nat_number_of: "int (number_of v :: nat) =  
+lemma int_nat_number_of:
+     "int (number_of v :: nat) =  
          (if neg (number_of v) then 0  
           else (number_of v :: int))"
 by (simp del: nat_number_of
@@ -92,18 +91,20 @@
 
 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
 apply (rule sym)
-apply (simp (no_asm_simp) add: nat_eq_iff int_Suc)
+apply (simp add: nat_eq_iff int_Suc)
 done
 
-lemma Suc_nat_number_of_add: "Suc (number_of v + n) =  
+lemma Suc_nat_number_of_add:
+     "Suc (number_of v + n) =  
         (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)" 
 by (simp del: nat_number_of 
          add: nat_number_of_def neg_nat
               Suc_nat_eq_nat_zadd1 number_of_succ) 
 
-lemma Suc_nat_number_of: "Suc (number_of v) =  
+lemma Suc_nat_number_of:
+     "Suc (number_of v) =  
         (if neg (number_of v) then 1 else number_of (bin_succ v))"
-apply (cut_tac n = "0" in Suc_nat_number_of_add)
+apply (cut_tac n = 0 in Suc_nat_number_of_add)
 apply (simp cong del: if_weak_cong)
 done
 declare Suc_nat_number_of [simp]
@@ -112,7 +113,8 @@
 (** Addition **)
 
 (*"neg" is used in rewrite rules for binary comparisons*)
-lemma add_nat_number_of: "(number_of v :: nat) + number_of v' =  
+lemma add_nat_number_of:
+     "(number_of v :: nat) + number_of v' =  
          (if neg (number_of v) then number_of v'  
           else if neg (number_of v') then number_of v  
           else number_of (bin_add v v'))"
@@ -125,12 +127,13 @@
 
 (** Subtraction **)
 
-lemma diff_nat_eq_if: "nat z - nat z' =  
+lemma diff_nat_eq_if:
+     "nat z - nat z' =  
         (if neg z' then nat z   
          else let d = z-z' in     
               if neg d then 0 else nat d)"
-apply (simp (no_asm) add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
-apply (simp (no_asm) add: diff_is_0_eq nat_le_eq_zle)
+apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
+apply (simp add: diff_is_0_eq nat_le_eq_zle)
 done
 
 lemma diff_nat_number_of: 
@@ -145,7 +148,8 @@
 
 (** Multiplication **)
 
-lemma mult_nat_number_of: "(number_of v :: nat) * number_of v' =  
+lemma mult_nat_number_of:
+     "(number_of v :: nat) * number_of v' =  
        (if neg (number_of v) then 0 else number_of (bin_mult v v'))"
 by (force dest!: neg_nat
           simp del: nat_number_of
@@ -156,7 +160,8 @@
 
 (** Quotient **)
 
-lemma div_nat_number_of: "(number_of v :: nat)  div  number_of v' =  
+lemma div_nat_number_of:
+     "(number_of v :: nat)  div  number_of v' =  
           (if neg (number_of v) then 0  
            else nat (number_of v div number_of v'))"
 by (force dest!: neg_nat
@@ -168,7 +173,8 @@
 
 (** Remainder **)
 
-lemma mod_nat_number_of: "(number_of v :: nat)  mod  number_of v' =  
+lemma mod_nat_number_of:
+     "(number_of v :: nat)  mod  number_of v' =  
         (if neg (number_of v) then 0  
          else if neg (number_of v') then number_of v  
          else nat (number_of v mod number_of v'))"
@@ -229,18 +235,19 @@
 
 (** Equals (=) **)
 
-lemma eq_nat_nat_iff: "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
-apply (auto elim!: nonneg_eq_int)
-done
+lemma eq_nat_nat_iff:
+     "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
+by (auto elim!: nonneg_eq_int)
 
 (*"neg" is used in rewrite rules for binary comparisons*)
-lemma eq_nat_number_of: "((number_of v :: nat) = number_of v') =  
+lemma eq_nat_number_of:
+     "((number_of v :: nat) = number_of v') =  
       (if neg (number_of v) then (iszero (number_of v') | neg (number_of v'))  
        else if neg (number_of v') then iszero (number_of v)  
        else iszero (number_of (bin_add v (bin_minus v'))))"
 apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
                   eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
-            split add: split_if cong add: imp_cong);
+            split add: split_if cong add: imp_cong)
 apply (simp only: nat_eq_iff nat_eq_iff2)
 apply (simp add: not_neg_eq_ge_0 [symmetric])
 done
@@ -250,13 +257,13 @@
 (** Less-than (<) **)
 
 (*"neg" is used in rewrite rules for binary comparisons*)
-lemma less_nat_number_of: "((number_of v :: nat) < number_of v') =  
+lemma less_nat_number_of:
+     "((number_of v :: nat) < number_of v') =  
          (if neg (number_of v) then neg (number_of (bin_minus v'))  
           else neg (number_of (bin_add v (bin_minus v'))))"
 apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
                 nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
-            cong add: imp_cong);
-apply (simp add: ); 
+            cong add: imp_cong, simp) 
 done
 
 declare less_nat_number_of [simp]
@@ -264,7 +271,8 @@
 
 (** Less-than-or-equals (<=) **)
 
-lemma le_nat_number_of_eq_not_less: "(number_of x <= (number_of y::nat)) =  
+lemma le_nat_number_of_eq_not_less:
+     "(number_of x <= (number_of y::nat)) =  
       (~ number_of y < (number_of x::nat))"
 apply (rule linorder_not_less [symmetric])
 done
@@ -279,8 +287,7 @@
 (** Nat **)
 
 lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
-apply (simp add: numerals)
-done
+by (simp add: numerals)
 
 (*Expresses a natural number constant as the Suc of another one.
   NOT suitable for rewriting because n recurs in the condition.*)
@@ -289,8 +296,7 @@
 (** Arith **)
 
 lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
-apply (simp add: numerals)
-done
+by (simp add: numerals)
 
 (* These two can be useful when m = number_of... *)
 
@@ -310,91 +316,96 @@
 done
 
 lemma diff_less': "[| 0<n; 0<m |] ==> m - n < (m::nat)"
-apply (simp add: diff_less numerals)
-done
+by (simp add: diff_less numerals)
 
 declare diff_less' [of "number_of v", standard, simp]
 
 (** Power **)
 
 lemma power_two: "(p::nat) ^ 2 = p*p"
-apply (simp add: numerals)
-done
+by (simp add: numerals)
 
 
 (*** Comparisons involving (0::nat) ***)
 
-lemma eq_number_of_0: "(number_of v = (0::nat)) =  
+lemma eq_number_of_0:
+     "(number_of v = (0::nat)) =  
       (if neg (number_of v) then True else iszero (number_of v))"
-apply (simp (no_asm) add: numeral_0_eq_0 [symmetric] iszero_0)
+apply (simp add: numeral_0_eq_0 [symmetric] iszero_0)
 done
 
-lemma eq_0_number_of: "((0::nat) = number_of v) =  
+lemma eq_0_number_of:
+     "((0::nat) = number_of v) =  
       (if neg (number_of v) then True else iszero (number_of v))"
 apply (rule trans [OF eq_sym_conv eq_number_of_0])
 done
 
-lemma less_0_number_of: "((0::nat) < number_of v) = neg (number_of (bin_minus v))"
-apply (simp (no_asm) add: numeral_0_eq_0 [symmetric])
-done
+lemma less_0_number_of:
+     "((0::nat) < number_of v) = neg (number_of (bin_minus v))"
+by (simp add: numeral_0_eq_0 [symmetric])
 
 (*Simplification already handles n<0, n<=0 and 0<=n.*)
 declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp]
 
 lemma neg_imp_number_of_eq_0: "neg (number_of v) ==> number_of v = (0::nat)"
-apply (simp (no_asm_simp) add: numeral_0_eq_0 [symmetric] iszero_0)
-done
+by (simp add: numeral_0_eq_0 [symmetric] iszero_0)
 
 
 
 (*** Comparisons involving Suc ***)
 
-lemma eq_number_of_Suc [simp]: "(number_of v = Suc n) =  
+lemma eq_number_of_Suc [simp]:
+     "(number_of v = Suc n) =  
         (let pv = number_of (bin_pred v) in  
          if neg pv then False else nat pv = n)"
 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
                   number_of_pred nat_number_of_def 
-            split add: split_if);
+            split add: split_if)
 apply (rule_tac x = "number_of v" in spec)
 apply (auto simp add: nat_eq_iff)
 done
 
-lemma Suc_eq_number_of [simp]: "(Suc n = number_of v) =  
+lemma Suc_eq_number_of [simp]:
+     "(Suc n = number_of v) =  
         (let pv = number_of (bin_pred v) in  
          if neg pv then False else nat pv = n)"
 apply (rule trans [OF eq_sym_conv eq_number_of_Suc])
 done
 
-lemma less_number_of_Suc [simp]: "(number_of v < Suc n) =  
+lemma less_number_of_Suc [simp]:
+     "(number_of v < Suc n) =  
         (let pv = number_of (bin_pred v) in  
          if neg pv then True else nat pv < n)"
 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
                   number_of_pred nat_number_of_def  
-            split add: split_if);
+            split add: split_if)
 apply (rule_tac x = "number_of v" in spec)
 apply (auto simp add: nat_less_iff)
 done
 
-lemma less_Suc_number_of [simp]: "(Suc n < number_of v) =  
+lemma less_Suc_number_of [simp]:
+     "(Suc n < number_of v) =  
         (let pv = number_of (bin_pred v) in  
          if neg pv then False else n < nat pv)"
 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
                   number_of_pred nat_number_of_def
-            split add: split_if);
+            split add: split_if)
 apply (rule_tac x = "number_of v" in spec)
 apply (auto simp add: zless_nat_eq_int_zless)
 done
 
-lemma le_number_of_Suc [simp]: "(number_of v <= Suc n) =  
+lemma le_number_of_Suc [simp]:
+     "(number_of v <= Suc n) =  
         (let pv = number_of (bin_pred v) in  
          if neg pv then True else nat pv <= n)"
-apply (simp (no_asm) add: Let_def less_Suc_number_of linorder_not_less [symmetric])
+apply (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
 done
 
-lemma le_Suc_number_of [simp]: "(Suc n <= number_of v) =  
+lemma le_Suc_number_of [simp]:
+     "(Suc n <= number_of v) =  
         (let pv = number_of (bin_pred v) in  
          if neg pv then False else n <= nat pv)"
-apply (simp (no_asm) add: Let_def less_number_of_Suc linorder_not_less [symmetric])
+apply (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
 done
 
 
@@ -402,46 +413,44 @@
 declare zadd_int [symmetric, simp]
 
 lemma lemma1: "(m+m = n+n) = (m = (n::int))"
-apply auto
-done
+by auto
 
 lemma lemma2: "m+m ~= (1::int) + (n + n)"
 apply auto
 apply (drule_tac f = "%x. x mod 2" in arg_cong)
-apply (simp (no_asm_use) add: zmod_zadd1_eq)
+apply (simp add: zmod_zadd1_eq)
 done
 
-lemma eq_number_of_BIT_BIT: "((number_of (v BIT x) ::int) = number_of (w BIT y)) =  
+lemma eq_number_of_BIT_BIT:
+     "((number_of (v BIT x) ::int) = number_of (w BIT y)) =  
       (x=y & (((number_of v) ::int) = number_of w))"
 by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute
                Ring_and_Field.add_left_cancel add_assoc left_zero
-            split add: split_if cong: imp_cong); 
+            split add: split_if cong: imp_cong) 
 
 
-lemma eq_number_of_BIT_Pls: "((number_of (v BIT x) ::int) = number_of bin.Pls) =  
+lemma eq_number_of_BIT_Pls:
+     "((number_of (v BIT x) ::int) = number_of bin.Pls) =  
       (x=False & (((number_of v) ::int) = number_of bin.Pls))"
 apply (simp only: simp_thms  add: number_of_BIT number_of_Pls eq_commute
             split add: split_if cong: imp_cong)
-apply (rule_tac x = "number_of v" in spec)
-apply safe
+apply (rule_tac x = "number_of v" in spec, safe)
 apply (simp_all (no_asm_use))
 apply (drule_tac f = "%x. x mod 2" in arg_cong)
-apply (simp (no_asm_use) add: zmod_zadd1_eq)
+apply (simp add: zmod_zadd1_eq)
 done
 
-lemma eq_number_of_BIT_Min: "((number_of (v BIT x) ::int) = number_of bin.Min) =  
+lemma eq_number_of_BIT_Min:
+     "((number_of (v BIT x) ::int) = number_of bin.Min) =  
       (x=True & (((number_of v) ::int) = number_of bin.Min))"
 apply (simp only: simp_thms  add: number_of_BIT number_of_Min eq_commute
             split add: split_if cong: imp_cong)
-apply (rule_tac x = "number_of v" in spec)
-apply auto
-apply (drule_tac f = "%x. x mod 2" in arg_cong)
-apply auto
+apply (rule_tac x = "number_of v" in spec, auto)
+apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
 done
 
 lemma eq_number_of_Pls_Min: "(number_of bin.Pls ::int) ~= number_of bin.Min"
-apply auto
-done
+by auto
 
 
 
@@ -452,7 +461,8 @@
 apply (simp_all (no_asm_simp) add: nat_mult_distrib)
 done
 
-lemma power_nat_number_of: "(number_of v :: nat) ^ n =  
+lemma power_nat_number_of:
+     "(number_of v :: nat) ^ n =  
        (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))"
 by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
          split add: split_if cong: imp_cong)
@@ -465,33 +475,32 @@
 (*** Literal arithmetic involving powers, type int ***)
 
 lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
-apply (simp (no_asm) add: zpower_zpower mult_commute)
-done
+by (simp add: zpower_zpower mult_commute)
 
 lemma zpower_two: "(p::int) ^ 2 = p*p"
-apply (simp add: numerals)
-done
+by (simp add: numerals)
 
 lemma zpower_odd: "(z::int) ^ (2*a + 1) = z * (z^a)^2"
-apply (simp (no_asm) add: zpower_even zpower_zadd_distrib)
-done
+by (simp add: zpower_even zpower_zadd_distrib)
 
-lemma zpower_number_of_even: "(z::int) ^ number_of (w BIT False) =  
+lemma zpower_number_of_even:
+     "(z::int) ^ number_of (w BIT False) =  
       (let w = z ^ (number_of w) in  w*w)"
 apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
 apply (simp only: number_of_add) 
-apply (rule_tac x = "number_of w" in spec , clarify)
+apply (rule_tac x = "number_of w" in spec, clarify)
 apply (case_tac " (0::int) <= x")
 apply (auto simp add: nat_mult_distrib zpower_even zpower_two)
 done
 
-lemma zpower_number_of_odd: "(z::int) ^ number_of (w BIT True) =  
+lemma zpower_number_of_odd:
+     "(z::int) ^ number_of (w BIT True) =  
           (if (0::int) <= number_of w                    
            then (let w = z ^ (number_of w) in  z*w*w)    
            else 1)"
 apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
 apply (simp only: number_of_add int_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) 
-apply (rule_tac x = "number_of w" in spec , clarify)
+apply (rule_tac x = "number_of w" in spec, clarify)
 apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even zpower_two neg_nat)
 done
 
@@ -606,6 +615,111 @@
 val nat_number = thms"nat_number";
 *}
 
+subsection {*Lemmas for the Combination and Cancellation Simprocs*}
+
+lemma nat_number_of_add_left:
+     "number_of v + (number_of v' + (k::nat)) =  
+         (if neg (number_of v) then number_of v' + k  
+          else if neg (number_of v') then number_of v + k  
+          else number_of (bin_add v v') + k)"
+apply simp
+done
+
+
+(** For combine_numerals **)
+
+lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
+by (simp add: add_mult_distrib)
+
+
+(** For cancel_numerals **)
+
+lemma nat_diff_add_eq1:
+     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
+by (simp split add: nat_diff_split add: add_mult_distrib)
+
+lemma nat_diff_add_eq2:
+     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
+by (simp split add: nat_diff_split add: add_mult_distrib)
+
+lemma nat_eq_add_iff1:
+     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_eq_add_iff2:
+     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_less_add_iff1:
+     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_less_add_iff2:
+     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_le_add_iff1:
+     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+lemma nat_le_add_iff2:
+     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
+by (auto split add: nat_diff_split simp add: add_mult_distrib)
+
+
+(** For cancel_numeral_factors **)
+
+lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
+by auto
+
+lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
+by auto
+
+lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
+by auto
+
+lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
+by auto
+
+
+(** For cancel_factor **)
+
+lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
+by auto
+
+lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
+by auto
+
+lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
+by auto
+
+lemma nat_mult_div_cancel_disj:
+     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
+by (simp add: nat_mult_div_cancel1)
+
+ML
+{*
+val nat_number_of_add_left = thm"nat_number_of_add_left";
+val left_add_mult_distrib = thm"left_add_mult_distrib";
+val nat_diff_add_eq1 = thm"nat_diff_add_eq1";
+val nat_diff_add_eq2 = thm"nat_diff_add_eq2";
+val nat_eq_add_iff1 = thm"nat_eq_add_iff1";
+val nat_eq_add_iff2 = thm"nat_eq_add_iff2";
+val nat_less_add_iff1 = thm"nat_less_add_iff1";
+val nat_less_add_iff2 = thm"nat_less_add_iff2";
+val nat_le_add_iff1 = thm"nat_le_add_iff1";
+val nat_le_add_iff2 = thm"nat_le_add_iff2";
+val nat_mult_le_cancel1 = thm"nat_mult_le_cancel1";
+val nat_mult_less_cancel1 = thm"nat_mult_less_cancel1";
+val nat_mult_eq_cancel1 = thm"nat_mult_eq_cancel1";
+val nat_mult_div_cancel1 = thm"nat_mult_div_cancel1";
+val nat_mult_le_cancel_disj = thm"nat_mult_le_cancel_disj";
+val nat_mult_less_cancel_disj = thm"nat_mult_less_cancel_disj";
+val nat_mult_eq_cancel_disj = thm"nat_mult_eq_cancel_disj";
+val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj";
+*}
+
+
 subsection {* Configuration of the code generator *}
 
 ML {*
diff -r 5efbb548107d -r e33ffff0123c src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Thu Dec 04 10:29:17 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,160 +0,0 @@
-(*  Title:      HOL/NatSimprocs.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2000  University of Cambridge
-
-Simprocs for nat numerals (see also nat_simprocs.ML).
-*)
-
-val ss_Int = simpset_of Int_thy;
-
-(** For simplifying  Suc m - #n **)
-
-Goal "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)";
-by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1]
-			    addsplits [nat_diff_split]) 1);
-qed "Suc_diff_eq_diff_pred";
-
-(*Now just instantiating n to (number_of v) does the right simplification,
-  but with some redundant inequality tests.*)
-Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
-by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0)" 1);
-by (asm_simp_tac (HOL_ss addsimps [less_Suc_eq_le, le_0_eq]) 1); 
-by (stac less_number_of_Suc 1);
-by (Simp_tac 1);
-qed "neg_number_of_bin_pred_iff_0";
-
-Goal "neg (number_of (bin_minus v)) ==> \
-\     Suc m - (number_of v) = m - (number_of (bin_pred v))";
-by (stac Suc_diff_eq_diff_pred 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (asm_full_simp_tac (ss_Int addsimps [diff_nat_number_of, 
-                    less_0_number_of RS sym, neg_number_of_bin_pred_iff_0]) 1);
-qed "Suc_diff_number_of";
-
-(* now redundant because of the inverse_fold simproc
-    Addsimps [Suc_diff_number_of]; *)
-
-Goal "nat_case a f (number_of v) = \
-\       (let pv = number_of (bin_pred v) in \
-\        if neg pv then a else f (nat pv))";
-by (simp_tac
-    (simpset() addsplits [nat.split]
-                        addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_case_number_of";
-
-Goal "nat_case a f ((number_of v) + n) = \
-\      (let pv = number_of (bin_pred v) in \
-\        if neg pv then nat_case a f n else f (nat pv + n))";
-by (stac add_eq_if 1);
-by (asm_simp_tac
-    (simpset() addsplits [nat.split]
-               addsimps [numeral_1_eq_Suc_0 RS sym, Let_def, 
-                   neg_imp_number_of_eq_0, neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_case_add_eq_if";
-
-Addsimps [nat_case_number_of, nat_case_add_eq_if];
-
-
-Goal "nat_rec a f (number_of v) = \
-\       (let pv = number_of (bin_pred v) in \
-\        if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))";
-by (case_tac "(number_of v)::nat" 1);
-by (ALLGOALS (asm_simp_tac
-              (simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0])));
-by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
-qed "nat_rec_number_of";
-
-Goal "nat_rec a f (number_of v + n) = \
-\       (let pv = number_of (bin_pred v) in \
-\        if neg pv then nat_rec a f n \
-\                  else f (nat pv + n) (nat_rec a f (nat pv + n)))";
-by (stac add_eq_if 1);
-by (asm_simp_tac
-    (simpset() addsplits [nat.split]
-               addsimps [numeral_1_eq_Suc_0 RS sym, Let_def, 
-                  neg_imp_number_of_eq_0, neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_rec_add_eq_if";
-
-Addsimps [nat_rec_number_of, nat_rec_add_eq_if];
-
-
-(** For simplifying  # m - Suc n **)
-
-Goal "m - Suc n = (m - 1) - n";
-by (simp_tac (numeral_ss addsplits [nat_diff_split]) 1);
-qed "diff_Suc_eq_diff_pred";
-
-(*Obsolete because of natdiff_cancel_numerals
-    Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred];
-  It LOOPS if Numeral1 is being replaced by 1.
-*)
-
-
-(** Evens and Odds, for Mutilated Chess Board **)
-
-(*Case analysis on b<2*)
-Goal "(n::nat) < 2 ==> n = 0 | n = Suc 0";
-by (arith_tac 1);
-qed "less_2_cases";
-
-Goal "Suc(Suc(m)) mod 2 = m mod 2";
-by (subgoal_tac "m mod 2 < 2" 1);
-by (Asm_simp_tac 2);
-by (etac (less_2_cases RS disjE) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def, mod_Suc, nat_1])));
-qed "mod2_Suc_Suc";
-Addsimps [mod2_Suc_Suc];
-
-Goal "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)";
-by (subgoal_tac "m mod 2 < 2" 1);
-by (Asm_simp_tac 2);
-by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
-qed "mod2_gr_0";
-Addsimps [mod2_gr_0];
-
-(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) 2 **)
-
-Goal "2 + n = Suc (Suc n)";
-by (Simp_tac 1);
-qed "add_2_eq_Suc";
-
-Goal "n + 2 = Suc (Suc n)";
-by (Simp_tac 1);
-qed "add_2_eq_Suc'";
-
-Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc'];
-
-(*Can be used to eliminate long strings of Sucs, but not by default*)
-Goal "Suc (Suc (Suc n)) = 3 + n";
-by (Simp_tac 1);
-qed "Suc3_eq_add_3";
-
-
-(** To collapse some needless occurrences of Suc 
-    At least three Sucs, since two and fewer are rewritten back to Suc again!
-
-    We already have some rules to simplify operands smaller than 3.
-**)
-
-Goal "m div (Suc (Suc (Suc n))) = m div (3+n)";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "div_Suc_eq_div_add3";
-
-Goal "m mod (Suc (Suc (Suc n))) = m mod (3+n)";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "mod_Suc_eq_mod_add3";
-
-Addsimps [div_Suc_eq_div_add3, mod_Suc_eq_mod_add3];
-
-Goal "(Suc (Suc (Suc m))) div n = (3+m) div n";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "Suc_div_eq_add3_div";
-
-Goal "(Suc (Suc (Suc m))) mod n = (3+m) mod n";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "Suc_mod_eq_add3_mod";
-
-Addsimps [inst "n" "number_of ?v" Suc_div_eq_add3_div,
-	  inst "n" "number_of ?v" Suc_mod_eq_add3_mod];
diff -r 5efbb548107d -r e33ffff0123c src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy	Thu Dec 04 16:16:36 2003 +0100
@@ -10,4 +10,126 @@
 
 setup nat_simprocs_setup
 
+subsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
+
+text{*Where K above is a literal*}
+
+lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
+by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
+
+(*Now just instantiating n to (number_of v) does the right simplification,
+  but with some redundant inequality tests.*)
+lemma neg_number_of_bin_pred_iff_0:
+     "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
+apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
+apply (simp only: less_Suc_eq_le le_0_eq)
+apply (subst less_number_of_Suc, simp)
+done
+
+text{*No longer required as a simprule because of the @{text inverse_fold}
+   simproc*}
+lemma Suc_diff_number_of:
+     "neg (number_of (bin_minus v)) ==>  
+      Suc m - (number_of v) = m - (number_of (bin_pred v))"
+apply (subst Suc_diff_eq_diff_pred, simp, simp)
+apply (force simp only: diff_nat_number_of less_0_number_of [symmetric] 
+                        neg_number_of_bin_pred_iff_0)
+done
+
+lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
+by (simp add: numerals split add: nat_diff_split)
+
+
+subsection{*For @{term nat_case} and @{term nat_rec}*}
+
+lemma nat_case_number_of [simp]:
+     "nat_case a f (number_of v) =  
+        (let pv = number_of (bin_pred v) in  
+         if neg pv then a else f (nat pv))"
+by (simp split add: nat.split add: Let_def neg_number_of_bin_pred_iff_0)
+
+lemma nat_case_add_eq_if [simp]:
+     "nat_case a f ((number_of v) + n) =  
+       (let pv = number_of (bin_pred v) in  
+         if neg pv then nat_case a f n else f (nat pv + n))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+            add: numeral_1_eq_Suc_0 [symmetric] Let_def 
+                 neg_imp_number_of_eq_0 neg_number_of_bin_pred_iff_0)
+done
+
+lemma nat_rec_number_of [simp]:
+     "nat_rec a f (number_of v) =  
+        (let pv = number_of (bin_pred v) in  
+         if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
+apply (case_tac " (number_of v) ::nat")
+apply (simp_all (no_asm_simp) add: Let_def neg_number_of_bin_pred_iff_0)
+apply (simp split add: split_if_asm)
+done
+
+lemma nat_rec_add_eq_if [simp]:
+     "nat_rec a f (number_of v + n) =  
+        (let pv = number_of (bin_pred v) in  
+         if neg pv then nat_rec a f n  
+                   else f (nat pv + n) (nat_rec a f (nat pv + n)))"
+apply (subst add_eq_if)
+apply (simp split add: nat.split
+            add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
+                 neg_number_of_bin_pred_iff_0)
+done
+
+
+subsection{*Various Other Lemmas*}
+
+subsubsection{*Evens and Odds, for Mutilated Chess Board*}
+
+(*Case analysis on b<2*)
+lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
+by arith
+
+lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
+apply (subgoal_tac "m mod 2 < 2")
+apply (erule less_2_cases [THEN disjE])
+apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
+done
+
+lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
+apply (subgoal_tac "m mod 2 < 2")
+apply (force simp del: mod_less_divisor, simp) 
+done
+
+subsubsection{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
+
+lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
+by simp
+
+lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
+by simp
+
+declare numeral_0_eq_0 [simp] numeral_1_eq_1 [simp] 
+
+text{*Can be used to eliminate long strings of Sucs, but not by default*}
+lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
+by simp
+
+
+text{*These lemmas collapse some needless occurrences of Suc:
+    at least three Sucs, since two and fewer are rewritten back to Suc again!
+    We already have some rules to simplify operands smaller than 3.*}
+
+lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
+by (simp add: Suc3_eq_add_3)
+
+lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
+by (simp add: Suc3_eq_add_3)
+
+declare Suc_div_eq_add3_div [of _ "number_of v", standard, simp]
+declare Suc_mod_eq_add3_mod [of _ "number_of v", standard, simp]
+
 end
diff -r 5efbb548107d -r e33ffff0123c src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Thu Dec 04 16:16:36 2003 +0100
@@ -420,9 +420,6 @@
 Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
 Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
 
-(*The Abel_Cancel simprocs are now obsolete*)
-Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
-
 (*examples:
 print_depth 22;
 set timing;
diff -r 5efbb548107d -r e33ffff0123c src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Thu Dec 04 16:16:36 2003 +0100
@@ -6,102 +6,6 @@
 Simprocs for nat numerals.
 *)
 
-Goal "number_of v + (number_of v' + (k::nat)) = \
-\        (if neg (number_of v) then number_of v' + k \
-\         else if neg (number_of v') then number_of v + k \
-\         else number_of (bin_add v v') + k)";
-by (Simp_tac 1);
-qed "nat_number_of_add_left";
-
-
-(** For combine_numerals **)
-
-Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)";
-by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1);
-qed "left_add_mult_distrib";
-
-
-(** For cancel_numerals **)
-
-Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]
-                            addsimps [add_mult_distrib]) 1);
-qed "nat_diff_add_eq1";
-
-Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]
-                            addsimps [add_mult_distrib]) 1);
-qed "nat_diff_add_eq2";
-
-Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
-                                  addsimps [add_mult_distrib]));
-qed "nat_eq_add_iff1";
-
-Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
-                                  addsimps [add_mult_distrib]));
-qed "nat_eq_add_iff2";
-
-Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
-                                  addsimps [add_mult_distrib]));
-qed "nat_less_add_iff1";
-
-Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
-                                  addsimps [add_mult_distrib]));
-qed "nat_less_add_iff2";
-
-Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
-                                  addsimps [add_mult_distrib]));
-qed "nat_le_add_iff1";
-
-Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
-                                  addsimps [add_mult_distrib]));
-qed "nat_le_add_iff2";
-
-
-(** For cancel_numeral_factors **)
-
-Goal "(0::nat) < k ==> (k*m <= k*n) = (m<=n)";
-by Auto_tac;
-qed "nat_mult_le_cancel1";
-
-Goal "(0::nat) < k ==> (k*m < k*n) = (m<n)";
-by Auto_tac;
-qed "nat_mult_less_cancel1";
-
-Goal "(0::nat) < k ==> (k*m = k*n) = (m=n)";
-by Auto_tac;
-qed "nat_mult_eq_cancel1";
-
-Goal "(0::nat) < k ==> (k*m) div (k*n) = (m div n)";
-by Auto_tac;
-qed "nat_mult_div_cancel1";
-
-
-(** For cancel_factor **)
-
-Goal "(k*m <= k*n) = ((0::nat) < k --> m<=n)";
-by Auto_tac;
-qed "nat_mult_le_cancel_disj";
-
-Goal "(k*m < k*n) = ((0::nat) < k & m<n)";
-by Auto_tac;
-qed "nat_mult_less_cancel_disj";
-
-Goal "(k*m = k*n) = (k = (0::nat) | m=n)";
-by Auto_tac;
-qed "nat_mult_eq_cancel_disj";
-
-Goal "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)";
-by (simp_tac (simpset() addsimps [nat_mult_div_cancel1]) 1);
-qed "nat_mult_div_cancel_disj";
-
-
 structure Nat_Numeral_Simprocs =
 struct
 
diff -r 5efbb548107d -r e33ffff0123c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Dec 04 10:29:17 2003 +0100
+++ b/src/HOL/IsaMakefile	Thu Dec 04 16:16:36 2003 +0100
@@ -88,8 +88,7 @@
   Integ/cooper_dec.ML Integ/cooper_proof.ML \
   Integ/Equiv.thy Integ/Int.thy Integ/IntArith.thy Integ/IntDef.thy \
   Integ/IntDiv.thy Integ/IntPower.thy \
-  Integ/NatBin.thy Integ/NatSimprocs.ML \
-  Integ/NatSimprocs.thy Integ/int_arith1.ML \
+  Integ/NatBin.thy Integ/NatSimprocs.thy Integ/int_arith1.ML \
   Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
   Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
   Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \