# HG changeset patch
# User haftmann
# Date 1438898208 -7200
# Node ID 86e7560e07d0176fa35b1d1559f52d62d95c8c32
# Parent  7f562aa4eb4be91577e0cb13d98c8625b738f110
slight cleanup of lemmas

diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Divides.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -30,13 +30,17 @@
     using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
 qed simp
 
-lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>
-  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
-  by (induct n) (simp_all add: no_zero_divisors)
-
-lemma semiring_div_power_eq_0_iff: -- \<open>FIXME cf. @{text power_eq_0_iff}, @{text power_eq_0_nat_iff}\<close>
-  "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"
-  using power_not_zero [of a n] by (auto simp add: zero_power)
+lemma div_by_1:
+  "a div 1 = a"
+  by (fact divide_1)
+
+lemma div_mult_self1_is_id:
+  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
+  by (fact nonzero_mult_divide_cancel_left)
+
+lemma div_mult_self2_is_id:
+  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
+  by (fact nonzero_mult_divide_cancel_right)
 
 text \<open>@{const divide} and @{const mod}\<close>
 
@@ -104,31 +108,24 @@
   "(b * c + a) mod b = a mod b"
   by (simp add: add.commute)
 
-lemma div_mult_self1_is_id:
-  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
-  by (fact nonzero_mult_divide_cancel_left)
-
-lemma div_mult_self2_is_id:
-  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
-  by (fact nonzero_mult_divide_cancel_right)
-
-lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
+lemma mod_mult_self1_is_0 [simp]:
+  "b * a mod b = 0"
   using mod_mult_self2 [of 0 b a] by simp
 
-lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
+lemma mod_mult_self2_is_0 [simp]:
+  "a * b mod b = 0"
   using mod_mult_self1 [of 0 a b] by simp
 
-lemma div_by_1: "a div 1 = a"
-  by (fact divide_1)
-
-lemma mod_by_1 [simp]: "a mod 1 = 0"
+lemma mod_by_1 [simp]:
+  "a mod 1 = 0"
 proof -
   from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
   then have "a + a mod 1 = a + 0" by simp
   then show ?thesis by (rule add_left_imp_eq)
 qed
 
-lemma mod_self [simp]: "a mod a = 0"
+lemma mod_self [simp]:
+  "a mod a = 0"
   using mod_mult_self2_is_0 [of 1] by simp
 
 lemma div_add_self1 [simp]:
@@ -181,7 +178,7 @@
   then show "b dvd a" ..
 qed
 
-lemma dvd_eq_mod_eq_0 [code]:
+lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
   "a dvd b \<longleftrightarrow> b mod a = 0"
   by (simp add: mod_eq_0_iff_dvd)
 
@@ -212,17 +209,6 @@
   finally show ?thesis .
 qed
 
-lemma div_dvd_div [simp]:
-  assumes "a dvd b" and "a dvd c"
-  shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
-using assms apply (cases "a = 0")
-apply auto
-apply (unfold dvd_def)
-apply auto
- apply(blast intro:mult.assoc[symmetric])
-apply(fastforce simp add: mult.assoc)
-done
-
 lemma dvd_mod_imp_dvd:
   assumes "k dvd m mod n" and "k dvd n"
   shows "k dvd m"
@@ -234,7 +220,8 @@
 
 text \<open>Addition respects modular equivalence.\<close>
 
-lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
+lemma mod_add_left_eq: -- \<open>FIXME reorient\<close>
+  "(a + b) mod c = (a mod c + b) mod c"
 proof -
   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
     by (simp only: mod_div_equality)
@@ -245,7 +232,8 @@
   finally show ?thesis .
 qed
 
-lemma mod_add_right_eq: "(a + b) mod c = (a + b mod c) mod c"
+lemma mod_add_right_eq: -- \<open>FIXME reorient\<close>
+  "(a + b) mod c = (a + b mod c) mod c"
 proof -
   have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
     by (simp only: mod_div_equality)
@@ -256,7 +244,8 @@
   finally show ?thesis .
 qed
 
-lemma mod_add_eq: "(a + b) mod c = (a mod c + b mod c) mod c"
+lemma mod_add_eq: -- \<open>FIXME reorient\<close>
+  "(a + b) mod c = (a mod c + b mod c) mod c"
 by (rule trans [OF mod_add_left_eq mod_add_right_eq])
 
 lemma mod_add_cong:
@@ -270,13 +259,10 @@
     by (simp only: mod_add_eq [symmetric])
 qed
 
-lemma div_add [simp]: "z dvd x \<Longrightarrow> z dvd y
-  \<Longrightarrow> (x + y) div z = x div z + y div z"
-by (cases "z = 0", simp, unfold dvd_def, auto simp add: algebra_simps)
-
 text \<open>Multiplication respects modular equivalence.\<close>
 
-lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
+lemma mod_mult_left_eq: -- \<open>FIXME reorient\<close>
+  "(a * b) mod c = ((a mod c) * b) mod c"
 proof -
   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
     by (simp only: mod_div_equality)
@@ -287,7 +273,8 @@
   finally show ?thesis .
 qed
 
-lemma mod_mult_right_eq: "(a * b) mod c = (a * (b mod c)) mod c"
+lemma mod_mult_right_eq: -- \<open>FIXME reorient\<close>
+  "(a * b) mod c = (a * (b mod c)) mod c"
 proof -
   have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
     by (simp only: mod_div_equality)
@@ -298,7 +285,8 @@
   finally show ?thesis .
 qed
 
-lemma mod_mult_eq: "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
+lemma mod_mult_eq: -- \<open>FIXME reorient\<close>
+  "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
 by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
 
 lemma mod_mult_cong:
@@ -314,7 +302,7 @@
 
 text \<open>Exponentiation respects modular equivalence.\<close>
 
-lemma power_mod: "(a mod b)^n mod b = a^n mod b"
+lemma power_mod: "(a mod b) ^ n mod b = a ^ n mod b"
 apply (induct n, simp_all)
 apply (rule mod_mult_right_eq [THEN trans])
 apply (simp (no_asm_simp))
@@ -338,15 +326,6 @@
   finally show ?thesis .
 qed
 
-lemma div_mult_div_if_dvd:
-  "y dvd x \<Longrightarrow> z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
-  apply (cases "y = 0", simp)
-  apply (cases "z = 0", simp)
-  apply (auto elim!: dvdE simp add: algebra_simps)
-  apply (subst mult.assoc [symmetric])
-  apply (simp add: no_zero_divisors)
-  done
-
 lemma div_mult_mult2 [simp]:
   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   by (drule div_mult_mult1) (simp add: mult.commute)
@@ -384,31 +363,6 @@
 lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
 by (blast intro: dvd_mod_imp_dvd dvd_mod)
 
-lemma div_power:
-  "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n"
-apply (induct n)
- apply simp
-apply(simp add: div_mult_div_if_dvd dvd_power_same)
-done
-
-lemma dvd_div_eq_mult:
-  assumes "a \<noteq> 0" and "a dvd b"
-  shows "b div a = c \<longleftrightarrow> b = c * a"
-proof
-  assume "b = c * a"
-  then show "b div a = c" by (simp add: assms)
-next
-  assume "b div a = c"
-  then have "b div a * a = c * a" by simp
-  moreover from \<open>a dvd b\<close> have "b div a * a = b" by simp
-  ultimately show "b = c * a" by simp
-qed
-
-lemma dvd_div_div_eq_mult:
-  assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
-  shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
-  using assms by (auto simp add: mult.commute [of _ a] dvd_div_eq_mult div_mult_swap intro: sym)
-
 end
 
 class ring_div = comm_ring_1 + semiring_div
@@ -477,10 +431,9 @@
 apply simp
 done
 
-lemma div_diff[simp]:
-  "\<lbrakk> z dvd x; z dvd y\<rbrakk> \<Longrightarrow> (x - y) div z = x div z - y div z"
-using div_add[where y = "- z" for z]
-by (simp add: dvd_neg_div)
+lemma div_diff [simp]:
+  "z dvd x \<Longrightarrow> z dvd y \<Longrightarrow> (x - y) div z = x div z - y div z"
+  using div_add [of _ _ "- y"] by (simp add: dvd_neg_div)
 
 lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
   using div_mult_mult1 [of "- 1" a b]
@@ -670,7 +623,7 @@
     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
   with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
   then show ?P and ?Q
-    by (simp_all add: div mod add_implies_diff [symmetric] le_add_diff_inverse2)
+    by (simp_all add: div mod add_implies_diff [symmetric])
 qed
 
 lemma divmod_digit_0:
@@ -701,11 +654,11 @@
 where
   "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
 
-lemma fst_divmod [simp]:
+lemma fst_divmod:
   "fst (divmod m n) = numeral m div numeral n"
   by (simp add: divmod_def)
 
-lemma snd_divmod [simp]:
+lemma snd_divmod:
   "snd (divmod m n) = numeral m mod numeral n"
   by (simp add: divmod_def)
 
@@ -722,16 +675,11 @@
   and evaluate accordingly.
 \<close>
 
-lemma divmod_step_eq [code]:
+lemma divmod_step_eq [code, simp]:
   "divmod_step l (q, r) = (if numeral l \<le> r
     then (2 * q + 1, r - numeral l) else (2 * q, r))"
   by (simp add: divmod_step_def)
 
-lemma divmod_step_simps [simp]:
-  "r < numeral l \<Longrightarrow> divmod_step l (q, r) = (2 * q, r)"
-  "numeral l \<le> r \<Longrightarrow> divmod_step l (q, r) = (2 * q + 1, r - numeral l)"
-  by (auto simp add: divmod_step_eq not_le)
-
 text \<open>
   This is a formulation of school-method division.
   If the divisor is smaller than the dividend, terminate.
