[STATEMENT]
lemma deriv_rec_0_idem[simp]:
  shows "deriv_rec f 0 = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv_rec f 0 = f
[PROOF STEP]
by (cases "(f, 0::nat)" rule: deriv_rec.cases, simp_all)


[STATEMENT]
lemma tmf_c_correct:
  fixes A::"float interval list" and I::"float interval" and f::floatarith and a::"real list"
  assumes "a all_in A"
  assumes "tmf_c prec A f i = Some I"
  shows "interpret_floatarith (deriv_rec f i) a / fact i \<in>\<^sub>r I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (deriv_rec f i) a / fact i \<in>\<^sub>r I
[PROOF STEP]
using compute_bound_fa_correct[OF assms(2)[unfolded tmf_c.simps], where i="a"] assms(1)
[PROOF STATE]
proof (prove)
using this:
a all_in A \<Longrightarrow> interpret_floatarith (Mult (deriv_rec f i) (Inverse (Num (fact i)))) a \<in>\<^sub>r I
a all_in A

goal (1 subgoal):
 1. interpret_floatarith (deriv_rec f i) a / fact i \<in>\<^sub>r I
[PROOF STEP]
by (simp add: divide_real_def fact_real_float_equiv)


[STATEMENT]
lemma tmf_ivl_cs_length:
  assumes "tmf_ivl_cs prec n A a f = Some cs"
  shows "length cs = n + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length cs = n + 1
[PROOF STEP]
by (simp add: Some_those_length[OF assms[unfolded tmf_ivl_cs.simps]])


[STATEMENT]
lemma tmf_ivl_cs_correct:
  fixes A::"float interval list" and f::floatarith
  assumes "a all_in I"
  assumes "tmf_ivl_cs prec ord I a f = Some cs"
  shows "\<And>i. i < ord \<Longrightarrow> tmf_c prec (map interval_of a) f i = Some (cs!i)"
    and "tmf_c prec I f ord = Some (cs!ord)"
    and "length cs = Suc ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i < ord \<Longrightarrow> tmf_c prec (map interval_of a) f i = Some (cs ! i)) &&& tmf_c prec I f ord = Some (cs ! ord) &&& length cs = Suc ord
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. i < ord \<Longrightarrow> tmf_c prec (map interval_of a) f i = Some (cs ! i)
 2. tmf_c prec I f ord = Some (cs ! ord)
 3. length cs = Suc ord
[PROOF STEP]
from tmf_ivl_cs_length[OF assms(2)]
[PROOF STATE]
proof (chain)
picking this:
length cs = ord + 1
[PROOF STEP]
show "tmf_c prec I f ord = Some (cs!ord)"
[PROOF STATE]
proof (prove)
using this:
length cs = ord + 1

goal (1 subgoal):
 1. tmf_c prec I f ord = Some (cs ! ord)
[PROOF STEP]
by (metis Some_those_nth assms(2) diff_zero length_map length_upt less_add_one
        nth_append_length tmf_ivl_cs.simps)
[PROOF STATE]
proof (state)
this:
tmf_c prec I f ord = Some (cs ! ord)

goal (2 subgoals):
 1. \<And>i. i < ord \<Longrightarrow> tmf_c prec (map interval_of a) f i = Some (cs ! i)
 2. length cs = Suc ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < ord \<Longrightarrow> tmf_c prec (map interval_of a) f i = Some (cs ! i)
 2. length cs = Suc ord
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < ord \<Longrightarrow> tmf_c prec (map interval_of a) f i = Some (cs ! i)
 2. length cs = Suc ord
[PROOF STEP]
assume "i < ord"
[PROOF STATE]
proof (state)
this:
i < ord

goal (2 subgoals):
 1. \<And>i. i < ord \<Longrightarrow> tmf_c prec (map interval_of a) f i = Some (cs ! i)
 2. length cs = Suc ord
[PROOF STEP]
have "Some (cs!i) = (map (tmf_c prec a f) [0..<ord] @ [tmf_c prec I f ord]) ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (cs ! i) = (map (tmf_c prec (map interval_of a) f) [0..<ord] @ [tmf_c prec I f ord]) ! i
[PROOF STEP]
apply(rule Some_those_nth)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. those (map (tmf_c prec (map interval_of a) f) [0..<ord] @ [tmf_c prec I f ord]) = Some cs
 2. i < length cs
[PROOF STEP]
using assms(2) tmf_ivl_cs_length \<open>i < ord\<close>
[PROOF STATE]
proof (prove)
using this:
tmf_ivl_cs prec ord I a f = Some cs
tmf_ivl_cs ?prec ?n ?A ?a ?f = Some ?cs \<Longrightarrow> length ?cs = ?n + 1
i < ord

goal (2 subgoals):
 1. those (map (tmf_c prec (map interval_of a) f) [0..<ord] @ [tmf_c prec I f ord]) = Some cs
 2. i < length cs
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Some (cs ! i) = (map (tmf_c prec (map interval_of a) f) [0..<ord] @ [tmf_c prec I f ord]) ! i

goal (2 subgoals):
 1. \<And>i. i < ord \<Longrightarrow> tmf_c prec (map interval_of a) f i = Some (cs ! i)
 2. length cs = Suc ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some (cs ! i) = (map (tmf_c prec (map interval_of a) f) [0..<ord] @ [tmf_c prec I f ord]) ! i
[PROOF STEP]
show "tmf_c prec a f i = Some (cs!i)"
[PROOF STATE]
proof (prove)
using this:
Some (cs ! i) = (map (tmf_c prec (map interval_of a) f) [0..<ord] @ [tmf_c prec I f ord]) ! i

goal (1 subgoal):
 1. tmf_c prec (map interval_of a) f i = Some (cs ! i)
[PROOF STEP]
using \<open>i < ord\<close>
[PROOF STATE]
proof (prove)
using this:
Some (cs ! i) = (map (tmf_c prec (map interval_of a) f) [0..<ord] @ [tmf_c prec I f ord]) ! i
i < ord

goal (1 subgoal):
 1. tmf_c prec (map interval_of a) f i = Some (cs ! i)
[PROOF STEP]
by (simp add: nth_append)
[PROOF STATE]
proof (state)
this:
tmf_c prec (map interval_of a) f i = Some (cs ! i)

goal (1 subgoal):
 1. length cs = Suc ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length cs = Suc ord
[PROOF STEP]
show "length cs = Suc ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length cs = Suc ord
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
map real_of_float a all_in I
tmf_ivl_cs prec ord I a f = Some cs

goal (1 subgoal):
 1. length cs = Suc ord
