# HG changeset patch
# User haftmann
# Date 1414347076 -3600
# Node ID af9eb5e566dda25719b23eb92f37f8bba986652d
# Parent  fa5b67fb70adeeaba4e844de1e3d434ab109d68b
eliminated redundancies;
more simp rules

diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/GCD.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -870,7 +870,8 @@
       by (simp add: ab'(1,2)[symmetric])
     hence "?g^n*a'^n dvd ?g^n *b'^n"
       by (simp only: power_mult_distrib mult.commute)
-    with zn z n have th0:"a'^n dvd b'^n" by auto
+    then have th0: "a'^n dvd b'^n"
+      using zn by auto
     have "a' dvd a'^n" by (simp add: m)
     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
     hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/Library/Discrete.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -109,7 +109,16 @@
     by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
 qed
 
-lemma mono_sqrt: "mono sqrt"
+lemma sqrt_zero [simp]:
+  "sqrt 0 = 0"
+  using sqrt_inverse_power2 [of 0] by simp
+
+lemma sqrt_one [simp]:
+  "sqrt 1 = 1"
+  using sqrt_inverse_power2 [of 1] by simp
+
+lemma mono_sqrt:
+  "mono sqrt"
 proof
   fix m n :: nat
   have *: "0 * 0 \<le> m" by simp
@@ -140,7 +149,7 @@
 lemma sqrt_power2_le [simp]: (* FIXME tune proof *)
   "(sqrt n)\<^sup>2 \<le> n"
 proof (cases "n > 0")
-  case False then show ?thesis by (simp add: sqrt_def)
+  case False then show ?thesis by simp
 next
   case True then have "sqrt n > 0" by simp
   then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -1232,9 +1232,8 @@
 lemma ereal_power_divide:
   fixes x y :: ereal
   shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n"
-  by (cases rule: ereal2_cases[of x y])
-     (auto simp: one_ereal_def zero_ereal_def power_divide not_le
-                 power_less_zero_eq zero_le_power_iff)
+  by (cases rule: ereal2_cases [of x y])
+     (auto simp: one_ereal_def zero_ereal_def power_divide zero_le_power_eq)
 
 lemma ereal_le_mult_one_interval:
   fixes x y :: ereal
diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/Library/FinFun.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -890,7 +890,7 @@
 by(simp add: finfun_upd_apply)
 
 lemma finfun_ext: "(\<And>a. f $ a = g $ a) \<Longrightarrow> f = g"
-by(auto simp add: finfun_apply_inject[symmetric] simp del: finfun_apply_inject)
+by(auto simp add: finfun_apply_inject[symmetric])
 
 lemma expand_finfun_eq: "(f = g) = (op $ f = op $ g)"
 by(auto intro: finfun_ext)
@@ -1287,7 +1287,7 @@
 lemma finfun_dom_update [simp]:
   "finfun_dom (f(a $:= b)) = (finfun_dom f)(a $:= (b \<noteq> finfun_default f))"
 including finfun unfolding finfun_dom_def finfun_update_def
-apply(simp add: finfun_default_update_const fun_upd_apply finfun_dom_finfunI)
+apply(simp add: finfun_default_update_const finfun_dom_finfunI)
 apply(fold finfun_update.rep_eq)
 apply(simp add: finfun_upd_apply fun_eq_iff fun_upd_def finfun_default_update_const)
 done
@@ -1495,7 +1495,7 @@
     thus "finite (UNIV :: 'b set)"
       by(rule finite_imageD)(auto intro!: inj_onI)
   qed
-  with False show ?thesis by simp
+  with False show ?thesis by auto
 qed
 
 lemma finite_UNIV_finfun:
diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/NSA/NSComplex.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -374,11 +374,11 @@
 lemma hcpow_minus:
      "!!x n. (-x::hcomplex) pow n =
       (if ( *p* even) n then (x pow n) else -(x pow n))"
-by transfer (rule neg_power_if)
+by transfer simp
 
 lemma hcpow_mult:
   "!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
-by transfer (rule power_mult_distrib)
+  by (fact hyperpow_mult)
 
 lemma hcpow_zero2 [simp]:
   "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"
diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/Parity.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -3,148 +3,19 @@
     Author:     Jacques D. Fleuriot
 *)
 
