# HG changeset patch
# User huffman
# Date 1273594231 25200
# Node ID 4d4462d644aec537e459295667957da0ab4837ae
# Parent  d9320cdcde73a607a84bacb208a729bf93f1c5cd
move floor lemmas from RealPow.thy to RComplete.thy

diff -r d9320cdcde73 -r 4d4462d644ae src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Tue May 11 07:58:48 2010 -0700
+++ b/src/HOL/RComplete.thy	Tue May 11 09:10:31 2010 -0700
@@ -837,5 +837,27 @@
   apply simp
 done
 
+subsection {* Exponentiation with floor *}
+
+lemma floor_power:
+  assumes "x = real (floor x)"
+  shows "floor (x ^ n) = floor x ^ n"
+proof -
+  have *: "x ^ n = real (floor x ^ n)"
+    using assms by (induct n arbitrary: x) simp_all
+  show ?thesis unfolding real_of_int_inject[symmetric]
+    unfolding * floor_real_of_int ..
+qed
+
+lemma natfloor_power:
+  assumes "x = real (natfloor x)"
+  shows "natfloor (x ^ n) = natfloor x ^ n"
+proof -
+  from assms have "0 \<le> floor x" by auto
+  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
+  from floor_power[OF this]
+  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
+    by simp
+qed
 
 end
diff -r d9320cdcde73 -r 4d4462d644ae src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue May 11 07:58:48 2010 -0700
+++ b/src/HOL/RealPow.thy	Tue May 11 09:10:31 2010 -0700
@@ -101,27 +101,4 @@
     by (rule power_le_imp_le_base)
 qed
 
-subsection {*Floor*}
-
-lemma floor_power:
-  assumes "x = real (floor x)"
-  shows "floor (x ^ n) = floor x ^ n"
-proof -
-  have *: "x ^ n = real (floor x ^ n)"
-    using assms by (induct n arbitrary: x) simp_all
-  show ?thesis unfolding real_of_int_inject[symmetric]
-    unfolding * floor_real_of_int ..
-qed
-
-lemma natfloor_power:
-  assumes "x = real (natfloor x)"
-  shows "natfloor (x ^ n) = natfloor x ^ n"
-proof -
-  from assms have "0 \<le> floor x" by auto
-  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
-  from floor_power[OF this]
-  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
-    by simp
-qed
-
 end