[PROOF STEP]
by (auto simp: split_beta' those_eq_Some_iff list_eq_iff_nth_eq)
[PROOF STATE]
proof (state)
this:
length cs = Suc ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Ipoly_fst_tmf_polys:
  "Ipoly xs (fst (tmf_polys z)) = (\<Sum>i<length z. xs ! 0 ^ i * (mid (z ! i)))"
  for xs::"real list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float (fst (tmf_polys z))) = (\<Sum>i<length z. xs ! 0 ^ i * real_of_float (mid (z ! i)))
[PROOF STEP]
proof (induction z)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ipoly xs (map_poly real_of_float (fst (tmf_polys []))) = (\<Sum>i<length []. xs ! 0 ^ i * real_of_float (mid ([] ! i)))
 2. \<And>a z. Ipoly xs (map_poly real_of_float (fst (tmf_polys z))) = (\<Sum>i<length z. xs ! 0 ^ i * real_of_float (mid (z ! i))) \<Longrightarrow> Ipoly xs (map_poly real_of_float (fst (tmf_polys (a # z)))) = (\<Sum>i<length (a # z). xs ! 0 ^ i * real_of_float (mid ((a # z) ! i)))
[PROOF STEP]
case (Cons z zs)
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float (fst (tmf_polys zs))) = (\<Sum>i<length zs. xs ! 0 ^ i * real_of_float (mid (zs ! i)))

goal (2 subgoals):
 1. Ipoly xs (map_poly real_of_float (fst (tmf_polys []))) = (\<Sum>i<length []. xs ! 0 ^ i * real_of_float (mid ([] ! i)))
 2. \<And>a z. Ipoly xs (map_poly real_of_float (fst (tmf_polys z))) = (\<Sum>i<length z. xs ! 0 ^ i * real_of_float (mid (z ! i))) \<Longrightarrow> Ipoly xs (map_poly real_of_float (fst (tmf_polys (a # z)))) = (\<Sum>i<length (a # z). xs ! 0 ^ i * real_of_float (mid ((a # z) ! i)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float (fst (tmf_polys (z # zs)))) = (\<Sum>i<length (z # zs). xs ! 0 ^ i * real_of_float (mid ((z # zs) ! i)))
[PROOF STEP]
unfolding list.size add_Suc_right sum.lessThan_Suc_shift
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float (fst (tmf_polys (z # zs)))) = xs ! 0 ^ 0 * real_of_float (mid ((z # zs) ! 0)) + (\<Sum>i<length zs + 0. xs ! 0 ^ Suc i * real_of_float (mid ((z # zs) ! Suc i)))
[PROOF STEP]
by (auto simp: split_beta' Let_def nth_Cons Cons sum_distrib_left ac_simps)
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float (fst (tmf_polys (z # zs)))) = (\<Sum>i<length (z # zs). xs ! 0 ^ i * real_of_float (mid ((z # zs) ! i)))

goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float (fst (tmf_polys []))) = (\<Sum>i<length []. xs ! 0 ^ i * real_of_float (mid ([] ! i)))
[PROOF STEP]
qed simp


[STATEMENT]
lemma insertion_fst_tmf_polys:
  "insertion e (fst (tmf_polys z)) = (\<Sum>i<length z. e 0 ^ i * (mid (z ! i)))"
  for e::"nat \<Rightarrow> real"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (map_poly real_of_float (fst (tmf_polys z))) = (\<Sum>i<length z. e 0 ^ i * real_of_float (mid (z ! i)))
[PROOF STEP]
proof (induction z)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. insertion e (map_poly real_of_float (fst (tmf_polys []))) = (\<Sum>i<length []. e 0 ^ i * real_of_float (mid ([] ! i)))
 2. \<And>a z. insertion e (map_poly real_of_float (fst (tmf_polys z))) = (\<Sum>i<length z. e 0 ^ i * real_of_float (mid (z ! i))) \<Longrightarrow> insertion e (map_poly real_of_float (fst (tmf_polys (a # z)))) = (\<Sum>i<length (a # z). e 0 ^ i * real_of_float (mid ((a # z) ! i)))
[PROOF STEP]
case (Cons z zs)
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (fst (tmf_polys zs))) = (\<Sum>i<length zs. e 0 ^ i * real_of_float (mid (zs ! i)))

goal (2 subgoals):
 1. insertion e (map_poly real_of_float (fst (tmf_polys []))) = (\<Sum>i<length []. e 0 ^ i * real_of_float (mid ([] ! i)))
 2. \<And>a z. insertion e (map_poly real_of_float (fst (tmf_polys z))) = (\<Sum>i<length z. e 0 ^ i * real_of_float (mid (z ! i))) \<Longrightarrow> insertion e (map_poly real_of_float (fst (tmf_polys (a # z)))) = (\<Sum>i<length (a # z). e 0 ^ i * real_of_float (mid ((a # z) ! i)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (map_poly real_of_float (fst (tmf_polys (z # zs)))) = (\<Sum>i<length (z # zs). e 0 ^ i * real_of_float (mid ((z # zs) ! i)))
[PROOF STEP]
unfolding list.size add_Suc_right sum.lessThan_Suc_shift
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (map_poly real_of_float (fst (tmf_polys (z # zs)))) = e 0 ^ 0 * real_of_float (mid ((z # zs) ! 0)) + (\<Sum>i<length zs + 0. e 0 ^ Suc i * real_of_float (mid ((z # zs) ! Suc i)))
[PROOF STEP]
by (auto simp: split_beta' Let_def nth_Cons Cons sum_distrib_left ac_simps)
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (fst (tmf_polys (z # zs)))) = (\<Sum>i<length (z # zs). e 0 ^ i * real_of_float (mid ((z # zs) ! i)))

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (fst (tmf_polys []))) = (\<Sum>i<length []. e 0 ^ i * real_of_float (mid ([] ! i)))
[PROOF STEP]
qed simp


[STATEMENT]
lemma Ipoly_snd_tmf_polys:
  "set_of (horner_eval (real_interval o centered o nth z) x (length z)) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys z))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (horner_eval (real_interval \<circ> centered \<circ> (!) z) x (length z)) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys z))))
[PROOF STEP]
proof (induction z)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set_of (horner_eval (real_interval \<circ> centered \<circ> (!) []) x (length [])) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys []))))
 2. \<And>a z. set_of (horner_eval (real_interval \<circ> centered \<circ> (!) z) x (length z)) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys z)))) \<Longrightarrow> set_of (horner_eval (real_interval \<circ> centered \<circ> (!) (a # z)) x (length (a # z))) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys (a # z)))))
[PROOF STEP]
case (Cons z zs)
[PROOF STATE]
proof (state)
this:
set_of (horner_eval (real_interval \<circ> centered \<circ> (!) zs) x (length zs)) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys zs))))

goal (2 subgoals):
 1. set_of (horner_eval (real_interval \<circ> centered \<circ> (!) []) x (length [])) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys []))))
 2. \<And>a z. set_of (horner_eval (real_interval \<circ> centered \<circ> (!) z) x (length z)) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys z)))) \<Longrightarrow> set_of (horner_eval (real_interval \<circ> centered \<circ> (!) (a # z)) x (length (a # z))) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys (a # z)))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (horner_eval (real_interval \<circ> centered \<circ> (!) (z # zs)) x (length (z # zs))) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys (z # zs)))))
[PROOF STEP]
using Cons[THEN set_of_mul_inc_right]
[PROOF STATE]
proof (prove)
using this:
set_of (?A * horner_eval (real_interval \<circ> centered \<circ> (!) zs) x (length zs)) \<subseteq> set_of (?A * Ipoly [x] (map_poly real_interval (snd (tmf_polys zs))))

goal (1 subgoal):
 1. set_of (horner_eval (real_interval \<circ> centered \<circ> (!) (z # zs)) x (length (z # zs))) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys (z # zs)))))
[PROOF STEP]
unfolding list.size add_Suc_right sum.lessThan_Suc_shift
[PROOF STATE]
proof (prove)
using this:
set_of (?A * horner_eval (real_interval \<circ> centered \<circ> (!) zs) x (length zs)) \<subseteq> set_of (?A * Ipoly [x] (map_poly real_interval (snd (tmf_polys zs))))

goal (1 subgoal):
 1. set_of (horner_eval (real_interval \<circ> centered \<circ> (!) (z # zs)) x (Suc (length zs + 0))) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys (z # zs)))))
[PROOF STEP]
by (auto simp: split_beta' Let_def nth_Cons sum_distrib_left ac_simps
        elim!: plus_in_intervalE intro!: plus_in_intervalI)
[PROOF STATE]
proof (state)
this:
set_of (horner_eval (real_interval \<circ> centered \<circ> (!) (z # zs)) x (length (z # zs))) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys (z # zs)))))

goal (1 subgoal):
 1. set_of (horner_eval (real_interval \<circ> centered \<circ> (!) []) x (length [])) \<subseteq> set_of (Ipoly [x] (map_poly real_interval (snd (tmf_polys []))))
[PROOF STEP]
qed (auto simp: real_interval_zero)


[STATEMENT]
lemma zero_interval[intro,simp]: "0 \<in>\<^sub>i 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<in>\<^sub>i 0
[PROOF STEP]
by (simp add: set_of_eq)


[STATEMENT]
lemma sum_in_intervalI: "sum f X \<in>\<^sub>i sum g X" if "\<And>x. x \<in> X \<Longrightarrow> f x \<in>\<^sub>i g x"
  for f :: "_ \<Rightarrow> 'a :: ordered_comm_monoid_add"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f X \<in>\<^sub>i sum g X
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?x \<in> X \<Longrightarrow> f ?x \<in>\<^sub>i g ?x

goal (1 subgoal):
 1. sum f X \<in>\<^sub>i sum g X
[PROOF STEP]
proof (induction X rule: infinite_finite_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x. x \<in> A \<Longrightarrow> f x \<in>\<^sub>i g x\<rbrakk> \<Longrightarrow> sum f A \<in>\<^sub>i sum g A
 2. (\<And>x. x \<in> {} \<Longrightarrow> f x \<in>\<^sub>i g x) \<Longrightarrow> sum f {} \<in>\<^sub>i sum g {}
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in>\<^sub>i g x) \<Longrightarrow> sum f F \<in>\<^sub>i sum g F; \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in>\<^sub>i g xa\<rbrakk> \<Longrightarrow> sum f (insert x F) \<in>\<^sub>i sum g (insert x F)
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> f x \<in>\<^sub>i g x) \<Longrightarrow> sum f F \<in>\<^sub>i sum g F
?x \<in> insert x F \<Longrightarrow> f ?x \<in>\<^sub>i g ?x

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x. x \<in> A \<Longrightarrow> f x \<in>\<^sub>i g x\<rbrakk> \<Longrightarrow> sum f A \<in>\<^sub>i sum g A
 2. (\<And>x. x \<in> {} \<Longrightarrow> f x \<in>\<^sub>i g x) \<Longrightarrow> sum f {} \<in>\<^sub>i sum g {}
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in>\<^sub>i g x) \<Longrightarrow> sum f F \<in>\<^sub>i sum g F; \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in>\<^sub>i g xa\<rbrakk> \<Longrightarrow> sum f (insert x F) \<in>\<^sub>i sum g (insert x F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> f x \<in>\<^sub>i g x) \<Longrightarrow> sum f F \<in>\<^sub>i sum g F
?x \<in> insert x F \<Longrightarrow> f ?x \<in>\<^sub>i g ?x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> f x \<in>\<^sub>i g x) \<Longrightarrow> sum f F \<in>\<^sub>i sum g F
?x \<in> insert x F \<Longrightarrow> f ?x \<in>\<^sub>i g ?x

goal (1 subgoal):
 1. sum f (insert x F) \<in>\<^sub>i sum g (insert x F)
[PROOF STEP]
by (auto intro!: plus_in_intervalI)
[PROOF STATE]
proof (state)
this:
sum f (insert x F) \<in>\<^sub>i sum g (insert x F)

goal (2 subgoals):
 1. \<And>A. \<lbrakk>infinite A; \<And>x. x \<in> A \<Longrightarrow> f x \<in>\<^sub>i g x\<rbrakk> \<Longrightarrow> sum f A \<in>\<^sub>i sum g A
 2. (\<And>x. x \<in> {} \<Longrightarrow> f x \<in>\<^sub>i g x) \<Longrightarrow> sum f {} \<in>\<^sub>i sum g {}
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma set_of_sum_subset: "set_of (sum f X) \<subseteq> set_of (sum g X)"
  if "\<And>x. x \<in> X \<Longrightarrow> set_of (f x) \<subseteq> set_of (g x)"
  for f :: "_\<Rightarrow>'a::linordered_ab_group_add interval"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (sum f X) \<subseteq> set_of (sum g X)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?x \<in> X \<Longrightarrow> set_of (f ?x) \<subseteq> set_of (g ?x)

goal (1 subgoal):
 1. set_of (sum f X) \<subseteq> set_of (sum g X)
[PROOF STEP]
by (induction X rule: infinite_finite_induct) (simp_all add: set_of_add_inc)


[STATEMENT]
lemma interval_of_plus: "interval_of (a + b) = interval_of a + interval_of b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interval_of (a + b) = interval_of a + interval_of b
[PROOF STEP]
by (simp add: interval_eqI)


[STATEMENT]
lemma interval_of_uminus: "interval_of (- a) = - interval_of a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interval_of (- a) = - interval_of a
[PROOF STEP]
by (simp add: interval_eqI)


[STATEMENT]
lemma interval_of_zero: "interval_of 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interval_of (0::'a) = 0
[PROOF STEP]
by (simp add: interval_eqI)


[STATEMENT]
lemma interval_of_sum: "interval_of (sum f X) = sum (\<lambda>x. interval_of (f x)) X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interval_of (sum f X) = (\<Sum>x\<in>X. interval_of (f x))
[PROOF STEP]
by (induction X rule: infinite_finite_induct) (auto simp: interval_of_plus interval_of_zero)


[STATEMENT]
lemma interval_of_prod: "interval_of (a * b) = interval_of a * interval_of b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interval_of (a * b) = interval_of a * interval_of b
[PROOF STEP]
by (simp add: lower_times upper_times interval_eqI)


[STATEMENT]
lemma in_set_of_interval_of[simp]: "x \<in>\<^sub>i (interval_of y) \<longleftrightarrow> x = y" for x y::"'a::order"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in>\<^sub>i interval_of y) = (x = y)
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
lemma real_interval_Ipoly: "real_interval (Ipoly xs p) = Ipoly (map real_interval xs) (map_poly real_interval p)"
  if "num_params p \<le> length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_interval (Ipoly xs p) = Ipoly (map real_interval xs) (map_poly real_interval p)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
num_params p \<le> length xs

goal (1 subgoal):
 1. real_interval (Ipoly xs p) = Ipoly (map real_interval xs) (map_poly real_interval p)
[PROOF STEP]
by (induction p)
    (auto simp: real_interval_plus real_interval_minus real_interval_times
      real_interval_uminus real_interval_power)


[STATEMENT]
lemma num_params_tmf_polys1: "num_params (fst (tmf_polys z)) \<le> Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (fst (tmf_polys z)) \<le> Suc 0
[PROOF STEP]
by (induction z) (auto simp: split_beta' Let_def)


[STATEMENT]
lemma num_params_tmf_polys2: "num_params (snd (tmf_polys z)) \<le> Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (snd (tmf_polys z)) \<le> Suc 0
[PROOF STEP]
by (induction z) (auto simp: split_beta' Let_def)


[STATEMENT]
lemma set_of_real_interval_subset: "set_of (real_interval x) \<subseteq> set_of (real_interval y)"
  if "set_of x \<subseteq> set_of y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (real_interval x) \<subseteq> set_of (real_interval y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
set_of x \<subseteq> set_of y

goal (1 subgoal):
 1. set_of (real_interval x) \<subseteq> set_of (real_interval y)
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
theorem tm_floatarith:
  assumes t: "tm_floatarith prec ord I xs f = Some t"
  assumes a: "xs all_in I" and x: "x \<in>\<^sub>r I ! 0"
  assumes xs_ne: "xs \<noteq> []"
  assumes deriv: "\<And>x. x \<in>\<^sub>r I ! 0 \<Longrightarrow> isDERIV 0 f (xs[0 := x])"
  assumes "\<And>i. 0 < i \<Longrightarrow> i < length xs \<Longrightarrow> e i = real_of_float (xs ! i)"
  assumes diff_e: "(x - real_of_float (xs ! 0)) = e 0"
  shows "interpret_floatarith f (xs[0:=x]) \<in>\<^sub>i range_tm e t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
from xs_ne a
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
map real_of_float xs all_in I
[PROOF STEP]
have I_ne[simp]: "I \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
map real_of_float xs all_in I

goal (1 subgoal):
 1. I \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I \<noteq> []

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have xs'_in: "xs[0 := x] all_in I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map real_of_float xs)[0 := x] all_in I
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
map real_of_float xs all_in I

goal (1 subgoal):
 1. (map real_of_float xs)[0 := x] all_in I
[PROOF STEP]
by (auto simp: nth_list_update x)
[PROOF STATE]
proof (state)
this:
(map real_of_float xs)[0 := x] all_in I

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
from t
[PROOF STATE]
proof (chain)
picking this:
tm_floatarith prec ord I xs f = Some t
[PROOF STEP]
obtain z where z: "tmf_ivl_cs prec ord I xs f = Some z"
    and tz: "tm_poly t = fst (tmf_polys z)"
    and tb: "tm_bound t = round_interval prec (Ipoly (List.map2 (-) I xs) (snd (tmf_polys z)))"
[PROOF STATE]
proof (prove)
using this:
tm_floatarith prec ord I xs f = Some t

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>tmf_ivl_cs prec ord I xs f = Some z; tm_poly t = fst (tmf_polys z); tm_bound t = round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
tm_floatarith prec ord I xs f = Some t
tm_floatarith prec ord I xs f = Some t

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>tmf_ivl_cs prec ord I xs f = Some z; tm_poly t = fst (tmf_polys z); tm_bound t = round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases t) (auto simp: those_eq_Some_iff split_beta' Let_def simp del: tmf_ivl_cs.simps)
[PROOF STATE]
proof (state)
this:
tmf_ivl_cs prec ord I xs f = Some z
tm_poly t = fst (tmf_polys z)
tm_bound t = round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
from tmf_ivl_cs_correct[OF a z(1)]
[PROOF STATE]
proof (chain)
picking this:
?i < ord \<Longrightarrow> tmf_c prec (map interval_of xs) f ?i = Some (z ! ?i)
tmf_c prec I f ord = Some (z ! ord)
length z = Suc ord
[PROOF STEP]
have z_less: "i < ord \<Longrightarrow> tmf_c prec (map interval_of xs) f i = Some (z ! i)"
    and lz: "length z = Suc ord" "length z - 1 = ord"
    and z_ord: "tmf_c prec I f ord = Some (z ! ord)" for i
[PROOF STATE]
proof (prove)
using this:
?i < ord \<Longrightarrow> tmf_c prec (map interval_of xs) f ?i = Some (z ! ?i)
tmf_c prec I f ord = Some (z ! ord)
length z = Suc ord

goal (1 subgoal):
 1. (i < ord \<Longrightarrow> tmf_c prec (map interval_of xs) f i = Some (z ! i)) &&& (length z = Suc ord &&& length z - 1 = ord) &&& tmf_c prec I f ord = Some (z ! ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < ord \<Longrightarrow> tmf_c prec (map interval_of xs) f ?i = Some (z ! ?i)
length z = Suc ord
length z - 1 = ord
tmf_c prec I f ord = Some (z ! ord)

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have rewr: "{..ord} = insert ord {..<ord}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..ord} = insert ord {..<ord}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{..ord} = insert ord {..<ord}

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
let ?diff = "\<lambda>(i::nat) (x::real). interpret_floatarith (deriv_rec f i) (xs[0:=x])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
let ?c = "real_of_float (xs ! 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
let ?n = "ord"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
let ?a = "real_of_float (lower (I!0))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
let ?b = "real_of_float (upper (I!0))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
let ?x = "x::real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
let ?f = "\<lambda>x::real. interpret_floatarith f (xs[0 := x])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have 2: "?diff 0 = ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. interpret_floatarith (deriv_rec f 0) ((map real_of_float xs)[0 := x])) = (\<lambda>x. interpret_floatarith f ((map real_of_float xs)[0 := x]))
[PROOF STEP]
using \<open>xs \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

goal (1 subgoal):
 1. (\<lambda>x. interpret_floatarith (deriv_rec f 0) ((map real_of_float xs)[0 := x])) = (\<lambda>x. interpret_floatarith f ((map real_of_float xs)[0 := x]))
[PROOF STEP]
by (simp add: map_update)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. interpret_floatarith (deriv_rec f 0) ((map real_of_float xs)[0 := x])) = (\<lambda>x. interpret_floatarith f ((map real_of_float xs)[0 := x]))

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have 3: "\<forall>m t. m < ?n \<and> ?a \<le> t \<and> t \<le> ?b \<longrightarrow> (?diff m has_real_derivative ?diff (Suc m) t) (at t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m t. m < ord \<and> real_of_float (lower (I ! 0)) \<le> t \<and> t \<le> real_of_float (upper (I ! 0)) \<longrightarrow> ((\<lambda>x. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := x])) has_real_derivative interpret_floatarith (deriv_rec f (Suc m)) ((map real_of_float xs)[0 := t])) (at t)
[PROOF STEP]
by (auto intro!: derivative_eq_intros deriv_rec_correct deriv simp: set_of_eq xs_ne)
[PROOF STATE]
proof (state)
this:
\<forall>m t. m < ord \<and> real_of_float (lower (I ! 0)) \<le> t \<and> t \<le> real_of_float (upper (I ! 0)) \<longrightarrow> ((\<lambda>x. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := x])) has_real_derivative interpret_floatarith (deriv_rec f (Suc m)) ((map real_of_float xs)[0 := t])) (at t)

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have 4: "?a \<le> ?c" "?c \<le> ?b"  "?a \<le> ?x" "?x \<le> ?b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (real_of_float (lower (I ! 0)) \<le> real_of_float (xs ! 0) &&& real_of_float (xs ! 0) \<le> real_of_float (upper (I ! 0))) &&& real_of_float (lower (I ! 0)) \<le> x &&& x \<le> real_of_float (upper (I ! 0))
[PROOF STEP]
using a xs_ne x
[PROOF STATE]
proof (prove)
using this:
map real_of_float xs all_in I
xs \<noteq> []
x \<in>\<^sub>r I ! 0

goal (1 subgoal):
 1. (real_of_float (lower (I ! 0)) \<le> real_of_float (xs ! 0) &&& real_of_float (xs ! 0) \<le> real_of_float (upper (I ! 0))) &&& real_of_float (lower (I ! 0)) \<le> x &&& x \<le> real_of_float (upper (I ! 0))
[PROOF STEP]
by (force simp: set_of_eq)+
[PROOF STATE]
proof (state)
this:
real_of_float (lower (I ! 0)) \<le> real_of_float (xs ! 0)
real_of_float (xs ! 0) \<le> real_of_float (upper (I ! 0))
real_of_float (lower (I ! 0)) \<le> x
x \<le> real_of_float (upper (I ! 0))

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
define cr where "cr \<equiv> \<lambda>s m. if m < ord then ?diff m ?c / fact m - mid (z ! m)
                           else ?diff m s / fact ord - mid (z ! ord)"
[PROOF STATE]
proof (state)
this:
cr \<equiv> \<lambda>s m. if m < ord then interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m - real_of_float (mid (z ! m)) else interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := s]) / fact ord - real_of_float (mid (z ! ord))

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
define ci where "ci \<equiv> \<lambda>i. real_interval (z ! i) - interval_of (real_of_float (mid (z ! i)))"
[PROOF STATE]
proof (state)
this:
ci \<equiv> \<lambda>i. real_interval (z ! i) - interval_of (real_of_float (mid (z ! i)))

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have cr_ord: "cr x ord \<in>\<^sub>i ci ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr x ord \<in>\<^sub>i ci ord
[PROOF STEP]
using tmf_c_correct[OF xs'_in z_ord]
[PROOF STATE]
proof (prove)
using this:
interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := x]) / fact ord \<in>\<^sub>r z ! ord

goal (1 subgoal):
 1. cr x ord \<in>\<^sub>i ci ord
[PROOF STEP]
by (auto simp: ci_def set_of_eq cr_def)
[PROOF STATE]
proof (state)
this:
cr x ord \<in>\<^sub>i ci ord

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have enclosure: "(\<Sum>m<ord. cr s m * (x - (xs ! 0)) ^ m) + cr s ord * (x - (xs ! 0)) ^ ord
      \<in>\<^sub>r round_interval prec (Ipoly (List.map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))"
    if cr_ord: "cr s ord \<in>\<^sub>i ci ord" for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
have "(\<Sum>m<ord. cr s m  * (x - xs!0) ^ m) + cr s ord * (x - xs!0) ^ ord =
        horner_eval (cr s) (x - xs!0) (Suc ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord = horner_eval (cr s) (x - real_of_float (xs ! 0)) (Suc ord)
[PROOF STEP]
by (simp add: horner_eval_eq_setsum)
[PROOF STATE]
proof (state)
this:
(\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord = horner_eval (cr s) (x - real_of_float (xs ! 0)) (Suc ord)

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord = horner_eval (cr s) (x - real_of_float (xs ! 0)) (Suc ord)

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
have "\<dots> \<in>\<^sub>i horner_eval ci (real_interval (I ! 0 - xs ! 0)) (Suc ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horner_eval (cr s) (x - real_of_float (xs ! 0)) (Suc ord) \<in>\<^sub>i horner_eval ci (real_interval (I ! 0 - interval_of (xs ! 0))) (Suc ord)
[PROOF STEP]
proof (rule horner_eval_interval)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < Suc ord \<Longrightarrow> cr s i \<in>\<^sub>i ci i
 2. x - real_of_float (xs ! 0) \<in>\<^sub>r I ! 0 - interval_of (xs ! 0)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < Suc ord \<Longrightarrow> cr s i \<in>\<^sub>i ci i
 2. x - real_of_float (xs ! 0) \<in>\<^sub>r I ! 0 - interval_of (xs ! 0)
[PROOF STEP]
assume "i < Suc ord"
[PROOF STATE]
proof (state)
this:
i < Suc ord

goal (2 subgoals):
 1. \<And>i. i < Suc ord \<Longrightarrow> cr s i \<in>\<^sub>i ci i
 2. x - real_of_float (xs ! 0) \<in>\<^sub>r I ! 0 - interval_of (xs ! 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < Suc ord
[PROOF STEP]
consider "i < ord" | "i = ord"
[PROOF STATE]
proof (prove)
using this:
i < Suc ord

goal (1 subgoal):
 1. \<lbrakk>i < ord \<Longrightarrow> thesis; i = ord \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < ord \<Longrightarrow> ?thesis; i = ord \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. \<And>i. i < Suc ord \<Longrightarrow> cr s i \<in>\<^sub>i ci i
 2. x - real_of_float (xs ! 0) \<in>\<^sub>r I ! 0 - interval_of (xs ! 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i < ord \<Longrightarrow> ?thesis; i = ord \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "cr s i \<in>\<^sub>i ci i"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < ord \<Longrightarrow> ?thesis; i = ord \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. cr s i \<in>\<^sub>i ci i
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < ord \<Longrightarrow> cr s i \<in>\<^sub>i ci i
 2. i = ord \<Longrightarrow> cr s i \<in>\<^sub>i ci i
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
i < ord

goal (2 subgoals):
 1. i < ord \<Longrightarrow> cr s i \<in>\<^sub>i ci i
 2. i = ord \<Longrightarrow> cr s i \<in>\<^sub>i ci i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i < ord

goal (1 subgoal):
 1. cr s i \<in>\<^sub>i ci i
[PROOF STEP]
by (auto simp: cr_def ci_def not_less less_Suc_eq_le
              intro!: minus_in_intervalI tmf_c_correct[OF _ z_less])
            (metis in_set_of_interval_of list_update_id map_update nth_map real_interval_of)
[PROOF STATE]
proof (state)
this:
cr s i \<in>\<^sub>i ci i

goal (1 subgoal):
 1. i = ord \<Longrightarrow> cr s i \<in>\<^sub>i ci i
[PROOF STEP]
qed (simp add: cr_ord)
[PROOF STATE]
proof (state)
this:
cr s i \<in>\<^sub>i ci i

goal (1 subgoal):
 1. x - real_of_float (xs ! 0) \<in>\<^sub>r I ! 0 - interval_of (xs ! 0)
[PROOF STEP]
qed (auto intro!: minus_in_intervalI simp: real_interval_minus x)
[PROOF STATE]
proof (state)
this:
horner_eval (cr s) (x - real_of_float (xs ! 0)) (Suc ord) \<in>\<^sub>i horner_eval ci (real_interval (I ! 0 - interval_of (xs ! 0))) (Suc ord)

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
horner_eval (cr s) (x - real_of_float (xs ! 0)) (Suc ord) \<in>\<^sub>i horner_eval ci (real_interval (I ! 0 - interval_of (xs ! 0))) (Suc ord)

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
have "\<dots> = set_of (horner_eval (real_interval o centered \<circ> (!) z)
      (real_interval (I ! 0 - xs ! 0)) (length z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (horner_eval ci (real_interval (I ! 0 - interval_of (xs ! 0))) (Suc ord)) = set_of (horner_eval (real_interval \<circ> centered \<circ> (!) z) (real_interval (I ! 0 - interval_of (xs ! 0))) (length z))
[PROOF STEP]
by (auto simp: ci_def centered_def real_interval_minus real_interval_of lz)
[PROOF STATE]
proof (state)
this:
set_of (horner_eval ci (real_interval (I ! 0 - interval_of (xs ! 0))) (Suc ord)) = set_of (horner_eval (real_interval \<circ> centered \<circ> (!) z) (real_interval (I ! 0 - interval_of (xs ! 0))) (length z))

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_of (horner_eval ci (real_interval (I ! 0 - interval_of (xs ! 0))) (Suc ord)) = set_of (horner_eval (real_interval \<circ> centered \<circ> (!) z) (real_interval (I ! 0 - interval_of (xs ! 0))) (length z))

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
have "\<dots> \<subseteq> set_of (Ipoly [real_interval (I ! 0 - xs ! 0)]
        (map_poly real_interval (snd (tmf_polys z))))"
      (is "_ \<subseteq> set_of ?x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (horner_eval (real_interval \<circ> centered \<circ> (!) z) (real_interval (I ! 0 - interval_of (xs ! 0))) (length z)) \<subseteq> set_of (Ipoly [real_interval (I ! 0 - interval_of (xs ! 0))] (map_poly real_interval (snd (tmf_polys z))))
[PROOF STEP]
by (rule Ipoly_snd_tmf_polys)
[PROOF STATE]
proof (state)
this:
set_of (horner_eval (real_interval \<circ> centered \<circ> (!) z) (real_interval (I ! 0 - interval_of (xs ! 0))) (length z)) \<subseteq> set_of (Ipoly [real_interval (I ! 0 - interval_of (xs ! 0))] (map_poly real_interval (snd (tmf_polys z))))

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_of (horner_eval (real_interval \<circ> centered \<circ> (!) z) (real_interval (I ! 0 - interval_of (xs ! 0))) (length z)) \<subseteq> set_of (Ipoly [real_interval (I ! 0 - interval_of (xs ! 0))] (map_poly real_interval (snd (tmf_polys z))))

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
have "\<dots> = set_of (real_interval (Ipoly [(I ! 0 - xs ! 0)] (snd (tmf_polys z))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (Ipoly [real_interval (I ! 0 - interval_of (xs ! 0))] (map_poly real_interval (snd (tmf_polys z)))) = set_of (real_interval (Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z))))
[PROOF STEP]
by (auto simp: real_interval_Ipoly num_params_tmf_polys2)
[PROOF STATE]
proof (state)
this:
set_of (Ipoly [real_interval (I ! 0 - interval_of (xs ! 0))] (map_poly real_interval (snd (tmf_polys z)))) = set_of (real_interval (Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z))))

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_of (Ipoly [real_interval (I ! 0 - interval_of (xs ! 0))] (map_poly real_interval (snd (tmf_polys z)))) = set_of (real_interval (Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z))))

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
have "\<dots> \<subseteq> set_of (real_interval (round_interval prec (Ipoly [(I ! 0 - xs ! 0)] (snd (tmf_polys z)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (real_interval (Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z)))) \<subseteq> set_of (real_interval (round_interval prec (Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z)))))
[PROOF STEP]
by (rule set_of_real_interval_subset) (rule round_ivl_correct)
[PROOF STATE]
proof (state)
this:
set_of (real_interval (Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z)))) \<subseteq> set_of (real_interval (round_interval prec (Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z)))))

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_of (real_interval (Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z)))) \<subseteq> set_of (real_interval (round_interval prec (Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z)))))

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
have "Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z)) = Ipoly (List.map2 (-) I (map interval_of xs)) (snd (tmf_polys z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z)) = Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z))
[PROOF STEP]
using  a
[PROOF STATE]
proof (prove)
using this:
map real_of_float xs all_in I

goal (1 subgoal):
 1. Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z)) = Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z))
[PROOF STEP]
apply (auto intro!: Ipoly_num_params_cong nth_equalityI
          simp: nth_Cons  simp del:length_greater_0_conv split: nat.splits dest!: less_le_trans[OF _ num_params_tmf_polys2[of z]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length I; \<forall>i<length I. real_of_float (xs ! i) \<in>\<^sub>r I ! i\<rbrakk> \<Longrightarrow> I ! 0 - interval_of (xs ! 0) = map2 (-) I (map interval_of xs) ! 0
[PROOF STEP]
apply (subst map2_nth)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length xs = length I; \<forall>i<length I. real_of_float (xs ! i) \<in>\<^sub>r I ! i\<rbrakk> \<Longrightarrow> 0 < length I
 2. \<lbrakk>length xs = length I; \<forall>i<length I. real_of_float (xs ! i) \<in>\<^sub>r I ! i\<rbrakk> \<Longrightarrow> 0 < length (map interval_of xs)
 3. \<lbrakk>length xs = length I; \<forall>i<length I. real_of_float (xs ! i) \<in>\<^sub>r I ! i\<rbrakk> \<Longrightarrow> I ! 0 - interval_of (xs ! 0) = I ! 0 - map interval_of xs ! 0
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Ipoly [I ! 0 - interval_of (xs ! 0)] (snd (tmf_polys z)) = Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z))

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))

goal (1 subgoal):
 1. (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cr ?s ord \<in>\<^sub>i ci ord \<Longrightarrow> (\<Sum>m<ord. cr ?s m * (x - real_of_float (xs ! 0)) ^ m) + cr ?s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
consider "0 < ord" "x \<noteq> xs ! 0" | "0 < ord" "x = xs ! 0" | "ord = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> thesis; ord = 0 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> ?thesis; ord = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> ?thesis; ord = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> ?thesis; ord = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
case hyps: 1
[PROOF STATE]
proof (state)
this:
0 < ord
x \<noteq> real_of_float (xs ! 0)

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ord
x \<noteq> real_of_float (xs ! 0)
[PROOF STEP]
have 1: "0 < ord" and 5: "x \<noteq> xs ! 0"
[PROOF STATE]
proof (prove)
using this:
0 < ord
x \<noteq> real_of_float (xs ! 0)

goal (1 subgoal):
 1. 0 < ord &&& x \<noteq> real_of_float (xs ! 0)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < ord
x \<noteq> real_of_float (xs ! 0)

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
from Taylor[OF 1 2 3 4 5]
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. (if x < real_of_float (xs ! 0) then x < t \<and> t < real_of_float (xs ! 0) else real_of_float (xs ! 0) < t \<and> t < x) \<and> interpret_floatarith f ((map real_of_float xs)[0 := x]) = (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := t]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord
[PROOF STEP]
obtain s where s: "(if ?x < ?c then ?x < s \<and> s < ?c else ?c < s \<and> s < ?x)"
      and tse: "?f ?x = (\<Sum>m<?n. ?diff m ?c / fact m * (?x - ?c) ^ m) + ?diff ?n s / fact ?n * (?x - ?c) ^ ?n"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. (if x < real_of_float (xs ! 0) then x < t \<and> t < real_of_float (xs ! 0) else real_of_float (xs ! 0) < t \<and> t < x) \<and> interpret_floatarith f ((map real_of_float xs)[0 := x]) = (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := t]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>if x < real_of_float (xs ! 0) then x < s \<and> s < real_of_float (xs ! 0) else real_of_float (xs ! 0) < s \<and> s < x; interpret_floatarith f ((map real_of_float xs)[0 := x]) = (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
if x < real_of_float (xs ! 0) then x < s \<and> s < real_of_float (xs ! 0) else real_of_float (xs ! 0) < s \<and> s < x
interpret_floatarith f ((map real_of_float xs)[0 := x]) = (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have "interpret_floatarith f ((map real_of_float xs)[0 := x]) -
    Ipoly (List.map2 (-) [x] [xs!0]) (fst (tmf_polys z)) =
    (\<Sum>m<?n. ?diff m ?c / fact m * (?x - ?c) ^ m) + ?diff ?n s / fact ?n * (?x - ?c) ^ ?n -
    (\<Sum>m\<le>?n. (x - xs!0) ^ m * mid (z ! m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) - Ipoly (map2 (-) [x] (map real_of_float [xs ! 0])) (map_poly real_of_float (fst (tmf_polys z))) = (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord - (\<Sum>m\<le>ord. (x - real_of_float (xs ! 0)) ^ m * real_of_float (mid (z ! m)))
[PROOF STEP]
unfolding tse
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord - Ipoly (map2 (-) [x] (map real_of_float [xs ! 0])) (map_poly real_of_float (fst (tmf_polys z))) = (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord - (\<Sum>m\<le>ord. (x - real_of_float (xs ! 0)) ^ m * real_of_float (mid (z ! m)))
[PROOF STEP]
by (simp add: Ipoly_fst_tmf_polys rewr lz)
[PROOF STATE]
proof (state)
this:
interpret_floatarith f ((map real_of_float xs)[0 := x]) - Ipoly (map2 (-) [x] (map real_of_float [xs ! 0])) (map_poly real_of_float (fst (tmf_polys z))) = (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord - (\<Sum>m\<le>ord. (x - real_of_float (xs ! 0)) ^ m * real_of_float (mid (z ! m)))

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
interpret_floatarith f ((map real_of_float xs)[0 := x]) - Ipoly (map2 (-) [x] (map real_of_float [xs ! 0])) (map_poly real_of_float (fst (tmf_polys z))) = (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord - (\<Sum>m\<le>ord. (x - real_of_float (xs ! 0)) ^ m * real_of_float (mid (z ! m)))

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have "\<dots> = (\<Sum>m<ord. cr s m  * (x - xs!0) ^ m) + cr s ord * (x - xs!0) ^ ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord - (\<Sum>m\<le>ord. (x - real_of_float (xs ! 0)) ^ m * real_of_float (mid (z ! m))) = (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord
[PROOF STEP]
unfolding rewr
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord - (\<Sum>m\<in>insert ord {..<ord}. (x - real_of_float (xs ! 0)) ^ m * real_of_float (mid (z ! m))) = (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord
[PROOF STEP]
by (simp add: algebra_simps cr_def sum.distrib sum_subtractf)
[PROOF STATE]
proof (state)
this:
(\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord - (\<Sum>m\<le>ord. (x - real_of_float (xs ! 0)) ^ m * real_of_float (mid (z ! m))) = (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m<ord. interpret_floatarith (deriv_rec f m) ((map real_of_float xs)[0 := real_of_float (xs ! 0)]) / fact m * (x - real_of_float (xs ! 0)) ^ m) + interpret_floatarith (deriv_rec f ord) ((map real_of_float xs)[0 := s]) / fact ord * (x - real_of_float (xs ! 0)) ^ ord - (\<Sum>m\<le>ord. (x - real_of_float (xs ! 0)) ^ m * real_of_float (mid (z ! m))) = (\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have "cr s ord \<in>\<^sub>i ci ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr s ord \<in>\<^sub>i ci ord
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
map real_of_float xs all_in I

goal (1 subgoal):
 1. cr s ord \<in>\<^sub>i ci ord
[PROOF STEP]
apply (auto simp: cr_def ci_def intro!: minus_in_intervalI
          tmf_c_correct[OF _ z_ord])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>length xs = length I; \<forall>i<length I. real_of_float (xs ! i) \<in>\<^sub>r I ! i; i < length I\<rbrakk> \<Longrightarrow> (map real_of_float xs)[0 := s] ! i \<in>\<^sub>r I ! i
[PROOF STEP]
by (smt "4"(1) "4"(2) "4"(3) "4"(4) a all_in_def in_real_intervalI length_greater_0_conv nth_list_update s xs_ne)
[PROOF STATE]
proof (state)
this:
cr s ord \<in>\<^sub>i ci ord

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
note enclosure[OF this]
[PROOF STATE]
proof (state)
this:
(\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m<ord. cr s m * (x - real_of_float (xs ! 0)) ^ m) + cr s ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have "Ipoly (List.map2 (-) [x] (map real_of_float [xs ! 0])) (map_poly real_of_float (fst (tmf_polys z))) =
        insertion e (map_poly real_of_float (fst (tmf_polys z)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly (map2 (-) [x] (map real_of_float [xs ! 0])) (map_poly real_of_float (fst (tmf_polys z))) = insertion e (map_poly real_of_float (fst (tmf_polys z)))
[PROOF STEP]
using diff_e
[PROOF STATE]
proof (prove)
using this:
x - real_of_float (xs ! 0) = e 0

goal (1 subgoal):
 1. Ipoly (map2 (-) [x] (map real_of_float [xs ! 0])) (map_poly real_of_float (fst (tmf_polys z))) = insertion e (map_poly real_of_float (fst (tmf_polys z)))
[PROOF STEP]
by (auto intro!: Ipoly_eq_insertionI simp: nth_Cons split: nat.splits dest: less_le_trans[OF _ num_params_tmf_polys1[of z]])
[PROOF STATE]
proof (state)
this:
Ipoly (map2 (-) [x] (map real_of_float [xs ! 0])) (map_poly real_of_float (fst (tmf_polys z))) = insertion e (map_poly real_of_float (fst (tmf_polys z)))

goal (3 subgoals):
 1. \<lbrakk>0 < ord; x \<noteq> real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 3. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
interpret_floatarith f ((map real_of_float xs)[0 := x]) - insertion e (map_poly real_of_float (fst (tmf_polys z))) \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interpret_floatarith f ((map real_of_float xs)[0 := x]) - insertion e (map_poly real_of_float (fst (tmf_polys z))) \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
by (simp add: tz tb range_tm_def set_of_eq)
[PROOF STATE]
proof (state)
this:
interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t

goal (2 subgoals):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
ord = 0

goal (2 subgoals):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
ord = 0
ord = 0
[PROOF STEP]
have "length z = Suc 0"
[PROOF STATE]
proof (prove)
using this:
ord = 0
ord = 0

goal (1 subgoal):
 1. length z = Suc 0
[PROOF STEP]
by (simp add: lz)
[PROOF STATE]
proof (state)
this:
length z = Suc 0

goal (2 subgoals):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length z = Suc 0
[PROOF STEP]
have "fst (tmf_polys z) = fst (tmf_polys [z ! 0])"
[PROOF STATE]
proof (prove)
using this:
length z = Suc 0

goal (1 subgoal):
 1. fst (tmf_polys z) = fst (tmf_polys [z ! 0])
[PROOF STEP]
by (cases z) auto
[PROOF STATE]
proof (state)
this:
fst (tmf_polys z) = fst (tmf_polys [z ! 0])

goal (2 subgoals):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst (tmf_polys z) = fst (tmf_polys [z ! 0])

goal (2 subgoals):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have "\<dots> = CN (mid (z ! 0))\<^sub>p 0 0\<^sub>p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (tmf_polys [z ! 0]) = CN (mid (z ! 0))\<^sub>p 0 0\<^sub>p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (tmf_polys [z ! 0]) = CN (mid (z ! 0))\<^sub>p 0 0\<^sub>p

goal (2 subgoals):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fst (tmf_polys z) = CN (mid (z ! 0))\<^sub>p 0 0\<^sub>p
[PROOF STEP]
have "fst (tmf_polys z) = CN (mid (z ! 0))\<^sub>p 0 0\<^sub>p"
[PROOF STATE]
proof (prove)
using this:
fst (tmf_polys z) = CN (mid (z ! 0))\<^sub>p 0 0\<^sub>p

goal (1 subgoal):
 1. fst (tmf_polys z) = CN (mid (z ! 0))\<^sub>p 0 0\<^sub>p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fst (tmf_polys z) = CN (mid (z ! 0))\<^sub>p 0 0\<^sub>p

goal (2 subgoals):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
 2. ord = 0 \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
with enclosure[OF cr_ord]
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>m<ord. cr x m * (x - real_of_float (xs ! 0)) ^ m) + cr x ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
fst (tmf_polys z) = CN (mid (z ! 0))\<^sub>p 0 0\<^sub>p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>m<ord. cr x m * (x - real_of_float (xs ! 0)) ^ m) + cr x ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
fst (tmf_polys z) = CN (mid (z ! 0))\<^sub>p 0 0\<^sub>p

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
by (simp add: cr_def 3 range_tm_def tz tb set_of_eq)
[PROOF STATE]
proof (state)
this:
interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t

goal (1 subgoal):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
0 < ord
x = real_of_float (xs ! 0)

goal (1 subgoal):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
have rewr: "{..<length z} = insert 0 {1..<length z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..<length z} = insert 0 {1..<length z}
[PROOF STEP]
by (auto simp: lz)
[PROOF STATE]
proof (state)
this:
{..<length z} = insert 0 {1..<length z}

goal (1 subgoal):
 1. \<lbrakk>0 < ord; x = real_of_float (xs ! 0)\<rbrakk> \<Longrightarrow> interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
from 2 enclosure[OF cr_ord]
[PROOF STATE]
proof (chain)
picking this:
0 < ord
x = real_of_float (xs ! 0)
(\<Sum>m<ord. cr x m * (x - real_of_float (xs ! 0)) ^ m) + cr x ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < ord
x = real_of_float (xs ! 0)
(\<Sum>m<ord. cr x m * (x - real_of_float (xs ! 0)) ^ m) + cr x ord * (x - real_of_float (xs ! 0)) ^ ord \<in>\<^sub>r round_interval prec (Ipoly (map2 (-) I (map interval_of xs)) (snd (tmf_polys z)))

goal (1 subgoal):
 1. interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t
[PROOF STEP]
by (auto simp: zero_power 2 cr_def range_tm_def tz tb insertion_fst_tmf_polys
          diff_e[symmetric] rewr set_of_eq)
[PROOF STATE]
proof (state)
this:
interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
interpret_floatarith f ((map real_of_float xs)[0 := x]) \<in>\<^sub>i range_tm e t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_polyadd[simp]: "insertion e (a +\<^sub>p b) = insertion e a + insertion e b"
  for a b::"'a::ring_1 poly"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (a +\<^sub>p b) = insertion e a + insertion e b
[PROOF STEP]
apply (induction a b rule: polyadd.induct)
[PROOF STATE]
proof (prove)
goal (28 subgoals):
 1. \<And>c c'. insertion e ((c)\<^sub>p +\<^sub>p (c')\<^sub>p) = insertion e (c)\<^sub>p + insertion e (c')\<^sub>p
 2. \<And>c c' n' p'. insertion e ((c)\<^sub>p +\<^sub>p c') = insertion e (c)\<^sub>p + insertion e c' \<Longrightarrow> insertion e ((c)\<^sub>p +\<^sub>p CN c' n' p') = insertion e (c)\<^sub>p + insertion e (CN c' n' p')
 3. \<And>c n p c'. insertion e (c +\<^sub>p (c')\<^sub>p) = insertion e c + insertion e (c')\<^sub>p \<Longrightarrow> insertion e (CN c n p +\<^sub>p (c')\<^sub>p) = insertion e (CN c n p) + insertion e (c')\<^sub>p
 4. \<And>c n p c' n' p'. \<lbrakk>insertion e (c +\<^sub>p CN c' n' p') = insertion e c + insertion e (CN c' n' p'); insertion e (CN c n p +\<^sub>p c') = insertion e (CN c n p) + insertion e c'; insertion e (c +\<^sub>p c') = insertion e c + insertion e c'; \<And>x. insertion e (p +\<^sub>p p') = insertion e p + insertion e p'\<rbrakk> \<Longrightarrow> insertion e (CN c n p +\<^sub>p CN c' n' p') = insertion e (CN c n p) + insertion e (CN c' n' p')
 5. \<And>v b. insertion e (poly.Bound v +\<^sub>p b) = insertion e (poly.Bound v) + insertion e b
 6. \<And>v va b. insertion e (Add v va +\<^sub>p b) = insertion e (Add v va) + insertion e b
 7. \<And>v va b. insertion e (Sub v va +\<^sub>p b) = insertion e (Sub v va) + insertion e b
 8. \<And>v va b. insertion e (Mul v va +\<^sub>p b) = insertion e (Mul v va) + insertion e b
 9. \<And>v b. insertion e (Neg v +\<^sub>p b) = insertion e (Neg v) + insertion e b
 10. \<And>v va b. insertion e (Pw v va +\<^sub>p b) = insertion e (Pw v va) + insertion e b
A total of 28 subgoals...
[PROOF STEP]
apply (auto simp: algebra_simps Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c p c' n' p'. \<lbrakk>insertion e (c +\<^sub>p CN c' n' p') = insertion e c + (insertion e c' + e n' * insertion e p'); insertion e (CN c n' p +\<^sub>p c') = insertion e c + (insertion e c' + e n' * insertion e p); insertion e (c +\<^sub>p c') = insertion e c + insertion e c'; insertion e p + insertion e p' = (0::'a); p +\<^sub>p p' = 0\<^sub>p\<rbrakk> \<Longrightarrow> e n' * insertion e p + e n' * insertion e p' = (0::'a)
[PROOF STEP]
by (metis (no_types) mult_zero_right ring_class.ring_distribs(1))


[STATEMENT]
lemma insertion_polyneg[simp]: "insertion e (~\<^sub>p b) =  - insertion e b"
  for b::"'a::ring_1 poly"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (~\<^sub>p b) = - insertion e b
[PROOF STEP]
by (induction b rule: polyneg.induct) (auto simp: algebra_simps Let_def)


[STATEMENT]
lemma insertion_polysub[simp]: "insertion e (a -\<^sub>p b) = insertion e a - insertion e b"
  for a b::"'a::ring_1 poly"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (a -\<^sub>p b) = insertion e a - insertion e b
[PROOF STEP]
by (simp add: polysub_def)


[STATEMENT]
lemma insertion_polymul[simp]: "insertion e (a *\<^sub>p b) = insertion e a * insertion e b"
  for a b::"'a::comm_ring_1 poly"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (a *\<^sub>p b) = insertion e a * insertion e b
[PROOF STEP]
by (induction a b rule: polymul.induct)
    (auto simp: algebra_simps Let_def)


[STATEMENT]
lemma insertion_polypow[simp]: "insertion e (a ^\<^sub>p b) = insertion e a ^ b"
  for a::"'a::comm_ring_1 poly"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (a ^\<^sub>p b) = insertion e a ^ b
[PROOF STEP]
proof (induction b rule: nat_less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<forall>m<n. insertion e (a ^\<^sub>p m) = insertion e a ^ m \<Longrightarrow> insertion e (a ^\<^sub>p n) = insertion e a ^ n
[PROOF STEP]
case (1 n)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. insertion e (a ^\<^sub>p m) = insertion e a ^ m

goal (1 subgoal):
 1. \<And>n. \<forall>m<n. insertion e (a ^\<^sub>p m) = insertion e a ^ m \<Longrightarrow> insertion e (a ^\<^sub>p n) = insertion e a ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m<n. insertion e (a ^\<^sub>p m) = insertion e a ^ m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. insertion e (a ^\<^sub>p m) = insertion e a ^ m

goal (1 subgoal):
 1. insertion e (a ^\<^sub>p n) = insertion e a ^ n
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>m<n. insertion e (a ^\<^sub>p m) = insertion e a ^ m; n = 0\<rbrakk> \<Longrightarrow> insertion e (a ^\<^sub>p n) = insertion e a ^ n
 2. \<And>nat. \<lbrakk>\<forall>m<n. insertion e (a ^\<^sub>p m) = insertion e a ^ m; n = Suc nat\<rbrakk> \<Longrightarrow> insertion e (a ^\<^sub>p n) = insertion e a ^ n
[PROOF STEP]
case (Suc nat)
[PROOF STATE]
proof (state)
this:
n = Suc nat

goal (2 subgoals):
 1. \<lbrakk>\<forall>m<n. insertion e (a ^\<^sub>p m) = insertion e a ^ m; n = 0\<rbrakk> \<Longrightarrow> insertion e (a ^\<^sub>p n) = insertion e a ^ n
 2. \<And>nat. \<lbrakk>\<forall>m<n. insertion e (a ^\<^sub>p m) = insertion e a ^ m; n = Suc nat\<rbrakk> \<Longrightarrow> insertion e (a ^\<^sub>p n) = insertion e a ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = Suc nat
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = Suc nat

goal (1 subgoal):
 1. insertion e (a ^\<^sub>p n) = insertion e a ^ n
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = Suc nat \<Longrightarrow> insertion e (let q = a ^\<^sub>p Suc nat div 2; d = q *\<^sub>p q in if odd nat then d else a *\<^sub>p d) = insertion e a * insertion e a ^ nat
[PROOF STEP]
apply (auto simp: Let_def div2_less_self 1 simp del: polypow.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = Suc nat; odd nat\<rbrakk> \<Longrightarrow> insertion e a * insertion e a ^ (nat div 2) * (insertion e a * insertion e a ^ (nat div 2)) = insertion e a * insertion e a ^ nat
 2. \<lbrakk>n = Suc nat; even nat\<rbrakk> \<Longrightarrow> insertion e a * (insertion e a ^ (nat div 2) * insertion e a ^ (nat div 2)) = insertion e a * insertion e a ^ nat
[PROOF STEP]
apply (metis even_Suc even_two_times_div_two odd_Suc_div_two semiring_normalization_rules(27) semiring_normalization_rules(36))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = Suc nat; even nat\<rbrakk> \<Longrightarrow> insertion e a * (insertion e a ^ (nat div 2) * insertion e a ^ (nat div 2)) = insertion e a * insertion e a ^ nat
[PROOF STEP]
apply (metis even_two_times_div_two semiring_normalization_rules(36))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
insertion e (a ^\<^sub>p n) = insertion e a ^ n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. insertion e (a ^\<^sub>p m) = insertion e a ^ m; n = 0\<rbrakk> \<Longrightarrow> insertion e (a ^\<^sub>p n) = insertion e a ^ n
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
insertion e (a ^\<^sub>p n) = insertion e a ^ n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_polynate [simp]:
  "insertion bs (polynate p) = (insertion bs p :: 'a::comm_ring_1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion bs (polynate p) = insertion bs p
[PROOF STEP]
by (induct p rule: polynate.induct) auto


[STATEMENT]
lemma tm_norm_poly_range:
  assumes "x \<in>\<^sub>i range_tm e t"
  shows "x \<in>\<^sub>i range_tm e (tm_norm_poly t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_norm_poly t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i range_tm e t

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_norm_poly t)
[PROOF STEP]
by (cases t) (simp add: range_tm_def)


[STATEMENT]
lemma split_by_degree_correct_insertion:
  fixes x :: "nat \<Rightarrow> real" and p :: "float poly"
  assumes "split_by_degree ord p = (l, r)"
  shows "maxdegree l \<le> ord" (is ?P1)
    and   "insertion x p = insertion x l + insertion x r" (is ?P2)
    and   "num_params l \<le> num_params p" (is ?P3)
    and   "num_params r \<le> num_params p" (is ?P4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (maxdegree l \<le> ord &&& insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)) &&& num_params l \<le> num_params p &&& num_params r \<le> num_params p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. maxdegree l \<le> ord
 2. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 3. num_params l \<le> num_params p
 4. num_params r \<le> num_params p
[PROOF STEP]
define xs where "xs = map x [0..<num_params p]"
[PROOF STATE]
proof (state)
this:
xs = map x [0..<num_params p]

goal (4 subgoals):
 1. maxdegree l \<le> ord
 2. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 3. num_params l \<le> num_params p
 4. num_params r \<le> num_params p
[PROOF STEP]
have xs: "i < num_params p \<Longrightarrow> x i = xs ! i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < num_params p \<Longrightarrow> x i = xs ! i
[PROOF STEP]
by (auto simp: xs_def)
[PROOF STATE]
proof (state)
this:
?i < num_params p \<Longrightarrow> x ?i = xs ! ?i

goal (4 subgoals):
 1. maxdegree l \<le> ord
 2. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 3. num_params l \<le> num_params p
 4. num_params r \<le> num_params p
[PROOF STEP]
have "insertion x p = Ipoly xs p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float p)
[PROOF STEP]
by (auto intro!: insertion_eq_IpolyI xs)
[PROOF STATE]
proof (state)
this:
insertion x (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float p)

goal (4 subgoals):
 1. maxdegree l \<le> ord
 2. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 3. num_params l \<le> num_params p
 4. num_params r \<le> num_params p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion x (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float p)

goal (4 subgoals):
 1. maxdegree l \<le> ord
 2. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 3. num_params l \<le> num_params p
 4. num_params r \<le> num_params p
[PROOF STEP]
from split_by_degree_correct[OF assms(1)[symmetric]]
[PROOF STATE]
proof (chain)
picking this:
maxdegree l \<le> ord
Ipoly ?x (map_poly real_of_float p) = Ipoly ?x (map_poly real_of_float l) + Ipoly ?x (map_poly real_of_float r)
num_params l \<le> num_params p
num_params r \<le> num_params p
[PROOF STEP]
have "maxdegree l \<le> ord"
    and p: "Ipoly xs (map_poly real_of_float p) =
    Ipoly xs (map_poly real_of_float l) + Ipoly xs (map_poly real_of_float r)"
   and l: "num_params l \<le> num_params p"
   and r: "num_params r \<le> num_params p"
[PROOF STATE]
proof (prove)
using this:
maxdegree l \<le> ord
Ipoly ?x (map_poly real_of_float p) = Ipoly ?x (map_poly real_of_float l) + Ipoly ?x (map_poly real_of_float r)
num_params l \<le> num_params p
num_params r \<le> num_params p

goal (1 subgoal):
 1. (maxdegree l \<le> ord &&& Ipoly xs (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float l) + Ipoly xs (map_poly real_of_float r)) &&& num_params l \<le> num_params p &&& num_params r \<le> num_params p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maxdegree l \<le> ord
Ipoly xs (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float l) + Ipoly xs (map_poly real_of_float r)
num_params l \<le> num_params p
num_params r \<le> num_params p

goal (4 subgoals):
 1. maxdegree l \<le> ord
 2. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 3. num_params l \<le> num_params p
 4. num_params r \<le> num_params p
[PROOF STEP]
show ?P1 ?P3 ?P4
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxdegree l \<le> ord &&& num_params l \<le> num_params p &&& num_params r \<le> num_params p
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
maxdegree l \<le> ord
num_params l \<le> num_params p
num_params r \<le> num_params p

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
note p
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float l) + Ipoly xs (map_poly real_of_float r)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float l) + Ipoly xs (map_poly real_of_float r)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
have "Ipoly xs (map_poly real_of_float l) = insertion x l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float l) = insertion x (map_poly real_of_float l)
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
num_params l \<le> num_params p

goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float l) = insertion x (map_poly real_of_float l)
[PROOF STEP]
by (auto intro!: xs Ipoly_eq_insertionI)
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float l) = insertion x (map_poly real_of_float l)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float l) = insertion x (map_poly real_of_float l)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
have "Ipoly xs (map_poly real_of_float r) = insertion x r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float r) = insertion x (map_poly real_of_float r)
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
num_params r \<le> num_params p

goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float r) = insertion x (map_poly real_of_float r)
[PROOF STEP]
by (auto intro!: xs Ipoly_eq_insertionI)
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float r) = insertion x (map_poly real_of_float r)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
show ?P2
[PROOF STATE]
proof (prove)
using this:
insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma split_by_prec_correct_insertion:
  fixes x :: "nat \<Rightarrow> real" and p :: "float poly"
  assumes "split_by_prec ord p = (l, r)"
  shows "insertion x p = insertion x l + insertion x r" (is ?P1)
    and "num_params l \<le> num_params p" (is ?P2)
    and "num_params r \<le> num_params p" (is ?P3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r) &&& num_params l \<le> num_params p &&& num_params r \<le> num_params p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 2. num_params l \<le> num_params p
 3. num_params r \<le> num_params p
[PROOF STEP]
define xs where "xs = map x [0..<num_params p]"
[PROOF STATE]
proof (state)
this:
xs = map x [0..<num_params p]

goal (3 subgoals):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 2. num_params l \<le> num_params p
 3. num_params r \<le> num_params p
[PROOF STEP]
have xs: "i < num_params p \<Longrightarrow> x i = xs ! i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < num_params p \<Longrightarrow> x i = xs ! i
[PROOF STEP]
by (auto simp: xs_def)
[PROOF STATE]
proof (state)
this:
?i < num_params p \<Longrightarrow> x ?i = xs ! ?i

goal (3 subgoals):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 2. num_params l \<le> num_params p
 3. num_params r \<le> num_params p
[PROOF STEP]
have "insertion x p = Ipoly xs p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float p)
[PROOF STEP]
by (auto intro!: insertion_eq_IpolyI xs)
[PROOF STATE]
proof (state)
this:
insertion x (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float p)

goal (3 subgoals):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 2. num_params l \<le> num_params p
 3. num_params r \<le> num_params p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion x (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float p)

goal (3 subgoals):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 2. num_params l \<le> num_params p
 3. num_params r \<le> num_params p
[PROOF STEP]
from split_by_prec_correct[OF assms(1)[symmetric]]
[PROOF STATE]
proof (chain)
picking this:
Ipoly ?args (map_poly real_of_float p) = Ipoly ?args (map_poly real_of_float l) + Ipoly ?args (map_poly real_of_float r)
num_params l \<le> num_params p
num_params r \<le> num_params p
[PROOF STEP]
have p: "Ipoly xs (map_poly real_of_float p) =
    Ipoly xs (map_poly real_of_float l) + Ipoly xs (map_poly real_of_float r)"
   and l: "num_params l \<le> num_params p"
   and r: "num_params r \<le> num_params p"
