[STATEMENT]
lemma compute_bound_poly_mono:
  assumes "num_params p \<le> length I"
  assumes mem: "I all_subset J" "a all_subset I"
  shows "set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
num_params p \<le> length I

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

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

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (x)\<^sub>p I a) \<subseteq> set_of (compute_bound_poly prec (x)\<^sub>p J a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_of (compute_bound_poly prec (x)\<^sub>p I a) \<subseteq> set_of (compute_bound_poly prec (x)\<^sub>p J a)

goal (7 subgoals):
 1. \<And>x a. num_params (poly.Bound x) \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec (poly.Bound x) I a) \<subseteq> set_of (compute_bound_poly prec (poly.Bound x) J a)
 2. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Add p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Add p1 p2) J a)
 3. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Sub p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Sub p1 p2) J a)
 4. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)
 5. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 6. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 7. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x a. num_params (poly.Bound x) \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec (poly.Bound x) I a) \<subseteq> set_of (compute_bound_poly prec (poly.Bound x) J a)
 2. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Add p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Add p1 p2) J a)
 3. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Sub p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Sub p1 p2) J a)
 4. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)
 5. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 6. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 7. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
case (Bound x)
[PROOF STATE]
proof (state)
this:
num_params (poly.Bound x) \<le> length I

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

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (poly.Bound x) I a) \<subseteq> set_of (compute_bound_poly prec (poly.Bound x) J a)
[PROOF STEP]
using mem
[PROOF STATE]
proof (prove)
using this:
num_params (poly.Bound x) \<le> length I
I all_subset J
a all_subset I

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (poly.Bound x) I a) \<subseteq> set_of (compute_bound_poly prec (poly.Bound x) J a)
[PROOF STEP]
by (simp add: round_interval_mono set_of_sub_inc)
[PROOF STATE]
proof (state)
this:
set_of (compute_bound_poly prec (poly.Bound x) I a) \<subseteq> set_of (compute_bound_poly prec (poly.Bound x) J a)

goal (6 subgoals):
 1. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Add p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Add p1 p2) J a)
 2. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Sub p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Sub p1 p2) J a)
 3. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)
 4. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 5. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 6. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Add p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Add p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Add p1 p2) J a)
 2. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Sub p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Sub p1 p2) J a)
 3. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)
 4. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 5. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 6. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
case (Add p1 p2)
[PROOF STATE]
proof (state)
this:
num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I ?a) \<subseteq> set_of (compute_bound_poly prec p1 J ?a)
num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I ?a) \<subseteq> set_of (compute_bound_poly prec p2 J ?a)
num_params (Add p1 p2) \<le> length I

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

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (Add p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Add p1 p2) J a)
[PROOF STEP]
using mem
[PROOF STATE]
proof (prove)
using this:
num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I ?a) \<subseteq> set_of (compute_bound_poly prec p1 J ?a)
num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I ?a) \<subseteq> set_of (compute_bound_poly prec p2 J ?a)
num_params (Add p1 p2) \<le> length I
I all_subset J
a all_subset I

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (Add p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Add p1 p2) J a)
[PROOF STEP]
by (simp add: round_interval_mono set_of_add_inc)
[PROOF STATE]
proof (state)
this:
set_of (compute_bound_poly prec (Add p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Add p1 p2) J a)

goal (5 subgoals):
 1. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Sub p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Sub p1 p2) J a)
 2. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)
 3. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 4. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 5. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Sub p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Sub p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Sub p1 p2) J a)
 2. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)
 3. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 4. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 5. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
case (Sub p1 p2)
[PROOF STATE]
proof (state)
this:
num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I ?a) \<subseteq> set_of (compute_bound_poly prec p1 J ?a)
num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I ?a) \<subseteq> set_of (compute_bound_poly prec p2 J ?a)
num_params (Sub p1 p2) \<le> length I

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

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (Sub p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Sub p1 p2) J a)
[PROOF STEP]
using mem
[PROOF STATE]
proof (prove)
using this:
num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I ?a) \<subseteq> set_of (compute_bound_poly prec p1 J ?a)
num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I ?a) \<subseteq> set_of (compute_bound_poly prec p2 J ?a)
num_params (Sub p1 p2) \<le> length I
I all_subset J
a all_subset I

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (Sub p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Sub p1 p2) J a)
[PROOF STEP]
by (simp add: round_interval_mono set_of_sub_inc)
[PROOF STATE]
proof (state)
this:
set_of (compute_bound_poly prec (Sub p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Sub p1 p2) J a)

