# HG changeset patch
# User huffman
# Date 1182309519 -7200
# Node ID 25ca91279a9b65a4aa8696da5806d79e81b08915
# Parent  771117253634ba292630d3088f26a69dc69da766
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems

diff -r 771117253634 -r 25ca91279a9b src/HOL/Hyperreal/Deriv.thy
--- a/src/HOL/Hyperreal/Deriv.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -205,14 +205,14 @@
 lemma DERIV_power_Suc:
   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
   assumes f: "DERIV f x :> D"
-  shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (of_nat n + 1) * (D * f x ^ n)"
+  shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
 proof (induct n)
 case 0
   show ?case by (simp add: power_Suc f)
 case (Suc k)
   from DERIV_mult' [OF f Suc] show ?case
     apply (simp only: of_nat_Suc left_distrib mult_1_left)
-    apply (simp only: power_Suc right_distrib mult_ac)
+    apply (simp only: power_Suc right_distrib mult_ac add_ac)
     done
 qed
 
diff -r 771117253634 -r 25ca91279a9b src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -374,7 +374,7 @@
 lemma of_hypnat_1 [simp]: "of_hypnat 1 = 1"
 by transfer (rule of_nat_1)
 
-lemma of_hypnat_hSuc: "\<And>m. of_hypnat (hSuc m) = of_hypnat m + 1"
+lemma of_hypnat_hSuc: "\<And>m. of_hypnat (hSuc m) = 1 + of_hypnat m"
 by transfer (rule of_nat_Suc)
 
 lemma of_hypnat_add [simp]:
diff -r 771117253634 -r 25ca91279a9b src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -556,7 +556,7 @@
 
 lemma exp_fdiffs: 
       "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
-by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def
+by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult
          del: mult_Suc of_nat_Suc)
 
 lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
@@ -569,7 +569,7 @@
                  -1 ^ (n div 2)/(real (fact n))  
               else 0)"
 by (auto intro!: ext 
-         simp add: diffs_def divide_inverse real_of_nat_def
+         simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult
          simp del: mult_Suc of_nat_Suc)
 
 lemma sin_fdiffs2: 
@@ -586,7 +586,7 @@
        = (%n. - (if even n then 0  
            else -1 ^ ((n - Suc 0)div 2)/(real (fact n))))"
 by (auto intro!: ext 
-         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def
+         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult
          simp del: mult_Suc of_nat_Suc)
 
 
diff -r 771117253634 -r 25ca91279a9b src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/IntDef.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -365,9 +365,6 @@
 lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
 by simp
 
-lemma int_Suc: "int (Suc m) = 1 + (int m)"
-by simp
-
 lemma int_Suc0_eq_1: "int (Suc 0) = 1"
 by simp
 
@@ -506,7 +503,7 @@
 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
 apply (cases w, cases z)
 apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
-                 mult add_ac)
+                 mult add_ac of_nat_mult)
 done
 
 lemma of_int_le_iff [simp]:
@@ -645,7 +642,7 @@
 
 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
   apply (cases "finite A")
-  apply (erule finite_induct, auto)
+  apply (erule finite_induct, auto simp add: of_nat_mult)
   done
 
 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
@@ -712,41 +709,41 @@
 
 subsection {* Legacy theorems *}
 
