[STATEMENT]
lemma func_lemma2:"(\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and>
          continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x))) \<Longrightarrow>
    (\<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)) \<Longrightarrow>
    ((\<lambda>v. Functions I f (vec_lambda(\<lambda>i. sterm_sem I (args i) v))) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi> i. sterm_sem I (args i) \<nu>) (\<chi> i. frechet I (args i) \<nu> v'))) (at \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x)); \<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x)); \<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)
[PROOF STEP]
assume a1: "\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and>
          continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x))"
[PROOF STATE]
proof (state)
this:
\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x))

goal (1 subgoal):
 1. \<lbrakk>\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x)); \<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x))
[PROOF STEP]
have a1':"\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x))

goal (1 subgoal):
 1. \<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x)); \<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)
[PROOF STEP]
assume a2: "\<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)"
[PROOF STATE]
proof (state)
this:
?\<theta>5 \<in> range args \<Longrightarrow> (sterm_sem I ?\<theta>5 has_derivative frechet I ?\<theta>5 \<nu>) (at \<nu>)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x)); \<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)
[PROOF STEP]
have "\<forall>f fa v. (\<exists>fb. \<not> (f (fb::'a) has_derivative fa fb (v::(real, 'a) vec)) (at v)) \<or> ((\<lambda>v. (\<chi> fa. (f fa v::real))) has_derivative (\<lambda>va. (\<chi> f. fa f v va))) (at v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f fa v. (\<exists>fb. \<not> (f fb has_derivative fa fb v) (at v)) \<or> ((\<lambda>v. \<chi>fa. f fa v) has_derivative (\<lambda>va. \<chi>f. fa f v va)) (at v)
[PROOF STEP]
using has_derivative_vec
[PROOF STATE]
proof (prove)
using this:
(\<And>i. (?f i has_derivative ?f' i) ?F) \<Longrightarrow> ((\<lambda>x. \<chi>i. ?f i x) has_derivative (\<lambda>h. \<chi>i. ?f' i h)) ?F

goal (1 subgoal):
 1. \<forall>f fa v. (\<exists>fb. \<not> (f fb has_derivative fa fb v) (at v)) \<or> ((\<lambda>v. \<chi>fa. f fa v) has_derivative (\<lambda>va. \<chi>f. fa f v va)) (at v)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>f fa v. (\<exists>fb. \<not> (f fb has_derivative fa fb v) (at v)) \<or> ((\<lambda>v. \<chi>fa. f fa v) has_derivative (\<lambda>va. \<chi>f. fa f v va)) (at v)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x)); \<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>f fa v. (\<exists>fb. \<not> (f fb has_derivative fa fb v) (at v)) \<or> ((\<lambda>v. \<chi>fa. f fa v) has_derivative (\<lambda>va. \<chi>f. fa f v va)) (at v)
[PROOF STEP]
have "((\<lambda>v. \<chi> f. sterm_sem I (args f) v) has_derivative (\<lambda>v. \<chi> f. frechet I (args f) \<nu> v)) (at \<nu>)"
[PROOF STATE]
proof (prove)
using this:
\<forall>f fa v. (\<exists>fb. \<not> (f fb has_derivative fa fb v) (at v)) \<or> ((\<lambda>v. \<chi>fa. f fa v) has_derivative (\<lambda>va. \<chi>f. fa f v va)) (at v)

goal (1 subgoal):
 1. ((\<lambda>v. \<chi>f. sterm_sem I (args f) v) has_derivative (\<lambda>v. \<chi>f. frechet I (args f) \<nu> v)) (at \<nu>)
[PROOF STEP]
by (auto simp add: a2 has_derivative_vec)
[PROOF STATE]
proof (state)
this:
((\<lambda>v. \<chi>f. sterm_sem I (args f) v) has_derivative (\<lambda>v. \<chi>f. frechet I (args f) \<nu> v)) (at \<nu>)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x)); \<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>v. \<chi>f. sterm_sem I (args f) v) has_derivative (\<lambda>v. \<chi>f. frechet I (args f) \<nu> v)) (at \<nu>)
[PROOF STEP]
show "((\<lambda>v. Functions I f (vec_lambda(\<lambda>f. sterm_sem I (args f) v))) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi> i. sterm_sem I (args i) \<nu>) (\<chi> i. frechet I (args i) \<nu> v'))) (at \<nu>)"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>v. \<chi>f. sterm_sem I (args f) v) has_derivative (\<lambda>v. \<chi>f. frechet I (args f) \<nu> v)) (at \<nu>)

goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>f. sterm_sem I (args f) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)
[PROOF STEP]
using a1' function_case_inner
[PROOF STATE]
proof (prove)
using this:
((\<lambda>v. \<chi>f. sterm_sem I (args f) v) has_derivative (\<lambda>v. \<chi>f. frechet I (args f) \<nu> v)) (at \<nu>)
\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x)
\<lbrakk>\<forall>x i. (Functions ?I i has_derivative FunctionFrechet ?I i x) (at x); ((\<lambda>v. \<chi>i. sterm_sem ?I (?args i) v) has_derivative (\<lambda>v. \<chi>i. frechet ?I (?args i) ?\<nu> v)) (at ?\<nu>)\<rbrakk> \<Longrightarrow> ((\<lambda>v. Functions ?I ?f (\<chi>i. sterm_sem ?I (?args i) v)) has_derivative frechet ?I ($f ?f ?args) ?\<nu>) (at ?\<nu>)

goal (1 subgoal):
 1. ((\<lambda>v. Functions I f (\<chi>f. sterm_sem I (args f) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>v. Functions I f (\<chi>f. sterm_sem I (args f) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma func_lemma:
  "is_interp I \<Longrightarrow>
  (\<And>\<theta> :: ('a::finite, 'c::finite) trm. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)) \<Longrightarrow>
  (sterm_sem I ($f f args) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_interp I; \<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I ($f f args) has_derivative frechet I ($f f args) \<nu>) (at \<nu>)
[PROOF STEP]
apply(auto simp add: sfunction_case is_interp_def function_case_inner)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x i. (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x)); \<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> ((\<lambda>v. Functions I f (\<chi>i. sterm_sem I (args i) v)) has_derivative (\<lambda>v'. (THE f'. \<forall>x. (Functions I f has_derivative f' x) (at x)) (\<chi>i. sterm_sem I (args i) \<nu>) (\<chi>i. frechet I (args i) \<nu> v'))) (at \<nu>)
[PROOF STEP]
apply(erule func_lemma2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<theta>. \<lbrakk>\<And>\<theta>. \<theta> \<in> range args \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>); \<theta> \<in> range args\<rbrakk> \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma frechet_correctness:
  fixes I :: "('a::finite, 'b::finite, 'c::finite) interp" and \<nu>
  assumes good_interp: "is_interp I"
  shows "dfree \<theta> \<Longrightarrow> FDERIV (sterm_sem I \<theta>) \<nu> :> (frechet I \<theta> \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> (sterm_sem I \<theta> has_derivative frechet I \<theta> \<nu>) (at \<nu>)
[PROOF STEP]
proof (induct rule: dfree.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. (sterm_sem I (Var i) has_derivative frechet I (Var i) \<nu>) (at \<nu>)
 2. \<And>r. (sterm_sem I (Const r) has_derivative frechet I (Const r) \<nu>) (at \<nu>)
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. (sterm_sem I (args i) has_derivative frechet I (args i) \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I ($f i args) has_derivative frechet I ($f i args) \<nu>) (at \<nu>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
[PROOF STEP]
case (dfree_Var i)
[PROOF STATE]
proof (state)
this:

goal (5 subgoals):
 1. \<And>i. (sterm_sem I (Var i) has_derivative frechet I (Var i) \<nu>) (at \<nu>)
 2. \<And>r. (sterm_sem I (Const r) has_derivative frechet I (Const r) \<nu>) (at \<nu>)
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. (sterm_sem I (args i) has_derivative frechet I (args i) \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I ($f i args) has_derivative frechet I ($f i args) \<nu>) (at \<nu>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sterm_sem I (Var i) has_derivative frechet I (Var i) \<nu>) (at \<nu>)
[PROOF STEP]
by (auto simp add: svar_case svar_deriv axis_def)
[PROOF STATE]
proof (state)
this:
(sterm_sem I (Var i) has_derivative frechet I (Var i) \<nu>) (at \<nu>)

goal (4 subgoals):
 1. \<And>r. (sterm_sem I (Const r) has_derivative frechet I (Const r) \<nu>) (at \<nu>)
 2. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. (sterm_sem I (args i) has_derivative frechet I (args i) \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I ($f i args) has_derivative frechet I ($f i args) \<nu>) (at \<nu>)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>r. (sterm_sem I (Const r) has_derivative frechet I (Const r) \<nu>) (at \<nu>)
 2. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. (sterm_sem I (args i) has_derivative frechet I (args i) \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I ($f i args) has_derivative frechet I ($f i args) \<nu>) (at \<nu>)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
[PROOF STEP]
case (dfree_Fun args i)
[PROOF STATE]
proof (state)
this:
dfree (args ?i5)
(sterm_sem I (args ?i5) has_derivative frechet I (args ?i5) \<nu>) (at \<nu>)

goal (4 subgoals):
 1. \<And>r. (sterm_sem I (Const r) has_derivative frechet I (Const r) \<nu>) (at \<nu>)
 2. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. (sterm_sem I (args i) has_derivative frechet I (args i) \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I ($f i args) has_derivative frechet I ($f i args) \<nu>) (at \<nu>)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
[PROOF STEP]
with good_interp
[PROOF STATE]
proof (chain)
picking this:
is_interp I
dfree (args ?i5)
(sterm_sem I (args ?i5) has_derivative frechet I (args ?i5) \<nu>) (at \<nu>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_interp I
dfree (args ?i5)
(sterm_sem I (args ?i5) has_derivative frechet I (args ?i5) \<nu>) (at \<nu>)

goal (1 subgoal):
 1. (sterm_sem I ($f i args) has_derivative frechet I ($f i args) \<nu>) (at \<nu>)
[PROOF STEP]
by (intro func_lemma) auto
[PROOF STATE]
proof (state)
this:
(sterm_sem I ($f i args) has_derivative frechet I ($f i args) \<nu>) (at \<nu>)

goal (3 subgoals):
 1. \<And>r. (sterm_sem I (Const r) has_derivative frechet I (Const r) \<nu>) (at \<nu>)
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; (sterm_sem I \<theta>\<^sub>1 has_derivative frechet I \<theta>\<^sub>1 \<nu>) (at \<nu>); dfree \<theta>\<^sub>2; (sterm_sem I \<theta>\<^sub>2 has_derivative frechet I \<theta>\<^sub>2 \<nu>) (at \<nu>)\<rbrakk> \<Longrightarrow> (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) has_derivative frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu>) (at \<nu>)
[PROOF STEP]
qed auto


[STATEMENT]
lemma sterm_determines_frechet:
  fixes I ::"('a1::finite, 'b1::finite, 'c::finite) interp"
    and J ::"('a2::finite, 'b2::finite, 'c::finite) interp"
    and \<theta>1 :: "('a1::finite, 'c::finite) trm"
    and \<theta>2 :: "('a2::finite, 'c::finite) trm"
    and \<nu>
  assumes good_interp1:"is_interp I"
  assumes good_interp2:"is_interp J"
  assumes free1:"dfree \<theta>1"
  assumes free2:"dfree \<theta>2"
  assumes sem:"sterm_sem I \<theta>1 = sterm_sem J \<theta>2"
  shows "frechet I \<theta>1 (fst \<nu>) (snd \<nu>) = frechet J \<theta>2 (fst \<nu>) (snd \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet I \<theta>1 (fst \<nu>) (snd \<nu>) = frechet J \<theta>2 (fst \<nu>) (snd \<nu>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. frechet I \<theta>1 (fst \<nu>) (snd \<nu>) = frechet J \<theta>2 (fst \<nu>) (snd \<nu>)
[PROOF STEP]
have d1:"(sterm_sem I \<theta>1 has_derivative (frechet I \<theta>1 (fst \<nu>))) (at (fst \<nu>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sterm_sem I \<theta>1 has_derivative frechet I \<theta>1 (fst \<nu>)) (at (fst \<nu>))
[PROOF STEP]
using frechet_correctness[OF good_interp1 free1]
[PROOF STATE]
proof (prove)
using this:
(sterm_sem I \<theta>1 has_derivative frechet I \<theta>1 ?\<nu>) (at ?\<nu>)

goal (1 subgoal):
 1. (sterm_sem I \<theta>1 has_derivative frechet I \<theta>1 (fst \<nu>)) (at (fst \<nu>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(sterm_sem I \<theta>1 has_derivative frechet I \<theta>1 (fst \<nu>)) (at (fst \<nu>))

goal (1 subgoal):
 1. frechet I \<theta>1 (fst \<nu>) (snd \<nu>) = frechet J \<theta>2 (fst \<nu>) (snd \<nu>)
[PROOF STEP]
have d2:"(sterm_sem J \<theta>2 has_derivative (frechet J \<theta>2 (fst \<nu>))) (at (fst \<nu>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sterm_sem J \<theta>2 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))
[PROOF STEP]
using frechet_correctness[OF good_interp2 free2]
[PROOF STATE]
proof (prove)
using this:
(sterm_sem J \<theta>2 has_derivative frechet J \<theta>2 ?\<nu>) (at ?\<nu>)

goal (1 subgoal):
 1. (sterm_sem J \<theta>2 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(sterm_sem J \<theta>2 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))

goal (1 subgoal):
 1. frechet I \<theta>1 (fst \<nu>) (snd \<nu>) = frechet J \<theta>2 (fst \<nu>) (snd \<nu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(sterm_sem J \<theta>2 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))
[PROOF STEP]
have d1':"(sterm_sem I \<theta>1 has_derivative (frechet J \<theta>2 (fst \<nu>))) (at (fst \<nu>))"
[PROOF STATE]
proof (prove)
using this:
(sterm_sem J \<theta>2 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))

goal (1 subgoal):
 1. (sterm_sem I \<theta>1 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))
[PROOF STEP]
using sem
[PROOF STATE]
proof (prove)
using this:
(sterm_sem J \<theta>2 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))
sterm_sem I \<theta>1 = sterm_sem J \<theta>2

goal (1 subgoal):
 1. (sterm_sem I \<theta>1 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(sterm_sem I \<theta>1 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))

goal (1 subgoal):
 1. frechet I \<theta>1 (fst \<nu>) (snd \<nu>) = frechet J \<theta>2 (fst \<nu>) (snd \<nu>)
[PROOF STEP]
thus "?thesis"
[PROOF STATE]
proof (prove)
using this:
(sterm_sem I \<theta>1 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))

goal (1 subgoal):
 1. frechet I \<theta>1 (fst \<nu>) (snd \<nu>) = frechet J \<theta>2 (fst \<nu>) (snd \<nu>)
[PROOF STEP]
using has_derivative_unique d1 d1'
[PROOF STATE]
proof (prove)
using this:
(sterm_sem I \<theta>1 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))
\<lbrakk>(?f has_derivative ?F) (at ?x); (?f has_derivative ?F') (at ?x)\<rbrakk> \<Longrightarrow> ?F = ?F'
(sterm_sem I \<theta>1 has_derivative frechet I \<theta>1 (fst \<nu>)) (at (fst \<nu>))
(sterm_sem I \<theta>1 has_derivative frechet J \<theta>2 (fst \<nu>)) (at (fst \<nu>))

goal (1 subgoal):
 1. frechet I \<theta>1 (fst \<nu>) (snd \<nu>) = frechet J \<theta>2 (fst \<nu>) (snd \<nu>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
frechet I \<theta>1 (fst \<nu>) (snd \<nu>) = frechet J \<theta>2 (fst \<nu>) (snd \<nu>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma the_deriv:
  assumes deriv:"(f has_derivative F) (at x)"
  shows "(THE G. (f has_derivative G) (at x)) = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE G. (f has_derivative G) (at x)) = F
[PROOF STEP]
apply(rule the_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (f has_derivative F) (at x)
 2. \<And>G. (f has_derivative G) (at x) \<Longrightarrow> G = F
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_derivative F) (at x)
[PROOF STEP]
by (rule deriv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>G. (f has_derivative G) (at x) \<Longrightarrow> G = F
[PROOF STEP]
subgoal for G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_derivative G) (at x) \<Longrightarrow> G = F
[PROOF STEP]
by (auto simp add: deriv has_derivative_unique)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma the_all_deriv:
  assumes deriv:"\<forall>x. (f has_derivative F x) (at x)"
  shows "(THE G. \<forall> x. (f has_derivative G x) (at x)) = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE G. \<forall>x. (f has_derivative G x) (at x)) = F
[PROOF STEP]
apply(rule the_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x. (f has_derivative F x) (at x)
 2. \<And>G. \<forall>x. (f has_derivative G x) (at x) \<Longrightarrow> G = F
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (f has_derivative F x) (at x)
[PROOF STEP]
by (rule deriv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>G. \<forall>x. (f has_derivative G x) (at x) \<Longrightarrow> G = F
[PROOF STEP]
subgoal for G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (f has_derivative G x) (at x) \<Longrightarrow> G = F
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x. (f has_derivative G x) (at x) \<Longrightarrow> G x = F x
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (f has_derivative G x) (at x) \<Longrightarrow> G x = F x
[PROOF STEP]
apply(erule allE[where x=x])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_derivative G x) (at x) \<Longrightarrow> G x = F x
[PROOF STEP]
by (auto simp add: deriv has_derivative_unique)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma frechet_linear:
  assumes good_interp:"is_interp I"
  fixes v \<theta>
  shows " dfree \<theta> \<Longrightarrow> bounded_linear (frechet I \<theta> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> bounded_linear (frechet I \<theta> v)
[PROOF STEP]
proof(induction rule: dfree.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. bounded_linear (frechet I (Var i) v)
 2. \<And>r. bounded_linear (frechet I (Const r) v)
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. bounded_linear (frechet I (args i) v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I ($f i args) v)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
case (dfree_Var i)
[PROOF STATE]
proof (state)
this:

goal (5 subgoals):
 1. \<And>i. bounded_linear (frechet I (Var i) v)
 2. \<And>r. bounded_linear (frechet I (Const r) v)
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. bounded_linear (frechet I (args i) v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I ($f i args) v)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (frechet I (Var i) v)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
bounded_linear (frechet I (Var i) v)

goal (4 subgoals):
 1. \<And>r. bounded_linear (frechet I (Const r) v)
 2. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. bounded_linear (frechet I (args i) v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I ($f i args) v)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>r. bounded_linear (frechet I (Const r) v)
 2. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. bounded_linear (frechet I (args i) v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I ($f i args) v)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
case (dfree_Const r)
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>r. bounded_linear (frechet I (Const r) v)
 2. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. bounded_linear (frechet I (args i) v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I ($f i args) v)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (frechet I (Const r) v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounded_linear (frechet I (Const r) v)

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. bounded_linear (frechet I (args i) v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I ($f i args) v)
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. bounded_linear (frechet I (args i) v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I ($f i args) v)
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
case (dfree_Fun args i)
[PROOF STATE]
proof (state)
this:
dfree (args ?i5)
bounded_linear (frechet I (args ?i5) v)

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. bounded_linear (frechet I (args i) v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I ($f i args) v)
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
have blin1:"\<And>x. bounded_linear(FunctionFrechet I i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. bounded_linear (FunctionFrechet I i x)
[PROOF STEP]
using good_interp
[PROOF STATE]
proof (prove)
using this:
is_interp I

goal (1 subgoal):
 1. \<And>x. bounded_linear (FunctionFrechet I i x)
[PROOF STEP]
unfolding is_interp_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I i x))

goal (1 subgoal):
 1. \<And>x. bounded_linear (FunctionFrechet I i x)
[PROOF STEP]
using has_derivative_bounded_linear
[PROOF STATE]
proof (prove)
using this:
\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I i x))
(?f has_derivative ?f') ?F \<Longrightarrow> bounded_linear ?f'

goal (1 subgoal):
 1. \<And>x. bounded_linear (FunctionFrechet I i x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bounded_linear (FunctionFrechet I i ?x5)

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. bounded_linear (frechet I (args i) v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I ($f i args) v)
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
have blin2:"bounded_linear (\<lambda> a. (\<chi> i. frechet I (args i) v a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (\<lambda>a. \<chi>i. frechet I (args i) v a)
[PROOF STEP]
using dfree_Fun.IH
[PROOF STATE]
proof (prove)
using this:
bounded_linear (frechet I (args ?i5) v)

goal (1 subgoal):
 1. bounded_linear (\<lambda>a. \<chi>i. frechet I (args i) v a)
[PROOF STEP]
by(rule bounded_linear_vec)
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>a. \<chi>i. frechet I (args i) v a)

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. bounded_linear (frechet I (args i) v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I ($f i args) v)
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bounded_linear (\<lambda>a. \<chi>i. frechet I (args i) v a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bounded_linear (\<lambda>a. \<chi>i. frechet I (args i) v a)

goal (1 subgoal):
 1. bounded_linear (frechet I ($f i args) v)
[PROOF STEP]
using bounded_linear_compose[of "FunctionFrechet I i (\<chi> i. sterm_sem I (args i) v)" "(\<lambda>a. (\<chi> i. frechet I (args i) v a))", OF blin1 blin2]
[PROOF STATE]
proof (prove)
using this:
bounded_linear (\<lambda>a. \<chi>i. frechet I (args i) v a)
bounded_linear (\<lambda>x. FunctionFrechet I i (\<chi>i. sterm_sem I (args i) v) (\<chi>i. frechet I (args i) v x))

goal (1 subgoal):
 1. bounded_linear (frechet I ($f i args) v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounded_linear (frechet I ($f i args) v)

goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
case (dfree_Plus \<theta>\<^sub>1 \<theta>\<^sub>2)
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>1
dfree \<theta>\<^sub>2
bounded_linear (frechet I \<theta>\<^sub>1 v)
bounded_linear (frechet I \<theta>\<^sub>2 v)

goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfree \<theta>\<^sub>1
dfree \<theta>\<^sub>2
bounded_linear (frechet I \<theta>\<^sub>1 v)
bounded_linear (frechet I \<theta>\<^sub>2 v)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>\<^sub>1
dfree \<theta>\<^sub>2
bounded_linear (frechet I \<theta>\<^sub>1 v)
bounded_linear (frechet I \<theta>\<^sub>2 v)

goal (1 subgoal):
 1. bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>1 v); bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>a. frechet I \<theta>\<^sub>1 v a + frechet I \<theta>\<^sub>2 v a)
[PROOF STEP]
using bounded_linear_add
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bounded_linear ?f; bounded_linear ?g\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>x. ?f x + ?g x)

goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>1 v); bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>a. frechet I \<theta>\<^sub>1 v a + frechet I \<theta>\<^sub>2 v a)
[PROOF STEP]
by (blast)
[PROOF STATE]
proof (state)
this:
bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) v)

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
case (dfree_Times \<theta>\<^sub>1 \<theta>\<^sub>2)
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>1
dfree \<theta>\<^sub>2
bounded_linear (frechet I \<theta>\<^sub>1 v)
bounded_linear (frechet I \<theta>\<^sub>2 v)

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; bounded_linear (frechet I \<theta>\<^sub>1 v); dfree \<theta>\<^sub>2; bounded_linear (frechet I \<theta>\<^sub>2 v)\<rbrakk> \<Longrightarrow> bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfree \<theta>\<^sub>1
dfree \<theta>\<^sub>2
bounded_linear (frechet I \<theta>\<^sub>1 v)
bounded_linear (frechet I \<theta>\<^sub>2 v)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>\<^sub>1
dfree \<theta>\<^sub>2
bounded_linear (frechet I \<theta>\<^sub>1 v)
bounded_linear (frechet I \<theta>\<^sub>2 v)