goal (4 subgoals):
 1. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)
 2. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 3. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 4. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>p1 p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (Mul p1 p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)
 2. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 3. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 4. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
case (Mul p1 p2)
[PROOF STATE]
proof (state)
this:
num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I ?a) \<subseteq> set_of (compute_bound_poly prec p1 J ?a)
num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I ?a) \<subseteq> set_of (compute_bound_poly prec p2 J ?a)
num_params (Mul p1 p2) \<le> length I

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

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)
[PROOF STEP]
using mem
[PROOF STATE]
proof (prove)
using this:
num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I ?a) \<subseteq> set_of (compute_bound_poly prec p1 J ?a)
num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I ?a) \<subseteq> set_of (compute_bound_poly prec p2 J ?a)
num_params (Mul p1 p2) \<le> length I
I all_subset J
a all_subset I

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)
[PROOF STEP]
by (simp add: round_interval_mono mult_float_interval_mono')
[PROOF STATE]
proof (state)
this:
set_of (compute_bound_poly prec (Mul p1 p2) I a) \<subseteq> set_of (compute_bound_poly prec (Mul p1 p2) J a)

goal (3 subgoals):
 1. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 2. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 3. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 2. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 3. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
case (Neg p)
[PROOF STATE]
proof (state)
this:
num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I ?a) \<subseteq> set_of (compute_bound_poly prec p J ?a)
num_params (Neg p) \<le> length I

goal (3 subgoals):
 1. \<And>p a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Neg p) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
 2. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 3. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I ?a) \<subseteq> set_of (compute_bound_poly prec p J ?a)
num_params (Neg p) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I ?a) \<subseteq> set_of (compute_bound_poly prec p J ?a)
num_params (Neg p) \<le> length I

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
[PROOF STEP]
using mem
[PROOF STATE]
proof (prove)
using this:
num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I ?a) \<subseteq> set_of (compute_bound_poly prec p J ?a)
num_params (Neg p) \<le> length I
I all_subset J
a all_subset I

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)
[PROOF STEP]
by (simp add: round_interval_mono set_of_neg_inc)
[PROOF STATE]
proof (state)
this:
set_of (compute_bound_poly prec (Neg p) I a) \<subseteq> set_of (compute_bound_poly prec (Neg p) J a)

goal (2 subgoals):
 1. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 2. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 2. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
case (Pw p x2a)
[PROOF STATE]
proof (state)
this:
num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I ?a) \<subseteq> set_of (compute_bound_poly prec p J ?a)
num_params (Pw p x2a) \<le> length I

goal (2 subgoals):
 1. \<And>p x2a a. \<lbrakk>\<And>a. num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I a) \<subseteq> set_of (compute_bound_poly prec p J a); num_params (Pw p x2a) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
 2. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I ?a) \<subseteq> set_of (compute_bound_poly prec p J ?a)
num_params (Pw p x2a) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I ?a) \<subseteq> set_of (compute_bound_poly prec p J ?a)
num_params (Pw p x2a) \<le> length I

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
[PROOF STEP]
using mem
[PROOF STATE]
proof (prove)
using this:
num_params p \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p I ?a) \<subseteq> set_of (compute_bound_poly prec p J ?a)
num_params (Pw p x2a) \<le> length I
I all_subset J
a all_subset I

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)
[PROOF STEP]
by (simp add: power_float_interval_mono)
[PROOF STATE]
proof (state)
this:
set_of (compute_bound_poly prec (Pw p x2a) I a) \<subseteq> set_of (compute_bound_poly prec (Pw p x2a) J a)

goal (1 subgoal):
 1. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
