[STATEMENT]
lemma nsubst_fml:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes \<nu>::"'sz state"
  assumes good_interp:"is_interp I"
  assumes NFA:"NFadmit \<sigma> \<phi>"
  assumes fsafe:"fsafe \<phi>"
  assumes frees:"(\<forall>i. dsafe (\<sigma> i))"
  shows "(\<nu> \<in> fml_sem I (FsubstFO \<phi> \<sigma>)) = (\<nu> \<in> fml_sem (adjointFO I \<sigma> \<nu>) \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> \<in> fml_sem I (FsubstFO \<phi> \<sigma>)) = (\<nu> \<in> fml_sem (adjointFO I \<sigma> \<nu>) \<phi>)
[PROOF STEP]
using good_interp NFA fsafe frees
[PROOF STATE]
proof (prove)
using this:
is_interp I
NFadmit \<sigma> \<phi>
fsafe \<phi>
\<forall>i. dsafe (\<sigma> i)

goal (1 subgoal):
 1. (\<nu> \<in> fml_sem I (FsubstFO \<phi> \<sigma>)) = (\<nu> \<in> fml_sem (adjointFO I \<sigma> \<nu>) \<phi>)
[PROOF STEP]
by (auto simp add: nsubst_hp_fml)


[STATEMENT]
lemma nsubst_hp:
  fixes I::"('sf, 'sc, 'sz) interp"
  fixes \<nu>::"'sz state"
  assumes good_interp:"is_interp I"
  assumes NPA:"NPadmit \<sigma> \<alpha>"
  assumes hpsafe:"hpsafe \<alpha>"
  assumes frees:"\<And>i. dsafe (\<sigma> i)"
  shows "((\<nu>, \<omega>) \<in> prog_sem I (PsubstFO \<alpha> \<sigma>)) = ((\<nu>, \<omega>) \<in>  prog_sem (adjointFO I \<sigma> \<nu>) \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<nu>, \<omega>) \<in> prog_sem I (PsubstFO \<alpha> \<sigma>)) = ((\<nu>, \<omega>) \<in> prog_sem (adjointFO I \<sigma> \<nu>) \<alpha>)
[PROOF STEP]
using good_interp NPA hpsafe frees nsubst_hp_fml
[PROOF STATE]
proof (prove)
using this:
is_interp I
NPadmit \<sigma> \<alpha>
hpsafe \<alpha>
dsafe (\<sigma> ?i7)
is_interp ?I \<Longrightarrow> (NPadmit ?\<sigma> ?\<alpha> \<longrightarrow> hpsafe ?\<alpha> \<longrightarrow> (\<forall>i. dsafe (?\<sigma> i)) \<longrightarrow> (\<forall>\<nu> \<omega>. ((\<nu>, \<omega>) \<in> prog_sem ?I (PsubstFO ?\<alpha> ?\<sigma>)) = ((\<nu>, \<omega>) \<in> prog_sem (adjointFO ?I ?\<sigma> \<nu>) ?\<alpha>))) \<and> (NFadmit ?\<sigma> ?\<phi> \<longrightarrow> fsafe ?\<phi> \<longrightarrow> (\<forall>i. dsafe (?\<sigma> i)) \<longrightarrow> (\<forall>\<nu>. (\<nu> \<in> fml_sem ?I (FsubstFO ?\<phi> ?\<sigma>)) = (\<nu> \<in> fml_sem (adjointFO ?I ?\<sigma> \<nu>) ?\<phi>)))

goal (1 subgoal):
 1. ((\<nu>, \<omega>) \<in> prog_sem I (PsubstFO \<alpha> \<sigma>)) = ((\<nu>, \<omega>) \<in> prog_sem (adjointFO I \<sigma> \<nu>) \<alpha>)
[PROOF STEP]
by blast


[STATEMENT]
lemma psubst_sterm:
  fixes I::"('sf, 'sc, 'sz) interp"
  assumes good_interp:"is_interp I"
  shows "(sterm_sem I \<theta> = sterm_sem (PFadjoint I \<sigma>) \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterm_sem I \<theta> = sterm_sem (PFadjoint I \<sigma>) \<theta>
