[STATEMENT]
lemma compute_bound_poly_correct:
  fixes p::"float poly"
  assumes "num_params p \<le> length I"
  assumes dev: "develops_at_within e a I"
  shows "insertion e (p::real poly) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
num_params p \<le> length I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a
[PROOF STEP]
proof (induction p)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x. num_params (x)\<^sub>p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float (x)\<^sub>p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (x)\<^sub>p) I a
 2. \<And>x. num_params (poly.Bound x) \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float (poly.Bound x)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (poly.Bound x)) I a
 3. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Add p1 p2)) I a
 4. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 5. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 6. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 7. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 8. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
case (C x)
[PROOF STATE]
proof (state)
this:
num_params (x)\<^sub>p \<le> length I

goal (8 subgoals):
 1. \<And>x. num_params (x)\<^sub>p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float (x)\<^sub>p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (x)\<^sub>p) I a
 2. \<And>x. num_params (poly.Bound x) \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float (poly.Bound x)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (poly.Bound x)) I a
 3. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Add p1 p2)) I a
 4. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 5. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 6. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 7. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 8. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params (x)\<^sub>p \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params (x)\<^sub>p \<le> length I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (x)\<^sub>p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (x)\<^sub>p) I a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (x)\<^sub>p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (x)\<^sub>p) I a

goal (7 subgoals):
 1. \<And>x. num_params (poly.Bound x) \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float (poly.Bound x)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (poly.Bound x)) I a
 2. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Add p1 p2)) I a
 3. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 4. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 5. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 6. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 7. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x. num_params (poly.Bound x) \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float (poly.Bound x)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (poly.Bound x)) I a
 2. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Add p1 p2)) I a
 3. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 4. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 5. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 6. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 7. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
case (Bound i)
[PROOF STATE]
proof (state)
this:
num_params (poly.Bound i) \<le> length I

goal (7 subgoals):
 1. \<And>x. num_params (poly.Bound x) \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float (poly.Bound x)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (poly.Bound x)) I a
 2. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Add p1 p2)) I a
 3. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 4. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 5. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 6. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 7. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params (poly.Bound i) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params (poly.Bound i) \<le> length I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (poly.Bound i)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (poly.Bound i)) I a
[PROOF STEP]
using dev
[PROOF STATE]
proof (prove)
using this:
num_params (poly.Bound i) \<le> length I
develops_at_within e a I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (poly.Bound i)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (poly.Bound i)) I a
[PROOF STEP]
by (auto simp: develops_at_within_def)
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (poly.Bound i)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (poly.Bound i)) I a

goal (6 subgoals):
 1. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Add p1 p2)) I a
 2. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 3. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 4. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 5. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 6. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Add p1 p2)) I a
 2. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 3. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 4. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 5. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 6. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
case (Add p1 p2)
[PROOF STATE]
proof (state)
this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (Add p1 p2) \<le> length I

goal (6 subgoals):
 1. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Add p1 p2)) I a
 2. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 3. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 4. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 5. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 6. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (Add p1 p2) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (Add p1 p2) \<le> length I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Add p1 p2)) I a
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Add p1 p2)) I a

goal (5 subgoals):
 1. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 2. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 3. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 4. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 5. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 2. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 3. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 4. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 5. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
case (Sub p1 p2)
[PROOF STATE]
proof (state)
this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (Sub p1 p2) \<le> length I

goal (5 subgoals):
 1. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
 2. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 3. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 4. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 5. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (Sub p1 p2) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (Sub p1 p2) \<le> length I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Sub p1 p2)) I a

goal (4 subgoals):
 1. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 2. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 3. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 4. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 2. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 3. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 4. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
case (Mul p1 p2)
[PROOF STATE]
proof (state)
this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (Mul p1 p2) \<le> length I

goal (4 subgoals):
 1. \<And>p1 p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
 2. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 3. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 4. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (Mul p1 p2) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (Mul p1 p2) \<le> length I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Mul p1 p2)) I a

goal (3 subgoals):
 1. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 2. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 3. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 2. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 3. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
case (Neg p)
[PROOF STATE]
proof (state)
this:
num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a
num_params (Neg p) \<le> length I

goal (3 subgoals):
 1. \<And>p. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
 2. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 3. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a
num_params (Neg p) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a
num_params (Neg p) \<le> length I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (Neg p)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Neg p)) I a

goal (2 subgoals):
 1. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 2. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 2. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
case (Pw p x2a)
[PROOF STATE]
proof (state)
this:
num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a
num_params (Pw p x2a) \<le> length I

goal (2 subgoals):
 1. \<And>p x2a. \<lbrakk>num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a; num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
 2. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a
num_params (Pw p x2a) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params p \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p) I a
num_params (Pw p x2a) \<le> length I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (Pw p x2a)) I a

goal (1 subgoal):
 1. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
case (CN p1 i p2)
[PROOF STATE]
proof (state)
this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (CN p1 i p2) \<le> length I

goal (1 subgoal):
 1. \<And>p1 x2a p2. \<lbrakk>num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a; num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a; num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> insertion e (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 x2a p2)) I a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (CN p1 i p2) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (CN p1 i p2) \<le> length I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (CN p1 i p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 i p2)) I a