case (CN p1 x2a p2)
[PROOF STATE]
proof (state)
this:
num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I ?a) \<subseteq> set_of (compute_bound_poly prec p1 J ?a)
num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I ?a) \<subseteq> set_of (compute_bound_poly prec p2 J ?a)
num_params (CN p1 x2a p2) \<le> length I

goal (1 subgoal):
 1. \<And>p1 x2a p2 a. \<lbrakk>\<And>a. num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I a) \<subseteq> set_of (compute_bound_poly prec p1 J a); \<And>a. num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I a) \<subseteq> set_of (compute_bound_poly prec p2 J a); num_params (CN p1 x2a p2) \<le> length I\<rbrakk> \<Longrightarrow> set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I ?a) \<subseteq> set_of (compute_bound_poly prec p1 J ?a)
num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I ?a) \<subseteq> set_of (compute_bound_poly prec p2 J ?a)
num_params (CN p1 x2a p2) \<le> length I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I ?a) \<subseteq> set_of (compute_bound_poly prec p1 J ?a)
num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I ?a) \<subseteq> set_of (compute_bound_poly prec p2 J ?a)
num_params (CN p1 x2a p2) \<le> length I

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
using mem
[PROOF STATE]
proof (prove)
using this:
num_params p1 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p1 I ?a) \<subseteq> set_of (compute_bound_poly prec p1 J ?a)
num_params p2 \<le> length I \<Longrightarrow> set_of (compute_bound_poly prec p2 I ?a) \<subseteq> set_of (compute_bound_poly prec p2 J ?a)
num_params (CN p1 x2a p2) \<le> length I
I all_subset J
a all_subset I

goal (1 subgoal):
 1. set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)
[PROOF STEP]
by (simp add: round_interval_mono mult_float_interval_mono'
        set_of_add_inc set_of_sub_inc)
[PROOF STATE]
proof (state)
this:
set_of (compute_bound_poly prec (CN p1 x2a p2) I a) \<subseteq> set_of (compute_bound_poly prec (CN p1 x2a p2) J a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compute_bound_tm_mono:
  fixes I :: "float interval list" and f :: "real list \<Rightarrow> real"
  assumes "num_params (tm_poly t) \<le> length I"
  assumes "I all_subset J"
  assumes "a all_subset I"
  shows "set_of (compute_bound_tm prec I a t) \<subseteq> set_of (compute_bound_tm prec J a t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (compute_bound_tm prec I a t) \<subseteq> set_of (compute_bound_tm prec J a t)
[PROOF STEP]
apply (simp add: compute_bound_tm_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (compute_bound_poly prec (map_poly interval_of (tm_poly t)) I a + tm_bound t) \<subseteq> set_of (compute_bound_poly prec (map_poly interval_of (tm_poly t)) J a + tm_bound t)
[PROOF STEP]
apply (rule set_of_add_inc_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (compute_bound_poly prec (map_poly interval_of (tm_poly t)) I a) \<subseteq> set_of (compute_bound_poly prec (map_poly interval_of (tm_poly t)) J a)
[PROOF STEP]
apply (rule compute_bound_poly_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. num_params (map_poly interval_of (tm_poly t)) \<le> length I
 2. I all_subset J
 3. a all_subset I
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_params (tm_poly t) \<le> length I
I all_subset J
a all_subset I

goal (3 subgoals):
 1. num_params (map_poly interval_of (tm_poly t)) \<le> length I
 2. I all_subset J
 3. a all_subset I
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
lemma zero_real_interval[intro,simp]: "0 \<in>\<^sub>r 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in>\<^sub>r 0
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
lemma range_TM_tm_const[simp]: "range_tm e (tm_const c) = interval_of c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range_tm e (tm_const c) = interval_of (real_of_float c)
[PROOF STEP]
by (auto simp: range_tm_def real_interval_zero tm_const_def)


[STATEMENT]
lemma num_params_tm_const[simp]: "num_params (tm_poly (tm_const c)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly (tm_const c)) = 0
[PROOF STEP]
by (auto simp: tm_const_def)


[STATEMENT]
lemma num_params_tm_pi[simp]: "num_params (tm_poly (tm_pi prec)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_params (tm_poly (tm_pi prec)) = 0
[PROOF STEP]
by (auto simp: tm_pi_def Let_def)


[STATEMENT]
lemma range_tm_tm_pi: "pi \<in>\<^sub>i range_tm e (tm_pi prec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi \<in>\<^sub>i range_tm e (tm_pi prec)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pi \<in>\<^sub>i range_tm e (tm_pi prec)
[PROOF STEP]
have "\<And>prec. real_of_float (lb_pi prec) \<le> real_of_float (ub_pi prec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>prec. real_of_float (lb_pi prec) \<le> real_of_float (ub_pi prec)
[PROOF STEP]
using iffD1[OF atLeastAtMost_iff, OF pi_boundaries]
[PROOF STATE]
proof (prove)
using this:
real_of_float (lb_pi ?n2) \<le> pi \<and> pi \<le> real_of_float (ub_pi ?n2)

goal (1 subgoal):
 1. \<And>prec. real_of_float (lb_pi prec) \<le> real_of_float (ub_pi prec)
[PROOF STEP]
using order_trans
[PROOF STATE]
proof (prove)
using this:
real_of_float (lb_pi ?n2) \<le> pi \<and> pi \<le> real_of_float (ub_pi ?n2)
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z

goal (1 subgoal):
 1. \<And>prec. real_of_float (lb_pi prec) \<le> real_of_float (ub_pi prec)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_float (lb_pi ?prec) \<le> real_of_float (ub_pi ?prec)

goal (1 subgoal):
 1. pi \<in>\<^sub>i range_tm e (tm_pi prec)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_float (lb_pi ?prec) \<le> real_of_float (ub_pi ?prec)
[PROOF STEP]
obtain ivl_pi where ivl_pi_def: "compute_bound_fa prec Pi [] = Some ivl_pi"
[PROOF STATE]
proof (prove)
using this:
real_of_float (lb_pi ?prec) \<le> real_of_float (ub_pi ?prec)

goal (1 subgoal):
 1. (\<And>ivl_pi. compute_bound_fa prec Pi [] = Some ivl_pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: approx.simps)
[PROOF STATE]
proof (state)
this:
compute_bound_fa prec Pi [] = Some ivl_pi

goal (1 subgoal):
 1. pi \<in>\<^sub>i range_tm e (tm_pi prec)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi \<in>\<^sub>i range_tm e (tm_pi prec)
[PROOF STEP]
unfolding range_tm_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly (tm_pi prec)))) + real_interval (tm_bound (tm_pi prec))
[PROOF STEP]
using compute_bound_fa_correct[OF ivl_pi_def, of "[]"]
[PROOF STATE]
proof (prove)
using this:
[] all_in [] \<Longrightarrow> interpret_floatarith Pi [] \<in>\<^sub>r ivl_pi

goal (1 subgoal):
 1. pi \<in>\<^sub>i interval_of (insertion e (map_poly real_of_float (tm_poly (tm_pi prec)))) + real_interval (tm_bound (tm_pi prec))
[PROOF STEP]
by (auto simp: set_of_eq Let_def centered_def ivl_pi_def tm_pi_def
        simp del: compute_bound_fa.simps)
[PROOF STATE]
proof (state)
this:
pi \<in>\<^sub>i range_tm e (tm_pi prec)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isDERIV_DERIV_floatarith:
  assumes "isDERIV v f vs"
  shows "isDERIV v (DERIV_floatarith v f) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV v (DERIV_floatarith v f) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isDERIV v f vs

goal (1 subgoal):
 1. isDERIV v (DERIV_floatarith v f) vs
[PROOF STEP]
proof(induction f)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Add f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Add f1 f2)) vs
 2. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Minus f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Minus f)) vs
 3. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Mult f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Mult f1 f2)) vs
 4. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Inverse f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Inverse f)) vs
 5. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Cos f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Cos f)) vs
 6. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Arctan f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Arctan f)) vs
 7. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Abs f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Abs f)) vs
 8. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Max f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Max f1 f2)) vs
 9. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Min f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Min f1 f2)) vs
 10. isDERIV v Pi vs \<Longrightarrow> isDERIV v (DERIV_floatarith v Pi) vs
A total of 18 subgoals...
[PROOF STEP]
case (Power f m)
[PROOF STATE]
proof (state)
this:
isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs
isDERIV v (Power f m) vs

goal (18 subgoals):
 1. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Add f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Add f1 f2)) vs
 2. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Minus f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Minus f)) vs
 3. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Mult f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Mult f1 f2)) vs
 4. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Inverse f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Inverse f)) vs
 5. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Cos f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Cos f)) vs
 6. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Arctan f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Arctan f)) vs
 7. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Abs f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Abs f)) vs
 8. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Max f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Max f1 f2)) vs
 9. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Min f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Min f1 f2)) vs
 10. isDERIV v Pi vs \<Longrightarrow> isDERIV v (DERIV_floatarith v Pi) vs
A total of 18 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs
isDERIV v (Power f m) vs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs
isDERIV v (Power f m) vs

goal (1 subgoal):
 1. isDERIV v (DERIV_floatarith v (Power f m)) vs
[PROOF STEP]
by (cases m) (auto simp: isDERIV_Power)
[PROOF STATE]
proof (state)
this:
isDERIV v (DERIV_floatarith v (Power f m)) vs

goal (17 subgoals):
 1. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Add f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Add f1 f2)) vs
 2. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Minus f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Minus f)) vs
 3. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Mult f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Mult f1 f2)) vs
 4. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Inverse f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Inverse f)) vs
 5. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Cos f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Cos f)) vs
 6. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Arctan f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Arctan f)) vs
 7. \<And>f. \<lbrakk>isDERIV v f vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f) vs; isDERIV v (Abs f) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Abs f)) vs
 8. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Max f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Max f1 f2)) vs
 9. \<And>f1 f2. \<lbrakk>isDERIV v f1 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f1) vs; isDERIV v f2 vs \<Longrightarrow> isDERIV v (DERIV_floatarith v f2) vs; isDERIV v (Min f1 f2) vs\<rbrakk> \<Longrightarrow> isDERIV v (DERIV_floatarith v (Min f1 f2)) vs
 10. isDERIV v Pi vs \<Longrightarrow> isDERIV v (DERIV_floatarith v Pi) vs
A total of 17 subgoals...
[PROOF STEP]
qed (simp_all add: numeral_eq_Suc add_nonneg_eq_0_iff )


[STATEMENT]
lemma isDERIV_is_analytic:
  "isDERIV i (Taylor_Models.deriv i f n) xs"
  if "isDERIV i f xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV i (local.deriv i f n) xs
[PROOF STEP]
using isDERIV_DERIV_floatarith that
[PROOF STATE]
proof (prove)
using this:
isDERIV ?v ?f ?vs \<Longrightarrow> isDERIV ?v (DERIV_floatarith ?v ?f) ?vs
isDERIV i f xs

goal (1 subgoal):
 1. isDERIV i (local.deriv i f n) xs
[PROOF STEP]
by(induction n) auto


[STATEMENT]
lemma deriv_correct:
  assumes "isDERIV i f (xs[i:=t])" "i < length xs"
  shows "((\<lambda>x. interpret_floatarith (deriv i f n) (xs[i:=x])) has_real_derivative interpret_floatarith (deriv i f (Suc n)) (xs[i:=t]))
    (at t within S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith (local.deriv i f n) (xs[i := x])) has_real_derivative interpret_floatarith (local.deriv i f (Suc n)) (xs[i := t])) (at t within S)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith (local.deriv i f n) (xs[i := x])) has_real_derivative interpret_floatarith (DERIV_floatarith i (local.deriv i f n)) (xs[i := t])) (at t within S)
[PROOF STEP]
apply (rule has_field_derivative_at_within)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith (local.deriv i f n) (xs[i := x])) has_real_derivative interpret_floatarith (DERIV_floatarith i (local.deriv i f n)) (xs[i := t])) (at t)
[PROOF STEP]
apply(rule DERIV_floatarith)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < length xs
 2. isDERIV i (local.deriv i f n) (xs[i := t])
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV i (local.deriv i f n) (xs[i := t])
[PROOF STEP]
apply (rule isDERIV_is_analytic)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV i f (xs[i := t])
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done