slight cleanup of lemmas
authorhaftmann
Thu Aug 06 23:56:48 2015 +0200 (2015-08-06)
changeset 6086786e7560e07d0
parent 60866 7f562aa4eb4b
child 60868 dd18c33c001e
child 60869 878e32cf3131
slight cleanup of lemmas
src/HOL/Divides.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Poly_Deriv.thy
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/NSComplex.thy
src/HOL/NSA/StarDef.thy
src/HOL/NthRoot.thy
src/HOL/Parity.thy
src/HOL/Power.thy
src/HOL/Rings.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
src/HOL/Word/Bit_Representation.thy
     1.1 --- a/src/HOL/Divides.thy	Thu Aug 06 19:12:09 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu Aug 06 23:56:48 2015 +0200
     1.3 @@ -30,13 +30,17 @@
     1.4      using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
     1.5  qed simp
     1.6  
     1.7 -lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>
     1.8 -  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
     1.9 -  by (induct n) (simp_all add: no_zero_divisors)
    1.10 -
    1.11 -lemma semiring_div_power_eq_0_iff: -- \<open>FIXME cf. @{text power_eq_0_iff}, @{text power_eq_0_nat_iff}\<close>
    1.12 -  "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"
    1.13 -  using power_not_zero [of a n] by (auto simp add: zero_power)
    1.14 +lemma div_by_1:
    1.15 +  "a div 1 = a"
    1.16 +  by (fact divide_1)
    1.17 +
    1.18 +lemma div_mult_self1_is_id:
    1.19 +  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
    1.20 +  by (fact nonzero_mult_divide_cancel_left)
    1.21 +
    1.22 +lemma div_mult_self2_is_id:
    1.23 +  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    1.24 +  by (fact nonzero_mult_divide_cancel_right)
    1.25  
    1.26  text \<open>@{const divide} and @{const mod}\<close>
    1.27  
    1.28 @@ -104,31 +108,24 @@
    1.29    "(b * c + a) mod b = a mod b"
    1.30    by (simp add: add.commute)
    1.31  
    1.32 -lemma div_mult_self1_is_id:
    1.33 -  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
    1.34 -  by (fact nonzero_mult_divide_cancel_left)
    1.35 -
    1.36 -lemma div_mult_self2_is_id:
    1.37 -  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    1.38 -  by (fact nonzero_mult_divide_cancel_right)
    1.39 -
    1.40 -lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
    1.41 +lemma mod_mult_self1_is_0 [simp]:
    1.42 +  "b * a mod b = 0"
    1.43    using mod_mult_self2 [of 0 b a] by simp
    1.44  
    1.45 -lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
    1.46 +lemma mod_mult_self2_is_0 [simp]:
    1.47 +  "a * b mod b = 0"
    1.48    using mod_mult_self1 [of 0 a b] by simp
    1.49  
    1.50 -lemma div_by_1: "a div 1 = a"
    1.51 -  by (fact divide_1)
    1.52 -
    1.53 -lemma mod_by_1 [simp]: "a mod 1 = 0"
    1.54 +lemma mod_by_1 [simp]:
    1.55 +  "a mod 1 = 0"
    1.56  proof -
    1.57    from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
    1.58    then have "a + a mod 1 = a + 0" by simp
    1.59    then show ?thesis by (rule add_left_imp_eq)
    1.60  qed
    1.61  
    1.62 -lemma mod_self [simp]: "a mod a = 0"
    1.63 +lemma mod_self [simp]:
    1.64 +  "a mod a = 0"
    1.65    using mod_mult_self2_is_0 [of 1] by simp
    1.66  
    1.67  lemma div_add_self1 [simp]:
    1.68 @@ -181,7 +178,7 @@
    1.69    then show "b dvd a" ..
    1.70  qed
    1.71  
    1.72 -lemma dvd_eq_mod_eq_0 [code]:
    1.73 +lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
    1.74    "a dvd b \<longleftrightarrow> b mod a = 0"
    1.75    by (simp add: mod_eq_0_iff_dvd)
    1.76  
    1.77 @@ -212,17 +209,6 @@
    1.78    finally show ?thesis .
    1.79  qed
    1.80  
    1.81 -lemma div_dvd_div [simp]:
    1.82 -  assumes "a dvd b" and "a dvd c"
    1.83 -  shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
    1.84 -using assms apply (cases "a = 0")
    1.85 -apply auto
    1.86 -apply (unfold dvd_def)
    1.87 -apply auto
    1.88 - apply(blast intro:mult.assoc[symmetric])
    1.89 -apply(fastforce simp add: mult.assoc)
    1.90 -done
    1.91 -
    1.92  lemma dvd_mod_imp_dvd:
    1.93    assumes "k dvd m mod n" and "k dvd n"
    1.94    shows "k dvd m"
    1.95 @@ -234,7 +220,8 @@
    1.96  
    1.97  text \<open>Addition respects modular equivalence.\<close>
    1.98  
    1.99 -lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
   1.100 +lemma mod_add_left_eq: -- \<open>FIXME reorient\<close>
   1.101 +  "(a + b) mod c = (a mod c + b) mod c"
   1.102  proof -
   1.103    have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   1.104      by (simp only: mod_div_equality)
   1.105 @@ -245,7 +232,8 @@
   1.106    finally show ?thesis .
   1.107  qed
   1.108  
   1.109 -lemma mod_add_right_eq: "(a + b) mod c = (a + b mod c) mod c"
   1.110 +lemma mod_add_right_eq: -- \<open>FIXME reorient\<close>
   1.111 +  "(a + b) mod c = (a + b mod c) mod c"
   1.112  proof -
   1.113    have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
   1.114      by (simp only: mod_div_equality)
   1.115 @@ -256,7 +244,8 @@
   1.116    finally show ?thesis .
   1.117  qed
   1.118  
   1.119 -lemma mod_add_eq: "(a + b) mod c = (a mod c + b mod c) mod c"
   1.120 +lemma mod_add_eq: -- \<open>FIXME reorient\<close>
   1.121 +  "(a + b) mod c = (a mod c + b mod c) mod c"
   1.122  by (rule trans [OF mod_add_left_eq mod_add_right_eq])
   1.123  
   1.124  lemma mod_add_cong:
   1.125 @@ -270,13 +259,10 @@
   1.126      by (simp only: mod_add_eq [symmetric])
   1.127  qed
   1.128  
   1.129 -lemma div_add [simp]: "z dvd x \<Longrightarrow> z dvd y
   1.130 -  \<Longrightarrow> (x + y) div z = x div z + y div z"
   1.131 -by (cases "z = 0", simp, unfold dvd_def, auto simp add: algebra_simps)
   1.132 -
   1.133  text \<open>Multiplication respects modular equivalence.\<close>
   1.134  
   1.135 -lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
   1.136 +lemma mod_mult_left_eq: -- \<open>FIXME reorient\<close>
   1.137 +  "(a * b) mod c = ((a mod c) * b) mod c"
   1.138  proof -
   1.139    have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
   1.140      by (simp only: mod_div_equality)
   1.141 @@ -287,7 +273,8 @@
   1.142    finally show ?thesis .
   1.143  qed
   1.144  
   1.145 -lemma mod_mult_right_eq: "(a * b) mod c = (a * (b mod c)) mod c"
   1.146 +lemma mod_mult_right_eq: -- \<open>FIXME reorient\<close>
   1.147 +  "(a * b) mod c = (a * (b mod c)) mod c"
   1.148  proof -
   1.149    have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
   1.150      by (simp only: mod_div_equality)
   1.151 @@ -298,7 +285,8 @@
   1.152    finally show ?thesis .
   1.153  qed
   1.154  
   1.155 -lemma mod_mult_eq: "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
   1.156 +lemma mod_mult_eq: -- \<open>FIXME reorient\<close>
   1.157 +  "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
   1.158  by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
   1.159  
   1.160  lemma mod_mult_cong:
   1.161 @@ -314,7 +302,7 @@
   1.162  
   1.163  text \<open>Exponentiation respects modular equivalence.\<close>
   1.164  
   1.165 -lemma power_mod: "(a mod b)^n mod b = a^n mod b"
   1.166 +lemma power_mod: "(a mod b) ^ n mod b = a ^ n mod b"
   1.167  apply (induct n, simp_all)
   1.168  apply (rule mod_mult_right_eq [THEN trans])
   1.169  apply (simp (no_asm_simp))
   1.170 @@ -338,15 +326,6 @@
   1.171    finally show ?thesis .
   1.172  qed
   1.173  
   1.174 -lemma div_mult_div_if_dvd:
   1.175 -  "y dvd x \<Longrightarrow> z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
   1.176 -  apply (cases "y = 0", simp)
   1.177 -  apply (cases "z = 0", simp)
   1.178 -  apply (auto elim!: dvdE simp add: algebra_simps)
   1.179 -  apply (subst mult.assoc [symmetric])
   1.180 -  apply (simp add: no_zero_divisors)
   1.181 -  done
   1.182 -
   1.183  lemma div_mult_mult2 [simp]:
   1.184    "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   1.185    by (drule div_mult_mult1) (simp add: mult.commute)
   1.186 @@ -384,31 +363,6 @@
   1.187  lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
   1.188  by (blast intro: dvd_mod_imp_dvd dvd_mod)
   1.189  
   1.190 -lemma div_power:
   1.191 -  "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n"
   1.192 -apply (induct n)
   1.193 - apply simp
   1.194 -apply(simp add: div_mult_div_if_dvd dvd_power_same)
   1.195 -done
   1.196 -
   1.197 -lemma dvd_div_eq_mult:
   1.198 -  assumes "a \<noteq> 0" and "a dvd b"
   1.199 -  shows "b div a = c \<longleftrightarrow> b = c * a"
   1.200 -proof
   1.201 -  assume "b = c * a"
   1.202 -  then show "b div a = c" by (simp add: assms)
   1.203 -next
   1.204 -  assume "b div a = c"
   1.205 -  then have "b div a * a = c * a" by simp
   1.206 -  moreover from \<open>a dvd b\<close> have "b div a * a = b" by simp
   1.207 -  ultimately show "b = c * a" by simp
   1.208 -qed
   1.209 -
   1.210 -lemma dvd_div_div_eq_mult:
   1.211 -  assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
   1.212 -  shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
   1.213 -  using assms by (auto simp add: mult.commute [of _ a] dvd_div_eq_mult div_mult_swap intro: sym)
   1.214 -
   1.215  end
   1.216  
   1.217  class ring_div = comm_ring_1 + semiring_div
   1.218 @@ -477,10 +431,9 @@
   1.219  apply simp
   1.220  done
   1.221  
   1.222 -lemma div_diff[simp]:
   1.223 -  "\<lbrakk> z dvd x; z dvd y\<rbrakk> \<Longrightarrow> (x - y) div z = x div z - y div z"
   1.224 -using div_add[where y = "- z" for z]
   1.225 -by (simp add: dvd_neg_div)
   1.226 +lemma div_diff [simp]:
   1.227 +  "z dvd x \<Longrightarrow> z dvd y \<Longrightarrow> (x - y) div z = x div z - y div z"
   1.228 +  using div_add [of _ _ "- y"] by (simp add: dvd_neg_div)
   1.229  
   1.230  lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
   1.231    using div_mult_mult1 [of "- 1" a b]
   1.232 @@ -670,7 +623,7 @@
   1.233      by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
   1.234    with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
   1.235    then show ?P and ?Q
   1.236 -    by (simp_all add: div mod add_implies_diff [symmetric] le_add_diff_inverse2)
   1.237 +    by (simp_all add: div mod add_implies_diff [symmetric])
   1.238  qed
   1.239  
   1.240  lemma divmod_digit_0:
   1.241 @@ -701,11 +654,11 @@
   1.242  where
   1.243    "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
   1.244  
   1.245 -lemma fst_divmod [simp]:
   1.246 +lemma fst_divmod:
   1.247    "fst (divmod m n) = numeral m div numeral n"
   1.248    by (simp add: divmod_def)
   1.249  
   1.250 -lemma snd_divmod [simp]:
   1.251 +lemma snd_divmod:
   1.252    "snd (divmod m n) = numeral m mod numeral n"
   1.253    by (simp add: divmod_def)
   1.254  
   1.255 @@ -722,16 +675,11 @@
   1.256    and evaluate accordingly.
   1.257  \<close>
   1.258  
   1.259 -lemma divmod_step_eq [code]:
   1.260 +lemma divmod_step_eq [code, simp]:
   1.261    "divmod_step l (q, r) = (if numeral l \<le> r
   1.262      then (2 * q + 1, r - numeral l) else (2 * q, r))"
   1.263    by (simp add: divmod_step_def)
   1.264  
   1.265 -lemma divmod_step_simps [simp]:
   1.266 -  "r < numeral l \<Longrightarrow> divmod_step l (q, r) = (2 * q, r)"
   1.267 -  "numeral l \<le> r \<Longrightarrow> divmod_step l (q, r) = (2 * q + 1, r - numeral l)"
   1.268 -  by (auto simp add: divmod_step_eq not_le)
   1.269 -
   1.270  text \<open>
   1.271    This is a formulation of school-method division.
   1.272    If the divisor is smaller than the dividend, terminate.
   1.273 @@ -740,13 +688,13 @@
   1.274    opposite direction.
   1.275  \<close>
   1.276  
   1.277 -lemma divmod_divmod_step [code]:
   1.278 +lemma divmod_divmod_step:
   1.279    "divmod m n = (if m < n then (0, numeral m)
   1.280      else divmod_step n (divmod m (Num.Bit0 n)))"
   1.281  proof (cases "m < n")
   1.282    case True then have "numeral m < numeral n" by simp
   1.283    then show ?thesis
   1.284 -    by (simp add: prod_eq_iff div_less mod_less)
   1.285 +    by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
   1.286  next
   1.287    case False
   1.288    have "divmod m n =
   1.289 @@ -754,10 +702,10 @@
   1.290        numeral m mod (2 * numeral n))"
   1.291    proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
   1.292      case True
   1.293 -    with divmod_step_simps
   1.294 +    with divmod_step_eq
   1.295        have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   1.296          (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
   1.297 -        by blast
   1.298 +        by simp
   1.299      moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
   1.300        have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
   1.301        and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
   1.302 @@ -766,10 +714,10 @@
   1.303    next
   1.304      case False then have *: "numeral m mod (2 * numeral n) < numeral n"
   1.305        by (simp add: not_le)
   1.306 -    with divmod_step_simps
   1.307 +    with divmod_step_eq
   1.308        have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   1.309          (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
   1.310 -        by blast
   1.311 +        by auto
   1.312      moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
   1.313        have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
   1.314        and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
   1.315 @@ -785,10 +733,17 @@
   1.316    with False show ?thesis by simp
   1.317  qed
   1.318  
   1.319 -lemma divmod_eq [simp]:
   1.320 -  "m < n \<Longrightarrow> divmod m n = (0, numeral m)"
   1.321 -  "n \<le> m \<Longrightarrow> divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
   1.322 -  by (auto simp add: divmod_divmod_step [of m n])
   1.323 +text \<open>The division rewrite proper – first, trivial results involving @{text 1}\<close>
   1.324 +
   1.325 +lemma divmod_trivial [simp, code]:
   1.326 +  "divmod Num.One Num.One = (numeral Num.One, 0)"
   1.327 +  "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
   1.328 +  "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
   1.329 +  "divmod num.One (num.Bit0 n) = (0, Numeral1)"
   1.330 +  "divmod num.One (num.Bit1 n) = (0, Numeral1)"
   1.331 +  using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
   1.332 +
   1.333 +text \<open>Division by an even number is a right-shift\<close>
   1.334  
   1.335  lemma divmod_cancel [simp, code]:
   1.336    "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
   1.337 @@ -799,10 +754,26 @@
   1.338      by (simp_all only: numeral_mult numeral.simps distrib) simp_all
   1.339    have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
   1.340    then show ?P and ?Q
   1.341 -    by (simp_all add: prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
   1.342 -      div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] add.commute del: numeral_times_numeral)
   1.343 +    by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
   1.344 +      div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
   1.345 +      add.commute del: numeral_times_numeral)
   1.346  qed
   1.347  
   1.348 +text \<open>The really hard work\<close>
   1.349 +
   1.350 +lemma divmod_steps [simp, code]:
   1.351 +  "divmod (num.Bit0 m) (num.Bit1 n) =
   1.352 +      (if m \<le> n then (0, numeral (num.Bit0 m))
   1.353 +       else divmod_step (num.Bit1 n)
   1.354 +             (divmod (num.Bit0 m)
   1.355 +               (num.Bit0 (num.Bit1 n))))"
   1.356 +  "divmod (num.Bit1 m) (num.Bit1 n) =
   1.357 +      (if m < n then (0, numeral (num.Bit1 m))
   1.358 +       else divmod_step (num.Bit1 n)
   1.359 +             (divmod (num.Bit1 m)
   1.360 +               (num.Bit0 (num.Bit1 n))))"
   1.361 +  by (simp_all add: divmod_divmod_step)
   1.362 +
   1.363  text \<open>Special case: divisibility\<close>
   1.364  
   1.365  definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
   1.366 @@ -817,6 +788,24 @@
   1.367    "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
   1.368    by (simp add: divmod_def mod_eq_0_iff_dvd)
   1.369  
   1.370 +text \<open>Generic computation of quotient and remainder\<close>  
   1.371 +
   1.372 +lemma numeral_div_numeral [simp]: 
   1.373 +  "numeral k div numeral l = fst (divmod k l)"
   1.374 +  by (simp add: fst_divmod)
   1.375 +
   1.376 +lemma numeral_mod_numeral [simp]: 
   1.377 +  "numeral k mod numeral l = snd (divmod k l)"
   1.378 +  by (simp add: snd_divmod)
   1.379 +
   1.380 +lemma one_div_numeral [simp]:
   1.381 +  "1 div numeral n = fst (divmod num.One n)"
   1.382 +  by (simp add: fst_divmod)
   1.383 +
   1.384 +lemma one_mod_numeral [simp]:
   1.385 +  "1 mod numeral n = snd (divmod num.One n)"
   1.386 +  by (simp add: snd_divmod)
   1.387 +  
   1.388  end
   1.389  
   1.390  
   1.391 @@ -1580,10 +1569,6 @@
   1.392      by simp
   1.393  qed
   1.394  
   1.395 -lemma odd_Suc_minus_one [simp]:
   1.396 -  "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
   1.397 -  by (auto elim: oddE)
   1.398 -
   1.399  lemma parity_induct [case_names zero even odd]:
   1.400    assumes zero: "P 0"
   1.401    assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
   1.402 @@ -2789,15 +2774,15 @@
   1.403  
   1.404  lemma div_nat_numeral [simp]:
   1.405    "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"
   1.406 -  by (simp add: nat_div_distrib)
   1.407 +  by (subst nat_div_distrib) simp_all
   1.408  
   1.409  lemma one_div_nat_numeral [simp]:
   1.410    "Suc 0 div numeral v' = nat (1 div numeral v')"
   1.411 -  by (subst nat_div_distrib, simp_all)
   1.412 +  by (subst nat_div_distrib) simp_all
   1.413  
   1.414  lemma mod_nat_numeral [simp]:
   1.415    "(numeral v :: nat) mod numeral v' = nat (numeral v mod numeral v')"
   1.416 -  by (simp add: nat_mod_distrib)
   1.417 +  by (subst nat_mod_distrib) simp_all
   1.418  
   1.419  lemma one_mod_nat_numeral [simp]:
   1.420    "Suc 0 mod numeral v' = nat (1 mod numeral v')"
     2.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Aug 06 19:12:09 2015 +0200
     2.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Aug 06 23:56:48 2015 +0200
     2.3 @@ -240,6 +240,8 @@
     2.4  
     2.5  instance fps :: (semiring_0_cancel) semiring_0_cancel ..
     2.6  
     2.7 +instance fps :: (semiring_1) semiring_1 ..
     2.8 +
     2.9  
    2.10  subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close>
    2.11  
    2.12 @@ -372,8 +374,9 @@
    2.13    by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1
    2.14      fps_const_add [symmetric])
    2.15  
    2.16 -lemma neg_numeral_fps_const: "- numeral k = fps_const (- numeral k)"
    2.17 -  by (simp only: numeral_fps_const fps_const_neg)
    2.18 +lemma neg_numeral_fps_const:
    2.19 +  "(- numeral k :: 'a :: ring_1 fps) = fps_const (- numeral k)"
    2.20 +  by (simp add: numeral_fps_const)
    2.21  
    2.22  
    2.23  subsection \<open>The eXtractor series X\<close>
    2.24 @@ -556,7 +559,7 @@
    2.25      unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
    2.26      by simp
    2.27    then have "x > (1 / y)^k" using yp
    2.28 -    by (simp add: field_simps nonzero_power_divide)
    2.29 +    by (simp add: field_simps)
    2.30    then show ?thesis
    2.31      using kp by blast
    2.32  qed
    2.33 @@ -2201,7 +2204,7 @@
    2.34      from a0 b0 have ab0[simp]: "(a/b)$0 = a$0 / b$0"
    2.35        by (simp add: fps_divide_def fps_mult_nth divide_inverse fps_inverse_def)
    2.36      have th0: "r k ((a/b)$0) ^ k = (a/b)$0"
    2.37 -      by (simp add: \<open>?lhs\<close> nonzero_power_divide[OF rb0'] ra0 rb0)
    2.38 +      by (simp add: \<open>?lhs\<close> power_divide ra0 rb0)
    2.39      from a0 b0 ra0' rb0' kp \<open>?lhs\<close>
    2.40      have th1: "r k ((a / b) $ 0) = (fps_radical r k a / fps_radical r k b) $ 0"
    2.41        by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse)
    2.42 @@ -2407,7 +2410,7 @@
    2.43  lemma fps_compose_0[simp]: "0 oo a = 0"
    2.44    by (simp add: fps_eq_iff fps_compose_nth)
    2.45  
    2.46 -lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a$0)"
    2.47 +lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a $ 0)"
    2.48    by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum.neutral)
    2.49  
    2.50  lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)"
     3.1 --- a/src/HOL/Library/Poly_Deriv.thy	Thu Aug 06 19:12:09 2015 +0200
     3.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Thu Aug 06 23:56:48 2015 +0200
     3.3 @@ -175,7 +175,7 @@
     3.4    next
     3.5      show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
     3.6       apply (subst lemma_order_pderiv1)
     3.7 -     by (metis * nd dvd_mult_cancel_right field_power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
     3.8 +     by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
     3.9    qed
    3.10    then show ?thesis
    3.11      by (metis \<open>n = Suc n'\<close> pe)
     4.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Aug 06 19:12:09 2015 +0200
     4.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Aug 06 23:56:48 2015 +0200
     4.3 @@ -1045,7 +1045,7 @@
     4.4        let
     4.5          val simp_ctxt =
     4.6            ctxt addsimps @{thms field_simps}
     4.7 -          addsimps [@{thm nonzero_power_divide}, @{thm power_divide}]
     4.8 +          addsimps [@{thm power_divide}]
     4.9          val th =
    4.10            Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
    4.11              (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
     5.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 06 19:12:09 2015 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 06 23:56:48 2015 +0200
     5.3 @@ -5257,7 +5257,7 @@
     5.4        also have "\<dots> < e * inverse 2 * 2"
     5.5          unfolding divide_inverse setsum_right_distrib[symmetric]
     5.6          apply (rule mult_strict_left_mono)
     5.7 -        unfolding power_inverse lessThan_Suc_atMost[symmetric]
     5.8 +        unfolding power_inverse [symmetric] lessThan_Suc_atMost[symmetric]
     5.9          apply (subst geometric_sum)
    5.10          using goal1
    5.11          apply auto
    5.12 @@ -9892,7 +9892,7 @@
    5.13              show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
    5.14                unfolding power_add divide_inverse inverse_mult_distrib
    5.15                unfolding setsum_right_distrib[symmetric] setsum_left_distrib[symmetric]
    5.16 -              unfolding power_inverse sum_gp
    5.17 +              unfolding power_inverse [symmetric] sum_gp
    5.18                apply(rule mult_strict_left_mono[OF _ e])
    5.19                unfolding power2_eq_square
    5.20                apply auto
     6.1 --- a/src/HOL/NSA/HyperDef.thy	Thu Aug 06 19:12:09 2015 +0200
     6.2 +++ b/src/HOL/NSA/HyperDef.thy	Thu Aug 06 23:56:48 2015 +0200
     6.3 @@ -441,12 +441,12 @@
     6.4  
     6.5  lemma hyperpow_not_zero:
     6.6    "\<And>r n. r \<noteq> (0::'a::{field} star) ==> r pow n \<noteq> 0"
     6.7 -by transfer (rule field_power_not_zero)
     6.8 +by transfer (rule power_not_zero)
     6.9  
    6.10  lemma hyperpow_inverse:
    6.11    "\<And>r n. r \<noteq> (0::'a::field star)
    6.12     \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
    6.13 -by transfer (rule power_inverse)
    6.14 +by transfer (rule power_inverse [symmetric])
    6.15  
    6.16  lemma hyperpow_hrabs:
    6.17    "\<And>r n. abs (r::'a::{linordered_idom} star) pow n = abs (r pow n)"
     7.1 --- a/src/HOL/NSA/NSComplex.thy	Thu Aug 06 19:12:09 2015 +0200
     7.2 +++ b/src/HOL/NSA/NSComplex.thy	Thu Aug 06 23:56:48 2015 +0200
     7.3 @@ -377,19 +377,20 @@
     7.4  by transfer simp
     7.5  
     7.6  lemma hcpow_mult:
     7.7 -  "!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
     7.8 +  "((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
     7.9    by (fact hyperpow_mult)
    7.10  
    7.11  lemma hcpow_zero2 [simp]:
    7.12 -  "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"
    7.13 -by transfer (rule power_0_Suc)
    7.14 +  "\<And>n. 0 pow (hSuc n) = (0::'a::semiring_1 star)"
    7.15 +  by transfer (rule power_0_Suc)
    7.16  
    7.17  lemma hcpow_not_zero [simp,intro]:
    7.18    "!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)"
    7.19 -by (rule hyperpow_not_zero)
    7.20 +  by (fact hyperpow_not_zero)
    7.21  
    7.22 -lemma hcpow_zero_zero: "r pow n = (0::hcomplex) ==> r = 0"
    7.23 -by (blast intro: ccontr dest: hcpow_not_zero)
    7.24 +lemma hcpow_zero_zero:
    7.25 +  "r pow n = (0::hcomplex) ==> r = 0"
    7.26 +  by (blast intro: ccontr dest: hcpow_not_zero)
    7.27  
    7.28  subsection{*The Function @{term hsgn}*}
    7.29  
     8.1 --- a/src/HOL/NSA/StarDef.thy	Thu Aug 06 19:12:09 2015 +0200
     8.2 +++ b/src/HOL/NSA/StarDef.thy	Thu Aug 06 23:56:48 2015 +0200
     8.3 @@ -688,7 +688,7 @@
     8.4    star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
     8.5  
     8.6  instance
     8.7 -  by default (transfer, auto)+
     8.8 +  by (standard; transfer) auto
     8.9  
    8.10  end
    8.11  
    8.12 @@ -699,14 +699,14 @@
    8.13    star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
    8.14  
    8.15  instance
    8.16 -  by default (transfer, auto)+
    8.17 +  by (standard; transfer) auto
    8.18  
    8.19  end
    8.20  
    8.21  instance star :: (lattice) lattice ..
    8.22  
    8.23  instance star :: (distrib_lattice) distrib_lattice
    8.24 -  by default (transfer, auto simp add: sup_inf_distrib1)
    8.25 +  by (standard; transfer) (auto simp add: sup_inf_distrib1)
    8.26  
    8.27  lemma Standard_inf [simp]:
    8.28    "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
    8.29 @@ -775,6 +775,8 @@
    8.30  apply (transfer, rule mult_1_right)
    8.31  done
    8.32  
    8.33 +instance star :: (power) power ..
    8.34 +
    8.35  instance star :: (comm_monoid_mult) comm_monoid_mult
    8.36  by (intro_classes, transfer, rule mult_1)
    8.37  
    8.38 @@ -843,6 +845,8 @@
    8.39  instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors
    8.40    by (intro_classes; transfer) (fact no_zero_divisors)
    8.41  
    8.42 +instance star :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors ..
    8.43 +  
    8.44  instance star :: (semiring_no_zero_divisors_cancel) semiring_no_zero_divisors_cancel
    8.45    by (intro_classes; transfer) simp_all
    8.46  
     9.1 --- a/src/HOL/NthRoot.thy	Thu Aug 06 19:12:09 2015 +0200
     9.2 +++ b/src/HOL/NthRoot.thy	Thu Aug 06 23:56:48 2015 +0200
     9.3 @@ -112,7 +112,7 @@
     9.4    have x: "\<And>a b :: real. (0 < b \<and> a < 0) \<Longrightarrow> \<not> a > b" by auto
     9.5    fix a b :: real assume "0 < n" "sgn a * \<bar>a\<bar> ^ n < sgn b * \<bar>b\<bar> ^ n" then show "a < b"
     9.6      using power_less_imp_less_base[of a n b]  power_less_imp_less_base[of "-b" n "-a"]
     9.7 -    by (simp add: sgn_real_def power_less_zero_eq x[of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
     9.8 +    by (simp add: sgn_real_def x [of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
     9.9  qed
    9.10  
    9.11  lemma real_root_gt_zero: "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> 0 < root n x"
    9.12 @@ -130,7 +130,7 @@
    9.13  by (auto simp add: order_le_less real_root_pow_pos)
    9.14  
    9.15  lemma sgn_root: "0 < n \<Longrightarrow> sgn (root n x) = sgn x"
    9.16 -  by (auto split: split_root simp: sgn_real_def power_less_zero_eq)
    9.17 +  by (auto split: split_root simp: sgn_real_def)
    9.18  
    9.19  lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
    9.20    using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: split_if_asm)
    9.21 @@ -496,7 +496,7 @@
    9.22  done
    9.23  
    9.24  lemma real_inv_sqrt_pow2: "0 < x ==> (inverse (sqrt x))\<^sup>2 = inverse x"
    9.25 -by (simp add: power_inverse [symmetric])
    9.26 +by (simp add: power_inverse)
    9.27  
    9.28  lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
    9.29  by simp
    9.30 @@ -525,7 +525,7 @@
    9.31    apply (cases "x = 0")
    9.32    apply simp_all
    9.33    using sqrt_divide_self_eq[of x]
    9.34 -  apply (simp add: inverse_eq_divide field_simps)
    9.35 +  apply (simp add: field_simps)
    9.36    done
    9.37  
    9.38  lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
    10.1 --- a/src/HOL/Parity.thy	Thu Aug 06 19:12:09 2015 +0200
    10.2 +++ b/src/HOL/Parity.thy	Thu Aug 06 23:56:48 2015 +0200
    10.3 @@ -195,6 +195,10 @@
    10.4    shows "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
    10.5    using even_abs_add_iff [of l k] by (simp add: ac_simps)
    10.6  
    10.7 +lemma odd_Suc_minus_one [simp]:
    10.8 +  "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
    10.9 +  by (auto elim: oddE)
   10.10 +
   10.11  instance int :: ring_parity
   10.12  proof
   10.13    show "\<not> 2 dvd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
    11.1 --- a/src/HOL/Power.thy	Thu Aug 06 19:12:09 2015 +0200
    11.2 +++ b/src/HOL/Power.thy	Thu Aug 06 23:56:48 2015 +0200
    11.3 @@ -9,6 +9,19 @@
    11.4  imports Num Equiv_Relations
    11.5  begin
    11.6  
    11.7 +context linordered_ring (* TODO: move *)
    11.8 +begin
    11.9 +
   11.10 +lemma sum_squares_ge_zero:
   11.11 +  "0 \<le> x * x + y * y"
   11.12 +  by (intro add_nonneg_nonneg zero_le_square)
   11.13 +
   11.14 +lemma not_sum_squares_lt_zero:
   11.15 +  "\<not> x * x + y * y < 0"
   11.16 +  by (simp add: not_less sum_squares_ge_zero)
   11.17 +
   11.18 +end
   11.19 +
   11.20  subsection \<open>Powers for Arbitrary Monoids\<close>
   11.21  
   11.22  class power = one + times
   11.23 @@ -186,6 +199,15 @@
   11.24  lemma one_power2: "1\<^sup>2 = 1" (* delete? *)
   11.25    by (rule power_one)
   11.26  
   11.27 +lemma power_0_Suc [simp]:
   11.28 +  "0 ^ Suc n = 0"
   11.29 +  by simp
   11.30 +
   11.31 +text\<open>It looks plausible as a simprule, but its effect can be strange.\<close>
   11.32 +lemma power_0_left:
   11.33 +  "0 ^ n = (if n = 0 then 1 else 0)"
   11.34 +  by (cases n) simp_all
   11.35 +
   11.36  end
   11.37  
   11.38  context comm_semiring_1
   11.39 @@ -229,6 +251,32 @@
   11.40  
   11.41  end
   11.42  
   11.43 +class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
   11.44 +begin
   11.45 +
   11.46 +subclass power .
   11.47 +
   11.48 +lemma power_eq_0_iff [simp]:
   11.49 +  "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
   11.50 +  by (induct n) auto
   11.51 +
   11.52 +lemma power_not_zero:
   11.53 +  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
   11.54 +  by (induct n) auto
   11.55 +
   11.56 +lemma zero_eq_power2 [simp]:
   11.57 +  "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
   11.58 +  unfolding power2_eq_square by simp
   11.59 +
   11.60 +end
   11.61 +
   11.62 +context semidom
   11.63 +begin
   11.64 +
   11.65 +subclass semiring_1_no_zero_divisors ..
   11.66 +
   11.67 +end
   11.68 +
   11.69  context ring_1
   11.70  begin
   11.71  
   11.72 @@ -252,7 +300,7 @@
   11.73  
   11.74  lemma power2_minus [simp]:
   11.75    "(- a)\<^sup>2 = a\<^sup>2"
   11.76 -  by (rule power_minus_Bit0)
   11.77 +  by (fact power_minus_Bit0)
   11.78  
   11.79  lemma power_minus1_even [simp]:
   11.80    "(- 1) ^ (2*n) = 1"
   11.81 @@ -272,29 +320,14 @@
   11.82  
   11.83  end
   11.84  
   11.85 -lemma power_eq_0_nat_iff [simp]:
   11.86 -  fixes m n :: nat
   11.87 -  shows "m ^ n = 0 \<longleftrightarrow> m = 0 \<and> n > 0"
   11.88 -  by (induct n) auto
   11.89 -
   11.90  context ring_1_no_zero_divisors
   11.91  begin
   11.92  
   11.93 -lemma power_eq_0_iff [simp]:
   11.94 -  "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
   11.95 -  by (induct n) auto
   11.96 -
   11.97 -lemma field_power_not_zero:
   11.98 -  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
   11.99 -  by (induct n) auto
  11.100 -
  11.101 -lemma zero_eq_power2 [simp]:
  11.102 -  "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
  11.103 -  unfolding power2_eq_square by simp
  11.104 +subclass semiring_1_no_zero_divisors .. 
  11.105  
  11.106  lemma power2_eq_1_iff:
  11.107    "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
  11.108 -  unfolding power2_eq_square by (rule square_eq_1_iff)
  11.109 +  using square_eq_1_iff [of a] by (simp add: power2_eq_square)
  11.110  
  11.111  end
  11.112  
  11.113 @@ -306,6 +339,16 @@
  11.114  
  11.115  end
  11.116  
  11.117 +context algebraic_semidom
  11.118 +begin
  11.119 +
  11.120 +lemma div_power:
  11.121 +  assumes "b dvd a"
  11.122 +  shows "(a div b) ^ n = a ^ n div b ^ n"
  11.123 +  using assms by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same)
  11.124 +
  11.125 +end
  11.126 +
  11.127  context normalization_semidom
  11.128  begin
  11.129  
  11.130 @@ -322,41 +365,42 @@
  11.131  context division_ring
  11.132  begin
  11.133  
  11.134 -text \<open>FIXME reorient or rename to @{text nonzero_inverse_power}\<close>
  11.135 -lemma nonzero_power_inverse:
  11.136 -  "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
  11.137 -  by (induct n)
  11.138 -    (simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero)
  11.139 +text\<open>Perhaps these should be simprules.\<close>
  11.140 +lemma power_inverse [field_simps, divide_simps]:
  11.141 +  "inverse a ^ n = inverse (a ^ n)"
  11.142 +proof (cases "a = 0")
  11.143 +  case True then show ?thesis by (simp add: power_0_left)
  11.144 +next
  11.145 +  case False then have "inverse (a ^ n) = inverse a ^ n"
  11.146 +    by (induct n) (simp_all add: nonzero_inverse_mult_distrib power_commutes)
  11.147 +  then show ?thesis by simp
  11.148 +qed
  11.149  
  11.150 -end
  11.151 +lemma power_one_over [field_simps, divide_simps]:
  11.152 +  "(1 / a) ^ n = 1 / a ^ n"
  11.153 +  using power_inverse [of a] by (simp add: divide_inverse)
  11.154 +
  11.155 +end  
  11.156  
  11.157  context field
  11.158  begin
  11.159  
  11.160 -lemma nonzero_power_divide:
  11.161 -  "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
  11.162 -  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
  11.163 +lemma power_diff:
  11.164 +  assumes nz: "a \<noteq> 0"
  11.165 +  shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
  11.166 +  by (induct m n rule: diff_induct) (simp_all add: nz power_not_zero)
  11.167  
  11.168 -declare nonzero_power_divide [where b = "numeral w" for w, simp]
  11.169 +lemma power_divide [field_simps, divide_simps]:
  11.170 +  "(a / b) ^ n = a ^ n / b ^ n"
  11.171 +  by (induct n) simp_all
  11.172 +
  11.173 +declare power_divide [where b = "numeral w" for w, simp]
  11.174  
  11.175  end
  11.176  
  11.177  
  11.178  subsection \<open>Exponentiation on ordered types\<close>
  11.179  
  11.180 -context linordered_ring (* TODO: move *)
  11.181 -begin
  11.182 -
  11.183 -lemma sum_squares_ge_zero:
  11.184 -  "0 \<le> x * x + y * y"
  11.185 -  by (intro add_nonneg_nonneg zero_le_square)
  11.186 -
  11.187 -lemma not_sum_squares_lt_zero:
  11.188 -  "\<not> x * x + y * y < 0"
  11.189 -  by (simp add: not_less sum_squares_ge_zero)
  11.190 -
  11.191 -end
  11.192 -
  11.193  context linordered_semidom
  11.194  begin
  11.195  
  11.196 @@ -702,12 +746,12 @@
  11.197  
  11.198  subsection \<open>Miscellaneous rules\<close>
  11.199  
  11.200 -lemma self_le_power:
  11.201 -  fixes x::"'a::linordered_semidom" 
  11.202 -  shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n"
  11.203 -  using power_increasing[of 1 n x] power_one_right[of x] by auto
  11.204 +lemma (in linordered_semidom) self_le_power:
  11.205 +  "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
  11.206 +  using power_increasing [of 1 n a] power_one_right [of a] by auto
  11.207  
  11.208 -lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
  11.209 +lemma (in power) power_eq_if:
  11.210 +  "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
  11.211    unfolding One_nat_def by (cases m) simp_all
  11.212  
  11.213  lemma (in comm_semiring_1) power2_sum:
  11.214 @@ -718,40 +762,6 @@
  11.215    "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
  11.216    by (simp add: algebra_simps power2_eq_square mult_2_right)
  11.217  
  11.218 -lemma power_0_Suc [simp]:
  11.219 -  "(0::'a::{power, semiring_0}) ^ Suc n = 0"
  11.220 -  by simp
  11.221 -
  11.222 -text\<open>It looks plausible as a simprule, but its effect can be strange.\<close>
  11.223 -lemma power_0_left:
  11.224 -  "0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))"
  11.225 -  by (induct n) simp_all
  11.226 -
  11.227 -lemma (in field) power_diff:
  11.228 -  assumes nz: "a \<noteq> 0"
  11.229 -  shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
  11.230 -  by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero)
  11.231 -
  11.232 -text\<open>Perhaps these should be simprules.\<close>
  11.233 -lemma power_inverse:
  11.234 -  fixes a :: "'a::division_ring"
  11.235 -  shows "inverse (a ^ n) = inverse a ^ n"
  11.236 -apply (cases "a = 0")
  11.237 -apply (simp add: power_0_left)
  11.238 -apply (simp add: nonzero_power_inverse)
  11.239 -done (* TODO: reorient or rename to inverse_power *)
  11.240 -
  11.241 -lemma power_one_over:
  11.242 -  "1 / (a::'a::{field, power}) ^ n =  (1 / a) ^ n"
  11.243 -  by (simp add: divide_inverse) (rule power_inverse)
  11.244 -
  11.245 -lemma power_divide [field_simps, divide_simps]:
  11.246 -  "(a / b) ^ n = (a::'a::field) ^ n / b ^ n"
  11.247 -apply (cases "b = 0")
  11.248 -apply (simp add: power_0_left)
  11.249 -apply (rule nonzero_power_divide)
  11.250 -apply assumption
  11.251 -done
  11.252  
  11.253  text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
  11.254  
  11.255 @@ -820,7 +830,7 @@
  11.256      assume "\<not> m \<le> n"
  11.257      then have "n < m" by simp
  11.258      with assms Suc show False
  11.259 -      by (auto simp add: algebra_simps) (simp add: power2_eq_square)
  11.260 +      by (simp add: power2_eq_square)
  11.261    qed
  11.262  qed
  11.263  
  11.264 @@ -916,4 +926,3 @@
  11.265    code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  11.266  
  11.267  end
  11.268 -
    12.1 --- a/src/HOL/Rings.thy	Thu Aug 06 19:12:09 2015 +0200
    12.2 +++ b/src/HOL/Rings.thy	Thu Aug 06 23:56:48 2015 +0200
    12.3 @@ -633,6 +633,20 @@
    12.4    "a div 1 = a"
    12.5    using nonzero_mult_divide_cancel_left [of 1 a] by simp
    12.6  
    12.7 +end
    12.8 +
    12.9 +class idom_divide = idom + semidom_divide
   12.10 +
   12.11 +class algebraic_semidom = semidom_divide
   12.12 +begin
   12.13 +
   12.14 +text \<open>
   12.15 +  Class @{class algebraic_semidom} enriches a integral domain
   12.16 +  by notions from algebra, like units in a ring.
   12.17 +  It is a separate class to avoid spoiling fields with notions
   12.18 +  which are degenerated there.
   12.19 +\<close>
   12.20 +
   12.21  lemma dvd_times_left_cancel_iff [simp]:
   12.22    assumes "a \<noteq> 0"
   12.23    shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
   12.24 @@ -667,19 +681,60 @@
   12.25    with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
   12.26  qed
   12.27  
   12.28 -end
   12.29 +lemma div_dvd_div [simp]:
   12.30 +  assumes "a dvd b" and "a dvd c"
   12.31 +  shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
   12.32 +proof (cases "a = 0")
   12.33 +  case True with assms show ?thesis by simp
   12.34 +next
   12.35 +  case False
   12.36 +  moreover from assms obtain k l where "b = a * k" and "c = a * l"
   12.37 +    by (auto elim!: dvdE)
   12.38 +  ultimately show ?thesis by simp
   12.39 +qed
   12.40  
   12.41 -class idom_divide = idom + semidom_divide
   12.42 -
   12.43 -class algebraic_semidom = semidom_divide
   12.44 -begin
   12.45 +lemma div_add [simp]:
   12.46 +  assumes "c dvd a" and "c dvd b"
   12.47 +  shows "(a + b) div c = a div c + b div c"
   12.48 +proof (cases "c = 0")
   12.49 +  case True then show ?thesis by simp
   12.50 +next
   12.51 +  case False
   12.52 +  moreover from assms obtain k l where "a = c * k" and "b = c * l"
   12.53 +    by (auto elim!: dvdE)
   12.54 +  moreover have "c * k + c * l = c * (k + l)"
   12.55 +    by (simp add: algebra_simps)
   12.56 +  ultimately show ?thesis
   12.57 +    by simp
   12.58 +qed
   12.59  
   12.60 -text \<open>
   12.61 -  Class @{class algebraic_semidom} enriches a integral domain
   12.62 -  by notions from algebra, like units in a ring.
   12.63 -  It is a separate class to avoid spoiling fields with notions
   12.64 -  which are degenerated there.
   12.65 -\<close>
   12.66 +lemma div_mult_div_if_dvd:
   12.67 +  assumes "b dvd a" and "d dvd c"
   12.68 +  shows "(a div b) * (c div d) = (a * c) div (b * d)"
   12.69 +proof (cases "b = 0 \<or> c = 0")
   12.70 +  case True with assms show ?thesis by auto
   12.71 +next
   12.72 +  case False
   12.73 +  moreover from assms obtain k l where "a = b * k" and "c = d * l"
   12.74 +    by (auto elim!: dvdE)
   12.75 +  moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
   12.76 +    by (simp add: ac_simps)
   12.77 +  ultimately show ?thesis by simp
   12.78 +qed
   12.79 +
   12.80 +lemma dvd_div_eq_mult:
   12.81 +  assumes "a \<noteq> 0" and "a dvd b"
   12.82 +  shows "b div a = c \<longleftrightarrow> b = c * a"
   12.83 +proof
   12.84 +  assume "b = c * a"
   12.85 +  then show "b div a = c" by (simp add: assms)
   12.86 +next
   12.87 +  assume "b div a = c"
   12.88 +  then have "b div a * a = c * a" by simp
   12.89 +  moreover from \<open>a \<noteq> 0\<close> \<open>a dvd b\<close> have "b div a * a = b"
   12.90 +    by (auto elim!: dvdE simp add: ac_simps)
   12.91 +  ultimately show "b = c * a" by simp
   12.92 +qed
   12.93  
   12.94  lemma dvd_div_mult_self [simp]:
   12.95    "a dvd b \<Longrightarrow> b div a * a = b"
   12.96 @@ -716,6 +771,22 @@
   12.97      by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
   12.98  qed
   12.99  
  12.100 +lemma dvd_div_div_eq_mult:
  12.101 +  assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
  12.102 +  shows "b div a = d div c \<longleftrightarrow> b * c = a * d" (is "?P \<longleftrightarrow> ?Q")
  12.103 +proof -
  12.104 +  from assms have "a * c \<noteq> 0" by simp
  12.105 +  then have "?P \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)"
  12.106 +    by simp
  12.107 +  also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a"
  12.108 +    by (simp add: ac_simps)
  12.109 +  also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a"
  12.110 +    using assms by (simp add: div_mult_swap)
  12.111 +  also have "\<dots> \<longleftrightarrow> ?Q"
  12.112 +    using assms by (simp add: ac_simps)
  12.113 +  finally show ?thesis .
  12.114 +qed
  12.115 +
  12.116  
  12.117  text \<open>Units: invertible elements in a ring\<close>
  12.118  
    13.1 --- a/src/HOL/Series.thy	Thu Aug 06 19:12:09 2015 +0200
    13.2 +++ b/src/HOL/Series.thy	Thu Aug 06 23:56:48 2015 +0200
    13.3 @@ -550,7 +550,7 @@
    13.4    fix n
    13.5    show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n"
    13.6      using r r0 M [of n]
    13.7 -    apply (auto simp add: abs_mult field_simps power_divide)
    13.8 +    apply (auto simp add: abs_mult field_simps)
    13.9      apply (cases "r=0", simp)
   13.10      apply (cases n, auto)
   13.11      done
    14.1 --- a/src/HOL/Transcendental.thy	Thu Aug 06 19:12:09 2015 +0200
    14.2 +++ b/src/HOL/Transcendental.thy	Thu Aug 06 23:56:48 2015 +0200
    14.3 @@ -160,7 +160,7 @@
    14.4    } note ** = this
    14.5    show ?thesis using *
    14.6      apply (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"])
    14.7 -    apply (simp add: N0 norm_mult nat_le_iff field_simps power_Suc ** 
    14.8 +    apply (simp add: N0 norm_mult field_simps ** 
    14.9                  del: of_nat_Suc real_of_int_add)
   14.10      done
   14.11  qed
   14.12 @@ -737,7 +737,7 @@
   14.13      by simp
   14.14    then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ n)"
   14.15      using False summable_mult2 [of "\<lambda>n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"]
   14.16 -    by (simp add: mult.assoc) (auto simp: power_Suc mult_ac)
   14.17 +    by (simp add: mult.assoc) (auto simp: ac_simps)
   14.18    then show ?thesis 
   14.19      by (simp add: diffs_def)
   14.20  qed
   14.21 @@ -1289,7 +1289,7 @@
   14.22  lemma exp_of_nat_mult:
   14.23    fixes x :: "'a::{real_normed_field,banach}"
   14.24    shows "exp(of_nat n * x) = exp(x) ^ n"
   14.25 -    by (induct n) (auto simp add: power_Suc distrib_left exp_add mult.commute)
   14.26 +    by (induct n) (auto simp add: distrib_left exp_add mult.commute)
   14.27  
   14.28  corollary exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
   14.29    by (simp add: exp_of_nat_mult real_of_nat_def)
   14.30 @@ -1668,7 +1668,7 @@
   14.31      hence "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
   14.32        by (rule le_imp_inverse_le) simp
   14.33      hence "inverse (fact (n + 2)) \<le> 1/(2::real) * (1/2)^n"
   14.34 -      by (simp add: power_inverse)
   14.35 +      by (simp add: power_inverse [symmetric])
   14.36      hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
   14.37        by (rule mult_mono)
   14.38          (rule mult_mono, simp_all add: power_le_one a b)
   14.39 @@ -2309,9 +2309,7 @@
   14.40    by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
   14.41  
   14.42  lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
   14.43 -  apply (induct n)
   14.44 -  apply simp
   14.45 -  by (simp add: add.commute power.simps(2) powr_add real_of_nat_Suc)
   14.46 +  by (induct n) (simp_all add: ac_simps powr_add real_of_nat_Suc)
   14.47  
   14.48  lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   14.49    unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
   14.50 @@ -3150,7 +3148,7 @@
   14.51          by (simp add: inverse_eq_divide less_divide_eq)
   14.52      } 
   14.53      then show ?thesis
   14.54 -      by (force intro!: sumr_pos_lt_pair [OF sm] simp add: power_Suc divide_inverse algebra_simps)
   14.55 +      by (force intro!: sumr_pos_lt_pair [OF sm] simp add: divide_inverse algebra_simps)
   14.56    qed
   14.57    ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
   14.58      by (rule order_less_trans)
   14.59 @@ -4403,9 +4401,7 @@
   14.60    shows "cos x \<noteq> 0 \<Longrightarrow> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
   14.61    apply (rule power_inverse [THEN subst])
   14.62    apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
   14.63 -  apply (auto dest: field_power_not_zero
   14.64 -          simp add: power_mult_distrib distrib_right power_divide tan_def
   14.65 -                    mult.assoc power_inverse [symmetric])
   14.66 +  apply (auto simp add: tan_def field_simps)
   14.67    done
   14.68  
   14.69  lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
   14.70 @@ -4524,7 +4520,8 @@
   14.71    apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
   14.72    apply (rule DERIV_cong [OF DERIV_tan])
   14.73    apply (rule cos_arctan_not_zero)
   14.74 -  apply (simp add: arctan power_inverse tan_sec [symmetric])
   14.75 +  apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
   14.76 +  apply (simp add: arctan power_inverse [symmetric] tan_sec [symmetric])
   14.77    apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
   14.78    apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
   14.79    done
   14.80 @@ -5426,7 +5423,7 @@
   14.81        unfolding Set_Interval.setsum_atMost_Suc_shift
   14.82        by simp
   14.83      also have "... = w * (\<Sum>i\<le>n. c (Suc i) * w^i)"
   14.84 -      by (simp add: power_Suc mult_ac setsum_right_distrib del: setsum_atMost_Suc)
   14.85 +      by (simp add: setsum_right_distrib ac_simps)
   14.86      finally have "(\<Sum>i\<le>Suc n. c i * w^i) = w * (\<Sum>i\<le>n. c (Suc i) * w^i)" .
   14.87    }
   14.88    then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
    15.1 --- a/src/HOL/Word/Bit_Representation.thy	Thu Aug 06 19:12:09 2015 +0200
    15.2 +++ b/src/HOL/Word/Bit_Representation.thy	Thu Aug 06 23:56:48 2015 +0200
    15.3 @@ -104,7 +104,7 @@
    15.4    "bin_last (numeral (Num.Bit1 w))"
    15.5    "\<not> bin_last (- numeral (Num.Bit0 w))"
    15.6    "bin_last (- numeral (Num.Bit1 w))"
    15.7 -  unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def zmod_zminus1_eq_if)
    15.8 +  by (simp_all add: bin_last_def zmod_zminus1_eq_if) (auto simp add: divmod_def)
    15.9  
   15.10  lemma bin_rest_numeral_simps [simp]:
   15.11    "bin_rest 0 = 0"
   15.12 @@ -115,7 +115,7 @@
   15.13    "bin_rest (numeral (Num.Bit1 w)) = numeral w"
   15.14    "bin_rest (- numeral (Num.Bit0 w)) = - numeral w"
   15.15    "bin_rest (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)"
   15.16 -  unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def zdiv_zminus1_eq_if)
   15.17 +  by (simp_all add: bin_rest_def zdiv_zminus1_eq_if) (auto simp add: divmod_def)
   15.18  
   15.19  lemma less_Bits: 
   15.20    "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"