[STATEMENT]
lemma eventually_isFDERIV:
  assumes iD: "isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x@params)"
  assumes m: "max_Var_floatariths fas \<le> DIM('a::executable_euclidean_space) + length params"
  shows "\<forall>\<^sub>F (x::'a) in at x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x @ params)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x @ params)
[PROOF STEP]
by (auto simp: isFDERIV_def all_nat_less_eq eventually_ball_finite_distrib isFDERIV_lengthD[OF iD]
      intro!: interpret_floatarith_eventually_isDERIV[OF isFDERIV_uptD[OF iD], rule_format]
        max_Var_floatarith_le_max_Var_floatariths[THEN order_trans] m)


[STATEMENT]
lemma isFDERIV_eventually_isFDERIV:
  assumes iD: "isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x@params)"
  assumes m: "max_Var_floatariths fas \<le> DIM('a::executable_euclidean_space) + length params"
    shows "\<forall>\<^sub>F (x::'a) in at x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x @ params)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x. isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x @ params)
[PROOF STEP]
by (rule eventually_isFDERIV) (use assms in \<open>auto simp: isFDERIV_def\<close>)


[STATEMENT]
lemma interpret_floatarith_FDERIV_floatariths_eucl_of_env:
  assumes iD: "isFDERIV DIM('a) xs fas vs"
  assumes fresh: "freshs_floatariths (fas) ds"
  assumes [simp]: "length ds = DIM ('a)"
    "\<And>i. i \<in> set xs \<Longrightarrow> i < length vs" "distinct xs"
    "\<And>i. i \<in> set ds \<Longrightarrow> i < length vs" "distinct ds"
  shows "((\<lambda>x::'a::executable_euclidean_space.
    eucl_of_list
      (interpret_floatariths fas (list_updates xs (list_of_eucl x) vs))::'a) has_derivative
        (\<lambda>d. eucl_of_list (interpret_floatariths
         (FDERIV_floatariths fas xs (map Var ds))
         (list_updates ds (list_of_eucl d) vs)))) (at (eucl_of_env xs vs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. einterpret fas (list_updates xs (list_of_eucl x) vs)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas xs (map Var ds)) (list_updates ds (list_of_eucl d) vs))) (at (eucl_of_env xs vs))
[PROOF STEP]
by (subst has_derivative_componentwise_within)
    (auto simp add: eucl_of_list_inner isFDERIV_lengthD[OF iD]
      intro!: interpret_floatarith_FDERIV_floatarith_eucl_of_env iD[THEN isFDERIV_isDERIV_D]
        fresh_floatariths_fresh_floatarithI fresh)


[STATEMENT]
lemma interpret_floatarith_FDERIV_floatariths_append:
  assumes iD: "isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x @ ramsch)"
  assumes m: "max_Var_floatariths fas \<le> DIM('a) + length ramsch"
  assumes [simp]: "length fas = DIM('a)"
  shows "((\<lambda>x::'a::executable_euclidean_space.
    eucl_of_list
      (interpret_floatariths fas (list_of_eucl x@ramsch))::'a) has_derivative
        (\<lambda>d. eucl_of_list (interpret_floatariths
         (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a)+length ramsch..<2*DIM('a) + length ramsch]))
         (list_of_eucl x @ ramsch @ list_of_eucl d)))) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. einterpret fas (list_of_eucl x @ ramsch)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a) + length ramsch..<2 * DIM('a) + length ramsch])) (list_of_eucl x @ ramsch @ list_of_eucl d))) (at x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. einterpret fas (list_of_eucl x @ ramsch)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a) + length ramsch..<2 * DIM('a) + length ramsch])) (list_of_eucl x @ ramsch @ list_of_eucl d))) (at x)