@@ -740,13 +688,13 @@
   opposite direction.
 \<close>
 
-lemma divmod_divmod_step [code]:
+lemma divmod_divmod_step:
   "divmod m n = (if m < n then (0, numeral m)
     else divmod_step n (divmod m (Num.Bit0 n)))"
 proof (cases "m < n")
   case True then have "numeral m < numeral n" by simp
   then show ?thesis
-    by (simp add: prod_eq_iff div_less mod_less)
+    by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
 next
   case False
   have "divmod m n =
@@ -754,10 +702,10 @@
       numeral m mod (2 * numeral n))"
   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
     case True
-    with divmod_step_simps
+    with divmod_step_eq
       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
-        by blast
+        by simp
     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
@@ -766,10 +714,10 @@
   next
     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
       by (simp add: not_le)
-    with divmod_step_simps
+    with divmod_step_eq
       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
-        by blast
+        by auto
     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
@@ -785,10 +733,17 @@
   with False show ?thesis by simp
 qed
 
-lemma divmod_eq [simp]:
-  "m < n \<Longrightarrow> divmod m n = (0, numeral m)"
-  "n \<le> m \<Longrightarrow> divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
-  by (auto simp add: divmod_divmod_step [of m n])
+text \<open>The division rewrite proper – first, trivial results involving @{text 1}\<close>
+
+lemma divmod_trivial [simp, code]:
+  "divmod Num.One Num.One = (numeral Num.One, 0)"
+  "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
+  "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
+  "divmod num.One (num.Bit0 n) = (0, Numeral1)"
+  "divmod num.One (num.Bit1 n) = (0, Numeral1)"
+  using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
+
+text \<open>Division by an even number is a right-shift\<close>
 
 lemma divmod_cancel [simp, code]:
   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
@@ -799,10 +754,26 @@
     by (simp_all only: numeral_mult numeral.simps distrib) simp_all
   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
   then show ?P and ?Q
-    by (simp_all add: prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
-      div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] add.commute del: numeral_times_numeral)
+    by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
+      div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
+      add.commute del: numeral_times_numeral)
 qed
 
+text \<open>The really hard work\<close>
+
+lemma divmod_steps [simp, code]:
+  "divmod (num.Bit0 m) (num.Bit1 n) =
+      (if m \<le> n then (0, numeral (num.Bit0 m))
+       else divmod_step (num.Bit1 n)
+             (divmod (num.Bit0 m)
+               (num.Bit0 (num.Bit1 n))))"
+  "divmod (num.Bit1 m) (num.Bit1 n) =
+      (if m < n then (0, numeral (num.Bit1 m))
+       else divmod_step (num.Bit1 n)
+             (divmod (num.Bit1 m)
+               (num.Bit0 (num.Bit1 n))))"
+  by (simp_all add: divmod_divmod_step)
+
 text \<open>Special case: divisibility\<close>
 
 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
@@ -817,6 +788,24 @@
   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
   by (simp add: divmod_def mod_eq_0_iff_dvd)
 
+text \<open>Generic computation of quotient and remainder\<close>  
+
+lemma numeral_div_numeral [simp]: 
+  "numeral k div numeral l = fst (divmod k l)"
+  by (simp add: fst_divmod)
+
+lemma numeral_mod_numeral [simp]: 
+  "numeral k mod numeral l = snd (divmod k l)"
+  by (simp add: snd_divmod)
+
+lemma one_div_numeral [simp]:
+  "1 div numeral n = fst (divmod num.One n)"
+  by (simp add: fst_divmod)
+
+lemma one_mod_numeral [simp]:
+  "1 mod numeral n = snd (divmod num.One n)"
+  by (simp add: snd_divmod)
+  
 end
 
 
@@ -1580,10 +1569,6 @@
     by simp
 qed
 
-lemma odd_Suc_minus_one [simp]:
-  "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
-  by (auto elim: oddE)
-
 lemma parity_induct [case_names zero even odd]:
   assumes zero: "P 0"
   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
@@ -2789,15 +2774,15 @@
 
 lemma div_nat_numeral [simp]:
   "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"
-  by (simp add: nat_div_distrib)
+  by (subst nat_div_distrib) simp_all
 
 lemma one_div_nat_numeral [simp]:
   "Suc 0 div numeral v' = nat (1 div numeral v')"
-  by (subst nat_div_distrib, simp_all)
+  by (subst nat_div_distrib) simp_all
 
 lemma mod_nat_numeral [simp]:
   "(numeral v :: nat) mod numeral v' = nat (numeral v mod numeral v')"
-  by (simp add: nat_mod_distrib)
+  by (subst nat_mod_distrib) simp_all
 
 lemma one_mod_nat_numeral [simp]:
   "Suc 0 mod numeral v' = nat (1 mod numeral v')"
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -240,6 +240,8 @@
 
 instance fps :: (semiring_0_cancel) semiring_0_cancel ..
 
