# HG changeset patch
# User huffman
# Date 1266965083 28800
# Node ID f9801fdeb7890e9630f3a8863c3438e238494d26
# Parent  c6331256b087d736b8f3ec15fb0d6d53ea40e626# Parent  cac5a37fb638c0afbec149b4631746bae893a4e2
merged

diff -r cac5a37fb638 -r f9801fdeb789 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Feb 23 17:55:00 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Feb 23 14:44:43 2010 -0800
@@ -1541,7 +1541,7 @@
     hence "real ?num \<noteq> 0" by auto
     have e_nat: "int (nat e) = e" using `0 \<le> e` by auto
     have num_eq: "real ?num = real (- floor_fl x)" using `0 < nat (- m)`
-      unfolding Float_floor real_of_float_minus real_of_float_simp real_of_nat_mult pow2_int[of "nat e", unfolded e_nat] realpow_real_of_nat[symmetric] by auto
+      unfolding Float_floor real_of_float_minus real_of_float_simp real_of_nat_mult pow2_int[of "nat e", unfolded e_nat] real_of_nat_power by auto
     have "0 < - floor_fl x" using `0 < ?num`[unfolded real_of_nat_less_iff[symmetric]] unfolding less_float_def num_eq[symmetric] real_of_float_0 real_of_nat_zero .
     hence "real (floor_fl x) < 0" unfolding less_float_def by auto
 
diff -r cac5a37fb638 -r f9801fdeb789 src/HOL/Import/HOL/prob_extra.imp
--- a/src/HOL/Import/HOL/prob_extra.imp	Tue Feb 23 17:55:00 2010 +0100
+++ b/src/HOL/Import/HOL/prob_extra.imp	Tue Feb 23 14:44:43 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 cac5a37fb638 -r f9801fdeb789 src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Tue Feb 23 17:55:00 2010 +0100
+++ b/src/HOL/Import/HOL/real.imp	Tue Feb 23 14:44:43 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 cac5a37fb638 -r f9801fdeb789 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Feb 23 17:55:00 2010 +0100
+++ b/src/HOL/Library/Float.thy	Tue Feb 23 14:44:43 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 cac5a37fb638 -r f9801fdeb789 src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Tue Feb 23 17:55:00 2010 +0100
+++ b/src/HOL/Probability/Borel.thy	Tue Feb 23 14:44:43 2010 -0800
@@ -82,7 +82,7 @@
     fix w n
     assume le: "f w \<le> g w - inverse(real(Suc n))"
     hence "0 < inverse(real(Suc n))"
-      by (metis inverse_real_of_nat_gt_zero)
+      by simp
     thus "f w < g w" using le
       by arith 
   qed
diff -r cac5a37fb638 -r f9801fdeb789 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Tue Feb 23 17:55:00 2010 +0100
+++ b/src/HOL/Rational.thy	Tue Feb 23 14:44:43 2010 -0800
@@ -6,6 +6,7 @@
 
 theory Rational
 imports GCD Archimedean_Field
+uses ("Tools/float_syntax.ML")
 begin
 
 subsection {* Rational numbers as quotient *}
@@ -1212,4 +1213,15 @@
   plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
   zero_rat_inst.zero_rat
 
+subsection{* Float syntax *}
+
+syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
+
+use "Tools/float_syntax.ML"
+setup Float_Syntax.setup
+
+text{* Test: *}
+lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
+by simp
+
 end
diff -r cac5a37fb638 -r f9801fdeb789 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Tue Feb 23 17:55:00 2010 +0100
+++ b/src/HOL/RealDef.thy	Tue Feb 23 14:44:43 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 cac5a37fb638 -r f9801fdeb789 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue Feb 23 17:55:00 2010 +0100
+++ b/src/HOL/RealPow.thy	Tue Feb 23 14:44:43 2010 -0800
@@ -7,12 +7,13 @@
 
 theory RealPow
 imports RealDef
-uses ("Tools/float_syntax.ML")
 begin
 
+(* FIXME: declare this in Rings.thy or not at all *)
 declare abs_mult_self [simp]
 
-lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
+(* 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"
@@ -31,18 +32,9 @@
 apply (simp split add: nat_diff_split)
 done
 
-lemma realpow_two_mult_inverse [simp]:
-     "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
-by (simp add:  real_mult_assoc [symmetric])
-
-lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
-by simp
-
 lemma realpow_two_diff:
      "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
-apply (unfold real_diff_def)
-apply (simp add: algebra_simps)
-done
+by (simp add: algebra_simps)
 
 lemma realpow_two_disj:
      "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
@@ -50,36 +42,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)
-done
-
-(* used by AFP Integration theory *)
-lemma realpow_increasing:
-     "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y"
-  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 *}
 
@@ -93,9 +55,6 @@
 lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
 by simp
 
-lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y"
-by (rule sum_squares_ge_zero)
-
 lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
 by (simp add: real_add_eq_0_iff [symmetric])
 
@@ -172,24 +131,7 @@
 apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
 done
 
-lemma inverse_real_of_nat_gt_zero [simp]: "0 < inverse (real (Suc n))"
-by simp
-
-lemma inverse_real_of_nat_ge_zero [simp]: "0 \<le> inverse (real (Suc n))"
-by simp
-
 lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
 by (case_tac "n", auto)
 
-subsection{* Float syntax *}
-
-syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
-
-use "Tools/float_syntax.ML"
-setup Float_Syntax.setup
-
-text{* Test: *}
-lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::real)"
-by simp
-
 end
diff -r cac5a37fb638 -r f9801fdeb789 src/HOL/ex/HarmonicSeries.thy
--- a/src/HOL/ex/HarmonicSeries.thy	Tue Feb 23 17:55:00 2010 +0100
+++ b/src/HOL/ex/HarmonicSeries.thy	Tue Feb 23 14:44:43 2010 -0800
@@ -73,7 +73,8 @@
       qed
       moreover from xs have "x \<le> 2^m" by auto
       ultimately have
-        "inverse (real x) \<ge> inverse (real ((2::nat)^m))" by simp
+        "inverse (real x) \<ge> inverse (real ((2::nat)^m))"
+        by (simp del: real_of_nat_power)
       moreover
       from xgt0 have "real x \<noteq> 0" by simp
       then have
@@ -107,7 +108,7 @@
         by (auto simp: tmdef dest: two_pow_sub)
       also have
         "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^m"
-        by (simp add: tmdef realpow_real_of_nat [symmetric])
+        by (simp add: tmdef)
       also from mgt0 have
         "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^((m - 1) + 1)"
         by auto
@@ -319,4 +320,4 @@
   ultimately show False by simp
 qed
 
-end
\ No newline at end of file
+end