generalize some lemmas from class linordered_ring_strict to linordered_ring
authorhuffman
Sat Mar 06 18:24:30 2010 -0800 (2010-03-06)
changeset 356310b8a5fd339ab
parent 35630 8e562d56d404
child 35632 61fd75e33137
generalize some lemmas from class linordered_ring_strict to linordered_ring
src/HOL/Nat_Numeral.thy
src/HOL/Parity.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Nat_Numeral.thy	Sat Mar 06 16:02:22 2010 -0800
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Sat Mar 06 18:24:30 2010 -0800
     1.3 @@ -113,7 +113,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -context linordered_ring_strict
     1.8 +context linordered_ring
     1.9  begin
    1.10  
    1.11  lemma sum_squares_ge_zero:
    1.12 @@ -124,6 +124,11 @@
    1.13    "\<not> x * x + y * y < 0"
    1.14    by (simp add: not_less sum_squares_ge_zero)
    1.15  
    1.16 +end
    1.17 +
    1.18 +context linordered_ring_strict
    1.19 +begin
    1.20 +
    1.21  lemma sum_squares_eq_zero_iff:
    1.22    "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
    1.23    by (simp add: add_nonneg_eq_0_iff)
    1.24 @@ -134,14 +139,7 @@
    1.25  
    1.26  lemma sum_squares_gt_zero_iff:
    1.27    "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
    1.28 -proof -
    1.29 -  have "x * x + y * y \<noteq> 0 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
    1.30 -    by (simp add: sum_squares_eq_zero_iff)
    1.31 -  then have "0 \<noteq> x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
    1.32 -    by auto
    1.33 -  then show ?thesis
    1.34 -    by (simp add: less_le sum_squares_ge_zero)
    1.35 -qed
    1.36 +  by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
    1.37  
    1.38  end
    1.39  
     2.1 --- a/src/HOL/Parity.thy	Sat Mar 06 16:02:22 2010 -0800
     2.2 +++ b/src/HOL/Parity.thy	Sat Mar 06 18:24:30 2010 -0800
     2.3 @@ -218,7 +218,7 @@
     2.4    done
     2.5  
     2.6  lemma zero_le_even_power: "even n ==>
     2.7 -    0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n"
     2.8 +    0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
     2.9    apply (simp add: even_nat_equiv_def2)
    2.10    apply (erule exE)
    2.11    apply (erule ssubst)
     3.1 --- a/src/HOL/Rings.thy	Sat Mar 06 16:02:22 2010 -0800
     3.2 +++ b/src/HOL/Rings.thy	Sat Mar 06 18:24:30 2010 -0800
     3.3 @@ -796,6 +796,13 @@
     3.4       auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
     3.5  qed (auto simp add: abs_if)
     3.6  
     3.7 +lemma zero_le_square [simp]: "0 \<le> a * a"
     3.8 +  using linear [of 0 a]
     3.9 +  by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
    3.10 +
    3.11 +lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
    3.12 +  by (simp add: not_less)
    3.13 +
    3.14  end
    3.15  
    3.16  (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
    3.17 @@ -873,12 +880,6 @@
    3.18    apply force
    3.19    done
    3.20  
    3.21 -lemma zero_le_square [simp]: "0 \<le> a * a"
    3.22 -by (simp add: zero_le_mult_iff linear)
    3.23 -
    3.24 -lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
    3.25 -by (simp add: not_less)
    3.26 -
    3.27  text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
    3.28     also with the relations @{text "\<le>"} and equality.*}
    3.29