# HG changeset patch
# User huffman
# Date 1266950245 28800
# Node ID e0b46cd724143fce44a2902fb33bf0c89f7e6164
# Parent  523124691b3a08d1fd5a862a67d1fc00e4303410
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power

diff -r 523124691b3a -r e0b46cd72414 src/HOL/Import/HOL/prob_extra.imp
--- a/src/HOL/Import/HOL/prob_extra.imp	Tue Feb 23 07:45:54 2010 -0800
+++ b/src/HOL/Import/HOL/prob_extra.imp	Tue Feb 23 10:37:25 2010 -0800
@@ -22,7 +22,7 @@
   "REAL_SUP_MAX" > "HOL4Prob.prob_extra.REAL_SUP_MAX"
   "REAL_SUP_LE_X" > "HOL4Prob.prob_extra.REAL_SUP_LE_X"
   "REAL_SUP_EXISTS_UNIQUE" > "HOL4Prob.prob_extra.REAL_SUP_EXISTS_UNIQUE"
-  "REAL_POW" > "RealPow.realpow_real_of_nat"
+  "REAL_POW" > "RealDef.power_real_of_nat"
   "REAL_LE_INV_LE" > "Rings.le_imp_inverse_le"
   "REAL_LE_EQ" > "Set.basic_trans_rules_26"
   "REAL_INVINV_ALL" > "Rings.inverse_inverse_eq"
diff -r 523124691b3a -r e0b46cd72414 src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Tue Feb 23 07:45:54 2010 -0800
+++ b/src/HOL/Import/HOL/real.imp	Tue Feb 23 10:37:25 2010 -0800
@@ -105,7 +105,7 @@
   "REAL_POASQ" > "HOL4Real.real.REAL_POASQ"
   "REAL_OVER1" > "Rings.divide_1"
   "REAL_OF_NUM_SUC" > "RealDef.real_of_nat_Suc"
-  "REAL_OF_NUM_POW" > "RealPow.realpow_real_of_nat"
+  "REAL_OF_NUM_POW" > "RealDef.power_real_of_nat"
   "REAL_OF_NUM_MUL" > "RealDef.real_of_nat_mult"
   "REAL_OF_NUM_LE" > "RealDef.real_of_nat_le_iff"
   "REAL_OF_NUM_EQ" > "RealDef.real_of_nat_inject"
diff -r 523124691b3a -r e0b46cd72414 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Feb 23 07:45:54 2010 -0800
+++ b/src/HOL/Library/Float.thy	Tue Feb 23 10:37:25 2010 -0800
@@ -789,12 +789,12 @@
     hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto
 
     from real_of_int_div4[of "?X" y]
-    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power[symmetric] real_number_of .
+    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
     also have "\<dots> < 1 * 2^?l" using `real x / real y < 1` by (rule mult_strict_right_mono, auto)
     finally have "?X div y < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
     hence "?X div y + 1 \<le> 2^?l" by auto
     hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)"
-      unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of
+      unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
       by (rule mult_right_mono, auto)
     hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto
     thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
@@ -863,12 +863,12 @@
     qed
 
     from real_of_int_div4[of "?X" y]
-    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power[symmetric] real_number_of .
+    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
     also have "\<dots> < 1/2 * 2^?l" using `real x / real y < 1/2` by (rule mult_strict_right_mono, auto)
     finally have "?X div y * 2 < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
     hence "?X div y + 1 < 2^?l" using `0 < ?X div y` by auto
     hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)"
-      unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of
+      unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
       by (rule mult_strict_right_mono, auto)
     hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto
     thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
@@ -1188,7 +1188,7 @@
   show "?thesis"
   proof (cases "0 < ?d")
     case True
-    hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto
+    hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
     show ?thesis
     proof (cases "m mod ?p = 0")
       case True
@@ -1224,7 +1224,7 @@
   show "?thesis"
   proof (cases "0 < ?d")
     case True
-    hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto
+    hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
     have "m div ?p * ?p \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
     also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
     finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e]
@@ -1263,7 +1263,7 @@
     case True
     have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m"
     proof -
-      have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power[symmetric] real_number_of unfolding pow2_int[symmetric] 
+      have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power real_number_of unfolding pow2_int[symmetric] 
         using `?l > 0` by auto
       also have "\<dots> \<le> real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding real_of_int_add by auto
       also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
@@ -1329,7 +1329,7 @@
     hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
     have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto
     also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
-    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
+    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
     also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
     finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
   next
@@ -1357,7 +1357,7 @@
     case False
     hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
     have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
-    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
+    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
     also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
     also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto
     finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
diff -r 523124691b3a -r e0b46cd72414 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Tue Feb 23 07:45:54 2010 -0800
+++ b/src/HOL/RealDef.thy	Tue Feb 23 10:37:25 2010 -0800
@@ -584,6 +584,11 @@
 lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
 by (simp add: real_of_int_def) 
 
+lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n"
+by (simp add: real_of_int_def of_int_power)
+
+lemmas power_real_of_int = real_of_int_power [symmetric]
+
 lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))"
   apply (subst real_eq_of_int)+
   apply (rule of_int_setsum)
@@ -731,6 +736,11 @@
 lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
 by (simp add: real_of_nat_def of_nat_mult)
 
+lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n"
+by (simp add: real_of_nat_def of_nat_power)
+
+lemmas power_real_of_nat = real_of_nat_power [symmetric]
+
 lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 
     (SUM x:A. real(f x))"
   apply (subst real_eq_of_nat)+
diff -r 523124691b3a -r e0b46cd72414 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue Feb 23 07:45:54 2010 -0800
+++ b/src/HOL/RealPow.thy	Tue Feb 23 10:37:25 2010 -0800
@@ -49,11 +49,6 @@
 apply auto
 done
 
-lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
-apply (induct "n")
-apply (auto simp add: real_of_nat_one real_of_nat_mult)
-done
-
 lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
 apply (induct "n")
 apply (auto simp add: zero_less_mult_iff)
@@ -65,21 +60,6 @@
   by (rule power_le_imp_le_base)
 
 
-subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
-
-lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
-apply (induct "n")
-apply (simp_all add: nat_mult_distrib)
-done
-declare real_of_int_power [symmetric, simp]
-
-lemma power_real_number_of:
-     "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
-by (simp only: real_number_of [symmetric] real_of_int_power)
-
-declare power_real_number_of [of _ "number_of w", standard, simp]
-
-
 subsection{* Squares of Reals *}
 
 lemma real_two_squares_add_zero_iff [simp]: