[STATEMENT]
lemma frechet_continuous:
  fixes I :: "('sf, 'sc, 'sz) interp"
  assumes good_interp:"is_interp I"
  shows "dfree \<theta> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree \<theta> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>))
[PROOF STEP]
proof (induction rule: dfree.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Var i)))
 2. \<And>r. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
case (dfree_Var i)
[PROOF STATE]
proof (state)
this:

goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Var i)))
 2. \<And>r. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have free:"dfree (Var i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree (Var i)
[PROOF STEP]
by (rule dfree_Var)
[PROOF STATE]
proof (state)
this:
dfree (Var i)

goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Var i)))
 2. \<And>r. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have bounded_linear:"bounded_linear (\<lambda> \<nu>'. \<nu>' \<bullet> axis i 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (\<lambda>\<nu>'. \<nu>' \<bullet> axis i (1::'a))
[PROOF STEP]
by (auto simp add: bounded_linear_vec_nth)
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>\<nu>'. \<nu>' \<bullet> axis i (1::?'a7))

goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Var i)))
 2. \<And>r. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have cont:"continuous_on UNIV (\<lambda>\<nu>. Blinfun(\<lambda> \<nu>'. \<nu>' \<bullet> axis i 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>\<nu>. Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i (1::'b)))
[PROOF STEP]
using continuous_on_const
[PROOF STATE]
proof (prove)
using this:
continuous_on ?s (\<lambda>x. ?c)

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>\<nu>. Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i (1::'b)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>\<nu>. Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i (1::?'b8)))

goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Var i)))
 2. \<And>r. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have eq:"\<And>\<nu> \<nu>'. (\<lambda>\<nu>. Blinfun(\<lambda> \<nu>'. \<nu>' \<bullet> axis i 1)) \<nu> \<nu>' = (blin_frechet (good_interp I) (simple_term (Var i))) \<nu> \<nu>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> \<nu>'. blinfun_apply (Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i 1)) \<nu>' = blinfun_apply (blin_frechet (good_interp I) (simple_term (Var i)) \<nu>) \<nu>'
[PROOF STEP]
unfolding axis_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> \<nu>'. blinfun_apply (Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> (\<chi>ia. if ia = i then 1 else 0))) \<nu>' = blinfun_apply (blin_frechet (good_interp I) (simple_term (Var i)) \<nu>) \<nu>'
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> \<nu>'. blinfun_apply (Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> (\<chi>ia. if ia = i then 1 else 0))) \<nu>' = frechet (raw_interp (good_interp I)) (raw_term (simple_term (Var i))) \<nu> \<nu>'
[PROOF STEP]
by (metis (no_types) axis_def blinfun_inner_left.abs_eq blinfun_inner_left.rep_eq dfree_Var_simps frechet.simps(1) mem_Collect_eq simple_term_inverse)
[PROOF STATE]
proof (state)
this:
blinfun_apply (Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i 1)) ?\<nu>'8 = blinfun_apply (blin_frechet (good_interp I) (simple_term (Var i)) ?\<nu>8) ?\<nu>'8

goal (5 subgoals):
 1. \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Var i)))
 2. \<And>r. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
 3. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 5. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have eq':"(\<lambda>\<nu>. Blinfun(\<lambda> \<nu>'. \<nu>' \<bullet> axis i 1)) = (blin_frechet (good_interp I) (simple_term (Var i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<nu>. Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i 1)) = blin_frechet (good_interp I) (simple_term (Var i))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu>. Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i 1) = blin_frechet (good_interp I) (simple_term (Var i)) \<nu>
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> ia. blinfun_apply (Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i 1)) ia = blinfun_apply (blin_frechet (good_interp I) (simple_term (Var i)) \<nu>) ia
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
blinfun_apply (Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i 1)) ?\<nu>'8 = blinfun_apply (blin_frechet (good_interp I) (simple_term (Var i)) ?\<nu>8) ?\<nu>'8

goal (1 subgoal):
 1. \<And>\<nu> ia. blinfun_apply (Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i 1)) ia = blinfun_apply (blin_frechet (good_interp I) (simple_term (Var i)) \<nu>) ia
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>\<nu>. Blinfun (\<lambda>\<nu>'. \<nu>' \<bullet> axis i 1)) = blin_frechet (good_interp I) (simple_term (Var i))

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

goal (1 subgoal):
 1. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Var i)))
[PROOF STEP]
by (metis cont)
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Var i)))

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

goal (4 subgoals):
 1. \<And>r. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
 2. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have free:"dfree (Const r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree (Const r)
[PROOF STEP]
by (rule dfree_Const)
[PROOF STATE]
proof (state)
this:
dfree (Const r)

goal (4 subgoals):
 1. \<And>r. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
 2. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have bounded_linear:"bounded_linear (\<lambda> \<nu>'. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (\<lambda>\<nu>'. 0::'b)
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>\<nu>'. 0::?'b7)

goal (4 subgoals):
 1. \<And>r. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
 2. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have cont:"continuous_on UNIV (\<lambda>\<nu>. Blinfun(\<lambda> \<nu>'. 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>\<nu>. Blinfun (\<lambda>\<nu>'. 0::'c))
[PROOF STEP]
using continuous_on_const
[PROOF STATE]
proof (prove)
using this:
continuous_on ?s (\<lambda>x. ?c)

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>\<nu>. Blinfun (\<lambda>\<nu>'. 0::'c))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>\<nu>. Blinfun (\<lambda>\<nu>'. 0::?'c8))

goal (4 subgoals):
 1. \<And>r. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
 2. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 4. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have eq':"(\<lambda>\<nu>. Blinfun(\<lambda> \<nu>'. 0)) = (blin_frechet (good_interp I) (simple_term (Const r)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<nu>. Blinfun (\<lambda>\<nu>'. 0)) = blin_frechet (good_interp I) (simple_term (Const r))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu>. Blinfun (\<lambda>\<nu>'. 0) = blin_frechet (good_interp I) (simple_term (Const r)) \<nu>
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> i. blinfun_apply (Blinfun (\<lambda>\<nu>'. 0)) i = blinfun_apply (blin_frechet (good_interp I) (simple_term (Const r)) \<nu>) i
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu> i. blinfun_apply (Blinfun (\<lambda>\<nu>'. 0)) i = frechet (raw_interp (good_interp I)) (raw_term (simple_term (Const r))) \<nu> i
[PROOF STEP]
using zero_blinfun.abs_eq zero_blinfun.rep_eq free
[PROOF STATE]
proof (prove)
using this:
0 = Blinfun (\<lambda>x. 0::?'b)
blinfun_apply 0 = (\<lambda>x. 0::?'b)
dfree (Const r)

goal (1 subgoal):
 1. \<And>\<nu> i. blinfun_apply (Blinfun (\<lambda>\<nu>'. 0)) i = frechet (raw_interp (good_interp I)) (raw_term (simple_term (Const r))) \<nu> i
[PROOF STEP]
by (metis frechet.simps(5) mem_Collect_eq simple_term_inverse)
[PROOF STATE]
proof (state)
this:
(\<lambda>\<nu>. Blinfun (\<lambda>\<nu>'. 0)) = blin_frechet (good_interp I) (simple_term (Const r))

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

goal (1 subgoal):
 1. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))
[PROOF STEP]
by (metis cont)
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Const r)))

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

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

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
assume frees:"(\<And>i. dfree (args i))"
[PROOF STATE]
proof (state)
this:
dfree (args ?i5)

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfree (args ?i5)
[PROOF STEP]
have free:"dfree ($f f args)"
[PROOF STATE]
proof (prove)
using this:
dfree (args ?i5)

goal (1 subgoal):
 1. dfree ($f f args)
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
dfree ($f f args)

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

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

goal (1 subgoal):
 1. \<And>f. continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I f x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I ?f5 x))

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have cont1:"\<And>v. continuous_on UNIV (\<lambda>v'. (\<chi> i. frechet I (args i) v v'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. continuous_on UNIV (\<lambda>v'. \<chi>i. frechet I (args i) v v')
[PROOF STEP]
apply(rule continuous_on_vec_lambda)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v i. continuous_on UNIV (frechet I (args i) v)
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args ?i5)))

goal (1 subgoal):
 1. \<And>v i. continuous_on UNIV (frechet I (args i) v)
[PROOF STEP]
by (simp add: frechet_linear frees good_interp linear_continuous_on)
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>v'. \<chi>i. frechet I (args i) ?v5 v')

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have eq:"(\<lambda>v. Blinfun(\<lambda>v'. FunctionFrechet I f (\<chi> i. sterm_sem I (args i) v) (\<chi> i. frechet I (args i) v v')))
    = (blin_frechet (good_interp I) (simple_term (Function f args)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. Blinfun (\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v) (\<chi>i. frechet I (args i) v v'))) = blin_frechet (good_interp I) (simple_term ($f f args))
[PROOF STEP]
using frechet_blin[OF good_interp free]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>v. Blinfun (frechet I ($f f args) v)) = blin_frechet (good_interp I) (simple_term ($f f args))

goal (1 subgoal):
 1. (\<lambda>v. Blinfun (\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v) (\<chi>i. frechet I (args i) v v'))) = blin_frechet (good_interp I) (simple_term ($f f args))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>v. Blinfun (\<lambda>v'. FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v) (\<chi>i. frechet I (args i) v v'))) = blin_frechet (good_interp I) (simple_term ($f f args))

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

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

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

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
let ?blin_ff ="(\<lambda>x. Blinfun (FunctionFrechet I f x))"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have some_eq:"(\<lambda>x. Blinfun (FunctionFrechet I f (\<chi> i. sterm_sem I (args i) x))) =
                ((?blin_ff) \<circ> (\<lambda>x. (\<chi> i. sterm_sem I (args i) x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) x))) = (\<lambda>x. Blinfun (FunctionFrechet I f x)) \<circ> (\<lambda>x. \<chi>i. sterm_sem I (args i) x)
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) x)) = ((\<lambda>x. Blinfun (FunctionFrechet I f x)) \<circ> (\<lambda>x. \<chi>i. sterm_sem I (args i) x)) x
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. blinfun_apply (Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) x))) i = blinfun_apply (((\<lambda>x. Blinfun (FunctionFrechet I f x)) \<circ> (\<lambda>x. \<chi>i. sterm_sem I (args i) x)) x) i
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. blinfun_apply (Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) x))) i = blinfun_apply (Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) x))) i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) x))) = (\<lambda>x. Blinfun (FunctionFrechet I f x)) \<circ> (\<lambda>x. \<chi>i. sterm_sem I (args i) x)

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have sub_cont:"continuous_on UNIV ((?blin_ff) \<circ> (\<lambda>x. (\<chi> i. sterm_sem I (args i) x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV ((\<lambda>x. Blinfun (FunctionFrechet I f x)) \<circ> (\<lambda>x. \<chi>i. sterm_sem I (args i) x))
[PROOF STEP]
apply(rule continuous_intros)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. continuous_on UNIV (sterm_sem I (args i))
 2. continuous_on (range (\<lambda>x. \<chi>i. sterm_sem I (args i) x)) (\<lambda>x. Blinfun (FunctionFrechet I f x))
[PROOF STEP]
apply (simp add: frees good_interp sterm_continuous')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (range (\<lambda>x. \<chi>i. sterm_sem I (args i) x)) (\<lambda>x. Blinfun (FunctionFrechet I f x))
[PROOF STEP]
using continuous_on_subset great_interp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_on ?s ?f; ?t \<subseteq> ?s\<rbrakk> \<Longrightarrow> continuous_on ?t ?f
continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I ?f5 x))

goal (1 subgoal):
 1. continuous_on (range (\<lambda>x. \<chi>i. sterm_sem I (args i) x)) (\<lambda>x. Blinfun (FunctionFrechet I f x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
continuous_on UNIV ((\<lambda>x. Blinfun (FunctionFrechet I f x)) \<circ> (\<lambda>x. \<chi>i. sterm_sem I (args i) x))

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have blin_frech_vec:"\<And>x. bounded_linear (\<lambda>v'. \<chi> i. frechet I (args i) x v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. bounded_linear (\<lambda>v'. \<chi>i. frechet I (args i) x v')
[PROOF STEP]
by (simp add: bounded_linear_vec frechet_linear frees good_interp)
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>v'. \<chi>i. frechet I (args i) ?x5 v')

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have frech_vec_eq:"(\<lambda>x. Blinfun (\<lambda>v'. \<chi> i. frechet I (args i) x v')) = (\<lambda>x. blinfun_vec (\<lambda> i. blin_frechet (good_interp I) (simple_term (args i)) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v')) = (\<lambda>x. blinfun_vec (\<lambda>i. blin_frechet (good_interp I) (simple_term (args i)) x))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v') = blinfun_vec (\<lambda>i. blin_frechet (good_interp I) (simple_term (args i)) x)
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. blinfun_apply (Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v')) i = blinfun_apply (blinfun_vec (\<lambda>i. blin_frechet (good_interp I) (simple_term (args i)) x)) i
[PROOF STEP]
apply(rule vec_extensionality)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i ia. blinfun_apply (Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v')) i $ ia = blinfun_apply (blinfun_vec (\<lambda>i. blin_frechet (good_interp I) (simple_term (args i)) x)) i $ ia
[PROOF STEP]
subgoal for x i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v')) i $ j = blinfun_apply (blinfun_vec (\<lambda>i. blin_frechet (good_interp I) (simple_term (args i)) x)) i $ j
[PROOF STEP]
using blin_frech_vec[of x]
[PROOF STATE]
proof (prove)
using this:
bounded_linear (\<lambda>v'. \<chi>i. frechet I (args i) x v')

goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v')) i $ j = blinfun_apply (blinfun_vec (\<lambda>i. blin_frechet (good_interp I) (simple_term (args i)) x)) i $ j
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (\<lambda>v'. \<chi>i. frechet I (args i) x v') \<Longrightarrow> blinfun_apply (Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v')) i $ j = frechet (raw_interp (good_interp I)) (raw_term (simple_term (args j))) x i
[PROOF STEP]
by (metis (no_types, lifting) blin_frechet.rep_eq bounded_linear_Blinfun_apply frechet_blin frechet_linear frees good_interp vec_lambda_beta)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>x. Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v')) = (\<lambda>x. blinfun_vec (\<lambda>i. blin_frechet (good_interp I) (simple_term (args i)) x))

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have cont_frech_vec:"continuous_on UNIV (\<lambda>x. blinfun_vec (\<lambda> i. blin_frechet (good_interp I) (simple_term (args i)) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. blinfun_vec (\<lambda>i. blin_frechet (good_interp I) (simple_term (args i)) x))
[PROOF STEP]
apply(rule continuous_blinfun_vec')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args ?i5)))

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

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have cont_intro:"\<And> s f g. 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>s f g. \<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 ?s5 ?f5; continuous_on ?s5 ?g5\<rbrakk> \<Longrightarrow> continuous_on ?s5 (\<lambda>x. ?f5 x o\<^sub>L ?g5 x)

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have cont:"continuous_on UNIV (\<lambda>v. blinfun_compose (Blinfun (FunctionFrechet I f (\<chi> i. sterm_sem I (args i) v))) (Blinfun(\<lambda>v'.  (\<chi> i. frechet I (args i) v v'))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>v. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v'))
[PROOF STEP]
apply(rule cont_intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) x)))
 2. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v'))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) x)))
[PROOF STEP]
using  sub_cont
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV ((\<lambda>x. Blinfun (FunctionFrechet I f x)) \<circ> (\<lambda>x. \<chi>i. sterm_sem I (args i) x))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) x)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v'))
[PROOF STEP]
using frech_vec_eq cont_frech_vec
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v')) = (\<lambda>x. blinfun_vec (\<lambda>i. blin_frechet (good_interp I) (simple_term (args i)) x))
continuous_on UNIV (\<lambda>x. blinfun_vec (\<lambda>i. blin_frechet (good_interp I) (simple_term (args i)) x))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) x v'))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>v. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v'))

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have best_eq:"(blin_frechet (good_interp I) (simple_term ($f f args))) = (\<lambda>v. blinfun_compose (Blinfun (FunctionFrechet I f (\<chi> i. sterm_sem I (args i) v))) (Blinfun(\<lambda>v'.  (\<chi> i. frechet I (args i) v v')))) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blin_frechet (good_interp I) (simple_term ($f f args)) = (\<lambda>v. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v'))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. blin_frechet (good_interp I) (simple_term ($f f args)) v = Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v')
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v i. blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i = blinfun_apply (Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v')) i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v i. blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i = blinfun_apply (Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v')) i
[PROOF STEP]
fix v :: "(real, 'sz) vec" and i :: "(real, 'sz) vec"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v i. blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i = blinfun_apply (Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v')) i
[PROOF STEP]
have "frechet I ($f f args) v i = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet I ($f f args) v i = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i
[PROOF STEP]
by (metis (no_types) bounded_linear_Blinfun_apply dfree_Fun_simps frechet_blin frechet_linear frees good_interp)
[PROOF STATE]
proof (state)
this:
frechet I ($f f args) v i = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i

goal (1 subgoal):
 1. \<And>v i. blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i = blinfun_apply (Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v')) i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
frechet I ($f f args) v i = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i
[PROOF STEP]
have "FunctionFrechet I f (\<chi> s. sterm_sem I (args s) v) (blinfun_apply (Blinfun (\<lambda>va. \<chi> s. frechet I (args s) v va)) i) = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i"
[PROOF STATE]
proof (prove)
using this:
frechet I ($f f args) v i = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i

goal (1 subgoal):
 1. FunctionFrechet I f (\<chi>s. sterm_sem I (args s) v) (blinfun_apply (Blinfun (\<lambda>va. \<chi>s. frechet I (args s) v va)) i) = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i
[PROOF STEP]
by (simp add: blin_frech_vec bounded_linear_Blinfun_apply)
[PROOF STATE]
proof (state)
this:
FunctionFrechet I f (\<chi>s. sterm_sem I (args s) v) (blinfun_apply (Blinfun (\<lambda>va. \<chi>s. frechet I (args s) v va)) i) = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i

goal (1 subgoal):
 1. \<And>v i. blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i = blinfun_apply (Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v')) i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FunctionFrechet I f (\<chi>s. sterm_sem I (args s) v) (blinfun_apply (Blinfun (\<lambda>va. \<chi>s. frechet I (args s) v va)) i) = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i
[PROOF STEP]
show "blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i = blinfun_apply (Blinfun (FunctionFrechet I f (\<chi> s. sterm_sem I (args s) v)) o\<^sub>L Blinfun (\<lambda>va. \<chi> s. frechet I (args s) v va)) i"
[PROOF STATE]
proof (prove)
using this:
FunctionFrechet I f (\<chi>s. sterm_sem I (args s) v) (blinfun_apply (Blinfun (\<lambda>va. \<chi>s. frechet I (args s) v va)) i) = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i

goal (1 subgoal):
 1. blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i = blinfun_apply (Blinfun (FunctionFrechet I f (\<chi>s. sterm_sem I (args s) v)) o\<^sub>L Blinfun (\<lambda>va. \<chi>s. frechet I (args s) v va)) i
[PROOF STEP]
by (metis (no_types) blinfun_apply_blinfun_compose bounded_linear_Blinfun_apply bounded_linears)
[PROOF STATE]
proof (state)
this:
blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i = blinfun_apply (Blinfun (FunctionFrechet I f (\<chi>s. sterm_sem I (args s) v)) o\<^sub>L Blinfun (\<lambda>va. \<chi>s. frechet I (args s) v va)) i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
blin_frechet (good_interp I) (simple_term ($f f args)) = (\<lambda>v. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v'))

goal (3 subgoals):
 1. \<And>args i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f i args)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 3. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
blin_frechet (good_interp I) (simple_term ($f f args)) = (\<lambda>v. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
blin_frechet (good_interp I) (simple_term ($f f args)) = (\<lambda>v. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v'))

goal (1 subgoal):
 1. continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f f args)))
[PROOF STEP]
using cont best_eq
[PROOF STATE]
proof (prove)
using this:
blin_frechet (good_interp I) (simple_term ($f f args)) = (\<lambda>v. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v'))
continuous_on UNIV (\<lambda>v. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v'))
blin_frechet (good_interp I) (simple_term ($f f args)) = (\<lambda>v. Blinfun (FunctionFrechet I f (\<chi>i. sterm_sem I (args i) v)) o\<^sub>L Blinfun (\<lambda>v'. \<chi>i. frechet I (args i) v v'))

goal (1 subgoal):
 1. continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f f args)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term ($f f args)))

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

goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
assume IH1:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1))"
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1))

goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
assume IH2:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))"
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))

goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
assume free1:"dfree \<theta>\<^sub>1"
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>1

goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
assume free2:"dfree \<theta>\<^sub>2"
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>2

goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have free:"dfree (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)
[PROOF STEP]
using free1 free2
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>\<^sub>1
dfree \<theta>\<^sub>2

goal (1 subgoal):
 1. dfree (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dfree (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)

goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have bounded_linear:"\<And>v. bounded_linear (\<lambda>v'. frechet I \<theta>\<^sub>1 v v' + frechet I \<theta>\<^sub>2 v v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. bounded_linear (\<lambda>v'. frechet I \<theta>\<^sub>1 v v' + frechet I \<theta>\<^sub>2 v v')
[PROOF STEP]
subgoal for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear (\<lambda>v'. frechet I \<theta>\<^sub>1 v v' + frechet I \<theta>\<^sub>2 v v')
[PROOF STEP]
using frechet_linear[OF good_interp free]
[PROOF STATE]
proof (prove)
using this:
bounded_linear (frechet I (Plus \<theta>\<^sub>1 \<theta>\<^sub>2) ?v)

goal (1 subgoal):
 1. bounded_linear (\<lambda>v'. frechet I \<theta>\<^sub>1 v v' + frechet I \<theta>\<^sub>2 v v')
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>v'. frechet I \<theta>\<^sub>1 ?v5 v' + frechet I \<theta>\<^sub>2 ?v5 v')

goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have eq2:"(\<lambda>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) = blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) = blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v = blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)) v
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v i. blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) i = blinfun_apply (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)) v) i
[PROOF STEP]
by (simp add: blinfun.add_left free1 free2 simple_term_inverse)
[PROOF STATE]
proof (state)
this:
(\<lambda>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) = blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))