[PROOF STATE]
proof (prove)
using this:
Ipoly ?args (map_poly real_of_float p) = Ipoly ?args (map_poly real_of_float l) + Ipoly ?args (map_poly real_of_float r)
num_params l \<le> num_params p
num_params r \<le> num_params p

goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float l) + Ipoly xs (map_poly real_of_float r) &&& num_params l \<le> num_params p &&& num_params r \<le> num_params p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float l) + Ipoly xs (map_poly real_of_float r)
num_params l \<le> num_params p
num_params r \<le> num_params p

goal (3 subgoals):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
 2. num_params l \<le> num_params p
 3. num_params r \<le> num_params p
[PROOF STEP]
show ?P2 ?P3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params l \<le> num_params p &&& num_params r \<le> num_params p
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
num_params l \<le> num_params p
num_params r \<le> num_params p

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
note p
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float l) + Ipoly xs (map_poly real_of_float r)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float p) = Ipoly xs (map_poly real_of_float l) + Ipoly xs (map_poly real_of_float r)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
have "Ipoly xs (map_poly real_of_float l) = insertion x l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float l) = insertion x (map_poly real_of_float l)
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
num_params l \<le> num_params p

goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float l) = insertion x (map_poly real_of_float l)
[PROOF STEP]
by (auto intro!: xs Ipoly_eq_insertionI)
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float l) = insertion x (map_poly real_of_float l)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float l) = insertion x (map_poly real_of_float l)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
have "Ipoly xs (map_poly real_of_float r) = insertion x r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float r) = insertion x (map_poly real_of_float r)
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
num_params r \<le> num_params p

goal (1 subgoal):
 1. Ipoly xs (map_poly real_of_float r) = insertion x (map_poly real_of_float r)
[PROOF STEP]
by (auto intro!: xs Ipoly_eq_insertionI)
[PROOF STATE]
proof (state)
this:
Ipoly xs (map_poly real_of_float r) = insertion x (map_poly real_of_float r)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
show ?P1
[PROOF STATE]
proof (prove)
using this:
insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)

goal (1 subgoal):
 1. insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion x (map_poly real_of_float p) = insertion x (map_poly real_of_float l) + insertion x (map_poly real_of_float r)

goal:
No subgoals!
[PROOF STEP]
qed