[PROOF STEP]
proof (induction \<theta>)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x. sterm_sem I (Var x) = sterm_sem (PFadjoint I \<sigma>) (Var x)
 2. \<And>x. sterm_sem I (Const x) = sterm_sem (PFadjoint I \<sigma>) (Const x)
 3. \<And>x1a x2a. (\<And>x2aa. x2aa \<in> range x2a \<Longrightarrow> sterm_sem I x2aa = sterm_sem (PFadjoint I \<sigma>) x2aa) \<Longrightarrow> sterm_sem I ($f x1a x2a) = sterm_sem (PFadjoint I \<sigma>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>sterm_sem I \<theta>1 = sterm_sem (PFadjoint I \<sigma>) \<theta>1; sterm_sem I \<theta>2 = sterm_sem (PFadjoint I \<sigma>) \<theta>2\<rbrakk> \<Longrightarrow> sterm_sem I (Plus \<theta>1 \<theta>2) = sterm_sem (PFadjoint I \<sigma>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>sterm_sem I \<theta>1 = sterm_sem (PFadjoint I \<sigma>) \<theta>1; sterm_sem I \<theta>2 = sterm_sem (PFadjoint I \<sigma>) \<theta>2\<rbrakk> \<Longrightarrow> sterm_sem I (Times \<theta>1 \<theta>2) = sterm_sem (PFadjoint I \<sigma>) (Times \<theta>1 \<theta>2)
 6. \<And>x. sterm_sem I ($' x) = sterm_sem (PFadjoint I \<sigma>) ($' x)
 7. \<And>\<theta>. sterm_sem I \<theta> = sterm_sem (PFadjoint I \<sigma>) \<theta> \<Longrightarrow> sterm_sem I (Differential \<theta>) = sterm_sem (PFadjoint I \<sigma>) (Differential \<theta>)
[PROOF STEP]
qed (auto simp add: PFadjoint_def)


[STATEMENT]
lemma psubst_dterm:
  fixes I::"('sf, 'sc, 'sz) interp"
  assumes good_interp:"is_interp I"
  shows "(dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>
[PROOF STEP]
proof (induction \<theta>)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x. dsafe (Var x) \<Longrightarrow> dterm_sem I (Var x) = dterm_sem (PFadjoint I \<sigma>) (Var x)
 2. \<And>x. dsafe (Const x) \<Longrightarrow> dterm_sem I (Const x) = dterm_sem (PFadjoint I \<sigma>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; dsafe x2aa\<rbrakk> \<Longrightarrow> dterm_sem I x2aa = dterm_sem (PFadjoint I \<sigma>) x2aa; dsafe ($f x1a x2a)\<rbrakk> \<Longrightarrow> dterm_sem I ($f x1a x2a) = dterm_sem (PFadjoint I \<sigma>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Plus \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Plus \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Times \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Times \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Times \<theta>1 \<theta>2)
 6. \<And>x. dsafe ($' x) \<Longrightarrow> dterm_sem I ($' x) = dterm_sem (PFadjoint I \<sigma>) ($' x)
 7. \<And>\<theta>. \<lbrakk>dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>; dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem I (Differential \<theta>) = dterm_sem (PFadjoint I \<sigma>) (Differential \<theta>)
[PROOF STEP]
case (Differential \<theta>)
[PROOF STATE]
proof (state)
this:
dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>
dsafe (Differential \<theta>)

goal (7 subgoals):
 1. \<And>x. dsafe (Var x) \<Longrightarrow> dterm_sem I (Var x) = dterm_sem (PFadjoint I \<sigma>) (Var x)
 2. \<And>x. dsafe (Const x) \<Longrightarrow> dterm_sem I (Const x) = dterm_sem (PFadjoint I \<sigma>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; dsafe x2aa\<rbrakk> \<Longrightarrow> dterm_sem I x2aa = dterm_sem (PFadjoint I \<sigma>) x2aa; dsafe ($f x1a x2a)\<rbrakk> \<Longrightarrow> dterm_sem I ($f x1a x2a) = dterm_sem (PFadjoint I \<sigma>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Plus \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Plus \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Times \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Times \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Times \<theta>1 \<theta>2)
 6. \<And>x. dsafe ($' x) \<Longrightarrow> dterm_sem I ($' x) = dterm_sem (PFadjoint I \<sigma>) ($' x)
 7. \<And>\<theta>. \<lbrakk>dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>; dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem I (Differential \<theta>) = dterm_sem (PFadjoint I \<sigma>) (Differential \<theta>)
[PROOF STEP]
assume safe:"dsafe (Differential \<theta>)"
[PROOF STATE]
proof (state)
this:
dsafe (Differential \<theta>)

goal (7 subgoals):
 1. \<And>x. dsafe (Var x) \<Longrightarrow> dterm_sem I (Var x) = dterm_sem (PFadjoint I \<sigma>) (Var x)
 2. \<And>x. dsafe (Const x) \<Longrightarrow> dterm_sem I (Const x) = dterm_sem (PFadjoint I \<sigma>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; dsafe x2aa\<rbrakk> \<Longrightarrow> dterm_sem I x2aa = dterm_sem (PFadjoint I \<sigma>) x2aa; dsafe ($f x1a x2a)\<rbrakk> \<Longrightarrow> dterm_sem I ($f x1a x2a) = dterm_sem (PFadjoint I \<sigma>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Plus \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Plus \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Times \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Times \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Times \<theta>1 \<theta>2)
 6. \<And>x. dsafe ($' x) \<Longrightarrow> dterm_sem I ($' x) = dterm_sem (PFadjoint I \<sigma>) ($' x)
 7. \<And>\<theta>. \<lbrakk>dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>; dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem I (Differential \<theta>) = dterm_sem (PFadjoint I \<sigma>) (Differential \<theta>)
[PROOF STEP]
from safe
[PROOF STATE]
proof (chain)
picking this:
dsafe (Differential \<theta>)
[PROOF STEP]
have free:"dfree \<theta>"
[PROOF STATE]
proof (prove)
using this:
dsafe (Differential \<theta>)

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

goal (7 subgoals):
 1. \<And>x. dsafe (Var x) \<Longrightarrow> dterm_sem I (Var x) = dterm_sem (PFadjoint I \<sigma>) (Var x)
 2. \<And>x. dsafe (Const x) \<Longrightarrow> dterm_sem I (Const x) = dterm_sem (PFadjoint I \<sigma>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; dsafe x2aa\<rbrakk> \<Longrightarrow> dterm_sem I x2aa = dterm_sem (PFadjoint I \<sigma>) x2aa; dsafe ($f x1a x2a)\<rbrakk> \<Longrightarrow> dterm_sem I ($f x1a x2a) = dterm_sem (PFadjoint I \<sigma>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Plus \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Plus \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Times \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Times \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Times \<theta>1 \<theta>2)
 6. \<And>x. dsafe ($' x) \<Longrightarrow> dterm_sem I ($' x) = dterm_sem (PFadjoint I \<sigma>) ($' x)
 7. \<And>\<theta>. \<lbrakk>dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>; dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem I (Differential \<theta>) = dterm_sem (PFadjoint I \<sigma>) (Differential \<theta>)
[PROOF STEP]
assume sem:"dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>"
[PROOF STATE]
proof (state)
this:
dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>

goal (7 subgoals):
 1. \<And>x. dsafe (Var x) \<Longrightarrow> dterm_sem I (Var x) = dterm_sem (PFadjoint I \<sigma>) (Var x)
 2. \<And>x. dsafe (Const x) \<Longrightarrow> dterm_sem I (Const x) = dterm_sem (PFadjoint I \<sigma>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; dsafe x2aa\<rbrakk> \<Longrightarrow> dterm_sem I x2aa = dterm_sem (PFadjoint I \<sigma>) x2aa; dsafe ($f x1a x2a)\<rbrakk> \<Longrightarrow> dterm_sem I ($f x1a x2a) = dterm_sem (PFadjoint I \<sigma>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Plus \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Plus \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Times \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Times \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Times \<theta>1 \<theta>2)
 6. \<And>x. dsafe ($' x) \<Longrightarrow> dterm_sem I ($' x) = dterm_sem (PFadjoint I \<sigma>) ($' x)
 7. \<And>\<theta>. \<lbrakk>dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>; dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem I (Differential \<theta>) = dterm_sem (PFadjoint I \<sigma>) (Differential \<theta>)
[PROOF STEP]
have "\<And>\<nu>. frechet I \<theta> (fst \<nu>) (snd \<nu>) = frechet (PFadjoint I \<sigma>) \<theta> (fst \<nu>) (snd \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<nu>. frechet I \<theta> (fst \<nu>) (snd \<nu>) = frechet (PFadjoint I \<sigma>) \<theta> (fst \<nu>) (snd \<nu>)
[PROOF STEP]
apply(rule sterm_determines_frechet)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>\<nu>. is_interp I
 2. \<And>\<nu>. is_interp (PFadjoint I \<sigma>)
 3. \<And>\<nu>. dfree \<theta>
 4. \<And>\<nu>. dfree \<theta>
 5. \<And>\<nu>. sterm_sem I \<theta> = sterm_sem (PFadjoint I \<sigma>) \<theta>
[PROOF STEP]
using good_interp free
[PROOF STATE]
proof (prove)
using this:
is_interp I
dfree \<theta>

goal (5 subgoals):
 1. \<And>\<nu>. is_interp I
 2. \<And>\<nu>. is_interp (PFadjoint I \<sigma>)
 3. \<And>\<nu>. dfree \<theta>
 4. \<And>\<nu>. dfree \<theta>
 5. \<And>\<nu>. sterm_sem I \<theta> = sterm_sem (PFadjoint I \<sigma>) \<theta>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_interp I; dfree \<theta>\<rbrakk> \<Longrightarrow> is_interp (PFadjoint I \<sigma>)
 2. \<lbrakk>is_interp I; dfree \<theta>\<rbrakk> \<Longrightarrow> sterm_sem I \<theta> = sterm_sem (PFadjoint I \<sigma>) \<theta>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_interp I; dfree \<theta>\<rbrakk> \<Longrightarrow> is_interp (PFadjoint I \<sigma>)
[PROOF STEP]
unfolding is_interp_def PFadjoint_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<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)); dfree \<theta>\<rbrakk> \<Longrightarrow> \<forall>x i. (Functions \<lparr>Functions = Functions I, Predicates = Predicates I, Contexts = case_sum (Contexts I) (\<lambda>f' _. fml_sem I (\<sigma> f')), Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i has_derivative FunctionFrechet \<lparr>Functions = Functions I, Predicates = Predicates I, Contexts = case_sum (Contexts I) (\<lambda>f' _. fml_sem I (\<sigma> f')), Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x) (at x) \<and> continuous_on UNIV (\<lambda>x. Blinfun (FunctionFrechet \<lparr>Functions = Functions I, Predicates = Predicates I, Contexts = case_sum (Contexts I) (\<lambda>f' _. fml_sem I (\<sigma> f')), Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> i x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_interp I; dfree \<theta>\<rbrakk> \<Longrightarrow> sterm_sem I \<theta> = sterm_sem (PFadjoint I \<sigma>) \<theta>
[PROOF STEP]
using psubst_sterm[of I \<theta>]
[PROOF STATE]
proof (prove)
using this:
is_interp I \<Longrightarrow> sterm_sem I \<theta> = sterm_sem (PFadjoint I ?\<sigma>) \<theta>

goal (1 subgoal):
 1. \<lbrakk>is_interp I; dfree \<theta>\<rbrakk> \<Longrightarrow> sterm_sem I \<theta> = sterm_sem (PFadjoint I \<sigma>) \<theta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
frechet I \<theta> (fst ?\<nu>7) (snd ?\<nu>7) = frechet (PFadjoint I \<sigma>) \<theta> (fst ?\<nu>7) (snd ?\<nu>7)

goal (7 subgoals):
 1. \<And>x. dsafe (Var x) \<Longrightarrow> dterm_sem I (Var x) = dterm_sem (PFadjoint I \<sigma>) (Var x)
 2. \<And>x. dsafe (Const x) \<Longrightarrow> dterm_sem I (Const x) = dterm_sem (PFadjoint I \<sigma>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; dsafe x2aa\<rbrakk> \<Longrightarrow> dterm_sem I x2aa = dterm_sem (PFadjoint I \<sigma>) x2aa; dsafe ($f x1a x2a)\<rbrakk> \<Longrightarrow> dterm_sem I ($f x1a x2a) = dterm_sem (PFadjoint I \<sigma>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Plus \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Plus \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Times \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Times \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Times \<theta>1 \<theta>2)
 6. \<And>x. dsafe ($' x) \<Longrightarrow> dterm_sem I ($' x) = dterm_sem (PFadjoint I \<sigma>) ($' x)
 7. \<And>\<theta>. \<lbrakk>dsafe \<theta> \<Longrightarrow> dterm_sem I \<theta> = dterm_sem (PFadjoint I \<sigma>) \<theta>; dsafe (Differential \<theta>)\<rbrakk> \<Longrightarrow> dterm_sem I (Differential \<theta>) = dterm_sem (PFadjoint I \<sigma>) (Differential \<theta>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
frechet I \<theta> (fst ?\<nu>7) (snd ?\<nu>7) = frechet (PFadjoint I \<sigma>) \<theta> (fst ?\<nu>7) (snd ?\<nu>7)
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
using this:
frechet I \<theta> (fst ?\<nu>7) (snd ?\<nu>7) = frechet (PFadjoint I \<sigma>) \<theta> (fst ?\<nu>7) (snd ?\<nu>7)

goal (1 subgoal):
 1. dterm_sem I (Differential \<theta>) = dterm_sem (PFadjoint I \<sigma>) (Differential \<theta>)
[PROOF STEP]
by (auto simp add: directional_derivative_def)
[PROOF STATE]
proof (state)
this:
dterm_sem I (Differential \<theta>) = dterm_sem (PFadjoint I \<sigma>) (Differential \<theta>)

goal (6 subgoals):
 1. \<And>x. dsafe (Var x) \<Longrightarrow> dterm_sem I (Var x) = dterm_sem (PFadjoint I \<sigma>) (Var x)
 2. \<And>x. dsafe (Const x) \<Longrightarrow> dterm_sem I (Const x) = dterm_sem (PFadjoint I \<sigma>) (Const x)
 3. \<And>x1a x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> range x2a; dsafe x2aa\<rbrakk> \<Longrightarrow> dterm_sem I x2aa = dterm_sem (PFadjoint I \<sigma>) x2aa; dsafe ($f x1a x2a)\<rbrakk> \<Longrightarrow> dterm_sem I ($f x1a x2a) = dterm_sem (PFadjoint I \<sigma>) ($f x1a x2a)
 4. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Plus \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Plus \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Plus \<theta>1 \<theta>2)
 5. \<And>\<theta>1 \<theta>2. \<lbrakk>dsafe \<theta>1 \<Longrightarrow> dterm_sem I \<theta>1 = dterm_sem (PFadjoint I \<sigma>) \<theta>1; dsafe \<theta>2 \<Longrightarrow> dterm_sem I \<theta>2 = dterm_sem (PFadjoint I \<sigma>) \<theta>2; dsafe (Times \<theta>1 \<theta>2)\<rbrakk> \<Longrightarrow> dterm_sem I (Times \<theta>1 \<theta>2) = dterm_sem (PFadjoint I \<sigma>) (Times \<theta>1 \<theta>2)
 6. \<And>x. dsafe ($' x) \<Longrightarrow> dterm_sem I ($' x) = dterm_sem (PFadjoint I \<sigma>) ($' x)
[PROOF STEP]
qed (auto simp add: PFadjoint_def)


[STATEMENT]
lemma psubst_ode:
assumes good_interp:"is_interp I"
shows "ODE_sem I ODE = ODE_sem (PFadjoint I \<sigma>) ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_sem I ODE = ODE_sem (PFadjoint I \<sigma>) ODE
[PROOF STEP]
proof (induction "ODE")
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. ODE_sem I (OVar x) = ODE_sem (PFadjoint I \<sigma>) (OVar x)
 2. \<And>x1a x2. ODE_sem I (OSing x1a x2) = ODE_sem (PFadjoint I \<sigma>) (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1; ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2\<rbrakk> \<Longrightarrow> ODE_sem I (OProd ODE1 ODE2) = ODE_sem (PFadjoint I \<sigma>) (OProd ODE1 ODE2)
[PROOF STEP]
case (OVar x)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>x. ODE_sem I (OVar x) = ODE_sem (PFadjoint I \<sigma>) (OVar x)
 2. \<And>x1a x2. ODE_sem I (OSing x1a x2) = ODE_sem (PFadjoint I \<sigma>) (OSing x1a x2)
 3. \<And>ODE1 ODE2. \<lbrakk>ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1; ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2\<rbrakk> \<Longrightarrow> ODE_sem I (OProd ODE1 ODE2) = ODE_sem (PFadjoint I \<sigma>) (OProd ODE1 ODE2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_sem I (OVar x) = ODE_sem (PFadjoint I \<sigma>) (OVar x)
[PROOF STEP]
unfolding PFadjoint_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_sem I (OVar x) = ODE_sem \<lparr>Functions = Functions I, Predicates = Predicates I, Contexts = case_sum (Contexts I) (\<lambda>f' _. fml_sem I (\<sigma> f')), Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I\<rparr> (OVar x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_sem I (OVar x) = ODE_sem (PFadjoint I \<sigma>) (OVar x)

goal (2 subgoals):
 1. \<And>x1a x2. ODE_sem I (OSing x1a x2) = ODE_sem (PFadjoint I \<sigma>) (OSing x1a x2)
 2. \<And>ODE1 ODE2. \<lbrakk>ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1; ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2\<rbrakk> \<Longrightarrow> ODE_sem I (OProd ODE1 ODE2) = ODE_sem (PFadjoint I \<sigma>) (OProd ODE1 ODE2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1a x2. ODE_sem I (OSing x1a x2) = ODE_sem (PFadjoint I \<sigma>) (OSing x1a x2)
 2. \<And>ODE1 ODE2. \<lbrakk>ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1; ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2\<rbrakk> \<Longrightarrow> ODE_sem I (OProd ODE1 ODE2) = ODE_sem (PFadjoint I \<sigma>) (OProd ODE1 ODE2)
[PROOF STEP]
case (OSing x1a x2)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x1a x2. ODE_sem I (OSing x1a x2) = ODE_sem (PFadjoint I \<sigma>) (OSing x1a x2)
 2. \<And>ODE1 ODE2. \<lbrakk>ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1; ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2\<rbrakk> \<Longrightarrow> ODE_sem I (OProd ODE1 ODE2) = ODE_sem (PFadjoint I \<sigma>) (OProd ODE1 ODE2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ODE_sem I (OSing x1a x2) = ODE_sem (PFadjoint I \<sigma>) (OSing x1a x2)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. \<chi>i. if i = x1a then sterm_sem I x2 a else 0) = (\<lambda>a. \<chi>i. if i = x1a then sterm_sem (PFadjoint I \<sigma>) x2 a else 0)
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<chi>i. if i = x1a then sterm_sem I x2 x else 0) = (\<chi>i. if i = x1a then sterm_sem (PFadjoint I \<sigma>) x2 x else 0)
[PROOF STEP]
apply (rule vec_extensionality)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. (\<chi>i. if i = x1a then sterm_sem I x2 x else 0) $ i = (\<chi>i. if i = x1a then sterm_sem (PFadjoint I \<sigma>) x2 x else 0) $ i
[PROOF STEP]
using psubst_sterm[OF good_interp, of x2 \<sigma>]
[PROOF STATE]
proof (prove)
using this:
sterm_sem I x2 = sterm_sem (PFadjoint I \<sigma>) x2

goal (1 subgoal):
 1. \<And>x i. (\<chi>i. if i = x1a then sterm_sem I x2 x else 0) $ i = (\<chi>i. if i = x1a then sterm_sem (PFadjoint I \<sigma>) x2 x else 0) $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_sem I (OSing x1a x2) = ODE_sem (PFadjoint I \<sigma>) (OSing x1a x2)

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1; ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2\<rbrakk> \<Longrightarrow> ODE_sem I (OProd ODE1 ODE2) = ODE_sem (PFadjoint I \<sigma>) (OProd ODE1 ODE2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1; ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2\<rbrakk> \<Longrightarrow> ODE_sem I (OProd ODE1 ODE2) = ODE_sem (PFadjoint I \<sigma>) (OProd ODE1 ODE2)
[PROOF STEP]
case (OProd ODE1 ODE2)
[PROOF STATE]
proof (state)
this:
ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1
ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2

goal (1 subgoal):
 1. \<And>ODE1 ODE2. \<lbrakk>ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1; ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2\<rbrakk> \<Longrightarrow> ODE_sem I (OProd ODE1 ODE2) = ODE_sem (PFadjoint I \<sigma>) (OProd ODE1 ODE2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1
ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ODE_sem I ODE1 = ODE_sem (PFadjoint I \<sigma>) ODE1
ODE_sem I ODE2 = ODE_sem (PFadjoint I \<sigma>) ODE2

goal (1 subgoal):
 1. ODE_sem I (OProd ODE1 ODE2) = ODE_sem (PFadjoint I \<sigma>) (OProd ODE1 ODE2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ODE_sem I (OProd ODE1 ODE2) = ODE_sem (PFadjoint I \<sigma>) (OProd ODE1 ODE2)

goal:
No subgoals!
[PROOF STEP]
qed