[STATEMENT]
lemma eval_poly_at_tm_range:
  assumes "num_params p \<le> 1"
  assumes tg_def: "e' 0 \<in>\<^sub>i range_tm e tg"
  assumes dev: "develops_at_within e a I" and params: "num_params (tm_poly tg) \<le> length I"
  shows "insertion e' p \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg)
[PROOF STEP]
using assms(1) params
[PROOF STATE]
proof (prove)
using this:
num_params p \<le> 1
num_params (tm_poly tg) \<le> length I

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

goal (8 subgoals):
 1. \<And>x. \<lbrakk>num_params (x)\<^sub>p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (x)\<^sub>p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (x)\<^sub>p tg)
 2. \<And>x. \<lbrakk>num_params (poly.Bound x) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (poly.Bound x)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (poly.Bound x) tg)
 3. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Add p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Add p1 p2) tg)
 4. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Sub p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Sub p1 p2) tg)
 5. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Mul p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Mul p1 p2) tg)
 6. \<And>p. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Neg p) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Neg p)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Neg p) tg)
 7. \<And>p x2a. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Pw p x2a) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Pw p x2a) tg)
 8. \<And>p1 x2a p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (CN p1 x2a p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1 x2a p2) tg)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
num_params (c)\<^sub>p \<le> 1
num_params (tm_poly tg) \<le> length I

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (c)\<^sub>p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (c)\<^sub>p tg)
[PROOF STEP]
using tg_def
[PROOF STATE]
proof (prove)
using this:
num_params (c)\<^sub>p \<le> 1
num_params (tm_poly tg) \<le> length I
e' 0 \<in>\<^sub>i range_tm e tg

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (c)\<^sub>p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (c)\<^sub>p tg)
[PROOF STEP]
by (cases tg) (auto simp: tm_const_def range_tm_def real_interval_zero)
[PROOF STATE]
proof (state)
this:
insertion e' (map_poly real_of_float (c)\<^sub>p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (c)\<^sub>p tg)

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

goal (7 subgoals):
 1. \<And>x. \<lbrakk>num_params (poly.Bound x) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (poly.Bound x)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (poly.Bound x) tg)
 2. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Add p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Add p1 p2) tg)
 3. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Sub p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Sub p1 p2) tg)
 4. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Mul p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Mul p1 p2) tg)
 5. \<And>p. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Neg p) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Neg p)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Neg p) tg)
 6. \<And>p x2a. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Pw p x2a) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Pw p x2a) tg)
 7. \<And>p1 x2a p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (CN p1 x2a p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1 x2a p2) tg)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
num_params (poly.Bound n) \<le> 1
num_params (tm_poly tg) \<le> length I

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (poly.Bound n)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (poly.Bound n) tg)
[PROOF STEP]
using tg_def
[PROOF STATE]
proof (prove)
using this:
num_params (poly.Bound n) \<le> 1
num_params (tm_poly tg) \<le> length I
e' 0 \<in>\<^sub>i range_tm e tg

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (poly.Bound n)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (poly.Bound n) tg)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insertion e' (map_poly real_of_float (poly.Bound n)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (poly.Bound n) tg)

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

goal (6 subgoals):
 1. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Add p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Add p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Add p1 p2) tg)
 2. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Sub p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Sub p1 p2) tg)
 3. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Mul p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Mul p1 p2) tg)
 4. \<And>p. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Neg p) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Neg p)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Neg p) tg)
 5. \<And>p x2a. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Pw p x2a) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Pw p x2a) tg)
 6. \<And>p1 x2a p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (CN p1 x2a p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1 x2a p2) tg)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_params p1l \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1l) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1l tg)
\<lbrakk>num_params p1r \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1r) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1r tg)
num_params (Add p1l p1r) \<le> 1
num_params (tm_poly tg) \<le> length I

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (Add p1l p1r)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Add p1l p1r) tg)
[PROOF STEP]
using tm_add_range
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_params p1l \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1l) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1l tg)
\<lbrakk>num_params p1r \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1r) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1r tg)
num_params (Add p1l p1r) \<le> 1
num_params (tm_poly tg) \<le> length I
\<lbrakk>?x \<in>\<^sub>i range_tm ?e ?t1.0; ?y \<in>\<^sub>i range_tm ?e ?t2.0\<rbrakk> \<Longrightarrow> ?x + ?y \<in>\<^sub>i range_tm ?e (tm_add ?t1.0 ?t2.0)

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (Add p1l p1r)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Add p1l p1r) tg)
[PROOF STEP]
by (simp add: func_plus)
[PROOF STATE]
proof (state)
this:
insertion e' (map_poly real_of_float (Add p1l p1r)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Add p1l p1r) tg)

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

goal (5 subgoals):
 1. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Sub p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Sub p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Sub p1 p2) tg)
 2. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Mul p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Mul p1 p2) tg)
 3. \<And>p. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Neg p) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Neg p)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Neg p) tg)
 4. \<And>p x2a. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Pw p x2a) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Pw p x2a) tg)
 5. \<And>p1 x2a p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (CN p1 x2a p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1 x2a p2) tg)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_params p1l \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1l) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1l tg)
\<lbrakk>num_params p1r \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1r) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1r tg)
num_params (Sub p1l p1r) \<le> 1
num_params (tm_poly tg) \<le> length I

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (Sub p1l p1r)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Sub p1l p1r) tg)
[PROOF STEP]
using tm_sub_range
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_params p1l \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1l) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1l tg)
\<lbrakk>num_params p1r \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1r) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1r tg)
num_params (Sub p1l p1r) \<le> 1
num_params (tm_poly tg) \<le> length I
\<lbrakk>?x \<in>\<^sub>i range_tm ?e ?t1.0; ?y \<in>\<^sub>i range_tm ?e ?t2.0\<rbrakk> \<Longrightarrow> ?x - ?y \<in>\<^sub>i range_tm ?e (tm_sub ?t1.0 ?t2.0)

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (Sub p1l p1r)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Sub p1l p1r) tg)
[PROOF STEP]
by (simp add: fun_diff_def)
[PROOF STATE]
proof (state)
this:
insertion e' (map_poly real_of_float (Sub p1l p1r)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Sub p1l p1r) tg)

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

goal (4 subgoals):
 1. \<And>p1 p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (Mul p1 p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Mul p1 p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Mul p1 p2) tg)
 2. \<And>p. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Neg p) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Neg p)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Neg p) tg)
 3. \<And>p x2a. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Pw p x2a) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Pw p x2a) tg)
 4. \<And>p1 x2a p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (CN p1 x2a p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1 x2a p2) tg)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_params p1l \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1l) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1l tg)
\<lbrakk>num_params p1r \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1r) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1r tg)
num_params (Mul p1l p1r) \<le> 1
num_params (tm_poly tg) \<le> length I

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (Mul p1l p1r)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Mul p1l p1r) tg)
[PROOF STEP]
by (auto intro!: tm_mul_range Mul dev num_params_eval_poly_le)
[PROOF STATE]
proof (state)
this:
insertion e' (map_poly real_of_float (Mul p1l p1r)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Mul p1l p1r) tg)

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

goal (3 subgoals):
 1. \<And>p. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Neg p) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Neg p)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Neg p) tg)
 2. \<And>p x2a. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Pw p x2a) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Pw p x2a) tg)
 3. \<And>p1 x2a p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (CN p1 x2a p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1 x2a p2) tg)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_params p1' \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1') \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1' tg)
num_params (Neg p1') \<le> 1
num_params (tm_poly tg) \<le> length I

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (Neg p1')) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Neg p1') tg)
[PROOF STEP]
using tm_neg_range
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_params p1' \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1') \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1' tg)
num_params (Neg p1') \<le> 1
num_params (tm_poly tg) \<le> length I
?x \<in>\<^sub>i range_tm ?e ?t \<Longrightarrow> - ?x \<in>\<^sub>i range_tm ?e (tm_neg ?t)

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (Neg p1')) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Neg p1') tg)
[PROOF STEP]
by (simp add: fun_Compl_def)
[PROOF STATE]
proof (state)
this:
insertion e' (map_poly real_of_float (Neg p1')) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Neg p1') tg)

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

goal (2 subgoals):
 1. \<And>p x2a. \<lbrakk>\<lbrakk>num_params p \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p tg); num_params (Pw p x2a) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (Pw p x2a)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Pw p x2a) tg)
 2. \<And>p1 x2a p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (CN p1 x2a p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1 x2a p2) tg)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_params p1' \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1') \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1' tg)
num_params (Pw p1' n) \<le> 1
num_params (tm_poly tg) \<le> length I

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (Pw p1' n)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Pw p1' n) tg)
[PROOF STEP]
by (auto intro!: tm_pow_range Pw dev num_params_eval_poly_le)
[PROOF STATE]
proof (state)
this:
insertion e' (map_poly real_of_float (Pw p1' n)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (Pw p1' n) tg)

goal (1 subgoal):
 1. \<And>p1 x2a p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (CN p1 x2a p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1 x2a p2) tg)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 x2a p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (CN p1 x2a p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1 x2a p2) tg)
[PROOF STEP]
case (CN p1l n p1r)
[PROOF STATE]
proof (state)
this:
\<lbrakk>num_params p1l \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1l) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1l tg)
\<lbrakk>num_params p1r \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1r) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1r tg)
num_params (CN p1l n p1r) \<le> 1
num_params (tm_poly tg) \<le> length I