[PROOF STEP]
using dev
[PROOF STATE]
proof (prove)
using this:
num_params p1 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p1) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p1) I a
num_params p2 \<le> length I \<Longrightarrow> insertion e (map_poly real_of_float p2) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of p2) I a
num_params (CN p1 i p2) \<le> length I
develops_at_within e a I

goal (1 subgoal):
 1. insertion e (map_poly real_of_float (CN p1 i p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 i p2)) I a
[PROOF STEP]
by (auto simp: develops_at_within_def)
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (CN p1 i p2)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (CN p1 i p2)) I a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compute_bound_tm_correct:
  fixes I :: "float interval list" and f :: "real list \<Rightarrow> real"
  assumes n: "num_params (tm_poly t) \<le> length I"
  assumes dev: "develops_at_within e a I"
  assumes x0: "x0 \<in>\<^sub>i range_tm e t"
  shows "x0 \<in>\<^sub>r compute_bound_tm prec I a t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x0 \<in>\<^sub>r compute_bound_tm prec I a t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x0 \<in>\<^sub>r compute_bound_tm prec I a t
[PROOF STEP]
let ?I = "insertion e (tm_poly t)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x0 \<in>\<^sub>r compute_bound_tm prec I a t
[PROOF STEP]
have "x0 = ?I + (x0 - ?I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x0 = insertion e (map_poly real_of_float (tm_poly t)) + (x0 - insertion e (map_poly real_of_float (tm_poly t)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x0 = insertion e (map_poly real_of_float (tm_poly t)) + (x0 - insertion e (map_poly real_of_float (tm_poly t)))

goal (1 subgoal):
 1. x0 \<in>\<^sub>r compute_bound_tm prec I a t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x0 = insertion e (map_poly real_of_float (tm_poly t)) + (x0 - insertion e (map_poly real_of_float (tm_poly t)))

goal (1 subgoal):
 1. x0 \<in>\<^sub>r compute_bound_tm prec I a t
[PROOF STEP]
have "\<dots> \<in>\<^sub>r compute_bound_tm prec I a t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (map_poly real_of_float (tm_poly t)) + (x0 - insertion e (map_poly real_of_float (tm_poly t))) \<in>\<^sub>r compute_bound_tm prec I a t
[PROOF STEP]
unfolding compute_bound_tm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (map_poly real_of_float (tm_poly t)) + (x0 - insertion e (map_poly real_of_float (tm_poly t))) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (tm_poly t)) I a + tm_bound t
[PROOF STEP]
apply (rule in_set_real_plus_interval)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. insertion e (map_poly real_of_float (tm_poly t)) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of (tm_poly t)) I a
 2. x0 - insertion e (map_poly real_of_float (tm_poly t)) \<in>\<^sub>r tm_bound t
[PROOF STEP]
apply (rule compute_bound_poly_correct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. num_params (tm_poly t) \<le> length I
 2. develops_at_within e a I
 3. x0 - insertion e (map_poly real_of_float (tm_poly t)) \<in>\<^sub>r tm_bound t
[PROOF STEP]
apply (rule assms)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. develops_at_within e a I
 2. x0 - insertion e (map_poly real_of_float (tm_poly t)) \<in>\<^sub>r tm_bound t
[PROOF STEP]
apply (rule dev)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x0 - insertion e (map_poly real_of_float (tm_poly t)) \<in>\<^sub>r tm_bound t
[PROOF STEP]
using range_tmD[OF x0]
[PROOF STATE]
proof (prove)
using this:
x0 \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t))) + real_interval (tm_bound t)

goal (1 subgoal):
 1. x0 - insertion e (map_poly real_of_float (tm_poly t)) \<in>\<^sub>r tm_bound t
[PROOF STEP]
by (auto simp: set_of_eq)
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (tm_poly t)) + (x0 - insertion e (map_poly real_of_float (tm_poly t))) \<in>\<^sub>r compute_bound_tm prec I a t

goal (1 subgoal):
 1. x0 \<in>\<^sub>r compute_bound_tm prec I a t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x0 \<in>\<^sub>r compute_bound_tm prec I a t
[PROOF STEP]
show "x0 \<in>\<^sub>r compute_bound_tm prec I a t"
[PROOF STATE]
proof (prove)
using this:
x0 \<in>\<^sub>r compute_bound_tm prec I a t

goal (1 subgoal):
 1. x0 \<in>\<^sub>r compute_bound_tm prec I a t
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x0 \<in>\<^sub>r compute_bound_tm prec I a t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compute_bound_tm_correct_subset:
  fixes I :: "float interval list" and f :: "real list \<Rightarrow> real"
  assumes n: "num_params (tm_poly t) \<le> length I"
  assumes dev: "develops_at_within e a I"
  shows "set_of (range_tm e t) \<subseteq> set_of (real_interval (compute_bound_tm prec I a t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (range_tm e t) \<subseteq> set_of (real_interval (compute_bound_tm prec I a t))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly t) \<le> length I
develops_at_within e a I

goal (1 subgoal):
 1. set_of (range_tm e t) \<subseteq> set_of (real_interval (compute_bound_tm prec I a t))
[PROOF STEP]
by (auto intro!: compute_bound_tm_correct)