goal (2 subgoals):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
 2. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have cont:"continuous_on UNIV (\<lambda>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v)
[PROOF STEP]
using continuous_on_add dfree_Plus.IH(1) dfree_Plus.IH(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_on ?s ?f; continuous_on ?s ?g\<rbrakk> \<Longrightarrow> continuous_on ?s (\<lambda>x. ?f x + ?g x)
continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1))
continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v)

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

goal (1 subgoal):
 1. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
using cont eq2
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v)
continuous_on UNIV (\<lambda>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v)
(\<lambda>v. blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v + blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) = blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2))

goal (1 subgoal):
 1. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Plus \<theta>\<^sub>1 \<theta>\<^sub>2)))

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

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
assume IH1:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1))"
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1))

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
assume IH2:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))"
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
assume free1:"dfree \<theta>\<^sub>1"
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>1

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
assume free2:"dfree \<theta>\<^sub>2"
[PROOF STATE]
proof (state)
this:
dfree \<theta>\<^sub>2

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have free:"dfree (Times \<theta>\<^sub>1 \<theta>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfree (Times \<theta>\<^sub>1 \<theta>\<^sub>2)
[PROOF STEP]
using free1 free2
[PROOF STATE]
proof (prove)
using this:
dfree \<theta>\<^sub>1
dfree \<theta>\<^sub>2