goal (1 subgoal):
 1. \<And>p1 x2a p2. \<lbrakk>\<lbrakk>num_params p1 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1 tg); \<lbrakk>num_params p2 \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p2) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p2 tg); num_params (CN p1 x2a p2) \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float (CN p1 x2a p2)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1 x2a p2) tg)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_params p1l \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1l) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1l tg)
\<lbrakk>num_params p1r \<le> 1; num_params (tm_poly tg) \<le> length I\<rbrakk> \<Longrightarrow> insertion e' (map_poly real_of_float p1r) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a p1r tg)
num_params (CN p1l n p1r) \<le> 1
num_params (tm_poly tg) \<le> length I

goal (1 subgoal):
 1. insertion e' (map_poly real_of_float (CN p1l n p1r)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1l n p1r) tg)
[PROOF STEP]
by (auto intro!: tm_mul_range tm_pow_range CN dev num_params_eval_poly_le tm_add_range tg_def)
[PROOF STATE]
proof (state)
this:
insertion e' (map_poly real_of_float (CN p1l n p1r)) \<in>\<^sub>i range_tm e (eval_poly_at_tm prec ord I a (CN p1l n p1r) tg)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tm_inc_err_range: "x \<in>\<^sub>i range_tm e (tm_inc_err i t)"
  if "x \<in>\<^sub>i range_tm e t + real_interval i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_inc_err i t)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i range_tm e t + real_interval i

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


[STATEMENT]
lemma num_params_tm_inc_err: "num_params (tm_poly (tm_inc_err i t)) \<le> X"
  if "num_params (tm_poly t) \<le> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly (tm_inc_err i t)) \<le> X
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly t) \<le> X

goal (1 subgoal):
 1. num_params (tm_poly (tm_inc_err i t)) \<le> X
[PROOF STEP]
by (cases t) auto


[STATEMENT]
lemma num_params_tm_comp_le: "num_params (tm_poly (tm_comp prec ord I a ga tf tg)) \<le> X"
  if "num_params (tm_poly tf) \<le> max 1 X" "num_params (tm_poly tg) \<le> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly (tm_comp prec ord I a ga tf tg)) \<le> X
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly tf) \<le> max 1 X
num_params (tm_poly tg) \<le> X

goal (1 subgoal):
 1. num_params (tm_poly (tm_comp prec ord I a ga tf tg)) \<le> X
[PROOF STEP]
by (cases tf) (auto intro!: num_params_tm_inc_err num_params_eval_poly_le num_params_tm_sub_le)


[STATEMENT]
lemma tm_comp_range:
  assumes tf_def: "x \<in>\<^sub>i range_tm e' tf"
  assumes tg_def: "e' 0 \<in>\<^sub>i range_tm e (tm_sub tg (tm_const ga))"
  assumes params: "num_params (tm_poly tf) \<le> 1" "num_params (tm_poly tg) \<le> length I"
  assumes dev: "develops_at_within e a I"
  shows "x \<in>\<^sub>i range_tm e (tm_comp prec ord I a ga tf tg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_comp prec ord I a ga tf tg)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_comp prec ord I a ga tf tg)
[PROOF STEP]
obtain pf ef where tf_decomp: "tf = TaylorModel pf ef"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pf ef. tf = TaylorModel pf ef \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using taylor_model.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = TaylorModel x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>pf ef. tf = TaylorModel pf ef \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tf = TaylorModel pf ef

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_comp prec ord I a ga tf tg)
[PROOF STEP]
obtain pg eg where tg_decomp: "tg = TaylorModel pg eg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pg eg. tg = TaylorModel pg eg \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using taylor_model.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = TaylorModel x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>pg eg. tg = TaylorModel pg eg \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tg = TaylorModel pg eg

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_comp prec ord I a ga tf tg)
[PROOF STEP]
from params
[PROOF STATE]
proof (chain)
picking this:
num_params (tm_poly tf) \<le> 1
num_params (tm_poly tg) \<le> length I
[PROOF STEP]
have params: "num_params pf \<le> Suc 0" "num_params pg \<le> length I"
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly tf) \<le> 1
num_params (tm_poly tg) \<le> length I

goal (1 subgoal):
 1. num_params pf \<le> Suc 0 &&& num_params pg \<le> length I
[PROOF STEP]
by (auto simp: tf_decomp tg_decomp)
[PROOF STATE]
proof (state)
this:
num_params pf \<le> Suc 0
num_params pg \<le> length I

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_comp prec ord I a ga tf tg)
[PROOF STEP]
from tf_def
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>i range_tm e' tf
[PROOF STEP]
obtain xe where x_def: "x = insertion e' pf + xe" "xe \<in>\<^sub>r ef"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i range_tm e' tf

goal (1 subgoal):
 1. (\<And>xe. \<lbrakk>x = insertion e' (map_poly real_of_float pf) + xe; xe \<in>\<^sub>r ef\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: tf_decomp range_tm_def elim!: plus_in_intervalE)
[PROOF STATE]
proof (state)
this:
x = insertion e' (map_poly real_of_float pf) + xe
xe \<in>\<^sub>r ef

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_comp prec ord I a ga tf tg)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_comp prec ord I a ga tf tg)
[PROOF STEP]
using tg_def
[PROOF STATE]
proof (prove)
using this:
e' 0 \<in>\<^sub>i range_tm e (tm_sub tg (tm_const ga))

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_comp prec ord I a ga tf tg)
[PROOF STEP]
by (auto simp: tf_decomp tg_decomp x_def params dev
        intro!: tm_inc_err_range eval_poly_at_tm_range plus_in_intervalI num_params_tm_sub_le)
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>i range_tm e (tm_comp prec ord I a ga tf tg)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mid_centered_collapse:
  "interval_of (real_of_float (mid abs_bound)) + real_interval (centered abs_bound) =
    real_interval abs_bound"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interval_of (real_of_float (mid abs_bound)) + real_interval (centered abs_bound) = real_interval abs_bound
[PROOF STEP]
by (auto simp: centered_def interval_eq_iff)


[STATEMENT]
lemma tm_abs_range:
  assumes x: "x \<in>\<^sub>i range_tm e t"
  assumes n: "num_params (tm_poly t) \<le> length I" and d: "develops_at_within e a I"
  shows "abs x \<in>\<^sub>i range_tm e (tm_abs prec I a t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>i range_tm e (tm_abs prec I a t)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>i range_tm e (tm_abs prec I a t)
[PROOF STEP]
obtain p e where t_def[simp]: "t = TaylorModel p e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p e. t = TaylorModel p e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using taylor_model.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = TaylorModel x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>p e. t = TaylorModel p e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = TaylorModel p e

goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>i range_tm e (tm_abs prec I a t)
[PROOF STEP]
define bound where "bound = compute_bound_tm prec I a t"
[PROOF STATE]
proof (state)
this:
bound = compute_bound_tm prec I a t

goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>i range_tm e (tm_abs prec I a t)
[PROOF STEP]
have bound: "x \<in>\<^sub>r bound"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>r bound
[PROOF STEP]
unfolding bound_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>r compute_bound_tm prec I a t
[PROOF STEP]
using n d x
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly t) \<le> length I
develops_at_within e a I
x \<in>\<^sub>i range_tm e t

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

goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>i range_tm e (tm_abs prec I a t)
[PROOF STEP]
define abs_bound where "abs_bound \<equiv> Ivl 0 (max \<bar>lower bound\<bar> \<bar>upper bound\<bar>)"
[PROOF STATE]
proof (state)
this:
abs_bound \<equiv> Ivl 0 (max \<bar>lower bound\<bar> \<bar>upper bound\<bar>)

goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>i range_tm e (tm_abs prec I a t)
[PROOF STEP]
have abs_bound: "\<bar>x\<bar> \<in>\<^sub>r abs_bound"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>r abs_bound
[PROOF STEP]
using bound
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>r bound

goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>r abs_bound
[PROOF STEP]
by (auto simp: abs_bound_def set_of_eq abs_real_def max_def min_def)
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> \<in>\<^sub>r abs_bound

goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>i range_tm e (tm_abs prec I a t)
[PROOF STEP]
have tm_abs_decomp: "tm_abs prec I a t = TaylorModel (poly.C (mid abs_bound)) (centered abs_bound)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tm_abs prec I a t = TaylorModel (mid abs_bound)\<^sub>p (centered abs_bound)
[PROOF STEP]
by (simp add: bound_def abs_bound_def Let_def tm_abs.simps)
[PROOF STATE]
proof (state)
this:
tm_abs prec I a t = TaylorModel (mid abs_bound)\<^sub>p (centered abs_bound)

goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>i range_tm e (tm_abs prec I a t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>i range_tm e (tm_abs prec I a t)
[PROOF STEP]
unfolding tm_abs_decomp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> \<in>\<^sub>i range_tm e (TaylorModel (mid abs_bound)\<^sub>p (centered abs_bound))
[PROOF STEP]
by (rule range_tmI) (auto simp: mid_centered_collapse abs_bound)
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> \<in>\<^sub>i range_tm e (tm_abs prec I a t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma num_params_tm_abs_le: "num_params (tm_poly (tm_abs prec I a t)) \<le> X" if "num_params (tm_poly t) \<le> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly (tm_abs prec I a t)) \<le> X
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly t) \<le> X

goal (1 subgoal):
 1. num_params (tm_poly (tm_abs prec I a t)) \<le> X
[PROOF STEP]
by (auto simp: tm_abs.simps Let_def)


[STATEMENT]
lemma real_interval_sup: "real_interval (sup a b) = sup (real_interval a) (real_interval b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_interval (sup a b) = sup (real_interval a) (real_interval b)
[PROOF STEP]
by (auto simp: interval_eq_iff inf_real_def inf_float_def sup_float_def sup_real_def min_def max_def)


[STATEMENT]
lemma in_interval_supI1: "x \<in>\<^sub>i a \<Longrightarrow> x \<in>\<^sub>i sup a b"
  and in_interval_supI2: "x \<in>\<^sub>i b \<Longrightarrow> x \<in>\<^sub>i sup a b"
  for x::"'a::lattice"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in>\<^sub>i a \<Longrightarrow> x \<in>\<^sub>i sup a b) &&& (x \<in>\<^sub>i b \<Longrightarrow> x \<in>\<^sub>i sup a b)
[PROOF STEP]
by (auto simp: set_of_eq le_infI1 le_infI2 le_supI1 le_supI2)


[STATEMENT]
lemma tm_union_range_left:
  assumes "x \<in>\<^sub>i range_tm e t1"
    "num_params (tm_poly t1) \<le> length I" "develops_at_within e a I"
  shows "x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
define b1 where "b1 \<equiv> compute_bound_tm prec I a t1"
[PROOF STATE]
proof (state)
this:
b1 \<equiv> compute_bound_tm prec I a t1

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
define b2 where "b2 \<equiv> compute_bound_tm prec I a t2"
[PROOF STATE]
proof (state)
this:
b2 \<equiv> compute_bound_tm prec I a t2

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
define b_combined where "b_combined \<equiv> sup b1 b2"
[PROOF STATE]
proof (state)
this:
b_combined \<equiv> sup b1 b2

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
obtain p e where tm_union_decomp: "tm_union prec I a t1 t2 = TaylorModel p e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p e. tm_union prec I a t1 t2 = TaylorModel p e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using taylor_model.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = TaylorModel x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>p e. tm_union prec I a t1 t2 = TaylorModel p e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tm_union prec I a t1 t2 = TaylorModel p e

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tm_union prec I a t1 t2 = TaylorModel p e
[PROOF STEP]
have p_def: "p = (mid b_combined)\<^sub>p"
    and e_def: "e = centered b_combined"
[PROOF STATE]
proof (prove)
using this:
tm_union prec I a t1 t2 = TaylorModel p e

goal (1 subgoal):
 1. p = (mid b_combined)\<^sub>p &&& e = centered b_combined
[PROOF STEP]
by (auto simp: Let_def b1_def b2_def b_combined_def interval_eq_iff)
[PROOF STATE]
proof (state)
this:
p = (mid b_combined)\<^sub>p
e = centered b_combined

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
have "x \<in>\<^sub>r b1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>r b1
[PROOF STEP]
by (auto simp : b1_def intro!: compute_bound_tm_correct assms)
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>r b1

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>r b1
[PROOF STEP]
have "x \<in>\<^sub>r b_combined"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>r b1

goal (1 subgoal):
 1. x \<in>\<^sub>r b_combined
[PROOF STEP]
by (auto simp: b_combined_def real_interval_sup in_interval_supI1)
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>r b_combined

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>r b_combined
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>r b_combined

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
unfolding tm_union_decomp
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>r b_combined

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (TaylorModel p e)
[PROOF STEP]
by (auto simp: range_tm_def p_def e_def mid_centered_collapse)
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tm_union_range_right:
  assumes "x \<in>\<^sub>i range_tm e t2"
    "num_params (tm_poly t2) \<le> length I" "develops_at_within e a I"
  shows "x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
using tm_union_range_left[OF assms]
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i range_tm e (tm_union ?prec I a t2 ?t2.0)

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_union prec I a t1 t2)
[PROOF STEP]
by (simp add: interval_union_commute)


[STATEMENT]
lemma num_params_tm_union_le:
  "num_params (tm_poly (tm_union prec I a t1 t2)) \<le> X"
  if "num_params (tm_poly t1) \<le> X" "num_params (tm_poly t2) \<le> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly (tm_union prec I a t1 t2)) \<le> X
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly t1) \<le> X
num_params (tm_poly t2) \<le> X

goal (1 subgoal):
 1. num_params (tm_poly (tm_union prec I a t1 t2)) \<le> X
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma tm_min_range:
  assumes "x \<in>\<^sub>i range_tm e t1"
  assumes "y \<in>\<^sub>i range_tm e t2"
    "num_params (tm_poly t1) \<le> length I"
    "num_params (tm_poly t2) \<le> length I"
    "develops_at_within e a I"
  shows "min x y \<in>\<^sub>i range_tm e (tm_min prec I a t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min x y \<in>\<^sub>i range_tm e (tm_min prec I a t1 t2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i range_tm e t1
y \<in>\<^sub>i range_tm e t2
num_params (tm_poly t1) \<le> length I
num_params (tm_poly t2) \<le> length I
develops_at_within e a I

goal (1 subgoal):
 1. min x y \<in>\<^sub>i range_tm e (tm_min prec I a t1 t2)
[PROOF STEP]
by (auto simp: Let_def tm_min.simps min_def intro: tm_union_range_left tm_union_range_right)


[STATEMENT]
lemma tm_max_range:
  assumes "x \<in>\<^sub>i range_tm e t1"
  assumes "y \<in>\<^sub>i range_tm e t2"
    "num_params (tm_poly t1) \<le> length I"
    "num_params (tm_poly t2) \<le> length I"
    "develops_at_within e a I"
  shows "max x y \<in>\<^sub>i range_tm e (tm_max prec I a t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max x y \<in>\<^sub>i range_tm e (tm_max prec I a t1 t2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i range_tm e t1
y \<in>\<^sub>i range_tm e t2
num_params (tm_poly t1) \<le> length I
num_params (tm_poly t2) \<le> length I
develops_at_within e a I

goal (1 subgoal):
 1. max x y \<in>\<^sub>i range_tm e (tm_max prec I a t1 t2)
[PROOF STEP]
by (auto simp: Let_def tm_max.simps max_def intro: tm_union_range_left tm_union_range_right)


[STATEMENT]
lemma mid_in_real_interval: "mid i \<in>\<^sub>r i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_float (mid i) \<in>\<^sub>r i
[PROOF STEP]
using lower_le_upper[of i]
[PROOF STATE]
proof (prove)
using this:
lower i \<le> upper i

goal (1 subgoal):
 1. real_of_float (mid i) \<in>\<^sub>r i
[PROOF STEP]
by (auto simp: mid_def set_of_eq powr_minus)


[STATEMENT]
lemma set_of_real_interval_mono:"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]
lemma tm_floatarith_eq_Some_num_params:
  "tm_floatarith prec ord a b f = Some tf \<Longrightarrow> num_params (tm_poly tf) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tm_floatarith prec ord a b f = Some tf \<Longrightarrow> num_params (tm_poly tf) \<le> 1
