[STATEMENT]
lemma subst_floatarith_eq_Num[simp]: "(subst_floatarith (\<lambda>x. Var (s x)) fa = Num x) \<longleftrightarrow> fa = Num x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (subst_floatarith (\<lambda>x. Var (s x)) fa = Num x) = (fa = Num x)
[PROOF STEP]
by (induction fa) auto


[STATEMENT]
lemma fold_const_fa_subst_eq_Num0_iff[simp]:
  "fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = Num x \<longleftrightarrow> fold_const_fa fa = Num x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fold_const_fa (subst_floatarith (\<lambda>x. Var (s x)) fa) = Num x) = (fold_const_fa fa = Num x)
[PROOF STEP]
unfolding subst_floatarith_Var_fold_const_fa[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (subst_floatarith (\<lambda>x. Var (s x)) (fold_const_fa fa) = Num x) = (fold_const_fa fa = Num x)
[PROOF STEP]
by simp


[STATEMENT]
lemma subst_floatarith_Var_FDERIV_floatarith:
  assumes len: "length xs = DIM('a::executable_euclidean_space)" and [simp]: "length ds = DIM('a)"
  assumes eq: "\<And>x y. x \<in> set xs \<Longrightarrow> (y = x) = (s y = x)"
  shows "subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_floatarith fa xs ds) =
    (FDERIV_floatarith (subst_floatarith (\<lambda>x. Var (s x)) fa) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_floatarith fa xs ds) = FDERIV_floatarith (subst_floatarith (\<lambda>x. Var (s x)) fa) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_floatarith fa xs ds) = FDERIV_floatarith (subst_floatarith (\<lambda>x. Var (s x)) fa) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds)
[PROOF STEP]
have [simp]: "\<And>x. x \<in> set xs \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith x fa1) =
    (DERIV_floatarith x (subst_floatarith (\<lambda>x. Var (s x)) fa1))"
    for fa1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith x fa1) = DERIV_floatarith x (subst_floatarith (\<lambda>x. Var (s x)) fa1)
[PROOF STEP]
by (rule subst_floatarith_Var_DERIV_floatarith) (rule eq)
[PROOF STATE]
proof (state)
this:
?x \<in> set xs \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (DERIV_floatarith ?x ?fa1.1) = DERIV_floatarith ?x (subst_floatarith (\<lambda>x. Var (s x)) ?fa1.1)

goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_floatarith fa xs ds) = FDERIV_floatarith (subst_floatarith (\<lambda>x. Var (s x)) fa) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds)
[PROOF STEP]
have map_eq: "(map (\<lambda>xa. if xa = s x then Num 1 else Num 0) xs) =
      (map (\<lambda>xa. if xa = x then Num 1 else Num 0) xs)"
    for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>xa. if xa = s x then Num 1 else Num 0) xs = map (\<lambda>xa. if xa = x then Num 1 else Num 0) xs
[PROOF STEP]
apply (subst map_eq_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xa\<in>set xs. (if xa = s x then Num 1 else Num 0) = (if xa = x then Num 1 else Num 0)
[PROOF STEP]
using eq[of x x] eq[of "s x"]
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs \<Longrightarrow> (x = x) = (s x = x)
s x \<in> set xs \<Longrightarrow> (?y = s x) = (s ?y = s x)

goal (1 subgoal):
 1. \<forall>xa\<in>set xs. (if xa = s x then Num 1 else Num 0) = (if xa = x then Num 1 else Num 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (\<lambda>xa. if xa = s ?x then Num 1 else Num 0) xs = map (\<lambda>xa. if xa = ?x then Num 1 else Num 0) xs

goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_floatarith fa xs ds) = FDERIV_floatarith (subst_floatarith (\<lambda>x. Var (s x)) fa) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_floatarith fa xs ds) = FDERIV_floatarith (subst_floatarith (\<lambda>x. Var (s x)) fa) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds)
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
length xs = DIM('a)

goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_floatarith fa xs ds) = FDERIV_floatarith (subst_floatarith (\<lambda>x. Var (s x)) fa) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds)
[PROOF STEP]
by (induction fa)
      (auto simp: FDERIV_floatarith_def o_def if_distrib
        subst_floatarith_Var_fold_const_fa fold_const_fa.simps(18) map_eq
        cong: map_cong if_cong)
[PROOF STATE]
proof (state)
this:
subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_floatarith fa xs ds) = FDERIV_floatarith (subst_floatarith (\<lambda>x. Var (s x)) fa) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_floatarith_Var_FDERIV_n_nth:
  assumes len: "length xs = DIM('a::executable_euclidean_space)" and [simp]: "length ds = DIM('a)"
  assumes eq: "\<And>x y. x \<in> set xs \<Longrightarrow> (y = x) = (s y = x)"
  assumes [simp]: "i < length fas"
  shows "subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds n ! i) =
    (FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) n ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds n ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) n ! i
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds 0 ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) 0 ! i
 2. \<And>n. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds n ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) n ! i \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds (Suc n) ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) (Suc n) ! i
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds n ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) n ! i

goal (2 subgoals):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds 0 ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) 0 ! i
 2. \<And>n. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds n ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) n ! i \<Longrightarrow> subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds (Suc n) ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) (Suc n) ! i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds (Suc n) ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) (Suc n) ! i
[PROOF STEP]
by (simp add: subst_floatarith_Var_FDERIV_floatarith[OF len _ eq] Suc.IH[symmetric])
[PROOF STATE]
proof (state)
this:
subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds (Suc n) ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) (Suc n) ! i

goal (1 subgoal):
 1. subst_floatarith (\<lambda>x. Var (s x)) (FDERIV_n_floatariths fas xs ds 0 ! i) = FDERIV_n_floatariths (map (subst_floatarith (\<lambda>x. Var (s x))) fas) xs (map (subst_floatarith (\<lambda>x. Var (s x))) ds) 0 ! i
[PROOF STEP]
qed simp


