1.1 --- a/src/HOL/Decision_Procs/Approximation.thy Fri Apr 17 16:41:31 2009 +0200
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Mon Apr 20 09:32:07 2009 +0200
1.3 @@ -23,8 +23,8 @@
1.4 qed
1.5
1.6 lemma horner_schema: fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
1.7 - assumes f_Suc: "\<And>n. f (Suc n) = G ((F^n) s) (f n)"
1.8 - shows "horner F G n ((F^j') s) (f j') x = (\<Sum> j = 0..< n. -1^j * (1 / real (f (j' + j))) * x^j)"
1.9 + assumes f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
1.10 + shows "horner F G n ((F o^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / real (f (j' + j))) * x ^ j)"
1.11 proof (induct n arbitrary: i k j')
1.12 case (Suc n)
1.13
1.14 @@ -33,13 +33,13 @@
1.15 qed auto
1.16
1.17 lemma horner_bounds':
1.18 - assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F^n) s) (f n)"
1.19 + assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
1.20 and lb_0: "\<And> i k x. lb 0 i k x = 0"
1.21 and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) - x * (ub n (F i) (G i k) x)"
1.22 and ub_0: "\<And> i k x. ub 0 i k x = 0"
1.23 and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) - x * (lb n (F i) (G i k) x)"
1.24 - shows "Ifloat (lb n ((F^j') s) (f j') x) \<le> horner F G n ((F^j') s) (f j') (Ifloat x) \<and>
1.25 - horner F G n ((F^j') s) (f j') (Ifloat x) \<le> Ifloat (ub n ((F^j') s) (f j') x)"
1.26 + shows "Ifloat (lb n ((F o^ j') s) (f j') x) \<le> horner F G n ((F o^ j') s) (f j') (Ifloat x) \<and>
1.27 + horner F G n ((F o^ j') s) (f j') (Ifloat x) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)"
1.28 (is "?lb n j' \<le> ?horner n j' \<and> ?horner n j' \<le> ?ub n j'")
1.29 proof (induct n arbitrary: j')
1.30 case 0 thus ?case unfolding lb_0 ub_0 horner.simps by auto
1.31 @@ -49,15 +49,15 @@
1.32 proof (rule add_mono)
1.33 show "Ifloat (lapprox_rat prec 1 (int (f j'))) \<le> 1 / real (f j')" using lapprox_rat[of prec 1 "int (f j')"] by auto
1.34 from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct2] `0 \<le> Ifloat x`
1.35 - show "- Ifloat (x * ub n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) x) \<le> - (Ifloat x * horner F G n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) (Ifloat x))"
1.36 + show "- Ifloat (x * ub n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) x) \<le> - (Ifloat x * horner F G n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) (Ifloat x))"
1.37 unfolding Ifloat_mult neg_le_iff_le by (rule mult_left_mono)
1.38 qed
1.39 moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps Ifloat_sub diff_def
1.40 proof (rule add_mono)
1.41 show "1 / real (f j') \<le> Ifloat (rapprox_rat prec 1 (int (f j')))" using rapprox_rat[of 1 "int (f j')" prec] by auto
1.42 from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct1] `0 \<le> Ifloat x`
1.43 - show "- (Ifloat x * horner F G n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) (Ifloat x)) \<le>
1.44 - - Ifloat (x * lb n (F ((F ^ j') s)) (G ((F ^ j') s) (f j')) x)"
1.45 + show "- (Ifloat x * horner F G n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) (Ifloat x)) \<le>
1.46 + - Ifloat (x * lb n (F ((F o^ j') s)) (G ((F o^ j') s) (f j')) x)"
1.47 unfolding Ifloat_mult neg_le_iff_le by (rule mult_left_mono)
1.48 qed
1.49 ultimately show ?case by blast
1.50 @@ -73,13 +73,13 @@
1.51 *}
1.52
1.53 lemma horner_bounds: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.54 - assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F^n) s) (f n)"
1.55 + assumes "0 \<le> Ifloat x" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
1.56 and lb_0: "\<And> i k x. lb 0 i k x = 0"
1.57 and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) - x * (ub n (F i) (G i k) x)"
1.58 and ub_0: "\<And> i k x. ub 0 i k x = 0"
1.59 and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) - x * (lb n (F i) (G i k) x)"
1.60 - shows "Ifloat (lb n ((F^j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1^j * (1 / real (f (j' + j))) * (Ifloat x)^j)" (is "?lb") and
1.61 - "(\<Sum>j=0..<n. -1^j * (1 / real (f (j' + j))) * (Ifloat x)^j) \<le> Ifloat (ub n ((F^j') s) (f j') x)" (is "?ub")
1.62 + shows "Ifloat (lb n ((F o^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * Ifloat x ^ j)" (is "?lb") and
1.63 + "(\<Sum>j=0..<n. -1 ^ j * (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)" (is "?ub")
1.64 proof -
1.65 have "?lb \<and> ?ub"
1.66 using horner_bounds'[where lb=lb, OF `0 \<le> Ifloat x` f_Suc lb_0 lb_Suc ub_0 ub_Suc]
1.67 @@ -88,13 +88,13 @@
1.68 qed
1.69
1.70 lemma horner_bounds_nonpos: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.71 - assumes "Ifloat x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F^n) s) (f n)"
1.72 + assumes "Ifloat x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F o^ n) s) (f n)"
1.73 and lb_0: "\<And> i k x. lb 0 i k x = 0"
1.74 and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 (int k) + x * (ub n (F i) (G i k) x)"
1.75 and ub_0: "\<And> i k x. ub 0 i k x = 0"
1.76 and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 (int k) + x * (lb n (F i) (G i k) x)"
1.77 - shows "Ifloat (lb n ((F^j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x)^j)" (is "?lb") and
1.78 - "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x)^j) \<le> Ifloat (ub n ((F^j') s) (f j') x)" (is "?ub")
1.79 + shows "Ifloat (lb n ((F o^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / real (f (j' + j))) * Ifloat x ^ j)" (is "?lb") and
1.80 + "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)" (is "?ub")
1.81 proof -
1.82 { fix x y z :: float have "x - y * z = x + - y * z"
1.83 by (cases x, cases y, cases z, simp add: plus_float.simps minus_float.simps uminus_float.simps times_float.simps algebra_simps)
1.84 @@ -104,13 +104,13 @@
1.85
1.86 have move_minus: "Ifloat (-x) = -1 * Ifloat x" by auto
1.87
1.88 - have sum_eq: "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x)^j) =
1.89 + have sum_eq: "(\<Sum>j=0..<n. (1 / real (f (j' + j))) * Ifloat x ^ j) =
1.90 (\<Sum>j = 0..<n. -1 ^ j * (1 / real (f (j' + j))) * Ifloat (- x) ^ j)"
1.91 proof (rule setsum_cong, simp)
1.92 fix j assume "j \<in> {0 ..< n}"
1.93 show "1 / real (f (j' + j)) * Ifloat x ^ j = -1 ^ j * (1 / real (f (j' + j))) * Ifloat (- x) ^ j"
1.94 unfolding move_minus power_mult_distrib real_mult_assoc[symmetric]
1.95 - unfolding real_mult_commute unfolding real_mult_assoc[of "-1^j", symmetric] power_mult_distrib[symmetric]
1.96 + unfolding real_mult_commute unfolding real_mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric]
1.97 by auto
1.98 qed
1.99
1.100 @@ -160,21 +160,21 @@
1.101 else (0, (max (-l) u) ^ n))"
1.102
1.103 lemma float_power_bnds: assumes "(l1, u1) = float_power_bnds n l u" and "x \<in> {Ifloat l .. Ifloat u}"
1.104 - shows "x^n \<in> {Ifloat l1..Ifloat u1}"
1.105 + shows "x ^ n \<in> {Ifloat l1..Ifloat u1}"
1.106 proof (cases "even n")
1.107 case True
1.108 show ?thesis
1.109 proof (cases "0 < l")
1.110 case True hence "odd n \<or> 0 < l" and "0 \<le> Ifloat l" unfolding less_float_def by auto
1.111 have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms unfolding float_power_bnds_def if_P[OF `odd n \<or> 0 < l`] by auto
1.112 - have "Ifloat l^n \<le> x^n" and "x^n \<le> Ifloat u^n " using `0 \<le> Ifloat l` and assms unfolding atLeastAtMost_iff using power_mono[of "Ifloat l" x] power_mono[of x "Ifloat u"] by auto
1.113 + have "Ifloat l ^ n \<le> x ^ n" and "x ^ n \<le> Ifloat u ^ n " using `0 \<le> Ifloat l` and assms unfolding atLeastAtMost_iff using power_mono[of "Ifloat l" x] power_mono[of x "Ifloat u"] by auto
1.114 thus ?thesis using assms `0 < l` unfolding atLeastAtMost_iff l1 u1 float_power less_float_def by auto
1.115 next
1.116 case False hence P: "\<not> (odd n \<or> 0 < l)" using `even n` by auto
1.117 show ?thesis
1.118 proof (cases "u < 0")
1.119 case True hence "0 \<le> - Ifloat u" and "- Ifloat u \<le> - x" and "0 \<le> - x" and "-x \<le> - Ifloat l" using assms unfolding less_float_def by auto
1.120 - hence "Ifloat u^n \<le> x^n" and "x^n \<le> Ifloat l^n" using power_mono[of "-x" "-Ifloat l" n] power_mono[of "-Ifloat u" "-x" n]
1.121 + hence "Ifloat u ^ n \<le> x ^ n" and "x ^ n \<le> Ifloat l ^ n" using power_mono[of "-x" "-Ifloat l" n] power_mono[of "-Ifloat u" "-x" n]
1.122 unfolding power_minus_even[OF `even n`] by auto
1.123 moreover have u1: "u1 = l ^ n" and l1: "l1 = u ^ n" using assms unfolding float_power_bnds_def if_not_P[OF P] if_P[OF True] by auto
1.124 ultimately show ?thesis using float_power by auto
1.125 @@ -194,11 +194,11 @@
1.126 next
1.127 case False hence "odd n \<or> 0 < l" by auto
1.128 have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms unfolding float_power_bnds_def if_P[OF `odd n \<or> 0 < l`] by auto
1.129 - have "Ifloat l^n \<le> x^n" and "x^n \<le> Ifloat u^n " using assms unfolding atLeastAtMost_iff using power_mono_odd[OF False] by auto
1.130 + have "Ifloat l ^ n \<le> x ^ n" and "x ^ n \<le> Ifloat u ^ n " using assms unfolding atLeastAtMost_iff using power_mono_odd[OF False] by auto
1.131 thus ?thesis unfolding atLeastAtMost_iff l1 u1 float_power less_float_def by auto
1.132 qed
1.133
1.134 -lemma bnds_power: "\<forall> x l u. (l1, u1) = float_power_bnds n l u \<and> x \<in> {Ifloat l .. Ifloat u} \<longrightarrow> Ifloat l1 \<le> x^n \<and> x^n \<le> Ifloat u1"
1.135 +lemma bnds_power: "\<forall> x l u. (l1, u1) = float_power_bnds n l u \<and> x \<in> {Ifloat l .. Ifloat u} \<longrightarrow> Ifloat l1 \<le> x ^ n \<and> x ^ n \<le> Ifloat u1"
1.136 using float_power_bnds by auto
1.137
1.138 section "Square root"
1.139 @@ -794,8 +794,8 @@
1.140 let "?f n" = "fact (2 * n)"
1.141
1.142 { fix n
1.143 - have F: "\<And>m. ((\<lambda>i. i + 2) ^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
1.144 - have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^ n) 1 * (((\<lambda>i. i + 2) ^ n) 1 + 1)"
1.145 + have F: "\<And>m. ((\<lambda>i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
1.146 + have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) o^ n) 1 * (((\<lambda>i. i + 2) o^ n) 1 + 1)"
1.147 unfolding F by auto } note f_eq = this
1.148
1.149 from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
1.150 @@ -811,7 +811,7 @@
1.151 have "0 < x * x" using `0 < x` unfolding less_float_def Ifloat_mult Ifloat_0
1.152 using mult_pos_pos[where a="Ifloat x" and b="Ifloat x"] by auto
1.153
1.154 - { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x^(2 * i))
1.155 + { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
1.156 = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
1.157 proof -
1.158 have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto
1.159 @@ -905,8 +905,8 @@
1.160 let "?f n" = "fact (2 * n + 1)"
1.161
1.162 { fix n
1.163 - have F: "\<And>m. ((\<lambda>i. i + 2) ^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
1.164 - have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^ n) 2 * (((\<lambda>i. i + 2) ^ n) 2 + 1)"
1.165 + have F: "\<And>m. ((\<lambda>i. i + 2) o^ n) m = m + 2 * n" by (induct n arbitrary: m, auto)
1.166 + have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) o^ n) 2 * (((\<lambda>i. i + 2) o^ n) 2 + 1)"
1.167 unfolding F by auto } note f_eq = this
1.168
1.169 from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
1.170 @@ -1382,8 +1382,8 @@
1.171 shows "exp (Ifloat x) \<in> { Ifloat (lb_exp_horner prec (get_even n) 1 1 x) .. Ifloat (ub_exp_horner prec (get_odd n) 1 1 x) }"
1.172 proof -
1.173 { fix n
1.174 - have F: "\<And> m. ((\<lambda>i. i + 1) ^ n) m = n + m" by (induct n, auto)
1.175 - have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) ^ n) 1" unfolding F by auto } note f_eq = this
1.176 + have F: "\<And> m. ((\<lambda>i. i + 1) o^ n) m = n + m" by (induct n, auto)
1.177 + have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) o^ n) 1" unfolding F by auto } note f_eq = this
1.178
1.179 note bounds = horner_bounds_nonpos[where f="fact" and lb="lb_exp_horner prec" and ub="ub_exp_horner prec" and j'=0 and s=1,
1.180 OF assms f_eq lb_exp_horner.simps ub_exp_horner.simps]
1.181 @@ -1631,10 +1631,10 @@
1.182
1.183 lemma ln_bounds:
1.184 assumes "0 \<le> x" and "x < 1"
1.185 - shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x^(Suc i)) \<le> ln (x + 1)" (is "?lb")
1.186 - and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x^(Suc i))" (is "?ub")
1.187 + shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x ^ (Suc i)) \<le> ln (x + 1)" (is "?lb")
1.188 + and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x ^ (Suc i))" (is "?ub")
1.189 proof -
1.190 - let "?a n" = "(1/real (n +1)) * x^(Suc n)"
1.191 + let "?a n" = "(1/real (n +1)) * x ^ (Suc n)"
1.192
1.193 have ln_eq: "(\<Sum> i. -1^i * ?a i) = ln (x + 1)"
1.194 using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
1.195 @@ -2479,7 +2479,7 @@
1.196 fun lift_var (Free (varname, _)) = (case AList.lookup (op =) bound_eqs varname of
1.197 SOME bound => bound
1.198 | NONE => raise TERM ("No bound equations found for " ^ varname, []))
1.199 - | lift_var t = raise TERM ("Can not convert expression " ^
1.200 + | lift_var t = raise TERM ("Can not convert expression " ^
1.201 (Syntax.string_of_term ctxt t), [t])
1.202
1.203 val _ $ vs = HOLogic.dest_Trueprop (Logic.strip_imp_concl goal')