moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
authorhuffman
Tue Feb 23 10:37:25 2010 -0800 (2010-02-23)
changeset 35344e0b46cd72414
parent 35343 523124691b3a
child 35345 04d01ad97267
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
src/HOL/Import/HOL/prob_extra.imp
src/HOL/Import/HOL/real.imp
src/HOL/Library/Float.thy
src/HOL/RealDef.thy
src/HOL/RealPow.thy
     1.1 --- a/src/HOL/Import/HOL/prob_extra.imp	Tue Feb 23 07:45:54 2010 -0800
     1.2 +++ b/src/HOL/Import/HOL/prob_extra.imp	Tue Feb 23 10:37:25 2010 -0800
     1.3 @@ -22,7 +22,7 @@
     1.4    "REAL_SUP_MAX" > "HOL4Prob.prob_extra.REAL_SUP_MAX"
     1.5    "REAL_SUP_LE_X" > "HOL4Prob.prob_extra.REAL_SUP_LE_X"
     1.6    "REAL_SUP_EXISTS_UNIQUE" > "HOL4Prob.prob_extra.REAL_SUP_EXISTS_UNIQUE"
     1.7 -  "REAL_POW" > "RealPow.realpow_real_of_nat"
     1.8 +  "REAL_POW" > "RealDef.power_real_of_nat"
     1.9    "REAL_LE_INV_LE" > "Rings.le_imp_inverse_le"
    1.10    "REAL_LE_EQ" > "Set.basic_trans_rules_26"
    1.11    "REAL_INVINV_ALL" > "Rings.inverse_inverse_eq"
     2.1 --- a/src/HOL/Import/HOL/real.imp	Tue Feb 23 07:45:54 2010 -0800
     2.2 +++ b/src/HOL/Import/HOL/real.imp	Tue Feb 23 10:37:25 2010 -0800
     2.3 @@ -105,7 +105,7 @@
     2.4    "REAL_POASQ" > "HOL4Real.real.REAL_POASQ"
     2.5    "REAL_OVER1" > "Rings.divide_1"
     2.6    "REAL_OF_NUM_SUC" > "RealDef.real_of_nat_Suc"
     2.7 -  "REAL_OF_NUM_POW" > "RealPow.realpow_real_of_nat"
     2.8 +  "REAL_OF_NUM_POW" > "RealDef.power_real_of_nat"
     2.9    "REAL_OF_NUM_MUL" > "RealDef.real_of_nat_mult"
    2.10    "REAL_OF_NUM_LE" > "RealDef.real_of_nat_le_iff"
    2.11    "REAL_OF_NUM_EQ" > "RealDef.real_of_nat_inject"
     3.1 --- a/src/HOL/Library/Float.thy	Tue Feb 23 07:45:54 2010 -0800
     3.2 +++ b/src/HOL/Library/Float.thy	Tue Feb 23 10:37:25 2010 -0800
     3.3 @@ -789,12 +789,12 @@
     3.4      hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto
     3.5  
     3.6      from real_of_int_div4[of "?X" y]
     3.7 -    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 .
     3.8 +    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 .
     3.9      also have "\<dots> < 1 * 2^?l" using `real x / real y < 1` by (rule mult_strict_right_mono, auto)
    3.10      finally have "?X div y < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
    3.11      hence "?X div y + 1 \<le> 2^?l" by auto
    3.12      hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)"
    3.13 -      unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of
    3.14 +      unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
    3.15        by (rule mult_right_mono, auto)
    3.16      hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto
    3.17      thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
    3.18 @@ -863,12 +863,12 @@
    3.19      qed
    3.20  
    3.21      from real_of_int_div4[of "?X" y]
    3.22 -    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 .
    3.23 +    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 .
    3.24      also have "\<dots> < 1/2 * 2^?l" using `real x / real y < 1/2` by (rule mult_strict_right_mono, auto)
    3.25      finally have "?X div y * 2 < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
    3.26      hence "?X div y + 1 < 2^?l" using `0 < ?X div y` by auto
    3.27      hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)"
    3.28 -      unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of
    3.29 +      unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
    3.30        by (rule mult_strict_right_mono, auto)
    3.31      hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto
    3.32      thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
    3.33 @@ -1188,7 +1188,7 @@
    3.34    show "?thesis"
    3.35    proof (cases "0 < ?d")
    3.36      case True
    3.37 -    hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto
    3.38 +    hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
    3.39      show ?thesis
    3.40      proof (cases "m mod ?p = 0")
    3.41        case True
    3.42 @@ -1224,7 +1224,7 @@
    3.43    show "?thesis"
    3.44    proof (cases "0 < ?d")
    3.45      case True
    3.46 -    hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto
    3.47 +    hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
    3.48      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])
    3.49      also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
    3.50      finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e]
    3.51 @@ -1263,7 +1263,7 @@
    3.52      case True
    3.53      have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m"
    3.54      proof -
    3.55 -      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] 
    3.56 +      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] 
    3.57          using `?l > 0` by auto
    3.58        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
    3.59        also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
    3.60 @@ -1329,7 +1329,7 @@
    3.61      hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
    3.62      have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto
    3.63      also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
    3.64 -    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
    3.65 +    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
    3.66      also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
    3.67      finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
    3.68    next
    3.69 @@ -1357,7 +1357,7 @@
    3.70      case False
    3.71      hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
    3.72      have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
    3.73 -    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
    3.74 +    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
    3.75      also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
    3.76      also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto
    3.77      finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
     4.1 --- a/src/HOL/RealDef.thy	Tue Feb 23 07:45:54 2010 -0800
     4.2 +++ b/src/HOL/RealDef.thy	Tue Feb 23 10:37:25 2010 -0800
     4.3 @@ -584,6 +584,11 @@
     4.4  lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
     4.5  by (simp add: real_of_int_def) 
     4.6  
     4.7 +lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n"
     4.8 +by (simp add: real_of_int_def of_int_power)
     4.9 +
    4.10 +lemmas power_real_of_int = real_of_int_power [symmetric]
    4.11 +
    4.12  lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))"
    4.13    apply (subst real_eq_of_int)+
    4.14    apply (rule of_int_setsum)
    4.15 @@ -731,6 +736,11 @@
    4.16  lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
    4.17  by (simp add: real_of_nat_def of_nat_mult)
    4.18  
    4.19 +lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n"
    4.20 +by (simp add: real_of_nat_def of_nat_power)
    4.21 +
    4.22 +lemmas power_real_of_nat = real_of_nat_power [symmetric]
    4.23 +
    4.24  lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 
    4.25      (SUM x:A. real(f x))"
    4.26    apply (subst real_eq_of_nat)+
     5.1 --- a/src/HOL/RealPow.thy	Tue Feb 23 07:45:54 2010 -0800
     5.2 +++ b/src/HOL/RealPow.thy	Tue Feb 23 10:37:25 2010 -0800
     5.3 @@ -49,11 +49,6 @@
     5.4  apply auto
     5.5  done
     5.6  
     5.7 -lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
     5.8 -apply (induct "n")
     5.9 -apply (auto simp add: real_of_nat_one real_of_nat_mult)
    5.10 -done
    5.11 -
    5.12  lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
    5.13  apply (induct "n")
    5.14  apply (auto simp add: zero_less_mult_iff)
    5.15 @@ -65,21 +60,6 @@
    5.16    by (rule power_le_imp_le_base)
    5.17  
    5.18  
    5.19 -subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
    5.20 -
    5.21 -lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
    5.22 -apply (induct "n")
    5.23 -apply (simp_all add: nat_mult_distrib)
    5.24 -done
    5.25 -declare real_of_int_power [symmetric, simp]
    5.26 -
    5.27 -lemma power_real_number_of:
    5.28 -     "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
    5.29 -by (simp only: real_number_of [symmetric] real_of_int_power)
    5.30 -
    5.31 -declare power_real_number_of [of _ "number_of w", standard, simp]
    5.32 -
    5.33 -
    5.34  subsection{* Squares of Reals *}
    5.35  
    5.36  lemma real_two_squares_add_zero_iff [simp]: