[STATEMENT]
lemma extendf_deriv_continuous:
  fixes f'::"('sf + 'sz,'sz) trm" and I::"('sf,'sc,'sz) interp"
  assumes free:"dfree f'"
  assumes good_interp:"is_interp I"
  shows "continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i f' \<nu> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i f' \<nu> x))
[PROOF STEP]
proof (induction rule: dfree.induct[OF free])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>args ia. \<lbrakk>\<And>i. dfree (args i); \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ia) \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i ($f ia args) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
case (3 args f)
[PROOF STATE]
proof (state)
this:
dfree (args ?i7)
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ?i7) \<nu> x))

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

goal (5 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>args ia. \<lbrakk>\<And>i. dfree (args i); \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ia) \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i ($f ia args) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
assume const:"\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x))"
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ?j7) \<nu> x))

goal (5 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>args ia. \<lbrakk>\<And>i. dfree (args i); \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ia) \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i ($f ia args) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ?j7) \<nu> x))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ?j7) \<nu> x))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i ($f f args) \<nu> x))
[PROOF STEP]
unfolding extendf_deriv.simps
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ?j7) \<nu> x))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (case f of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff))
[PROOF STEP]
apply(cases f)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (case f of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff))
 2. \<And>b. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inr b\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (case f of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff))
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (case f of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
have boundedF:"\<And>x. bounded_linear (((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y))
                          (\<chi> i. dterm_sem (extendf I x) (args i) \<nu>) ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. bounded_linear ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>))
[PROOF STEP]
using blinfun.bounded_linear_right
[PROOF STATE]
proof (prove)
using this:
bounded_linear (blinfun_apply ?a)

goal (1 subgoal):
 1. \<And>x. bounded_linear ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>))
[PROOF STEP]
using good_interp
[PROOF STATE]
proof (prove)
using this:
bounded_linear (blinfun_apply ?a)
is_interp I

goal (1 subgoal):
 1. \<And>x. bounded_linear ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>))
[PROOF STEP]
unfolding is_interp_def
[PROOF STATE]
proof (prove)
using this:
bounded_linear (blinfun_apply ?a)
\<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 ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounded_linear ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I ?x7) (args i) \<nu>))

goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
have boundedG:"\<And>x. bounded_linear (\<lambda> b. (\<chi> ia. extendf_deriv I i (args ia) \<nu> x b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)
[PROOF STEP]
by (simp add: bounded_linear_vec dfrees extendf_deriv_bounded good_interp)
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> ?x7 b)

goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
have boundedH:"\<And>x. bounded_linear (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y))
                          (\<chi> i. dterm_sem
                          (extendf I x)

                                 (args i) \<nu>)
                          (\<chi> ia. extendf_deriv I i (args ia) \<nu> x b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. bounded_linear (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
[PROOF STEP]
using bounded_linear_compose  boundedG boundedF
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bounded_linear ?f; bounded_linear ?g\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>x. ?f (?g x))
bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> ?x7 b)
bounded_linear ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I ?x7) (args i) \<nu>))

goal (1 subgoal):
 1. \<And>x. bounded_linear (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I ?x7) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> ?x7 b))

goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
have eq:"(\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y))
                          (\<chi> i. dterm_sem
                                 (extendf I x)
                                 (args i) \<nu>)
                          (\<chi> ia. extendf_deriv I i (args ia) \<nu> x b)))
                          =
                (\<lambda>x. blinfun_compose(Blinfun((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y))
                          (\<chi> i. dterm_sem
                                 (extendf I x)
                                 (args i) \<nu>) )) (Blinfun(\<lambda> b. (\<chi> ia. extendf_deriv I i (args ia) \<nu> x b))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) = (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) = Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x ia. blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia
[PROOF STEP]
subgoal for x ia
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia
[PROOF STEP]
using boundedG[of x]  blinfun_apply_blinfun_compose bounded_linear_Blinfun_apply
[PROOF STATE]
proof (prove)
using this:
bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)
blinfun_apply (?a o\<^sub>L ?b) ?c = blinfun_apply ?a (blinfun_apply ?b ?c)
bounded_linear ?f \<Longrightarrow> blinfun_apply (Blinfun ?f) = ?f

goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b); \<And>a b c. blinfun_apply (a o\<^sub>L b) c = blinfun_apply a (blinfun_apply b c); \<And>f. bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f\<rbrakk> \<Longrightarrow> blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia
[PROOF STEP]
have f1: "bounded_linear (\<lambda>v. FunctionFrechet I a (\<chi> s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi> s. extendf_deriv I i (args s) \<nu> x v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))
[PROOF STEP]
using FunctionFrechet.simps \<open>bounded_linear (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi> i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi> ia. extendf_deriv I i (args ia) \<nu> x b))\<close>
[PROOF STATE]
proof (prove)
using this:
FunctionFrechet ?I ?i = (THE f'. \<forall>x. (Functions ?I ?i has_derivative f' x) (at x))
bounded_linear (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))

goal (1 subgoal):
 1. bounded_linear (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))

goal (1 subgoal):
 1. \<lbrakk>bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b); \<And>a b c. blinfun_apply (a o\<^sub>L b) c = blinfun_apply a (blinfun_apply b c); \<And>f. bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f\<rbrakk> \<Longrightarrow> blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia
[PROOF STEP]
have "bounded_linear (FunctionFrechet I a (\<chi> s. dterm_sem (extendf I x) (args s) \<nu>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))
[PROOF STEP]
using good_interp is_interp_def
[PROOF STATE]
proof (prove)
using this:
is_interp I
is_interp ?I \<equiv> \<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. bounded_linear (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bounded_linear (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))

goal (1 subgoal):
 1. \<lbrakk>bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b); \<And>a b c. blinfun_apply (a o\<^sub>L b) c = blinfun_apply a (blinfun_apply b c); \<And>f. bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f\<rbrakk> \<Longrightarrow> blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bounded_linear (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))
[PROOF STEP]
have "blinfun_apply (Blinfun (FunctionFrechet I a (\<chi> s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi> s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi> s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi> s. extendf_deriv I i (args s) \<nu> x v))) ia"
[PROOF STATE]
proof (prove)
using this:
bounded_linear (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))

goal (1 subgoal):
 1. blinfun_apply (Blinfun (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi>s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))) ia
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
bounded_linear (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))
bounded_linear (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))

goal (1 subgoal):
 1. blinfun_apply (Blinfun (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi>s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))) ia
[PROOF STEP]
by (simp add: bounded_linear_Blinfun_apply)
[PROOF STATE]
proof (state)
this:
blinfun_apply (Blinfun (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi>s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))) ia

goal (1 subgoal):
 1. \<lbrakk>bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b); \<And>a b c. blinfun_apply (a o\<^sub>L b) c = blinfun_apply a (blinfun_apply b c); \<And>f. bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f\<rbrakk> \<Longrightarrow> blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
blinfun_apply (Blinfun (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi>s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))) ia
[PROOF STEP]
have "blinfun_apply (Blinfun (FunctionFrechet I a (\<chi> s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi> s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi> s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi> s. extendf_deriv I i (args s) \<nu> x v))) ia \<and> bounded_linear (\<lambda>v. \<chi> s. extendf_deriv I i (args s) \<nu> x v)"
[PROOF STATE]
proof (prove)
using this:
blinfun_apply (Blinfun (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi>s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))) ia

goal (1 subgoal):
 1. blinfun_apply (Blinfun (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi>s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))) ia \<and> bounded_linear (\<lambda>v. \<chi>s. extendf_deriv I i (args s) \<nu> x v)
[PROOF STEP]
by (metis \<open>bounded_linear (\<lambda>b. \<chi> ia. extendf_deriv I i (args ia) \<nu> x b)\<close>)
[PROOF STATE]
proof (state)
this:
blinfun_apply (Blinfun (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi>s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))) ia \<and> bounded_linear (\<lambda>v. \<chi>s. extendf_deriv I i (args s) \<nu> x v)

goal (1 subgoal):
 1. \<lbrakk>bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b); \<And>a b c. blinfun_apply (a o\<^sub>L b) c = blinfun_apply a (blinfun_apply b c); \<And>f. bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f\<rbrakk> \<Longrightarrow> blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia
[PROOF STEP]
(* failed *)
[PROOF STATE]
proof (state)
this:
blinfun_apply (Blinfun (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi>s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))) ia \<and> bounded_linear (\<lambda>v. \<chi>s. extendf_deriv I i (args s) \<nu> x v)