goal (1 subgoal):
 1. bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)
[PROOF STEP]
by (auto simp add: bounded_linear_add bounded_linear_const_mult bounded_linear_mult_const)
[PROOF STATE]
proof (state)
this:
bounded_linear (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frechet_blin:"is_interp I \<Longrightarrow> dfree \<theta> \<Longrightarrow> (\<lambda>v. Blinfun (\<lambda>v'. frechet I \<theta> v v')) = blin_frechet (good_interp I) (simple_term \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_interp I; dfree \<theta>\<rbrakk> \<Longrightarrow> (\<lambda>v. Blinfun (frechet I \<theta> v)) = blin_frechet (good_interp I) (simple_term \<theta>)
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>is_interp I; dfree \<theta>\<rbrakk> \<Longrightarrow> Blinfun (frechet I \<theta> v) = blin_frechet (good_interp I) (simple_term \<theta>) v
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v i. \<lbrakk>is_interp I; dfree \<theta>\<rbrakk> \<Longrightarrow> blinfun_apply (Blinfun (frechet I \<theta> v)) i = blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>) v) i
[PROOF STEP]
by (simp add: bounded_linear_Blinfun_apply frechet_linear good_interp_inverse simple_term_inverse)


[STATEMENT]
lemma sterm_continuous:
  assumes good_interp:"is_interp I"
  shows "dfree \<theta> \<Longrightarrow> continuous_on UNIV (sterm_sem I \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> continuous_on UNIV (sterm_sem I \<theta>)