[PROOF STEP]
have m_nth: "ia < max_Var_floatariths fas \<Longrightarrow> ia < DIM('a) + length ramsch" for ia
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia < max_Var_floatariths fas \<Longrightarrow> ia < DIM('a) + length ramsch
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
max_Var_floatariths fas \<le> DIM('a) + length ramsch

goal (1 subgoal):
 1. ia < max_Var_floatariths fas \<Longrightarrow> ia < DIM('a) + length ramsch
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?ia < max_Var_floatariths fas \<Longrightarrow> ?ia < DIM('a) + length ramsch

goal (1 subgoal):
 1. ((\<lambda>x. einterpret fas (list_of_eucl x @ ramsch)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a) + length ramsch..<2 * DIM('a) + length ramsch])) (list_of_eucl x @ ramsch @ list_of_eucl d))) (at x)
[PROOF STEP]
have m_nth': "ia < max_Var_floatarith (fas ! j) \<Longrightarrow> ia < DIM('a) + length ramsch" if "j < DIM('a)" for j ia
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia < max_Var_floatarith (fas ! j) \<Longrightarrow> ia < DIM('a) + length ramsch
[PROOF STEP]
using m_nth max_Var_floatariths_lessI that
[PROOF STATE]
proof (prove)
using this:
?ia < max_Var_floatariths fas \<Longrightarrow> ?ia < DIM('a) + length ramsch
\<lbrakk>?i < max_Var_floatarith (?fas ! ?j); ?j < length ?fas\<rbrakk> \<Longrightarrow> ?i < max_Var_floatariths ?fas
j < DIM('a)

goal (1 subgoal):
 1. ia < max_Var_floatarith (fas ! j) \<Longrightarrow> ia < DIM('a) + length ramsch
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j < DIM('a); ?ia < max_Var_floatarith (fas ! ?j)\<rbrakk> \<Longrightarrow> ?ia < DIM('a) + length ramsch

goal (1 subgoal):
 1. ((\<lambda>x. einterpret fas (list_of_eucl x @ ramsch)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a) + length ramsch..<2 * DIM('a) + length ramsch])) (list_of_eucl x @ ramsch @ list_of_eucl d))) (at x)
[PROOF STEP]
have "((\<lambda>xa::'a. eucl_of_list
         (interpret_floatariths fas
           (list_updates [0..<DIM('a)] (list_of_eucl xa)
             (list_of_eucl x @ ramsch @ replicate DIM('a) 0)))::'a) has_derivative
 (\<lambda>d. eucl_of_list
        (interpret_floatariths
          (FDERIV_floatariths fas [0..<DIM('a)] (map Var [length ramsch + DIM('a)..<length ramsch + 2 * DIM('a)]))
          (list_updates [length ramsch + DIM('a)..<length ramsch + 2 * DIM('a)] (list_of_eucl d)
            (list_of_eucl x @ ramsch @ replicate DIM('a) 0)))))
 (at (eucl_of_env [0..<DIM('a)] (list_of_eucl x @ ramsch @ replicate DIM('a) 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>xa. einterpret fas (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ ramsch @ replicate DIM('a) 0))) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [length ramsch + DIM('a)..<length ramsch + 2 * DIM('a)])) (list_updates [length ramsch + DIM('a)..<length ramsch + 2 * DIM('a)] (list_of_eucl d) (list_of_eucl x @ ramsch @ replicate DIM('a) 0)))) (at (eucl_of_env [0..<DIM('a)] (list_of_eucl x @ ramsch @ replicate DIM('a) 0)))
[PROOF STEP]
by (rule interpret_floatarith_FDERIV_floatariths_eucl_of_env[of
          "[0..<DIM('a)]" fas "list_of_eucl x@ramsch@replicate DIM('a) 0" "[length ramsch+DIM('a)..<length ramsch+2*DIM('a)]"])
       (auto intro!: iD[THEN isFDERIV_uptD] freshs_floatarith_max_Var_floatarithI isFDERIV_max_Var_congI[OF iD]
        max_Var_floatarith_le_max_Var_floatariths[THEN order_trans] m[THEN order_trans]
        freshs_floatariths_max_Var_floatarithsI simp: nth_append m add.commute less_diff_conv2 m_nth)
[PROOF STATE]
proof (state)
this:
((\<lambda>xa. einterpret fas (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ ramsch @ replicate DIM('a) 0))) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [length ramsch + DIM('a)..<length ramsch + 2 * DIM('a)])) (list_updates [length ramsch + DIM('a)..<length ramsch + 2 * DIM('a)] (list_of_eucl d) (list_of_eucl x @ ramsch @ replicate DIM('a) 0)))) (at (eucl_of_env [0..<DIM('a)] (list_of_eucl x @ ramsch @ replicate DIM('a) 0)))

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

goal (1 subgoal):
 1. ((\<lambda>x. einterpret fas (list_of_eucl x @ ramsch)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a) + length ramsch..<2 * DIM('a) + length ramsch])) (list_of_eucl x @ ramsch @ list_of_eucl d))) (at x)
[PROOF STEP]
have "interpret_floatariths fas (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ ramsch @ replicate DIM('a) 0)) =
    interpret_floatariths fas (list_of_eucl xa @ ramsch)" for xa::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatariths fas (list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ ramsch @ replicate DIM('a) 0)) = interpret_floatariths fas (list_of_eucl xa @ ramsch)
[PROOF STEP]
apply (auto intro!: nth_equalityI interpret_floatarith_max_Var_cong simp: )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>i < DIM('a); ia < max_Var_floatarith (fas ! i)\<rbrakk> \<Longrightarrow> (list_of_eucl xa @ ramsch) ! ia = list_updates [0..<DIM('a)] (list_of_eucl xa) (list_of_eucl x @ ramsch @ replicate DIM('a) 0) ! ia
[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_floatariths fas (list_updates [0..<DIM('a)] (list_of_eucl ?xa) (list_of_eucl x @ ramsch @ replicate DIM('a) 0)) = interpret_floatariths fas (list_of_eucl ?xa @ ramsch)

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

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

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

goal (1 subgoal):
 1. ((\<lambda>x. einterpret fas (list_of_eucl x @ ramsch)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a) + length ramsch..<2 * DIM('a) + length ramsch])) (list_of_eucl x @ ramsch @ list_of_eucl d))) (at x)
[PROOF STEP]
have "(eucl_of_env [0..<DIM('a)] (list_of_eucl x @ ramsch @ replicate DIM('a) 0)) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eucl_of_env [0..<DIM('a)] (list_of_eucl x @ ramsch @ 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 @ ramsch @ replicate DIM('a) 0) = x

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

goal (1 subgoal):
 1. ((\<lambda>x. einterpret fas (list_of_eucl x @ ramsch)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a) + length ramsch..<2 * DIM('a) + length ramsch])) (list_of_eucl x @ ramsch @ list_of_eucl d))) (at x)
[PROOF STEP]
by (simp add: add.commute)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. einterpret fas (list_of_eucl x @ ramsch)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a) + length ramsch..<2 * DIM('a) + length ramsch])) (list_of_eucl x @ ramsch @ list_of_eucl d))) (at x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma continuous_on_min[continuous_intros]:
  fixes f g :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. min (f x) (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>continuous_on A f; continuous_on A g\<rbrakk> \<Longrightarrow> continuous_on A (\<lambda>x. min (f x) (g x))
[PROOF STEP]
by (auto simp: continuous_on_def intro!: tendsto_min)


[STATEMENT]
lemma continuous_on_if_const[continuous_intros]:
  "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. if p then f x else g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. if p then f x else g x)
[PROOF STEP]
by (cases p) auto


[STATEMENT]
lemma continuous_on_floatarith:
  assumes "continuous_on_floatarith fa" "length xs = DIM('a)" "distinct xs"
  shows "continuous_on UNIV (\<lambda>x. interpret_floatarith fa (list_updates xs (list_of_eucl (x::'a::executable_euclidean_space)) vs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. interpret_floatarith fa (list_updates xs (list_of_eucl x) vs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on_floatarith fa
length xs = DIM('a)
distinct xs

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. interpret_floatarith fa (list_updates xs (list_of_eucl x) vs))
[PROOF STEP]
by (induction fa)
    (auto intro!: continuous_intros split: if_splits simp: list_updates_nth list_of_eucl_nth_if)


[STATEMENT]
lemma open_form:
  assumes "open_form f" "length xs = DIM('a::executable_euclidean_space)" "distinct xs"
  shows "open (Collect (\<lambda>x::'a. interpret_form f (list_updates xs (list_of_eucl x) vs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open {x. interpret_form f (list_updates xs (list_of_eucl x) vs)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
open_form f
length xs = DIM('a)
distinct xs

goal (1 subgoal):
 1. open {x. interpret_form f (list_updates xs (list_of_eucl x) vs)}
[PROOF STEP]
by (induction f) (auto intro!: open_Collect_less continuous_on_floatarith open_Collect_conj open_Collect_disj)


[STATEMENT]
lemma one_add_square_eq_0: "1 + (x)\<^sup>2 \<noteq> (0::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + x\<^sup>2 \<noteq> 0
[PROOF STEP]
by (sos "((R<1 + (([~1] * A=0) + (R<1 * (R<1 * [x]^2)))))")


[STATEMENT]
lemma isDERIV_fold_const_fa[intro]:
  assumes "isDERIV x fa vs"
  shows "isDERIV x (fold_const_fa fa) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x (fold_const_fa fa) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isDERIV x fa vs

goal (1 subgoal):
 1. isDERIV x (fold_const_fa fa) vs
[PROOF STEP]
apply (induction fa)
[PROOF STATE]
proof (prove)
goal (18 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Add fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Add fa1 fa2)) vs
 2. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Minus fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Minus fa)) vs
 3. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Mult fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Mult fa1 fa2)) vs
 4. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Inverse fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Inverse fa)) vs
 5. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Cos fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Cos fa)) vs
 6. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Arctan fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Arctan fa)) vs
 7. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Abs fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Abs fa)) vs
 8. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Max fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Max fa1 fa2)) vs
 9. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Min fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Min fa1 fa2)) vs
 10. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
A total of 18 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa1_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa1_) vs; isDERIV x fa2_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa2_) vs; isDERIV x (Add fa1_ fa2_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Add fa1_ fa2_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits option.splits)
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Minus fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Minus fa)) vs
 2. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Mult fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Mult fa1 fa2)) vs
 3. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Inverse fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Inverse fa)) vs
 4. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Cos fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Cos fa)) vs
 5. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Arctan fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Arctan fa)) vs
 6. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Abs fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Abs fa)) vs
 7. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Max fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Max fa1 fa2)) vs
 8. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Min fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Min fa1 fa2)) vs
 9. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
 10. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Sqrt fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa)) vs
A total of 17 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa_) vs; isDERIV x (Minus fa_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Minus fa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Mult fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Mult fa1 fa2)) vs
 2. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Inverse fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Inverse fa)) vs
 3. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Cos fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Cos fa)) vs
 4. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Arctan fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Arctan fa)) vs
 5. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Abs fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Abs fa)) vs
 6. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Max fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Max fa1 fa2)) vs
 7. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Min fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Min fa1 fa2)) vs
 8. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
 9. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Sqrt fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa)) vs
 10. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Exp fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa)) vs
A total of 16 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa1_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa1_) vs; isDERIV x fa2_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa2_) vs; isDERIV x (Mult fa1_ fa2_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Mult fa1_ fa2_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits option.splits)
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Inverse fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Inverse fa)) vs
 2. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Cos fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Cos fa)) vs
 3. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Arctan fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Arctan fa)) vs
 4. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Abs fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Abs fa)) vs
 5. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Max fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Max fa1 fa2)) vs
 6. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Min fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Min fa1 fa2)) vs
 7. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
 8. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Sqrt fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa)) vs
 9. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Exp fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa)) vs
 10. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Powr fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1 fa2)) vs
A total of 15 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa_) vs; isDERIV x (Inverse fa_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Inverse fa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Cos fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Cos fa)) vs
 2. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Arctan fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Arctan fa)) vs
 3. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Abs fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Abs fa)) vs
 4. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Max fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Max fa1 fa2)) vs
 5. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Min fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Min fa1 fa2)) vs
 6. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
 7. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Sqrt fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa)) vs
 8. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Exp fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa)) vs
 9. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Powr fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1 fa2)) vs
 10. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Ln fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa)) vs
A total of 14 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa_) vs; isDERIV x (Cos fa_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Cos fa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Arctan fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Arctan fa)) vs
 2. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Abs fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Abs fa)) vs
 3. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Max fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Max fa1 fa2)) vs
 4. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Min fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Min fa1 fa2)) vs
 5. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
 6. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Sqrt fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa)) vs
 7. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Exp fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa)) vs
 8. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Powr fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1 fa2)) vs
 9. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Ln fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa)) vs
 10. \<And>fa x2a. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e x2a) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e x2a)) vs
A total of 13 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa_) vs; isDERIV x (Arctan fa_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Arctan fa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Abs fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Abs fa)) vs
 2. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Max fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Max fa1 fa2)) vs
 3. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Min fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Min fa1 fa2)) vs
 4. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
 5. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Sqrt fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa)) vs
 6. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Exp fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa)) vs
 7. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Powr fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1 fa2)) vs
 8. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Ln fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa)) vs
 9. \<And>fa x2a. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e x2a) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e x2a)) vs
 10. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Floor fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa)) vs
A total of 12 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa_) vs; isDERIV x (Abs fa_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Abs fa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Max fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Max fa1 fa2)) vs
 2. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Min fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Min fa1 fa2)) vs
 3. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
 4. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Sqrt fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa)) vs
 5. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Exp fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa)) vs
 6. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Powr fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1 fa2)) vs
 7. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Ln fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa)) vs
 8. \<And>fa x2a. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e x2a) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e x2a)) vs
 9. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Floor fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa)) vs
 10. \<And>xa. isDERIV x (Var xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa)) vs
A total of 11 subgoals...
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa1_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa1_) vs; isDERIV x fa2_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa2_) vs; isDERIV x (Max fa1_ fa2_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Max fa1_ fa2_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Min fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Min fa1 fa2)) vs
 2. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
 3. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Sqrt fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa)) vs
 4. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Exp fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa)) vs
 5. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Powr fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1 fa2)) vs
 6. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Ln fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa)) vs
 7. \<And>fa x2a. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e x2a) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e x2a)) vs
 8. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Floor fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa)) vs
 9. \<And>xa. isDERIV x (Var xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa)) vs
 10. \<And>xa. isDERIV x (Num xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa)) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa1_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa1_) vs; isDERIV x fa2_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa2_) vs; isDERIV x (Min fa1_ fa2_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Min fa1_ fa2_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
 2. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Sqrt fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa)) vs
 3. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Exp fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa)) vs
 4. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Powr fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1 fa2)) vs
 5. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Ln fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa)) vs
 6. \<And>fa x2a. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e x2a) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e x2a)) vs
 7. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Floor fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa)) vs
 8. \<And>xa. isDERIV x (Var xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa)) vs
 9. \<And>xa. isDERIV x (Num xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa)) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x Pi vs \<Longrightarrow> isDERIV x (fold_const_fa Pi) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Sqrt fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa)) vs
 2. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Exp fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa)) vs
 3. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Powr fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1 fa2)) vs
 4. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Ln fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa)) vs
 5. \<And>fa x2a. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e x2a) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e x2a)) vs
 6. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Floor fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa)) vs
 7. \<And>xa. isDERIV x (Var xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa)) vs
 8. \<And>xa. isDERIV x (Num xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa)) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa_) vs; isDERIV x (Sqrt fa_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Sqrt fa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Exp fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa)) vs
 2. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Powr fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1 fa2)) vs
 3. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Ln fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa)) vs
 4. \<And>fa x2a. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e x2a) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e x2a)) vs
 5. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Floor fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa)) vs
 6. \<And>xa. isDERIV x (Var xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa)) vs
 7. \<And>xa. isDERIV x (Num xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa)) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa_) vs; isDERIV x (Exp fa_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Exp fa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>fa1 fa2. \<lbrakk>isDERIV x fa1 vs \<Longrightarrow> isDERIV x (fold_const_fa fa1) vs; isDERIV x fa2 vs \<Longrightarrow> isDERIV x (fold_const_fa fa2) vs; isDERIV x (Powr fa1 fa2) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1 fa2)) vs
 2. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Ln fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa)) vs
 3. \<And>fa x2a. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e x2a) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e x2a)) vs
 4. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Floor fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa)) vs
 5. \<And>xa. isDERIV x (Var xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa)) vs
 6. \<And>xa. isDERIV x (Num xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa)) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa1_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa1_) vs; isDERIV x fa2_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa2_) vs; isDERIV x (Powr fa1_ fa2_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Powr fa1_ fa2_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Ln fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa)) vs
 2. \<And>fa x2a. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e x2a) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e x2a)) vs
 3. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Floor fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa)) vs
 4. \<And>xa. isDERIV x (Var xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa)) vs
 5. \<And>xa. isDERIV x (Num xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa)) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa_) vs; isDERIV x (Ln fa_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Ln fa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>fa x2a. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e x2a) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e x2a)) vs
 2. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Floor fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa)) vs
 3. \<And>xa. isDERIV x (Var xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa)) vs
 4. \<And>xa. isDERIV x (Num xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa)) vs
