[STATEMENT]
lemma interpret_floatarith_FDERIV_floatarith_append:
  assumes iD: "\<And>i j. i < DIM('a) \<Longrightarrow> isDERIV i (fa) (list_of_eucl x @ params)"
  assumes m: "max_Var_floatarith fa \<le> DIM('a) + length params"
  shows "((\<lambda>x::'a::executable_euclidean_space.
      interpret_floatarith fa (list_of_eucl x @ params)) has_derivative
        (\<lambda>d. interpret_floatarith
         (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2*DIM('a)]))
         (list_of_eucl x @ params @ list_of_eucl d))) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
have m_nth: "ia < max_Var_floatarith fa \<Longrightarrow> ia < DIM('a) + length params" for ia
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia < max_Var_floatarith fa \<Longrightarrow> ia < DIM('a) + length params
[PROOF STEP]
using less_le_trans m
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z
max_Var_floatarith fa \<le> DIM('a) + length params

goal (1 subgoal):
 1. ia < max_Var_floatarith fa \<Longrightarrow> ia < DIM('a) + length params
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?ia < max_Var_floatarith fa \<Longrightarrow> ?ia < DIM('a) + length params

goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
have "((\<lambda>xa::'a. interpret_floatarith fa
           (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ params @ replicate DIM('a) 0))) has_derivative
   (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)]))
          (list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl d)
            (list_of_eucl x @ params @ replicate DIM('a) 0))))
   (at (eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>xa. interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ params @ replicate DIM('a) 0))) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl d) (list_of_eucl x @ params @ replicate DIM('a) 0)))) (at (eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0)))
[PROOF STEP]
by (rule interpret_floatarith_FDERIV_floatarith_eucl_of_env)
      (auto intro!: iD freshs_floatarith_max_Var_floatarithI isDERIV_max_Var_floatarithI[OF iD]
        max_Var_floatarith_le_max_Var_floatariths[THEN order_trans] m[THEN order_trans]
        simp: nth_append add.commute less_diff_conv2 m_nth)
[PROOF STATE]
proof (state)
this:
((\<lambda>xa. interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ params @ replicate DIM('a) 0))) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl d) (list_of_eucl x @ params @ replicate DIM('a) 0)))) (at (eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0)))

goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((\<lambda>xa. interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ params @ replicate DIM('a) 0))) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl d) (list_of_eucl x @ params @ replicate DIM('a) 0)))) (at (eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0)))

goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
have "interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ params @ replicate DIM('a) 0)) =
    interpret_floatarith fa (list_of_eucl xa @ params)" for xa::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ params @ replicate DIM('a) 0)) = interpret_floatarith fa (list_of_eucl xa @ params)
[PROOF STEP]
apply (auto intro!: nth_equalityI interpret_floatarith_max_Var_cong simp: )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < max_Var_floatarith fa \<Longrightarrow> (list_of_eucl xa @ params) ! i = list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ params @ replicate DIM('a) 0) ! i
[PROOF STEP]
apply (auto simp: list_updates_nth nth_append dest: m_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl ?xa) (list_of_eucl x @ params @ replicate DIM('a) 0)) = interpret_floatarith fa (list_of_eucl ?xa @ params)

goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl ?xa) (list_of_eucl x @ params @ replicate DIM('a) 0)) = interpret_floatarith fa (list_of_eucl ?xa @ params)

goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
have "(list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl d) (list_of_eucl x @ params @ replicate DIM('a) 0)) =
    (list_of_eucl x @ params @ list_of_eucl d)" for d::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl d) (list_of_eucl x @ params @ replicate DIM('a) 0) = list_of_eucl x @ params @ list_of_eucl d
[PROOF STEP]
by (auto simp: intro!: nth_equalityI simp: list_updates_nth nth_append add.commute)
[PROOF STATE]
proof (state)
this:
list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl ?d) (list_of_eucl x @ params @ replicate DIM('a) 0) = list_of_eucl x @ params @ list_of_eucl ?d

goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl ?d) (list_of_eucl x @ params @ replicate DIM('a) 0) = list_of_eucl x @ params @ list_of_eucl ?d

goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
have "(eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0)) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0) = x
[PROOF STEP]
by (auto intro!: euclidean_eqI[where 'a='a] simp: eucl_of_env_def eucl_of_list_inner nth_append)
[PROOF STATE]
proof (state)
this:
eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0) = x

goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>xa. interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ params @ replicate DIM('a) 0))) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl d) (list_of_eucl x @ params @ replicate DIM('a) 0)))) (at (eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0)))
interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl ?xa) (list_of_eucl x @ params @ replicate DIM('a) 0)) = interpret_floatarith fa (list_of_eucl ?xa @ params)
list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl ?d) (list_of_eucl x @ params @ replicate DIM('a) 0) = list_of_eucl x @ params @ list_of_eucl ?d
eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0) = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>xa. interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ params @ replicate DIM('a) 0))) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl d) (list_of_eucl x @ params @ replicate DIM('a) 0)))) (at (eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0)))
interpret_floatarith fa (list_updates [0..<DIM('a)] (list_of_eucl ?xa) (list_of_eucl x @ params @ replicate DIM('a) 0)) = interpret_floatarith fa (list_of_eucl ?xa @ params)
list_updates [length params + DIM('a)..<length params + 2 * DIM('a)] (list_of_eucl ?d) (list_of_eucl x @ params @ replicate DIM('a) 0) = list_of_eucl x @ params @ list_of_eucl ?d
eucl_of_env [0..<DIM('a)] (list_of_eucl x @ params @ replicate DIM('a) 0) = x

goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>x. interpret_floatarith fa (list_of_eucl x @ params)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [length params + DIM('a)..<length params + 2 * DIM('a)])) (list_of_eucl x @ params @ list_of_eucl d))) (at x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interpret_floatarith_FDERIV_floatarith:
  assumes iD: "\<And>i j. i < DIM('a) \<Longrightarrow> isDERIV i (fa) (list_of_eucl x)"
  assumes m: "max_Var_floatarith fa \<le> DIM('a)"
  shows "((\<lambda>x::'a::executable_euclidean_space.
      interpret_floatarith fa (list_of_eucl x)) has_derivative
        (\<lambda>d. interpret_floatarith
         (FDERIV_floatarith fa [0..<DIM('a)] (map Var [DIM('a)..<2*DIM('a)]))
         (list_of_eucl x @ list_of_eucl d))) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)])) (list_of_eucl x @ list_of_eucl d))) (at x)
[PROOF STEP]
using interpret_floatarith_FDERIV_floatarith_append[where params=Nil,simplified, OF assms]
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i < DIM('a) \<Longrightarrow> i < DIM('a)) \<Longrightarrow> ((\<lambda>x. interpret_floatarith fa (list_of_eucl x)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)])) (list_of_eucl x @ list_of_eucl d))) (at x)

goal (1 subgoal):
 1. ((\<lambda>x. interpret_floatarith fa (list_of_eucl x)) has_derivative (\<lambda>d. interpret_floatarith (FDERIV_floatarith fa [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)])) (list_of_eucl x @ list_of_eucl d))) (at x)
[PROOF STEP]
by simp