[STATEMENT]
lemma adjoint_safe:
  assumes good_interp:"is_interp I"
  assumes good_subst:"(\<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f') "
  shows "is_interp (adjoint I \<sigma> \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_interp (local.adjoint I \<sigma> \<nu>)
[PROOF STEP]
apply(unfold adjoint_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_interp \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr>
[PROOF STEP]
apply(unfold is_interp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x i. (Functions \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i has_derivative FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x))
[PROOF STEP]
apply(auto simp del: extendf.simps extendc.simps FunctionFrechet.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. ((case SFunctions \<sigma> i of None \<Rightarrow> Functions I i | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x) (at x)
 2. \<And>i. continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x))
[PROOF STEP]
subgoal for x i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((case SFunctions \<sigma> i of None \<Rightarrow> Functions I i | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x) (at x)
[PROOF STEP]
apply(cases "SFunctions \<sigma> i = None")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. SFunctions \<sigma> i = None \<Longrightarrow> ((case SFunctions \<sigma> i of None \<Rightarrow> Functions I i | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x) (at x)
 2. SFunctions \<sigma> i \<noteq> None \<Longrightarrow> ((case SFunctions \<sigma> i of None \<Rightarrow> Functions I i | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x) (at x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFunctions \<sigma> i = None \<Longrightarrow> ((case SFunctions \<sigma> i of None \<Rightarrow> Functions I i | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x) (at x)
[PROOF STEP]
apply(auto simp del: extendf.simps extendc.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFunctions \<sigma> i = None \<Longrightarrow> (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x)
[PROOF STEP]
using good_interp
[PROOF STATE]
proof (prove)
using this:
is_interp I

goal (1 subgoal):
 1. SFunctions \<sigma> i = None \<Longrightarrow> (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at 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. SFunctions \<sigma> i = None \<Longrightarrow> (Functions I i has_derivative (THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x) (at x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFunctions \<sigma> i \<noteq> None \<Longrightarrow> ((case SFunctions \<sigma> i of None \<Rightarrow> Functions I i | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x) (at x)
[PROOF STEP]
apply(auto  simp del: extendf.simps extendc.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. SFunctions \<sigma> i = Some y \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) y \<nu>) has_derivative (THE f'. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) y \<nu>) has_derivative f' x) (at x)) x) (at x)
[PROOF STEP]
subgoal for f'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFunctions \<sigma> i = Some f' \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
using good_subst[of i f']
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'

goal (1 subgoal):
 1. SFunctions \<sigma> i = Some f' \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
apply (auto  simp del: extendf.simps extendc.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
assume some:"SFunctions \<sigma> i = Some f'"
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> i = Some f'

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
assume free:"dfree f'"
[PROOF STATE]
proof (state)
this:
dfree f'

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
let ?f = "(\<lambda>R. dterm_sem (extendf I R) f' \<nu>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
let ?Pred = "(\<lambda>fd. (\<forall>x. (?f has_derivative (fd x)) (at x)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
let ?f''="extendf_deriv I i f' \<nu>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
have Pf:"?Pred ?f''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)
[PROOF STEP]
using extendf_deriv[OF good_subst[of i f'] good_interp, of \<nu> i, OF some]
[PROOF STATE]
proof (prove)
using this:
\<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)

goal (1 subgoal):
 1. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
have "(THE G. (?f has_derivative G) (at x)) = ?f'' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE G. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G) (at x)) = extendf_deriv I i f' \<nu> x
[PROOF STEP]
apply(rule the_deriv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)
[PROOF STEP]
using Pf
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)

goal (1 subgoal):
 1. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE G. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G) (at x)) = extendf_deriv I i f' \<nu> x

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(THE G. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G) (at x)) = extendf_deriv I i f' \<nu> x
[PROOF STEP]
have the_eq:"(THE G. \<forall> x. (?f has_derivative G x) (at x)) = ?f''"
[PROOF STATE]
proof (prove)
using this:
(THE G. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G) (at x)) = extendf_deriv I i f' \<nu> x

goal (1 subgoal):
 1. (THE G. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G x) (at x)) = extendf_deriv I i f' \<nu>
[PROOF STEP]
using Pf the_all_deriv
[PROOF STATE]
proof (prove)
using this:
(THE G. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G) (at x)) = extendf_deriv I i f' \<nu> x
\<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)
\<forall>x. (?f has_derivative ?F x) (at x) \<Longrightarrow> (THE G. \<forall>x. (?f has_derivative G x) (at x)) = ?F

goal (1 subgoal):
 1. (THE G. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G x) (at x)) = extendf_deriv I i f' \<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE G. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G x) (at x)) = extendf_deriv I i f' \<nu>

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
show "((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
using the_eq Pf
[PROOF STATE]
proof (prove)
using this:
(THE G. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G x) (at x)) = extendf_deriv I i f' \<nu>
\<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)

