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
authorhuffman
Wed Jun 20 05:18:39 2007 +0200 (2007-06-20)
changeset 2343125ca91279a9b
parent 23430 771117253634
child 23432 cec811764a38
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
src/HOL/Hyperreal/Deriv.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/IntDef.thy
src/HOL/IntDiv.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Word.thy
src/HOL/Nat.thy
src/HOL/NumberTheory/Fib.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/Power.thy
src/HOL/Real/Float.thy
src/HOL/Real/RealDef.thy
src/HOL/SetInterval.thy
src/HOL/ex/NatSum.thy
     1.1 --- a/src/HOL/Hyperreal/Deriv.thy	Wed Jun 20 05:06:56 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Deriv.thy	Wed Jun 20 05:18:39 2007 +0200
     1.3 @@ -205,14 +205,14 @@
     1.4  lemma DERIV_power_Suc:
     1.5    fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
     1.6    assumes f: "DERIV f x :> D"
     1.7 -  shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (of_nat n + 1) * (D * f x ^ n)"
     1.8 +  shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
     1.9  proof (induct n)
    1.10  case 0
    1.11    show ?case by (simp add: power_Suc f)
    1.12  case (Suc k)
    1.13    from DERIV_mult' [OF f Suc] show ?case
    1.14      apply (simp only: of_nat_Suc left_distrib mult_1_left)
    1.15 -    apply (simp only: power_Suc right_distrib mult_ac)
    1.16 +    apply (simp only: power_Suc right_distrib mult_ac add_ac)
    1.17      done
    1.18  qed
    1.19  
     2.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Wed Jun 20 05:06:56 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Jun 20 05:18:39 2007 +0200
     2.3 @@ -374,7 +374,7 @@
     2.4  lemma of_hypnat_1 [simp]: "of_hypnat 1 = 1"
     2.5  by transfer (rule of_nat_1)
     2.6  
     2.7 -lemma of_hypnat_hSuc: "\<And>m. of_hypnat (hSuc m) = of_hypnat m + 1"
     2.8 +lemma of_hypnat_hSuc: "\<And>m. of_hypnat (hSuc m) = 1 + of_hypnat m"
     2.9  by transfer (rule of_nat_Suc)
    2.10  
    2.11  lemma of_hypnat_add [simp]:
     3.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jun 20 05:06:56 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jun 20 05:18:39 2007 +0200
     3.3 @@ -556,7 +556,7 @@
     3.4  
     3.5  lemma exp_fdiffs: 
     3.6        "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
     3.7 -by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def
     3.8 +by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult
     3.9           del: mult_Suc of_nat_Suc)
    3.10  
    3.11  lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
    3.12 @@ -569,7 +569,7 @@
    3.13                   -1 ^ (n div 2)/(real (fact n))  
    3.14                else 0)"
    3.15  by (auto intro!: ext 
    3.16 -         simp add: diffs_def divide_inverse real_of_nat_def
    3.17 +         simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult
    3.18           simp del: mult_Suc of_nat_Suc)
    3.19  
    3.20  lemma sin_fdiffs2: 
    3.21 @@ -586,7 +586,7 @@
    3.22         = (%n. - (if even n then 0  
    3.23             else -1 ^ ((n - Suc 0)div 2)/(real (fact n))))"
    3.24  by (auto intro!: ext 
    3.25 -         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def
    3.26 +         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult
    3.27           simp del: mult_Suc of_nat_Suc)
    3.28  
    3.29  
     4.1 --- a/src/HOL/IntDef.thy	Wed Jun 20 05:06:56 2007 +0200
     4.2 +++ b/src/HOL/IntDef.thy	Wed Jun 20 05:18:39 2007 +0200
     4.3 @@ -365,9 +365,6 @@
     4.4  lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
     4.5  by simp
     4.6  
     4.7 -lemma int_Suc: "int (Suc m) = 1 + (int m)"
     4.8 -by simp
     4.9 -
    4.10  lemma int_Suc0_eq_1: "int (Suc 0) = 1"
    4.11  by simp
    4.12  
    4.13 @@ -506,7 +503,7 @@
    4.14  lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
    4.15  apply (cases w, cases z)
    4.16  apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
    4.17 -                 mult add_ac)
    4.18 +                 mult add_ac of_nat_mult)
    4.19  done
    4.20  
    4.21  lemma of_int_le_iff [simp]:
    4.22 @@ -645,7 +642,7 @@
    4.23  
    4.24  lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    4.25    apply (cases "finite A")
    4.26 -  apply (erule finite_induct, auto)
    4.27 +  apply (erule finite_induct, auto simp add: of_nat_mult)
    4.28    done
    4.29  
    4.30  lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
    4.31 @@ -712,41 +709,41 @@
    4.32  
    4.33  subsection {* Legacy theorems *}
    4.34  
    4.35 -lemmas zminus_zminus = minus_minus [where 'a=int]
    4.36 +lemmas zminus_zminus = minus_minus [of "?z::int"]
    4.37  lemmas zminus_0 = minus_zero [where 'a=int]
    4.38 -lemmas zminus_zadd_distrib = minus_add_distrib [where 'a=int]
    4.39 -lemmas zadd_commute = add_commute [where 'a=int]
    4.40 -lemmas zadd_assoc = add_assoc [where 'a=int]
    4.41 -lemmas zadd_left_commute = add_left_commute [where 'a=int]
    4.42 +lemmas zminus_zadd_distrib = minus_add_distrib [of "?z::int" "?w"]
    4.43 +lemmas zadd_commute = add_commute [of "?z::int" "?w"]
    4.44 +lemmas zadd_assoc = add_assoc [of "?z1.0::int" "?z2.0" "?z3.0"]
    4.45 +lemmas zadd_left_commute = add_left_commute [of "?x::int" "?y" "?z"]
    4.46  lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
    4.47  lemmas zmult_ac = OrderedGroup.mult_ac
    4.48 -lemmas zadd_0 = OrderedGroup.add_0_left [where 'a=int]
    4.49 -lemmas zadd_0_right = OrderedGroup.add_0_left [where 'a=int]
    4.50 -lemmas zadd_zminus_inverse2 = left_minus [where 'a=int]
    4.51 -lemmas zmult_zminus = mult_minus_left [where 'a=int]
    4.52 -lemmas zmult_commute = mult_commute [where 'a=int]
    4.53 -lemmas zmult_assoc = mult_assoc [where 'a=int]
    4.54 -lemmas zadd_zmult_distrib = left_distrib [where 'a=int]
    4.55 -lemmas zadd_zmult_distrib2 = right_distrib [where 'a=int]
    4.56 -lemmas zdiff_zmult_distrib = left_diff_distrib [where 'a=int]
    4.57 -lemmas zdiff_zmult_distrib2 = right_diff_distrib [where 'a=int]
    4.58 +lemmas zadd_0 = OrderedGroup.add_0_left [of "?z::int"]
    4.59 +lemmas zadd_0_right = OrderedGroup.add_0_left [of "?z::int"]
    4.60 +lemmas zadd_zminus_inverse2 = left_minus [of "?z::int"]
    4.61 +lemmas zmult_zminus = mult_minus_left [of "?z::int" "?w"]
    4.62 +lemmas zmult_commute = mult_commute [of "?z::int" "?w"]
    4.63 +lemmas zmult_assoc = mult_assoc [of "?z1.0::int" "?z2.0" "?z3.0"]
    4.64 +lemmas zadd_zmult_distrib = left_distrib [of "?z1.0::int" "?z2.0" "?w"]
    4.65 +lemmas zadd_zmult_distrib2 = right_distrib [of "?w::int" "?z1.0" "?z2.0"]
    4.66 +lemmas zdiff_zmult_distrib = left_diff_distrib [of "?z1.0::int" "?z2.0" "?w"]
    4.67 +lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "?w::int" "?z1.0" "?z2.0"]
    4.68  
    4.69  lemmas int_distrib =
    4.70    zadd_zmult_distrib zadd_zmult_distrib2
    4.71    zdiff_zmult_distrib zdiff_zmult_distrib2
    4.72  
    4.73 -lemmas zmult_1 = mult_1_left [where 'a=int]
    4.74 -lemmas zmult_1_right = mult_1_right [where 'a=int]
    4.75 +lemmas zmult_1 = mult_1_left [of "?z::int"]
    4.76 +lemmas zmult_1_right = mult_1_right [of "?z::int"]
    4.77  
    4.78 -lemmas zle_refl = order_refl [where 'a=int]
    4.79 +lemmas zle_refl = order_refl [of "?w::int"]
    4.80  lemmas zle_trans = order_trans [where 'a=int and x="?i" and y="?j" and z="?k"]
    4.81 -lemmas zle_anti_sym = order_antisym [where 'a=int]
    4.82 -lemmas zle_linear = linorder_linear [where 'a=int]
    4.83 +lemmas zle_anti_sym = order_antisym [of "?z::int" "?w"]
    4.84 +lemmas zle_linear = linorder_linear [of "?z::int" "?w"]
    4.85  lemmas zless_linear = linorder_less_linear [where 'a = int]
    4.86  
    4.87 -lemmas zadd_left_mono = add_left_mono [where 'a=int]
    4.88 -lemmas zadd_strict_right_mono = add_strict_right_mono [where 'a=int]
    4.89 -lemmas zadd_zless_mono = add_less_le_mono [where 'a=int]
    4.90 +lemmas zadd_left_mono = add_left_mono [of "?i::int" "?j" "?k"]
    4.91 +lemmas zadd_strict_right_mono = add_strict_right_mono [of "?i::int" "?j" "?k"]
    4.92 +lemmas zadd_zless_mono = add_less_le_mono [of "?w'::int" "?w" "?z'" "?z"]
    4.93  
    4.94  lemmas int_0_less_1 = zero_less_one [where 'a=int]
    4.95  lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
    4.96 @@ -756,16 +753,17 @@
    4.97  lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
    4.98  lemmas int_mult = of_nat_mult [where 'a=int]
    4.99  lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
   4.100 -lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int]
   4.101 +lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="?n"]
   4.102  lemmas zless_int = of_nat_less_iff [where 'a=int]
   4.103 -lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int]
   4.104 +lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="?k"]
   4.105  lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
   4.106  lemmas zle_int = of_nat_le_iff [where 'a=int]
   4.107  lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
   4.108 -lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int]
   4.109 +lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="?n"]
   4.110  lemmas int_0 = of_nat_0 [where ?'a_1.0=int]
   4.111  lemmas int_1 = of_nat_1 [where 'a=int]
   4.112 -lemmas abs_int_eq = abs_of_nat [where 'a=int]
   4.113 +lemmas int_Suc = of_nat_Suc [where ?'a_1.0=int]
   4.114 +lemmas abs_int_eq = abs_of_nat [where 'a=int and n="?m"]
   4.115  lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
   4.116  lemmas int_setsum = of_nat_setsum [where 'a=int]
   4.117  lemmas int_setprod = of_nat_setprod [where 'a=int]
     5.1 --- a/src/HOL/IntDiv.thy	Wed Jun 20 05:06:56 2007 +0200
     5.2 +++ b/src/HOL/IntDiv.thy	Wed Jun 20 05:18:39 2007 +0200
     5.3 @@ -1242,10 +1242,8 @@
     5.4    done
     5.5  
     5.6  theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
     5.7 -  unfolding dvd_def
     5.8 -  apply (rule_tac s="\<exists>k. int y = int x * int k" in trans)
     5.9 -  apply (simp only: of_nat_mult [symmetric] of_nat_eq_iff)
    5.10 -  apply (simp add: ex_nat cong add: conj_cong)
    5.11 +  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
    5.12 +    nat_0_le cong add: conj_cong)
    5.13    apply (rule iffI)
    5.14    apply iprover
    5.15    apply (erule exE)
    5.16 @@ -1255,7 +1253,7 @@
    5.17    apply (case_tac "0 \<le> k")
    5.18    apply iprover
    5.19    apply (simp add: linorder_not_le)
    5.20 -  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF of_nat_0_less_iff]])
    5.21 +  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
    5.22    apply assumption
    5.23    apply (simp add: mult_ac)
    5.24    done
    5.25 @@ -1284,24 +1282,24 @@
    5.26    apply (auto simp add: dvd_def nat_abs_mult_distrib)
    5.27    apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
    5.28     apply (rule_tac x = "-(int k)" in exI)
    5.29 -  apply auto
    5.30 +  apply (auto simp add: int_mult)
    5.31    done
    5.32  
    5.33  lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
    5.34 -  apply (auto simp add: dvd_def abs_if)
    5.35 +  apply (auto simp add: dvd_def abs_if int_mult)
    5.36      apply (rule_tac [3] x = "nat k" in exI)
    5.37      apply (rule_tac [2] x = "-(int k)" in exI)
    5.38      apply (rule_tac x = "nat (-k)" in exI)
    5.39 -    apply (cut_tac [3] m = m in int_less_0_conv)
    5.40 -    apply (cut_tac m = m in int_less_0_conv)
    5.41 +    apply (cut_tac [3] k = m in int_less_0_conv)
    5.42 +    apply (cut_tac k = m in int_less_0_conv)
    5.43      apply (auto simp add: zero_le_mult_iff mult_less_0_iff
    5.44        nat_mult_distrib [symmetric] nat_eq_iff2)
    5.45    done
    5.46  
    5.47  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
    5.48 -  apply (auto simp add: dvd_def)
    5.49 +  apply (auto simp add: dvd_def int_mult)
    5.50    apply (rule_tac x = "nat k" in exI)
    5.51 -  apply (cut_tac m = m in int_less_0_conv)
    5.52 +  apply (cut_tac k = m in int_less_0_conv)
    5.53    apply (auto simp add: zero_le_mult_iff mult_less_0_iff
    5.54      nat_mult_distrib [symmetric] nat_eq_iff2)
    5.55    done
    5.56 @@ -1377,7 +1375,7 @@
    5.57  apply (subst split_div, auto)
    5.58  apply (subst split_zdiv, auto)
    5.59  apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
    5.60 -apply (auto simp add: IntDiv.quorem_def)
    5.61 +apply (auto simp add: IntDiv.quorem_def of_nat_mult)
    5.62  done
    5.63  
    5.64  lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
    5.65 @@ -1385,7 +1383,7 @@
    5.66  apply (subst split_zmod, auto)
    5.67  apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
    5.68         in unique_remainder)
    5.69 -apply (auto simp add: IntDiv.quorem_def)
    5.70 +apply (auto simp add: IntDiv.quorem_def of_nat_mult)
    5.71  done
    5.72  
    5.73  text{*Suggested by Matthias Daum*}
     6.1 --- a/src/HOL/Library/GCD.thy	Wed Jun 20 05:06:56 2007 +0200
     6.2 +++ b/src/HOL/Library/GCD.thy	Wed Jun 20 05:18:39 2007 +0200
     6.3 @@ -265,7 +265,7 @@
     6.4    from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
     6.5      unfolding dvd_def by blast
     6.6    from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
     6.7 -  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by simp
     6.8 +  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
     6.9    then show ?thesis
    6.10      apply (subst zdvd_abs1 [symmetric])
    6.11      apply (subst zdvd_abs2 [symmetric])
     7.1 --- a/src/HOL/Library/Parity.thy	Wed Jun 20 05:06:56 2007 +0200
     7.2 +++ b/src/HOL/Library/Parity.thy	Wed Jun 20 05:18:39 2007 +0200
     7.3 @@ -20,7 +20,7 @@
     7.4    even_def: "even x \<equiv> x mod 2 = 0" ..
     7.5  
     7.6  instance nat :: even_odd
     7.7 -  even_nat_def: "even x \<equiv> even (int_of_nat x)" ..
     7.8 +  even_nat_def: "even x \<equiv> even (int x)" ..
     7.9  
    7.10  
    7.11  subsection {* Even and odd are mutually exclusive *}
    7.12 @@ -135,7 +135,7 @@
    7.13    by (simp add: even_nat_def)
    7.14  
    7.15  lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
    7.16 -  by (simp add: even_nat_def)
    7.17 +  by (simp add: even_nat_def int_mult)
    7.18  
    7.19  lemma even_nat_sum: "even ((x::nat) + y) =
    7.20      ((even x & even y) | (odd x & odd y))"
    7.21 @@ -152,7 +152,7 @@
    7.22    by (simp add: even_nat_def)
    7.23  
    7.24  lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
    7.25 -  by (simp add: even_nat_def of_nat_power)
    7.26 +  by (simp add: even_nat_def int_power)
    7.27  
    7.28  lemma even_nat_zero: "even (0::nat)"
    7.29    by (simp add: even_nat_def)
     8.1 --- a/src/HOL/Library/Word.thy	Wed Jun 20 05:06:56 2007 +0200
     8.2 +++ b/src/HOL/Library/Word.thy	Wed Jun 20 05:18:39 2007 +0200
     8.3 @@ -927,12 +927,12 @@
     8.4  next
     8.5    fix xs
     8.6    assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
     8.7 -  show "bv_to_int (norm_signed (\<one>#xs)) = - int (bv_to_nat (bv_not xs)) + -1"
     8.8 +  show "bv_to_int (norm_signed (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
     8.9    proof (rule bit_list_cases [of xs], simp_all)
    8.10      fix ys
    8.11      assume [simp]: "xs = \<one>#ys"
    8.12      from ind
    8.13 -    show "bv_to_int (norm_signed (\<one>#ys)) = - int (bv_to_nat (bv_not ys)) + -1"
    8.14 +    show "bv_to_int (norm_signed (\<one>#ys)) = -1 - int (bv_to_nat (bv_not ys))"
    8.15        by simp
    8.16    qed
    8.17  qed
    8.18 @@ -945,9 +945,9 @@
    8.19      by (simp add: int_nat_two_exp)
    8.20  next
    8.21    fix bs
    8.22 -  have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0" by simp
    8.23 +  have "-1 - int (bv_to_nat (bv_not bs)) \<le> 0" by simp
    8.24    also have "... < 2 ^ length bs" by (induct bs) simp_all
    8.25 -  finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" .
    8.26 +  finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs" .
    8.27  qed
    8.28  
    8.29  lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w"
    8.30 @@ -959,7 +959,7 @@
    8.31  next
    8.32    fix bs
    8.33    from bv_to_nat_upper_range [of "bv_not bs"]
    8.34 -  show "- (2 ^ length bs) \<le> - int (bv_to_nat (bv_not bs)) + -1"
    8.35 +  show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
    8.36      by (simp add: int_nat_two_exp)
    8.37  qed
    8.38  
     9.1 --- a/src/HOL/Nat.thy	Wed Jun 20 05:06:56 2007 +0200
     9.2 +++ b/src/HOL/Nat.thy	Wed Jun 20 05:18:39 2007 +0200
     9.3 @@ -1298,7 +1298,7 @@
     9.4  
     9.5  primrec
     9.6    of_nat_0:   "of_nat 0 = 0"
     9.7 -  of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
     9.8 +  of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
     9.9  
    9.10  lemma of_nat_id [simp]: "(of_nat n \<Colon> nat) = n"
    9.11    by (induct n) auto
    9.12 @@ -1309,19 +1309,20 @@
    9.13  lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
    9.14    by (induct m) (simp_all add: add_ac)
    9.15  
    9.16 -lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
    9.17 +lemma of_nat_mult: "of_nat (m*n) = of_nat m * of_nat n"
    9.18    by (induct m) (simp_all add: add_ac left_distrib)
    9.19  
    9.20  lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
    9.21    apply (induct m, simp_all)
    9.22    apply (erule order_trans)
    9.23 +  apply (rule ord_le_eq_trans [OF _ add_commute])
    9.24    apply (rule less_add_one [THEN order_less_imp_le])
    9.25    done
    9.26  
    9.27  lemma less_imp_of_nat_less:
    9.28      "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
    9.29    apply (induct m n rule: diff_induct, simp_all)
    9.30 -  apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
    9.31 +  apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
    9.32    done
    9.33  
    9.34  lemma of_nat_less_imp_less:
    10.1 --- a/src/HOL/NumberTheory/Fib.thy	Wed Jun 20 05:06:56 2007 +0200
    10.2 +++ b/src/HOL/NumberTheory/Fib.thy	Wed Jun 20 05:18:39 2007 +0200
    10.3 @@ -85,7 +85,7 @@
    10.4    (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1
    10.5     else fib (Suc n) * fib (Suc n) + 1)"
    10.6    apply (rule int_int_eq [THEN iffD1]) 
    10.7 -  apply (simp add: fib_Cassini_int del: of_nat_mult) 
    10.8 +  apply (simp add: fib_Cassini_int)
    10.9    apply (subst zdiff_int [symmetric]) 
   10.10     apply (insert fib_Suc_gr_0 [of n], simp_all)
   10.11    done
    11.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 20 05:06:56 2007 +0200
    11.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 20 05:18:39 2007 +0200
    11.3 @@ -281,7 +281,7 @@
    11.4  
    11.5  lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
    11.6    using P_set_card Q_set_card P_set_finite Q_set_finite
    11.7 -  by (auto simp add: S_def setsum_constant)
    11.8 +  by (auto simp add: S_def zmult_int setsum_constant)
    11.9  
   11.10  lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
   11.11    by (auto simp add: S1_def S2_def)
    12.1 --- a/src/HOL/Power.thy	Wed Jun 20 05:06:56 2007 +0200
    12.2 +++ b/src/HOL/Power.thy	Wed Jun 20 05:18:39 2007 +0200
    12.3 @@ -333,7 +333,7 @@
    12.4  
    12.5  lemma of_nat_power:
    12.6    "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
    12.7 -by (induct n, simp_all add: power_Suc)
    12.8 +by (induct n, simp_all add: power_Suc of_nat_mult)
    12.9  
   12.10  lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
   12.11  by (insert one_le_power [of i n], simp)
    13.1 --- a/src/HOL/Real/Float.thy	Wed Jun 20 05:06:56 2007 +0200
    13.2 +++ b/src/HOL/Real/Float.thy	Wed Jun 20 05:18:39 2007 +0200
    13.3 @@ -35,8 +35,7 @@
    13.4      apply (auto, induct_tac n)
    13.5      apply (simp_all add: pow2_def)
    13.6      apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
    13.7 -    apply (auto simp add: h)
    13.8 -    by (simp add: add_commute)
    13.9 +    by (auto simp add: h)
   13.10    show ?thesis
   13.11    proof (induct a)
   13.12      case (1 n)
   13.13 @@ -46,7 +45,7 @@
   13.14      show ?case
   13.15        apply (auto)
   13.16        apply (subst pow2_neg[of "- int n"])
   13.17 -      apply (subst pow2_neg[of "- int n + -1"])
   13.18 +      apply (subst pow2_neg[of "-1 - int n"])
   13.19        apply (auto simp add: g pos)
   13.20        done
   13.21    qed
   13.22 @@ -269,18 +268,10 @@
   13.23    norm_float :: "int*int \<Rightarrow> int*int"
   13.24  
   13.25  lemma int_div_zdiv: "int (a div b) = (int a) div (int b)"
   13.26 -apply (subst split_div, auto)
   13.27 -apply (subst split_zdiv, auto)
   13.28 -apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
   13.29 -apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
   13.30 -done
   13.31 +by (rule zdiv_int)
   13.32  
   13.33  lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)"
   13.34 -apply (subst split_mod, auto)
   13.35 -apply (subst split_zmod, auto)
   13.36 -apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia in IntDiv.unique_remainder)
   13.37 -apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
   13.38 -done
   13.39 +by (rule zmod_int)
   13.40  
   13.41  lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
   13.42  by arith
    14.1 --- a/src/HOL/Real/RealDef.thy	Wed Jun 20 05:06:56 2007 +0200
    14.2 +++ b/src/HOL/Real/RealDef.thy	Wed Jun 20 05:18:39 2007 +0200
    14.3 @@ -712,7 +712,7 @@
    14.4  by (simp add: real_of_nat_def del: of_nat_Suc)
    14.5  
    14.6  lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
    14.7 -by (simp add: real_of_nat_def)
    14.8 +by (simp add: real_of_nat_def of_nat_mult)
    14.9  
   14.10  lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 
   14.11      (SUM x:A. real(f x))"
    15.1 --- a/src/HOL/SetInterval.thy	Wed Jun 20 05:06:56 2007 +0200
    15.2 +++ b/src/HOL/SetInterval.thy	Wed Jun 20 05:18:39 2007 +0200
    15.3 @@ -756,7 +756,7 @@
    15.4    show ?case by simp
    15.5  next
    15.6    case (Suc n)
    15.7 -  then show ?case by (simp add: right_distrib add_assoc mult_ac)
    15.8 +  then show ?case by (simp add: ring_eq_simps)
    15.9  qed
   15.10  
   15.11  theorem arith_series_general:
   15.12 @@ -779,7 +779,7 @@
   15.13    also from ngt1 
   15.14    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)"
   15.15      by (simp only: mult_ac gauss_sum [of "n - 1"])
   15.16 -       (simp add:  mult_ac of_nat_Suc [symmetric])
   15.17 +       (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
   15.18    finally show ?thesis by (simp add: mult_ac add_ac right_distrib)
   15.19  next
   15.20    assume "\<not>(n > 1)"
    16.1 --- a/src/HOL/ex/NatSum.thy	Wed Jun 20 05:06:56 2007 +0200
    16.2 +++ b/src/HOL/ex/NatSum.thy	Wed Jun 20 05:18:39 2007 +0200
    16.3 @@ -106,7 +106,7 @@
    16.4    "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
    16.5      of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
    16.6      (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
    16.7 -  by (induct m) simp_all
    16.8 +  by (induct m) (simp_all add: of_nat_mult)
    16.9  
   16.10  
   16.11  text {*