-header {* Even and Odd for int and nat *}
+header {* Parity in rings and semirings *}
 
 theory Parity
 imports Nat_Transfer
 begin
 
-subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
-
-lemma two_dvd_Suc_Suc_iff [simp]:
-  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
-  using dvd_add_triv_right_iff [of 2 n] by simp
-
-lemma two_dvd_Suc_iff:
-  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
-  by (induct n) auto
-
-lemma two_dvd_diff_nat_iff:
-  fixes m n :: nat
-  shows "2 dvd m - n \<longleftrightarrow> m < n \<or> 2 dvd m + n"
-proof (cases "n \<le> m")
-  case True
-  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
-  moreover have "2 dvd m - n \<longleftrightarrow> 2 dvd m - n + n * 2" by simp
-  ultimately have "2 dvd m - n \<longleftrightarrow> 2 dvd m + n" by (simp only:)
-  then show ?thesis by auto
-next
-  case False
-  then show ?thesis by simp
-qed 
-  
-lemma two_dvd_diff_iff:
-  fixes k l :: int
-  shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
-  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
-
-lemma two_dvd_abs_add_iff:
-  fixes k l :: int
-  shows "2 dvd \<bar>k\<bar> + l \<longleftrightarrow> 2 dvd k + l"
-  by (cases "k \<ge> 0") (simp_all add: two_dvd_diff_iff ac_simps)
-
-lemma two_dvd_add_abs_iff:
-  fixes k l :: int
-  shows "2 dvd k + \<bar>l\<bar> \<longleftrightarrow> 2 dvd k + l"
-  using two_dvd_abs_add_iff [of l k] by (simp add: ac_simps)
-
-
-subsection {* Ring structures with parity *}
+subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
 
 class semiring_parity = semiring_dvd + semiring_numeral +
-  assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1"
-  assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
-  assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
-  assumes not_dvd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
-begin
-
-lemma two_dvd_plus_one_iff [simp]:
-  "2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a"
-  by (auto simp add: dvd_add_right_iff intro: not_dvd_not_dvd_dvd_add)
-
-lemma not_two_dvdE [elim?]:
-  assumes "\<not> 2 dvd a"
-  obtains b where "a = 2 * b + 1"
-proof -
-  from assms obtain b where *: "a = b + 1"
-    by (blast dest: not_dvd_ex_decrement)
-  with assms have "2 dvd b + 2" by simp
-  then have "2 dvd b" by simp
-  then obtain c where "b = 2 * c" ..
-  with * have "a = 2 * c + 1" by simp
-  with that show thesis .
-qed
-
-end
-
-instance nat :: semiring_parity
-proof
-  show "\<not> (2 :: nat) dvd 1"
-    by (rule notI, erule dvdE) simp
-next
-  fix m n :: nat
-  assume "\<not> 2 dvd m"
-  moreover assume "\<not> 2 dvd n"
-  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
-    by (simp add: two_dvd_Suc_iff)
-  then have "2 dvd Suc m + Suc n"
-    by (blast intro: dvd_add)
-  also have "Suc m + Suc n = m + n + 2"
-    by simp
-  finally show "2 dvd m + n"
-    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
-next
-  fix m n :: nat
-  assume *: "2 dvd m * n"
-  show "2 dvd m \<or> 2 dvd n"
-  proof (rule disjCI)
-    assume "\<not> 2 dvd n"
-    then have "2 dvd Suc n" by (simp add: two_dvd_Suc_iff)
-    then obtain r where "Suc n = 2 * r" ..
-    moreover from * obtain s where "m * n = 2 * s" ..
-    then have "2 * s + m = m * Suc n" by simp
-    ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
-    then have "m = 2 * (m * r - s)" by simp
-    then show "2 dvd m" ..
-  qed
-next
-  fix n :: nat
-  assume "\<not> 2 dvd n"
-  then show "\<exists>m. n = m + 1"
-    by (cases n) simp_all
-qed
-
-class ring_parity = comm_ring_1 + semiring_parity
-
-instance int :: ring_parity
-proof
-  show "\<not> (2 :: int) dvd 1" by (simp add: dvd_int_unfold_dvd_nat)
-  fix k l :: int
-  assume "\<not> 2 dvd k"
-  moreover assume "\<not> 2 dvd l"
-  ultimately have "2 dvd nat \<bar>k\<bar> + nat \<bar>l\<bar>" 
-    by (auto simp add: dvd_int_unfold_dvd_nat intro: not_dvd_not_dvd_dvd_add)
-  then have "2 dvd \<bar>k\<bar> + \<bar>l\<bar>"
-    by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
-  then show "2 dvd k + l"
-    by (simp add: two_dvd_abs_add_iff two_dvd_add_abs_iff)
-next
-  fix k l :: int
-  assume "2 dvd k * l"
-  then show "2 dvd k \<or> 2 dvd l"
-    by (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib)
-next
-  fix k :: int
-  have "k = (k - 1) + 1" by simp
-  then show "\<exists>l. k = l + 1" ..
-qed
-
-
-subsection {* Dedicated @{text even}/@{text odd} predicate *}
-
-subsubsection {* Properties *}
-
-context semiring_parity
+  assumes odd_one [simp]: "\<not> 2 dvd 1"
+  assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
+  assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
+  assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
 begin
 
 abbreviation even :: "'a \<Rightarrow> bool"
@@ -155,6 +26,14 @@
 where
   "odd a \<equiv> \<not> 2 dvd a"
 
+lemma even_zero [simp]:
+  "even 0"
+  by (fact dvd_0_right)
+
+lemma even_plus_one_iff [simp]:
+  "even (a + 1) \<longleftrightarrow> odd a"
+  by (auto simp add: dvd_add_right_iff intro: odd_even_add)
+
 lemma evenE [elim?]:
   assumes "even a"
   obtains b where "a = 2 * b"
@@ -163,19 +42,19 @@
 lemma oddE [elim?]:
   assumes "odd a"
   obtains b where "a = 2 * b + 1"
-  using assms by (rule not_two_dvdE)
-  
+proof -
+  from assms obtain b where *: "a = b + 1"
+    by (blast dest: odd_ex_decrement)
+  with assms have "even (b + 2)" by simp
+  then have "even b" by simp
+  then obtain c where "b = 2 * c" ..
+  with * have "a = 2 * c + 1" by simp
+  with that show thesis .
+qed
+ 
 lemma even_times_iff [simp]:
   "even (a * b) \<longleftrightarrow> even a \<or> even b"
-  by (auto simp add: dest: two_is_prime)
-
-lemma even_zero [simp]:
-  "even 0"
-  by simp
-
-lemma odd_one [simp]:
-  "odd 1"
-  by simp
+  by (auto dest: even_multD)
 
 lemma even_numeral [simp]:
   "even (numeral (Num.Bit0 n))"
@@ -206,7 +85,7 @@
 
 lemma even_add [simp]:
   "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