[STATEMENT]
lemma subst_floatarith_Var_max_Var_floatarith:
  assumes "\<And>i. i < max_Var_floatarith fa \<Longrightarrow> s i = i"
  shows "subst_floatarith (\<lambda>i. Var (s i)) fa = fa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_floatarith (\<lambda>i. Var (s i)) fa = fa
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i < max_Var_floatarith fa \<Longrightarrow> s ?i = ?i

goal (1 subgoal):
 1. subst_floatarith (\<lambda>i. Var (s i)) fa = fa
[PROOF STEP]
by (induction fa) auto


[STATEMENT]
lemma interpret_floatarith_subst_floatarith_idem:
  assumes mv: "max_Var_floatarith fa \<le> length vs"
  assumes idem: "\<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j"
  shows "interpret_floatarith (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = interpret_floatarith fa vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = interpret_floatarith fa vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
max_Var_floatarith fa \<le> length vs
?j < max_Var_floatarith fa \<Longrightarrow> vs ! s ?j = vs ! ?j

goal (1 subgoal):
 1. interpret_floatarith (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = interpret_floatarith fa vs
[PROOF STEP]
by (induction fa) auto


[STATEMENT]
lemma isDERIV_subst_Var_floatarith:
  assumes mv: "max_Var_floatarith fa \<le> length vs"
  assumes idem: "\<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j"
  assumes "\<And>j. s j = i \<longleftrightarrow> j = i"
  shows "isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs
[PROOF STEP]
using mv idem
[PROOF STATE]
proof (prove)
using this:
max_Var_floatarith fa \<le> length vs
?j < max_Var_floatarith fa \<Longrightarrow> vs ! s ?j = vs ! ?j

goal (1 subgoal):
 1. isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs
[PROOF STEP]
proof (induction fa)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Add fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Add fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Add fa1 fa2)) vs = isDERIV i (Add fa1 fa2) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Minus fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Minus fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Minus fa)) vs = isDERIV i (Minus fa) vs
 3. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Mult fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Mult fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Mult fa1 fa2)) vs = isDERIV i (Mult fa1 fa2) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Inverse fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Inverse fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Inverse fa)) vs = isDERIV i (Inverse fa) vs
 5. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Cos fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Cos fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Cos fa)) vs = isDERIV i (Cos fa) vs
 6. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Arctan fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Arctan fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Arctan fa)) vs = isDERIV i (Arctan fa) vs
 7. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Abs fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Abs fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Abs fa)) vs = isDERIV i (Abs fa) vs
 8. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Max fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Max fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Max fa1 fa2)) vs = isDERIV i (Max fa1 fa2) vs
 9. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Min fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Min fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Min fa1 fa2)) vs = isDERIV i (Min fa1 fa2) vs
 10. \<lbrakk>max_Var_floatarith Pi \<le> length vs; \<And>j. j < max_Var_floatarith Pi \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) Pi) vs = isDERIV i Pi vs
A total of 18 subgoals...
[PROOF STEP]
case (Power fa n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs
max_Var_floatarith (fa ^\<^sub>e n) \<le> length vs
?j < max_Var_floatarith (fa ^\<^sub>e n) \<Longrightarrow> vs ! s ?j = vs ! ?j

goal (18 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Add fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Add fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Add fa1 fa2)) vs = isDERIV i (Add fa1 fa2) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Minus fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Minus fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Minus fa)) vs = isDERIV i (Minus fa) vs
 3. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Mult fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Mult fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Mult fa1 fa2)) vs = isDERIV i (Mult fa1 fa2) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Inverse fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Inverse fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Inverse fa)) vs = isDERIV i (Inverse fa) vs
 5. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Cos fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Cos fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Cos fa)) vs = isDERIV i (Cos fa) vs
 6. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Arctan fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Arctan fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Arctan fa)) vs = isDERIV i (Arctan fa) vs
 7. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Abs fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Abs fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Abs fa)) vs = isDERIV i (Abs fa) vs
 8. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Max fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Max fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Max fa1 fa2)) vs = isDERIV i (Max fa1 fa2) vs
 9. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Min fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Min fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Min fa1 fa2)) vs = isDERIV i (Min fa1 fa2) vs
 10. \<lbrakk>max_Var_floatarith Pi \<le> length vs; \<And>j. j < max_Var_floatarith Pi \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) Pi) vs = isDERIV i Pi vs
A total of 18 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs
max_Var_floatarith (fa ^\<^sub>e n) \<le> length vs
?j < max_Var_floatarith (fa ^\<^sub>e n) \<Longrightarrow> vs ! s ?j = vs ! ?j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs
max_Var_floatarith (fa ^\<^sub>e n) \<le> length vs
?j < max_Var_floatarith (fa ^\<^sub>e n) \<Longrightarrow> vs ! s ?j = vs ! ?j

goal (1 subgoal):
 1. isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (fa ^\<^sub>e n)) vs = isDERIV i (fa ^\<^sub>e n) vs
[PROOF STEP]
by (cases n) auto
[PROOF STATE]
proof (state)
this:
isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (fa ^\<^sub>e n)) vs = isDERIV i (fa ^\<^sub>e n) vs

goal (17 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Add fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Add fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Add fa1 fa2)) vs = isDERIV i (Add fa1 fa2) vs
 2. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Minus fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Minus fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Minus fa)) vs = isDERIV i (Minus fa) vs
 3. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Mult fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Mult fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Mult fa1 fa2)) vs = isDERIV i (Mult fa1 fa2) vs
 4. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Inverse fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Inverse fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Inverse fa)) vs = isDERIV i (Inverse fa) vs
 5. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Cos fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Cos fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Cos fa)) vs = isDERIV i (Cos fa) vs
 6. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Arctan fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Arctan fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Arctan fa)) vs = isDERIV i (Arctan fa) vs
 7. \<And>fa. \<lbrakk>\<lbrakk>max_Var_floatarith fa \<le> length vs; \<And>j. j < max_Var_floatarith fa \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa) vs = isDERIV i fa vs; max_Var_floatarith (Abs fa) \<le> length vs; \<And>j. j < max_Var_floatarith (Abs fa) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Abs fa)) vs = isDERIV i (Abs fa) vs
 8. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Max fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Max fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Max fa1 fa2)) vs = isDERIV i (Max fa1 fa2) vs
 9. \<And>fa1 fa2. \<lbrakk>\<lbrakk>max_Var_floatarith fa1 \<le> length vs; \<And>j. j < max_Var_floatarith fa1 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa1) vs = isDERIV i fa1 vs; \<lbrakk>max_Var_floatarith fa2 \<le> length vs; \<And>j. j < max_Var_floatarith fa2 \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) fa2) vs = isDERIV i fa2 vs; max_Var_floatarith (Min fa1 fa2) \<le> length vs; \<And>j. j < max_Var_floatarith (Min fa1 fa2) \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) (Min fa1 fa2)) vs = isDERIV i (Min fa1 fa2) vs
 10. \<lbrakk>max_Var_floatarith Pi \<le> length vs; \<And>j. j < max_Var_floatarith Pi \<Longrightarrow> vs ! s j = vs ! j\<rbrakk> \<Longrightarrow> isDERIV i (subst_floatarith (\<lambda>i. Var (s i)) Pi) vs = isDERIV i Pi vs