+instance fps :: (semiring_1) semiring_1 ..
+
 
 subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close>
 
@@ -372,8 +374,9 @@
   by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1
     fps_const_add [symmetric])
 
-lemma neg_numeral_fps_const: "- numeral k = fps_const (- numeral k)"
-  by (simp only: numeral_fps_const fps_const_neg)
+lemma neg_numeral_fps_const:
+  "(- numeral k :: 'a :: ring_1 fps) = fps_const (- numeral k)"
+  by (simp add: numeral_fps_const)
 
 
 subsection \<open>The eXtractor series X\<close>
@@ -556,7 +559,7 @@
     unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
     by simp
   then have "x > (1 / y)^k" using yp
-    by (simp add: field_simps nonzero_power_divide)
+    by (simp add: field_simps)
   then show ?thesis
     using kp by blast
 qed
@@ -2201,7 +2204,7 @@
     from a0 b0 have ab0[simp]: "(a/b)$0 = a$0 / b$0"
       by (simp add: fps_divide_def fps_mult_nth divide_inverse fps_inverse_def)
     have th0: "r k ((a/b)$0) ^ k = (a/b)$0"
-      by (simp add: \<open>?lhs\<close> nonzero_power_divide[OF rb0'] ra0 rb0)
+      by (simp add: \<open>?lhs\<close> power_divide ra0 rb0)
     from a0 b0 ra0' rb0' kp \<open>?lhs\<close>
     have th1: "r k ((a / b) $ 0) = (fps_radical r k a / fps_radical r k b) $ 0"
       by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse)
@@ -2407,7 +2410,7 @@
 lemma fps_compose_0[simp]: "0 oo a = 0"
   by (simp add: fps_eq_iff fps_compose_nth)
 
-lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a$0)"
+lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a $ 0)"
   by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum.neutral)
 
 lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)"
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -175,7 +175,7 @@
   next
     show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
      apply (subst lemma_order_pderiv1)
