author wenzelm Thu, 13 Sep 2012 17:20:44 +0200 changeset 49352 207c333f61af parent 49350 ea3fa2e0f960 (current diff) parent 49351 0dd3449640b4 (diff) child 49353 023be49d7fb8
merged
```--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Sep 13 17:15:04 2012 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Sep 13 17:20:44 2012 +0200
@@ -23,15 +23,20 @@
"horner F G 0 i k x       = 0" |
"horner F G (Suc n) i k x = 1 / k - x * horner F G n (F i) (G i k) x"

-lemma horner_schema': fixes x :: real  and a :: "nat \<Rightarrow> real"
+lemma horner_schema':
+  fixes x :: real and a :: "nat \<Rightarrow> real"
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)"
proof -
-  have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)" by auto
-  show ?thesis unfolding setsum_right_distrib shift_pow diff_minus setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
+  have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)"
+    by auto
+  show ?thesis
+    unfolding setsum_right_distrib shift_pow diff_minus setsum_negf[symmetric]
setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n  *a n * x^n"] by auto
qed

-lemma horner_schema: fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
+lemma horner_schema:
+  fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
assumes f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / (f (j' + j))) * x ^ j)"
proof (induct n arbitrary: j')
@@ -46,15 +51,16 @@
lemma horner_bounds':
fixes lb :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" and ub :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float"
assumes "0 \<le> real x" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
-  and lb_0: "\<And> i k x. lb 0 i k x = 0"
-  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)"
-  and ub_0: "\<And> i k x. ub 0 i k x = 0"
-  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)"
+    and lb_0: "\<And> i k x. lb 0 i k x = 0"
+    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)"
+    and ub_0: "\<And> i k x. ub 0 i k x = 0"
+    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)"
shows "(lb n ((F ^^ j') s) (f j') x) \<le> horner F G n ((F ^^ j') s) (f j') x \<and>
horner F G n ((F ^^ j') s) (f j') x \<le> (ub n ((F ^^ j') s) (f j') x)"
(is "?lb n j' \<le> ?horner n j' \<and> ?horner n j' \<le> ?ub n j'")
proof (induct n arbitrary: j')
-  case 0 thus ?case unfolding lb_0 ub_0 horner.simps by auto
+  case 0
+  thus ?case unfolding lb_0 ub_0 horner.simps by auto
next
case (Suc n)
thus ?case using lapprox_rat[of prec 1 "f j'"] using rapprox_rat[of 1 "f j'" prec]
@@ -71,12 +77,13 @@

*}

-lemma horner_bounds: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+lemma horner_bounds:
+  fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
assumes "0 \<le> real x" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
-  and lb_0: "\<And> i k x. lb 0 i k x = 0"
-  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)"
-  and ub_0: "\<And> i k x. ub 0 i k x = 0"
-  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)"
+    and lb_0: "\<And> i k x. lb 0 i k x = 0"
+    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)"
+    and ub_0: "\<And> i k x. ub 0 i k x = 0"
+    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)"
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
"(\<Sum>j=0..<n. -1 ^ j * (1 / (f (j' + j))) * (x ^ j)) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
proof -
@@ -86,12 +93,13 @@
thus "?lb" and "?ub" by auto
qed

-lemma horner_bounds_nonpos: fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+lemma horner_bounds_nonpos:
+  fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat"
assumes "real x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
-  and lb_0: "\<And> i k x. lb 0 i k x = 0"
-  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)"
-  and ub_0: "\<And> i k x. ub 0 i k x = 0"
-  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)"
+    and lb_0: "\<And> i k x. lb 0 i k x = 0"
+    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)"
+    and ub_0: "\<And> i k x. ub 0 i k x = 0"
+    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)"
shows "(lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / (f (j' + j))) * real x ^ j)" (is "?lb") and
"(\<Sum>j=0..<n. (1 / (f (j' + j))) * real x ^ j) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
proof -
@@ -320,8 +328,7 @@
thus ?thesis unfolding lb_sqrt.simps by auto
qed

-lemma bnds_sqrt':
-  shows "sqrt x \<in> {(lb_sqrt prec x) .. (ub_sqrt prec x) }"
+lemma bnds_sqrt': "sqrt x \<in> {(lb_sqrt prec x) .. (ub_sqrt prec x)}"
proof -
{ fix x :: float assume "0 < x"
hence "0 < real x" and "0 \<le> real x" by auto
@@ -402,7 +409,8 @@
| "lb_arctan_horner prec (Suc n) k x =
(lapprox_rat prec 1 k) - x * (ub_arctan_horner prec n (k + 2) x)"

-lemma arctan_0_1_bounds': assumes "0 \<le> real x" "real x \<le> 1" and "even n"
+lemma arctan_0_1_bounds':
+  assumes "0 \<le> real x" "real x \<le> 1" and "even n"
shows "arctan x \<in> {(x * lb_arctan_horner prec n 1 (x * x)) .. (x * ub_arctan_horner prec (Suc n) 1 (x * x))}"
proof -
let "?c i" = "-1^i * (1 / (i * 2 + (1::nat)) * real x ^ (i * 2 + 1))"
@@ -2031,7 +2039,8 @@
qed
qed

-lemma ub_ln_lb_ln_bounds: assumes "0 < x"
+lemma ub_ln_lb_ln_bounds:
+  assumes "0 < x"
shows "the (lb_ln prec x) \<le> ln x \<and> ln x \<le> the (ub_ln prec x)"
(is "?lb \<le> ?ln \<and> ?ln \<le> ?ub")
proof (cases "x < 1")
@@ -2067,7 +2076,8 @@
unfolding if_not_P[OF `\<not> x \<le> 0`] if_P[OF True] by auto
qed

-lemma lb_ln: assumes "Some y = lb_ln prec x"
+lemma lb_ln:
+  assumes "Some y = lb_ln prec x"
shows "y \<le> ln x" and "0 < real x"
proof -
have "0 < x"
@@ -2080,7 +2090,8 @@
thus "y \<le> ln x" unfolding assms[symmetric] by auto
qed

-lemma ub_ln: assumes "Some y = ub_ln prec x"
+lemma ub_ln:
+  assumes "Some y = ub_ln prec x"
shows "ln x \<le> y" and "0 < real x"
proof -
have "0 < x"
@@ -2577,7 +2588,7 @@
lemma approx_form_approx_form':
assumes "approx_form' prec f s n l u bs ss" and "(x::real) \<in> { l .. u }"
obtains l' u' where "x \<in> { l' .. u' }"
-  and "approx_form prec f (bs[n := Some (l', u')]) ss"
+    and "approx_form prec f (bs[n := Some (l', u')]) ss"
using assms proof (induct s arbitrary: l u)
case 0
from this(1)[of l u] this(2,3)
@@ -2605,7 +2616,7 @@

lemma approx_form_aux:
assumes "approx_form prec f vs ss"
-  and "bounded_by xs vs"
+    and "bounded_by xs vs"
shows "interpret_form f xs"
using assms proof (induct f arbitrary: vs)
case (Bound x a b f)
@@ -2658,8 +2669,8 @@
case (Less a b)
then obtain l u l' u'
where l_eq: "Some (l, u) = approx prec a vs"
-    and u_eq: "Some (l', u') = approx prec b vs"
-    and inequality: "u < l'"
+      and u_eq: "Some (l', u') = approx prec b vs"
+      and inequality: "u < l'"
by (cases "approx prec a vs", auto,
cases "approx prec b vs", auto)
from inequality approx[OF Less.prems(2) l_eq] approx[OF Less.prems(2) u_eq]
@@ -2668,8 +2679,8 @@
case (LessEqual a b)
then obtain l u l' u'
where l_eq: "Some (l, u) = approx prec a vs"
-    and u_eq: "Some (l', u') = approx prec b vs"
-    and inequality: "u \<le> l'"
+      and u_eq: "Some (l', u') = approx prec b vs"
+      and inequality: "u \<le> l'"
by (cases "approx prec a vs", auto,
cases "approx prec b vs", auto)
from inequality approx[OF LessEqual.prems(2) l_eq] approx[OF LessEqual.prems(2) u_eq]
@@ -2740,21 +2751,27 @@
shows "DERIV (\<lambda> x'. interpret_floatarith f (vs[n := x'])) x :>
interpret_floatarith (DERIV_floatarith n f) (vs[n := x])"
(is "DERIV (?i f) x :> _")
-using isDERIV proof (induct f arbitrary: x)
-     case (Inverse a) thus ?case
+using isDERIV
+proof (induct f arbitrary: x)
+  case (Inverse a)
+  thus ?case
+    by (auto intro!: DERIV_intros simp add: algebra_simps power2_eq_square)
+next
+  case (Cos a)
+  thus ?case
by (auto intro!: DERIV_intros
-next case (Cos a) thus ?case
-  apply (auto intro!: DERIV_intros
simp del: interpret_floatarith.simps(5)
-  done
-next case (Power a n) thus ?case
-  by (cases n, auto intro!: DERIV_intros
-                    simp del: power_Suc)
-next case (Ln a) thus ?case
-    by (auto intro!: DERIV_intros simp add: divide_inverse)
-next case (Var i) thus ?case using `n < length vs` by auto
+next
+  case (Power a n)
+  thus ?case
+    by (cases n) (auto intro!: DERIV_intros simp del: power_Suc)
+next
+  case (Ln a)
+  thus ?case by (auto intro!: DERIV_intros simp add: divide_inverse)
+next
+  case (Var i)
+  thus ?case using `n < length vs` by auto
qed (auto intro!: DERIV_intros)

declare approx.simps[simp del]
@@ -2783,13 +2800,14 @@

lemma isDERIV_approx:
assumes "bounded_by xs vs"
-  and isDERIV_approx: "isDERIV_approx prec x f vs"
+    and isDERIV_approx: "isDERIV_approx prec x f vs"
shows "isDERIV x f xs"
-using isDERIV_approx proof (induct f)
+  using isDERIV_approx
+proof (induct f)
case (Inverse a)
then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
and *: "0 < l \<or> u < 0"
-    by (cases "approx prec a vs", auto)
+    by (cases "approx prec a vs") auto
with approx[OF `bounded_by xs vs` approx_Some]
have "interpret_floatarith a xs \<noteq> 0" by auto
thus ?case using Inverse by auto
@@ -2797,7 +2815,7 @@
case (Ln a)
then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
and *: "0 < l"
-    by (cases "approx prec a vs", auto)
+    by (cases "approx prec a vs") auto
with approx[OF `bounded_by xs vs` approx_Some]
have "0 < interpret_floatarith a xs" by auto
thus ?case using Ln by auto
@@ -2805,46 +2823,49 @@
case (Sqrt a)
then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
and *: "0 < l"
-    by (cases "approx prec a vs", auto)
+    by (cases "approx prec a vs") auto
with approx[OF `bounded_by xs vs` approx_Some]
have "0 < interpret_floatarith a xs" by auto
thus ?case using Sqrt by auto
next
-  case (Power a n) thus ?case by (cases n, auto)
+  case (Power a n) thus ?case by (cases n) auto
qed auto

lemma bounded_by_update_var:
assumes "bounded_by xs vs" and "vs ! i = Some (l, u)"
-  and bnd: "x \<in> { real l .. real u }"
+    and bnd: "x \<in> { real l .. real u }"
shows "bounded_by (xs[i := x]) vs"
proof (cases "i < length xs")
-  case False thus ?thesis using `bounded_by xs vs` by auto
+  case False
+  thus ?thesis using `bounded_by xs vs` by auto
next
let ?xs = "xs[i := x]"
case True hence "i < length ?xs" by auto
-{ fix j
-  assume "j < length vs"
-  have "case vs ! j of None \<Rightarrow> True | Some (l, u) \<Rightarrow> ?xs ! j \<in> { real l .. real u }"
-  proof (cases "vs ! j")
-    case (Some b)
-    thus ?thesis
-    proof (cases "i = j")
-      case True
-      thus ?thesis using `vs ! i = Some (l, u)` Some and bnd `i < length ?xs`
-        by auto
-    next
-      case False
-      thus ?thesis using `bounded_by xs vs`[THEN bounded_byE, OF `j < length vs`] Some
-        by auto
-    qed
-  qed auto }
+  {
+    fix j
+    assume "j < length vs"
+    have "case vs ! j of None \<Rightarrow> True | Some (l, u) \<Rightarrow> ?xs ! j \<in> { real l .. real u }"
+    proof (cases "vs ! j")
+      case (Some b)
+      thus ?thesis
+      proof (cases "i = j")
+        case True
+        thus ?thesis using `vs ! i = Some (l, u)` Some and bnd `i < length ?xs`
+          by auto
+      next
+        case False
+        thus ?thesis
+          using `bounded_by xs vs`[THEN bounded_byE, OF `j < length vs`] Some by auto
+      qed
+    qed auto
+  }
thus ?thesis unfolding bounded_by_def by auto
qed

lemma isDERIV_approx':
assumes "bounded_by xs vs"
-  and vs_x: "vs ! x = Some (l, u)" and X_in: "X \<in> { real l .. real u }"
-  and approx: "isDERIV_approx prec x f vs"
+    and vs_x: "vs ! x = Some (l, u)" and X_in: "X \<in> { real l .. real u }"
+    and approx: "isDERIV_approx prec x f vs"
shows "isDERIV x f (xs[x := X])"
proof -
note bounded_by_update_var[OF `bounded_by xs vs` vs_x X_in] approx
@@ -2853,8 +2874,8 @@

lemma DERIV_approx:
assumes "n < length xs" and bnd: "bounded_by xs vs"
-  and isD: "isDERIV_approx prec n f vs"
-  and app: "Some (l, u) = approx prec (DERIV_floatarith n f) vs" (is "_ = approx _ ?D _")
+    and isD: "isDERIV_approx prec n f vs"
+    and app: "Some (l, u) = approx prec (DERIV_floatarith n f) vs" (is "_ = approx _ ?D _")
shows "\<exists>(x::real). l \<le> x \<and> x \<le> u \<and>
DERIV (\<lambda> x. interpret_floatarith f (xs[n := x])) (xs!n) :> x"
(is "\<exists> x. _ \<and> _ \<and> DERIV (?i f) _ :> _")
@@ -2867,17 +2888,19 @@
show "DERIV (?i f) (xs!n) :> (?i ?D (xs!n))" by simp
qed

-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
-"lift_bin (Some (l1, u1)) (Some (l2, u2)) f = f l1 u1 l2 u2" |
-"lift_bin a b f = None"
+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
+  "lift_bin (Some (l1, u1)) (Some (l2, u2)) f = f l1 u1 l2 u2"
+| "lift_bin a b f = None"

lemma lift_bin:
assumes lift_bin_Some: "Some (l, u) = lift_bin a b f"
obtains l1 u1 l2 u2
where "a = Some (l1, u1)"
-  and "b = Some (l2, u2)"
-  and "f l1 u1 l2 u2 = Some (l, u)"
-using assms by (cases a, simp, cases b, simp, auto)
+    and "b = Some (l2, u2)"
+    and "f l1 u1 l2 u2 = Some (l, u)"
+  using assms by (cases a, simp, cases b, simp, auto)

fun approx_tse where
"approx_tse prec n 0 c k f bs = approx prec f bs" |
@@ -2894,10 +2917,11 @@

lemma bounded_by_Cons:
assumes bnd: "bounded_by xs vs"
-  and x: "x \<in> { real l .. real u }"
+    and x: "x \<in> { real l .. real u }"
shows "bounded_by (x#xs) ((Some (l, u))#vs)"
proof -
-  { fix i assume *: "i < length ((Some (l, u))#vs)"
+  {
+    fix i assume *: "i < length ((Some (l, u))#vs)"
have "case ((Some (l,u))#vs) ! i of Some (l, u) \<Rightarrow> (x#xs)!i \<in> { real l .. real u } | None \<Rightarrow> True"
proof (cases i)
case 0 with x show ?thesis by auto
@@ -2905,15 +2929,16 @@
case (Suc i) with * have "i < length vs" by auto
from bnd[THEN bounded_byE, OF this]
show ?thesis unfolding Suc nth_Cons_Suc .
-    qed }
+    qed
+  }
thus ?thesis by (auto simp add: bounded_by_def)
qed

lemma approx_tse_generic:
assumes "bounded_by xs vs"
-  and bnd_c: "bounded_by (xs[x := c]) vs" and "x < length vs" and "x < length xs"
-  and bnd_x: "vs ! x = Some (lx, ux)"
-  and ate: "Some (l, u) = approx_tse prec x s c k f vs"
+    and bnd_c: "bounded_by (xs[x := c]) vs" and "x < length vs" and "x < length xs"
+    and bnd_x: "vs ! x = Some (lx, ux)"
+    and ate: "Some (l, u) = approx_tse prec x s c k f vs"
shows "\<exists> n. (\<forall> m < n. \<forall> (z::real) \<in> {lx .. ux}.
DERIV (\<lambda> y. interpret_floatarith ((DERIV_floatarith x ^^ m) f) (xs[x := y])) z :>
(interpret_floatarith ((DERIV_floatarith x ^^ (Suc m)) f) (xs[x := z])))
@@ -2925,36 +2950,39 @@
(xs!x - c)^n \<in> {l .. u})" (is "\<exists> n. ?taylor f k l u n")
using ate proof (induct s arbitrary: k f l u)
case 0
-  { fix t::real assume "t \<in> {lx .. ux}"
+  {
+    fix t::real assume "t \<in> {lx .. ux}"
note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
from approx[OF this 0[unfolded approx_tse.simps]]
have "(interpret_floatarith f (xs[x := t])) \<in> {l .. u}"
-  } thus ?case by (auto intro!: exI[of _ 0])
+  }
+  thus ?case by (auto intro!: exI[of _ 0])
next
case (Suc s)
show ?case
proof (cases "isDERIV_approx prec x f vs")
case False
note ap = Suc.prems[unfolded approx_tse.simps if_not_P[OF False]]
-
-    { fix t::real assume "t \<in> {lx .. ux}"
+    {
+      fix t::real assume "t \<in> {lx .. ux}"
note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
from approx[OF this ap]
have "(interpret_floatarith f (xs[x := t])) \<in> {l .. u}"
-    } thus ?thesis by (auto intro!: exI[of _ 0])
+    }
+    thus ?thesis by (auto intro!: exI[of _ 0])
next
case True
with Suc.prems
obtain l1 u1 l2 u2
where a: "Some (l1, u1) = approx prec f (vs[x := Some (c,c)])"
-      and ate: "Some (l2, u2) = approx_tse prec x s c (Suc k) (DERIV_floatarith x f) vs"
-      and final: "Some (l, u) = approx prec
-             (Mult (Inverse (Num (Float (int k) 0)))
-                   (Mult (Add (Var (Suc (Suc 0))) (Minus (Num c)))
-                         (Var (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
+        and ate: "Some (l2, u2) = approx_tse prec x s c (Suc k) (DERIV_floatarith x f) vs"
+        and final: "Some (l, u) = approx prec
+               (Mult (Inverse (Num (Float (int k) 0)))
+                     (Mult (Add (Var (Suc (Suc 0))) (Minus (Num c)))
+                           (Var (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
by (auto elim!: lift_bin) blast

from bnd_c `x < length xs`
@@ -2966,9 +2994,11 @@
(is "?f 0 (real c) \<in> _")
by auto

-    { fix f :: "'a \<Rightarrow> 'a" fix n :: nat fix x :: 'a
+    {
+      fix f :: "'a \<Rightarrow> 'a" fix n :: nat fix x :: 'a
have "(f ^^ Suc n) x = (f ^^ n) (f x)"
-        by (induct n, auto) }
+        by (induct n) auto
+    }
note funpow_Suc = this[symmetric]
from Suc.hyps[OF ate, unfolded this]
obtain n
@@ -2978,7 +3008,8 @@
(is "\<forall> t \<in> _. ?X (Suc k) f n t \<in> _")
by blast

-    { fix m and z::real
+    {
+      fix m and z::real
assume "m < Suc n" and bnd_z: "z \<in> { lx .. ux }"
have "DERIV (?f m) z :> ?f (Suc m) z"
proof (cases m)
@@ -2990,7 +3021,8 @@
hence "m' < n" using `m < Suc n` by auto
from DERIV_hyp[OF this bnd_z]
show ?thesis using Suc by simp
-      qed } note DERIV = this
+      qed
+    } note DERIV = this

have "\<And> k i. k < i \<Longrightarrow> {k ..< i} = insert k {Suc k ..< i}" by auto
hence setprod_head_Suc: "\<And> k i. \<Prod> {k ..< k + Suc i} = k * \<Prod> {Suc k ..< Suc k + i}" by auto
@@ -2999,7 +3031,8 @@
def C \<equiv> "xs!x - c"

-    { fix t::real assume t: "t \<in> {lx .. ux}"
+    {
+      fix t::real assume t: "t \<in> {lx .. ux}"
hence "bounded_by [xs!x] [vs!x]"
using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`]
by (cases "vs!x", auto simp add: bounded_by_def)
@@ -3016,24 +3049,28 @@
(simp only: mult_left_commute [of _ "inverse (real k)"] setsum_right_distrib [symmetric])
-      finally have "?T \<in> {l .. u}" . }
+      finally have "?T \<in> {l .. u}" .
+    }
thus ?thesis using DERIV by blast
qed
qed

