# HG changeset patch
# User huffman
# Date 1234666891 28800
# Node ID 2146e512cec98e10cf19585d62aa9158a7e35cf3
# Parent  c9ced4f54e820fe889ebabbb0a6788f72eb43bc9
generalize lemma fps_square_eq_iff, move to Ring_and_Field

diff -r c9ced4f54e82 -r 2146e512cec9 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 16:51:18 2009 -0800
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 19:01:31 2009 -0800
@@ -691,17 +691,6 @@
   by (simp_all add: fps_power_def)
 end
 
-lemma fps_square_eq_iff: "(a:: 'a::idom fps)^ 2 = b^2  \<longleftrightarrow> (a = b \<or> a = -b)"
-proof-
-  {assume "a = b \<or> a = -b" hence "a^2 = b^2" by auto}
-  moreover
-  {assume "a^2 = b^2 "
-    hence "a^2 - b^2 = 0" by simp
-    hence "(a-b) * (a+b) = 0" by (simp add: power2_eq_square ring_simps)
-    hence "a = b \<or> a = -b" by (simp add: eq_neg_iff_add_eq_0)}
-  ultimately show ?thesis by blast
-qed
-
 lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
   by (induct n, auto simp add: fps_power_def expand_fps_eq fps_mult_nth)
 
diff -r c9ced4f54e82 -r 2146e512cec9 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Sat Feb 14 16:51:18 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Sat Feb 14 19:01:31 2009 -0800
@@ -374,6 +374,18 @@
 
 subclass ring_1_no_zero_divisors ..
 
+lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
+proof
+  assume "a * a = b * b"
+  then have "(a - b) * (a + b) = 0"
+    by (simp add: algebra_simps)
+  then show "a = b \<or> a = - b"
+    by (simp add: right_minus_eq eq_neg_iff_add_eq_0)
+next
+  assume "a = b \<or> a = - b"
+  then show "a * a = b * b" by auto
+qed
+
 end
 
 class division_ring = ring_1 + inverse +