--- 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
--- 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"
--- 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"
--- 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`] .
--- 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
--- 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
--- 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)+
--- 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
--- 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