A total of 17 subgoals...
[PROOF STEP]
qed (auto simp: interpret_floatarith_subst_floatarith_idem)


[STATEMENT]
lemma isFDERIV_subst_Var_floatarith:
  assumes mv: "max_Var_floatariths fas \<le> length vs"
  assumes idem: "\<And>j. j < max_Var_floatariths fas \<Longrightarrow> vs ! (s j) = vs ! j"
  assumes "\<And>i j. i \<in> set xs \<Longrightarrow> s j = i \<longleftrightarrow> j = i"
  shows "isFDERIV n xs (map (subst_floatarith (\<lambda>i. Var (s i))) fas) vs = isFDERIV n xs fas vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isFDERIV n xs (map (subst_floatarith (\<lambda>i. Var (s i))) fas) vs = isFDERIV n xs fas vs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isFDERIV n xs (map (subst_floatarith (\<lambda>i. Var (s i))) fas) vs = isFDERIV n xs fas vs
[PROOF STEP]
have mv: "\<And>i. i < length fas \<Longrightarrow> max_Var_floatarith (fas ! i) \<le> length vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length fas \<Longrightarrow> max_Var_floatarith (fas ! i) \<le> length vs
[PROOF STEP]
apply (rule order_trans[OF _ mv])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length fas \<Longrightarrow> max_Var_floatarith (fas ! i) \<le> max_Var_floatariths fas
[PROOF STEP]
by (intro max_Var_floatarith_le_max_Var_floatariths_nth)
[PROOF STATE]
proof (state)
this:
?i < length fas \<Longrightarrow> max_Var_floatarith (fas ! ?i) \<le> length vs

goal (1 subgoal):
 1. isFDERIV n xs (map (subst_floatarith (\<lambda>i. Var (s i))) fas) vs = isFDERIV n xs fas vs
[PROOF STEP]
have idem: "\<And>i j. i < length fas \<Longrightarrow> j < max_Var_floatarith (fas ! i) \<Longrightarrow> vs ! s j = vs ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < length fas; j < max_Var_floatarith (fas ! i)\<rbrakk> \<Longrightarrow> vs ! s j = vs ! j
[PROOF STEP]
using idem
[PROOF STATE]
proof (prove)
using this:
?j < max_Var_floatariths fas \<Longrightarrow> vs ! s ?j = vs ! ?j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < length fas; j < max_Var_floatarith (fas ! i)\<rbrakk> \<Longrightarrow> vs ! s j = vs ! j
[PROOF STEP]
by (auto simp: dest!: max_Var_floatariths_lessI)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < length fas; ?j < max_Var_floatarith (fas ! ?i)\<rbrakk> \<Longrightarrow> vs ! s ?j = vs ! ?j

goal (1 subgoal):
 1. isFDERIV n xs (map (subst_floatarith (\<lambda>i. Var (s i))) fas) vs = isFDERIV n xs fas vs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isFDERIV n xs (map (subst_floatarith (\<lambda>i. Var (s i))) fas) vs = isFDERIV n xs fas vs
[PROOF STEP]
unfolding isFDERIV_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>i<n. \<forall>j<n. isDERIV (xs ! i) (map (subst_floatarith (\<lambda>i. Var (s i))) fas ! j) vs) \<and> length (map (subst_floatarith (\<lambda>i. Var (s i))) fas) = n \<and> length xs = n) = ((\<forall>i<n. \<forall>j<n. isDERIV (xs ! i) (fas ! j) vs) \<and> length fas = n \<and> length xs = n)
[PROOF STEP]
using mv idem assms(3)
[PROOF STATE]
proof (prove)
using this:
?i < length fas \<Longrightarrow> max_Var_floatarith (fas ! ?i) \<le> length vs
\<lbrakk>?i < length fas; ?j < max_Var_floatarith (fas ! ?i)\<rbrakk> \<Longrightarrow> vs ! s ?j = vs ! ?j
?i \<in> set xs \<Longrightarrow> (s ?j = ?i) = (?j = ?i)

goal (1 subgoal):
 1. ((\<forall>i<n. \<forall>j<n. isDERIV (xs ! i) (map (subst_floatarith (\<lambda>i. Var (s i))) fas ! j) vs) \<and> length (map (subst_floatarith (\<lambda>i. Var (s i))) fas) = n \<and> length xs = n) = ((\<forall>i<n. \<forall>j<n. isDERIV (xs ! i) (fas ! j) vs) \<and> length fas = n \<and> length xs = n)
[PROOF STEP]
by (auto simp: isDERIV_subst_Var_floatarith)
[PROOF STATE]
proof (state)
this:
isFDERIV n xs (map (subst_floatarith (\<lambda>i. Var (s i))) fas) vs = isFDERIV n xs fas vs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interpret_floatariths_append[simp]:
  "interpret_floatariths (xs @ ys) vs = interpret_floatariths xs vs @ interpret_floatariths ys vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatariths (xs @ ys) vs = interpret_floatariths xs vs @ interpret_floatariths ys vs
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma not_fresh_inner_floatariths:
  assumes "length xs = length ys"
  shows "\<not> fresh_floatarith (inner_floatariths xs ys) i \<longleftrightarrow> \<not>fresh_floatariths xs i \<or> \<not>fresh_floatariths ys i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> fresh_floatarith (inner_floatariths xs ys) i) = (\<not> fresh_floatariths xs i \<or> \<not> fresh_floatariths ys i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs = length ys

