[STATEMENT]
lemma dhops_le_hops_imp_update_strictly_fresher:
  assumes "dip \<in> vD(rt2 nhip)"
      and sqn: "sqn (rt2 nhip) dip = osn"
      and hop: "the (dhops (rt2 nhip) dip) \<le> hops"
      and **: "rt \<noteq> update rt dip (osn, kno, val, Suc hops, nhip, {})"
    shows "update rt dip (osn, kno, val, Suc hops, nhip, {}) \<sqsubset>\<^bsub>dip\<^esub> rt2 nhip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update rt dip (osn, kno, val, Suc hops, nhip, {}) \<sqsubset>\<^bsub>dip\<^esub> rt2 nhip
[PROOF STEP]
unfolding rt_strictly_fresher_def'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) < nsqn\<^sub>r (the (rt2 nhip dip)) \<or> nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip)) \<and> \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
proof (rule disjI2, rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))
 2. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
from **
[PROOF STATE]
proof (chain)
picking this:
rt \<noteq> update rt dip (osn, kno, val, Suc hops, nhip, {})
[PROOF STEP]
have "nsqn (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip = osn"
[PROOF STATE]
proof (prove)
using this:
rt \<noteq> update rt dip (osn, kno, val, Suc hops, nhip, {})

goal (1 subgoal):
 1. nsqn (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip = osn
[PROOF STEP]
by (rule nsqn_update_changed_kno_val)
[PROOF STATE]
proof (state)
this:
nsqn (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip = osn

goal (2 subgoals):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))
 2. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
with \<open>dip\<in>vD(rt2 nhip)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> vD (rt2 nhip)
nsqn (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip = osn
[PROOF STEP]
have "nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = osn"
[PROOF STATE]
proof (prove)
using this:
dip \<in> vD (rt2 nhip)
nsqn (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip = osn

goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = osn
[PROOF STEP]
by (simp add: kD_nsqn)
[PROOF STATE]
proof (state)
this:
nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = osn

goal (2 subgoals):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))
 2. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = osn

goal (2 subgoals):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))
 2. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
have "osn = sqn (rt2 nhip) dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. osn = sqn (rt2 nhip) dip
[PROOF STEP]
by (rule sqn [symmetric])
[PROOF STATE]
proof (state)
this:
osn = sqn (rt2 nhip) dip

goal (2 subgoals):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))
 2. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
osn = sqn (rt2 nhip) dip

goal (2 subgoals):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))
 2. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
have "sqn (rt2 nhip) dip = nsqn\<^sub>r (the (rt2 nhip dip))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqn (rt2 nhip) dip = nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
unfolding nsqn\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqn (rt2 nhip) dip = (if \<pi>\<^sub>4 (the (rt2 nhip dip)) = val \<or> \<pi>\<^sub>2 (the (rt2 nhip dip)) = 0 then \<pi>\<^sub>2 (the (rt2 nhip dip)) else \<pi>\<^sub>2 (the (rt2 nhip dip)) - 1)
[PROOF STEP]
using \<open>dip \<in> vD(rt2 nhip)\<close>
[PROOF STATE]
proof (prove)
using this:
dip \<in> vD (rt2 nhip)

goal (1 subgoal):
 1. sqn (rt2 nhip) dip = (if \<pi>\<^sub>4 (the (rt2 nhip dip)) = val \<or> \<pi>\<^sub>2 (the (rt2 nhip dip)) = 0 then \<pi>\<^sub>2 (the (rt2 nhip dip)) else \<pi>\<^sub>2 (the (rt2 nhip dip)) - 1)
[PROOF STEP]
by - (metis vD_flag_val proj2_eq_sqn proj4_eq_flag vD_iD_gives_kD(1))
[PROOF STATE]
proof (state)
this:
sqn (rt2 nhip) dip = nsqn\<^sub>r (the (rt2 nhip dip))

goal (2 subgoals):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))
 2. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
show "nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
                                                              = nsqn\<^sub>r (the (rt2 nhip dip))"
[PROOF STATE]
proof (prove)
using this:
nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))

goal (1 subgoal):
 1. nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
nsqn\<^sub>r (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip)) = nsqn\<^sub>r (the (rt2 nhip dip))

goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
have "the (dhops (rt2 nhip) dip) \<le> hops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (dhops (rt2 nhip) dip) \<le> hops
[PROOF STEP]
by (rule hop)
[PROOF STATE]
proof (state)
this:
the (dhops (rt2 nhip) dip) \<le> hops

goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
the (dhops (rt2 nhip) dip) \<le> hops

goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
have "hops < hops + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hops < hops + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hops < hops + 1

goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hops < hops + 1

goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
have "hops + 1 = the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hops + 1 = the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
rt \<noteq> update rt dip (osn, kno, val, Suc hops, nhip, {})

goal (1 subgoal):
 1. hops + 1 = the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hops + 1 = the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)

goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
the (dhops (rt2 nhip) dip) < the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)
[PROOF STEP]
have "the (dhops (rt2 nhip) dip)
                        < the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)"
[PROOF STATE]
proof (prove)
using this:
the (dhops (rt2 nhip) dip) < the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)

goal (1 subgoal):
 1. the (dhops (rt2 nhip) dip) < the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
the (dhops (rt2 nhip) dip) < the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)

goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
thus "\<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))"
[PROOF STATE]
proof (prove)
using this:
the (dhops (rt2 nhip) dip) < the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)

goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
using \<open>dip \<in> vD(rt2 nhip)\<close>
[PROOF STATE]
proof (prove)
using this:
the (dhops (rt2 nhip) dip) < the (dhops (update rt dip (osn, kno, val, Suc hops, nhip, {})) dip)
dip \<in> vD (rt2 nhip)

goal (1 subgoal):
 1. \<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))
[PROOF STEP]
by (simp add: proj5_eq_dhops)
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>5 (the (rt2 nhip dip)) < \<pi>\<^sub>5 (the (update rt dip (osn, kno, val, Suc hops, nhip, {}) dip))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nsqn_invalidate:
  assumes "dip \<in> kD(rt)"
      and "\<forall>ip\<in>dom(dests). ip \<in> vD(rt) \<and> the (dests ip) = inc (sqn rt ip)"
    shows "nsqn (invalidate rt dests) dip = nsqn rt dip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = nsqn rt dip
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = nsqn rt dip
[PROOF STEP]
from \<open>dip \<in> kD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
[PROOF STEP]
have "dip \<in> kD(invalidate rt dests)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt

goal (1 subgoal):
 1. dip \<in> kD (invalidate rt dests)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dip \<in> kD (invalidate rt dests)

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = nsqn rt dip
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
\<forall>ip\<in>dom dests. ip \<in> vD rt \<and> the (dests ip) = inc (sqn rt ip)
[PROOF STEP]
have "rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests"
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
\<forall>ip\<in>dom dests. ip \<in> vD rt \<and> the (dests ip) = inc (sqn rt ip)

goal (1 subgoal):
 1. rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
by (rule rt_fresh_as_inc_invalidate)
[PROOF STATE]
proof (state)
this:
rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = nsqn rt dip
[PROOF STEP]
with \<open>dip \<in> kD(rt)\<close> \<open>dip \<in> kD(invalidate rt dests)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> kD rt
dip \<in> kD (invalidate rt dests)
rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dip \<in> kD rt
dip \<in> kD (invalidate rt dests)
rt \<approx>\<^bsub>dip\<^esub> invalidate rt dests

goal (1 subgoal):
 1. nsqn (invalidate rt dests) dip = nsqn rt dip
[PROOF STEP]
by (simp add: kD_nsqn del: invalidate_kD_inv)
         (erule(2) rt_fresh_as_nsqnr)
[PROOF STATE]
proof (state)
this:
nsqn (invalidate rt dests) dip = nsqn rt dip

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma interp_eq:
  "f = f' \<Longrightarrow> p = p' \<Longrightarrow> c = c' \<Longrightarrow> PP = PP' \<Longrightarrow> ode = ode' \<Longrightarrow> odebv = odebv' \<Longrightarrow>
   \<lparr>Functions = f, Predicates = p, Contexts = c, Programs = PP, ODEs = ode, ODEBV = odebv\<rparr> =
   \<lparr>Functions = f', Predicates = p', Contexts = c', Programs = PP', ODEs = ode', ODEBV = odebv'\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = f'; p = p'; c = c'; PP = PP'; ode = ode'; odebv = odebv'\<rbrakk> \<Longrightarrow> \<lparr>Functions = f, Predicates = p, Contexts = c, Programs = PP, ODEs = ode, ODEBV = odebv\<rparr> = \<lparr>Functions = f', Predicates = p', Contexts = c', Programs = PP', ODEs = ode', ODEBV = odebv'\<rparr>
[PROOF STEP]
by auto


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

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

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) ($f f args) \<nu>)
[PROOF STEP]
apply(cases f)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) ($f f args) \<nu>)
 2. \<And>b. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) (args i) \<nu>); f = Inr b\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) ($f f args) \<nu>)
[PROOF STEP]
apply (auto simp add: continuous_intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Functions I a (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
apply(rule continuous_on_compose2[of UNIV "Functions I a" UNIV "(\<lambda> x. (\<chi> i. dterm_sem
                       \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I,
                          Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
                       (args i) \<nu>))"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (Functions I a)
 2. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
 3. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> range (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<subseteq> UNIV
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (Functions I a)
[PROOF STEP]
using is_interpD[OF good_interp]
[PROOF STATE]
proof (prove)
using this:
\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (Functions I a)
[PROOF STEP]
using has_derivative_continuous_on[of UNIV "(Functions I a)" "(THE f'. \<forall>x. (Functions I a has_derivative f' x) (at x))"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x)
(\<And>x. x \<in> UNIV \<Longrightarrow> (Functions I a has_derivative (THE f'. \<forall>x. (Functions I a has_derivative f' x) (at x)) x) (at x)) \<Longrightarrow> continuous_on UNIV (Functions I a)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (Functions I a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
 2. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> range (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<subseteq> UNIV
[PROOF STEP]
apply(rule continuous_on_vec_lambda)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>)
 2. \<lbrakk>\<And>i. dfree (args i); \<And>i. continuous_on UNIV (\<lambda>x. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>); f = Inl a\<rbrakk> \<Longrightarrow> range (\<lambda>x. \<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<subseteq> UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. dterm_sem (extendf I x) ($f f args) \<nu>)

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


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

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

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

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

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

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

goal (1 subgoal):
 1. bounded_linear (extendf_deriv I i ($f f args) \<nu> x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x)\<rbrakk> \<Longrightarrow> bounded_linear (case f of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)
[PROOF STEP]
apply(cases f)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear (case f of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)
 2. \<And>b. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inr b\<rbrakk> \<Longrightarrow> bounded_linear (case f of Inl ff \<Rightarrow> (THE f'. \<forall>y. (Functions I ff has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) \<circ> (\<lambda>\<nu>'. \<chi>ia. extendf_deriv I i (args ia) \<nu> x \<nu>') | Inr ff \<Rightarrow> \<lambda>\<nu>'. \<nu>' $ ff)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>b. (THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>) (\<chi>ia. extendf_deriv I i (args ia) \<nu> x b))
[PROOF STEP]
apply(rule bounded_linear_compose[of "(THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y))
           (\<chi> i. dterm_sem
                  \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
                     ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
                  (args i) \<nu>)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
 2. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>xa. \<chi>ia. extendf_deriv I i (args ia) \<nu> x xa)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
using good_interp
[PROOF STATE]
proof (prove)
using this:
is_interp I

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
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. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
using has_derivative_bounded_linear
[PROOF STATE]
proof (prove)
using this:
\<forall>x i. (Functions I i has_derivative FunctionFrechet I i x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet I i x))
(?f has_derivative ?f') ?F \<Longrightarrow> bounded_linear ?f'

goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear ((THE f'. \<forall>y. (Functions I a has_derivative f' y) (at y)) (\<chi>i. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (args i) \<nu>))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>xa. \<chi>ia. extendf_deriv I i (args ia) \<nu> x xa)
[PROOF STEP]
apply(rule bounded_linear_vec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>\<And>i. dfree (args i); \<And>ia. bounded_linear (extendf_deriv I i (args ia) \<nu> x); f = Inl a\<rbrakk> \<Longrightarrow> bounded_linear (extendf_deriv I i (args ia) \<nu> x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
bounded_linear (extendf_deriv I i ($f f args) \<nu> x)

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

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

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

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

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

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

goal (1 subgoal):
 1. bounded_linear (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x); bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>a. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x a + extendf_deriv I i \<theta>\<^sub>1 \<nu> x a * dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>)
[PROOF STEP]
apply(rule bounded_linear_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x); bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>xa. dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>1 \<nu> * extendf_deriv I i \<theta>\<^sub>2 \<nu> x xa)
 2. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x); bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>xa. extendf_deriv I i \<theta>\<^sub>1 \<nu> x xa * dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>)
[PROOF STEP]
apply(rule bounded_linear_const_mult)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x); bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)\<rbrakk> \<Longrightarrow> bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)
 2. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x); bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>xa. extendf_deriv I i \<theta>\<^sub>1 \<nu> x xa * dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x); bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)\<rbrakk> \<Longrightarrow> bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x); bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)\<rbrakk> \<Longrightarrow> bounded_linear (\<lambda>xa. extendf_deriv I i \<theta>\<^sub>1 \<nu> x xa * dterm_sem \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> \<theta>\<^sub>2 \<nu>)
[PROOF STEP]
apply(rule bounded_linear_mult_const)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x); bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)\<rbrakk> \<Longrightarrow> bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfree \<theta>\<^sub>1; dfree \<theta>\<^sub>2; bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x); bounded_linear (extendf_deriv I i \<theta>\<^sub>2 \<nu> x)\<rbrakk> \<Longrightarrow> bounded_linear (extendf_deriv I i \<theta>\<^sub>1 \<nu> x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
bounded_linear (extendf_deriv I i (Times \<theta>\<^sub>1 \<theta>\<^sub>2) \<nu> x)

goal:
No subgoals!
[PROOF STEP]
qed