[PROOF STEP]
proof(induction rule: dfree.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (sterm_sem I (Var i))
 2. \<And>r. continuous_on UNIV (sterm_sem I (Const r))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (sterm_sem I (args i))\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I ($f i args))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
case (dfree_Fun args i)
[PROOF STATE]
proof (state)
this:
dfree (args ?i5)
continuous_on UNIV (sterm_sem I (args ?i5))

goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (sterm_sem I (Var i))
 2. \<And>r. continuous_on UNIV (sterm_sem I (Const r))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (sterm_sem I (args i))\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I ($f i args))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
assume IH:"\<And>i. continuous_on UNIV (sterm_sem I (args i))"
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (sterm_sem I (args ?i5))

goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (sterm_sem I (Var i))
 2. \<And>r. continuous_on UNIV (sterm_sem I (Const r))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (sterm_sem I (args i))\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I ($f i args))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
have con1:"continuous_on UNIV (Functions I i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (Functions I i)
[PROOF STEP]
using good_interp
[PROOF STATE]
proof (prove)
using this:
is_interp I

goal (1 subgoal):
 1. continuous_on UNIV (Functions I i)
[PROOF STEP]
unfolding is_interp_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I i x))

goal (1 subgoal):
 1. continuous_on UNIV (Functions I i)