goal (1 subgoal):
 1. dfree (Times \<theta>\<^sub>1 \<theta>\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dfree (Times \<theta>\<^sub>1 \<theta>\<^sub>2)

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have bounded_linear:"\<And>v. bounded_linear (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. bounded_linear (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)
[PROOF STEP]
apply(rule bounded_linear_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. bounded_linear (\<lambda>x. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v x)
 2. \<And>v. bounded_linear (\<lambda>x. frechet I \<theta>\<^sub>1 v x * sterm_sem I \<theta>\<^sub>2 v)
[PROOF STEP]
apply(rule bounded_linear_const_mult)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. bounded_linear (frechet I \<theta>\<^sub>2 v)
 2. \<And>v. bounded_linear (\<lambda>x. frechet I \<theta>\<^sub>1 v x * sterm_sem I \<theta>\<^sub>2 v)
[PROOF STEP]
using frechet_linear[OF good_interp free2]
[PROOF STATE]
proof (prove)
using this:
bounded_linear (frechet I \<theta>\<^sub>2 ?v)

goal (2 subgoals):
 1. \<And>v. bounded_linear (frechet I \<theta>\<^sub>2 v)
 2. \<And>v. bounded_linear (\<lambda>x. frechet I \<theta>\<^sub>1 v x * sterm_sem I \<theta>\<^sub>2 v)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. (\<And>v. bounded_linear (frechet I \<theta>\<^sub>2 v)) \<Longrightarrow> bounded_linear (\<lambda>x. frechet I \<theta>\<^sub>1 v x * sterm_sem I \<theta>\<^sub>2 v)
[PROOF STEP]
apply(rule bounded_linear_mult_const)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. (\<And>v. bounded_linear (frechet I \<theta>\<^sub>2 v)) \<Longrightarrow> bounded_linear (frechet I \<theta>\<^sub>1 v)
[PROOF STEP]
using frechet_linear[OF good_interp free1]
[PROOF STATE]
proof (prove)
using this:
bounded_linear (frechet I \<theta>\<^sub>1 ?v)

goal (1 subgoal):
 1. \<And>v. (\<And>v. bounded_linear (frechet I \<theta>\<^sub>2 v)) \<Longrightarrow> bounded_linear (frechet I \<theta>\<^sub>1 v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounded_linear (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 ?v5 * frechet I \<theta>\<^sub>2 ?v5 v' + frechet I \<theta>\<^sub>1 ?v5 v' * sterm_sem I \<theta>\<^sub>2 ?v5)

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bounded_linear (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 ?v5 * frechet I \<theta>\<^sub>2 ?v5 v' + frechet I \<theta>\<^sub>1 ?v5 v' * sterm_sem I \<theta>\<^sub>2 ?v5)
[PROOF STEP]
have blin':"\<And>v. (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v) \<in> {f. bounded_linear f}"
[PROOF STATE]
proof (prove)
using this:
bounded_linear (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 ?v5 * frechet I \<theta>\<^sub>2 ?v5 v' + frechet I \<theta>\<^sub>1 ?v5 v' * sterm_sem I \<theta>\<^sub>2 ?v5)

goal (1 subgoal):
 1. \<And>v. (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v) \<in> {f. bounded_linear f}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>v'. sterm_sem I \<theta>\<^sub>1 ?v5 * frechet I \<theta>\<^sub>2 ?v5 v' + frechet I \<theta>\<^sub>1 ?v5 v' * sterm_sem I \<theta>\<^sub>2 ?v5) \<in> {f. bounded_linear f}

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have blinfun_eq:"\<And>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)
    =  scaleR (sterm_sem I \<theta>\<^sub>1 v) (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) + scaleR (sterm_sem I \<theta>\<^sub>2 v) (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v) = sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v i. blinfun_apply (Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) i = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i
[PROOF STEP]
subgoal for v i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) i = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i
[PROOF STEP]
using Blinfun_inverse[OF blin', of v]
[PROOF STATE]
proof (prove)
using this:
blinfun_apply (Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)

goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) i = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v) \<Longrightarrow> sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v i + frechet I \<theta>\<^sub>1 v i * sterm_sem I \<theta>\<^sub>2 v = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i
[PROOF STEP]
using blinfun.add_left[of "sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v" "sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v"]
        blinfun.scaleR_left[of "sterm_sem I \<theta>\<^sub>1 v" "blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v"]
        blinfun.scaleR_left[of "sterm_sem I \<theta>\<^sub>2 v" "blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v"]
        bounded_linear_Blinfun_apply
        frechet_blin[OF good_interp free1]
        frechet_blin[OF good_interp free2]
        frechet_linear[OF good_interp free1]
        frechet_linear[OF good_interp free2]
        mult.commute
        real_scaleR_def
[PROOF STATE]
proof (prove)
using this:
blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) ?b = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) ?b + blinfun_apply (sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) ?b
blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) ?b = sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) ?b
blinfun_apply (sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) ?b = sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) ?b
bounded_linear ?f \<Longrightarrow> blinfun_apply (Blinfun ?f) = ?f
(\<lambda>v. Blinfun (frechet I \<theta>\<^sub>1 v)) = blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)
(\<lambda>v. Blinfun (frechet I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2)
bounded_linear (frechet I \<theta>\<^sub>1 ?v)
bounded_linear (frechet I \<theta>\<^sub>2 ?v)
?a * ?b = ?b * ?a
?a *\<^sub>R ?x = ?a * ?x

goal (1 subgoal):
 1. blinfun_apply (Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v) \<Longrightarrow> sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v i + frechet I \<theta>\<^sub>1 v i * sterm_sem I \<theta>\<^sub>2 v = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>blinfun_apply (Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v); \<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b + blinfun_apply (sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b; \<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b = sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b; \<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b = sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b; \<And>f. bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f; (\<lambda>v. Blinfun (frechet I \<theta>\<^sub>1 v)) = blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1); (\<lambda>v. Blinfun (frechet I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2); \<And>v. bounded_linear (frechet I \<theta>\<^sub>1 v); \<And>v. bounded_linear (frechet I \<theta>\<^sub>2 v); \<And>a b. a * b = b * a; \<And>a x. a *\<^sub>R x = a * x\<rbrakk> \<Longrightarrow> sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v i + frechet I \<theta>\<^sub>1 v i * sterm_sem I \<theta>\<^sub>2 v = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i
[PROOF STEP]
have f1: "\<And>v. blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) = frechet I \<theta>\<^sub>1 v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) = frechet I \<theta>\<^sub>1 v
[PROOF STEP]
by (metis (no_types) \<open>(\<lambda>v. Blinfun (frechet I \<theta>\<^sub>1 v)) = blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)\<close> \<open>\<And>v. bounded_linear (frechet I \<theta>\<^sub>1 v)\<close> bounded_linear_Blinfun_apply)
[PROOF STATE]
proof (state)
this:
blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) ?v5) = frechet I \<theta>\<^sub>1 ?v5