[PROOF STEP]
by (auto simp: tm_floatarith.simps split_beta' Let_def those_eq_Some_iff num_params_tmf_polys1)


[STATEMENT]
lemma compute_tm_by_comp_range:
  assumes "max_Var_floatarith f \<le> 1"
  assumes a: "a all_subset I"
  assumes tx_range: "x \<in>\<^sub>i range_tm e tg"
  assumes t_def: "compute_tm_by_comp prec ord I a f (Some tg) c = Some t"
  assumes f_deriv:
    "\<And>x. x \<in>\<^sub>r compute_bound_tm prec I a tg \<Longrightarrow> c (compute_bound_tm prec I a tg) \<Longrightarrow> isDERIV 0 f [x]"
  assumes params: "num_params (tm_poly tg) \<le> length I"
    and dev: "develops_at_within e a I"
  shows "interpret_floatarith f [x] \<in>\<^sub>i range_tm e t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm e t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm e t
[PROOF STEP]
from t_def[simplified, simplified Let_def]
[PROOF STATE]
proof (chain)
picking this:
(if c (compute_bound_tm prec I a tg) then map_option (\<lambda>tf. tm_comp prec ord I a (mid (compute_bound_tm prec a a tg)) tf tg) (tm_floatarith prec ord [compute_bound_tm prec I a tg] [mid (compute_bound_tm prec a a tg)] f) else None) = Some t
[PROOF STEP]
obtain tf
    where t1_def: "tm_floatarith prec ord [compute_bound_tm prec I (a) tg]
          [mid (compute_bound_tm prec a a tg)] f =
         Some tf"
      and t_decomp: "t = tm_comp prec ord I a (mid (compute_bound_tm prec a a tg)) tf tg "
      and c_true:   "c (compute_bound_tm prec I a tg)"
[PROOF STATE]
proof (prove)
using this:
(if c (compute_bound_tm prec I a tg) then map_option (\<lambda>tf. tm_comp prec ord I a (mid (compute_bound_tm prec a a tg)) tf tg) (tm_floatarith prec ord [compute_bound_tm prec I a tg] [mid (compute_bound_tm prec a a tg)] f) else None) = Some t

goal (1 subgoal):
 1. (\<And>tf. \<lbrakk>tm_floatarith prec ord [compute_bound_tm prec I a tg] [mid (compute_bound_tm prec a a tg)] f = Some tf; t = tm_comp prec ord I a (mid (compute_bound_tm prec a a tg)) tf tg; c (compute_bound_tm prec I a tg)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: split_beta' Let_def split: if_splits)
[PROOF STATE]
proof (state)
this:
tm_floatarith prec ord [compute_bound_tm prec I a tg] [mid (compute_bound_tm prec a a tg)] f = Some tf
t = tm_comp prec ord I a (mid (compute_bound_tm prec a a tg)) tf tg
c (compute_bound_tm prec I a tg)

goal (1 subgoal):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm e t
[PROOF STEP]
have a1: "mid (compute_bound_tm prec a a tg) \<in>\<^sub>r (compute_bound_tm prec I a tg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_float (mid (compute_bound_tm prec a a tg)) \<in>\<^sub>r compute_bound_tm prec I a tg
[PROOF STEP]
apply(rule rev_subsetD[OF mid_in_real_interval])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (real_interval (compute_bound_tm prec a a tg)) \<subseteq> set_of (real_interval (compute_bound_tm prec I a tg))
[PROOF STEP]
apply (rule set_of_real_interval_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (compute_bound_tm prec a a tg) \<subseteq> set_of (compute_bound_tm prec I a tg)
[PROOF STEP]
apply (rule compute_bound_tm_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. num_params (tm_poly tg) \<le> length a
 2. a all_subset I
 3. a all_subset a
[PROOF STEP]
using params a
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly tg) \<le> length I
a all_subset I

goal (3 subgoals):
 1. num_params (tm_poly tg) \<le> length a
 2. a all_subset I
 3. a all_subset a
[PROOF STEP]
by (auto simp add: set_of_eq elim!: range_tmD)
[PROOF STATE]
proof (state)
this:
real_of_float (mid (compute_bound_tm prec a a tg)) \<in>\<^sub>r compute_bound_tm prec I a tg

goal (1 subgoal):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm e t
[PROOF STEP]
from \<open>max_Var_floatarith f \<le> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
max_Var_floatarith f \<le> 1
[PROOF STEP]
have [simp]: "\<And>x. 0 \<le> length x \<Longrightarrow> (\<lambda>x. interpret_floatarith f [x ! 0]) x = interpret_floatarith f x"
[PROOF STATE]
proof (prove)
using this:
max_Var_floatarith f \<le> 1

goal (1 subgoal):
 1. \<And>x. 0 \<le> length x \<Longrightarrow> interpret_floatarith f [x ! 0] = interpret_floatarith f x
[PROOF STEP]
by (induction f, simp_all)
[PROOF STATE]
proof (state)
this:
0 \<le> length ?x \<Longrightarrow> interpret_floatarith f [?x ! 0] = interpret_floatarith f ?x

goal (1 subgoal):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm e t
[PROOF STEP]
let ?mid = "real_of_float (mid (compute_bound_tm prec a a tg))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm e t
[PROOF STEP]
have 1: "interpret_floatarith f [x] \<in>\<^sub>i range_tm (\<lambda>_. x - ?mid) tf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm (\<lambda>_. x - real_of_float (mid (compute_bound_tm prec a a tg))) tf
[PROOF STEP]
apply (rule tm_floatarith[OF t1_def, simplified])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. real_of_float (mid (compute_bound_tm prec a a tg)) \<in>\<^sub>r compute_bound_tm prec I a tg
 2. x \<in>\<^sub>r compute_bound_tm prec I a tg
 3. \<And>x. x \<in>\<^sub>r compute_bound_tm prec I a tg \<Longrightarrow> isDERIV 0 f [x]
 4. x - real_of_float (mid (compute_bound_tm prec a a tg)) = x - real_of_float (mid (compute_bound_tm prec a a tg))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_float (mid (compute_bound_tm prec a a tg)) \<in>\<^sub>r compute_bound_tm prec I a tg
[PROOF STEP]
apply (rule rev_subsetD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. real_of_float (mid (compute_bound_tm prec a a tg)) \<in> ?A
 2. ?A \<subseteq> set_of (real_interval (compute_bound_tm prec I a tg))
[PROOF STEP]
apply (rule mid_in_real_interval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (real_interval (compute_bound_tm prec a a tg)) \<subseteq> set_of (real_interval (compute_bound_tm prec I a tg))
[PROOF STEP]
apply (rule set_of_real_interval_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (compute_bound_tm prec a a tg) \<subseteq> set_of (compute_bound_tm prec I a tg)
[PROOF STEP]
apply (rule compute_bound_tm_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. num_params (tm_poly tg) \<le> length a
 2. a all_subset I
 3. a all_subset a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
max_Var_floatarith f \<le> 1
a all_subset I
x \<in>\<^sub>i range_tm e tg
compute_tm_by_comp prec ord I a f (Some tg) c = Some t
\<lbrakk>?x \<in>\<^sub>r compute_bound_tm prec I a tg; c (compute_bound_tm prec I a tg)\<rbrakk> \<Longrightarrow> isDERIV 0 f [?x]
num_params (tm_poly tg) \<le> length I
develops_at_within e a I

goal (3 subgoals):
 1. num_params (tm_poly tg) \<le> length a
 2. a all_subset I
 3. a all_subset a
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. x \<in>\<^sub>r compute_bound_tm prec I a tg
 2. \<And>x. x \<in>\<^sub>r compute_bound_tm prec I a tg \<Longrightarrow> isDERIV 0 f [x]
 3. x - real_of_float (mid (compute_bound_tm prec a a tg)) = x - real_of_float (mid (compute_bound_tm prec a a tg))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>r compute_bound_tm prec I a tg
[PROOF STEP]
by (rule compute_bound_tm_correct assms)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>r compute_bound_tm prec I a tg \<Longrightarrow> isDERIV 0 f [x]
 2. x - real_of_float (mid (compute_bound_tm prec a a tg)) = x - real_of_float (mid (compute_bound_tm prec a a tg))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x_ \<in>\<^sub>r compute_bound_tm prec I a tg \<Longrightarrow> isDERIV 0 f [x_]
[PROOF STEP]
by (auto intro!: assms c_true)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - real_of_float (mid (compute_bound_tm prec a a tg)) = x - real_of_float (mid (compute_bound_tm prec a a tg))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - real_of_float (mid (compute_bound_tm prec a a tg)) = x - real_of_float (mid (compute_bound_tm prec a a tg))
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
interpret_floatarith f [x] \<in>\<^sub>i range_tm (\<lambda>_. x - real_of_float (mid (compute_bound_tm prec a a tg))) tf

goal (1 subgoal):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm e t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm e t
[PROOF STEP]
unfolding t_decomp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm e (tm_comp prec ord I a (mid (compute_bound_tm prec a a tg)) tf tg)
[PROOF STEP]
apply (rule tm_comp_range)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. interpret_floatarith f [x] \<in>\<^sub>i range_tm ?e' tf
 2. ?e' 0 \<in>\<^sub>i range_tm e (tm_sub tg (tm_const (mid (compute_bound_tm prec a a tg))))
 3. num_params (tm_poly tf) \<le> 1
 4. num_params (tm_poly tg) \<le> length I
 5. develops_at_within e a I
[PROOF STEP]
apply (rule 1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. x - real_of_float (mid (compute_bound_tm prec a a tg)) \<in>\<^sub>i range_tm e (tm_sub tg (tm_const (mid (compute_bound_tm prec a a tg))))
 2. num_params (tm_poly tf) \<le> 1
 3. num_params (tm_poly tg) \<le> length I
 4. develops_at_within e a I
[PROOF STEP]
using tm_floatarith_eq_Some_num_params[OF t1_def]
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly tf) \<le> 1

goal (4 subgoals):
 1. x - real_of_float (mid (compute_bound_tm prec a a tg)) \<in>\<^sub>i range_tm e (tm_sub tg (tm_const (mid (compute_bound_tm prec a a tg))))
 2. num_params (tm_poly tf) \<le> 1
 3. num_params (tm_poly tg) \<le> length I
 4. develops_at_within e a I
[PROOF STEP]
by (auto simp: intro!: tm_sub_range assms )
[PROOF STATE]
proof (state)
this:
interpret_floatarith f [x] \<in>\<^sub>i range_tm e t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compute_tm_by_comp_num_params_le:
  assumes "compute_tm_by_comp prec ord I a f (Some t0) i = Some t"
  assumes "1 \<le> X" "num_params (tm_poly t0) \<le> X"
  shows "num_params (tm_poly t) \<le> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly t) \<le> X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
compute_tm_by_comp prec ord I a f (Some t0) i = Some t
1 \<le> X
num_params (tm_poly t0) \<le> X

goal (1 subgoal):
 1. num_params (tm_poly t) \<le> X
[PROOF STEP]
by (auto simp: compute_tm_by_comp.simps Let_def intro!: num_params_tm_comp_le
      dest!: tm_floatarith_eq_Some_num_params
      split: option.splits if_splits)


[STATEMENT]
lemma compute_tm_by_comp_eq_Some_iff: "compute_tm_by_comp prec ord I a f t0 i = Some t \<longleftrightarrow>
  (\<exists>z x2. t0 = Some x2 \<and>
    tm_floatarith prec ord [compute_bound_tm prec I a x2]
      [mid (compute_bound_tm prec a a x2)] f =
      Some z
   \<and> tm_comp prec ord I a
      (mid (compute_bound_tm prec a a x2)) z x2 = t
   \<and> i (compute_bound_tm prec I a x2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (compute_tm_by_comp prec ord I a f t0 i = Some t) = (\<exists>z x2. t0 = Some x2 \<and> tm_floatarith prec ord [compute_bound_tm prec I a x2] [mid (compute_bound_tm prec a a x2)] f = Some z \<and> tm_comp prec ord I a (mid (compute_bound_tm prec a a x2)) z x2 = t \<and> i (compute_bound_tm prec I a x2))
[PROOF STEP]
by (auto simp: compute_tm_by_comp.simps Let_def split: option.splits)