goal (1 subgoal):
 1. \<lbrakk>bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b); \<And>a b c. blinfun_apply (a o\<^sub>L b) c = blinfun_apply a (blinfun_apply b c); \<And>f. bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f\<rbrakk> \<Longrightarrow> blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
blinfun_apply (Blinfun (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi>s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))) ia \<and> bounded_linear (\<lambda>v. \<chi>s. extendf_deriv I i (args s) \<nu> x v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
blinfun_apply (Blinfun (FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>))) (\<chi>s. extendf_deriv I i (args s) \<nu> x ia) = blinfun_apply (Blinfun (\<lambda>v. FunctionFrechet I a (\<chi>s. dterm_sem (extendf I x) (args s) \<nu>) (\<chi>s. extendf_deriv I i (args s) \<nu> x v))) ia \<and> bounded_linear (\<lambda>v. \<chi>s. extendf_deriv I i (args s) \<nu> x v)

goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia
[PROOF STEP]
by (simp add: bounded_linear_Blinfun_apply)
[PROOF STATE]
proof (state)
this:
blinfun_apply (Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) ia = blinfun_apply (Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) = (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))

goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
have bounds:"\<And>ia x. bounded_linear (extendf_deriv I i (args ia) \<nu> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia x. bounded_linear (extendf_deriv I i (args ia) \<nu> x)
[PROOF STEP]
by (simp add: dfrees extendf_deriv_bounded good_interp)
[PROOF STATE]
proof (state)
this:
bounded_linear (extendf_deriv I i (args ?ia7) \<nu> ?x7)

goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
have vec_bound:"\<And>x. bounded_linear (\<lambda>b. \<chi> ia. extendf_deriv I i (args ia) \<nu> x b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)
[PROOF STEP]
by (simp add: boundedG)
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> ?x7 b)

goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
have blinfun_vec:"(\<lambda>x. Blinfun (\<lambda>b. \<chi> ia. extendf_deriv I i (args ia) \<nu> x b)) = (\<lambda>x. blinfun_vec (\<lambda> ia.  Blinfun(\<lambda>b. extendf_deriv I i (args ia) \<nu> x b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) = (\<lambda>x. blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x)))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b) = blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x))
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x ia. blinfun_apply (Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia = blinfun_apply (blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x))) ia
[PROOF STEP]
apply(rule vec_extensionality)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x ia iaa. blinfun_apply (Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) ia $ iaa = blinfun_apply (blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x))) ia $ iaa
[PROOF STEP]
subgoal for x y ia
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) y $ ia = blinfun_apply (blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x))) y $ ia
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) y $ ia = blinfun_apply (blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x))) y $ ia
[PROOF STEP]
have "(\<chi> s. extendf_deriv I i (args s) \<nu> x y) $ ia = blinfun_apply (blinfun_vec (\<lambda>s. Blinfun (extendf_deriv I i (args s) \<nu> x))) y $ ia"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>s. extendf_deriv I i (args s) \<nu> x y) $ ia = blinfun_apply (blinfun_vec (\<lambda>s. Blinfun (extendf_deriv I i (args s) \<nu> x))) y $ ia
[PROOF STEP]
by (simp add: bounded_linear_Blinfun_apply bounds)
[PROOF STATE]
proof (state)
this:
(\<chi>s. extendf_deriv I i (args s) \<nu> x y) $ ia = blinfun_apply (blinfun_vec (\<lambda>s. Blinfun (extendf_deriv I i (args s) \<nu> x))) y $ ia

goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) y $ ia = blinfun_apply (blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x))) y $ ia
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<chi>s. extendf_deriv I i (args s) \<nu> x y) $ ia = blinfun_apply (blinfun_vec (\<lambda>s. Blinfun (extendf_deriv I i (args s) \<nu> x))) y $ ia
[PROOF STEP]
have "(\<chi> s. extendf_deriv I i (args s) \<nu> x y) $ ia = blinfun_apply (blinfun_vec (\<lambda>s. Blinfun (extendf_deriv I i (args s) \<nu> x))) y $ ia \<and> bounded_linear (\<lambda>v. \<chi> s. extendf_deriv I i (args s) \<nu> x v)"
[PROOF STATE]
proof (prove)
using this:
(\<chi>s. extendf_deriv I i (args s) \<nu> x y) $ ia = blinfun_apply (blinfun_vec (\<lambda>s. Blinfun (extendf_deriv I i (args s) \<nu> x))) y $ ia

