[STATEMENT]
lemma tm_lower_order_of_normed_range:
  assumes "x \<in>\<^sub>i range_tm e t"
  assumes dev: "develops_at_within e a I"
  assumes "num_params (tm_poly t) \<le> length I"
  shows "x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
obtain p err where t_decomp: "t = TaylorModel p err"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p err. t = TaylorModel p err \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases t) simp
[PROOF STATE]
proof (state)
this:
t = TaylorModel p err

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
obtain pl pr where p_split: "split_by_degree ord p = (pl, pr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pl pr. split_by_degree ord p = (pl, pr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "split_by_degree ord p", simp)
[PROOF STATE]
proof (state)
this:
split_by_degree ord p = (pl, pr)

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
from split_by_degree_correct_insertion[OF p_split]
[PROOF STATE]
proof (chain)
picking this:
maxdegree pl \<le> ord
insertion ?x (map_poly real_of_float p) = insertion ?x (map_poly real_of_float pl) + insertion ?x (map_poly real_of_float pr)
num_params pl \<le> num_params p
num_params pr \<le> num_params p
[PROOF STEP]
have params: "maxdegree pl \<le> ord" "num_params pl \<le> num_params p" "num_params pr \<le> num_params p"
    and ins: "insertion e (map_poly real_of_float p) =
      insertion e (map_poly real_of_float pl) + insertion e (map_poly real_of_float pr)"
[PROOF STATE]
proof (prove)
using this:
maxdegree pl \<le> ord
insertion ?x (map_poly real_of_float p) = insertion ?x (map_poly real_of_float pl) + insertion ?x (map_poly real_of_float pr)
num_params pl \<le> num_params p
num_params pr \<le> num_params p

goal (1 subgoal):
 1. (maxdegree pl \<le> ord &&& num_params pl \<le> num_params p &&& num_params pr \<le> num_params p) &&& insertion e (map_poly real_of_float p) = insertion e (map_poly real_of_float pl) + insertion e (map_poly real_of_float pr)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maxdegree pl \<le> ord
num_params pl \<le> num_params p
num_params pr \<le> num_params p
insertion e (map_poly real_of_float p) = insertion e (map_poly real_of_float pl) + insertion e (map_poly real_of_float pr)

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
from assms params
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>i range_tm e t
develops_at_within e a I
num_params (tm_poly t) \<le> length I
maxdegree pl \<le> ord
num_params pl \<le> num_params p
num_params pr \<le> num_params p
[PROOF STEP]
have params_pr: "num_params pr \<le> length I"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i range_tm e t
develops_at_within e a I
num_params (tm_poly t) \<le> length I
maxdegree pl \<le> ord
num_params pl \<le> num_params p
num_params pr \<le> num_params p

goal (1 subgoal):
 1. num_params pr \<le> length I
[PROOF STEP]
by (auto simp: t_decomp)
[PROOF STATE]
proof (state)
this:
num_params pr \<le> length I

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
have "range_tm e t =
    interval_of (insertion e (map_poly real_of_float pl)) +
    (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range_tm e t = interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)
[PROOF STEP]
by (auto simp: t_decomp range_tm_def ins ac_simps interval_of_plus)
[PROOF STATE]
proof (state)
this:
range_tm e t = interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
term round_interval
[PROOF STATE]
proof (state)
this:
range_tm e t = interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
range_tm e t = interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
have "set_of \<dots> \<subseteq> set_of (interval_of (insertion e pl)) +
    set_of (real_interval (round_interval prec (err + compute_bound_poly prec pr I a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)) \<subseteq> set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (err + compute_bound_poly prec (map_poly interval_of pr) I a)))
[PROOF STEP]
unfolding set_of_plus real_interval_plus add.commute[of err]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pl))) + (set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err)) \<subseteq> set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (compute_bound_poly prec (map_poly interval_of pr) I a + err)))
[PROOF STEP]
apply (rule set_plus_mono2[OF order_refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> set_of (real_interval (round_interval prec (compute_bound_poly prec (map_poly interval_of pr) I a + err)))
[PROOF STEP]
apply (rule order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> ?y3
 2. ?y3 \<subseteq> set_of (real_interval (round_interval prec (compute_bound_poly prec (map_poly interval_of pr) I a + err)))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ?y3 \<subseteq> set_of (real_interval (round_interval prec (compute_bound_poly prec (map_poly interval_of pr) I a + err)))
 2. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> ?y3
[PROOF STEP]
apply (rule set_of_real_interval_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set_of ?x6 \<subseteq> set_of (round_interval prec (compute_bound_poly prec (map_poly interval_of pr) I a + err))
 2. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> set_of (real_interval ?x6)
[PROOF STEP]
apply (rule round_ivl_correct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> set_of (real_interval (compute_bound_poly prec (map_poly interval_of pr) I a + err))
[PROOF STEP]
unfolding set_of_plus real_interval_plus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> set_of (real_interval (compute_bound_poly prec (map_poly interval_of pr) I a)) + set_of (real_interval err)
[PROOF STEP]
apply (rule set_plus_mono2[OF _ order_refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pr))) \<subseteq> set_of (real_interval (compute_bound_poly prec (map_poly interval_of pr) I a))
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float pr)) \<Longrightarrow> x \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of pr) I a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (map_poly real_of_float pr) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of pr) I a
[PROOF STEP]
apply (rule compute_bound_poly_correct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. num_params pr \<le> length I
 2. develops_at_within e a I
[PROOF STEP]
apply (rule params_pr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. develops_at_within e a I
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
this:
set_of (interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)) \<subseteq> set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (err + compute_bound_poly prec (map_poly interval_of pr) I a)))

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_of (interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)) \<subseteq> set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (err + compute_bound_poly prec (map_poly interval_of pr) I a)))

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
have "\<dots> = set_of (range_tm e (tm_lower_order_of_normed prec ord I a t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (err + compute_bound_poly prec (map_poly interval_of pr) I a))) = set_of (range_tm e (tm_lower_order_of_normed prec ord I a t))
[PROOF STEP]
by (simp add: t_decomp split_beta' Let_def p_split range_tm_def set_of_plus)
[PROOF STATE]
proof (state)
this:
set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (err + compute_bound_poly prec (map_poly interval_of pr) I a))) = set_of (range_tm e (tm_lower_order_of_normed prec ord I a t))

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set_of (range_tm e t) \<subseteq> set_of (range_tm e (tm_lower_order_of_normed prec ord I a t))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set_of (range_tm e t) \<subseteq> set_of (range_tm e (tm_lower_order_of_normed prec ord I a t))

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set_of (range_tm e t) \<subseteq> set_of (range_tm e (tm_lower_order_of_normed prec ord I a t))
x \<in>\<^sub>i range_tm e t
develops_at_within e a I
num_params (tm_poly t) \<le> length I

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>i range_tm e (tm_lower_order_of_normed prec ord I a t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma num_params_tm_norm_poly_le: "num_params (tm_poly (tm_norm_poly t)) \<le> X"
  if "num_params (tm_poly t) \<le> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly (tm_norm_poly 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_norm_poly t)) \<le> X
[PROOF STEP]
by (cases t) (auto simp: intro!: num_params_polynate[THEN order_trans])


[STATEMENT]
lemma tm_lower_order_range:
  assumes "x \<in>\<^sub>i range_tm e t"
  assumes dev: "develops_at_within e a I"
  assumes "num_params (tm_poly t) \<le> length I"
  shows "x \<in>\<^sub>i range_tm e (tm_lower_order prec ord I a t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_lower_order prec ord I a t)
[PROOF STEP]
by (auto simp add: intro!: tm_lower_order_of_normed_range tm_norm_poly_range assms
      num_params_tm_norm_poly_le)


[STATEMENT]
lemma tm_round_floats_of_normed_range:
  assumes "x \<in>\<^sub>i range_tm e t"
  assumes dev: "develops_at_within e a I"
  assumes "num_params (tm_poly t) \<le> length I"
  shows "x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)"
    \<comment> \<open>TODO: this is a clone of @{thm tm_lower_order_of_normed_range} -> general sweeping method!\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
obtain p err where t_decomp: "t = TaylorModel p err"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p err. t = TaylorModel p err \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases t) simp
[PROOF STATE]
proof (state)
this:
t = TaylorModel p err

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
obtain pl pr where p_prec: "split_by_prec prec p = (pl, pr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pl pr. split_by_prec prec p = (pl, pr) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "split_by_prec prec p", simp)
[PROOF STATE]
proof (state)
this:
split_by_prec prec p = (pl, pr)

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
from split_by_prec_correct_insertion[OF p_prec]
[PROOF STATE]
proof (chain)
picking this:
insertion ?x (map_poly real_of_float p) = insertion ?x (map_poly real_of_float pl) + insertion ?x (map_poly real_of_float pr)
num_params pl \<le> num_params p
num_params pr \<le> num_params p
[PROOF STEP]
have params: "num_params pl \<le> num_params p" "num_params pr \<le> num_params p"
    and ins: "insertion e (map_poly real_of_float p) =
      insertion e (map_poly real_of_float pl) + insertion e (map_poly real_of_float pr)"
[PROOF STATE]
proof (prove)
using this:
insertion ?x (map_poly real_of_float p) = insertion ?x (map_poly real_of_float pl) + insertion ?x (map_poly real_of_float pr)
num_params pl \<le> num_params p
num_params pr \<le> num_params p

goal (1 subgoal):
 1. (num_params pl \<le> num_params p &&& num_params pr \<le> num_params p) &&& insertion e (map_poly real_of_float p) = insertion e (map_poly real_of_float pl) + insertion e (map_poly real_of_float pr)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
num_params pl \<le> num_params p
num_params pr \<le> num_params p
insertion e (map_poly real_of_float p) = insertion e (map_poly real_of_float pl) + insertion e (map_poly real_of_float pr)

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
from assms params
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>i range_tm e t
develops_at_within e a I
num_params (tm_poly t) \<le> length I
num_params pl \<le> num_params p
num_params pr \<le> num_params p
[PROOF STEP]
have params_pr: "num_params pr \<le> length I"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i range_tm e t
develops_at_within e a I
num_params (tm_poly t) \<le> length I
num_params pl \<le> num_params p
num_params pr \<le> num_params p

goal (1 subgoal):
 1. num_params pr \<le> length I
[PROOF STEP]
by (auto simp: t_decomp)
[PROOF STATE]
proof (state)
this:
num_params pr \<le> length I

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
have "range_tm e t =
    interval_of (insertion e (map_poly real_of_float pl)) +
    (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range_tm e t = interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)
[PROOF STEP]
by (auto simp: t_decomp range_tm_def ins ac_simps interval_of_plus)
[PROOF STATE]
proof (state)
this:
range_tm e t = interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
range_tm e t = interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
have "set_of \<dots> \<subseteq> set_of (interval_of (insertion e pl)) +
    set_of (real_interval (round_interval prec (err + compute_bound_poly prec pr I a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)) \<subseteq> set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (err + compute_bound_poly prec (map_poly interval_of pr) I a)))
[PROOF STEP]
unfolding set_of_plus real_interval_plus add.commute[of err]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pl))) + (set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err)) \<subseteq> set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (compute_bound_poly prec (map_poly interval_of pr) I a + err)))
[PROOF STEP]
apply (rule set_plus_mono2[OF order_refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> set_of (real_interval (round_interval prec (compute_bound_poly prec (map_poly interval_of pr) I a + err)))
[PROOF STEP]
apply (rule order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> ?y3
 2. ?y3 \<subseteq> set_of (real_interval (round_interval prec (compute_bound_poly prec (map_poly interval_of pr) I a + err)))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ?y3 \<subseteq> set_of (real_interval (round_interval prec (compute_bound_poly prec (map_poly interval_of pr) I a + err)))
 2. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> ?y3
[PROOF STEP]
apply (rule set_of_real_interval_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set_of ?x6 \<subseteq> set_of (round_interval prec (compute_bound_poly prec (map_poly interval_of pr) I a + err))
 2. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> set_of (real_interval ?x6)
[PROOF STEP]
apply (rule round_ivl_correct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> set_of (real_interval (compute_bound_poly prec (map_poly interval_of pr) I a + err))
[PROOF STEP]
unfolding set_of_plus real_interval_plus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pr))) + set_of (real_interval err) \<subseteq> set_of (real_interval (compute_bound_poly prec (map_poly interval_of pr) I a)) + set_of (real_interval err)
[PROOF STEP]
apply (rule set_plus_mono2[OF _ order_refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pr))) \<subseteq> set_of (real_interval (compute_bound_poly prec (map_poly interval_of pr) I a))
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float pr)) \<Longrightarrow> x \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of pr) I a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (map_poly real_of_float pr) \<in>\<^sub>r compute_bound_poly prec (map_poly interval_of pr) I a
[PROOF STEP]
apply (rule compute_bound_poly_correct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. num_params pr \<le> length I
 2. develops_at_within e a I
[PROOF STEP]
apply (rule params_pr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. develops_at_within e a I
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
this:
set_of (interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)) \<subseteq> set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (err + compute_bound_poly prec (map_poly interval_of pr) I a)))

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_of (interval_of (insertion e (map_poly real_of_float pl)) + (interval_of (insertion e (map_poly real_of_float pr)) + real_interval err)) \<subseteq> set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (err + compute_bound_poly prec (map_poly interval_of pr) I a)))

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
have "\<dots> = set_of (range_tm e (tm_round_floats_of_normed prec I a t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (err + compute_bound_poly prec (map_poly interval_of pr) I a))) = set_of (range_tm e (tm_round_floats_of_normed prec I a t))
[PROOF STEP]
by (simp add: t_decomp split_beta' Let_def p_prec range_tm_def set_of_plus)
[PROOF STATE]
proof (state)
this:
set_of (interval_of (insertion e (map_poly real_of_float pl))) + set_of (real_interval (round_interval prec (err + compute_bound_poly prec (map_poly interval_of pr) I a))) = set_of (range_tm e (tm_round_floats_of_normed prec I a t))

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set_of (range_tm e t) \<subseteq> set_of (range_tm e (tm_round_floats_of_normed prec I a t))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set_of (range_tm e t) \<subseteq> set_of (range_tm e (tm_round_floats_of_normed prec I a t))

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set_of (range_tm e t) \<subseteq> set_of (range_tm e (tm_round_floats_of_normed prec I a t))
x \<in>\<^sub>i range_tm e t
develops_at_within e a I
num_params (tm_poly t) \<le> length I

goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>i range_tm e (tm_round_floats_of_normed prec I a t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma num_params_split_by_degree_le: "num_params (fst (split_by_degree ord x)) \<le> K"
  "num_params (snd (split_by_degree ord x)) \<le> K"
  if "num_params x \<le> K" for x::"float poly"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (fst (split_by_degree ord x)) \<le> K &&& num_params (snd (split_by_degree ord x)) \<le> K
[PROOF STEP]
using split_by_degree_correct_insertion(3,4)[of ord x, OF surjective_pairing] that
[PROOF STATE]
proof (prove)
using this:
num_params (fst (split_by_degree ord x)) \<le> num_params x
num_params (snd (split_by_degree ord x)) \<le> num_params x
num_params x \<le> K

goal (1 subgoal):
 1. num_params (fst (split_by_degree ord x)) \<le> K &&& num_params (snd (split_by_degree ord x)) \<le> K
[PROOF STEP]
by auto


[STATEMENT]
lemma num_params_split_by_prec_le: "num_params (fst (split_by_prec ord x)) \<le> K"
  "num_params (snd (split_by_prec ord x)) \<le> K"
  if "num_params x \<le> K" for x::"float poly"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (fst (split_by_prec ord x)) \<le> K &&& num_params (snd (split_by_prec ord x)) \<le> K
[PROOF STEP]
using split_by_prec_correct_insertion(2,3)[of ord x, OF surjective_pairing] that
[PROOF STATE]
proof (prove)
using this:
num_params (fst (split_by_prec ord x)) \<le> num_params x
num_params (snd (split_by_prec ord x)) \<le> num_params x
num_params x \<le> K

goal (1 subgoal):
 1. num_params (fst (split_by_prec ord x)) \<le> K &&& num_params (snd (split_by_prec ord x)) \<le> K
[PROOF STEP]
by auto


[STATEMENT]
lemma num_params_tm_norm'_le:
  "num_params (tm_poly (tm_round_floats_of_normed 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_round_floats_of_normed 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_round_floats_of_normed prec I a t)) \<le> X
[PROOF STEP]
by (cases t) (auto simp: tm_norm'.simps split_beta' Let_def intro!: num_params_split_by_prec_le)


[STATEMENT]
lemma tm_round_floats_range:
  assumes "x \<in>\<^sub>i range_tm e t" "develops_at_within e a I" "num_params (tm_poly t) \<le> length I"
  shows "x \<in>\<^sub>i range_tm e (tm_round_floats prec I a t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_round_floats prec I a t)
[PROOF STEP]
by (auto intro!: tm_round_floats_of_normed_range assms tm_norm_poly_range num_params_tm_norm_poly_le)


[STATEMENT]
lemma num_params_tm_lower_order_of_normed_le: "num_params (tm_poly (tm_lower_order_of_normed prec ord 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_lower_order_of_normed prec ord 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_lower_order_of_normed prec ord I a t)) \<le> X
[PROOF STEP]
apply (cases t)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>num_params (tm_poly t) \<le> X; t = TaylorModel x1 x2\<rbrakk> \<Longrightarrow> num_params (tm_poly (tm_lower_order_of_normed prec ord I a t)) \<le> X
[PROOF STEP]
apply (auto simp: split_beta' Let_def intro!: num_params_polynate[THEN order_trans])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>num_params x1 \<le> X; t = TaylorModel x1 x2\<rbrakk> \<Longrightarrow> num_params (fst (split_by_degree ord x1)) \<le> X
[PROOF STEP]
apply (rule order_trans[OF split_by_degree_correct(3)])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>num_params x1 \<le> X; t = TaylorModel x1 x2\<rbrakk> \<Longrightarrow> (fst (split_by_degree ord x1), ?r3 x1 x2) = split_by_degree (?ord3 x1 x2) (?p3 x1 x2)
 2. \<And>x1 x2. \<lbrakk>num_params x1 \<le> X; t = TaylorModel x1 x2\<rbrakk> \<Longrightarrow> num_params (?p3 x1 x2) \<le> X
[PROOF STEP]
by (auto simp: prod_eq_iff)


[STATEMENT]
lemma tm_norm'_range:
  assumes "x \<in>\<^sub>i range_tm e t" "develops_at_within e a I" "num_params (tm_poly t) \<le> length I"
  shows "x \<in>\<^sub>i range_tm e (tm_norm' prec ord I a t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_norm' prec ord I a t)
[PROOF STEP]
by (auto intro!: tm_round_floats_of_normed_range tm_lower_order_of_normed_range assms
      num_params_tm_norm_poly_le num_params_tm_lower_order_of_normed_le
      simp: tm_norm'.simps)


[STATEMENT]
lemma num_params_tm_norm':
  "num_params (tm_poly (tm_norm' prec ord 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_norm' prec ord 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_norm' prec ord I a t)) \<le> X
[PROOF STEP]
by (cases t) (auto simp: tm_norm'.simps split_beta' Let_def
      intro!: num_params_tm_norm'_le num_params_split_by_prec_le num_params_split_by_degree_le)


[STATEMENT]
lemma tm_norm_range:
  assumes "x \<in>\<^sub>i range_tm e t" "develops_at_within e a I" "num_params (tm_poly t) \<le> length I"
  shows "x \<in>\<^sub>i range_tm e (tm_norm prec ord I a t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in>\<^sub>i range_tm e (tm_norm prec ord I a t)
[PROOF STEP]
by (auto intro!: assms tm_norm'_range tm_norm_poly_range num_params_tm_norm_poly_le)


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

goal (1 subgoal):
 1. - x \<in>\<^sub>i range_tm e (tm_neg t)
[PROOF STEP]
by (cases t)
    (auto simp: set_of_eq range_tm_def interval_of_plus interval_of_uminus map_poly_homo_polyneg)


[STATEMENT]
lemma tm_bound_tm_add[simp]: "tm_bound (tm_add t1 t2) = tm_bound t1 + tm_bound t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tm_bound (tm_add t1 t2) = tm_bound t1 + tm_bound t2
[PROOF STEP]
by (cases t1; cases t2) auto


[STATEMENT]
lemma interval_of_add: "interval_of (a + b) = interval_of a + interval_of b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interval_of (a + b) = interval_of a + interval_of b
[PROOF STEP]
by (auto intro!: interval_eqI)


[STATEMENT]
lemma tm_sub_range:
  assumes "x \<in>\<^sub>i range_tm e t1"
  assumes "y \<in>\<^sub>i range_tm e t2"
  shows "x - y \<in>\<^sub>i range_tm e (tm_sub t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - y \<in>\<^sub>i range_tm e (tm_sub t1 t2)
[PROOF STEP]
using tm_add_range[OF assms(1) tm_neg_range[OF assms(2)]]
[PROOF STATE]
proof (prove)
using this:
x + - y \<in>\<^sub>i range_tm e (tm_add t1 (tm_neg t2))

goal (1 subgoal):
 1. x - y \<in>\<^sub>i range_tm e (tm_sub t1 t2)
[PROOF STEP]
by simp


[STATEMENT]
lemma set_of_intervalI: "set_of (interval_of y) \<subseteq> set_of Y" if "y \<in>\<^sub>i Y" for y::"'a::order"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of y) \<subseteq> set_of Y
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
y \<in>\<^sub>i Y

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


[STATEMENT]
lemma set_of_real_intervalI: "set_of (interval_of y) \<subseteq> set_of (real_interval Y)" if "y \<in>\<^sub>r Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (interval_of y) \<subseteq> set_of (real_interval Y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
y \<in>\<^sub>r Y

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


[STATEMENT]
lemma tm_mul_range:
  assumes "x \<in>\<^sub>i range_tm e t1"
  assumes "y \<in>\<^sub>i range_tm e t2"
  assumes dev: "develops_at_within e a I"
  assumes params: "num_params (tm_poly t1) \<le> length I" "num_params (tm_poly t2) \<le> length I"
  shows "x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
define p1 where "p1 = tm_poly t1"
[PROOF STATE]
proof (state)
this:
p1 = tm_poly t1

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
define p2 where "p2 = tm_poly t2"
[PROOF STATE]
proof (state)
this:
p2 = tm_poly t2

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
define e1 where "e1 = tm_bound t1"
[PROOF STATE]
proof (state)
this:
e1 = tm_bound t1

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
define e2 where "e2 = tm_bound t2"
[PROOF STATE]
proof (state)
this:
e2 = tm_bound t2

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
have t1_def: "t1 = TaylorModel p1 e1" and t2_def: "t2 = TaylorModel p2 e2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t1 = TaylorModel p1 e1 &&& t2 = TaylorModel p2 e2
[PROOF STEP]
by (auto simp: p1_def e1_def p2_def e2_def)
[PROOF STATE]
proof (state)
this:
t1 = TaylorModel p1 e1
t2 = TaylorModel p2 e2

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
from params
[PROOF STATE]
proof (chain)
picking this:
num_params (tm_poly t1) \<le> length I
num_params (tm_poly t2) \<le> length I
[PROOF STEP]
have params: "num_params p1 \<le> length I" "num_params p2 \<le> length I"
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly t1) \<le> length I
num_params (tm_poly t2) \<le> length I

goal (1 subgoal):
 1. num_params p1 \<le> length I &&& num_params p2 \<le> length I
[PROOF STEP]
by (auto simp: p1_def p2_def)
[PROOF STATE]
proof (state)
this:
num_params p1 \<le> length I
num_params p2 \<le> length I

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
from range_tmD[OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t1))) + real_interval (tm_bound t1)
[PROOF STEP]
obtain xe where x: "x = insertion e p1 + xe"
    (is "_ = ?x' + _")
    and xe: "xe \<in>\<^sub>r e1"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t1))) + real_interval (tm_bound t1)

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

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
from range_tmD[OF assms(2)]
[PROOF STATE]
proof (chain)
picking this:
y \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t2))) + real_interval (tm_bound t2)
[PROOF STEP]
obtain ye where y: "y = insertion e p2 + ye"
    (is "_ = ?y' + _")
    and ye: "ye \<in>\<^sub>r e2"
[PROOF STATE]
proof (prove)
using this:
y \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly t2))) + real_interval (tm_bound t2)

goal (1 subgoal):
 1. (\<And>ye. \<lbrakk>y = insertion e (map_poly real_of_float p2) + ye; ye \<in>\<^sub>r e2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: p2_def e2_def elim!: plus_in_intervalE)
[PROOF STATE]
proof (state)
this:
y = insertion e (map_poly real_of_float p2) + ye
ye \<in>\<^sub>r e2

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
have "x * y = insertion e (p1 *\<^sub>p p2) + (xe * ?y' + ?x' * ye + xe * ye)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y = insertion e (map_poly real_of_float (p1 *\<^sub>p p2)) + (xe * insertion e (map_poly real_of_float p2) + insertion e (map_poly real_of_float p1) * ye + xe * ye)
[PROOF STEP]
by (simp add: algebra_simps x y map_poly_homo_polymul)
[PROOF STATE]
proof (state)
this:
x * y = insertion e (map_poly real_of_float (p1 *\<^sub>p p2)) + (xe * insertion e (map_poly real_of_float p2) + insertion e (map_poly real_of_float p1) * ye + xe * ye)

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * y = insertion e (map_poly real_of_float (p1 *\<^sub>p p2)) + (xe * insertion e (map_poly real_of_float p2) + insertion e (map_poly real_of_float p1) * ye + xe * ye)

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
have "\<dots> \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion e (map_poly real_of_float (p1 *\<^sub>p p2)) + (xe * insertion e (map_poly real_of_float p2) + insertion e (map_poly real_of_float p1) * ye + xe * ye) \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
by (auto intro!: tm_round_floats_of_normed_range assms tm_norm'_range
        simp: split_beta' Let_def t1_def t2_def)
     (auto simp: range_tm_def real_interval_plus real_interval_times intro!: plus_in_intervalI
        times_in_intervalI xe ye params compute_bound_poly_correct dev
        num_params_polymul[THEN order_trans])
[PROOF STATE]
proof (state)
this:
insertion e (map_poly real_of_float (p1 *\<^sub>p p2)) + (xe * insertion e (map_poly real_of_float p2) + insertion e (map_poly real_of_float p1) * ye + xe * ye) \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)

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

goal (1 subgoal):
 1. x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x * y \<in>\<^sub>i range_tm e (tm_mul prec ord I a t1 t2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma num_params_tm_mul_le:
  "num_params (tm_poly (tm_mul prec ord 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_mul prec ord 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_mul prec ord I a t1 t2)) \<le> X
[PROOF STEP]
by (cases t1; cases t2)
     (auto simp: intro!: num_params_tm_norm' num_params_polymul[THEN order_trans])


[STATEMENT]
lemma num_params_tm_add_le:
  "num_params (tm_poly (tm_add 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_add 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_add t1 t2)) \<le> X
[PROOF STEP]
by (cases t1; cases t2)
     (auto simp: tm_add.simps
       intro!: num_params_tm_norm' num_params_polymul[THEN order_trans]
       num_params_polyadd[THEN order_trans])


[STATEMENT]
lemma num_params_tm_neg_eq[simp]:
  "num_params (tm_poly (tm_neg t1)) = num_params (tm_poly t1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly (tm_neg t1)) = num_params (tm_poly t1)
[PROOF STEP]
by (cases t1) (auto simp: tm_neg.simps num_params_polyneg)


[STATEMENT]
lemma num_params_tm_sub_le:
  "num_params (tm_poly (tm_sub 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_sub 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_sub t1 t2)) \<le> X
[PROOF STEP]
by (cases t1; cases t2) (auto simp: tm_sub.simps intro!: num_params_tm_add_le)


[STATEMENT]
lemma num_params_eval_poly_le: "num_params (tm_poly (eval_poly_at_tm prec ord I a p t)) \<le> x"
  if "num_params (tm_poly t) \<le> x" "num_params p \<le> max 1 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly (eval_poly_at_tm prec ord I a p t)) \<le> x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly t) \<le> x
num_params p \<le> max 1 x

goal (1 subgoal):
 1. num_params (tm_poly (eval_poly_at_tm prec ord I a p t)) \<le> x
[PROOF STEP]
by (induction prec ord I a p t rule: eval_poly_at_tm.induct)
    (auto intro!: num_params_tm_add_le num_params_tm_sub_le num_params_tm_mul_le
      num_params_tm_pow_le)