goal (1 subgoal):
 1. \<lbrakk>blinfun_apply (Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v); \<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b + blinfun_apply (sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b; \<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b = sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b; \<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b = sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b; \<And>f. bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f; (\<lambda>v. Blinfun (frechet I \<theta>\<^sub>1 v)) = blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1); (\<lambda>v. Blinfun (frechet I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2); \<And>v. bounded_linear (frechet I \<theta>\<^sub>1 v); \<And>v. bounded_linear (frechet I \<theta>\<^sub>2 v); \<And>a b. a * b = b * a; \<And>a x. a *\<^sub>R x = a * x\<rbrakk> \<Longrightarrow> sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v i + frechet I \<theta>\<^sub>1 v i * sterm_sem I \<theta>\<^sub>2 v = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i
[PROOF STEP]
have "\<And>v. blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) = frechet I \<theta>\<^sub>2 v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) = frechet I \<theta>\<^sub>2 v
[PROOF STEP]
by (metis (no_types) \<open>(\<lambda>v. Blinfun (frechet I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2)\<close> \<open>\<And>v. bounded_linear (frechet I \<theta>\<^sub>2 v)\<close> bounded_linear_Blinfun_apply)
[PROOF STATE]
proof (state)
this:
blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) ?v5) = frechet I \<theta>\<^sub>2 ?v5

goal (1 subgoal):
 1. \<lbrakk>blinfun_apply (Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v); \<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b + blinfun_apply (sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b; \<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b = sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b; \<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b = sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b; \<And>f. bounded_linear f \<Longrightarrow> blinfun_apply (Blinfun f) = f; (\<lambda>v. Blinfun (frechet I \<theta>\<^sub>1 v)) = blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1); (\<lambda>v. Blinfun (frechet I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2); \<And>v. bounded_linear (frechet I \<theta>\<^sub>1 v); \<And>v. bounded_linear (frechet I \<theta>\<^sub>2 v); \<And>a b. a * b = b * a; \<And>a x. a *\<^sub>R x = a * x\<rbrakk> \<Longrightarrow> sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v i + frechet I \<theta>\<^sub>1 v i * sterm_sem I \<theta>\<^sub>2 v = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) ?v5) = frechet I \<theta>\<^sub>2 ?v5
[PROOF STEP]
show "sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v i + frechet I \<theta>\<^sub>1 v i * sterm_sem I \<theta>\<^sub>2 v = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i"
[PROOF STATE]
proof (prove)
using this:
blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) ?v5) = frechet I \<theta>\<^sub>2 ?v5