goal (1 subgoal):
 1. (\<chi>s. extendf_deriv I i (args s) \<nu> x y) $ ia = blinfun_apply (blinfun_vec (\<lambda>s. Blinfun (extendf_deriv I i (args s) \<nu> x))) y $ ia \<and> bounded_linear (\<lambda>v. \<chi>s. extendf_deriv I i (args s) \<nu> x v)
[PROOF STEP]
by (metis \<open>bounded_linear (\<lambda>b. \<chi> ia. extendf_deriv I i (args ia) \<nu> x b)\<close>)
[PROOF STATE]
proof (state)
this:
(\<chi>s. extendf_deriv I i (args s) \<nu> x y) $ ia = blinfun_apply (blinfun_vec (\<lambda>s. Blinfun (extendf_deriv I i (args s) \<nu> x))) y $ ia \<and> bounded_linear (\<lambda>v. \<chi>s. extendf_deriv I i (args s) \<nu> x v)

goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) y $ ia = blinfun_apply (blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x))) y $ ia
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<chi>s. extendf_deriv I i (args s) \<nu> x y) $ ia = blinfun_apply (blinfun_vec (\<lambda>s. Blinfun (extendf_deriv I i (args s) \<nu> x))) y $ ia \<and> bounded_linear (\<lambda>v. \<chi>s. extendf_deriv I i (args s) \<nu> x v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<chi>s. extendf_deriv I i (args s) \<nu> x y) $ ia = blinfun_apply (blinfun_vec (\<lambda>s. Blinfun (extendf_deriv I i (args s) \<nu> x))) y $ ia \<and> bounded_linear (\<lambda>v. \<chi>s. extendf_deriv I i (args s) \<nu> x v)

goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) y $ ia = blinfun_apply (blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x))) y $ ia
[PROOF STEP]
by (simp add: bounded_linear_Blinfun_apply)
[PROOF STATE]
proof (state)
this:
blinfun_apply (Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) y $ ia = blinfun_apply (blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x))) y $ ia

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>x. Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) = (\<lambda>x. blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x)))

goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
have vec_cont:"continuous_on UNIV (\<lambda>x. blinfun_vec (\<lambda> ia.  Blinfun(\<lambda>b. extendf_deriv I i (args ia) \<nu> x b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x)))
[PROOF STEP]
apply(rule continuous_blinfun_vec')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ia) \<nu> x))
[PROOF STEP]
using "3.IH"
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ?i7) \<nu> x))

goal (1 subgoal):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args ia) \<nu> x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x)))

goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
have cont_intro:"\<And> f g s. continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x  o\<^sub>L  g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f g s. \<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. f x o\<^sub>L g x)
[PROOF STEP]
by(auto intro: continuous_intros)
[PROOF STATE]
proof (state)
this:
\<lbrakk>continuous_on ?s7 ?f7; continuous_on ?s7 ?g7\<rbrakk> \<Longrightarrow> continuous_on ?s7 (\<lambda>x. ?f7 x o\<^sub>L ?g7 x)

goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
have cont:"continuous_on UNIV (\<lambda>x. blinfun_compose(Blinfun((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y))
                          (\<chi> i. dterm_sem
                                 \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I,
                                    Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
                                 (args i) \<nu>) )) (Blinfun(\<lambda> b. (\<chi> ia. extendf_deriv I i (args ia) \<nu> x b))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
[PROOF STEP]
apply(rule cont_intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)))
 2. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
 2. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
[PROOF STEP]
using blinfun_vec vec_cont
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)) = (\<lambda>x. blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x)))
continuous_on UNIV (\<lambda>x. blinfun_vec (\<lambda>ia. Blinfun (extendf_deriv I i (args ia) \<nu> x)))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)))
[PROOF STEP]
apply(rule continuous_on_compose2[of UNIV "(\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) x))"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) x))
 2. continuous_on UNIV (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
 3. range (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<subseteq> UNIV
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) x))
[PROOF STEP]
using good_interp
[PROOF STATE]
proof (prove)
using this:
is_interp I

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) 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. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
 2. range (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<subseteq> UNIV
[PROOF STEP]
apply(rule continuous_on_vec_lambda)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
 2. range (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<subseteq> UNIV
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
[PROOF STEP]
using extendf_dterm_sem_continuous[OF dfrees[of i] good_interp]
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) (args i) ?\<nu>)

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<subseteq> UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))