-lemmas zminus_zminus = minus_minus [where 'a=int]
+lemmas zminus_zminus = minus_minus [of "?z::int"]
 lemmas zminus_0 = minus_zero [where 'a=int]
-lemmas zminus_zadd_distrib = minus_add_distrib [where 'a=int]
-lemmas zadd_commute = add_commute [where 'a=int]
-lemmas zadd_assoc = add_assoc [where 'a=int]
-lemmas zadd_left_commute = add_left_commute [where 'a=int]
+lemmas zminus_zadd_distrib = minus_add_distrib [of "?z::int" "?w"]
+lemmas zadd_commute = add_commute [of "?z::int" "?w"]
+lemmas zadd_assoc = add_assoc [of "?z1.0::int" "?z2.0" "?z3.0"]
+lemmas zadd_left_commute = add_left_commute [of "?x::int" "?y" "?z"]
 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
 lemmas zmult_ac = OrderedGroup.mult_ac
-lemmas zadd_0 = OrderedGroup.add_0_left [where 'a=int]
-lemmas zadd_0_right = OrderedGroup.add_0_left [where 'a=int]
-lemmas zadd_zminus_inverse2 = left_minus [where 'a=int]
-lemmas zmult_zminus = mult_minus_left [where 'a=int]
-lemmas zmult_commute = mult_commute [where 'a=int]
-lemmas zmult_assoc = mult_assoc [where 'a=int]
-lemmas zadd_zmult_distrib = left_distrib [where 'a=int]
-lemmas zadd_zmult_distrib2 = right_distrib [where 'a=int]
-lemmas zdiff_zmult_distrib = left_diff_distrib [where 'a=int]
-lemmas zdiff_zmult_distrib2 = right_diff_distrib [where 'a=int]
+lemmas zadd_0 = OrderedGroup.add_0_left [of "?z::int"]
+lemmas zadd_0_right = OrderedGroup.add_0_left [of "?z::int"]
+lemmas zadd_zminus_inverse2 = left_minus [of "?z::int"]
+lemmas zmult_zminus = mult_minus_left [of "?z::int" "?w"]
+lemmas zmult_commute = mult_commute [of "?z::int" "?w"]
+lemmas zmult_assoc = mult_assoc [of "?z1.0::int" "?z2.0" "?z3.0"]
+lemmas zadd_zmult_distrib = left_distrib [of "?z1.0::int" "?z2.0" "?w"]
+lemmas zadd_zmult_distrib2 = right_distrib [of "?w::int" "?z1.0" "?z2.0"]
+lemmas zdiff_zmult_distrib = left_diff_distrib [of "?z1.0::int" "?z2.0" "?w"]
+lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "?w::int" "?z1.0" "?z2.0"]
 
 lemmas int_distrib =
   zadd_zmult_distrib zadd_zmult_distrib2
   zdiff_zmult_distrib zdiff_zmult_distrib2
 
-lemmas zmult_1 = mult_1_left [where 'a=int]
-lemmas zmult_1_right = mult_1_right [where 'a=int]
+lemmas zmult_1 = mult_1_left [of "?z::int"]
+lemmas zmult_1_right = mult_1_right [of "?z::int"]
 
-lemmas zle_refl = order_refl [where 'a=int]
+lemmas zle_refl = order_refl [of "?w::int"]
 lemmas zle_trans = order_trans [where 'a=int and x="?i" and y="?j" and z="?k"]
-lemmas zle_anti_sym = order_antisym [where 'a=int]
-lemmas zle_linear = linorder_linear [where 'a=int]
+lemmas zle_anti_sym = order_antisym [of "?z::int" "?w"]
+lemmas zle_linear = linorder_linear [of "?z::int" "?w"]
 lemmas zless_linear = linorder_less_linear [where 'a = int]
 
-lemmas zadd_left_mono = add_left_mono [where 'a=int]
-lemmas zadd_strict_right_mono = add_strict_right_mono [where 'a=int]
-lemmas zadd_zless_mono = add_less_le_mono [where 'a=int]
+lemmas zadd_left_mono = add_left_mono [of "?i::int" "?j" "?k"]
+lemmas zadd_strict_right_mono = add_strict_right_mono [of "?i::int" "?j" "?k"]
+lemmas zadd_zless_mono = add_less_le_mono [of "?w'::int" "?w" "?z'" "?z"]
 
 lemmas int_0_less_1 = zero_less_one [where 'a=int]
 lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
@@ -756,16 +753,17 @@
 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
 lemmas int_mult = of_nat_mult [where 'a=int]
 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
-lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int]
+lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="?n"]
 lemmas zless_int = of_nat_less_iff [where 'a=int]
-lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int]
+lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="?k"]
 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
 lemmas zle_int = of_nat_le_iff [where 'a=int]
 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
-lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int]
+lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="?n"]
 lemmas int_0 = of_nat_0 [where ?'a_1.0=int]
 lemmas int_1 = of_nat_1 [where 'a=int]
-lemmas abs_int_eq = abs_of_nat [where 'a=int]
+lemmas int_Suc = of_nat_Suc [where ?'a_1.0=int]
+lemmas abs_int_eq = abs_of_nat [where 'a=int and n="?m"]
 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
 lemmas int_setsum = of_nat_setsum [where 'a=int]
 lemmas int_setprod = of_nat_setprod [where 'a=int]
diff -r 771117253634 -r 25ca91279a9b src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/IntDiv.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -1242,10 +1242,8 @@
   done
 
 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
-  unfolding dvd_def
-  apply (rule_tac s="\<exists>k. int y = int x * int k" in trans)
-  apply (simp only: of_nat_mult [symmetric] of_nat_eq_iff)
-  apply (simp add: ex_nat cong add: conj_cong)
+  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
+    nat_0_le cong add: conj_cong)
   apply (rule iffI)
   apply iprover
   apply (erule exE)
@@ -1255,7 +1253,7 @@
   apply (case_tac "0 \<le> k")
   apply iprover
   apply (simp add: linorder_not_le)
-  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF of_nat_0_less_iff]])
+  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   apply assumption
   apply (simp add: mult_ac)
   done
@@ -1284,24 +1282,24 @@
   apply (auto simp add: dvd_def nat_abs_mult_distrib)
   apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
    apply (rule_tac x = "-(int k)" in exI)
-  apply auto
+  apply (auto simp add: int_mult)
   done
 
 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
-  apply (auto simp add: dvd_def abs_if)
+  apply (auto simp add: dvd_def abs_if int_mult)
     apply (rule_tac [3] x = "nat k" in exI)
     apply (rule_tac [2] x = "-(int k)" in exI)
     apply (rule_tac x = "nat (-k)" in exI)
-    apply (cut_tac [3] m = m in int_less_0_conv)
-    apply (cut_tac m = m in int_less_0_conv)
+    apply (cut_tac [3] k = m in int_less_0_conv)
+    apply (cut_tac k = m in int_less_0_conv)
     apply (auto simp add: zero_le_mult_iff mult_less_0_iff
       nat_mult_distrib [symmetric] nat_eq_iff2)
   done
 
 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
-  apply (auto simp add: dvd_def)
+  apply (auto simp add: dvd_def int_mult)
   apply (rule_tac x = "nat k" in exI)
-  apply (cut_tac m = m in int_less_0_conv)
+  apply (cut_tac k = m in int_less_0_conv)
   apply (auto simp add: zero_le_mult_iff mult_less_0_iff
     nat_mult_distrib [symmetric] nat_eq_iff2)
   done
@@ -1377,7 +1375,7 @@
 apply (subst split_div, auto)
 apply (subst split_zdiv, auto)
 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
-apply (auto simp add: IntDiv.quorem_def)
+apply (auto simp add: IntDiv.quorem_def of_nat_mult)
 done
 
 lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
@@ -1385,7 +1383,7 @@
 apply (subst split_zmod, auto)
 apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
        in unique_remainder)
-apply (auto simp add: IntDiv.quorem_def)
+apply (auto simp add: IntDiv.quorem_def of_nat_mult)
 done
 
 text{*Suggested by Matthias Daum*}
diff -r 771117253634 -r 25ca91279a9b src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Library/GCD.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -265,7 +265,7 @@
   from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
     unfolding dvd_def by blast
   from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
-  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by simp
+  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
   then show ?thesis
     apply (subst zdvd_abs1 [symmetric])
     apply (subst zdvd_abs2 [symmetric])
diff -r 771117253634 -r 25ca91279a9b src/HOL/Library/Parity.thy
--- a/src/HOL/Library/Parity.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Library/Parity.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -20,7 +20,7 @@
   even_def: "even x \<equiv> x mod 2 = 0" ..
 
 instance nat :: even_odd
-  even_nat_def: "even x \<equiv> even (int_of_nat x)" ..
+  even_nat_def: "even x \<equiv> even (int x)" ..
 
 
 subsection {* Even and odd are mutually exclusive *}
@@ -135,7 +135,7 @@
   by (simp add: even_nat_def)
 
 lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
-  by (simp add: even_nat_def)
+  by (simp add: even_nat_def int_mult)
 
 lemma even_nat_sum: "even ((x::nat) + y) =
     ((even x & even y) | (odd x & odd y))"
@@ -152,7 +152,7 @@
   by (simp add: even_nat_def)
 
 lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
-  by (simp add: even_nat_def of_nat_power)
+  by (simp add: even_nat_def int_power)
 
 lemma even_nat_zero: "even (0::nat)"
   by (simp add: even_nat_def)
diff -r 771117253634 -r 25ca91279a9b src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Library/Word.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -927,12 +927,12 @@
 next
   fix xs
   assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
-  show "bv_to_int (norm_signed (\<one>#xs)) = - int (bv_to_nat (bv_not xs)) + -1"
+  show "bv_to_int (norm_signed (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
   proof (rule bit_list_cases [of xs], simp_all)
     fix ys
     assume [simp]: "xs = \<one>#ys"
     from ind
-    show "bv_to_int (norm_signed (\<one>#ys)) = - int (bv_to_nat (bv_not ys)) + -1"
+    show "bv_to_int (norm_signed (\<one>#ys)) = -1 - int (bv_to_nat (bv_not ys))"
       by simp
   qed
 qed
@@ -945,9 +945,9 @@
     by (simp add: int_nat_two_exp)
 next
   fix bs
-  have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0" by simp
+  have "-1 - int (bv_to_nat (bv_not bs)) \<le> 0" by simp
   also have "... < 2 ^ length bs" by (induct bs) simp_all
-  finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" .
+  finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs" .
 qed
 
 lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w"
@@ -959,7 +959,7 @@
 next
   fix bs
   from bv_to_nat_upper_range [of "bv_not bs"]
-  show "- (2 ^ length bs) \<le> - int (bv_to_nat (bv_not bs)) + -1"
+  show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
     by (simp add: int_nat_two_exp)
 qed
 
diff -r 771117253634 -r 25ca91279a9b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Nat.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -1298,7 +1298,7 @@
 
 primrec
   of_nat_0:   "of_nat 0 = 0"
-  of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
+  of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
 
 lemma of_nat_id [simp]: "(of_nat n \<Colon> nat) = n"
   by (induct n) auto
@@ -1309,19 +1309,20 @@
 lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
   by (induct m) (simp_all add: add_ac)
 
-lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
+lemma of_nat_mult: "of_nat (m*n) = of_nat m * of_nat n"
   by (induct m) (simp_all add: add_ac left_distrib)
 
 lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
   apply (induct m, simp_all)
   apply (erule order_trans)
+  apply (rule ord_le_eq_trans [OF _ add_commute])
   apply (rule less_add_one [THEN order_less_imp_le])
   done
 
 lemma less_imp_of_nat_less:
     "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
   apply (induct m n rule: diff_induct, simp_all)
-  apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
+  apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
   done
 
 lemma of_nat_less_imp_less:
diff -r 771117253634 -r 25ca91279a9b src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -85,7 +85,7 @@
   (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1
    else fib (Suc n) * fib (Suc n) + 1)"
   apply (rule int_int_eq [THEN iffD1]) 
-  apply (simp add: fib_Cassini_int del: of_nat_mult) 
+  apply (simp add: fib_Cassini_int)
   apply (subst zdiff_int [symmetric]) 
    apply (insert fib_Suc_gr_0 [of n], simp_all)
   done
diff -r 771117253634 -r 25ca91279a9b src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -281,7 +281,7 @@
 
 lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
   using P_set_card Q_set_card P_set_finite Q_set_finite
-  by (auto simp add: S_def setsum_constant)
+  by (auto simp add: S_def zmult_int setsum_constant)
 
 lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
   by (auto simp add: S1_def S2_def)
diff -r 771117253634 -r 25ca91279a9b src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Power.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -333,7 +333,7 @@
 
 lemma of_nat_power:
   "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
-by (induct n, simp_all add: power_Suc)
+by (induct n, simp_all add: power_Suc of_nat_mult)
 
 lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
 by (insert one_le_power [of i n], simp)
diff -r 771117253634 -r 25ca91279a9b src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Real/Float.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -35,8 +35,7 @@
     apply (auto, induct_tac n)
     apply (simp_all add: pow2_def)
     apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
-    apply (auto simp add: h)
-    by (simp add: add_commute)
+    by (auto simp add: h)
   show ?thesis
   proof (induct a)
     case (1 n)
@@ -46,7 +45,7 @@
     show ?case
       apply (auto)
       apply (subst pow2_neg[of "- int n"])
-      apply (subst pow2_neg[of "- int n + -1"])
+      apply (subst pow2_neg[of "-1 - int n"])
       apply (auto simp add: g pos)
       done
   qed
@@ -269,18 +268,10 @@
   norm_float :: "int*int \<Rightarrow> int*int"
 
 lemma int_div_zdiv: "int (a div b) = (int a) div (int b)"
-apply (subst split_div, auto)
-apply (subst split_zdiv, auto)
-apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
-apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
-done
+by (rule zdiv_int)
 
 lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)"
-apply (subst split_mod, auto)
-apply (subst split_zmod, auto)
-apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia in IntDiv.unique_remainder)
-apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
-done
+by (rule zmod_int)
 
 lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
 by arith
diff -r 771117253634 -r 25ca91279a9b src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -712,7 +712,7 @@
 by (simp add: real_of_nat_def del: of_nat_Suc)
 
 lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
-by (simp add: real_of_nat_def)
+by (simp add: real_of_nat_def of_nat_mult)
 
 lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 
     (SUM x:A. real(f x))"
diff -r 771117253634 -r 25ca91279a9b src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/SetInterval.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -756,7 +756,7 @@
   show ?case by simp
 next
   case (Suc n)
-  then show ?case by (simp add: right_distrib add_assoc mult_ac)
+  then show ?case by (simp add: ring_eq_simps)
 qed
 
 theorem arith_series_general:
@@ -779,7 +779,7 @@
   also from ngt1 
   have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
     by (simp only: mult_ac gauss_sum [of "n - 1"])
-       (simp add:  mult_ac of_nat_Suc [symmetric])
+       (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
   finally show ?thesis by (simp add: mult_ac add_ac right_distrib)
 next
   assume "\<not>(n > 1)"
diff -r 771117253634 -r 25ca91279a9b src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/ex/NatSum.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -106,7 +106,7 @@
   "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
     of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
     (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
-  by (induct m) simp_all
+  by (induct m) (simp_all add: of_nat_mult)
 
 
 text {*