[PROOF STEP]
subgoal for fa n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (fa ^\<^sub>e n) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e n)) vs
[PROOF STEP]
by (cases n) (auto simp: fold_const_fa.simps split: floatarith.splits nat.splits)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>fa. \<lbrakk>isDERIV x fa vs \<Longrightarrow> isDERIV x (fold_const_fa fa) vs; isDERIV x (Floor fa) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa)) vs
 2. \<And>xa. isDERIV x (Var xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa)) vs
 3. \<And>xa. isDERIV x (Num xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa)) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isDERIV x fa_ vs \<Longrightarrow> isDERIV x (fold_const_fa fa_) vs; isDERIV x (Floor fa_) vs\<rbrakk> \<Longrightarrow> isDERIV x (fold_const_fa (Floor fa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits) (subst (asm) fold_const_fa[symmetric], force)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. isDERIV x (Var xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa)) vs
 2. \<And>xa. isDERIV x (Num xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa)) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x (Var xa_) vs \<Longrightarrow> isDERIV x (fold_const_fa (Var xa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. isDERIV x (Num xa) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa)) vs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x (Num xa_) vs \<Longrightarrow> isDERIV x (fold_const_fa (Num xa_)) vs
[PROOF STEP]
by (auto simp: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma isDERIV_fold_const_fa_minus[intro!]:
  assumes "isDERIV x (fold_const_fa fa) vs"
  shows "isDERIV x (fold_const_fa (Minus fa)) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x (fold_const_fa (Minus fa)) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isDERIV x (fold_const_fa fa) vs

goal (1 subgoal):
 1. isDERIV x (fold_const_fa (Minus fa)) vs
[PROOF STEP]
by (induction fa) (auto simp: fold_const_fa.simps split: floatarith.splits)


[STATEMENT]
lemma isDERIV_fold_const_fa_plus[intro!]:
  assumes "isDERIV x (fold_const_fa fa) vs"
  assumes "isDERIV x (fold_const_fa fb) vs"
  shows "isDERIV x (fold_const_fa (Add fa fb)) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x (fold_const_fa (Add fa fb)) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isDERIV x (fold_const_fa fa) vs
isDERIV x (fold_const_fa fb) vs

goal (1 subgoal):
 1. isDERIV x (fold_const_fa (Add fa fb)) vs
[PROOF STEP]
by (induction fa)
    (auto simp: fold_const_fa.simps
      split: floatarith.splits option.splits)


[STATEMENT]
lemma isDERIV_fold_const_fa_mult[intro!]:
  assumes "isDERIV x (fold_const_fa fa) vs"
  assumes "isDERIV x (fold_const_fa fb) vs"
  shows "isDERIV x (fold_const_fa (Mult fa fb)) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x (fold_const_fa (Mult fa fb)) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isDERIV x (fold_const_fa fa) vs
isDERIV x (fold_const_fa fb) vs

goal (1 subgoal):
 1. isDERIV x (fold_const_fa (Mult fa fb)) vs
[PROOF STEP]
by (induction fa)
    (auto simp: fold_const_fa.simps
      split: floatarith.splits option.splits)


[STATEMENT]
lemma isDERIV_fold_const_fa_power[intro!]:
  assumes "isDERIV x (fold_const_fa fa) vs"
  shows "isDERIV x (fold_const_fa (fa ^\<^sub>e n)) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x (fold_const_fa (fa ^\<^sub>e n)) vs
[PROOF STEP]
apply (cases n, simp add: fold_const_fa.simps split: floatarith.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e n)) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isDERIV x (fold_const_fa fa) vs

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> isDERIV x (fold_const_fa (fa ^\<^sub>e n)) vs
[PROOF STEP]
by (induction fa)
    (auto simp: fold_const_fa.simps split: floatarith.splits option.splits)


[STATEMENT]
lemma isDERIV_fold_const_fa_inverse[intro!]:
  assumes "isDERIV x (fold_const_fa fa) vs"
  assumes "interpret_floatarith fa vs \<noteq> 0"
  shows "isDERIV x (fold_const_fa (Inverse fa)) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV x (fold_const_fa (Inverse fa)) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isDERIV x (fold_const_fa fa) vs
interpret_floatarith fa vs \<noteq> 0

goal (1 subgoal):
 1. isDERIV x (fold_const_fa (Inverse fa)) vs
[PROOF STEP]
by (simp add: fold_const_fa.simps)


[STATEMENT]
lemma add_square_ne_zero[simp]: "(y::'a::linordered_idom) > 0 \<Longrightarrow> y + x\<^sup>2 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < y \<Longrightarrow> y + x\<^sup>2 \<noteq> (0::'a)
[PROOF STEP]
by auto (metis less_add_same_cancel2 power2_less_0)