goal (1 subgoal):
 1. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
[PROOF STEP]
show " continuous_on UNIV
       (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y))
                          (\<chi> i. dterm_sem
                                 \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I,
                                    Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
                                 (args i) \<nu>)
                          (\<chi> ia. extendf_deriv I i (args ia) \<nu> x b)))"
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
(\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) = (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem (extendf I x) (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b)); (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))) = (\<lambda>x. Blinfun ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)) o\<^sub>L Blinfun (\<lambda>b. \<chi>ia. extendf_deriv I i (args ia) \<nu> x b))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<And>j. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (args j) \<nu> x)); f = Inr b\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (case f of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i ($f f args) \<nu> x))

goal (4 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
case (4 \<theta>\<^sub>1 \<theta>\<^sub>2)
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>1
dfree \<theta>\<^sub>2
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))

goal (4 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
assume free1:"dfree \<theta>\<^sub>1"
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>1

goal (4 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
assume free2:"dfree \<theta>\<^sub>2"
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>2

goal (4 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
assume IH1:"continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))"
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))

goal (4 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
assume IH2:"continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))"
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))

goal (4 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
have bound:"\<And>x. bounded_linear  (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. bounded_linear (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)
[PROOF STEP]
using extendf_deriv_bounded[OF free1 good_interp] extendf_deriv_bounded[OF free2 good_interp]
[PROOF STATE]
proof (prove)
using this:
bounded_linear (extendf_deriv I ?i \<theta>\<^sub>1 ?\<nu> ?x)
bounded_linear (extendf_deriv I ?i \<theta>\<^sub>2 ?\<nu> ?x)

goal (1 subgoal):
 1. \<And>x. bounded_linear (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)
[PROOF STEP]
by (simp add: bounded_linear_add)
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> ?x7 a + extendf_deriv I i \<theta>\<^sub>2 \<nu> ?x7 a)

goal (4 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
have eq:"(\<lambda>x. Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)) = (\<lambda>x. Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a) + Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>2 \<nu> x a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)) = (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a) = Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x ia. blinfun_apply (Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)) ia = blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)) ia
[PROOF STEP]
subgoal for x j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)) j = blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)) j
[PROOF STEP]
using bound[of x] extendf_deriv_bounded[OF free1 good_interp]
      extendf_deriv_bounded[OF free2 good_interp]
      blinfun.add_left[of "Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)" "Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)"]
      bounded_linear_Blinfun_apply[of "(extendf_deriv I i \<theta>\<^sub>1 \<nu> x)"]
      bounded_linear_Blinfun_apply[of "(extendf_deriv I i \<theta>\<^sub>2 \<nu> x)"]
[PROOF STATE]
proof (prove)
using this:
bounded_linear (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)
bounded_linear (extendf_deriv I ?i \<theta>\<^sub>1 ?\<nu> ?x)
bounded_linear (extendf_deriv I ?i \<theta>\<^sub>2 ?\<nu> ?x)
blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)) ?b = blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)) ?b + blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)) ?b
bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) \<Longrightarrow> blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)) = extendf_deriv I i \<theta>\<^sub>1 \<nu> x
bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) \<Longrightarrow> blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)) = extendf_deriv I i \<theta>\<^sub>2 \<nu> x

goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)) j = blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)) j
[PROOF STEP]
by (simp add: bounded_linear_Blinfun_apply)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>x. Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)) = (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))

goal (4 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
have "continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a) + Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>2 \<nu> x a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))
[PROOF STEP]
apply(rule continuous_intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
 2. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))
[PROOF STEP]
using IH1 IH2
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))

goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
 2. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))

goal (4 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)) \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a))
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a)) = (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x) + Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)) \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a + extendf_deriv I i \<theta>\<^sub>2 \<nu> x a))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))

goal (3 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
case (5 \<theta>\<^sub>1 \<theta>\<^sub>2)
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>1
dfree \<theta>\<^sub>2
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))

goal (3 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
assume free1:"dfree \<theta>\<^sub>1"
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>1

goal (3 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
assume free2:"dfree \<theta>\<^sub>2"
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>2

goal (3 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
assume IH1:"continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))"
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))

goal (3 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
assume IH2:"continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))"
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))