goal (1 subgoal):
 1. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x) (at x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x))
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x))
[PROOF STEP]
apply(cases "SFunctions \<sigma> i = None")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. SFunctions \<sigma> i = None \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x))
 2. SFunctions \<sigma> i \<noteq> None \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFunctions \<sigma> i = None \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x))
[PROOF STEP]
apply(auto  simp del: extendf.simps extendc.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFunctions \<sigma> i = None \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x))
[PROOF STEP]
using good_interp
[PROOF STATE]
proof (prove)
using this:
is_interp I

goal (1 subgoal):
 1. SFunctions \<sigma> i = None \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) 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. SFunctions \<sigma> i = None \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I i has_derivative f' x) (at x)) x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFunctions \<sigma> i \<noteq> None \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = \<lambda>f. case SFunctions \<sigma> f of None \<Rightarrow> Functions I f | Some f' \<Rightarrow> \<lambda>R. dterm_sem (extendf I R) f' \<nu>, Predicates = \<lambda>p. case SPredicates \<sigma> p of None \<Rightarrow> Predicates I p | Some p' \<Rightarrow> \<lambda>R. \<nu> \<in> fml_sem (extendf I R) p', Contexts = \<lambda>c. case SContexts \<sigma> c of None \<Rightarrow> Contexts I c | Some c' \<Rightarrow> \<lambda>R. fml_sem (extendc I R) c', Programs = \<lambda>a. case SPrograms \<sigma> a of None \<Rightarrow> Programs I a | Some x \<Rightarrow> prog_sem I x, ODEs = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEs I ode | Some x \<Rightarrow> ODE_sem I x, ODEBV = \<lambda>ode. case SODEs \<sigma> ode of None \<Rightarrow> ODEBV I ode | Some x \<Rightarrow> ODE_vars I x\<rparr> i x))
[PROOF STEP]
apply(auto  simp del: extendf.simps extendc.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. SFunctions \<sigma> i = Some y \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) y \<nu>) has_derivative f' x) (at x)) x))
[PROOF STEP]
subgoal for f'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFunctions \<sigma> i = Some f' \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
using good_subst[of i f']
[PROOF STATE]
proof (prove)
using this:
SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'

goal (1 subgoal):
 1. SFunctions \<sigma> i = Some f' \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
apply (auto  simp del: extendf.simps extendc.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
assume some:"SFunctions \<sigma> i = Some f'"
[PROOF STATE]
proof (state)
this:
SFunctions \<sigma> i = Some f'

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
assume free:"dfree f'"
[PROOF STATE]
proof (state)
this:
dfree f'

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
let ?f = "(\<lambda>R. dterm_sem (extendf I R) f' \<nu>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
let ?Pred = "(\<lambda>fd. (\<forall>x. (?f has_derivative (fd x)) (at x)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
let ?f''="extendf_deriv I i f' \<nu>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
have Pf:"?Pred ?f''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)
[PROOF STEP]
using extendf_deriv[OF good_subst[of i f'] good_interp, of \<nu> i, OF some]
[PROOF STATE]
proof (prove)
using this:
\<exists>f''. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)

goal (1 subgoal):
 1. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
have "\<And>x. (THE G. (?f has_derivative G) (at x)) = ?f'' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (THE G. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G) (at x)) = extendf_deriv I i f' \<nu> x
[PROOF STEP]
apply(rule the_deriv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)
[PROOF STEP]
using Pf
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)

goal (1 subgoal):
 1. \<And>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE G. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G) (at ?x7)) = extendf_deriv I i f' \<nu> ?x7

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(THE G. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G) (at ?x7)) = extendf_deriv I i f' \<nu> ?x7
[PROOF STEP]
have the_eq:"(THE G. \<forall> x. (?f has_derivative G x) (at x)) = ?f''"
[PROOF STATE]
proof (prove)
using this:
(THE G. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G) (at ?x7)) = extendf_deriv I i f' \<nu> ?x7

goal (1 subgoal):
 1. (THE G. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G x) (at x)) = extendf_deriv I i f' \<nu>
[PROOF STEP]
using Pf the_all_deriv
[PROOF STATE]
proof (prove)
using this:
(THE G. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G) (at ?x7)) = extendf_deriv I i f' \<nu> ?x7
\<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)
\<forall>x. (?f has_derivative ?F x) (at x) \<Longrightarrow> (THE G. \<forall>x. (?f has_derivative G x) (at x)) = ?F

goal (1 subgoal):
 1. (THE G. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G x) (at x)) = extendf_deriv I i f' \<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE G. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G x) (at x)) = extendf_deriv I i f' \<nu>

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
have "continuous_on UNIV (\<lambda>x. Blinfun (?f'' x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i f' \<nu> x))
[PROOF STEP]
by(rule extendf_deriv_continuous[OF free good_interp])
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i f' \<nu> x))

goal (1 subgoal):
 1. \<lbrakk>SFunctions \<sigma> i = Some f'; dfree f'\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
show "continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
using the_eq Pf
[PROOF STATE]
proof (prove)
using this:
(THE G. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative G x) (at x)) = extendf_deriv I i f' \<nu>
\<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative extendf_deriv I i f' \<nu> x) (at x)

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
by (simp add: \<open>continuous_on UNIV (\<lambda>x. Blinfun (extendf_deriv I i f' \<nu> x))\<close>)
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>R. dterm_sem (extendf I R) f' \<nu>) has_derivative f'a x) (at x)) x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma adjointFO_safe:
  assumes good_interp:"is_interp I"
  assumes good_subst:"(\<And>i. dsafe (\<sigma> i))"
  shows "is_interp (adjointFO I \<sigma> \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_interp (adjointFO I \<sigma> \<nu>)
[PROOF STEP]
apply(unfold adjointFO_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_interp \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr>
[PROOF STEP]
apply(unfold is_interp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x i. (Functions \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i has_derivative FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x))
[PROOF STEP]
apply(auto simp del: extendf.simps extendc.simps FunctionFrechet.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. ((case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x) (at x)
 2. \<And>i. continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x))
[PROOF STEP]
subgoal for x i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x) (at x)
[PROOF STEP]
apply(cases "i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. i = Inl a \<Longrightarrow> ((case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x) (at x)
 2. \<And>b. i = Inr b \<Longrightarrow> ((case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x) (at x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = Inl a_ \<Longrightarrow> ((case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x) (at x)
[PROOF STEP]
apply(auto  simp del: extendf.simps extendc.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = Inl a_ \<Longrightarrow> (Functions I a_ has_derivative (THE f'. \<forall>x. (Functions I a_ has_derivative f' x) (at x)) x) (at x)
[PROOF STEP]
using good_interp
[PROOF STATE]
proof (prove)
using this:
is_interp I

goal (1 subgoal):
 1. i = Inl a_ \<Longrightarrow> (Functions I a_ has_derivative (THE f'. \<forall>x. (Functions I a_ has_derivative f' x) (at x)) x) (at 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. i = Inl a_ \<Longrightarrow> (Functions I a_ has_derivative (THE f'. \<forall>x. (Functions I a_ has_derivative f' x) (at x)) x) (at x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. i = Inr b \<Longrightarrow> ((case i of Inl x \<Rightarrow> Functions I x | Inr f' \<Rightarrow> \<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x) (at x)
[PROOF STEP]
apply(auto  simp del: extendf.simps extendc.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. i = Inr b \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> b) \<nu>) has_derivative (THE f'. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> b) \<nu>) has_derivative f' x) (at x)) x) (at x)
[PROOF STEP]
subgoal for f'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
assume some:"i = Inr f'"
[PROOF STATE]
proof (state)
this:
i = Inr f'

goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
have free:"dsafe (\<sigma> f')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dsafe (\<sigma> f')
[PROOF STEP]
using good_subst
[PROOF STATE]
proof (prove)
using this:
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. dsafe (\<sigma> f')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dsafe (\<sigma> f')

goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
let ?f = "(\<lambda>_. dterm_sem I (\<sigma> f') \<nu>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
let ?Pred = "(\<lambda>fd. (\<forall>x. (?f has_derivative (fd x)) (at x)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
let ?f''="(\<lambda>_ _. 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
have Pf:"?Pred ?f''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
[PROOF STEP]
proof (induction "\<sigma> f'")
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x. Var x = \<sigma> f' \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
 2. \<And>x. Const x = \<sigma> f' \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
 3. \<And>x1a x2a. \<lbrakk>\<sigma> f' \<in> range x2a \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x); $f x1a x2a = \<sigma> f'\<rbrakk> \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
 4. \<And>xa1 xa2. \<lbrakk>xa1 = \<sigma> f' \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x); xa2 = \<sigma> f' \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x); Plus xa1 xa2 = \<sigma> f'\<rbrakk> \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
 5. \<And>xa1 xa2. \<lbrakk>xa1 = \<sigma> f' \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x); xa2 = \<sigma> f' \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x); Times xa1 xa2 = \<sigma> f'\<rbrakk> \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
 6. \<And>x. $' x = \<sigma> f' \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
 7. \<And>xa. \<lbrakk>xa = \<sigma> f' \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x); Differential xa = \<sigma> f'\<rbrakk> \<Longrightarrow> \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
[PROOF STEP]
qed (auto)
[PROOF STATE]
proof (state)
this:
\<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)

goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
have "(THE G. (?f has_derivative G) (at x)) = ?f'' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE G. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative G) (at x)) = (\<lambda>_. 0)
[PROOF STEP]
apply(rule the_deriv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
[PROOF STEP]
using Pf
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)

goal (1 subgoal):
 1. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE G. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative G) (at x)) = (\<lambda>_. 0)

goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(THE G. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative G) (at x)) = (\<lambda>_. 0)
[PROOF STEP]
have the_eq:"(THE G. \<forall> x. (?f has_derivative G x) (at x)) = ?f''"
[PROOF STATE]
proof (prove)
using this:
(THE G. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative G) (at x)) = (\<lambda>_. 0)

goal (1 subgoal):
 1. (THE G. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)
[PROOF STEP]
using Pf the_all_deriv[of ?f ?f'']
[PROOF STATE]
proof (prove)
using this:
(THE G. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative G) (at x)) = (\<lambda>_. 0)
\<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
\<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x) \<Longrightarrow> (THE G. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)

goal (1 subgoal):
 1. (THE G. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE G. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)

goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
have another_eq:"(THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x = (\<lambda> _. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x = (\<lambda>_. 0)
[PROOF STEP]
using Pf
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)

goal (1 subgoal):
 1. (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x = (\<lambda>_. 0)
[PROOF STEP]
by (simp add: the_eq)
[PROOF STATE]
proof (state)
this:
(THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x = (\<lambda>_. 0)

goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x = (\<lambda>_. 0)
[PROOF STEP]
show "((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)"
[PROOF STATE]
proof (prove)
using this:
(THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x = (\<lambda>_. 0)

goal (1 subgoal):
 1. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
using the_eq Pf
[PROOF STATE]
proof (prove)
using this:
(THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x = (\<lambda>_. 0)
(THE G. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)
\<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)

goal (1 subgoal):
 1. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative (THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) (at x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x))
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x))
[PROOF STEP]
apply(cases i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. i = Inl a \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x))
 2. \<And>b. i = Inr b \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = Inl a_ \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x))
[PROOF STEP]
apply(auto  simp del: extendf.simps extendc.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = Inl a_ \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I a_ has_derivative f' x) (at x)) x))
[PROOF STEP]
using good_interp
[PROOF STATE]
proof (prove)
using this:
is_interp I

goal (1 subgoal):
 1. i = Inl a_ \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I a_ has_derivative f' x) (at x)) 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. i = Inl a_ \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. (Functions I a_ has_derivative f' x) (at x)) x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. i = Inr b \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = case_sum (Functions I) (\<lambda>f' _. dterm_sem I (\<sigma> f') \<nu>), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x))
[PROOF STEP]
apply(auto  simp del: extendf.simps extendc.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. i = Inr b \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> b) \<nu>) has_derivative f' x) (at x)) x))
[PROOF STEP]
subgoal for f'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
using good_subst[of f']
[PROOF STATE]
proof (prove)
using this:
dsafe (\<sigma> f')

goal (1 subgoal):
 1. i = Inr f' \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
assume some:"i = Inr f'"
[PROOF STATE]
proof (state)
this:
i = Inr f'

goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
have free:"dsafe (\<sigma> f')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dsafe (\<sigma> f')
[PROOF STEP]
using good_subst
[PROOF STATE]
proof (prove)
using this:
dsafe (\<sigma> ?i7)

goal (1 subgoal):
 1. dsafe (\<sigma> f')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dsafe (\<sigma> f')

goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
let ?f = "(\<lambda>R. dterm_sem I (\<sigma> f') \<nu>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
let ?Pred = "(\<lambda>fd. (\<forall>x. (?f has_derivative (fd x)) (at x)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
let ?f''="(\<lambda>_ _. 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
(* *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
have Pf:"?Pred ?f''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)

goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
have "\<And>x. (THE G. (?f has_derivative G) (at x)) = ?f'' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (THE G. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G) (at x)) = (\<lambda>_. 0)
[PROOF STEP]
apply(rule the_deriv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
[PROOF STEP]
using Pf
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)

goal (1 subgoal):
 1. \<And>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE G. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G) (at ?x11)) = (\<lambda>_. 0)

goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(THE G. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G) (at ?x11)) = (\<lambda>_. 0)
[PROOF STEP]
have the_eq:"(THE G. \<forall> x. (?f has_derivative G x) (at x)) = ?f''"
[PROOF STATE]
proof (prove)
using this:
(THE G. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G) (at ?x11)) = (\<lambda>_. 0)

goal (1 subgoal):
 1. (THE G. \<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)
[PROOF STEP]
using Pf the_all_deriv[of "(\<lambda>R. dterm_sem I (\<sigma> f') \<nu>)" "(\<lambda>_ _. 0)"]
[PROOF STATE]
proof (prove)
using this:
(THE G. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G) (at ?x11)) = (\<lambda>_. 0)
\<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x)
\<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative (\<lambda>_. 0)) (at x) \<Longrightarrow> (THE G. \<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)

goal (1 subgoal):
 1. (THE G. \<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(THE G. \<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)

goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(THE G. \<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)
[PROOF STEP]
have blin_cont:"continuous_on UNIV (\<lambda>x. Blinfun (?f'' x))"
[PROOF STATE]
proof (prove)
using this:
(THE G. \<forall>x. ((\<lambda>R. dterm_sem I (\<sigma> f') \<nu>) has_derivative G x) (at x)) = (\<lambda>_ _. 0)

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>_. 0::'d))
[PROOF STEP]
by (simp add: continuous_on_const)
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun (\<lambda>_. 0::?'d14))

goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
have truth:"(\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
        = (\<lambda>x. Blinfun (\<lambda> _. 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x)) = (\<lambda>x. Blinfun (\<lambda>_. 0))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x) = Blinfun (\<lambda>_. 0)
[PROOF STEP]
apply(rule blinfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. blinfun_apply (Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x)) i = blinfun_apply (Blinfun (\<lambda>_. 0)) i
[PROOF STEP]
by (simp add: local.the_eq)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x)) = (\<lambda>x. Blinfun (\<lambda>_. 0))

goal (1 subgoal):
 1. \<lbrakk>i = Inr f'; dsafe (\<sigma> f')\<rbrakk> \<Longrightarrow> continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x)) = (\<lambda>x. Blinfun (\<lambda>_. 0))
[PROOF STEP]
show "continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x)) = (\<lambda>x. Blinfun (\<lambda>_. 0))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
using truth
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x)) = (\<lambda>x. Blinfun (\<lambda>_. 0))
(\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x)) = (\<lambda>x. Blinfun (\<lambda>_. 0))

goal (1 subgoal):
 1. continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))
[PROOF STEP]
by (metis (mono_tags, lifting) blin_cont continuous_on_eq)
[PROOF STATE]
proof (state)
this:
continuous_on UNIV (\<lambda>x. Blinfun ((THE f'a. \<forall>x. ((\<lambda>_. dterm_sem I (\<sigma> f') \<nu>) has_derivative f'a x) (at x)) x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done