goal (1 subgoal):
 1. (\<not> fresh_floatarith (inner_floatariths xs ys) i) = (\<not> fresh_floatariths xs i \<or> \<not> fresh_floatariths ys i)
[PROOF STEP]
by (induction xs ys rule: list_induct2) auto


[STATEMENT]
lemma fresh_inner_floatariths:
  assumes "length xs = length ys"
  shows "fresh_floatarith (inner_floatariths xs ys) i \<longleftrightarrow> fresh_floatariths xs i \<and> fresh_floatariths ys i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_floatarith (inner_floatariths xs ys) i = (fresh_floatariths xs i \<and> fresh_floatariths ys i)
[PROOF STEP]
using not_fresh_inner_floatariths assms
[PROOF STATE]
proof (prove)
using this:
length ?xs = length ?ys \<Longrightarrow> (\<not> fresh_floatarith (inner_floatariths ?xs ?ys) ?i) = (\<not> fresh_floatariths ?xs ?i \<or> \<not> fresh_floatariths ?ys ?i)
length xs = length ys

goal (1 subgoal):
 1. fresh_floatarith (inner_floatariths xs ys) i = (fresh_floatariths xs i \<and> fresh_floatariths ys i)
[PROOF STEP]
by auto


[STATEMENT]
lemma not_fresh_floatariths_map:
  " \<not> fresh_floatariths (map f xs) i \<longleftrightarrow> (\<exists>x \<in> set xs. \<not>fresh_floatarith (f x) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> fresh_floatariths (map f xs) i) = (\<exists>x\<in>set xs. \<not> fresh_floatarith (f x) i)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma fresh_floatariths_map:
  " fresh_floatariths (map f xs) i \<longleftrightarrow> (\<forall>x \<in> set xs. fresh_floatarith (f x) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_floatariths (map f xs) i = (\<forall>x\<in>set xs. fresh_floatarith (f x) i)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma fresh_floatarith_fold_const_fa: "fresh_floatarith fa i \<Longrightarrow> fresh_floatarith (fold_const_fa fa) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_floatarith fa i \<Longrightarrow> fresh_floatarith (fold_const_fa fa) i
[PROOF STEP]
by (induction fa) (auto simp: fold_const_fa.simps split: floatarith.splits option.splits)


[STATEMENT]
lemma fresh_floatarith_fold_const_fa_Add[intro!]:
  assumes "fresh_floatarith (fold_const_fa a) i" "fresh_floatarith (fold_const_fa b) i"
  shows "fresh_floatarith (fold_const_fa (Add a b)) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_floatarith (fold_const_fa (Add a b)) i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fresh_floatarith (fold_const_fa a) i
fresh_floatarith (fold_const_fa b) i

goal (1 subgoal):
 1. fresh_floatarith (fold_const_fa (Add a b)) i
[PROOF STEP]
by (auto simp: fold_const_fa.simps split!: floatarith.splits option.splits)


[STATEMENT]
lemma fresh_floatarith_fold_const_fa_Mult[intro!]:
  assumes "fresh_floatarith (fold_const_fa a) i" "fresh_floatarith (fold_const_fa b) i"
  shows "fresh_floatarith (fold_const_fa (Mult a b)) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_floatarith (fold_const_fa (Mult a b)) i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fresh_floatarith (fold_const_fa a) i
fresh_floatarith (fold_const_fa b) i

goal (1 subgoal):
 1. fresh_floatarith (fold_const_fa (Mult a b)) i
[PROOF STEP]
by (auto simp: fold_const_fa.simps split!: floatarith.splits option.splits)


[STATEMENT]
lemma fresh_floatarith_fold_const_fa_Minus[intro!]:
  assumes "fresh_floatarith (fold_const_fa b) i"
  shows "fresh_floatarith (fold_const_fa (Minus b)) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_floatarith (fold_const_fa (Minus b)) i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fresh_floatarith (fold_const_fa b) i

goal (1 subgoal):
 1. fresh_floatarith (fold_const_fa (Minus b)) i
[PROOF STEP]
by (auto simp: fold_const_fa.simps split!: floatarith.splits)


[STATEMENT]
lemma fresh_FDERIV_floatarith:
  "fresh_floatarith ode_e i \<Longrightarrow> fresh_floatariths ds i
  \<Longrightarrow> length ds = DIM('a)
  \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a::executable_euclidean_space)] ds) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i
