--- 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)
--- 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)
--- 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
--- 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:
--- 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)"
--- 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)
--- 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"
--- 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]
--- 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"