goal (3 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
have bounded:"\<And>x. bounded_linear (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a +
                       extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. bounded_linear (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)
[PROOF STEP]
using extendf_deriv_bounded[OF free1 good_interp] extendf_deriv_bounded[OF free2 good_interp]
[PROOF STATE]
proof (prove)
using this:
bounded_linear (extendf_deriv I ?i \<theta>\<^sub>1 ?\<nu> ?x)
bounded_linear (extendf_deriv I ?i \<theta>\<^sub>2 ?\<nu> ?x)

goal (1 subgoal):
 1. \<And>x. bounded_linear (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)
[PROOF STEP]
by (simp add: bounded_linear_add bounded_linear_const_mult bounded_linear_mult_const)
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>a. dterm_sem (extendf I ?x7) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> ?x7 a + extendf_deriv I i \<theta>\<^sub>1 \<nu> ?x7 a * dterm_sem (extendf I ?x7) \<theta>\<^sub>2 \<nu>)

goal (3 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
have eq:"(\<lambda>x. Blinfun (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a +
                       extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)) =
           (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>2 \<nu> x a) +
           dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. Blinfun (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)) = (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Blinfun (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>) = dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x ia. blinfun_apply (Blinfun (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)) ia = blinfun_apply (dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)) ia
[PROOF STEP]
subgoal for x j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)) j = blinfun_apply (dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)) j
[PROOF STEP]
using extendf_deriv_bounded[OF free1 good_interp] extendf_deriv_bounded[OF free2 good_interp] bounded[of x]
      blinfun.scaleR_left
      bounded_linear_Blinfun_apply[of "Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)"]
      bounded_linear_Blinfun_apply[of "Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)"]
      mult.commute
      plus_blinfun.rep_eq[of "dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)" "dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)"]
      real_scaleR_def
[PROOF STATE]
proof (prove)
using this:
bounded_linear (extendf_deriv I ?i \<theta>\<^sub>1 ?\<nu> ?x)
bounded_linear (extendf_deriv I ?i \<theta>\<^sub>2 ?\<nu> ?x)
bounded_linear (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)
blinfun_apply (?r *\<^sub>R ?a) ?b = ?r *\<^sub>R blinfun_apply ?a ?b
bounded_linear (blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))) \<Longrightarrow> blinfun_apply (Blinfun (blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)))) = blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))
bounded_linear (blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))) \<Longrightarrow> blinfun_apply (Blinfun (blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)))) = blinfun_apply (Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
?a * ?b = ?b * ?a
blinfun_apply (dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)) = (\<lambda>xa. blinfun_apply (dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)) xa + blinfun_apply (dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)) xa)
?a *\<^sub>R ?x = ?a * ?x

goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)) j = blinfun_apply (dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)) j
[PROOF STEP]
by (simp add: blinfun.scaleR_left bounded_linear_Blinfun_apply)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>x. Blinfun (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)) = (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))

goal (3 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
have "continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>2 \<nu> x a) +
           dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (\<lambda>a. extendf_deriv I i \<theta>\<^sub>1 \<nu> x a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
[PROOF STEP]
apply(rule continuous_intros)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu>)
 2. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))
 3. continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
[PROOF STEP]
apply(rule extendf_dterm_sem_continuous[OF free1 good_interp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))
 2. continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
[PROOF STEP]
apply(rule IH2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
[PROOF STEP]
apply(rule continuous_intros)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)
 2. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
[PROOF STEP]
apply(rule extendf_dterm_sem_continuous[OF free2 good_interp])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
[PROOF STEP]
by(rule IH1)
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))

goal (3 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)); dfree \<theta>\<^sub>2; continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x))\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))
[PROOF STEP]
unfolding extendf_deriv.simps
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>))
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))
(\<lambda>x. Blinfun (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>)) = (\<lambda>x. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>2 \<nu> x) + dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu> *\<^sub>R Blinfun (extendf_deriv I i \<theta>\<^sub>1 \<nu> x))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>a. dterm_sem (extendf I x) \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem (extendf I x) \<theta>\<^sub>2 \<nu>))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x))

goal (2 subgoals):
 1. \<And>ia. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Var ia) \<nu> x))
 2. \<And>r. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i (Const r) \<nu> x))
[PROOF STEP]
qed (auto intro: continuous_intros)