[PROOF STEP]
proof (induction ode_e)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Add ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Add ode_e1 ode_e2) [0..<DIM('a)] ds) i
 2. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Minus ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Minus ode_e) [0..<DIM('a)] ds) i
 3. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Mult ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Mult ode_e1 ode_e2) [0..<DIM('a)] ds) i
 4. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Inverse ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Inverse ode_e) [0..<DIM('a)] ds) i
 5. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Cos ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Cos ode_e) [0..<DIM('a)] ds) i
 6. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Arctan ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Arctan ode_e) [0..<DIM('a)] ds) i
 7. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Abs ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Abs ode_e) [0..<DIM('a)] ds) i
 8. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Max ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Max ode_e1 ode_e2) [0..<DIM('a)] ds) i
 9. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Min ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Min ode_e1 ode_e2) [0..<DIM('a)] ds) i
 10. \<lbrakk>fresh_floatarith Pi i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith Pi [0..<DIM('a)] ds) i
A total of 18 subgoals...
[PROOF STEP]
case (Power ode_e n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i
fresh_floatarith (ode_e ^\<^sub>e n) i
fresh_floatariths ds i
length ds = DIM('a)

goal (18 subgoals):
 1. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Add ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Add ode_e1 ode_e2) [0..<DIM('a)] ds) i
 2. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Minus ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Minus ode_e) [0..<DIM('a)] ds) i
 3. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Mult ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Mult ode_e1 ode_e2) [0..<DIM('a)] ds) i
 4. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Inverse ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Inverse ode_e) [0..<DIM('a)] ds) i
 5. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Cos ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Cos ode_e) [0..<DIM('a)] ds) i
 6. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Arctan ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Arctan ode_e) [0..<DIM('a)] ds) i
 7. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Abs ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Abs ode_e) [0..<DIM('a)] ds) i
 8. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Max ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Max ode_e1 ode_e2) [0..<DIM('a)] ds) i
 9. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Min ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Min ode_e1 ode_e2) [0..<DIM('a)] ds) i
 10. \<lbrakk>fresh_floatarith Pi i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith Pi [0..<DIM('a)] ds) i
A total of 18 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i
fresh_floatarith (ode_e ^\<^sub>e n) i
fresh_floatariths ds i
length ds = DIM('a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i
fresh_floatarith (ode_e ^\<^sub>e n) i
fresh_floatariths ds i
length ds = DIM('a)

goal (1 subgoal):
 1. fresh_floatarith (FDERIV_floatarith (ode_e ^\<^sub>e n) [0..<DIM('a)] ds) i
[PROOF STEP]
by (cases n) (auto simp: FDERIV_floatarith_def fresh_inner_floatariths fresh_floatariths_map fresh_floatarith_fold_const_fa)
[PROOF STATE]
proof (state)
this:
fresh_floatarith (FDERIV_floatarith (ode_e ^\<^sub>e n) [0..<DIM('a)] ds) i

goal (17 subgoals):
 1. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Add ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Add ode_e1 ode_e2) [0..<DIM('a)] ds) i
 2. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Minus ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Minus ode_e) [0..<DIM('a)] ds) i
 3. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Mult ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Mult ode_e1 ode_e2) [0..<DIM('a)] ds) i
 4. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Inverse ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Inverse ode_e) [0..<DIM('a)] ds) i
 5. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Cos ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Cos ode_e) [0..<DIM('a)] ds) i
 6. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Arctan ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Arctan ode_e) [0..<DIM('a)] ds) i
 7. \<And>ode_e. \<lbrakk>\<lbrakk>fresh_floatarith ode_e i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; fresh_floatarith (Abs ode_e) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Abs ode_e) [0..<DIM('a)] ds) i
 8. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Max ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Max ode_e1 ode_e2) [0..<DIM('a)] ds) i
 9. \<And>ode_e1 ode_e2. \<lbrakk>\<lbrakk>fresh_floatarith ode_e1 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e1 [0..<DIM('a)] ds) i; \<lbrakk>fresh_floatarith ode_e2 i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ode_e2 [0..<DIM('a)] ds) i; fresh_floatarith (Min ode_e1 ode_e2) i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith (Min ode_e1 ode_e2) [0..<DIM('a)] ds) i
 10. \<lbrakk>fresh_floatarith Pi i; fresh_floatariths ds i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith Pi [0..<DIM('a)] ds) i
A total of 17 subgoals...
[PROOF STEP]
qed (auto simp: FDERIV_floatarith_def fresh_inner_floatariths fresh_floatariths_map fresh_floatarith_fold_const_fa)


[STATEMENT]
lemma not_fresh_FDERIV_floatarith:
  "\<not> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a::executable_euclidean_space)] ds) i
  \<Longrightarrow> length ds = DIM('a)
  \<Longrightarrow> \<not>fresh_floatarith ode_e i \<or> \<not>fresh_floatariths ds i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> \<not> fresh_floatarith ode_e i \<or> \<not> fresh_floatariths ds i
[PROOF STEP]
using fresh_FDERIV_floatarith
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>fresh_floatarith ?ode_e ?i; fresh_floatariths ?ds ?i; length ?ds = DIM(?'a)\<rbrakk> \<Longrightarrow> fresh_floatarith (FDERIV_floatarith ?ode_e [0..<DIM(?'a)] ?ds) ?i

goal (1 subgoal):
 1. \<lbrakk>\<not> fresh_floatarith (FDERIV_floatarith ode_e [0..<DIM('a)] ds) i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> \<not> fresh_floatarith ode_e i \<or> \<not> fresh_floatariths ds i
[PROOF STEP]
by auto


[STATEMENT]
lemma not_fresh_FDERIV_floatariths:
  "\<not> fresh_floatariths (FDERIV_floatariths ode_e [0..<DIM('a::executable_euclidean_space)] ds) i \<Longrightarrow>
  length ds = DIM('a) \<Longrightarrow> \<not>fresh_floatariths ode_e i \<or> \<not>fresh_floatariths ds i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> fresh_floatariths (FDERIV_floatariths ode_e [0..<DIM('a)] ds) i; length ds = DIM('a)\<rbrakk> \<Longrightarrow> \<not> fresh_floatariths ode_e i \<or> \<not> fresh_floatariths ds i
[PROOF STEP]
by (induction ode_e) (auto simp: FDERIV_floatariths_def dest!: not_fresh_FDERIV_floatarith)


[STATEMENT]
lemma isDERIV_FDERIV_floatarith_linear:
  fixes x h::"'a::executable_euclidean_space"
  assumes "\<And>k. k < DIM('a) \<Longrightarrow> isDERIV i (DERIV_floatarith k fa) xs"
  assumes "max_Var_floatarith fa \<le> DIM('a)"
  assumes [simp]: "length xs = DIM('a)" "length hs = DIM('a)"
  shows "isDERIV i (FDERIV_floatarith fa [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)]))
            (xs @ hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV i (FDERIV_floatarith fa [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)])) (xs @ hs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?k < DIM('a) \<Longrightarrow> isDERIV i (DERIV_floatarith ?k fa) xs
max_Var_floatarith fa \<le> DIM('a)
length xs = DIM('a)
length hs = DIM('a)

goal (1 subgoal):
 1. isDERIV i (FDERIV_floatarith fa [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)])) (xs @ hs)
[PROOF STEP]
apply (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>k. k < DIM('a) \<Longrightarrow> isDERIV i (DERIV_floatarith k fa) xs; max_Var_floatarith fa \<le> DIM('a); k < DIM('a)\<rbrakk> \<Longrightarrow> isDERIV i (fold_const_fa (DERIV_floatarith k fa)) (xs @ hs)
[PROOF STEP]
apply (rule isDERIV_max_Var_floatarithI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>\<And>k. k < DIM('a) \<Longrightarrow> isDERIV i (DERIV_floatarith k fa) xs; max_Var_floatarith fa \<le> DIM('a); k < DIM('a)\<rbrakk> \<Longrightarrow> isDERIV i (fold_const_fa (DERIV_floatarith k fa)) (?ys7 k)
 2. \<And>k ia. \<lbrakk>\<And>k. k < DIM('a) \<Longrightarrow> isDERIV i (DERIV_floatarith k fa) xs; max_Var_floatarith fa \<le> DIM('a); k < DIM('a); ia < max_Var_floatarith (fold_const_fa (DERIV_floatarith k fa))\<rbrakk> \<Longrightarrow> (xs @ hs) ! ia = ?ys7 k ! ia
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k ia. \<lbrakk>\<And>k. k < DIM('a) \<Longrightarrow> isDERIV i (DERIV_floatarith k fa) xs; max_Var_floatarith fa \<le> DIM('a); k < DIM('a); ia < max_Var_floatarith (fold_const_fa (DERIV_floatarith k fa))\<rbrakk> \<Longrightarrow> (xs @ hs) ! ia = xs ! ia
[PROOF STEP]
apply (auto simp: nth_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k ia. \<lbrakk>\<And>k. k < DIM('a) \<Longrightarrow> isDERIV i (DERIV_floatarith k fa) xs; max_Var_floatarith fa \<le> DIM('a); k < DIM('a); ia < max_Var_floatarith (fold_const_fa (DERIV_floatarith k fa)); \<not> ia < DIM('a)\<rbrakk> \<Longrightarrow> hs ! (ia - DIM('a)) = xs ! ia
[PROOF STEP]
by (metis add_diff_inverse_nat leD max_Var_floatarith_DERIV_floatarith
      max_Var_floatarith_fold_const_fa trans_le_add1)


[STATEMENT]
lemma isFDERIV_approx:
  "bounded_by vs VS \<Longrightarrow> isFDERIV_approx prec n xs fas VS \<Longrightarrow> isFDERIV n xs fas vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_by vs VS; isFDERIV_approx prec n xs fas VS\<rbrakk> \<Longrightarrow> isFDERIV n xs fas vs
[PROOF STEP]
by (auto simp: isFDERIV_approx_def isFDERIV_def intro!: isDERIV_approx)


[STATEMENT]
lemma isnFDERIV_approx:
  "bounded_by vs VS \<Longrightarrow> isnFDERIV_approx prec N fas xs ds VS n \<Longrightarrow> isnFDERIV N fas xs ds vs n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_by vs VS; isnFDERIV_approx prec N fas xs ds VS n\<rbrakk> \<Longrightarrow> isnFDERIV N fas xs ds vs n
[PROOF STEP]
by (induction n) (auto intro!: isFDERIV_approx)


[STATEMENT]
lemma plain_floatarith_approx_not_None:
  assumes "plain_floatarith N fa" "N \<le> length XS" "\<And>i. i < N \<Longrightarrow> XS ! i \<noteq> None"
  shows "approx p fa XS \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. approx p fa XS \<noteq> None
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
plain_floatarith N fa
N \<le> length XS
?i < N \<Longrightarrow> XS ! ?i \<noteq> None

goal (1 subgoal):
 1. approx p fa XS \<noteq> None
[PROOF STEP]
by (induction fa)
    (auto simp: Let_def split_beta' prod_eq_iff approx.simps)


[STATEMENT]
lemma interpret_Rad_of[simp]: "interpret_floatarith (Rad_of w) xs = rad_of (interpret_floatarith w xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (Rad_of w) xs = rad_of (interpret_floatarith w xs)
[PROOF STEP]
by (auto simp: Rad_of_def rad_of_def)


[STATEMENT]
lemma interpret_Deg_of[simp]: "interpret_floatarith (Deg_of w) xs = deg_of (interpret_floatarith w xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (Deg_of w) xs = deg_of (interpret_floatarith w xs)
[PROOF STEP]
by (auto simp: Deg_of_def deg_of_def inverse_eq_divide)


[STATEMENT]
lemma valid_SDG_CFG_node:
  "valid_SDG_node n \<Longrightarrow> valid_node (parent_node n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_SDG_node n \<Longrightarrow> valid_node (parent_node n)
[PROOF STEP]
by(cases n) auto


[STATEMENT]
lemma Formal_in_parent_det:
  assumes "valid_SDG_node (Formal_in (m,x))" and "valid_SDG_node (Formal_in (m',x'))"
  and "get_proc m = get_proc m'"
  shows "m = m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = m'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m = m'
[PROOF STEP]
from \<open>valid_SDG_node (Formal_in (m,x))\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node (Formal_in (m, x))
[PROOF STEP]
obtain a Q r p fs ins outs
    where "valid_edge a" and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "targetnode a = m"
    and "(p,ins,outs) \<in> set procs" and "x < length ins"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node (Formal_in (m, x))

goal (1 subgoal):
 1. (\<And>a Q r p fs ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; targetnode a = m; (p, ins, outs) \<in> set procs; x < length ins\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = m
(p, ins, outs) \<in> set procs
x < length ins

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
from \<open>valid_SDG_node (Formal_in (m',x'))\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node (Formal_in (m', x'))
[PROOF STEP]
obtain a' Q' r' p' f' ins' outs'
    where "valid_edge a'" and "kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>f'" and "targetnode a' = m'"
    and "(p',ins',outs') \<in> set procs" and "x' < length ins'"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node (Formal_in (m', x'))

goal (1 subgoal):
 1. (\<And>a' Q' r' p' f' ins' outs'. \<lbrakk>valid_edge a'; kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>f'; targetnode a' = m'; (p', ins', outs') \<in> set procs; x' < length ins'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>f'
targetnode a' = m'
(p', ins', outs') \<in> set procs
x' < length ins'

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>targetnode a = m\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = m
[PROOF STEP]
have "get_proc m = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = m

goal (1 subgoal):
 1. get_proc m = p
[PROOF STEP]
by(fastforce intro:get_proc_call)
[PROOF STATE]
proof (state)
this:
get_proc m = p

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
get_proc m = p

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>f'\<close> \<open>targetnode a' = m'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>f'
targetnode a' = m'
[PROOF STEP]
have "get_proc m' = p'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>f'
targetnode a' = m'

goal (1 subgoal):
 1. get_proc m' = p'
[PROOF STEP]
by(fastforce intro:get_proc_call)
[PROOF STATE]
proof (state)
this:
get_proc m' = p'

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
get_proc m = p
get_proc m' = p'
[PROOF STEP]
have "p = p'"
[PROOF STATE]
proof (prove)
using this:
get_proc m = p
get_proc m' = p'

goal (1 subgoal):
 1. p = p'
[PROOF STEP]
using \<open>get_proc m = get_proc m'\<close>
[PROOF STATE]
proof (prove)
using this:
get_proc m = p
get_proc m' = p'
get_proc m = get_proc m'

goal (1 subgoal):
 1. p = p'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p = p'

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>f'\<close>
    \<open>targetnode a = m\<close> \<open>targetnode a' = m'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>f'
targetnode a = m
targetnode a' = m'
p = p'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p'\<^esub>f'
targetnode a = m
targetnode a' = m'
p = p'

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
by(fastforce intro:same_proc_call_unique_target)
[PROOF STATE]
proof (state)
this:
m = m'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_SDG_node_parent_Entry:
  assumes "valid_SDG_node n" and "parent_node n = (_Entry_)"
  shows "n = CFG_node (_Entry_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = CFG_node (_Entry_)
[PROOF STEP]
proof(cases n)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1. n = CFG_node x1 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 4. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 5. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
case CFG_node
[PROOF STATE]
proof (state)
this:
n = CFG_node x1_

goal (5 subgoals):
 1. \<And>x1. n = CFG_node x1 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 4. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 5. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>parent_node n = (_Entry_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Entry_)
n = CFG_node x1_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Entry_)
n = CFG_node x1_

goal (1 subgoal):
 1. n = CFG_node (_Entry_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Entry_)

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
case (Formal_in z)
[PROOF STATE]
proof (state)
this:
n = Formal_in z

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>parent_node n = (_Entry_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Entry_)
n = Formal_in z
[PROOF STEP]
obtain x
    where [simp]:"z = ((_Entry_),x)"
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Entry_)
n = Formal_in z

goal (1 subgoal):
 1. (\<And>x. z = ((_Entry_), x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = ((_Entry_), x)

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>valid_SDG_node n\<close> Formal_in
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Formal_in z
z = ((_Entry_), x)
[PROOF STEP]
obtain a where "valid_edge a"
    and "targetnode a = (_Entry_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Formal_in z
z = ((_Entry_), x)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>valid_edge a; targetnode a = (_Entry_)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_edge a
targetnode a = (_Entry_)

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
targetnode a = (_Entry_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(rule Entry_target,simp+)
[PROOF STATE]
proof (state)
this:
False

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. n = CFG_node (_Entry_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Entry_)

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
case (Formal_out z)
[PROOF STATE]
proof (state)
this:
n = Formal_out z

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>parent_node n = (_Entry_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Entry_)
n = Formal_out z
[PROOF STEP]
obtain x
    where [simp]:"z = ((_Entry_),x)"
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Entry_)
n = Formal_out z

goal (1 subgoal):
 1. (\<And>x. z = ((_Entry_), x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = ((_Entry_), x)

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>valid_SDG_node n\<close> Formal_out
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Formal_out z
z = ((_Entry_), x)
[PROOF STEP]
obtain a Q p f where "valid_edge a"
    and "kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f" and  "sourcenode a = (_Entry_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Formal_out z
z = ((_Entry_), x)

goal (1 subgoal):
 1. (\<And>a Q p f. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; sourcenode a = (_Entry_)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
sourcenode a = (_Entry_)

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
[PROOF STEP]
have "get_proc (sourcenode a) = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. get_proc (sourcenode a) = p
[PROOF STEP]
by(rule get_proc_return)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode a) = p

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>sourcenode a = (_Entry_)\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a = (_Entry_)
get_proc (sourcenode a) = p
[PROOF STEP]
have "p = Main"
[PROOF STATE]
proof (prove)
using this:
sourcenode a = (_Entry_)
get_proc (sourcenode a) = p

goal (1 subgoal):
 1. p = Main
[PROOF STEP]
by(auto simp:get_proc_Entry)
[PROOF STATE]
proof (state)
this:
p = Main

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
p = Main
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
p = Main

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce intro:Main_no_return_source)
[PROOF STATE]
proof (state)
this:
False

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. n = CFG_node (_Entry_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Entry_)

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
case (Actual_in z)
[PROOF STATE]
proof (state)
this:
n = Actual_in z

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>parent_node n = (_Entry_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Entry_)
n = Actual_in z
[PROOF STEP]
obtain x
    where [simp]:"z = ((_Entry_),x)"
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Entry_)
n = Actual_in z

goal (1 subgoal):
 1. (\<And>x. z = ((_Entry_), x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = ((_Entry_), x)

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>valid_SDG_node n\<close> Actual_in
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Actual_in z
z = ((_Entry_), x)
[PROOF STEP]
obtain a Q r p fs where "valid_edge a"
    and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "sourcenode a = (_Entry_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Actual_in z
z = ((_Entry_), x)

goal (1 subgoal):
 1. (\<And>a Q r p fs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; sourcenode a = (_Entry_)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
sourcenode a = (_Entry_)

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
sourcenode a = (_Entry_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(rule Entry_no_call_source,auto)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Entry_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. n = CFG_node (_Entry_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Entry_)

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
case (Actual_out z)
[PROOF STATE]
proof (state)
this:
n = Actual_out z

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>parent_node n = (_Entry_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Entry_)
n = Actual_out z
[PROOF STEP]
obtain x
    where [simp]:"z = ((_Entry_),x)"
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Entry_)
n = Actual_out z

goal (1 subgoal):
 1. (\<And>x. z = ((_Entry_), x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = ((_Entry_), x)

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
with \<open>valid_SDG_node n\<close> Actual_out
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Actual_out z
z = ((_Entry_), x)
[PROOF STEP]
obtain a where "valid_edge a"
    "targetnode a = (_Entry_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Actual_out z
z = ((_Entry_), x)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>valid_edge a; targetnode a = (_Entry_)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_edge a
targetnode a = (_Entry_)

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
targetnode a = (_Entry_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(rule Entry_target,simp+)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Entry_)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. n = CFG_node (_Entry_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Entry_)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_SDG_node_parent_Exit:
  assumes "valid_SDG_node n" and "parent_node n = (_Exit_)"
  shows "n = CFG_node (_Exit_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = CFG_node (_Exit_)
[PROOF STEP]
proof(cases n)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1. n = CFG_node x1 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 4. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 5. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
case CFG_node
[PROOF STATE]
proof (state)
this:
n = CFG_node x1_

goal (5 subgoals):
 1. \<And>x1. n = CFG_node x1 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 4. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 5. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>parent_node n = (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Exit_)
n = CFG_node x1_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Exit_)
n = CFG_node x1_

goal (1 subgoal):
 1. n = CFG_node (_Exit_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Exit_)

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
case (Formal_in z)
[PROOF STATE]
proof (state)
this:
n = Formal_in z

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>parent_node n = (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Exit_)
n = Formal_in z
[PROOF STEP]
obtain x
    where [simp]:"z = ((_Exit_),x)"
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Exit_)
n = Formal_in z

goal (1 subgoal):
 1. (\<And>x. z = ((_Exit_), x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = ((_Exit_), x)

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>valid_SDG_node n\<close> Formal_in
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Formal_in z
z = ((_Exit_), x)
[PROOF STEP]
obtain a Q r p fs where "valid_edge a"
    and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "targetnode a = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Formal_in z
z = ((_Exit_), x)

goal (1 subgoal):
 1. (\<And>a Q r p fs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; targetnode a = (_Exit_)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = (_Exit_)

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
have "get_proc (targetnode a) = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. get_proc (targetnode a) = p
[PROOF STEP]
by(rule get_proc_call)
[PROOF STATE]
proof (state)
this:
get_proc (targetnode a) = p

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>targetnode a = (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a = (_Exit_)
get_proc (targetnode a) = p
[PROOF STEP]
have "p = Main"
[PROOF STATE]
proof (prove)
using this:
targetnode a = (_Exit_)
get_proc (targetnode a) = p

goal (1 subgoal):
 1. p = Main
[PROOF STEP]
by(auto simp:get_proc_Exit)
[PROOF STATE]
proof (state)
this:
p = Main

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
p = Main
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
p = Main

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce intro:Main_no_call_target)
[PROOF STATE]
proof (state)
this:
False

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. n = CFG_node (_Exit_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Exit_)

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
case (Formal_out z)
[PROOF STATE]
proof (state)
this:
n = Formal_out z

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>parent_node n = (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Exit_)
n = Formal_out z
[PROOF STEP]
obtain x
    where [simp]:"z = ((_Exit_),x)"
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Exit_)
n = Formal_out z

goal (1 subgoal):
 1. (\<And>x. z = ((_Exit_), x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = ((_Exit_), x)

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>valid_SDG_node n\<close> Formal_out
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Formal_out z
z = ((_Exit_), x)
[PROOF STEP]
obtain a where "valid_edge a"
    and "sourcenode a = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Formal_out z
z = ((_Exit_), x)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>valid_edge a; sourcenode a = (_Exit_)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_edge a
sourcenode a = (_Exit_)

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
sourcenode a = (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(rule Exit_source,simp+)
[PROOF STATE]
proof (state)
this:
False

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. n = CFG_node (_Exit_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Exit_)

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
case (Actual_in z)
[PROOF STATE]
proof (state)
this:
n = Actual_in z

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>parent_node n = (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Exit_)
n = Actual_in z
[PROOF STEP]
obtain x
    where [simp]:"z = ((_Exit_),x)"
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Exit_)
n = Actual_in z

goal (1 subgoal):
 1. (\<And>x. z = ((_Exit_), x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = ((_Exit_), x)

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>valid_SDG_node n\<close> Actual_in
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Actual_in z
z = ((_Exit_), x)
[PROOF STEP]
obtain a where "valid_edge a"
    and "sourcenode a = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Actual_in z
z = ((_Exit_), x)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>valid_edge a; sourcenode a = (_Exit_)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_edge a
sourcenode a = (_Exit_)

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
sourcenode a = (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(rule Exit_source,simp+)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (_Exit_)
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. n = CFG_node (_Exit_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Exit_)

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
case (Actual_out z)
[PROOF STATE]
proof (state)
this:
n = Actual_out z

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>parent_node n = (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Exit_)
n = Actual_out z
[PROOF STEP]
obtain x
    where [simp]:"z = ((_Exit_),x)"
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Exit_)
n = Actual_out z

goal (1 subgoal):
 1. (\<And>x. z = ((_Exit_), x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = ((_Exit_), x)

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
with \<open>valid_SDG_node n\<close> Actual_out
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Actual_out z
z = ((_Exit_), x)
[PROOF STEP]
obtain a Q p f where "valid_edge a"
    and "kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f" and "targetnode a = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Actual_out z
z = ((_Exit_), x)

goal (1 subgoal):
 1. (\<And>a Q p f. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; targetnode a = (_Exit_)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
targetnode a = (_Exit_)

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
targetnode a = (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(erule Exit_no_return_target,auto)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (_Exit_)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. n = CFG_node (_Exit_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (_Exit_)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_Use_valid_SDG_node:
  "V \<in> Use\<^bsub>SDG\<^esub> n \<Longrightarrow> valid_SDG_node n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> Use\<^bsub>SDG\<^esub> n \<Longrightarrow> valid_SDG_node n
[PROOF STEP]
by(induct rule:SDG_Use.induct,auto intro:valid_SDG_CFG_node)