# HG changeset patch
# User huffman
# Date 1273626418 25200
# Node ID 34dc65df701421fe4cb78aad9087f38f3baa1dbc
# Parent  042c2b3ea2d0cb8f32cb088bce58a42a8073161e
no more RealPow.thy (remaining lemmas moved to RealDef.thy)

diff -r 042c2b3ea2d0 -r 34dc65df7014 src/HOL/IsaMakefile
--- 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 \
diff -r 042c2b3ea2d0 -r 34dc65df7014 src/HOL/RealDef.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"
diff -r 042c2b3ea2d0 -r 34dc65df7014 src/HOL/RealPow.thy
--- 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
diff -r 042c2b3ea2d0 -r 34dc65df7014 src/HOL/RealVector.thy
--- 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 *}