-  by (auto simp add: dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
+  by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
 
 lemma odd_add [simp]:
   "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
@@ -218,7 +97,7 @@
 
 end
 
-context ring_parity
+class ring_parity = comm_ring_1 + semiring_parity
 begin
 
 lemma even_minus [simp]:
@@ -232,22 +111,110 @@
 end
 
 
-subsubsection {* Particularities for @{typ nat} and @{typ int} *}
+subsection {* Instances for @{typ nat} and @{typ int} *}
+
+lemma even_Suc_Suc_iff [simp]:
+  "even (Suc (Suc n)) \<longleftrightarrow> even n"
+  using dvd_add_triv_right_iff [of 2 n] by simp
 
 lemma even_Suc [simp]:
-  "even (Suc n) = odd n"
-  by (fact two_dvd_Suc_iff)
+  "even (Suc n) \<longleftrightarrow> odd n"
+  by (induct n) auto
+
+lemma even_diff_nat [simp]:
+  fixes m n :: nat
+  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
+proof (cases "n \<le> m")
+  case True
+  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
+  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
+  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
+  then show ?thesis by auto
+next
+  case False
+  then show ?thesis by simp
+qed 
+  
+lemma even_diff_iff [simp]:
+  fixes k l :: int
+  shows "even (k - l) \<longleftrightarrow> even (k + l)"
+  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
+
+lemma even_abs_add_iff [simp]:
+  fixes k l :: int
+  shows "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)"
+  by (cases "k \<ge> 0") (simp_all add: ac_simps)
+
+lemma even_add_abs_iff [simp]:
+  fixes k l :: int
+  shows "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)"
+  using even_abs_add_iff [of l k] by (simp add: ac_simps)
+
+instance nat :: semiring_parity
+proof
+  show "odd (1 :: nat)"
+    by (rule notI, erule dvdE) simp
+next
+  fix m n :: nat
+  assume "odd m"
+  moreover assume "odd n"
+  ultimately have *: "even (Suc m) \<and> even (Suc n)"
+    by simp
+  then have "even (Suc m + Suc n)"
+    by (blast intro: dvd_add)
+  also have "Suc m + Suc n = m + n + 2"
+    by simp
+  finally show "even (m + n)"
+    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
+next
+  fix m n :: nat
+  assume *: "even (m * n)"
+  show "even m \<or> even n"
+  proof (rule disjCI)
+    assume "odd n"
+    then have "even (Suc n)" by simp
+    then obtain r where "Suc n = 2 * r" ..
+    moreover from * obtain s where "m * n = 2 * s" ..
+    then have "2 * s + m = m * Suc n" by simp
+    ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
+    then have "m = 2 * (m * r - s)" by simp
+    then show "even m" ..
+  qed
+next
+  fix n :: nat
+  assume "odd n"
+  then show "\<exists>m. n = m + 1"
+    by (cases n) simp_all
+qed
 
 lemma odd_pos: 
   "odd (n :: nat) \<Longrightarrow> 0 < n"
   by (auto elim: oddE)
   
-lemma even_diff_nat [simp]:
-  fixes m n :: nat
-  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
-  by (fact two_dvd_diff_nat_iff)
+instance int :: ring_parity
+proof
+  show "odd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
+  fix k l :: int
+  assume "odd k"
+  moreover assume "odd l"
+  ultimately have "even (nat \<bar>k\<bar> + nat \<bar>l\<bar>)" 
+    by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
+  then have "even (\<bar>k\<bar> + \<bar>l\<bar>)"
+    by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
+  then show "even (k + l)"
+    by simp
+next
+  fix k l :: int
+  assume "even (k * l)"
+  then show "even k \<or> even l"
+    by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
+next
+  fix k :: int
+  have "k = (k - 1) + 1" by simp
+  then show "\<exists>l. k = l + 1" ..
+qed
 
-lemma even_int_iff:
+lemma even_int_iff [simp]:
   "even (int n) \<longleftrightarrow> even n"
   by (simp add: dvd_int_iff)
 
@@ -255,11 +222,8 @@
   "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   by (simp add: even_int_iff [symmetric])
 
-lemma even_num_iff:
-  "0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)"
-  by simp
 
-text {* Parity and powers *}
+subsection {* Parity and powers *}
 
 context comm_ring_1
 begin
@@ -272,10 +236,6 @@
   "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
   by (auto elim: oddE)
 
-lemma neg_power_if:
-  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
-  by simp
-
 lemma neg_one_even_power [simp]:
   "even n \<Longrightarrow> (- 1) ^ n = 1"
   by simp
@@ -286,28 +246,9 @@
 
 end  
 
-lemma zero_less_power_nat_eq_numeral [simp]: -- \<open>FIXME move\<close>
-  "0 < (n :: nat) ^ numeral w \<longleftrightarrow> 0 < n \<or> numeral w = (0 :: nat)"
-  by (fact nat_zero_less_power_iff)
-
 context linordered_idom
 begin
 
-lemma power_eq_0_iff' [simp]: -- \<open>FIXME move\<close>
-  "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
-  by (induct n) auto
-
-lemma power2_less_eq_zero_iff [simp]: -- \<open>FIXME move\<close>
-  "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
-proof (cases "a = 0")
-  case True then show ?thesis by simp
-next
-  case False then have "a < 0 \<or> a > 0" by auto
-  then have "a\<^sup>2 > 0" by auto
-  then have "\<not> a\<^sup>2 \<le> 0" by (simp add: not_le)
-  with False show ?thesis by simp
-qed
-
 lemma zero_le_even_power:
   "even n \<Longrightarrow> 0 \<le> a ^ n"
   by (auto elim: evenE)
@@ -316,35 +257,20 @@
   "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
   by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
 
-lemma zero_le_power_iff: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
-  "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
-proof (cases "even n")
-  case True
-  then obtain k where "n = 2 * k" ..
-  then show ?thesis by simp
-next
-  case False
-  then obtain k where "n = 2 * k + 1" ..
-  moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
-    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
-  ultimately show ?thesis
-    by (auto simp add: zero_le_mult_iff zero_le_even_power)
-qed
-
 lemma zero_le_power_eq:
   "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
-  using zero_le_power_iff [of a n] by auto
-
+  by (auto simp add: zero_le_even_power zero_le_odd_power)
+  
 lemma zero_less_power_eq:
   "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
 proof -
   have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
-    unfolding power_eq_0_iff' [of a n, symmetric] by blast
+    unfolding power_eq_0_iff [of a n, symmetric] by blast
   show ?thesis
   unfolding less_le zero_le_power_eq by auto
 qed
 
-lemma power_less_zero_eq:
+lemma power_less_zero_eq [simp]:
   "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
   unfolding not_le [symmetric] zero_le_power_eq by auto
   
@@ -408,10 +334,6 @@
   "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0"
   by (fact power_less_zero_eq)
 
-lemma power_eq_0_iff_numeral [simp]:
-  "a ^ numeral w = (0 :: nat) \<longleftrightarrow> a = 0 \<and> numeral w \<noteq> (0 :: nat)"
-  by (fact power_eq_0_iff)
-
 lemma power_even_abs_numeral [simp]:
   "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w"
   by (fact power_even_abs)
diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/Power.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -244,9 +244,18 @@
 
 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
@@ -559,6 +568,10 @@
   "\<not> a\<^sup>2 < 0"
   by (force simp add: power2_eq_square mult_less_0_iff)
 
+lemma power2_less_eq_zero_iff [simp]:
+  "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
+  by (simp add: le_less)
+
 lemma abs_power2 [simp]:
   "abs (a\<^sup>2) = a\<^sup>2"
   by (simp add: power2_eq_square abs_mult abs_mult_self)
@@ -631,15 +644,13 @@
 lemma 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 power2_sum:
-  fixes x y :: "'a::comm_semiring_1"
-  shows "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y"
+lemma (in comm_semiring_1) power2_sum:
+  "(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 power2_diff:
-  fixes x y :: "'a::comm_ring_1"
-  shows "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
-  by (simp add: ring_distribs power2_eq_square mult_2) (rule mult.commute)
+lemma (in comm_ring_1) power2_diff:
+  "(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"
@@ -650,12 +661,6 @@
   "0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))"
   by (induct n) simp_all
 
-lemma power_eq_0_iff [simp]:
-  "a ^ n = 0 \<longleftrightarrow>
-     a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,power}) \<and> n \<noteq> 0"
-  by (induct n)
-    (auto simp add: no_zero_divisors elim: contrapos_pp)
-
 lemma (in field) power_diff:
   assumes nz: "a \<noteq> 0"
   shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/Presburger.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -457,8 +457,6 @@
 context linordered_idom
 begin
 
-declare zero_le_power_iff [presburger]
-
 declare zero_le_power_eq [presburger]
 
 declare zero_less_power_eq [presburger]
diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -425,8 +425,8 @@
 qed
 
 lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \<noteq> c"
-  using AE_discrete_difference[of "{c::'a}" lborel] emeasure_lborel_cbox[of c c]
-  by (auto simp del: emeasure_lborel_cbox simp add: cbox_sing setprod_constant)
+  using SOME_Basis AE_discrete_difference [of "{c}" lborel]
+    emeasure_lborel_cbox [of c c] by (auto simp add: cbox_sing)
 
 lemma emeasure_lborel_Ioo[simp]:
   assumes [simp]: "l \<le> u"