lemma setprod_fact: "\<Prod> {1..<1 + k} = fact (k :: nat)"
proof (induct k)
+  case 0
+  show ?case by simp
+next
case (Suc k)
have "{ 1 ..< Suc (Suc k) } = insert (Suc k) { 1 ..< Suc k }" by auto
hence "\<Prod> { 1 ..< Suc (Suc k) } = (Suc k) * \<Prod> { 1 ..< Suc k }" by auto
thus ?case using Suc by auto
-qed simp
+qed

lemma approx_tse:
assumes "bounded_by xs vs"
-  and bnd_x: "vs ! x = Some (lx, ux)" and bnd_c: "real c \<in> {lx .. ux}"
-  and "x < length vs" and "x < length xs"
-  and ate: "Some (l, u) = approx_tse prec x s c 1 f vs"
+    and bnd_x: "vs ! x = Some (lx, ux)" and bnd_c: "real c \<in> {lx .. ux}"
+    and "x < length vs" and "x < length xs"
+    and ate: "Some (l, u) = approx_tse prec x s c 1 f vs"
shows "interpret_floatarith f xs \<in> { l .. u }"
proof -
def F \<equiv> "\<lambda> n z. interpret_floatarith ((DERIV_floatarith x ^^ n) f) (xs[x := z])"
@@ -3247,10 +3284,18 @@
case (Assign x a f') with assms
show ?thesis by (auto elim!: option_caseE simp add: f_def approx_tse_form_def)
qed } thus ?thesis unfolding f_def by auto
-next case Assign with assms show ?thesis by (auto simp add: approx_tse_form_def)
-next case LessEqual with assms show ?thesis by (auto simp add: approx_tse_form_def)
-next case Less with assms show ?thesis by (auto simp add: approx_tse_form_def)
-next case AtLeastAtMost with assms show ?thesis by (auto simp add: approx_tse_form_def)
+next
+  case Assign
+  with assms show ?thesis by (auto simp add: approx_tse_form_def)
+next
+  case LessEqual
+  with assms show ?thesis by (auto simp add: approx_tse_form_def)
+next
+  case Less
+  with assms show ?thesis by (auto simp add: approx_tse_form_def)
+next
+  case AtLeastAtMost
+  with assms show ?thesis by (auto simp add: approx_tse_form_def)
qed

text {* @{term approx_form_eval} is only used for the {\tt value}-command. *}```