1.1 --- a/src/HOL/Nat_Numeral.thy Tue Apr 28 13:34:48 2009 +0200
1.2 +++ b/src/HOL/Nat_Numeral.thy Tue Apr 28 15:50:29 2009 +0200
1.3 @@ -10,6 +10,8 @@
1.4 uses ("Tools/nat_simprocs.ML")
1.5 begin
1.6
1.7 +subsection {* Numerals for natural numbers *}
1.8 +
1.9 text {*
1.10 Arithmetic for naturals is reduced to that for the non-negative integers.
1.11 *}
1.12 @@ -28,7 +30,16 @@
1.13 "nat (number_of v) = number_of v"
1.14 unfolding nat_number_of_def ..
1.15
1.16 -context recpower
1.17 +
1.18 +subsection {* Special case: squares and cubes *}
1.19 +
1.20 +lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
1.21 + by (simp add: nat_number_of_def)
1.22 +
1.23 +lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
1.24 + by (simp add: nat_number_of_def)
1.25 +
1.26 +context power
1.27 begin
1.28
1.29 abbreviation (xsymbols)
1.30 @@ -43,6 +54,205 @@
1.31
1.32 end
1.33
1.34 +context monoid_mult
1.35 +begin
1.36 +
1.37 +lemma power2_eq_square: "a\<twosuperior> = a * a"
1.38 + by (simp add: numeral_2_eq_2)
1.39 +
1.40 +lemma power3_eq_cube: "a ^ 3 = a * a * a"
1.41 + by (simp add: numeral_3_eq_3 mult_assoc)
1.42 +
1.43 +lemma power_even_eq:
1.44 + "a ^ (2*n) = (a ^ n) ^ 2"
1.45 + by (subst OrderedGroup.mult_commute) (simp add: power_mult)
1.46 +
1.47 +lemma power_odd_eq:
1.48 + "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
1.49 + by (simp add: power_even_eq)
1.50 +
1.51 +end
1.52 +
1.53 +context semiring_1
1.54 +begin
1.55 +
1.56 +lemma zero_power2 [simp]: "0\<twosuperior> = 0"
1.57 + by (simp add: power2_eq_square)
1.58 +
1.59 +lemma one_power2 [simp]: "1\<twosuperior> = 1"
1.60 + by (simp add: power2_eq_square)
1.61 +
1.62 +end
1.63 +
1.64 +context comm_ring_1
1.65 +begin
1.66 +
1.67 +lemma power2_minus [simp]:
1.68 + "(- a)\<twosuperior> = a\<twosuperior>"
1.69 + by (simp add: power2_eq_square)
1.70 +
1.71 +text{*
1.72 + We cannot prove general results about the numeral @{term "-1"},
1.73 + so we have to use @{term "- 1"} instead.
1.74 +*}
1.75 +
1.76 +lemma power_minus1_even [simp]:
1.77 + "(- 1) ^ (2*n) = 1"
1.78 +proof (induct n)
1.79 + case 0 show ?case by simp
1.80 +next
1.81 + case (Suc n) then show ?case by (simp add: power_add)
1.82 +qed
1.83 +
1.84 +lemma power_minus1_odd:
1.85 + "(- 1) ^ Suc (2*n) = - 1"
1.86 + by simp
1.87 +
1.88 +lemma power_minus_even [simp]:
1.89 + "(-a) ^ (2*n) = a ^ (2*n)"
1.90 + by (simp add: power_minus [of a])
1.91 +
1.92 +end
1.93 +
1.94 +context ordered_ring_strict
1.95 +begin
1.96 +
1.97 +lemma sum_squares_ge_zero:
1.98 + "0 \<le> x * x + y * y"
1.99 + by (intro add_nonneg_nonneg zero_le_square)
1.100 +
1.101 +lemma not_sum_squares_lt_zero:
1.102 + "\<not> x * x + y * y < 0"
1.103 + by (simp add: not_less sum_squares_ge_zero)
1.104 +
1.105 +lemma sum_squares_eq_zero_iff:
1.106 + "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
1.107 + by (simp add: sum_nonneg_eq_zero_iff)
1.108 +
1.109 +lemma sum_squares_le_zero_iff:
1.110 + "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
1.111 + by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
1.112 +
1.113 +lemma sum_squares_gt_zero_iff:
1.114 + "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
1.115 +proof -
1.116 + have "x * x + y * y \<noteq> 0 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
1.117 + by (simp add: sum_squares_eq_zero_iff)
1.118 + then have "0 \<noteq> x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
1.119 + by auto
1.120 + then show ?thesis
1.121 + by (simp add: less_le sum_squares_ge_zero)
1.122 +qed
1.123 +
1.124 +end
1.125 +
1.126 +context ordered_semidom
1.127 +begin
1.128 +
1.129 +lemma power2_le_imp_le:
1.130 + "x\<twosuperior> \<le> y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
1.131 + unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
1.132 +
1.133 +lemma power2_less_imp_less:
1.134 + "x\<twosuperior> < y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
1.135 + by (rule power_less_imp_less_base)
1.136 +
1.137 +lemma power2_eq_imp_eq:
1.138 + "x\<twosuperior> = y\<twosuperior> \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
1.139 + unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
1.140 +
1.141 +end
1.142 +
1.143 +context ordered_idom
1.144 +begin
1.145 +
1.146 +lemma zero_eq_power2 [simp]:
1.147 + "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
1.148 + by (force simp add: power2_eq_square)
1.149 +
1.150 +lemma zero_le_power2 [simp]:
1.151 + "0 \<le> a\<twosuperior>"
1.152 + by (simp add: power2_eq_square)
1.153 +
1.154 +lemma zero_less_power2 [simp]:
1.155 + "0 < a\<twosuperior> \<longleftrightarrow> a \<noteq> 0"
1.156 + by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
1.157 +
1.158 +lemma power2_less_0 [simp]:
1.159 + "\<not> a\<twosuperior> < 0"
1.160 + by (force simp add: power2_eq_square mult_less_0_iff)
1.161 +
1.162 +lemma abs_power2 [simp]:
1.163 + "abs (a\<twosuperior>) = a\<twosuperior>"
1.164 + by (simp add: power2_eq_square abs_mult abs_mult_self)
1.165 +
1.166 +lemma power2_abs [simp]:
1.167 + "(abs a)\<twosuperior> = a\<twosuperior>"
1.168 + by (simp add: power2_eq_square abs_mult_self)
1.169 +
1.170 +lemma odd_power_less_zero:
1.171 + "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
1.172 +proof (induct n)
1.173 + case 0
1.174 + then show ?case by simp
1.175 +next
1.176 + case (Suc n)
1.177 + have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
1.178 + by (simp add: mult_ac power_add power2_eq_square)
1.179 + thus ?case
1.180 + by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
1.181 +qed
1.182 +
1.183 +lemma odd_0_le_power_imp_0_le:
1.184 + "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
1.185 + using odd_power_less_zero [of a n]
1.186 + by (force simp add: linorder_not_less [symmetric])
1.187 +
1.188 +lemma zero_le_even_power'[simp]:
1.189 + "0 \<le> a ^ (2*n)"
1.190 +proof (induct n)
1.191 + case 0
1.192 + show ?case by (simp add: zero_le_one)
1.193 +next
1.194 + case (Suc n)
1.195 + have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
1.196 + by (simp add: mult_ac power_add power2_eq_square)
1.197 + thus ?case
1.198 + by (simp add: Suc zero_le_mult_iff)
1.199 +qed
1.200 +
1.201 +lemma sum_power2_ge_zero:
1.202 + "0 \<le> x\<twosuperior> + y\<twosuperior>"
1.203 + unfolding power2_eq_square by (rule sum_squares_ge_zero)
1.204 +
1.205 +lemma not_sum_power2_lt_zero:
1.206 + "\<not> x\<twosuperior> + y\<twosuperior> < 0"
1.207 + unfolding power2_eq_square by (rule not_sum_squares_lt_zero)
1.208 +
1.209 +lemma sum_power2_eq_zero_iff:
1.210 + "x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
1.211 + unfolding power2_eq_square by (rule sum_squares_eq_zero_iff)
1.212 +
1.213 +lemma sum_power2_le_zero_iff:
1.214 + "x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
1.215 + unfolding power2_eq_square by (rule sum_squares_le_zero_iff)
1.216 +
1.217 +lemma sum_power2_gt_zero_iff:
1.218 + "0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
1.219 + unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
1.220 +
1.221 +end
1.222 +
1.223 +lemma power2_sum:
1.224 + fixes x y :: "'a::number_ring"
1.225 + shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
1.226 + by (simp add: ring_distribs power2_eq_square)
1.227 +
1.228 +lemma power2_diff:
1.229 + fixes x y :: "'a::number_ring"
1.230 + shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
1.231 + by (simp add: ring_distribs power2_eq_square)
1.232 +
1.233
1.234 subsection {* Predicate for negative binary numbers *}
1.235
1.236 @@ -115,11 +325,6 @@
1.237 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
1.238 by (simp add: nat_numeral_1_eq_1)
1.239
1.240 -lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
1.241 -apply (unfold nat_number_of_def)
1.242 -apply (rule nat_2)
1.243 -done
1.244 -
1.245
1.246 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
1.247
1.248 @@ -314,128 +519,10 @@
1.249
1.250 subsection{*Powers with Numeric Exponents*}
1.251
1.252 -text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
1.253 -We cannot prove general results about the numeral @{term "-1"}, so we have to
1.254 -use @{term "- 1"} instead.*}
1.255 +text{*Squares of literal numerals will be evaluated.*}
1.256 +lemmas power2_eq_square_number_of [simp] =
1.257 + power2_eq_square [of "number_of w", standard]
1.258
1.259 -lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
1.260 - by (simp add: numeral_2_eq_2 Power.power_Suc)
1.261 -
1.262 -lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
1.263 - by (simp add: power2_eq_square)
1.264 -
1.265 -lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
1.266 - by (simp add: power2_eq_square)
1.267 -
1.268 -lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
1.269 - apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
1.270 - apply (erule ssubst)
1.271 - apply (simp add: power_Suc mult_ac)
1.272 - apply (unfold nat_number_of_def)
1.273 - apply (subst nat_eq_iff)
1.274 - apply simp
1.275 -done
1.276 -
1.277 -text{*Squares of literal numerals will be evaluated.*}
1.278 -lemmas power2_eq_square_number_of =
1.279 - power2_eq_square [of "number_of w", standard]
1.280 -declare power2_eq_square_number_of [simp]
1.281 -
1.282 -
1.283 -lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
1.284 - by (simp add: power2_eq_square)
1.285 -
1.286 -lemma zero_less_power2[simp]:
1.287 - "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
1.288 - by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
1.289 -
1.290 -lemma power2_less_0[simp]:
1.291 - fixes a :: "'a::{ordered_idom,recpower}"
1.292 - shows "~ (a\<twosuperior> < 0)"
1.293 -by (force simp add: power2_eq_square mult_less_0_iff)
1.294 -
1.295 -lemma zero_eq_power2[simp]:
1.296 - "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
1.297 - by (force simp add: power2_eq_square mult_eq_0_iff)
1.298 -
1.299 -lemma abs_power2[simp]:
1.300 - "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
1.301 - by (simp add: power2_eq_square abs_mult abs_mult_self)
1.302 -
1.303 -lemma power2_abs[simp]:
1.304 - "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
1.305 - by (simp add: power2_eq_square abs_mult_self)
1.306 -
1.307 -lemma power2_minus[simp]:
1.308 - "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
1.309 - by (simp add: power2_eq_square)
1.310 -
1.311 -lemma power2_le_imp_le:
1.312 - fixes x y :: "'a::{ordered_semidom,recpower}"
1.313 - shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
1.314 -unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
1.315 -
1.316 -lemma power2_less_imp_less:
1.317 - fixes x y :: "'a::{ordered_semidom,recpower}"
1.318 - shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
1.319 -by (rule power_less_imp_less_base)
1.320 -
1.321 -lemma power2_eq_imp_eq:
1.322 - fixes x y :: "'a::{ordered_semidom,recpower}"
1.323 - shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
1.324 -unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
1.325 -
1.326 -lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
1.327 -proof (induct n)
1.328 - case 0 show ?case by simp
1.329 -next
1.330 - case (Suc n) then show ?case by (simp add: power_Suc power_add)
1.331 -qed
1.332 -
1.333 -lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
1.334 - by (simp add: power_Suc)
1.335 -
1.336 -lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
1.337 - by (subst mult_commute) (simp add: power_mult)
1.338 -
1.339 -lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
1.340 - by (simp add: power_even_eq)
1.341 -
1.342 -lemma power_minus_even [simp]:
1.343 - "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
1.344 - by (simp add: power_minus [of a])
1.345 -
1.346 -lemma zero_le_even_power'[simp]:
1.347 - "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
1.348 -proof (induct "n")
1.349 - case 0
1.350 - show ?case by (simp add: zero_le_one)
1.351 -next
1.352 - case (Suc n)
1.353 - have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
1.354 - by (simp add: mult_ac power_add power2_eq_square)
1.355 - thus ?case
1.356 - by (simp add: prems zero_le_mult_iff)
1.357 -qed
1.358 -
1.359 -lemma odd_power_less_zero:
1.360 - "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
1.361 -proof (induct "n")
1.362 - case 0
1.363 - then show ?case by simp
1.364 -next
1.365 - case (Suc n)
1.366 - have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
1.367 - by (simp add: mult_ac power_add power2_eq_square)
1.368 - thus ?case
1.369 - by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
1.370 -qed
1.371 -
1.372 -lemma odd_0_le_power_imp_0_le:
1.373 - "0 \<le> a ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
1.374 -apply (insert odd_power_less_zero [of a n])
1.375 -apply (force simp add: linorder_not_less [symmetric])
1.376 -done
1.377
1.378 text{*Simprules for comparisons where common factors can be cancelled.*}
1.379 lemmas zero_compare_simps =
1.380 @@ -621,7 +708,7 @@
1.381 text{*For arbitrary rings*}
1.382
1.383 lemma power_number_of_even:
1.384 - fixes z :: "'a::{number_ring,recpower}"
1.385 + fixes z :: "'a::number_ring"
1.386 shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
1.387 unfolding Let_def nat_number_of_def number_of_Bit0
1.388 apply (rule_tac x = "number_of w" in spec, clarify)
1.389 @@ -630,7 +717,7 @@
1.390 done
1.391
1.392 lemma power_number_of_odd:
1.393 - fixes z :: "'a::{number_ring,recpower}"
1.394 + fixes z :: "'a::number_ring"
1.395 shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
1.396 then (let w = z ^ (number_of w) in z * w * w) else 1)"
1.397 unfolding Let_def nat_number_of_def number_of_Bit1
1.398 @@ -697,11 +784,11 @@
1.399 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
1.400 by (simp add: Let_def)
1.401
1.402 -lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
1.403 -by (simp add: power_mult power_Suc);
1.404 +lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})"
1.405 + by (simp only: number_of_Min power_minus1_even)
1.406
1.407 -lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
1.408 -by (simp add: power_mult power_Suc);
1.409 +lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring})"
1.410 + by (simp only: number_of_Min power_minus1_odd)
1.411
1.412
1.413 subsection{*Literal arithmetic and @{term of_nat}*}
2.1 --- a/src/HOL/NthRoot.thy Tue Apr 28 13:34:48 2009 +0200
2.2 +++ b/src/HOL/NthRoot.thy Tue Apr 28 15:50:29 2009 +0200
2.3 @@ -565,16 +565,6 @@
2.4 lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
2.5 by (simp add: power2_eq_square [symmetric])
2.6
2.7 -lemma power2_sum:
2.8 - fixes x y :: "'a::{number_ring,recpower}"
2.9 - shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
2.10 -by (simp add: ring_distribs power2_eq_square)
2.11 -
2.12 -lemma power2_diff:
2.13 - fixes x y :: "'a::{number_ring,recpower}"
2.14 - shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
2.15 -by (simp add: ring_distribs power2_eq_square)
2.16 -
2.17 lemma real_sqrt_sum_squares_triangle_ineq:
2.18 "sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
2.19 apply (rule power2_le_imp_le, simp)
3.1 --- a/src/HOL/RealPow.thy Tue Apr 28 13:34:48 2009 +0200
3.2 +++ b/src/HOL/RealPow.thy Tue Apr 28 15:50:29 2009 +0200
3.3 @@ -83,75 +83,6 @@
3.4 declare power_real_number_of [of _ "number_of w", standard, simp]
3.5
3.6
3.7 -subsection {* Properties of Squares *}
3.8 -
3.9 -lemma sum_squares_ge_zero:
3.10 - fixes x y :: "'a::ordered_ring_strict"
3.11 - shows "0 \<le> x * x + y * y"
3.12 -by (intro add_nonneg_nonneg zero_le_square)
3.13 -
3.14 -lemma not_sum_squares_lt_zero:
3.15 - fixes x y :: "'a::ordered_ring_strict"
3.16 - shows "\<not> x * x + y * y < 0"
3.17 -by (simp add: linorder_not_less sum_squares_ge_zero)
3.18 -
3.19 -lemma sum_nonneg_eq_zero_iff:
3.20 - fixes x y :: "'a::pordered_ab_group_add"
3.21 - assumes x: "0 \<le> x" and y: "0 \<le> y"
3.22 - shows "(x + y = 0) = (x = 0 \<and> y = 0)"
3.23 -proof (auto)
3.24 - from y have "x + 0 \<le> x + y" by (rule add_left_mono)
3.25 - also assume "x + y = 0"
3.26 - finally have "x \<le> 0" by simp
3.27 - thus "x = 0" using x by (rule order_antisym)
3.28 -next
3.29 - from x have "0 + y \<le> x + y" by (rule add_right_mono)
3.30 - also assume "x + y = 0"
3.31 - finally have "y \<le> 0" by simp
3.32 - thus "y = 0" using y by (rule order_antisym)
3.33 -qed
3.34 -
3.35 -lemma sum_squares_eq_zero_iff:
3.36 - fixes x y :: "'a::ordered_ring_strict"
3.37 - shows "(x * x + y * y = 0) = (x = 0 \<and> y = 0)"
3.38 -by (simp add: sum_nonneg_eq_zero_iff)
3.39 -
3.40 -lemma sum_squares_le_zero_iff:
3.41 - fixes x y :: "'a::ordered_ring_strict"
3.42 - shows "(x * x + y * y \<le> 0) = (x = 0 \<and> y = 0)"
3.43 -by (simp add: order_le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
3.44 -
3.45 -lemma sum_squares_gt_zero_iff:
3.46 - fixes x y :: "'a::ordered_ring_strict"
3.47 - shows "(0 < x * x + y * y) = (x \<noteq> 0 \<or> y \<noteq> 0)"
3.48 -by (simp add: order_less_le sum_squares_ge_zero sum_squares_eq_zero_iff)
3.49 -
3.50 -lemma sum_power2_ge_zero:
3.51 - fixes x y :: "'a::{ordered_idom,recpower}"
3.52 - shows "0 \<le> x\<twosuperior> + y\<twosuperior>"
3.53 -unfolding power2_eq_square by (rule sum_squares_ge_zero)
3.54 -
3.55 -lemma not_sum_power2_lt_zero:
3.56 - fixes x y :: "'a::{ordered_idom,recpower}"
3.57 - shows "\<not> x\<twosuperior> + y\<twosuperior> < 0"
3.58 -unfolding power2_eq_square by (rule not_sum_squares_lt_zero)
3.59 -
3.60 -lemma sum_power2_eq_zero_iff:
3.61 - fixes x y :: "'a::{ordered_idom,recpower}"
3.62 - shows "(x\<twosuperior> + y\<twosuperior> = 0) = (x = 0 \<and> y = 0)"
3.63 -unfolding power2_eq_square by (rule sum_squares_eq_zero_iff)
3.64 -
3.65 -lemma sum_power2_le_zero_iff:
3.66 - fixes x y :: "'a::{ordered_idom,recpower}"
3.67 - shows "(x\<twosuperior> + y\<twosuperior> \<le> 0) = (x = 0 \<and> y = 0)"
3.68 -unfolding power2_eq_square by (rule sum_squares_le_zero_iff)
3.69 -
3.70 -lemma sum_power2_gt_zero_iff:
3.71 - fixes x y :: "'a::{ordered_idom,recpower}"
3.72 - shows "(0 < x\<twosuperior> + y\<twosuperior>) = (x \<noteq> 0 \<or> y \<noteq> 0)"
3.73 -unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
3.74 -
3.75 -
3.76 subsection{* Squares of Reals *}
3.77
3.78 lemma real_two_squares_add_zero_iff [simp]: