--- a/src/HOL/IsaMakefile Tue May 11 17:20:11 2010 -0700
+++ b/src/HOL/IsaMakefile Tue May 11 18:06:58 2010 -0700
@@ -357,7 +357,6 @@
Rat.thy \
Real.thy \
RealDef.thy \
- RealPow.thy \
RealVector.thy \
SEQ.thy \
Series.thy \
--- a/src/HOL/RealDef.thy Tue May 11 17:20:11 2010 -0700
+++ b/src/HOL/RealDef.thy Tue May 11 18:06:58 2010 -0700
@@ -1539,6 +1539,7 @@
lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
by arith
+text {* FIXME: redundant with @{text add_eq_0_iff} below *}
lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)"
by auto
@@ -1554,8 +1555,86 @@
lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (-x \<le> y)"
by auto
+subsection {* Lemmas about powers *}
-subsubsection{*Density of the Reals*}
+text {* FIXME: declare this in Rings.thy or not at all *}
+declare abs_mult_self [simp]
+
+(* used by Import/HOL/real.imp *)
+lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
+by simp
+
+lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
+apply (induct "n")
+apply (auto simp add: real_of_nat_Suc)
+apply (subst mult_2)
+apply (erule add_less_le_mono)
+apply (rule two_realpow_ge_one)
+done
+
+text {* 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)
+
+text {* 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)
+
+text {* TODO: no longer real-specific; rename and move elsewhere *}
+lemma realpow_two_diff:
+ fixes x :: "'a::comm_ring_1"
+ shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
+by (simp add: algebra_simps)
+
+text {* 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)
+
+text {* TODO: no longer real-specific; rename and move elsewhere *}
+lemma realpow_two_disj:
+ 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)
+
+text {* 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)
+
+text {* 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)
+
+text {* 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)
+
+text {* 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)
+
+text {* 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_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
+by (rule_tac y = 0 in order_trans, auto)
+
+lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
+by (auto simp add: power2_eq_square)
+
+
+subsection{*Density of the Reals*}
lemma real_lbound_gt_zero:
"[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
--- a/src/HOL/RealPow.thy Tue May 11 17:20:11 2010 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(* Title : HOL/RealPow.thy
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
-*)
-
-header {* Natural powers theory *}
-
-theory RealPow
-imports RealDef RComplete
-begin
-
-(* FIXME: declare this in Rings.thy or not at all *)
-declare abs_mult_self [simp]
-
-(* used by Import/HOL/real.imp *)
-lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
-by simp
-
-lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
-apply (induct "n")
-apply (auto simp add: real_of_nat_Suc)
-apply (subst mult_2)
-apply (erule add_less_le_mono)
-apply (rule two_realpow_ge_one)
-done
-
-(* 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)
-
-(* 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:
- 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:
- 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)
-
-(* 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)
-
-(* 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_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
-by (rule_tac y = 0 in order_trans, auto)
-
-lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
-by (auto simp add: power2_eq_square)
-
-end
--- a/src/HOL/RealVector.thy Tue May 11 17:20:11 2010 -0700
+++ b/src/HOL/RealVector.thy Tue May 11 18:06:58 2010 -0700
@@ -5,7 +5,7 @@
header {* Vector Spaces and Algebras over the Reals *}
theory RealVector
-imports RealPow
+imports RComplete
begin
subsection {* Locale for additive functions *}