[STATEMENT]
lemma in_interval_realI: "a \<in>\<^sub>i I" if "a \<in>\<^sub>r I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>i I
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
real_of_float a \<in>\<^sub>r I

goal (1 subgoal):
 1. a \<in>\<^sub>i I
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
lemma all_subset_all_inI: "map interval_of a all_subset I" if "a all_in I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map interval_of a all_subset I
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
map real_of_float a all_in I

goal (1 subgoal):
 1. map interval_of a all_subset I
[PROOF STEP]
by (auto simp: in_interval_realI)


[STATEMENT]
lemma compute_tm_by_comp_None: "compute_tm_by_comp p ord I a x None k = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compute_tm_by_comp p ord I a x None k = None
[PROOF STEP]
by (rule ccontr) (auto simp: compute_tm_by_comp_eq_Some_iff)


[STATEMENT]
lemma approx_tm_num_Vars_None:
  assumes "max_Var_floatarith f > length env"
  shows "approx_tm p ord I a f env = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. approx_tm p ord I a f env = None
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length env < max_Var_floatarith f

goal (1 subgoal):
 1. approx_tm p ord I a f env = None
[PROOF STEP]
by (induction f) (auto split: option.splits if_splits simp: max_def compute_tm_by_comp_None)


[STATEMENT]
lemma approx_tm_num_Vars:
  assumes "approx_tm prec ord I a f env = Some t"
  shows "max_Var_floatarith f \<le> length env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatarith f \<le> length env
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> max_Var_floatarith f \<le> length env \<Longrightarrow> False
[PROOF STEP]
using approx_tm_num_Vars_None[of env f prec ord I a] assms
[PROOF STATE]
proof (prove)
using this:
length env < max_Var_floatarith f \<Longrightarrow> approx_tm prec ord I a f env = None
approx_tm prec ord I a f env = Some t

goal (1 subgoal):
 1. \<not> max_Var_floatarith f \<le> length env \<Longrightarrow> False
[PROOF STEP]
by auto