goal (1 subgoal):
 1. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v i + frechet I \<theta>\<^sub>1 v i * sterm_sem I \<theta>\<^sub>2 v = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) ?v5) = frechet I \<theta>\<^sub>2 ?v5
blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) ?v5) = frechet I \<theta>\<^sub>1 ?v5

goal (1 subgoal):
 1. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v i + frechet I \<theta>\<^sub>1 v i * sterm_sem I \<theta>\<^sub>2 v = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i
[PROOF STEP]
by (simp add: \<open>\<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b + blinfun_apply (sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b\<close> \<open>\<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b = sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v) b\<close> \<open>\<And>b. blinfun_apply (sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b = sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blinfun_apply (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) b\<close>)
[PROOF STATE]
proof (state)
this:
sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v i + frechet I \<theta>\<^sub>1 v i * sterm_sem I \<theta>\<^sub>2 v = blinfun_apply (sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v) i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 ?v5 * frechet I \<theta>\<^sub>2 ?v5 v' + frechet I \<theta>\<^sub>1 ?v5 v' * sterm_sem I \<theta>\<^sub>2 ?v5) = sterm_sem I \<theta>\<^sub>1 ?v5 *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) ?v5 + sterm_sem I \<theta>\<^sub>2 ?v5 *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) ?v5

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have cont':"continuous_on UNIV
    (\<lambda>v. scaleR (sterm_sem I \<theta>\<^sub>1 v) (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v)
       + scaleR (sterm_sem I \<theta>\<^sub>2 v) (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>v. sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v)
[PROOF STEP]
apply(rule continuous_on_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (\<lambda>x. sterm_sem I \<theta>\<^sub>1 x *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) x)
 2. continuous_on UNIV (\<lambda>x. sterm_sem I \<theta>\<^sub>2 x *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) x)
[PROOF STEP]
apply(rule continuous_on_scaleR)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous_on UNIV (sterm_sem I \<theta>\<^sub>1)
 2. continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))
 3. continuous_on UNIV (\<lambda>x. sterm_sem I \<theta>\<^sub>2 x *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) x)
[PROOF STEP]
apply(rule sterm_continuous[OF good_interp free1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))
 2. continuous_on UNIV (\<lambda>x. sterm_sem I \<theta>\<^sub>2 x *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) x)
[PROOF STEP]
apply(rule IH2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. sterm_sem I \<theta>\<^sub>2 x *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) x)
[PROOF STEP]
apply(rule continuous_on_scaleR)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on UNIV (sterm_sem I \<theta>\<^sub>2)
 2. continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1))
[PROOF STEP]
apply(rule sterm_continuous[OF good_interp free2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1))
[PROOF STEP]
by(rule IH1)
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>v. sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v)

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have cont:"continuous_on UNIV (\<lambda>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v))
[PROOF STEP]
using cont' blinfun_eq
[PROOF STATE]
proof (prove)
using this:
continuous_on UNIV (\<lambda>v. sterm_sem I \<theta>\<^sub>1 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) v + sterm_sem I \<theta>\<^sub>2 v *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) v)
Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 ?v5 * frechet I \<theta>\<^sub>2 ?v5 v' + frechet I \<theta>\<^sub>1 ?v5 v' * sterm_sem I \<theta>\<^sub>2 ?v5) = sterm_sem I \<theta>\<^sub>1 ?v5 *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2) ?v5 + sterm_sem I \<theta>\<^sub>2 ?v5 *\<^sub>R blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1) ?v5

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v))

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
have eq:"(\<lambda>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
using frechet_blin[OF good_interp free]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>v. Blinfun (frechet I (Times \<theta>\<^sub>1 \<theta>\<^sub>2) v)) = blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2))

goal (1 subgoal):
 1. (\<lambda>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2))

goal (1 subgoal):
 1. \<And>\<theta>\<^sub>1 \<theta>\<^sub>2. \<lbrakk>dfree \<theta>\<^sub>1; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>1)); dfree \<theta>\<^sub>2; continuous_on UNIV (blin_frechet (good_interp I) (simple_term \<theta>\<^sub>2))\<rbrakk> \<Longrightarrow> continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<lambda>v. Blinfun (\<lambda>v'. sterm_sem I \<theta>\<^sub>1 v * frechet I \<theta>\<^sub>2 v v' + frechet I \<theta>\<^sub>1 v v' * sterm_sem I \<theta>\<^sub>2 v)) = blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2))

goal (1 subgoal):
 1. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))
[PROOF STEP]
by (metis cont)
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (blin_frechet (good_interp I) (simple_term (Times \<theta>\<^sub>1 \<theta>\<^sub>2)))

goal:
No subgoals!
[PROOF STEP]
qed