[PROOF STEP]
using continuous_on_eq_continuous_within has_derivative_continuous
[PROOF STATE]
proof (prove)
using this:
\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I i x))
continuous_on ?s ?f = (\<forall>x\<in>?s. continuous (at x within ?s) ?f)
(?f has_derivative ?f') (at ?x within ?s) \<Longrightarrow> continuous (at ?x within ?s) ?f

goal (1 subgoal):
 1. continuous_on UNIV (Functions I i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (Functions I i)

goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (sterm_sem I (Var i))
 2. \<And>r. continuous_on UNIV (sterm_sem I (Const r))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (sterm_sem I (args i))\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I ($f i args))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
have con2:"continuous_on UNIV (\<lambda> x. (\<chi> i. sterm_sem I (args i) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. \<chi>i. sterm_sem I (args i) x)
[PROOF STEP]
apply(rule continuous_on_vec_lambda)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. continuous_on UNIV (sterm_sem I (args i))
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (sterm_sem I (args ?i5))

goal (1 subgoal):
 1. \<And>i. continuous_on UNIV (sterm_sem I (args i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. \<chi>i. sterm_sem I (args i) x)

goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (sterm_sem I (Var i))
 2. \<And>r. continuous_on UNIV (sterm_sem I (Const r))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (sterm_sem I (args i))\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I ($f i args))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
have con:"continuous_on UNIV ((Functions I i) \<circ> (\<lambda>x.  (\<chi> i. sterm_sem I (args i) x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (Functions I i \<circ> (\<lambda>x. \<chi>i. sterm_sem I (args i) x))
[PROOF STEP]
apply(rule continuous_on_compose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. \<chi>i. sterm_sem I (args i) x)
 2. continuous_on (range (\<lambda>x. \<chi>i. sterm_sem I (args i) x)) (Functions I i)
[PROOF STEP]
using con1 con2
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (Functions I i)
continuous_on UNIV (\<lambda>x. \<chi>i. sterm_sem I (args i) x)

goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. \<chi>i. sterm_sem I (args i) x)
 2. continuous_on (range (\<lambda>x. \<chi>i. sterm_sem I (args i) x)) (Functions I i)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>continuous_on UNIV (Functions I i); continuous_on UNIV (\<lambda>x. \<chi>i. sterm_sem I (args i) x)\<rbrakk> \<Longrightarrow> continuous_on (range (\<lambda>x. \<chi>i. sterm_sem I (args i) x)) (Functions I i)