-     by (metis * nd dvd_mult_cancel_right field_power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
+     by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
   qed
   then show ?thesis
     by (metis \<open>n = Suc n'\<close> pe)
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Aug 06 23:56:48 2015 +0200
@@ -1045,7 +1045,7 @@
       let
         val simp_ctxt =
           ctxt addsimps @{thms field_simps}
-          addsimps [@{thm nonzero_power_divide}, @{thm power_divide}]
+          addsimps [@{thm power_divide}]
         val th =
           Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
             (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -5257,7 +5257,7 @@
       also have "\<dots> < e * inverse 2 * 2"
         unfolding divide_inverse setsum_right_distrib[symmetric]
         apply (rule mult_strict_left_mono)
-        unfolding power_inverse lessThan_Suc_atMost[symmetric]
+        unfolding power_inverse [symmetric] lessThan_Suc_atMost[symmetric]
         apply (subst geometric_sum)
         using goal1
         apply auto
@@ -9892,7 +9892,7 @@
             show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
               unfolding power_add divide_inverse inverse_mult_distrib
               unfolding setsum_right_distrib[symmetric] setsum_left_distrib[symmetric]
-              unfolding power_inverse sum_gp
+              unfolding power_inverse [symmetric] sum_gp
               apply(rule mult_strict_left_mono[OF _ e])
               unfolding power2_eq_square
               apply auto
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -441,12 +441,12 @@
 
 lemma hyperpow_not_zero:
   "\<And>r n. r \<noteq> (0::'a::{field} star) ==> r pow n \<noteq> 0"
-by transfer (rule field_power_not_zero)
+by transfer (rule power_not_zero)
 
 lemma hyperpow_inverse:
   "\<And>r n. r \<noteq> (0::'a::field star)
    \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
-by transfer (rule power_inverse)
+by transfer (rule power_inverse [symmetric])
 
 lemma hyperpow_hrabs:
   "\<And>r n. abs (r::'a::{linordered_idom} star) pow n = abs (r pow n)"
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/NSA/NSComplex.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -377,19 +377,20 @@
 by transfer simp
 
 lemma hcpow_mult:
-  "!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
+  "((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
   by (fact hyperpow_mult)
 
 lemma hcpow_zero2 [simp]:
-  "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"
-by transfer (rule power_0_Suc)
+  "\<And>n. 0 pow (hSuc n) = (0::'a::semiring_1 star)"
+  by transfer (rule power_0_Suc)
 
 lemma hcpow_not_zero [simp,intro]:
   "!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)"
-by (rule hyperpow_not_zero)
+  by (fact hyperpow_not_zero)
 
-lemma hcpow_zero_zero: "r pow n = (0::hcomplex) ==> r = 0"
-by (blast intro: ccontr dest: hcpow_not_zero)
+lemma hcpow_zero_zero:
+  "r pow n = (0::hcomplex) ==> r = 0"
+  by (blast intro: ccontr dest: hcpow_not_zero)
 
 subsection{*The Function @{term hsgn}*}
 
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -688,7 +688,7 @@
   star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
 
 instance
-  by default (transfer, auto)+
+  by (standard; transfer) auto
 
 end
 
@@ -699,14 +699,14 @@
   star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
 
 instance
-  by default (transfer, auto)+
+  by (standard; transfer) auto
 
 end
 
 instance star :: (lattice) lattice ..
 
 instance star :: (distrib_lattice) distrib_lattice
-  by default (transfer, auto simp add: sup_inf_distrib1)
+  by (standard; transfer) (auto simp add: sup_inf_distrib1)
 
 lemma Standard_inf [simp]:
   "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
@@ -775,6 +775,8 @@
 apply (transfer, rule mult_1_right)
 done
 
+instance star :: (power) power ..
+
 instance star :: (comm_monoid_mult) comm_monoid_mult
 by (intro_classes, transfer, rule mult_1)
 
@@ -843,6 +845,8 @@
 instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors
   by (intro_classes; transfer) (fact no_zero_divisors)
 
+instance star :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors ..
+  
 instance star :: (semiring_no_zero_divisors_cancel) semiring_no_zero_divisors_cancel
   by (intro_classes; transfer) simp_all
 
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/NthRoot.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -112,7 +112,7 @@
   have x: "\<And>a b :: real. (0 < b \<and> a < 0) \<Longrightarrow> \<not> a > b" by auto
   fix a b :: real assume "0 < n" "sgn a * \<bar>a\<bar> ^ n < sgn b * \<bar>b\<bar> ^ n" then show "a < b"
     using power_less_imp_less_base[of a n b]  power_less_imp_less_base[of "-b" n "-a"]
-    by (simp add: sgn_real_def power_less_zero_eq x[of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
+    by (simp add: sgn_real_def x [of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
 qed
 
 lemma real_root_gt_zero: "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> 0 < root n x"
@@ -130,7 +130,7 @@
 by (auto simp add: order_le_less real_root_pow_pos)
 
 lemma sgn_root: "0 < n \<Longrightarrow> sgn (root n x) = sgn x"
-  by (auto split: split_root simp: sgn_real_def power_less_zero_eq)
+  by (auto split: split_root simp: sgn_real_def)
 
 lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
   using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: split_if_asm)
@@ -496,7 +496,7 @@
 done
 
 lemma real_inv_sqrt_pow2: "0 < x ==> (inverse (sqrt x))\<^sup>2 = inverse x"
-by (simp add: power_inverse [symmetric])
+by (simp add: power_inverse)
 
 lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
 by simp
@@ -525,7 +525,7 @@
   apply (cases "x = 0")
   apply simp_all
   using sqrt_divide_self_eq[of x]
-  apply (simp add: inverse_eq_divide field_simps)
+  apply (simp add: field_simps)
   done
 
 lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Parity.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -195,6 +195,10 @@
   shows "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
   using even_abs_add_iff [of l k] by (simp add: ac_simps)
 
+lemma odd_Suc_minus_one [simp]:
+  "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
+  by (auto elim: oddE)
+
 instance int :: ring_parity
 proof
   show "\<not> 2 dvd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Power.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -9,6 +9,19 @@
 imports Num Equiv_Relations
 begin
 
+context linordered_ring (* TODO: move *)
+begin
+
+lemma sum_squares_ge_zero:
+  "0 \<le> x * x + y * y"
+  by (intro add_nonneg_nonneg zero_le_square)
+
+lemma not_sum_squares_lt_zero:
+  "\<not> x * x + y * y < 0"
+  by (simp add: not_less sum_squares_ge_zero)
+
+end
+
 subsection \<open>Powers for Arbitrary Monoids\<close>
 
 class power = one + times
@@ -186,6 +199,15 @@
 lemma one_power2: "1\<^sup>2 = 1" (* delete? *)
   by (rule power_one)
 
+lemma power_0_Suc [simp]:
+  "0 ^ Suc n = 0"
+  by simp
+
+text\<open>It looks plausible as a simprule, but its effect can be strange.\<close>
+lemma power_0_left:
+  "0 ^ n = (if n = 0 then 1 else 0)"
+  by (cases n) simp_all
+
 end
 
 context comm_semiring_1
@@ -229,6 +251,32 @@
 
 end
 
+class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
+begin
+
+subclass power .
+
+lemma power_eq_0_iff [simp]:
+  "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
+  by (induct n) auto
+
+lemma power_not_zero:
+  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
+  by (induct n) auto
+
+lemma zero_eq_power2 [simp]:
+  "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
+  unfolding power2_eq_square by simp
+
+end
+
+context semidom
+begin
+
+subclass semiring_1_no_zero_divisors ..
+
+end
+
 context ring_1
 begin
 
@@ -252,7 +300,7 @@
 
 lemma power2_minus [simp]:
   "(- a)\<^sup>2 = a\<^sup>2"
-  by (rule power_minus_Bit0)
+  by (fact power_minus_Bit0)
 
 lemma power_minus1_even [simp]:
   "(- 1) ^ (2*n) = 1"
@@ -272,29 +320,14 @@
 
 end
 
-lemma power_eq_0_nat_iff [simp]:
-  fixes m n :: nat
-  shows "m ^ n = 0 \<longleftrightarrow> m = 0 \<and> n > 0"
-  by (induct n) auto
-
 context ring_1_no_zero_divisors
 begin
 
-lemma power_eq_0_iff [simp]:
-  "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
-  by (induct n) auto
-
-lemma field_power_not_zero:
-  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
-  by (induct n) auto
-
-lemma zero_eq_power2 [simp]:
-  "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
-  unfolding power2_eq_square by simp
+subclass semiring_1_no_zero_divisors .. 
 
 lemma power2_eq_1_iff:
   "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
-  unfolding power2_eq_square by (rule square_eq_1_iff)
+  using square_eq_1_iff [of a] by (simp add: power2_eq_square)
 
 end
 
@@ -306,6 +339,16 @@
 
 end
 
+context algebraic_semidom
+begin
+
+lemma div_power:
+  assumes "b dvd a"
+  shows "(a div b) ^ n = a ^ n div b ^ n"
+  using assms by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same)
+
+end
+
 context normalization_semidom
 begin
 
@@ -322,41 +365,42 @@
 context division_ring
 begin
 
-text \<open>FIXME reorient or rename to @{text nonzero_inverse_power}\<close>
-lemma nonzero_power_inverse:
-  "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
-  by (induct n)
-    (simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero)
+text\<open>Perhaps these should be simprules.\<close>
+lemma power_inverse [field_simps, divide_simps]:
+  "inverse a ^ n = inverse (a ^ n)"
+proof (cases "a = 0")
+  case True then show ?thesis by (simp add: power_0_left)
+next
+  case False then have "inverse (a ^ n) = inverse a ^ n"
+    by (induct n) (simp_all add: nonzero_inverse_mult_distrib power_commutes)
+  then show ?thesis by simp
+qed
 
-end
+lemma power_one_over [field_simps, divide_simps]:
+  "(1 / a) ^ n = 1 / a ^ n"
+  using power_inverse [of a] by (simp add: divide_inverse)
+
+end  
 
 context field
 begin
 
-lemma nonzero_power_divide:
-  "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
-  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
+lemma power_diff:
+  assumes nz: "a \<noteq> 0"
+  shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
+  by (induct m n rule: diff_induct) (simp_all add: nz power_not_zero)
 
-declare nonzero_power_divide [where b = "numeral w" for w, simp]
+lemma power_divide [field_simps, divide_simps]:
+  "(a / b) ^ n = a ^ n / b ^ n"
+  by (induct n) simp_all
+
+declare power_divide [where b = "numeral w" for w, simp]
 
 end
 
 
 subsection \<open>Exponentiation on ordered types\<close>
 
-context linordered_ring (* TODO: move *)
-begin
-
-lemma sum_squares_ge_zero:
-  "0 \<le> x * x + y * y"
-  by (intro add_nonneg_nonneg zero_le_square)
-
-lemma not_sum_squares_lt_zero:
-  "\<not> x * x + y * y < 0"
-  by (simp add: not_less sum_squares_ge_zero)
-
-end
-
 context linordered_semidom
 begin
 
@@ -702,12 +746,12 @@
 
 subsection \<open>Miscellaneous rules\<close>
 
-lemma self_le_power:
-  fixes x::"'a::linordered_semidom" 
-  shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n"
-  using power_increasing[of 1 n x] power_one_right[of x] by auto
+lemma (in linordered_semidom) self_le_power:
+  "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
+  using power_increasing [of 1 n a] power_one_right [of a] by auto
 
-lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
+lemma (in power) power_eq_if:
+  "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   unfolding One_nat_def by (cases m) simp_all
 
 lemma (in comm_semiring_1) power2_sum:
@@ -718,40 +762,6 @@
   "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
   by (simp add: algebra_simps power2_eq_square mult_2_right)
 
-lemma power_0_Suc [simp]:
-  "(0::'a::{power, semiring_0}) ^ Suc n = 0"
-  by simp
-
-text\<open>It looks plausible as a simprule, but its effect can be strange.\<close>
-lemma power_0_left:
-  "0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))"
-  by (induct n) simp_all
-
-lemma (in field) power_diff:
-  assumes nz: "a \<noteq> 0"
-  shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
-  by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero)
-
-text\<open>Perhaps these should be simprules.\<close>
-lemma power_inverse:
-  fixes a :: "'a::division_ring"
-  shows "inverse (a ^ n) = inverse a ^ n"
-apply (cases "a = 0")
-apply (simp add: power_0_left)
-apply (simp add: nonzero_power_inverse)
-done (* TODO: reorient or rename to inverse_power *)
-
-lemma power_one_over:
-  "1 / (a::'a::{field, power}) ^ n =  (1 / a) ^ n"
-  by (simp add: divide_inverse) (rule power_inverse)
-
-lemma power_divide [field_simps, divide_simps]:
-  "(a / b) ^ n = (a::'a::field) ^ n / b ^ n"
-apply (cases "b = 0")
-apply (simp add: power_0_left)
-apply (rule nonzero_power_divide)
-apply assumption
-done
 
 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
 
@@ -820,7 +830,7 @@
     assume "\<not> m \<le> n"
     then have "n < m" by simp
     with assms Suc show False
-      by (auto simp add: algebra_simps) (simp add: power2_eq_square)
+      by (simp add: power2_eq_square)
   qed
 qed
 
@@ -916,4 +926,3 @@
   code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end
-
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Rings.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -633,6 +633,20 @@
   "a div 1 = a"
   using nonzero_mult_divide_cancel_left [of 1 a] by simp
 
+end
+
+class idom_divide = idom + semidom_divide
+
+class algebraic_semidom = semidom_divide
+begin
+
+text \<open>
+  Class @{class algebraic_semidom} enriches a integral domain
+  by notions from algebra, like units in a ring.
+  It is a separate class to avoid spoiling fields with notions
+  which are degenerated there.
+\<close>
+
 lemma dvd_times_left_cancel_iff [simp]:
   assumes "a \<noteq> 0"
   shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
@@ -667,19 +681,60 @@
   with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
 qed
 
-end
+lemma div_dvd_div [simp]:
+  assumes "a dvd b" and "a dvd c"
+  shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
+proof (cases "a = 0")
+  case True with assms show ?thesis by simp
+next
+  case False
+  moreover from assms obtain k l where "b = a * k" and "c = a * l"
+    by (auto elim!: dvdE)
+  ultimately show ?thesis by simp
+qed
 
-class idom_divide = idom + semidom_divide
-
-class algebraic_semidom = semidom_divide
-begin
+lemma div_add [simp]:
+  assumes "c dvd a" and "c dvd b"
+  shows "(a + b) div c = a div c + b div c"
+proof (cases "c = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  moreover from assms obtain k l where "a = c * k" and "b = c * l"
+    by (auto elim!: dvdE)
+  moreover have "c * k + c * l = c * (k + l)"
+    by (simp add: algebra_simps)
+  ultimately show ?thesis
+    by simp
+qed
 
-text \<open>
-  Class @{class algebraic_semidom} enriches a integral domain
-  by notions from algebra, like units in a ring.
-  It is a separate class to avoid spoiling fields with notions
-  which are degenerated there.
-\<close>
+lemma div_mult_div_if_dvd:
+  assumes "b dvd a" and "d dvd c"
+  shows "(a div b) * (c div d) = (a * c) div (b * d)"
+proof (cases "b = 0 \<or> c = 0")
+  case True with assms show ?thesis by auto
+next
+  case False
+  moreover from assms obtain k l where "a = b * k" and "c = d * l"
+    by (auto elim!: dvdE)
+  moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
+    by (simp add: ac_simps)
+  ultimately show ?thesis by simp
+qed
+
+lemma dvd_div_eq_mult:
+  assumes "a \<noteq> 0" and "a dvd b"
+  shows "b div a = c \<longleftrightarrow> b = c * a"
+proof
+  assume "b = c * a"
+  then show "b div a = c" by (simp add: assms)
+next
+  assume "b div a = c"
+  then have "b div a * a = c * a" by simp
+  moreover from \<open>a \<noteq> 0\<close> \<open>a dvd b\<close> have "b div a * a = b"
+    by (auto elim!: dvdE simp add: ac_simps)
+  ultimately show "b = c * a" by simp
+qed
 
 lemma dvd_div_mult_self [simp]:
   "a dvd b \<Longrightarrow> b div a * a = b"
@@ -716,6 +771,22 @@
     by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
 qed
 
+lemma dvd_div_div_eq_mult:
+  assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
+  shows "b div a = d div c \<longleftrightarrow> b * c = a * d" (is "?P \<longleftrightarrow> ?Q")
+proof -
+  from assms have "a * c \<noteq> 0" by simp
+  then have "?P \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)"
+    by simp
+  also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a"
+    by (simp add: ac_simps)
+  also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a"
+    using assms by (simp add: div_mult_swap)
+  also have "\<dots> \<longleftrightarrow> ?Q"
+    using assms by (simp add: ac_simps)
+  finally show ?thesis .
+qed
+
 
 text \<open>Units: invertible elements in a ring\<close>
 
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Series.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -550,7 +550,7 @@
   fix n
   show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n"
     using r r0 M [of n]
-    apply (auto simp add: abs_mult field_simps power_divide)
+    apply (auto simp add: abs_mult field_simps)
     apply (cases "r=0", simp)
     apply (cases n, auto)
     done
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Transcendental.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -160,7 +160,7 @@
   } note ** = this
   show ?thesis using *
     apply (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"])
-    apply (simp add: N0 norm_mult nat_le_iff field_simps power_Suc ** 
+    apply (simp add: N0 norm_mult field_simps ** 
                 del: of_nat_Suc real_of_int_add)
     done
 qed
@@ -737,7 +737,7 @@
     by simp
   then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ n)"
     using False summable_mult2 [of "\<lambda>n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"]
-    by (simp add: mult.assoc) (auto simp: power_Suc mult_ac)
+    by (simp add: mult.assoc) (auto simp: ac_simps)
   then show ?thesis 
     by (simp add: diffs_def)
 qed
@@ -1289,7 +1289,7 @@
 lemma exp_of_nat_mult:
   fixes x :: "'a::{real_normed_field,banach}"
   shows "exp(of_nat n * x) = exp(x) ^ n"
-    by (induct n) (auto simp add: power_Suc distrib_left exp_add mult.commute)
+    by (induct n) (auto simp add: distrib_left exp_add mult.commute)
 
 corollary exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
   by (simp add: exp_of_nat_mult real_of_nat_def)
@@ -1668,7 +1668,7 @@
     hence "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
       by (rule le_imp_inverse_le) simp
     hence "inverse (fact (n + 2)) \<le> 1/(2::real) * (1/2)^n"
-      by (simp add: power_inverse)
+      by (simp add: power_inverse [symmetric])
     hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
       by (rule mult_mono)
         (rule mult_mono, simp_all add: power_le_one a b)
@@ -2309,9 +2309,7 @@
   by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
 
 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
-  apply (induct n)
-  apply simp
-  by (simp add: add.commute power.simps(2) powr_add real_of_nat_Suc)
+  by (induct n) (simp_all add: ac_simps powr_add real_of_nat_Suc)
 
 lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
@@ -3150,7 +3148,7 @@
         by (simp add: inverse_eq_divide less_divide_eq)
     } 
     then show ?thesis
-      by (force intro!: sumr_pos_lt_pair [OF sm] simp add: power_Suc divide_inverse algebra_simps)
+      by (force intro!: sumr_pos_lt_pair [OF sm] simp add: divide_inverse algebra_simps)
   qed
   ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
     by (rule order_less_trans)
@@ -4403,9 +4401,7 @@
   shows "cos x \<noteq> 0 \<Longrightarrow> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
   apply (rule power_inverse [THEN subst])
   apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
-  apply (auto dest: field_power_not_zero
-          simp add: power_mult_distrib distrib_right power_divide tan_def
-                    mult.assoc power_inverse [symmetric])
+  apply (auto simp add: tan_def field_simps)
   done
 
 lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
@@ -4524,7 +4520,8 @@
   apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
   apply (rule DERIV_cong [OF DERIV_tan])
   apply (rule cos_arctan_not_zero)
-  apply (simp add: arctan power_inverse tan_sec [symmetric])
+  apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
+  apply (simp add: arctan power_inverse [symmetric] tan_sec [symmetric])
   apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
   apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
   done
@@ -5426,7 +5423,7 @@
       unfolding Set_Interval.setsum_atMost_Suc_shift
       by simp
     also have "... = w * (\<Sum>i\<le>n. c (Suc i) * w^i)"
-      by (simp add: power_Suc mult_ac setsum_right_distrib del: setsum_atMost_Suc)
+      by (simp add: setsum_right_distrib ac_simps)
     finally have "(\<Sum>i\<le>Suc n. c i * w^i) = w * (\<Sum>i\<le>n. c (Suc i) * w^i)" .
   }
   then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -104,7 +104,7 @@
   "bin_last (numeral (Num.Bit1 w))"
   "\<not> bin_last (- numeral (Num.Bit0 w))"
   "bin_last (- numeral (Num.Bit1 w))"
-  unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def zmod_zminus1_eq_if)
+  by (simp_all add: bin_last_def zmod_zminus1_eq_if) (auto simp add: divmod_def)
 
 lemma bin_rest_numeral_simps [simp]:
   "bin_rest 0 = 0"
@@ -115,7 +115,7 @@
   "bin_rest (numeral (Num.Bit1 w)) = numeral w"
   "bin_rest (- numeral (Num.Bit0 w)) = - numeral w"
   "bin_rest (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)"
-  unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def zdiv_zminus1_eq_if)
+  by (simp_all add: bin_rest_def zdiv_zminus1_eq_if) (auto simp add: divmod_def)
 
 lemma less_Bits: 
   "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"