# HG changeset patch
# User huffman
# Date 1267928670 28800
# Node ID 0b8a5fd339ab3e7c64081d1290afb7c02621dcf2
# Parent  8e562d56d404597ce7e030842ef267acd004424b
generalize some lemmas from class linordered_ring_strict to linordered_ring

diff -r 8e562d56d404 -r 0b8a5fd339ab src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Sat Mar 06 16:02:22 2010 -0800
+++ b/src/HOL/Nat_Numeral.thy	Sat Mar 06 18:24:30 2010 -0800
@@ -113,7 +113,7 @@
 
 end
 
-context linordered_ring_strict
+context linordered_ring
 begin
 
 lemma sum_squares_ge_zero:
@@ -124,6 +124,11 @@
   "\<not> x * x + y * y < 0"
   by (simp add: not_less sum_squares_ge_zero)
 
+end
+
+context linordered_ring_strict
+begin
+
 lemma sum_squares_eq_zero_iff:
   "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   by (simp add: add_nonneg_eq_0_iff)
@@ -134,14 +139,7 @@
 
 lemma sum_squares_gt_zero_iff:
   "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
-proof -
-  have "x * x + y * y \<noteq> 0 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
-    by (simp add: sum_squares_eq_zero_iff)
-  then have "0 \<noteq> x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
-    by auto
-  then show ?thesis
-    by (simp add: less_le sum_squares_ge_zero)
-qed
+  by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
 
 end
 
diff -r 8e562d56d404 -r 0b8a5fd339ab src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Mar 06 16:02:22 2010 -0800
+++ b/src/HOL/Parity.thy	Sat Mar 06 18:24:30 2010 -0800
@@ -218,7 +218,7 @@
   done
 
 lemma zero_le_even_power: "even n ==>
-    0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n"
+    0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
   apply (simp add: even_nat_equiv_def2)
   apply (erule exE)
   apply (erule ssubst)
diff -r 8e562d56d404 -r 0b8a5fd339ab src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Mar 06 16:02:22 2010 -0800
+++ b/src/HOL/Rings.thy	Sat Mar 06 18:24:30 2010 -0800
@@ -796,6 +796,13 @@
      auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
 qed (auto simp add: abs_if)
 
+lemma zero_le_square [simp]: "0 \<le> a * a"
+  using linear [of 0 a]
+  by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
+
+lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
+  by (simp add: not_less)
+
 end
 
 (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
@@ -873,12 +880,6 @@
   apply force
   done
 
-lemma zero_le_square [simp]: "0 \<le> a * a"
-by (simp add: zero_le_mult_iff linear)
-
-lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
-by (simp add: not_less)
-
 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
    also with the relations @{text "\<le>"} and equality.*}