--- 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