tuned proofs;
authorwenzelm
Thu Sep 13 17:20:04 2012 +0200 (2012-09-13)
changeset 493510dd3449640b4
parent 49349 be27a453aacc
child 49352 207c333f61af
tuned proofs;
src/HOL/Decision_Procs/Approximation.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Sep 13 16:43:33 2012 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Sep 13 17:20:04 2012 +0200
     1.3 @@ -23,15 +23,20 @@
     1.4  "horner F G 0 i k x       = 0" |
     1.5  "horner F G (Suc n) i k x = 1 / k - x * horner F G n (F i) (G i k) x"
     1.6  
     1.7 -lemma horner_schema': fixes x :: real  and a :: "nat \<Rightarrow> real"
     1.8 +lemma horner_schema':
     1.9 +  fixes x :: real and a :: "nat \<Rightarrow> real"
    1.10    shows "a 0 - x * (\<Sum> i=0..<n. (-1)^i * a (Suc i) * x^i) = (\<Sum> i=0..<Suc n. (-1)^i * a i * x^i)"
    1.11  proof -
    1.12 -  have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)" by auto
    1.13 -  show ?thesis unfolding setsum_right_distrib shift_pow diff_minus setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
    1.14 +  have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)"
    1.15 +    by auto
    1.16 +  show ?thesis
    1.17 +    unfolding setsum_right_distrib shift_pow diff_minus setsum_negf[symmetric]
    1.18 +    setsum_head_upt_Suc[OF zero_less_Suc]
    1.19      setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n  *a n * x^n"] by auto
    1.20  qed
    1.21  
    1.22 -lemma horner_schema: fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
    1.23 +lemma horner_schema:
    1.24 +  fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
    1.25    assumes f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
    1.26    shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / (f (j' + j))) * x ^ j)"
    1.27  proof (induct n arbitrary: j')
    1.28 @@ -46,15 +51,16 @@
    1.29  lemma horner_bounds':
    1.30    fixes lb :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" and ub :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float"
    1.31    assumes "0 \<le> real x" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
    1.32 -  and lb_0: "\<And> i k x. lb 0 i k x = 0"
    1.33 -  and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 k - x * (ub n (F i) (G i k) x)"
    1.34 -  and ub_0: "\<And> i k x. ub 0 i k x = 0"
    1.35 -  and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 k - x * (lb n (F i) (G i k) x)"
    1.36 +    and lb_0: "\<And> i k x. lb 0 i k x = 0"
    1.37 +    and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 k - x * (ub n (F i) (G i k) x)"
    1.38 +    and ub_0: "\<And> i k x. ub 0 i k x = 0"
    1.39 +    and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 k - x * (lb n (F i) (G i k) x)"
    1.40    shows "(lb n ((F ^^ j') s) (f j') x) \<le> horner F G n ((F ^^ j') s) (f j') x \<and>
    1.41           horner F G n ((F ^^ j') s) (f j') x \<le> (ub n ((F ^^ j') s) (f j') x)"
    1.42    (is "?lb n j' \<le> ?horner n j' \<and> ?horner n j' \<le> ?ub n j'")
    1.43  proof (induct n arbitrary: j')
    1.44 -  case 0 thus ?case unfolding lb_0 ub_0 horner.simps by auto
    1.45 +  case 0
    1.46 +  thus ?case unfolding lb_0 ub_0 horner.simps by auto
    1.47  next
    1.48    case (Suc n)
    1.49    thus ?case using lapprox_rat[of prec 1 "f j'"] using rapprox_rat[of 1 "f j'" prec]
    1.50 @@ -71,12 +77,13 @@
    1.51  
    1.52  *}
    1.53  
    1.54 -lemma horner_bounds: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.55 +lemma horner_bounds:
    1.56 +  fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.57    assumes "0 \<le> real x" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
    1.58 -  and lb_0: "\<And> i k x. lb 0 i k x = 0"
    1.59 -  and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 k - x * (ub n (F i) (G i k) x)"
    1.60 -  and ub_0: "\<And> i k x. ub 0 i k x = 0"
    1.61 -  and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 k - x * (lb n (F i) (G i k) x)"
    1.62 +    and lb_0: "\<And> i k x. lb 0 i k x = 0"
    1.63 +    and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 k - x * (ub n (F i) (G i k) x)"
    1.64 +    and ub_0: "\<And> i k x. ub 0 i k x = 0"
    1.65 +    and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 k - x * (lb n (F i) (G i k) x)"
    1.66    shows "(lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1 ^ j * (1 / (f (j' + j))) * (x ^ j))" (is "?lb") and
    1.67      "(\<Sum>j=0..<n. -1 ^ j * (1 / (f (j' + j))) * (x ^ j)) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
    1.68  proof -
    1.69 @@ -86,12 +93,13 @@
    1.70    thus "?lb" and "?ub" by auto
    1.71  qed
    1.72  
    1.73 -lemma horner_bounds_nonpos: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.74 +lemma horner_bounds_nonpos:
    1.75 +  fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.76    assumes "real x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
    1.77 -  and lb_0: "\<And> i k x. lb 0 i k x = 0"
    1.78 -  and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 k + x * (ub n (F i) (G i k) x)"
    1.79 -  and ub_0: "\<And> i k x. ub 0 i k x = 0"
    1.80 -  and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 k + x * (lb n (F i) (G i k) x)"
    1.81 +    and lb_0: "\<And> i k x. lb 0 i k x = 0"
    1.82 +    and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 k + x * (ub n (F i) (G i k) x)"
    1.83 +    and ub_0: "\<And> i k x. ub 0 i k x = 0"
    1.84 +    and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 k + x * (lb n (F i) (G i k) x)"
    1.85    shows "(lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / (f (j' + j))) * real x ^ j)" (is "?lb") and
    1.86      "(\<Sum>j=0..<n. (1 / (f (j' + j))) * real x ^ j) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
    1.87  proof -
    1.88 @@ -320,8 +328,7 @@
    1.89    thus ?thesis unfolding lb_sqrt.simps by auto
    1.90  qed
    1.91  
    1.92 -lemma bnds_sqrt':
    1.93 -  shows "sqrt x \<in> {(lb_sqrt prec x) .. (ub_sqrt prec x) }"
    1.94 +lemma bnds_sqrt': "sqrt x \<in> {(lb_sqrt prec x) .. (ub_sqrt prec x)}"
    1.95  proof -
    1.96    { fix x :: float assume "0 < x"
    1.97      hence "0 < real x" and "0 \<le> real x" by auto
    1.98 @@ -402,7 +409,8 @@
    1.99  | "lb_arctan_horner prec (Suc n) k x =
   1.100      (lapprox_rat prec 1 k) - x * (ub_arctan_horner prec n (k + 2) x)"
   1.101  
   1.102 -lemma arctan_0_1_bounds': assumes "0 \<le> real x" "real x \<le> 1" and "even n"
   1.103 +lemma arctan_0_1_bounds':
   1.104 +  assumes "0 \<le> real x" "real x \<le> 1" and "even n"
   1.105    shows "arctan x \<in> {(x * lb_arctan_horner prec n 1 (x * x)) .. (x * ub_arctan_horner prec (Suc n) 1 (x * x))}"
   1.106  proof -
   1.107    let "?c i" = "-1^i * (1 / (i * 2 + (1::nat)) * real x ^ (i * 2 + 1))"
   1.108 @@ -2031,7 +2039,8 @@
   1.109    qed
   1.110  qed
   1.111  
   1.112 -lemma ub_ln_lb_ln_bounds: assumes "0 < x"
   1.113 +lemma ub_ln_lb_ln_bounds:
   1.114 +  assumes "0 < x"
   1.115    shows "the (lb_ln prec x) \<le> ln x \<and> ln x \<le> the (ub_ln prec x)"
   1.116    (is "?lb \<le> ?ln \<and> ?ln \<le> ?ub")
   1.117  proof (cases "x < 1")
   1.118 @@ -2067,7 +2076,8 @@
   1.119      unfolding if_not_P[OF `\<not> x \<le> 0`] if_P[OF True] by auto
   1.120  qed
   1.121  
   1.122 -lemma lb_ln: assumes "Some y = lb_ln prec x"
   1.123 +lemma lb_ln:
   1.124 +  assumes "Some y = lb_ln prec x"
   1.125    shows "y \<le> ln x" and "0 < real x"
   1.126  proof -
   1.127    have "0 < x"
   1.128 @@ -2080,7 +2090,8 @@
   1.129    thus "y \<le> ln x" unfolding assms[symmetric] by auto
   1.130  qed
   1.131  
   1.132 -lemma ub_ln: assumes "Some y = ub_ln prec x"
   1.133 +lemma ub_ln:
   1.134 +  assumes "Some y = ub_ln prec x"
   1.135    shows "ln x \<le> y" and "0 < real x"
   1.136  proof -
   1.137    have "0 < x"
   1.138 @@ -2577,7 +2588,7 @@
   1.139  lemma approx_form_approx_form':
   1.140    assumes "approx_form' prec f s n l u bs ss" and "(x::real) \<in> { l .. u }"
   1.141    obtains l' u' where "x \<in> { l' .. u' }"
   1.142 -  and "approx_form prec f (bs[n := Some (l', u')]) ss"
   1.143 +    and "approx_form prec f (bs[n := Some (l', u')]) ss"
   1.144  using assms proof (induct s arbitrary: l u)
   1.145    case 0
   1.146    from this(1)[of l u] this(2,3)
   1.147 @@ -2605,7 +2616,7 @@
   1.148  
   1.149  lemma approx_form_aux:
   1.150    assumes "approx_form prec f vs ss"
   1.151 -  and "bounded_by xs vs"
   1.152 +    and "bounded_by xs vs"
   1.153    shows "interpret_form f xs"
   1.154  using assms proof (induct f arbitrary: vs)
   1.155    case (Bound x a b f)
   1.156 @@ -2658,8 +2669,8 @@
   1.157    case (Less a b)
   1.158    then obtain l u l' u'
   1.159      where l_eq: "Some (l, u) = approx prec a vs"
   1.160 -    and u_eq: "Some (l', u') = approx prec b vs"
   1.161 -    and inequality: "u < l'"
   1.162 +      and u_eq: "Some (l', u') = approx prec b vs"
   1.163 +      and inequality: "u < l'"
   1.164      by (cases "approx prec a vs", auto,
   1.165        cases "approx prec b vs", auto)
   1.166    from inequality approx[OF Less.prems(2) l_eq] approx[OF Less.prems(2) u_eq]
   1.167 @@ -2668,8 +2679,8 @@
   1.168    case (LessEqual a b)
   1.169    then obtain l u l' u'
   1.170      where l_eq: "Some (l, u) = approx prec a vs"
   1.171 -    and u_eq: "Some (l', u') = approx prec b vs"
   1.172 -    and inequality: "u \<le> l'"
   1.173 +      and u_eq: "Some (l', u') = approx prec b vs"
   1.174 +      and inequality: "u \<le> l'"
   1.175      by (cases "approx prec a vs", auto,
   1.176        cases "approx prec b vs", auto)
   1.177    from inequality approx[OF LessEqual.prems(2) l_eq] approx[OF LessEqual.prems(2) u_eq]
   1.178 @@ -2740,21 +2751,27 @@
   1.179    shows "DERIV (\<lambda> x'. interpret_floatarith f (vs[n := x'])) x :>
   1.180                 interpret_floatarith (DERIV_floatarith n f) (vs[n := x])"
   1.181     (is "DERIV (?i f) x :> _")
   1.182 -using isDERIV proof (induct f arbitrary: x)
   1.183 -     case (Inverse a) thus ?case
   1.184 +using isDERIV
   1.185 +proof (induct f arbitrary: x)
   1.186 +  case (Inverse a)
   1.187 +  thus ?case
   1.188 +    by (auto intro!: DERIV_intros simp add: algebra_simps power2_eq_square)
   1.189 +next
   1.190 +  case (Cos a)
   1.191 +  thus ?case
   1.192      by (auto intro!: DERIV_intros
   1.193 -             simp add: algebra_simps power2_eq_square)
   1.194 -next case (Cos a) thus ?case
   1.195 -  apply (auto intro!: DERIV_intros
   1.196             simp del: interpret_floatarith.simps(5)
   1.197             simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
   1.198 -  done
   1.199 -next case (Power a n) thus ?case
   1.200 -  by (cases n, auto intro!: DERIV_intros
   1.201 -                    simp del: power_Suc)
   1.202 -next case (Ln a) thus ?case
   1.203 -    by (auto intro!: DERIV_intros simp add: divide_inverse)
   1.204 -next case (Var i) thus ?case using `n < length vs` by auto
   1.205 +next
   1.206 +  case (Power a n)
   1.207 +  thus ?case
   1.208 +    by (cases n) (auto intro!: DERIV_intros simp del: power_Suc)
   1.209 +next
   1.210 +  case (Ln a)
   1.211 +  thus ?case by (auto intro!: DERIV_intros simp add: divide_inverse)
   1.212 +next
   1.213 +  case (Var i)
   1.214 +  thus ?case using `n < length vs` by auto
   1.215  qed (auto intro!: DERIV_intros)
   1.216  
   1.217  declare approx.simps[simp del]
   1.218 @@ -2783,13 +2800,14 @@
   1.219  
   1.220  lemma isDERIV_approx:
   1.221    assumes "bounded_by xs vs"
   1.222 -  and isDERIV_approx: "isDERIV_approx prec x f vs"
   1.223 +    and isDERIV_approx: "isDERIV_approx prec x f vs"
   1.224    shows "isDERIV x f xs"
   1.225 -using isDERIV_approx proof (induct f)
   1.226 +  using isDERIV_approx
   1.227 +proof (induct f)
   1.228    case (Inverse a)
   1.229    then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
   1.230      and *: "0 < l \<or> u < 0"
   1.231 -    by (cases "approx prec a vs", auto)
   1.232 +    by (cases "approx prec a vs") auto
   1.233    with approx[OF `bounded_by xs vs` approx_Some]
   1.234    have "interpret_floatarith a xs \<noteq> 0" by auto
   1.235    thus ?case using Inverse by auto
   1.236 @@ -2797,7 +2815,7 @@
   1.237    case (Ln a)
   1.238    then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
   1.239      and *: "0 < l"
   1.240 -    by (cases "approx prec a vs", auto)
   1.241 +    by (cases "approx prec a vs") auto
   1.242    with approx[OF `bounded_by xs vs` approx_Some]
   1.243    have "0 < interpret_floatarith a xs" by auto
   1.244    thus ?case using Ln by auto
   1.245 @@ -2805,46 +2823,49 @@
   1.246    case (Sqrt a)
   1.247    then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
   1.248      and *: "0 < l"
   1.249 -    by (cases "approx prec a vs", auto)
   1.250 +    by (cases "approx prec a vs") auto
   1.251    with approx[OF `bounded_by xs vs` approx_Some]
   1.252    have "0 < interpret_floatarith a xs" by auto
   1.253    thus ?case using Sqrt by auto
   1.254  next
   1.255 -  case (Power a n) thus ?case by (cases n, auto)
   1.256 +  case (Power a n) thus ?case by (cases n) auto
   1.257  qed auto
   1.258  
   1.259  lemma bounded_by_update_var:
   1.260    assumes "bounded_by xs vs" and "vs ! i = Some (l, u)"
   1.261 -  and bnd: "x \<in> { real l .. real u }"
   1.262 +    and bnd: "x \<in> { real l .. real u }"
   1.263    shows "bounded_by (xs[i := x]) vs"
   1.264  proof (cases "i < length xs")
   1.265 -  case False thus ?thesis using `bounded_by xs vs` by auto
   1.266 +  case False
   1.267 +  thus ?thesis using `bounded_by xs vs` by auto
   1.268  next
   1.269    let ?xs = "xs[i := x]"
   1.270    case True hence "i < length ?xs" by auto
   1.271 -{ fix j
   1.272 -  assume "j < length vs"
   1.273 -  have "case vs ! j of None \<Rightarrow> True | Some (l, u) \<Rightarrow> ?xs ! j \<in> { real l .. real u }"
   1.274 -  proof (cases "vs ! j")
   1.275 -    case (Some b)
   1.276 -    thus ?thesis
   1.277 -    proof (cases "i = j")
   1.278 -      case True
   1.279 -      thus ?thesis using `vs ! i = Some (l, u)` Some and bnd `i < length ?xs`
   1.280 -        by auto
   1.281 -    next
   1.282 -      case False
   1.283 -      thus ?thesis using `bounded_by xs vs`[THEN bounded_byE, OF `j < length vs`] Some
   1.284 -        by auto
   1.285 -    qed
   1.286 -  qed auto }
   1.287 +  {
   1.288 +    fix j
   1.289 +    assume "j < length vs"
   1.290 +    have "case vs ! j of None \<Rightarrow> True | Some (l, u) \<Rightarrow> ?xs ! j \<in> { real l .. real u }"
   1.291 +    proof (cases "vs ! j")
   1.292 +      case (Some b)
   1.293 +      thus ?thesis
   1.294 +      proof (cases "i = j")
   1.295 +        case True
   1.296 +        thus ?thesis using `vs ! i = Some (l, u)` Some and bnd `i < length ?xs`
   1.297 +          by auto
   1.298 +      next
   1.299 +        case False
   1.300 +        thus ?thesis
   1.301 +          using `bounded_by xs vs`[THEN bounded_byE, OF `j < length vs`] Some by auto
   1.302 +      qed
   1.303 +    qed auto
   1.304 +  }
   1.305    thus ?thesis unfolding bounded_by_def by auto
   1.306  qed
   1.307  
   1.308  lemma isDERIV_approx':
   1.309    assumes "bounded_by xs vs"
   1.310 -  and vs_x: "vs ! x = Some (l, u)" and X_in: "X \<in> { real l .. real u }"
   1.311 -  and approx: "isDERIV_approx prec x f vs"
   1.312 +    and vs_x: "vs ! x = Some (l, u)" and X_in: "X \<in> { real l .. real u }"
   1.313 +    and approx: "isDERIV_approx prec x f vs"
   1.314    shows "isDERIV x f (xs[x := X])"
   1.315  proof -
   1.316    note bounded_by_update_var[OF `bounded_by xs vs` vs_x X_in] approx
   1.317 @@ -2853,8 +2874,8 @@
   1.318  
   1.319  lemma DERIV_approx:
   1.320    assumes "n < length xs" and bnd: "bounded_by xs vs"
   1.321 -  and isD: "isDERIV_approx prec n f vs"
   1.322 -  and app: "Some (l, u) = approx prec (DERIV_floatarith n f) vs" (is "_ = approx _ ?D _")
   1.323 +    and isD: "isDERIV_approx prec n f vs"
   1.324 +    and app: "Some (l, u) = approx prec (DERIV_floatarith n f) vs" (is "_ = approx _ ?D _")
   1.325    shows "\<exists>(x::real). l \<le> x \<and> x \<le> u \<and>
   1.326               DERIV (\<lambda> x. interpret_floatarith f (xs[n := x])) (xs!n) :> x"
   1.327           (is "\<exists> x. _ \<and> _ \<and> DERIV (?i f) _ :> _")
   1.328 @@ -2867,17 +2888,19 @@
   1.329    show "DERIV (?i f) (xs!n) :> (?i ?D (xs!n))" by simp
   1.330  qed
   1.331  
   1.332 -fun lift_bin :: "(float * float) option \<Rightarrow> (float * float) option \<Rightarrow> (float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> (float * float) option) \<Rightarrow> (float * float) option" where
   1.333 -"lift_bin (Some (l1, u1)) (Some (l2, u2)) f = f l1 u1 l2 u2" |
   1.334 -"lift_bin a b f = None"
   1.335 +fun lift_bin :: "(float * float) option \<Rightarrow>
   1.336 +    (float * float) option \<Rightarrow> (float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> (float * float) option) \<Rightarrow>
   1.337 +    (float * float) option" where
   1.338 +  "lift_bin (Some (l1, u1)) (Some (l2, u2)) f = f l1 u1 l2 u2"
   1.339 +| "lift_bin a b f = None"
   1.340  
   1.341  lemma lift_bin:
   1.342    assumes lift_bin_Some: "Some (l, u) = lift_bin a b f"
   1.343    obtains l1 u1 l2 u2
   1.344    where "a = Some (l1, u1)"
   1.345 -  and "b = Some (l2, u2)"
   1.346 -  and "f l1 u1 l2 u2 = Some (l, u)"
   1.347 -using assms by (cases a, simp, cases b, simp, auto)
   1.348 +    and "b = Some (l2, u2)"
   1.349 +    and "f l1 u1 l2 u2 = Some (l, u)"
   1.350 +  using assms by (cases a, simp, cases b, simp, auto)
   1.351  
   1.352  fun approx_tse where
   1.353  "approx_tse prec n 0 c k f bs = approx prec f bs" |
   1.354 @@ -2894,10 +2917,11 @@
   1.355  
   1.356  lemma bounded_by_Cons:
   1.357    assumes bnd: "bounded_by xs vs"
   1.358 -  and x: "x \<in> { real l .. real u }"
   1.359 +    and x: "x \<in> { real l .. real u }"
   1.360    shows "bounded_by (x#xs) ((Some (l, u))#vs)"
   1.361  proof -
   1.362 -  { fix i assume *: "i < length ((Some (l, u))#vs)"
   1.363 +  {
   1.364 +    fix i assume *: "i < length ((Some (l, u))#vs)"
   1.365      have "case ((Some (l,u))#vs) ! i of Some (l, u) \<Rightarrow> (x#xs)!i \<in> { real l .. real u } | None \<Rightarrow> True"
   1.366      proof (cases i)
   1.367        case 0 with x show ?thesis by auto
   1.368 @@ -2905,15 +2929,16 @@
   1.369        case (Suc i) with * have "i < length vs" by auto
   1.370        from bnd[THEN bounded_byE, OF this]
   1.371        show ?thesis unfolding Suc nth_Cons_Suc .
   1.372 -    qed }
   1.373 +    qed
   1.374 +  }
   1.375    thus ?thesis by (auto simp add: bounded_by_def)
   1.376  qed
   1.377  
   1.378  lemma approx_tse_generic:
   1.379    assumes "bounded_by xs vs"
   1.380 -  and bnd_c: "bounded_by (xs[x := c]) vs" and "x < length vs" and "x < length xs"
   1.381 -  and bnd_x: "vs ! x = Some (lx, ux)"
   1.382 -  and ate: "Some (l, u) = approx_tse prec x s c k f vs"
   1.383 +    and bnd_c: "bounded_by (xs[x := c]) vs" and "x < length vs" and "x < length xs"
   1.384 +    and bnd_x: "vs ! x = Some (lx, ux)"
   1.385 +    and ate: "Some (l, u) = approx_tse prec x s c k f vs"
   1.386    shows "\<exists> n. (\<forall> m < n. \<forall> (z::real) \<in> {lx .. ux}.
   1.387        DERIV (\<lambda> y. interpret_floatarith ((DERIV_floatarith x ^^ m) f) (xs[x := y])) z :>
   1.388              (interpret_floatarith ((DERIV_floatarith x ^^ (Suc m)) f) (xs[x := z])))
   1.389 @@ -2925,36 +2950,39 @@
   1.390        (xs!x - c)^n \<in> {l .. u})" (is "\<exists> n. ?taylor f k l u n")
   1.391  using ate proof (induct s arbitrary: k f l u)
   1.392    case 0
   1.393 -  { fix t::real assume "t \<in> {lx .. ux}"
   1.394 +  {
   1.395 +    fix t::real assume "t \<in> {lx .. ux}"
   1.396      note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
   1.397      from approx[OF this 0[unfolded approx_tse.simps]]
   1.398      have "(interpret_floatarith f (xs[x := t])) \<in> {l .. u}"
   1.399        by (auto simp add: algebra_simps)
   1.400 -  } thus ?case by (auto intro!: exI[of _ 0])
   1.401 +  }
   1.402 +  thus ?case by (auto intro!: exI[of _ 0])
   1.403  next
   1.404    case (Suc s)
   1.405    show ?case
   1.406    proof (cases "isDERIV_approx prec x f vs")
   1.407      case False
   1.408      note ap = Suc.prems[unfolded approx_tse.simps if_not_P[OF False]]
   1.409 -
   1.410 -    { fix t::real assume "t \<in> {lx .. ux}"
   1.411 +    {
   1.412 +      fix t::real assume "t \<in> {lx .. ux}"
   1.413        note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
   1.414        from approx[OF this ap]
   1.415        have "(interpret_floatarith f (xs[x := t])) \<in> {l .. u}"
   1.416          by (auto simp add: algebra_simps)
   1.417 -    } thus ?thesis by (auto intro!: exI[of _ 0])
   1.418 +    }
   1.419 +    thus ?thesis by (auto intro!: exI[of _ 0])
   1.420    next
   1.421      case True
   1.422      with Suc.prems
   1.423      obtain l1 u1 l2 u2
   1.424        where a: "Some (l1, u1) = approx prec f (vs[x := Some (c,c)])"
   1.425 -      and ate: "Some (l2, u2) = approx_tse prec x s c (Suc k) (DERIV_floatarith x f) vs"
   1.426 -      and final: "Some (l, u) = approx prec
   1.427 -        (Add (Var 0)
   1.428 -             (Mult (Inverse (Num (Float (int k) 0)))
   1.429 -                   (Mult (Add (Var (Suc (Suc 0))) (Minus (Num c)))
   1.430 -                         (Var (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
   1.431 +        and ate: "Some (l2, u2) = approx_tse prec x s c (Suc k) (DERIV_floatarith x f) vs"
   1.432 +        and final: "Some (l, u) = approx prec
   1.433 +          (Add (Var 0)
   1.434 +               (Mult (Inverse (Num (Float (int k) 0)))
   1.435 +                     (Mult (Add (Var (Suc (Suc 0))) (Minus (Num c)))
   1.436 +                           (Var (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
   1.437        by (auto elim!: lift_bin) blast
   1.438  
   1.439      from bnd_c `x < length xs`
   1.440 @@ -2966,9 +2994,11 @@
   1.441                (is "?f 0 (real c) \<in> _")
   1.442        by auto
   1.443  
   1.444 -    { fix f :: "'a \<Rightarrow> 'a" fix n :: nat fix x :: 'a
   1.445 +    {
   1.446 +      fix f :: "'a \<Rightarrow> 'a" fix n :: nat fix x :: 'a
   1.447        have "(f ^^ Suc n) x = (f ^^ n) (f x)"
   1.448 -        by (induct n, auto) }
   1.449 +        by (induct n) auto
   1.450 +    }
   1.451      note funpow_Suc = this[symmetric]
   1.452      from Suc.hyps[OF ate, unfolded this]
   1.453      obtain n
   1.454 @@ -2978,7 +3008,8 @@
   1.455            (is "\<forall> t \<in> _. ?X (Suc k) f n t \<in> _")
   1.456        by blast
   1.457  
   1.458 -    { fix m and z::real
   1.459 +    {
   1.460 +      fix m and z::real
   1.461        assume "m < Suc n" and bnd_z: "z \<in> { lx .. ux }"
   1.462        have "DERIV (?f m) z :> ?f (Suc m) z"
   1.463        proof (cases m)
   1.464 @@ -2990,7 +3021,8 @@
   1.465          hence "m' < n" using `m < Suc n` by auto
   1.466          from DERIV_hyp[OF this bnd_z]
   1.467          show ?thesis using Suc by simp
   1.468 -      qed } note DERIV = this
   1.469 +      qed
   1.470 +    } note DERIV = this
   1.471  
   1.472      have "\<And> k i. k < i \<Longrightarrow> {k ..< i} = insert k {Suc k ..< i}" by auto
   1.473      hence setprod_head_Suc: "\<And> k i. \<Prod> {k ..< k + Suc i} = k * \<Prod> {Suc k ..< Suc k + i}" by auto
   1.474 @@ -2999,7 +3031,8 @@
   1.475        unfolding setsum_head_upt_Suc[OF zero_less_Suc] ..
   1.476      def C \<equiv> "xs!x - c"
   1.477  
   1.478 -    { fix t::real assume t: "t \<in> {lx .. ux}"
   1.479 +    {
   1.480 +      fix t::real assume t: "t \<in> {lx .. ux}"
   1.481        hence "bounded_by [xs!x] [vs!x]"
   1.482          using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`]
   1.483          by (cases "vs!x", auto simp add: bounded_by_def)
   1.484 @@ -3016,24 +3049,28 @@
   1.485          unfolding funpow_Suc C_def[symmetric] setsum_move0 setprod_head_Suc
   1.486          by (auto simp add: algebra_simps)
   1.487            (simp only: mult_left_commute [of _ "inverse (real k)"] setsum_right_distrib [symmetric])
   1.488 -      finally have "?T \<in> {l .. u}" . }
   1.489 +      finally have "?T \<in> {l .. u}" .
   1.490 +    }
   1.491      thus ?thesis using DERIV by blast
   1.492    qed
   1.493  qed
   1.494  
   1.495  lemma setprod_fact: "\<Prod> {1..<1 + k} = fact (k :: nat)"
   1.496  proof (induct k)
   1.497 +  case 0
   1.498 +  show ?case by simp
   1.499 +next
   1.500    case (Suc k)
   1.501    have "{ 1 ..< Suc (Suc k) } = insert (Suc k) { 1 ..< Suc k }" by auto
   1.502    hence "\<Prod> { 1 ..< Suc (Suc k) } = (Suc k) * \<Prod> { 1 ..< Suc k }" by auto
   1.503    thus ?case using Suc by auto
   1.504 -qed simp
   1.505 +qed
   1.506  
   1.507  lemma approx_tse:
   1.508    assumes "bounded_by xs vs"
   1.509 -  and bnd_x: "vs ! x = Some (lx, ux)" and bnd_c: "real c \<in> {lx .. ux}"
   1.510 -  and "x < length vs" and "x < length xs"
   1.511 -  and ate: "Some (l, u) = approx_tse prec x s c 1 f vs"
   1.512 +    and bnd_x: "vs ! x = Some (lx, ux)" and bnd_c: "real c \<in> {lx .. ux}"
   1.513 +    and "x < length vs" and "x < length xs"
   1.514 +    and ate: "Some (l, u) = approx_tse prec x s c 1 f vs"
   1.515    shows "interpret_floatarith f xs \<in> { l .. u }"
   1.516  proof -
   1.517    def F \<equiv> "\<lambda> n z. interpret_floatarith ((DERIV_floatarith x ^^ n) f) (xs[x := z])"
   1.518 @@ -3247,10 +3284,18 @@
   1.519        case (Assign x a f') with assms
   1.520        show ?thesis by (auto elim!: option_caseE simp add: f_def approx_tse_form_def)
   1.521      qed } thus ?thesis unfolding f_def by auto
   1.522 -next case Assign with assms show ?thesis by (auto simp add: approx_tse_form_def)
   1.523 -next case LessEqual with assms show ?thesis by (auto simp add: approx_tse_form_def)
   1.524 -next case Less with assms show ?thesis by (auto simp add: approx_tse_form_def)
   1.525 -next case AtLeastAtMost with assms show ?thesis by (auto simp add: approx_tse_form_def)
   1.526 +next
   1.527 +  case Assign
   1.528 +  with assms show ?thesis by (auto simp add: approx_tse_form_def)
   1.529 +next
   1.530 +  case LessEqual
   1.531 +  with assms show ?thesis by (auto simp add: approx_tse_form_def)
   1.532 +next
   1.533 +  case Less
   1.534 +  with assms show ?thesis by (auto simp add: approx_tse_form_def)
   1.535 +next
   1.536 +  case AtLeastAtMost
   1.537 +  with assms show ?thesis by (auto simp add: approx_tse_form_def)
   1.538  qed
   1.539  
   1.540  text {* @{term approx_form_eval} is only used for the {\tt value}-command. *}