[PROOF STEP]
using continuous_on_subset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_on ?s ?f; ?t \<subseteq> ?s\<rbrakk> \<Longrightarrow> continuous_on ?t ?f

goal (1 subgoal):
 1. \<lbrakk>continuous_on UNIV (Functions I i); continuous_on UNIV (\<lambda>x. \<chi>i. sterm_sem I (args i) x)\<rbrakk> \<Longrightarrow> continuous_on (range (\<lambda>x. \<chi>i. sterm_sem I (args i) x)) (Functions I i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (Functions I i \<circ> (\<lambda>x. \<chi>i. sterm_sem I (args i) x))

goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (sterm_sem I (Var i))
 2. \<And>r. continuous_on UNIV (sterm_sem I (Const r))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (sterm_sem I (args i))\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I ($f i args))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (sterm_sem I ($f i args))
[PROOF STEP]
using con comp_def
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (Functions I i \<circ> (\<lambda>x. \<chi>i. sterm_sem I (args i) x))
?f \<circ> ?g = (\<lambda>x. ?f (?g x))

goal (1 subgoal):
 1. continuous_on UNIV (sterm_sem I ($f i args))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (sterm_sem I ($f i args))

goal (4 subgoals):
 1. \<And>i. continuous_on UNIV (sterm_sem I (Var i))
 2. \<And>r. continuous_on UNIV (sterm_sem I (Const r))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (sterm_sem I \<theta>\<^sub>1); dfree \<theta>\<^sub>2; continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem I (Times \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
qed (auto intro: continuous_intros)


[STATEMENT]
lemma sterm_continuous':
  assumes good_interp:"is_interp I"
  shows "dfree \<theta> \<Longrightarrow> continuous_on S (sterm_sem I \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> continuous_on S (sterm_sem I \<theta>)
[PROOF STEP]
using sterm_continuous continuous_on_subset good_interp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_interp ?I; dfree ?\<theta>\<rbrakk> \<Longrightarrow> continuous_on UNIV (sterm_sem ?I ?\<theta>)
\<lbrakk>continuous_on ?s ?f; ?t \<subseteq> ?s\<rbrakk> \<Longrightarrow> continuous_on ?t ?f
is_interp I

goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> continuous_on S (sterm_sem I \<theta>)
[PROOF STEP]
by blast