# HG changeset patch
# User huffman
# Date 1267975774 28800
# Node ID 61fd75e33137df7c5acb124cd660f448bb891269
# Parent  0b8a5fd339ab3e7c64081d1290afb7c02621dcf2
generalize some lemmas, and remove a few unnecessary ones

diff -r 0b8a5fd339ab -r 61fd75e33137 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Sat Mar 06 18:24:30 2010 -0800
+++ b/src/HOL/RealPow.thy	Sun Mar 07 07:29:34 2010 -0800
@@ -24,71 +24,76 @@
 apply (rule two_realpow_ge_one)
 done
 
-lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma realpow_Suc_le_self:
+  fixes r :: "'a::linordered_semidom"
+  shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r"
 by (insert power_decreasing [of 1 "Suc n" r], simp)
 
-lemma realpow_minus_mult [rule_format]:
-     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
-apply (simp split add: nat_diff_split)
-done
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma realpow_minus_mult:
+  fixes x :: "'a::monoid_mult"
+  shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
+by (simp add: power_commutes split add: nat_diff_split)
 
+(* TODO: no longer real-specific; rename and move elsewhere *)
 lemma realpow_two_diff:
-     "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
+  fixes x :: "'a::comm_ring_1"
+  shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
 by (simp add: algebra_simps)
 
+(* TODO: move elsewhere *)
+lemma add_eq_0_iff:
+  fixes x y :: "'a::group_add"
+  shows "x + y = 0 \<longleftrightarrow> y = - x"
+by (auto dest: minus_unique)
+
+(* TODO: no longer real-specific; rename and move elsewhere *)
 lemma realpow_two_disj:
-     "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
-apply (cut_tac x = x and y = y in realpow_two_diff)
-apply auto
-done
+  fixes x :: "'a::idom"
+  shows "(x^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
+using realpow_two_diff [of x y]
+by (auto simp add: add_eq_0_iff)
 
 
 subsection{* Squares of Reals *}
 
+(* FIXME: declare this [simp] for all types, or not at all *)
 lemma real_two_squares_add_zero_iff [simp]:
   "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
 by (rule sum_squares_eq_zero_iff)
 
-lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
-by simp
-
-lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
-by simp
-
-lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
-by (simp add: real_add_eq_0_iff [symmetric])
-
-lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
-by (simp add: left_distrib right_diff_distrib)
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma real_squared_diff_one_factored:
+  fixes x :: "'a::ring_1"
+  shows "x * x - 1 = (x + 1) * (x - 1)"
+by (simp add: algebra_simps)
 
-lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)"
-apply auto
-apply (drule right_minus_eq [THEN iffD2]) 
-apply (auto simp add: real_squared_diff_one_factored)
-done
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma real_mult_is_one [simp]:
+  fixes x :: "'a::ring_1_no_zero_divisors"
+  shows "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
+proof -
+  have "x * x = 1 \<longleftrightarrow> (x + 1) * (x - 1) = 0"
+    by (simp add: algebra_simps)
+  also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1"
+    by (auto simp add: add_eq_0_iff minus_equation_iff [of _ 1])
+  finally show ?thesis .
+qed
 
-lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
-by simp
-
-lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
-by simp
-
+(* FIXME: declare this [simp] for all types, or not at all *)
 lemma realpow_two_sum_zero_iff [simp]:
      "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
 by (rule sum_power2_eq_zero_iff)
 
+(* FIXME: declare this [simp] for all types, or not at all *)
 lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
 by (rule sum_power2_ge_zero)
 
+(* FIXME: declare this [simp] for all types, or not at all *)
 lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
 by (intro add_nonneg_nonneg zero_le_power2)
 
-lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
-by (simp add: sum_squares_gt_zero_iff)
-
-lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
-by (simp add: sum_squares_gt_zero_iff)
-
 lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
 by (rule_tac j = 0 in real_le_trans, auto)
 
@@ -96,8 +101,9 @@
 by (auto simp add: power2_eq_square)
 
 (* The following theorem is by Benjamin Porter *)
+(* TODO: no longer real-specific; rename and move elsewhere *)
 lemma real_sq_order:
-  fixes x::real
+  fixes x :: "'a::linordered_semidom"
   assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
   shows "x \<le> y"
 proof -
@@ -150,8 +156,11 @@
 apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
 done
 
-lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
-by (case_tac "n", auto)
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma realpow_num_eq_if:
+  fixes m :: "'a::power"
+  shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
+by (cases n, auto)
 
 
 end