[STATEMENT]
lemma isDERIV_max_Var_floatarithI:
  assumes "isDERIV n f ys"
  assumes "\<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i"
  shows "isDERIV n f xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV n f xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isDERIV n f ys
?i < max_Var_floatarith f \<Longrightarrow> xs ! ?i = ys ! ?i

goal (1 subgoal):
 1. isDERIV n f xs
[PROOF STEP]
proof (induction f)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Add f1 f2) ys; \<And>i. i < max_Var_floatarith (Add f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Add f1 f2) xs
 2. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Minus f) ys; \<And>i. i < max_Var_floatarith (Minus f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Minus f) xs
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Mult f1 f2) ys; \<And>i. i < max_Var_floatarith (Mult f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Mult f1 f2) xs
 4. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Inverse f) ys; \<And>i. i < max_Var_floatarith (Inverse f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Inverse f) xs
 5. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Cos f) ys; \<And>i. i < max_Var_floatarith (Cos f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Cos f) xs
 6. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Arctan f) ys; \<And>i. i < max_Var_floatarith (Arctan f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Arctan f) xs
 7. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Abs f) ys; \<And>i. i < max_Var_floatarith (Abs f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Abs f) xs
 8. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Max f1 f2) ys; \<And>i. i < max_Var_floatarith (Max f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Max f1 f2) xs
 9. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Min f1 f2) ys; \<And>i. i < max_Var_floatarith (Min f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Min f1 f2) xs
 10. \<lbrakk>isDERIV n Pi ys; \<And>i. i < max_Var_floatarith Pi \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n Pi xs
A total of 18 subgoals...
[PROOF STEP]
case (Power f n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs
isDERIV n (f ^\<^sub>e n) ys
?i < max_Var_floatarith (f ^\<^sub>e n) \<Longrightarrow> xs ! ?i = ys ! ?i

goal (18 subgoals):
 1. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Add f1 f2) ys; \<And>i. i < max_Var_floatarith (Add f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Add f1 f2) xs
 2. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Minus f) ys; \<And>i. i < max_Var_floatarith (Minus f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Minus f) xs
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Mult f1 f2) ys; \<And>i. i < max_Var_floatarith (Mult f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Mult f1 f2) xs
 4. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Inverse f) ys; \<And>i. i < max_Var_floatarith (Inverse f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Inverse f) xs
 5. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Cos f) ys; \<And>i. i < max_Var_floatarith (Cos f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Cos f) xs
 6. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Arctan f) ys; \<And>i. i < max_Var_floatarith (Arctan f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Arctan f) xs
 7. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Abs f) ys; \<And>i. i < max_Var_floatarith (Abs f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Abs f) xs
 8. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Max f1 f2) ys; \<And>i. i < max_Var_floatarith (Max f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Max f1 f2) xs
 9. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Min f1 f2) ys; \<And>i. i < max_Var_floatarith (Min f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Min f1 f2) xs
 10. \<lbrakk>isDERIV n Pi ys; \<And>i. i < max_Var_floatarith Pi \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n Pi xs
A total of 18 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs
isDERIV n (f ^\<^sub>e n) ys
?i < max_Var_floatarith (f ^\<^sub>e n) \<Longrightarrow> xs ! ?i = ys ! ?i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs
isDERIV n (f ^\<^sub>e n) ys
?i < max_Var_floatarith (f ^\<^sub>e n) \<Longrightarrow> xs ! ?i = ys ! ?i

goal (1 subgoal):
 1. isDERIV n (f ^\<^sub>e n) xs
[PROOF STEP]
by (cases n) auto
[PROOF STATE]
proof (state)
this:
isDERIV n (f ^\<^sub>e n) xs

goal (17 subgoals):
 1. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Add f1 f2) ys; \<And>i. i < max_Var_floatarith (Add f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Add f1 f2) xs
 2. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Minus f) ys; \<And>i. i < max_Var_floatarith (Minus f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Minus f) xs
 3. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Mult f1 f2) ys; \<And>i. i < max_Var_floatarith (Mult f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Mult f1 f2) xs
 4. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Inverse f) ys; \<And>i. i < max_Var_floatarith (Inverse f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Inverse f) xs
 5. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Cos f) ys; \<And>i. i < max_Var_floatarith (Cos f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Cos f) xs
 6. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Arctan f) ys; \<And>i. i < max_Var_floatarith (Arctan f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Arctan f) xs
 7. \<And>f. \<lbrakk>\<lbrakk>isDERIV n f ys; \<And>i. i < max_Var_floatarith f \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f xs; isDERIV n (Abs f) ys; \<And>i. i < max_Var_floatarith (Abs f) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Abs f) xs
 8. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Max f1 f2) ys; \<And>i. i < max_Var_floatarith (Max f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Max f1 f2) xs
 9. \<And>f1 f2. \<lbrakk>\<lbrakk>isDERIV n f1 ys; \<And>i. i < max_Var_floatarith f1 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f1 xs; \<lbrakk>isDERIV n f2 ys; \<And>i. i < max_Var_floatarith f2 \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n f2 xs; isDERIV n (Min f1 f2) ys; \<And>i. i < max_Var_floatarith (Min f1 f2) \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n (Min f1 f2) xs
 10. \<lbrakk>isDERIV n Pi ys; \<And>i. i < max_Var_floatarith Pi \<Longrightarrow> xs ! i = ys ! i\<rbrakk> \<Longrightarrow> isDERIV n Pi xs
A total of 17 subgoals...
[PROOF STEP]
qed (auto simp: max_def interpret_floatarith_max_Var_cong[of _ xs ys] split: if_splits)


[STATEMENT]
lemma isFDERIV_I: "(\<And>i j. i < n \<Longrightarrow> j < n \<Longrightarrow> isDERIV (xs ! i) (fas ! j) vs) \<Longrightarrow>
  length fas = n \<Longrightarrow> length xs = n \<Longrightarrow> isFDERIV n xs fas vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i j. \<lbrakk>i < n; j < n\<rbrakk> \<Longrightarrow> isDERIV (xs ! i) (fas ! j) vs; length fas = n; length xs = n\<rbrakk> \<Longrightarrow> isFDERIV n xs fas vs
[PROOF STEP]
by (auto simp: isFDERIV_def)


[STATEMENT]
lemma isFDERIV_isDERIV_D: "isFDERIV n xs fas vs \<Longrightarrow> i < n \<Longrightarrow> j < n \<Longrightarrow> isDERIV (xs ! i) (fas ! j) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isFDERIV n xs fas vs; i < n; j < n\<rbrakk> \<Longrightarrow> isDERIV (xs ! i) (fas ! j) vs
[PROOF STEP]
by (auto simp: isFDERIV_def)


[STATEMENT]
lemma isFDERIV_lengthD: "length fas = n" "length xs = n" if "isFDERIV n xs fas vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length fas = n &&& length xs = n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
isFDERIV n xs fas vs

goal (1 subgoal):
 1. length fas = n &&& length xs = n
[PROOF STEP]
by (auto simp: isFDERIV_def)


[STATEMENT]
lemma isFDERIV_uptD: "isFDERIV n [0..<n] fas vs \<Longrightarrow> i < n \<Longrightarrow> j < n \<Longrightarrow> isDERIV i (fas ! j) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isFDERIV n [0..<n] fas vs; i < n; j < n\<rbrakk> \<Longrightarrow> isDERIV i (fas ! j) vs
[PROOF STEP]
by (auto simp: isFDERIV_def)


[STATEMENT]
lemma isFDERIV_max_Var_cong: "isFDERIV n xs fas ws \<longleftrightarrow> isFDERIV n xs fas vs"
  if c: "(\<And>i. i < max_Var_floatariths fas \<Longrightarrow> vs ! i = ws ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isFDERIV n xs fas ws = isFDERIV n xs fas vs
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
?i < max_Var_floatariths fas \<Longrightarrow> vs ! ?i = ws ! ?i

goal (1 subgoal):
 1. isFDERIV n xs fas ws = isFDERIV n xs fas vs
[PROOF STEP]
by (auto intro: isFDERIV_max_Var_congI)


[STATEMENT]
lemma isDERIV_max_VarI:
  "i \<ge> max_Var_floatarith fa \<Longrightarrow> isDERIV j fa xs \<Longrightarrow> isDERIV i fa xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>max_Var_floatarith fa \<le> i; isDERIV j fa xs\<rbrakk> \<Longrightarrow> isDERIV i fa xs
[PROOF STEP]
by (induction fa) (auto simp: isDERIV_Power_iff)


[STATEMENT]
lemma interpret_floatariths_Var[simp]:
  "interpret_floatariths (map floatarith.Var xs) vs = (map (nth vs) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatariths (map Var xs) vs = map ((!) vs) xs
[PROOF STEP]
by (induction xs) auto


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


[STATEMENT]
lemma map_nth_append_upt[simp]:
  assumes "a \<ge> length xs"
  shows "map ((!) (xs @ ys)) [a..<b] = map ((!) ys) [a - length xs..<b - length xs]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) (xs @ ys)) [a..<b] = map ((!) ys) [a - length xs..<b - length xs]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs \<le> a

goal (1 subgoal):
 1. map ((!) (xs @ ys)) [a..<b] = map ((!) ys) [a - length xs..<b - length xs]
[PROOF STEP]
by (auto intro!: nth_equalityI simp: nth_append)


[STATEMENT]
lemma map_nth_Cons_upt[simp]:
  assumes "a > 0"
  shows "map ((!) (x # ys)) [a..<b] = map ((!) ys) [a - Suc 0..<b - Suc 0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) (x # ys)) [a..<b] = map ((!) ys) [a - Suc 0..<b - Suc 0]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < a

goal (1 subgoal):
 1. map ((!) (x # ys)) [a..<b] = map ((!) ys) [a - Suc 0..<b - Suc 0]
[PROOF STEP]
by (auto intro!: nth_equalityI simp: nth_append)


[STATEMENT]
lemma map_nth_eq_self[simp]:
  shows "length fas = l \<Longrightarrow> (map ((!) fas) [0..<l]) = fas"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length fas = l \<Longrightarrow> map ((!) fas) [0..<l] = fas
[PROOF STEP]
by (auto simp: intro!: nth_equalityI)


[STATEMENT]
lemma matrix_matrix_mult_zero[simp]:
  "a ** 0 = 0" "0 ** a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ** 0 = 0 &&& 0 ** a = 0
[PROOF STEP]
by (vector matrix_matrix_mult_def)+


[STATEMENT]
lemma scaleR_blinfun_compose_left: "i *\<^sub>R (A o\<^sub>L B) = i *\<^sub>R A o\<^sub>L B"
  and scaleR_blinfun_compose_right: "i *\<^sub>R (A o\<^sub>L B) = A o\<^sub>L i *\<^sub>R B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i *\<^sub>R (A o\<^sub>L B) = i *\<^sub>R A o\<^sub>L B &&& i *\<^sub>R (A o\<^sub>L B) = A o\<^sub>L i *\<^sub>R B
[PROOF STEP]
by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)


[STATEMENT]
lemma matrix_add_rdistrib: "((B + C) ** A) = (B ** A) + (C ** A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (B + C) ** A = B ** A + C ** A
[PROOF STEP]
by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)


[STATEMENT]
lemma matrix_scaleR_right: "r *\<^sub>R (a::'a::real_algebra_1^'n^'m) ** b = r *\<^sub>R (a ** b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r *\<^sub>R a ** b = r *\<^sub>R (a ** b)
[PROOF STEP]
by (vector matrix_matrix_mult_def algebra_simps scaleR_sum_right)


[STATEMENT]
lemma matrix_scaleR_left: "(a::'a::real_algebra_1^'n^'m) ** r *\<^sub>R b = r *\<^sub>R (a ** b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ** r *\<^sub>R b = r *\<^sub>R (a ** b)
[PROOF STEP]
by (vector matrix_matrix_mult_def algebra_simps scaleR_sum_right)


[STATEMENT]
lemma bounded_bilinear_matrix_matrix_mult[bounded_bilinear]:
   "bounded_bilinear ((**)::
    ('a::{euclidean_space, real_normed_algebra_1}^'n^'m) \<Rightarrow>
    ('a::{euclidean_space, real_normed_algebra_1}^'p^'n) \<Rightarrow>
    ('a::{euclidean_space, real_normed_algebra_1}^'p^'m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_bilinear (**)
[PROOF STEP]
unfolding bilinear_conv_bounded_bilinear[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bilinear (**)
[PROOF STEP]
unfolding bilinear_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. linear ((**) x)) \<and> (\<forall>y. linear (\<lambda>x. x ** y))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. linear ((**) x)
 2. \<And>y. linear (\<lambda>x. x ** y)
[PROOF STEP]
by unfold_locales (auto simp: matrix_add_ldistrib matrix_add_rdistrib matrix_scaleR_right matrix_scaleR_left)


[STATEMENT]
lemma norm_axis: "norm (axis ia 1::'a::{real_normed_algebra_1}^'n) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (axis ia (1::'a)) = 1
[PROOF STEP]
by (auto simp: axis_def norm_vec_def L2_set_def if_distrib if_distribR sum.delta
      cong: if_cong)


[STATEMENT]
lemma abs_vec_nth_blinfun_apply_lemma:
  fixes x::"(real^'n) \<Rightarrow>\<^sub>L (real^'m)"
  shows "abs (vec_nth (blinfun_apply x (axis ia 1)) i) \<le> norm x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>blinfun_apply x (axis ia 1) $ i\<bar> \<le> norm x
[PROOF STEP]
apply (rule component_le_norm_cart[THEN order_trans])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (blinfun_apply x (axis ia 1)) \<le> norm x
[PROOF STEP]
apply (rule norm_blinfun[THEN order_trans])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm x * norm (axis ia 1) \<le> norm x
[PROOF STEP]
by (auto simp: norm_axis)


[STATEMENT]
lemma bounded_linear_matrix_blinfun_apply: "bounded_linear (\<lambda>x::(real^'n) \<Rightarrow>\<^sub>L (real^'m). matrix (blinfun_apply x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (\<lambda>x. matrix (blinfun_apply x))
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b1 b2. matrix (blinfun_apply (b1 + b2)) = matrix (blinfun_apply b1) + matrix (blinfun_apply b2)
 2. \<And>r b. matrix (blinfun_apply (r *\<^sub>R b)) = r *\<^sub>R matrix (blinfun_apply b)
 3. \<exists>K. \<forall>x. norm (matrix (blinfun_apply x)) \<le> norm x * K
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix (blinfun_apply (b1_ + b2_)) = matrix (blinfun_apply b1_) + matrix (blinfun_apply b2_)
[PROOF STEP]
by (vector blinfun.bilinear_simps matrix_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r b. matrix (blinfun_apply (r *\<^sub>R b)) = r *\<^sub>R matrix (blinfun_apply b)
 2. \<exists>K. \<forall>x. norm (matrix (blinfun_apply x)) \<le> norm x * K
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix (blinfun_apply (r_ *\<^sub>R b_)) = r_ *\<^sub>R matrix (blinfun_apply b_)
[PROOF STEP]
by (vector blinfun.bilinear_simps matrix_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>K. \<forall>x. norm (matrix (blinfun_apply x)) \<le> norm x * K
[PROOF STEP]
apply (rule exI[where x="real (CARD('n) * CARD('m))"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. norm (matrix (blinfun_apply x)) \<le> norm x * real (CARD('n) * CARD('m))
[PROOF STEP]
apply (auto simp: matrix_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. norm (\<chi>i j. blinfun_apply x (axis j 1) $ i) \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply (subst norm_vec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. L2_set (\<lambda>i. norm ((\<chi>i j. blinfun_apply x (axis j 1) $ i) $ i)) UNIV \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply (rule L2_set_le_sum[THEN order_trans])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. i \<in> UNIV \<Longrightarrow> 0 \<le> norm ((\<chi>i j. blinfun_apply x (axis j 1) $ i) $ i)
 2. \<And>x. (\<Sum>i\<in>UNIV. norm ((\<chi>i j. blinfun_apply x (axis j 1) $ i) $ i)) \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<Sum>i\<in>UNIV. norm ((\<chi>i j. blinfun_apply x (axis j 1) $ i) $ i)) \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<Sum>i\<in>UNIV. norm (\<chi>j. blinfun_apply x (axis j 1) $ i)) \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply (rule sum_mono[THEN order_trans])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. i \<in> UNIV \<Longrightarrow> norm (\<chi>j. blinfun_apply x (axis j 1) $ i) \<le> ?g19 x i
 2. \<And>x. sum (?g19 x) UNIV \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply (subst norm_vec_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. i \<in> UNIV \<Longrightarrow> L2_set (\<lambda>ia. norm ((\<chi>j. blinfun_apply x (axis j 1) $ i) $ ia)) UNIV \<le> ?g24 x x i i
 2. \<And>x. (\<Sum>i\<in>UNIV. ?g24 x x i i) \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply (rule L2_set_le_sum)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i ia. \<lbrakk>i \<in> UNIV; ia \<in> UNIV\<rbrakk> \<Longrightarrow> 0 \<le> norm ((\<chi>j. blinfun_apply x (axis j 1) $ i) $ ia)
 2. \<And>x. (\<Sum>i\<in>UNIV. \<Sum>ia\<in>UNIV. norm ((\<chi>j. blinfun_apply x (axis j 1) $ i) $ ia)) \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<Sum>i\<in>UNIV. \<Sum>ia\<in>UNIV. norm ((\<chi>j. blinfun_apply x (axis j 1) $ i) $ ia)) \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply (rule sum_mono[THEN order_trans])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. i \<in> UNIV \<Longrightarrow> (\<Sum>ia\<in>UNIV. norm ((\<chi>j. blinfun_apply x (axis j 1) $ i) $ ia)) \<le> ?g29 x i
 2. \<And>x. sum (?g29 x) UNIV \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply (rule sum_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i ia. \<lbrakk>i \<in> UNIV; ia \<in> UNIV\<rbrakk> \<Longrightarrow> norm ((\<chi>j. blinfun_apply x (axis j 1) $ i) $ ia) \<le> ?g32 x i ia
 2. \<And>x. (\<Sum>i\<in>UNIV. sum (?g32 x i) UNIV) \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i ia. \<bar>blinfun_apply x (axis ia 1) $ i\<bar> \<le> ?g32 x i ia
 2. \<And>x. (\<Sum>i\<in>UNIV. sum (?g32 x i) UNIV) \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply (rule abs_vec_nth_blinfun_apply_lemma)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<Sum>i\<in>UNIV. \<Sum>i\<in>UNIV. norm x) \<le> norm x * (real CARD('n) * real CARD('m))
[PROOF STEP]
apply (simp add: abs_vec_nth_blinfun_apply_lemma)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma matrix_has_derivative:
  shows "((\<lambda>x::(real^'n)\<Rightarrow>\<^sub>L(real^'n). matrix (blinfun_apply x)) has_derivative (\<lambda>h. matrix (blinfun_apply h))) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. matrix (blinfun_apply x)) has_derivative (\<lambda>h. matrix (blinfun_apply h))) (at x)
[PROOF STEP]
apply (auto simp: has_derivative_at2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bounded_linear (\<lambda>h. matrix (blinfun_apply h))
 2. (\<lambda>y. (1 / norm (y - x)) *\<^sub>R (matrix (blinfun_apply y) - (matrix (blinfun_apply x) + matrix (blinfun_apply (y - x))))) \<midarrow>x\<rightarrow> 0
[PROOF STEP]
unfolding linear_linear
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bounded_linear (\<lambda>h. matrix (blinfun_apply h))
 2. (\<lambda>y. (1 / norm (y - x)) *\<^sub>R (matrix (blinfun_apply y) - (matrix (blinfun_apply x) + matrix (blinfun_apply (y - x))))) \<midarrow>x\<rightarrow> 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (\<lambda>h. matrix (blinfun_apply h))
[PROOF STEP]
by (rule bounded_linear_matrix_blinfun_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>y. (1 / norm (y - x)) *\<^sub>R (matrix (blinfun_apply y) - (matrix (blinfun_apply x) + matrix (blinfun_apply (y - x))))) \<midarrow>x\<rightarrow> 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>y. (1 / norm (y - x)) *\<^sub>R (matrix (blinfun_apply y) - (matrix (blinfun_apply x) + matrix (blinfun_apply (y - x))))) \<midarrow>x\<rightarrow> 0
[PROOF STEP]
by (auto simp: blinfun.bilinear_simps matrix_def) vector
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma interpret_floatarith_inner_eq:
  assumes "length xs = length ys"
  shows "interpret_floatarith (inner_floatariths xs ys) vs =
    (\<Sum>i<length ys. (interpret_floatariths xs vs ! i) * (interpret_floatariths ys vs ! i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs = length ys

goal (1 subgoal):
 1. interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)
[PROOF STEP]
proof (induction rule: list_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. interpret_floatarith (inner_floatariths [] []) vs = (\<Sum>i<length []. interpret_floatariths [] vs ! i * interpret_floatariths [] vs ! i)
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)\<rbrakk> \<Longrightarrow> interpret_floatarith (inner_floatariths (x # xs) (y # ys)) vs = (\<Sum>i<length (y # ys). interpret_floatariths (x # xs) vs ! i * interpret_floatariths (y # ys) vs ! i)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. interpret_floatarith (inner_floatariths [] []) vs = (\<Sum>i<length []. interpret_floatariths [] vs ! i * interpret_floatariths [] vs ! i)
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)\<rbrakk> \<Longrightarrow> interpret_floatarith (inner_floatariths (x # xs) (y # ys)) vs = (\<Sum>i<length (y # ys). interpret_floatariths (x # xs) vs ! i * interpret_floatariths (y # ys) vs ! i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (inner_floatariths [] []) vs = (\<Sum>i<length []. interpret_floatariths [] vs ! i * interpret_floatariths [] vs ! i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
interpret_floatarith (inner_floatariths [] []) vs = (\<Sum>i<length []. interpret_floatariths [] vs ! i * interpret_floatariths [] vs ! i)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)\<rbrakk> \<Longrightarrow> interpret_floatarith (inner_floatariths (x # xs) (y # ys)) vs = (\<Sum>i<length (y # ys). interpret_floatariths (x # xs) vs ! i * interpret_floatariths (y # ys) vs ! i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)\<rbrakk> \<Longrightarrow> interpret_floatarith (inner_floatariths (x # xs) (y # ys)) vs = (\<Sum>i<length (y # ys). interpret_floatariths (x # xs) vs ! i * interpret_floatariths (y # ys) vs ! i)
[PROOF STEP]
case (Cons x xs y ys)
[PROOF STATE]
proof (state)
this:
length xs = length ys
interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)\<rbrakk> \<Longrightarrow> interpret_floatarith (inner_floatariths (x # xs) (y # ys)) vs = (\<Sum>i<length (y # ys). interpret_floatariths (x # xs) vs ! i * interpret_floatariths (y # ys) vs ! i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs = length ys
interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)

goal (1 subgoal):
 1. interpret_floatarith (inner_floatariths (x # xs) (y # ys)) vs = (\<Sum>i<length (y # ys). interpret_floatariths (x # xs) vs ! i * interpret_floatariths (y # ys) vs ! i)
[PROOF STEP]
unfolding length_Cons sum.lessThan_Suc_shift
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
interpret_floatarith (inner_floatariths xs ys) vs = (\<Sum>i<length ys. interpret_floatariths xs vs ! i * interpret_floatariths ys vs ! i)

goal (1 subgoal):
 1. interpret_floatarith (inner_floatariths (x # xs) (y # ys)) vs = interpret_floatariths (x # xs) vs ! 0 * interpret_floatariths (y # ys) vs ! 0 + (\<Sum>i<length ys. interpret_floatariths (x # xs) vs ! Suc i * interpret_floatariths (y # ys) vs ! Suc i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
interpret_floatarith (inner_floatariths (x # xs) (y # ys)) vs = (\<Sum>i<length (y # ys). interpret_floatariths (x # xs) vs ! i * interpret_floatariths (y # ys) vs ! i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_Var_floatarith_inner_floatariths[simp]:
  assumes "length f = length g"
  shows "max_Var_floatarith (inner_floatariths f g) = max (max_Var_floatariths f) (max_Var_floatariths g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatarith (inner_floatariths f g) = max (max_Var_floatariths f) (max_Var_floatariths g)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length f = length g

goal (1 subgoal):
 1. max_Var_floatarith (inner_floatariths f g) = max (max_Var_floatariths f) (max_Var_floatariths g)
[PROOF STEP]
by (induction f g rule: list_induct2) auto


[STATEMENT]
lemma max_Var_floatarith_DERIV_floatarith:
  "max_Var_floatarith (DERIV_floatarith x fa) \<le> max_Var_floatarith fa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatarith (DERIV_floatarith x fa) \<le> max_Var_floatarith fa
[PROOF STEP]
by (induction x fa rule: DERIV_floatarith.induct) (auto)


[STATEMENT]
lemma max_Var_floatarith_FDERIV_floatarith:
  "length xs = length d \<Longrightarrow>
    max_Var_floatarith (FDERIV_floatarith fa xs d) \<le> max (max_Var_floatarith fa) (max_Var_floatariths d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length d \<Longrightarrow> max_Var_floatarith (FDERIV_floatarith fa xs d) \<le> max (max_Var_floatarith fa) (max_Var_floatariths d)
[PROOF STEP]
unfolding FDERIV_floatarith_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length d \<Longrightarrow> max_Var_floatarith (inner_floatariths (map (\<lambda>x. fold_const_fa (DERIV_floatarith x fa)) xs) d) \<le> max (max_Var_floatarith fa) (max_Var_floatariths d)
[PROOF STEP]
by (auto simp: max_Var_floatariths_Max intro!: max_Var_floatarith_DERIV_floatarith[THEN order_trans]
      max_Var_floatarith_fold_const_fa[THEN order_trans])


[STATEMENT]
lemma max_Var_floatarith_FDERIV_floatariths:
  "length xs = length d \<Longrightarrow> max_Var_floatariths (FDERIV_floatariths fa xs d) \<le> max (max_Var_floatariths fa) (max_Var_floatariths d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length d \<Longrightarrow> max_Var_floatariths (FDERIV_floatariths fa xs d) \<le> max (max_Var_floatariths fa) (max_Var_floatariths d)
[PROOF STEP]
by (auto simp: FDERIV_floatariths_def max_Var_floatariths_Max
      intro!: max_Var_floatarith_FDERIV_floatarith[THEN order_trans])
    (auto simp: max_def)


[STATEMENT]
lemma length_FDERIV_floatariths[simp]:
  "length (FDERIV_floatariths fas xs ds) = length fas"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (FDERIV_floatariths fas xs ds) = length fas
[PROOF STEP]
by (auto simp: FDERIV_floatariths_def)


[STATEMENT]
lemma FDERIV_floatariths_nth[simp]:
  "i < length fas \<Longrightarrow> FDERIV_floatariths fas xs ds ! i  = FDERIV_floatarith (fas ! i) xs ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length fas \<Longrightarrow> FDERIV_floatariths fas xs ds ! i = FDERIV_floatarith (fas ! i) xs ds
[PROOF STEP]
by (auto simp: FDERIV_floatariths_def)


[STATEMENT]
lemma FDERIV_n_floatariths_Suc[simp]:
  "FDERIV_n_floatariths fa xs ds 0 = fa"
  "FDERIV_n_floatariths fa xs ds (Suc n) = FDERIV_floatariths (FDERIV_n_floatariths fa xs ds n) xs ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FDERIV_n_floatariths fa xs ds 0 = fa &&& FDERIV_n_floatariths fa xs ds (Suc n) = FDERIV_floatariths (FDERIV_n_floatariths fa xs ds n) xs ds
[PROOF STEP]
by (auto simp: FDERIV_n_floatariths_def)


[STATEMENT]
lemma length_FDERIV_n_floatariths[simp]: "length (FDERIV_n_floatariths fa xs ds n) = length fa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (FDERIV_n_floatariths fa xs ds n) = length fa
[PROOF STEP]
by (induction n) (auto simp: FDERIV_n_floatariths_def)


[STATEMENT]
lemma max_Var_floatarith_FDERIV_n_floatariths:
  "length xs = length d \<Longrightarrow> max_Var_floatariths (FDERIV_n_floatariths fa xs d n) \<le> max (max_Var_floatariths fa) (max_Var_floatariths d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length d \<Longrightarrow> max_Var_floatariths (FDERIV_n_floatariths fa xs d n) \<le> max (max_Var_floatariths fa) (max_Var_floatariths d)
[PROOF STEP]
by (induction n)
    (auto intro!: max_Var_floatarith_FDERIV_floatariths[THEN order_trans] simp: FDERIV_n_floatariths_def)


[STATEMENT]
lemma interpret_floatarith_FDERIV_floatarith_cong:
  assumes rq: "\<And>i. i < max_Var_floatarith f \<Longrightarrow> rs ! i = qs ! i"
  assumes [simp]: "length ds = length xs" "length es = length xs"
  assumes "interpret_floatariths ds qs = interpret_floatariths es rs"
  shows "interpret_floatarith (FDERIV_floatarith f xs ds) qs =
   interpret_floatarith (FDERIV_floatarith f xs es) rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (FDERIV_floatarith f xs ds) qs = interpret_floatarith (FDERIV_floatarith f xs es) rs
[PROOF STEP]
apply (auto simp: FDERIV_floatarith_def interpret_floatarith_inner_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<length xs. interpret_floatarith (DERIV_floatarith (xs ! i) f) qs * interpret_floatarith (ds ! i) qs) = (\<Sum>i<length xs. interpret_floatarith (DERIV_floatarith (xs ! i) f) rs * interpret_floatarith (es ! i) rs)
[PROOF STEP]
apply (rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {..<length xs} \<Longrightarrow> interpret_floatarith (DERIV_floatarith (xs ! x) f) qs * interpret_floatarith (ds ! x) qs = interpret_floatarith (DERIV_floatarith (xs ! x) f) rs * interpret_floatarith (es ! x) rs
[PROOF STEP]
subgoal premises prems for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (DERIV_floatarith (xs ! i) f) qs * interpret_floatarith (ds ! i) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs * interpret_floatarith (es ! i) rs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith (DERIV_floatarith (xs ! i) f) qs * interpret_floatarith (ds ! i) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs * interpret_floatarith (es ! i) rs
[PROOF STEP]
have "interpret_floatarith (DERIV_floatarith (xs ! i) f) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (DERIV_floatarith (xs ! i) f) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs
[PROOF STEP]
apply (rule interpret_floatarith_max_Var_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. ia < max_Var_floatarith (DERIV_floatarith (xs ! i) f) \<Longrightarrow> rs ! ia = qs ! ia
[PROOF STEP]
apply (auto simp: intro!: rq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. ia < max_Var_floatarith (DERIV_floatarith (xs ! i) f) \<Longrightarrow> ia < max_Var_floatarith f
[PROOF STEP]
by (metis leD le_trans max_Var_floatarith_DERIV_floatarith nat_less_le)
[PROOF STATE]
proof (state)
this:
interpret_floatarith (DERIV_floatarith (xs ! i) f) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs

goal (1 subgoal):
 1. interpret_floatarith (DERIV_floatarith (xs ! i) f) qs * interpret_floatarith (ds ! i) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs * interpret_floatarith (es ! i) rs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interpret_floatarith (DERIV_floatarith (xs ! i) f) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs

goal (1 subgoal):
 1. interpret_floatarith (DERIV_floatarith (xs ! i) f) qs * interpret_floatarith (ds ! i) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs * interpret_floatarith (es ! i) rs
[PROOF STEP]
have "interpret_floatarith (ds ! i) qs = interpret_floatarith (es ! i) rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (ds ! i) qs = interpret_floatarith (es ! i) rs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i < max_Var_floatarith f \<Longrightarrow> rs ! ?i = qs ! ?i
length ds = length xs
length es = length xs
interpret_floatariths ds qs = interpret_floatariths es rs

goal (1 subgoal):
 1. interpret_floatarith (ds ! i) qs = interpret_floatarith (es ! i) rs
[PROOF STEP]
by (metis \<open>i \<in> {..<length xs}\<close> interpret_floatariths_nth lessThan_iff)
[PROOF STATE]
proof (state)
this:
interpret_floatarith (ds ! i) qs = interpret_floatarith (es ! i) rs

goal (1 subgoal):
 1. interpret_floatarith (DERIV_floatarith (xs ! i) f) qs * interpret_floatarith (ds ! i) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs * interpret_floatarith (es ! i) rs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
interpret_floatarith (DERIV_floatarith (xs ! i) f) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs
interpret_floatarith (ds ! i) qs = interpret_floatarith (es ! i) rs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interpret_floatarith (DERIV_floatarith (xs ! i) f) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs
interpret_floatarith (ds ! i) qs = interpret_floatarith (es ! i) rs

goal (1 subgoal):
 1. interpret_floatarith (DERIV_floatarith (xs ! i) f) qs * interpret_floatarith (ds ! i) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs * interpret_floatarith (es ! i) rs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
interpret_floatarith (DERIV_floatarith (xs ! i) f) qs * interpret_floatarith (ds ! i) qs = interpret_floatarith (DERIV_floatarith (xs ! i) f) rs * interpret_floatarith (es ! i) rs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma length_mmult_fa[simp]: "length (mmult_fa l m n AS BS) = l * n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (mmult_fa l m n AS BS) = l * n
[PROOF STEP]
by (auto simp: mmult_fa_def length_concat o_def sum_list_distinct_conv_sum_set)


[STATEMENT]
lemma einterpret_mmult_fa:
  assumes [simp]: "Dn = CARD('n::enum)" "Dm = CARD('m::enum)" "Dl = CARD('l::enum)"
    "length A = CARD('l)*CARD('m)" "length B = CARD('m)*CARD('n)"
  shows "einterpret (mmult_fa Dl Dm Dn A B) vs = (einterpret A vs::((real, 'm::enum) vec, 'l) vec) ** (einterpret B vs::((real, 'n::enum) vec, 'm) vec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. einterpret (mmult_fa Dl Dm Dn A B) vs = einterpret A vs ** einterpret B vs
[PROOF STEP]
apply (vector matrix_matrix_mult_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i ia. einterpret (mmult_fa Dl Dm Dn A B) vs $ i $ ia = (\<Sum>k\<in>UNIV. einterpret A vs $ i $ k * einterpret B vs $ k $ ia)
[PROOF STEP]
apply (auto simp: mmult_fa_def vec_nth_eucl_of_list_eq2 index_Basis_list_axis2
      concat_map_map_index length_concat o_def sum_list_distinct_conv_sum_set
      interpret_floatarith_inner_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. (\<Sum>ib<CARD('m). interpret_floatarith (A ! (index enum_class.enum i * CARD('m) + ib)) vs * interpret_floatarith (B ! (ib * CARD('n) + index enum_class.enum ia)) vs) = (\<Sum>k\<in>UNIV. interpret_floatarith (A ! (index enum_class.enum i * CARD('m) + index enum_class.enum k)) vs * interpret_floatarith (B ! (index enum_class.enum k * CARD('n) + index enum_class.enum ia)) vs)
[PROOF STEP]
apply (subst sum_index_enum_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. (\<Sum>ib<CARD('m). interpret_floatarith (A ! (index enum_class.enum i * CARD('m) + ib)) vs * interpret_floatarith (B ! (ib * CARD('n) + index enum_class.enum ia)) vs) = (\<Sum>ib<CARD('m). interpret_floatarith (A ! (index enum_class.enum i * CARD('m) + ib)) vs * interpret_floatarith (B ! (ib * CARD('n) + index enum_class.enum ia)) vs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma max_Var_floatariths_mmult_fa:
  assumes [simp]: "length A = D * E" "length B = E * F"
  shows "max_Var_floatariths (mmult_fa D E F A B) \<le> max (max_Var_floatariths A) (max_Var_floatariths B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (mmult_fa D E F A B) \<le> max (max_Var_floatariths A) (max_Var_floatariths B)
[PROOF STEP]
apply (auto simp: mmult_fa_def concat_map_map_index intro!: max_Var_floatariths_leI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i ia. \<lbrakk>i < F * D; ia < E\<rbrakk> \<Longrightarrow> max_Var_floatarith (A ! (i div F * E + ia)) \<le> max (max_Var_floatariths A) (max_Var_floatariths B)
 2. \<And>i ia. \<lbrakk>i < F * D; ia < E\<rbrakk> \<Longrightarrow> max_Var_floatarith (B ! (ia * F + [0..<F] ! (i mod F))) \<le> max (max_Var_floatariths A) (max_Var_floatariths B)
[PROOF STEP]
apply (rule max.coboundedI1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i ia. \<lbrakk>i < F * D; ia < E\<rbrakk> \<Longrightarrow> max_Var_floatarith (A ! (i div F * E + ia)) \<le> max_Var_floatariths A
 2. \<And>i ia. \<lbrakk>i < F * D; ia < E\<rbrakk> \<Longrightarrow> max_Var_floatarith (B ! (ia * F + [0..<F] ! (i mod F))) \<le> max (max_Var_floatariths A) (max_Var_floatariths B)
[PROOF STEP]
apply (auto intro!: max_Var_floatarith_le_max_Var_floatariths_nth max.coboundedI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>i < F * D; ia < E\<rbrakk> \<Longrightarrow> ia * F + [0..<F] ! (i mod F) < E * F
[PROOF STEP]
apply (cases "F = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i ia. \<lbrakk>i < F * D; ia < E; F = 0\<rbrakk> \<Longrightarrow> ia * F + [0..<F] ! (i mod F) < E * F
 2. \<And>i ia. \<lbrakk>i < F * D; ia < E; F \<noteq> 0\<rbrakk> \<Longrightarrow> ia * F + [0..<F] ! (i mod F) < E * F
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma isDERIV_inner_iff:
  assumes "length xs = length ys"
  shows "isDERIV i (inner_floatariths xs ys) vs \<longleftrightarrow>
    (\<forall>k < length xs. isDERIV i (xs ! k) vs) \<and> (\<forall>k < length ys. isDERIV i (ys ! k) vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV i (inner_floatariths xs ys) vs = ((\<forall>k<length xs. isDERIV i (xs ! k) vs) \<and> (\<forall>k<length ys. isDERIV i (ys ! k) vs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs = length ys

goal (1 subgoal):
 1. isDERIV i (inner_floatariths xs ys) vs = ((\<forall>k<length xs. isDERIV i (xs ! k) vs) \<and> (\<forall>k<length ys. isDERIV i (ys ! k) vs))
[PROOF STEP]
by (induction xs ys rule: list_induct2) (auto simp: nth_Cons split: nat.splits)


[STATEMENT]
lemma isDERIV_Power: "isDERIV x (fa) vs \<Longrightarrow> isDERIV x (fa ^\<^sub>e n) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x fa vs \<Longrightarrow> isDERIV x (fa ^\<^sub>e n) vs
[PROOF STEP]
by (induction n) (auto simp: FDERIV_floatarith_def isDERIV_inner_iff)


[STATEMENT]
lemma isDERIV_mmult_fa_nth:
  assumes "\<And>j. j < D * E \<Longrightarrow> isDERIV i (A ! j) xs"
  assumes "\<And>j. j < E * F \<Longrightarrow> isDERIV i (B ! j) xs"
  assumes [simp]: "length A = D * E" "length B = E * F" "j < D * F"
  shows "isDERIV i (mmult_fa D E F A B ! j) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV i (mmult_fa D E F A B ! j) xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?j < D * E \<Longrightarrow> isDERIV i (A ! ?j) xs
?j < E * F \<Longrightarrow> isDERIV i (B ! ?j) xs
length A = D * E
length B = E * F
j < D * F

goal (1 subgoal):
 1. isDERIV i (mmult_fa D E F A B ! j) xs
[PROOF STEP]
apply (cases "F = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>j. j < D * E \<Longrightarrow> isDERIV i (A ! j) xs; \<And>j. j < E * F \<Longrightarrow> isDERIV i (B ! j) xs; length A = D * E; length B = E * F; j < D * F; F = 0\<rbrakk> \<Longrightarrow> isDERIV i (mmult_fa D E F A B ! j) xs
 2. \<lbrakk>\<And>j. j < D * E \<Longrightarrow> isDERIV i (A ! j) xs; \<And>j. j < E * F \<Longrightarrow> isDERIV i (B ! j) xs; length A = D * E; length B = E * F; j < D * F; F \<noteq> 0\<rbrakk> \<Longrightarrow> isDERIV i (mmult_fa D E F A B ! j) xs
[PROOF STEP]
apply (auto simp: mmult_fa_def concat_map_map_index isDERIV_inner_iff ac_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>j. j < D * E \<Longrightarrow> isDERIV i (A ! j) xs; \<And>j. j < E * F \<Longrightarrow> isDERIV i (B ! j) xs; 0 < F; k < E\<rbrakk> \<Longrightarrow> isDERIV i (A ! (k + E * (j div F))) xs
[PROOF STEP]
apply (metis add.commute assms(5) in_square_lemma less_square_imp_div_less mult.commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma einterpret_mvmult_fa:
  assumes [simp]: "Dn = CARD('n::enum)" "Dm = CARD('m::enum)"
    "length A = CARD('n)*CARD('m)" "length B = CARD('m)"
  shows "einterpret (mvmult_fa Dn Dm A B) vs = (einterpret A vs::((real, 'm::enum) vec, 'n) vec) *v (einterpret B vs::(real, 'm) vec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. einterpret (mvmult_fa Dn Dm A B) vs = einterpret A vs *v einterpret B vs
[PROOF STEP]
apply (vector matrix_vector_mult_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. einterpret (mvmult_fa Dn Dm A B) vs $ i = (\<Sum>j\<in>UNIV. einterpret A vs $ i $ j * einterpret B vs $ j)
[PROOF STEP]
apply (auto simp: mvmult_fa_def vec_nth_eucl_of_list_eq2 index_Basis_list_axis2 index_Basis_list_axis1 vec_nth_eucl_of_list_eq
      concat_map_map_index length_concat o_def sum_list_distinct_conv_sum_set
      interpret_floatarith_inner_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (\<Sum>ia<CARD('m). interpret_floatarith (A ! (index enum_class.enum i * CARD('m) + ia)) vs * interpret_floatarith (B ! ia) vs) = (\<Sum>j\<in>UNIV. interpret_floatarith (A ! (index enum_class.enum i * CARD('m) + index enum_class.enum j)) vs * interpret_floatarith (B ! index enum_class.enum j) vs)
[PROOF STEP]
apply (subst sum_index_enum_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (\<Sum>ia<CARD('m). interpret_floatarith (A ! (index enum_class.enum i * CARD('m) + ia)) vs * interpret_floatarith (B ! ia) vs) = (\<Sum>ia<CARD('m). interpret_floatarith (A ! (index enum_class.enum i * CARD('m) + ia)) vs * interpret_floatarith (B ! ia) vs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma max_Var_floatariths_mvult_fa:
  assumes [simp]: "length A = D * E" "length B = E"
  shows "max_Var_floatariths (mvmult_fa D E A B) \<le> max (max_Var_floatariths A) (max_Var_floatariths B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (mvmult_fa D E A B) \<le> max (max_Var_floatariths A) (max_Var_floatariths B)
[PROOF STEP]
apply (auto simp: mvmult_fa_def concat_map_map_index intro!: max_Var_floatariths_leI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>i < D; ia < E\<rbrakk> \<Longrightarrow> max_Var_floatarith (A ! (i * E + ia)) \<le> max (max_Var_floatariths A) (max_Var_floatariths B)
[PROOF STEP]
apply (rule max.coboundedI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>i < D; ia < E\<rbrakk> \<Longrightarrow> max_Var_floatarith (A ! (i * E + ia)) \<le> max_Var_floatariths A
[PROOF STEP]
by (auto intro!: max_Var_floatarith_le_max_Var_floatariths_nth max.coboundedI2)


[STATEMENT]
lemma isDERIV_mvmult_fa_nth:
  assumes "\<And>j. j < D * E \<Longrightarrow> isDERIV i (A ! j) xs"
  assumes "\<And>j. j < E \<Longrightarrow> isDERIV i (B ! j) xs"
  assumes [simp]: "length A = D * E" "length B = E" "j < D"
  shows "isDERIV i (mvmult_fa D E A B ! j) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV i (mvmult_fa D E A B ! j) xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?j < D * E \<Longrightarrow> isDERIV i (A ! ?j) xs
?j < E \<Longrightarrow> isDERIV i (B ! ?j) xs
length A = D * E
length B = E
j < D

goal (1 subgoal):
 1. isDERIV i (mvmult_fa D E A B ! j) xs
[PROOF STEP]
apply (auto simp: mvmult_fa_def concat_map_map_index isDERIV_inner_iff ac_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>j. j < D * E \<Longrightarrow> isDERIV i (A ! j) xs; \<And>j. j < E \<Longrightarrow> isDERIV i (B ! j) xs; k < E\<rbrakk> \<Longrightarrow> isDERIV i (A ! (k + E * j)) xs
[PROOF STEP]
by (metis assms(5) in_square_lemma semiring_normalization_rules(24) semiring_normalization_rules(7))


[STATEMENT]
lemma max_Var_floatariths_mapI:
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> max_Var_floatarith (f x) \<le> m"
  shows "max_Var_floatariths (map f xs) \<le> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (map f xs) \<le> m
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> max_Var_floatarith (f ?x) \<le> m

goal (1 subgoal):
 1. max_Var_floatariths (map f xs) \<le> m
[PROOF STEP]
by (force intro!: max_Var_floatariths_leI simp: in_set_conv_nth)


[STATEMENT]
lemma FDERIV_n_floatariths_nth: "i < length fas \<Longrightarrow> FDERIV_n_floatariths fas xs ds n ! i = FDERIV_n_floatarith (fas ! i) xs ds n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length fas \<Longrightarrow> FDERIV_n_floatariths fas xs ds n ! i = FDERIV_n_floatarith (fas ! i) xs ds n
[PROOF STEP]
by (induction n)
    (auto simp: FDERIV_n_floatarith_def FDERIV_floatariths_nth)


[STATEMENT]
lemma einterpret_fold_const_fa[simp]:
  "(einterpret (map (\<lambda>i. fold_const_fa (fa i)) xs) vs::'a::executable_euclidean_space) =
    einterpret (map fa xs) vs" if "length xs = DIM('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. einterpret (map (\<lambda>i. fold_const_fa (fa i)) xs) vs = einterpret (map fa xs) vs
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
length xs = DIM('a)

goal (1 subgoal):
 1. einterpret (map (\<lambda>i. fold_const_fa (fa i)) xs) vs = einterpret (map fa xs) vs
[PROOF STEP]
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner)


[STATEMENT]
lemma einterpret_plus[simp]:
  shows "(einterpret (map (\<lambda>i. fa1 i + fa2 i) [0..<DIM('a)]) vs::'a) =
    einterpret (map fa1 [0..<DIM('a::executable_euclidean_space)]) vs + einterpret (map fa2 [0..<DIM('a)]) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. einterpret (map (\<lambda>i. fa1 i + fa2 i) [0..<DIM('a)]) vs = einterpret (map fa1 [0..<DIM('a)]) vs + einterpret (map fa2 [0..<DIM('a)]) vs
[PROOF STEP]
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner)


[STATEMENT]
lemma einterpret_uminus[simp]:
  shows "(einterpret (map (\<lambda>i. - fa1 i) [0..<DIM('a)]) vs::'a::executable_euclidean_space) =
    - einterpret (map fa1 [0..<DIM('a)]) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. einterpret (map (\<lambda>i. - fa1 i) [0..<DIM('a)]) vs = - einterpret (map fa1 [0..<DIM('a)]) vs
[PROOF STEP]
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner)


[STATEMENT]
lemma diff_floatarith_conv_add_uminus: "a - b = a + - b" for a b::floatarith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a - b = a + - b
[PROOF STEP]
by (auto simp: minus_floatarith_def plus_floatarith_def uminus_floatarith_def)


[STATEMENT]
lemma einterpret_minus[simp]:
  shows "(einterpret (map (\<lambda>i. fa1 i - fa2 i) [0..<DIM('a)]) vs::'a::executable_euclidean_space) =
    einterpret (map fa1 [0..<DIM('a)]) vs - einterpret (map fa2 [0..<DIM('a)]) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. einterpret (map (\<lambda>i. fa1 i - fa2 i) [0..<DIM('a)]) vs = einterpret (map fa1 [0..<DIM('a)]) vs - einterpret (map fa2 [0..<DIM('a)]) vs
[PROOF STEP]
by (simp add: diff_floatarith_conv_add_uminus)


[STATEMENT]
lemma einterpret_scaleR[simp]:
  shows "(einterpret (map (\<lambda>i. fa1 * fa2 i) [0..<DIM('a)]) vs::'a::executable_euclidean_space) =
    interpret_floatarith (fa1) vs *\<^sub>R einterpret (map fa2 [0..<DIM('a)]) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. einterpret (map (\<lambda>i. fa1 * fa2 i) [0..<DIM('a)]) vs = interpret_floatarith fa1 vs *\<^sub>R einterpret (map fa2 [0..<DIM('a)]) vs
[PROOF STEP]
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner)


[STATEMENT]
lemma einterpret_nth[simp]:
  assumes [simp]: "length xs = DIM('a)"
  shows "(einterpret (map ((!) xs) [0..<DIM('a)]) vs::'a::executable_euclidean_space) = einterpret xs vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. einterpret (map ((!) xs) [0..<DIM('a)]) vs = einterpret xs vs
[PROOF STEP]
by (auto intro!: euclidean_eqI[where 'a='a] simp: algebra_simps eucl_of_list_inner)


[STATEMENT]
lemma length_mvmult_fa[simp]: "length (mvmult_fa D E xs ys) = D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (mvmult_fa D E xs ys) = D
[PROOF STEP]
by (auto simp: mvmult_fa_def)


[STATEMENT]
lemma interpret_mvmult_nth:
  assumes "D = CARD('n::enum)"
  assumes "E = CARD('m::enum)"
  assumes "length xs = D * E"
  assumes "length ys = E"
  assumes "n < CARD('n)"
  shows "interpret_floatarith (mvmult_fa D E xs ys ! n) vs =
    ((einterpret xs vs::((real, 'm) vec, 'n) vec) *v einterpret ys vs) \<bullet> (Basis_list ! n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (mvmult_fa D E xs ys ! n) vs = (einterpret xs vs *v einterpret ys vs) \<bullet> Basis_list ! n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatarith (mvmult_fa D E xs ys ! n) vs = (einterpret xs vs *v einterpret ys vs) \<bullet> Basis_list ! n
[PROOF STEP]
have "interpret_floatarith (mvmult_fa D E xs ys ! n) vs = einterpret (mvmult_fa D E xs ys) vs \<bullet> (Basis_list ! n::'n rvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (mvmult_fa D E xs ys ! n) vs = einterpret (mvmult_fa D E xs ys) vs \<bullet> Basis_list ! n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
D = CARD('n)
E = CARD('m)
length xs = D * E
length ys = E
n < CARD('n)

goal (1 subgoal):
 1. interpret_floatarith (mvmult_fa D E xs ys ! n) vs = einterpret (mvmult_fa D E xs ys) vs \<bullet> Basis_list ! n
[PROOF STEP]
by (auto simp: eucl_of_list_inner)
[PROOF STATE]
proof (state)
this:
interpret_floatarith (mvmult_fa D E xs ys ! n) vs = einterpret (mvmult_fa D E xs ys) vs \<bullet> Basis_list ! n

goal (1 subgoal):
 1. interpret_floatarith (mvmult_fa D E xs ys ! n) vs = (einterpret xs vs *v einterpret ys vs) \<bullet> Basis_list ! n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
interpret_floatarith (mvmult_fa D E xs ys ! n) vs = einterpret (mvmult_fa D E xs ys) vs \<bullet> Basis_list ! n

goal (1 subgoal):
 1. interpret_floatarith (mvmult_fa D E xs ys ! n) vs = (einterpret xs vs *v einterpret ys vs) \<bullet> Basis_list ! n
[PROOF STEP]
from einterpret_mvmult_fa[OF assms(1,2), of xs ys vs]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length xs = CARD('n) * CARD('m); length ys = CARD('m)\<rbrakk> \<Longrightarrow> einterpret (mvmult_fa D E xs ys) vs = einterpret xs vs *v einterpret ys vs
[PROOF STEP]
have "einterpret (mvmult_fa D E xs ys) vs = (einterpret xs vs::((real, 'm) vec, 'n) vec) *v einterpret ys vs"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs = CARD('n) * CARD('m); length ys = CARD('m)\<rbrakk> \<Longrightarrow> einterpret (mvmult_fa D E xs ys) vs = einterpret xs vs *v einterpret ys vs

goal (1 subgoal):
 1. einterpret (mvmult_fa D E xs ys) vs = einterpret xs vs *v einterpret ys vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs = CARD('n) * CARD('m); length ys = CARD('m)\<rbrakk> \<Longrightarrow> einterpret (mvmult_fa D E xs ys) vs = einterpret xs vs *v einterpret ys vs
D = CARD('n)
E = CARD('m)
length xs = D * E
length ys = E
n < CARD('n)

goal (1 subgoal):
 1. einterpret (mvmult_fa D E xs ys) vs = einterpret xs vs *v einterpret ys vs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
einterpret (mvmult_fa D E xs ys) vs = einterpret xs vs *v einterpret ys vs

goal (1 subgoal):
 1. interpret_floatarith (mvmult_fa D E xs ys ! n) vs = (einterpret xs vs *v einterpret ys vs) \<bullet> Basis_list ! n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
interpret_floatarith (mvmult_fa D E xs ys ! n) vs = (einterpret xs vs *v einterpret ys vs) \<bullet> Basis_list ! n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interpret_floatarith (mvmult_fa D E xs ys ! n) vs = (einterpret xs vs *v einterpret ys vs) \<bullet> Basis_list ! n

goal (1 subgoal):
 1. interpret_floatarith (mvmult_fa D E xs ys ! n) vs = (einterpret xs vs *v einterpret ys vs) \<bullet> Basis_list ! n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
interpret_floatarith (mvmult_fa D E xs ys ! n) vs = (einterpret xs vs *v einterpret ys vs) \<bullet> Basis_list ! n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma take_eq_map_nth: "n < length xs \<Longrightarrow> take n xs = map ((!) xs) [0..<n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> take n xs = map ((!) xs) [0..<n]
[PROOF STEP]
by (induction xs) (auto intro!: nth_equalityI)


[STATEMENT]
lemma interpret_Floatreal: "interpret_floatarith (floatarith.Num f) vs = (real_of_float f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (Num f) vs = real_of_float f
[PROOF STEP]
by simp


[STATEMENT]
lemma eucl_of_list_interpret_floatariths_cong:
  fixes y::"'a::executable_euclidean_space"
  assumes "\<And>b. b \<in> Basis \<Longrightarrow> interpret_floatarith (fa (index Basis_list b)) vs = y \<bullet> b"
  assumes "length xs = DIM('a)"
  shows "eucl_of_list (interpret_floatariths (map fa [0..<DIM('a)]) vs) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. einterpret (map fa [0..<DIM('a)]) vs = y
[PROOF STEP]
apply (rule euclidean_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. b \<in> Basis \<Longrightarrow> einterpret (map fa [0..<DIM('a)]) vs \<bullet> b = y \<bullet> b
[PROOF STEP]
apply (subst eucl_of_list_inner)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b. b \<in> Basis \<Longrightarrow> b \<in> Basis
 2. \<And>b. b \<in> Basis \<Longrightarrow> length (interpret_floatariths (map fa [0..<DIM('a)]) vs) = DIM('a)
 3. \<And>b. b \<in> Basis \<Longrightarrow> interpret_floatariths (map fa [0..<DIM('a)]) vs ! index Basis_list b = y \<bullet> b
[PROOF STEP]
by (auto simp: assms)


[STATEMENT]
lemma interpret_floatariths_fold_const_fa[simp]:
  "interpret_floatariths (map fold_const_fa ds) = interpret_floatariths ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatariths (map fold_const_fa ds) = interpret_floatariths ds
[PROOF STEP]
by (auto intro!: nth_equalityI)


[STATEMENT]
lemma interpret_floatarith_subst_floatarith:
  assumes "max_Var_floatarith fa \<le> D"
  shows "interpret_floatarith (subst_floatarith s fa) vs =
    interpret_floatarith fa (map (\<lambda>i. interpret_floatarith (s i) vs) [0..<D])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (subst_floatarith s fa) vs = interpret_floatarith fa (map (\<lambda>i. interpret_floatarith (s i) vs) [0..<D])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
max_Var_floatarith fa \<le> D

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


[STATEMENT]
lemma max_Var_floatarith_subst_floatarith_le[THEN order_trans]:
  assumes "length xs \<ge> max_Var_floatarith fa"
  shows "max_Var_floatarith (subst_floatarith ((!) xs) fa) \<le> max_Var_floatariths xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatarith (subst_floatarith ((!) xs) fa) \<le> max_Var_floatariths xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
max_Var_floatarith fa \<le> length xs

goal (1 subgoal):
 1. max_Var_floatarith (subst_floatarith ((!) xs) fa) \<le> max_Var_floatariths xs
[PROOF STEP]
by (induction fa) (auto intro!: max_Var_floatarith_le_max_Var_floatariths_nth)


[STATEMENT]
lemma max_Var_floatariths_subst_floatarith_le[THEN order_trans]:
  assumes "length xs \<ge> max_Var_floatariths fas"
  shows "max_Var_floatariths (map (subst_floatarith ((!) xs)) fas) \<le> max_Var_floatariths xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (map (subst_floatarith ((!) xs)) fas) \<le> max_Var_floatariths xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
max_Var_floatariths fas \<le> length xs

goal (1 subgoal):
 1. max_Var_floatariths (map (subst_floatarith ((!) xs)) fas) \<le> max_Var_floatariths xs
[PROOF STEP]
by (induction fas) (auto simp: max_Var_floatarith_subst_floatarith_le)


[STATEMENT]
lemma interpret_floatarith_Norm:
  "interpret_floatarith (Norm xs) vs = L2_set (\<lambda>i. interpret_floatarith (xs ! i) vs) {0..<length xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (Norm xs) vs = L2_set (\<lambda>i. interpret_floatarith (xs ! i) vs) {0..<length xs}
[PROOF STEP]
by (auto simp: Norm_def L2_set_def sum_list_sum_nth power2_eq_square)


[STATEMENT]
lemma interpret_floatarith_Nr[simp]: "interpret_floatarith (N\<^sub>r U) vs = real_of_float (float_of U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (N\<^sub>r U) vs = real_of_float (float_of U)
[PROOF STEP]
by (auto simp: N\<^sub>r_def)


[STATEMENT]
lemma list_updates_nth_notmem:
  assumes "length xs = length ys"
  assumes "i \<notin> set xs"
  shows "list_updates xs ys vs ! i = vs ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_updates xs ys vs ! i = vs ! i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
i \<notin> set xs

goal (1 subgoal):
 1. list_updates xs ys vs ! i = vs ! i
[PROOF STEP]
by (induction xs ys arbitrary: i vs rule: list_induct2) auto


[STATEMENT]
lemma list_updates_nth_less:
  assumes "length xs = length ys" "distinct xs"
  assumes "i < length vs"
  shows "list_updates xs ys vs ! i = (if i \<in> set xs then ys ! (index xs i) else vs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_updates xs ys vs ! i = (if i \<in> set xs then ys ! index xs i else vs ! i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
distinct xs
i < length vs

goal (1 subgoal):
 1. list_updates xs ys vs ! i = (if i \<in> set xs then ys ! index xs i else vs ! i)
[PROOF STEP]
by (induction xs ys arbitrary: i vs rule: list_induct2) (auto simp: list_updates_nth_notmem)


[STATEMENT]
lemma length_list_updates[simp]: "length (list_updates xs ys vs) = length vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (list_updates xs ys vs) = length vs
[PROOF STEP]
by (induction xs ys vs rule: list_updates.induct) simp_all


[STATEMENT]
lemma list_updates_nth_ge[simp]:
  "x \<ge> length vs \<Longrightarrow> length xs = length ys \<Longrightarrow> list_updates xs ys vs ! x = vs ! x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length vs \<le> x; length xs = length ys\<rbrakk> \<Longrightarrow> list_updates xs ys vs ! x = vs ! x
[PROOF STEP]
apply (induction xs ys vs rule: list_updates.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_ xs. \<lbrakk>length xs \<le> x; length [] = length uu_\<rbrakk> \<Longrightarrow> list_updates [] uu_ xs ! x = xs ! x
 2. \<And>v va xs. \<lbrakk>length xs \<le> x; length (v # va) = length []\<rbrakk> \<Longrightarrow> list_updates (v # va) [] xs ! x = xs ! x
 3. \<And>i is u us xs. \<lbrakk>\<lbrakk>length (xs[i := u]) \<le> x; length is = length us\<rbrakk> \<Longrightarrow> list_updates is us (xs[i := u]) ! x = xs[i := u] ! x; length xs \<le> x; length (i # is) = length (u # us)\<rbrakk> \<Longrightarrow> list_updates (i # is) (u # us) xs ! x = xs ! x
[PROOF STEP]
apply (auto simp: nth_list_update)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i is u us xs. \<lbrakk>list_updates is us (xs[i := u]) ! x = xs[i := u] ! x; length xs \<le> x; length is = length us\<rbrakk> \<Longrightarrow> xs[i := u] ! x = xs ! x
[PROOF STEP]
by (metis list_update_beyond nth_list_update_neq)


[STATEMENT]
lemma list_of_eucl_coord_update:
  assumes [simp]: "length xs = DIM('a::executable_euclidean_space)"
  assumes [simp]: "distinct xs"
  assumes [simp]: "i \<in> Basis"
  assumes [simp]: "\<And>n. n \<in> set xs \<Longrightarrow> n < length vs"
  shows "list_updates xs (list_of_eucl (x + (p - x \<bullet> i) *\<^sub>R i::'a)) vs =
   (list_updates xs (list_of_eucl x) vs)[xs ! index Basis_list i := p]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_updates xs (list_of_eucl (x + (p - x \<bullet> i) *\<^sub>R i)) vs = (list_updates xs (list_of_eucl x) vs)[xs ! index Basis_list i := p]
[PROOF STEP]
apply (auto intro!: nth_equalityI simp: list_updates_nth nth_list_update)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (x + (p - x \<bullet> i) *\<^sub>R i) \<bullet> Basis_list ! index xs (xs ! index Basis_list i) = p
 2. \<And>ia. \<lbrakk>ia \<in> set xs; xs ! index Basis_list i \<noteq> ia\<rbrakk> \<Longrightarrow> (x + (p - x \<bullet> i) *\<^sub>R i) \<bullet> Basis_list ! index xs ia = x \<bullet> Basis_list ! index xs ia
[PROOF STEP]
apply (simp add: algebra_simps inner_Basis index_nth_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>ia \<in> set xs; xs ! index Basis_list i \<noteq> ia\<rbrakk> \<Longrightarrow> (x + (p - x \<bullet> i) *\<^sub>R i) \<bullet> Basis_list ! index xs ia = x \<bullet> Basis_list ! index xs ia
[PROOF STEP]
apply (auto simp add: algebra_simps inner_Basis index_nth_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_updates_list_of_eucl_of_env[simp]:
  assumes [simp]: "length xs = DIM('a::executable_euclidean_space)" "distinct xs"
  shows "list_updates xs (list_of_eucl (eucl_of_env xs vs::'a)) vs = vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_updates xs (list_of_eucl (eucl_of_env xs vs)) vs = vs
[PROOF STEP]
by (auto intro!: nth_equalityI simp: list_updates_nth nth_list_update eucl_of_env_def)


[STATEMENT]
lemma nth_nth_eucl_of_env_inner:
  "b \<in> Basis \<Longrightarrow> length is = DIM('a) \<Longrightarrow> vs ! (is ! index Basis_list b) = eucl_of_env is vs \<bullet> b"
  for b::"'a::executable_euclidean_space"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<in> Basis; length is = DIM('a)\<rbrakk> \<Longrightarrow> vs ! (is ! index Basis_list b) = eucl_of_env is vs \<bullet> b
[PROOF STEP]
by (auto simp: eucl_of_env_def eucl_of_list_inner)


[STATEMENT]
lemma list_updates_idem[simp]:
  assumes "(\<And>i. i \<in> set X0 \<Longrightarrow> i < length vs)"
  shows "(list_updates X0 (map ((!) vs) X0) vs) = vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_updates X0 (map ((!) vs) X0) vs = vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i \<in> set X0 \<Longrightarrow> ?i < length vs

goal (1 subgoal):
 1. list_updates X0 (map ((!) vs) X0) vs = vs
[PROOF STEP]
by (induction X0) auto


[STATEMENT]
lemma pairwise_orthogonal_Basis[intro, simp]: "pairwise orthogonal Basis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairwise orthogonal Basis
[PROOF STEP]
by (auto simp: pairwise_alt orthogonal_def inner_Basis)


[STATEMENT]
lemma freshs_floatarith[simp]:
  assumes "freshs_floatarith fa ds" "length ds = length xs"
  shows "interpret_floatarith fa (list_updates ds xs vs) = interpret_floatarith fa vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith fa (list_updates ds xs vs) = interpret_floatarith fa vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
freshs_floatarith fa ds
length ds = length xs

goal (1 subgoal):
 1. interpret_floatarith fa (list_updates ds xs vs) = interpret_floatarith fa vs
[PROOF STEP]
by (induction fa) (auto simp: list_updates_nth_notmem)


[STATEMENT]
lemma freshs_floatarith_max_Var_floatarithI:
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> max_Var_floatarith f \<le> x"
  shows "freshs_floatarith f xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freshs_floatarith f xs
[PROOF STEP]
using assms Suc_n_not_le_n
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> max_Var_floatarith f \<le> ?x
\<not> Suc ?n \<le> ?n

goal (1 subgoal):
 1. freshs_floatarith f xs
[PROOF STEP]
by (induction f; force)


[STATEMENT]
lemma freshs_floatariths_max_Var_floatarithsI:
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> max_Var_floatariths f \<le> x"
  shows "freshs_floatariths f xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freshs_floatariths f xs
[PROOF STEP]
using assms le_trans max_Var_floatarith_le_max_Var_floatariths
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> max_Var_floatariths f \<le> ?x
\<lbrakk>?i \<le> ?j; ?j \<le> ?k\<rbrakk> \<Longrightarrow> ?i \<le> ?k
?fa \<in> set ?fas \<Longrightarrow> max_Var_floatarith ?fa \<le> max_Var_floatariths ?fas

goal (1 subgoal):
 1. freshs_floatariths f xs
[PROOF STEP]
by (force simp: freshs_floatariths_def intro!: freshs_floatarith_max_Var_floatarithI)


[STATEMENT]
lemma freshs_floatariths_freshs_floatarithI:
  assumes "\<And>fa. fa \<in> set fas \<Longrightarrow> freshs_floatarith fa xs"
  shows "freshs_floatariths fas xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freshs_floatariths fas xs
[PROOF STEP]
by (auto simp: freshs_floatariths_def assms)


[STATEMENT]
lemma fresh_floatariths_fresh_floatarithI:
  assumes "freshs_floatariths fas xs"
  assumes "fa \<in> set fas"
  shows "freshs_floatarith fa xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freshs_floatarith fa xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
freshs_floatariths fas xs
fa \<in> set fas

goal (1 subgoal):
 1. freshs_floatarith fa xs
[PROOF STEP]
by (auto simp: freshs_floatariths_def)


[STATEMENT]
lemma fresh_floatariths_fresh_floatarith[simp]:
  "fresh_floatariths (fas) i \<Longrightarrow> fa \<in> set fas \<Longrightarrow> fresh_floatarith fa i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fresh_floatariths fas i; fa \<in> set fas\<rbrakk> \<Longrightarrow> fresh_floatarith fa i
[PROOF STEP]
by (induction fas) auto


[STATEMENT]
lemma interpret_floatariths_fresh_cong:
  assumes "\<And>i. \<not>fresh_floatariths f i \<Longrightarrow> xs ! i = ys ! i"
  shows "interpret_floatariths f ys = interpret_floatariths f xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatariths f ys = interpret_floatariths f xs
[PROOF STEP]
by (auto intro!: nth_equalityI assms interpret_floatarith_fresh_cong simp: )


[STATEMENT]
lemma subterms_self[simp]: "fa2 \<in> subterms fa2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fa2 \<in> subterms fa2
[PROOF STEP]
by (induction fa2) auto