Theory USubst_Lemma
theory "USubst_Lemma"
imports
Ordinary_Differential_Equations.ODE_Analysis
"Ids"
"Lib"
"Syntax"
"Denotational_Semantics"
"Frechet_Correctness"
"Static_Semantics"
"Coincidence"
"Bound_Effect"
"USubst"
begin context ids begin
section ‹Soundness proof for uniform substitution rule›
lemma interp_eq:
"f = f' ⟹ p = p' ⟹ c = c' ⟹ PP = PP' ⟹ ode = ode' ⟹ odebv = odebv' ⟹
⦇Functions = f, Predicates = p, Contexts = c, Programs = PP, ODEs = ode, ODEBV = odebv⦈ =
⦇Functions = f', Predicates = p', Contexts = c', Programs = PP', ODEs = ode', ODEBV = odebv'⦈"
by auto
subsection ‹Lemmas about well-formedness of (adjoint) interpretations.›
text ‹When adding a function to an interpretation with {\tt extendf}, we need to show it's C1 continuous.
We do this by explicitly constructing the derivative {\tt extendf\_deriv} and showing it's continuous.›
primrec extendf_deriv :: "('sf,'sc,'sz) interp ⇒ 'sf ⇒ ('sf + 'sz,'sz) trm ⇒ 'sz state ⇒ 'sz Rvec ⇒ ('sz Rvec ⇒ real)"
where
"extendf_deriv I _ (Var i) ν x = (λ_. 0)"
| "extendf_deriv I _ (Const r) ν x = (λ_. 0)"
| "extendf_deriv I g (Function f args) ν x =
(case f of
Inl ff ⇒ (THE f'. ∀y. (Functions I ff has_derivative f' y) (at y))
(χ i. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈
(args i) ν) ∘
(λν'. χ ia. extendf_deriv I g (args ia) ν x ν')
| Inr ff ⇒ (λ ν'. ν' $ ff))"
| "extendf_deriv I g (Plus t1 t2) ν x = (λν'. (extendf_deriv I g t1 ν x ν') + (extendf_deriv I g t2 ν x ν'))"
| "extendf_deriv I g (Times t1 t2) ν x =
(λν'. ((dterm_sem (extendf I x) t1 ν * (extendf_deriv I g t2 ν x ν')))
+ (extendf_deriv I g t1 ν x ν') * (dterm_sem (extendf I x) t2 ν))"
| "extendf_deriv I g ($' _) ν = undefined"
| "extendf_deriv I g (Differential _) ν = undefined"
lemma extendf_dterm_sem_continuous:
fixes f'::"('sf + 'sz,'sz) trm" and I::"('sf,'sc,'sz) interp"
assumes free:"dfree f'"
assumes good_interp:"is_interp I"
shows "continuous_on UNIV (λx. dterm_sem (extendf I x) f' ν)"
proof(induction rule: dfree.induct[OF free])
case (3 args f)
then show ?case
apply(cases f)
apply (auto simp add: continuous_intros)
subgoal for a
apply(rule continuous_on_compose2[of UNIV "Functions I a" UNIV "(λ x. (χ i. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I,
Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I⦈
(args i) ν))"])
subgoal
using is_interpD[OF good_interp]
using has_derivative_continuous_on[of UNIV "(Functions I a)" "(THE f'. ∀x. (Functions I a has_derivative f' x) (at x))"]
by auto
apply(rule continuous_on_vec_lambda) by auto
done
qed (auto simp add: continuous_intros)
lemma extendf_deriv_bounded:
fixes f'::"('sf + 'sz,'sz) trm" and I::"('sf,'sc,'sz) interp"
assumes free:"dfree f'"
assumes good_interp:"is_interp I"
shows "bounded_linear (extendf_deriv I i f' ν x)"
proof(induction rule: dfree.induct[OF free])
case (1 i)
then show ?case by auto
next
case (2 r)
then show ?case by auto
next
case (3 args f)
then show ?case apply auto
apply(cases f)
apply auto
subgoal for a
apply(rule bounded_linear_compose[of "(THE f'. ∀y. (Functions I a has_derivative f' y) (at y))
(χ i. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈
(args i) ν)"])
subgoal using good_interp unfolding is_interp_def using has_derivative_bounded_linear by fastforce
apply(rule bounded_linear_vec)
by auto
done
next
case (4 θ⇩1 θ⇩2)
then show ?case apply auto
using bounded_linear_add by blast
next
case (5 θ⇩1 θ⇩2)
then show ?case apply auto
apply(rule bounded_linear_add)
apply(rule bounded_linear_const_mult)
subgoal by auto
apply(rule bounded_linear_mult_const)
subgoal by auto
done
qed
lemma extendf_deriv_continuous:
fixes f'::"('sf + 'sz,'sz) trm" and I::"('sf,'sc,'sz) interp"
assumes free:"dfree f'"
assumes good_interp:"is_interp I"
shows "continuous_on UNIV (λx. Blinfun (extendf_deriv I i f' ν x))"
proof (induction rule: dfree.induct[OF free])
case (3 args f)
assume dfrees:"⋀i. dfree (args i)"
assume const:"⋀j. continuous_on UNIV (λx. Blinfun (extendf_deriv I i (args j) ν x))"
then show ?case
unfolding extendf_deriv.simps
apply(cases f)
subgoal for a
apply simp
proof -
have boundedF:"⋀x. bounded_linear (((THE f'. ∀y. (Functions I a has_derivative f' y) (at y))
(χ i. dterm_sem (extendf I x) (args i) ν) ))"
using blinfun.bounded_linear_right using good_interp unfolding is_interp_def
by auto
have boundedG:"⋀x. bounded_linear (λ b. (χ ia. extendf_deriv I i (args ia) ν x b))"
by (simp add: bounded_linear_vec dfrees extendf_deriv_bounded good_interp)
have boundedH:"⋀x. bounded_linear (λb. (THE f'. ∀y. (Functions I a has_derivative f' y) (at y))
(χ i. dterm_sem
(extendf I x)
(args i) ν)
(χ ia. extendf_deriv I i (args ia) ν x b))"
using bounded_linear_compose boundedG boundedF by blast
have eq:"(λx. Blinfun (λb. (THE f'. ∀y. (Functions I a has_derivative f' y) (at y))
(χ i. dterm_sem
(extendf I x)
(args i) ν)
(χ ia. extendf_deriv I i (args ia) ν x b)))
=
(λx. blinfun_compose(Blinfun((THE f'. ∀y. (Functions I a has_derivative f' y) (at y))
(χ i. dterm_sem
(extendf I x)
(args i) ν) )) (Blinfun(λ b. (χ ia. extendf_deriv I i (args ia) ν x b))))"
apply(rule ext)
apply(rule blinfun_eqI)
subgoal for x ia
using boundedG[of x] blinfun_apply_blinfun_compose bounded_linear_Blinfun_apply
proof -
have f1: "bounded_linear (λv. FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν) (χ s. extendf_deriv I i (args s) ν x v))"
using FunctionFrechet.simps ‹bounded_linear (λb. (THE f'. ∀y. (Functions I a has_derivative f' y) (at y)) (χ i. dterm_sem (extendf I x) (args i) ν) (χ ia. extendf_deriv I i (args ia) ν x b))›
by fastforce
have "bounded_linear (FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν))"
using good_interp is_interp_def by blast
then have "blinfun_apply (Blinfun (FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν))) (χ s. extendf_deriv I i (args s) ν x ia) = blinfun_apply (Blinfun (λv. FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν) (χ s. extendf_deriv I i (args s) ν x v))) ia"
using f1 by (simp add: bounded_linear_Blinfun_apply)
then have "blinfun_apply (Blinfun (FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν))) (χ s. extendf_deriv I i (args s) ν x ia) = blinfun_apply (Blinfun (λv. FunctionFrechet I a (χ s. dterm_sem (extendf I x) (args s) ν) (χ s. extendf_deriv I i (args s) ν x v))) ia ∧ bounded_linear (λv. χ s. extendf_deriv I i (args s) ν x v)"
by (metis ‹bounded_linear (λb. χ ia. extendf_deriv I i (args ia) ν x b)›)
then show ?thesis
by (simp add: bounded_linear_Blinfun_apply)
qed
done
have bounds:"⋀ia x. bounded_linear (extendf_deriv I i (args ia) ν x)"
by (simp add: dfrees extendf_deriv_bounded good_interp)
have vec_bound:"⋀x. bounded_linear (λb. χ ia. extendf_deriv I i (args ia) ν x b)"
by (simp add: boundedG)
have blinfun_vec:"(λx. Blinfun (λb. χ ia. extendf_deriv I i (args ia) ν x b)) = (λx. blinfun_vec (λ ia. Blinfun(λb. extendf_deriv I i (args ia) ν x b)))"
apply(rule ext)
apply(rule blinfun_eqI)
apply(rule vec_extensionality)
subgoal for x y ia
proof -
have "(χ s. extendf_deriv I i (args s) ν x y) $ ia = blinfun_apply (blinfun_vec (λs. Blinfun (extendf_deriv I i (args s) ν x))) y $ ia"
by (simp add: bounded_linear_Blinfun_apply bounds)
then have "(χ s. extendf_deriv I i (args s) ν x y) $ ia = blinfun_apply (blinfun_vec (λs. Blinfun (extendf_deriv I i (args s) ν x))) y $ ia ∧ bounded_linear (λv. χ s. extendf_deriv I i (args s) ν x v)"
by (metis ‹bounded_linear (λb. χ ia. extendf_deriv I i (args ia) ν x b)›)
then show ?thesis
by (simp add: bounded_linear_Blinfun_apply)
qed
done
have vec_cont:"continuous_on UNIV (λx. blinfun_vec (λ ia. Blinfun(λb. extendf_deriv I i (args ia) ν x b)))"
apply(rule continuous_blinfun_vec')
using "3.IH" by blast
have cont_intro:"⋀ f g s. continuous_on s f ⟹ continuous_on s g ⟹ continuous_on s (λx. f x o⇩L g x)"
by(auto intro: continuous_intros)
have cont:"continuous_on UNIV (λx. blinfun_compose(Blinfun((THE f'. ∀y. (Functions I a has_derivative f' y) (at y))
(χ i. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I,
Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I⦈
(args i) ν) )) (Blinfun(λ b. (χ ia. extendf_deriv I i (args ia) ν x b))))"
apply(rule cont_intro)
defer
subgoal using blinfun_vec vec_cont by presburger
apply(rule continuous_on_compose2[of UNIV "(λx. Blinfun ((THE f'. ∀y. (Functions I a has_derivative f' y) (at y)) x))"])
subgoal using good_interp unfolding is_interp_def by simp
apply(rule continuous_on_vec_lambda)
subgoal for i using extendf_dterm_sem_continuous[OF dfrees[of i] good_interp] by auto
by auto
then show " continuous_on UNIV
(λx. Blinfun (λb. (THE f'. ∀y. (Functions I a has_derivative f' y) (at y))
(χ i. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I,
Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I⦈
(args i) ν)
(χ ia. extendf_deriv I i (args ia) ν x b)))"
using eq apply simp by presburger
qed
by simp
next
case (4 θ⇩1 θ⇩2)
assume free1:"dfree θ⇩1"
assume free2:"dfree θ⇩2"
assume IH1:"continuous_on UNIV (λx. Blinfun (extendf_deriv I i θ⇩1 ν x))"
assume IH2:"continuous_on UNIV (λx. Blinfun (extendf_deriv I i θ⇩2 ν x))"
have bound:"⋀x. bounded_linear (λa. extendf_deriv I i θ⇩1 ν x a + extendf_deriv I i θ⇩2 ν x a)"
using extendf_deriv_bounded[OF free1 good_interp] extendf_deriv_bounded[OF free2 good_interp]
by (simp add: bounded_linear_add)
have eq:"(λx. Blinfun (λa. extendf_deriv I i θ⇩1 ν x a + extendf_deriv I i θ⇩2 ν x a)) = (λx. Blinfun (λa. extendf_deriv I i θ⇩1 ν x a) + Blinfun (λa. extendf_deriv I i θ⇩2 ν x a))"
apply(rule ext)
apply(rule blinfun_eqI)
subgoal for x j
using bound[of x] extendf_deriv_bounded[OF free1 good_interp]
extendf_deriv_bounded[OF free2 good_interp]
blinfun.add_left[of "Blinfun (extendf_deriv I i θ⇩1 ν x)" "Blinfun (extendf_deriv I i θ⇩2 ν x)"]
bounded_linear_Blinfun_apply[of "(extendf_deriv I i θ⇩1 ν x)"]
bounded_linear_Blinfun_apply[of "(extendf_deriv I i θ⇩2 ν x)"]
by (simp add: bounded_linear_Blinfun_apply)
done
have "continuous_on UNIV (λx. Blinfun (λa. extendf_deriv I i θ⇩1 ν x a) + Blinfun (λa. extendf_deriv I i θ⇩2 ν x a))"
apply(rule continuous_intros)
using IH1 IH2 by auto
then show ?case
apply simp
using eq by presburger
next
case (5 θ⇩1 θ⇩2)
assume free1:"dfree θ⇩1"
assume free2:"dfree θ⇩2"
assume IH1:"continuous_on UNIV (λx. Blinfun (extendf_deriv I i θ⇩1 ν x))"
assume IH2:"continuous_on UNIV (λx. Blinfun (extendf_deriv I i θ⇩2 ν x))"
have bounded:"⋀x. bounded_linear (λa. dterm_sem (extendf I x) θ⇩1 ν * extendf_deriv I i θ⇩2 ν x a +
extendf_deriv I i θ⇩1 ν x a * dterm_sem (extendf I x) θ⇩2 ν)"
using extendf_deriv_bounded[OF free1 good_interp] extendf_deriv_bounded[OF free2 good_interp]
by (simp add: bounded_linear_add bounded_linear_const_mult bounded_linear_mult_const)
have eq:"(λx. Blinfun (λa. dterm_sem (extendf I x) θ⇩1 ν * extendf_deriv I i θ⇩2 ν x a +
extendf_deriv I i θ⇩1 ν x a * dterm_sem (extendf I x) θ⇩2 ν)) =
(λx. dterm_sem (extendf I x) θ⇩1 ν *⇩R Blinfun (λa. extendf_deriv I i θ⇩2 ν x a) +
dterm_sem (extendf I x) θ⇩2 ν *⇩R Blinfun (λa. extendf_deriv I i θ⇩1 ν x a))"
apply(rule ext)
apply(rule blinfun_eqI)
subgoal for x j
using extendf_deriv_bounded[OF free1 good_interp] extendf_deriv_bounded[OF free2 good_interp] bounded[of x]
blinfun.scaleR_left
bounded_linear_Blinfun_apply[of "Blinfun (extendf_deriv I i θ⇩2 ν x)"]
bounded_linear_Blinfun_apply[of "Blinfun (extendf_deriv I i θ⇩1 ν x)"]
mult.commute
plus_blinfun.rep_eq[of "dterm_sem (extendf I x) θ⇩1 ν *⇩R Blinfun (extendf_deriv I i θ⇩2 ν x)" "dterm_sem (extendf I x) θ⇩2 ν *⇩R Blinfun (extendf_deriv I i θ⇩1 ν x)"]
real_scaleR_def
by (simp add: blinfun.scaleR_left bounded_linear_Blinfun_apply)
done
have "continuous_on UNIV (λx. dterm_sem (extendf I x) θ⇩1 ν *⇩R Blinfun (λa. extendf_deriv I i θ⇩2 ν x a) +
dterm_sem (extendf I x) θ⇩2 ν *⇩R Blinfun (λa. extendf_deriv I i θ⇩1 ν x a))"
apply(rule continuous_intros)+
apply(rule extendf_dterm_sem_continuous[OF free1 good_interp])
apply(rule IH2)
apply(rule continuous_intros)+
apply(rule extendf_dterm_sem_continuous[OF free2 good_interp])
by(rule IH1)
then show ?case
unfolding extendf_deriv.simps
using eq by presburger
qed (auto intro: continuous_intros)
lemma extendf_deriv:
fixes f'::"('sf + 'sz,'sz) trm" and I::"('sf,'sc,'sz) interp"
assumes free:"dfree f'"
assumes good_interp:"is_interp I"
shows "∃f''. ∀x. ((λR. dterm_sem (extendf I R) f' ν) has_derivative (extendf_deriv I i_f f' ν x)) (at x)"
using free apply (induction rule: dfree.induct)
apply(auto)+
defer
subgoal for θ⇩1 θ⇩2 x
apply(rule has_derivative_mult)
by auto
subgoal for args i x
apply(cases "i")
defer
apply auto
subgoal for b using has_derivative_proj' by blast
subgoal for a
proof -
assume dfrees:"(⋀i. dfree (args i))"
assume IH1:"(⋀ia. ∀x. ((λR. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈
(args ia) ν) has_derivative
extendf_deriv I i_f (args ia) ν x)
(at x))"
then have IH1':"(⋀ia. ⋀x. ((λR. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈
(args ia) ν) has_derivative
extendf_deriv I i_f (args ia) ν x)
(at x))"
by auto
assume a:"i = Inl a"
have chain:"⋀f f' x s g g'. (f has_derivative f') (at x within s) ⟹
(g has_derivative g') (at (f x) within f ` s) ⟹ (g ∘ f has_derivative g' ∘ f') (at x within s)"
by (auto intro: derivative_intros)
let ?f = "(λx. Functions I a x)"
let ?g = "(λ R. (χ i. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I,
Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I⦈
(args i) ν))"
let ?myf' = "(λx. (THE f'. ∀y. (Functions I a has_derivative f' y) (at y)) (?g x))"
let ?myg' = "(λx. (λν'. χ ia. extendf_deriv I i_f (args ia) ν x ν'))"
have fg_eq:"(λR. Functions I a
(χ i. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈
(args i) ν)) = (?f ∘ ?g)"
by auto
have "∀x. ((?f o ?g) has_derivative (?myf' x ∘ ?myg' x)) (at x)"
apply (rule allI)
apply (rule diff_chain_at)
subgoal for xa
apply (rule has_derivative_vec)
subgoal for i using IH1'[of i xa] by auto
done
subgoal for xa
proof -
have deriv:"⋀x. (Functions I a has_derivative FunctionFrechet I a x) (at x)"
and cont:"continuous_on UNIV (λx. Blinfun (FunctionFrechet I a x))"
using good_interp[unfolded is_interp_def] by auto
show ?thesis
apply(rule has_derivative_at_withinI)
using deriv by auto
qed
done
then have "((?f o ?g) has_derivative (?myf' x ∘ ?myg' x)) (at x)" by auto
then show "((λR. Functions I a
(χ i. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. R $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈
(args i) ν)) has_derivative
(THE f'. ∀y. (Functions I a has_derivative f' y) (at y))
(χ i. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. x $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈
(args i) ν) ∘
(λν'. χ ia. extendf_deriv I i_f (args ia) ν x ν'))
(at x) "
using fg_eq by auto
qed
done
done
lemma adjoint_safe:
assumes good_interp:"is_interp I"
assumes good_subst:"(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f') "
shows "is_interp (adjoint I σ ν)"
apply(unfold adjoint_def)
apply(unfold is_interp_def)
apply(auto simp del: extendf.simps extendc.simps FunctionFrechet.simps)
subgoal for x i
apply(cases "SFunctions σ i = None")
subgoal
apply(auto simp del: extendf.simps extendc.simps)
using good_interp unfolding is_interp_def by simp
apply(auto simp del: extendf.simps extendc.simps)
subgoal for f'
using good_subst[of i f'] apply (auto simp del: extendf.simps extendc.simps)
proof -
assume some:"SFunctions σ i = Some f'"
assume free:"dfree f'"
let ?f = "(λR. dterm_sem (extendf I R) f' ν)"
let ?Pred = "(λfd. (∀x. (?f has_derivative (fd x)) (at x)))"
let ?f''="extendf_deriv I i f' ν"
have Pf:"?Pred ?f''"
using extendf_deriv[OF good_subst[of i f'] good_interp, of ν i, OF some]
by auto
have "(THE G. (?f has_derivative G) (at x)) = ?f'' x"
apply(rule the_deriv)
using Pf by auto
then have the_eq:"(THE G. ∀ x. (?f has_derivative G x) (at x)) = ?f''"
using Pf the_all_deriv by auto
show "((λR. dterm_sem (extendf I R) f' ν) has_derivative (THE f'a. ∀x. ((λR. dterm_sem (extendf I R) f' ν) has_derivative f'a x) (at x)) x) (at x)"
using the_eq Pf by simp
qed
done
subgoal for i
apply(cases "SFunctions σ i = None")
subgoal
apply(auto simp del: extendf.simps extendc.simps)
using good_interp unfolding is_interp_def by simp
apply(auto simp del: extendf.simps extendc.simps)
subgoal for f'
using good_subst[of i f'] apply (auto simp del: extendf.simps extendc.simps)
proof -
assume some:"SFunctions σ i = Some f'"
assume free:"dfree f'"
let ?f = "(λR. dterm_sem (extendf I R) f' ν)"
let ?Pred = "(λfd. (∀x. (?f has_derivative (fd x)) (at x)))"
let ?f''="extendf_deriv I i f' ν"
have Pf:"?Pred ?f''"
using extendf_deriv[OF good_subst[of i f'] good_interp, of ν i, OF some]
by auto
have "⋀x. (THE G. (?f has_derivative G) (at x)) = ?f'' x"
apply(rule the_deriv)
using Pf by auto
then have the_eq:"(THE G. ∀ x. (?f has_derivative G x) (at x)) = ?f''"
using Pf the_all_deriv by auto
have "continuous_on UNIV (λx. Blinfun (?f'' x))"
by(rule extendf_deriv_continuous[OF free good_interp])
show "continuous_on UNIV (λx. Blinfun ((THE f'a. ∀x. ((λR. dterm_sem (extendf I R) f' ν) has_derivative f'a x) (at x)) x))"
using the_eq Pf
by (simp add: ‹continuous_on UNIV (λx. Blinfun (extendf_deriv I i f' ν x))›)
qed
done
done
lemma adjointFO_safe:
assumes good_interp:"is_interp I"
assumes good_subst:"(⋀i. dsafe (σ i))"
shows "is_interp (adjointFO I σ ν)"
apply(unfold adjointFO_def)
apply(unfold is_interp_def)
apply(auto simp del: extendf.simps extendc.simps FunctionFrechet.simps)
subgoal for x i
apply(cases "i")
subgoal
apply(auto simp del: extendf.simps extendc.simps)
using good_interp unfolding is_interp_def by simp
apply(auto simp del: extendf.simps extendc.simps)
subgoal for f'
proof -
assume some:"i = Inr f'"
have free:"dsafe (σ f')" using good_subst by auto
let ?f = "(λ_. dterm_sem I (σ f') ν)"
let ?Pred = "(λfd. (∀x. (?f has_derivative (fd x)) (at x)))"
let ?f''="(λ_ _. 0)"
have Pf:"?Pred ?f''"
proof (induction "σ f'")
qed (auto)
have "(THE G. (?f has_derivative G) (at x)) = ?f'' x"
apply(rule the_deriv)
using Pf by auto
then have the_eq:"(THE G. ∀ x. (?f has_derivative G x) (at x)) = ?f''"
using Pf the_all_deriv[of ?f ?f''] by auto
have another_eq:"(THE f'a. ∀x. ((λ_. dterm_sem I (σ f') ν) has_derivative f'a x) (at x)) x = (λ _. 0)"
using Pf by (simp add: the_eq)
then show "((λ_. dterm_sem I (σ f') ν) has_derivative (THE f'a. ∀x. ((λ_. dterm_sem I (σ f') ν) has_derivative f'a x) (at x)) x) (at x)"
using the_eq Pf by simp
qed
done
subgoal for i
apply(cases i)
subgoal
apply(auto simp del: extendf.simps extendc.simps)
using good_interp unfolding is_interp_def by simp
apply(auto simp del: extendf.simps extendc.simps)
subgoal for f'
using good_subst[of f']
proof -
assume some:"i = Inr f'"
have free:"dsafe (σ f')" using good_subst by auto
let ?f = "(λR. dterm_sem I (σ f') ν)"
let ?Pred = "(λfd. (∀x. (?f has_derivative (fd x)) (at x)))"
let ?f''="(λ_ _. 0)"
have Pf:"?Pred ?f''" by simp
have "⋀x. (THE G. (?f has_derivative G) (at x)) = ?f'' x"
apply(rule the_deriv)
using Pf by auto
then have the_eq:"(THE G. ∀ x. (?f has_derivative G x) (at x)) = ?f''"
using Pf the_all_deriv[of "(λR. dterm_sem I (σ f') ν)" "(λ_ _. 0)"]
by blast
then have blin_cont:"continuous_on UNIV (λx. Blinfun (?f'' x))"
by (simp add: continuous_on_const)
have truth:"(λx. Blinfun ((THE f'a. ∀x. ((λ_. dterm_sem I (σ f') ν) has_derivative f'a x) (at x)) x))
= (λx. Blinfun (λ _. 0))"
apply(rule ext)
apply(rule blinfun_eqI)
by (simp add: local.the_eq)
then show "continuous_on UNIV (λx. Blinfun ((THE f'a. ∀x. ((λ_. dterm_sem I (σ f') ν) has_derivative f'a x) (at x)) x))"
using truth
by (metis (mono_tags, lifting) blin_cont continuous_on_eq)
qed
done
done
subsection ‹Lemmas about adjoint interpretations›
lemma adjoint_consequence:"(⋀f f'. SFunctions σ f = Some f' ⟹ dsafe f') ⟹ (⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f') ⟹ Vagree ν ω (FVS σ) ⟹ adjoint I σ ν = adjoint I σ ω"
apply(unfold FVS_def)
apply(auto)
apply(unfold adjoint_def)
apply(rule interp_eq)
apply(auto simp add: fun_eq_iff)
subgoal for xa xaa
apply(cases "SFunctions σ xa")
apply(auto)
subgoal for a
proof -
assume safes:"(⋀f f'. SFunctions σ f = Some f' ⟹ dsafe f')"
assume agrees:"Vagree ν ω (⋃x. SFV σ x)"
assume some:"SFunctions σ xa = Some a"
from safes some have safe:"dsafe a" by auto
have sub:"SFV σ (Inl xa) ⊆ (⋃x. SFV σ x)"
by blast
from agrees
have "Vagree ν ω (SFV σ (Inl xa))"
using agree_sub[OF sub agrees] by auto
then have agree:"Vagree ν ω (FVT a)"
using some by auto
show "?thesis"
using coincidence_dterm[of a, OF safes[of xa a, OF some] agree] by auto
qed
done
subgoal for xa xaa
apply(cases "SPredicates σ xa")
apply(auto)
subgoal for a
proof -
assume safes:"(⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f')"
assume agrees:"Vagree ν ω (⋃x. SFV σ x)"
assume some:"SPredicates σ xa = Some a"
assume sem:"ν ∈ fml_sem ⦇Functions = case_sum (Functions I) (λf' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈
a"
from safes some have safe:"fsafe a" by auto
have sub:"SFV σ (Inr (Inr xa)) ⊆ (⋃x. SFV σ x)"
by blast
from agrees
have "Vagree ν ω (SFV σ (Inr (Inr xa)))"
using agree_sub[OF sub agrees] by auto
then have agree:"Vagree ν ω (FVF a)"
using some by auto
let ?I' = "⦇Functions = case_sum (Functions I) (λf' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈"
have IA:"⋀S. Iagree ?I' ?I' (SIGF a)" using Iagree_refl by auto
show "?thesis"
using coincidence_formula[of a, OF safes[of xa a, OF some] IA agree] sem by auto
qed
done
subgoal for xa xaa
apply(cases "SPredicates σ xa")
apply(auto)
subgoal for a
proof -
assume safes:"(⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f')"
assume agrees:"Vagree ν ω (⋃x. SFV σ x)"
assume some:"SPredicates σ xa = Some a"
assume sem:"ω ∈ fml_sem ⦇Functions = case_sum (Functions I) (λf' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈
a"
from safes some have safe:"fsafe a" by auto
have sub:"SFV σ (Inr (Inr xa)) ⊆ (⋃x. SFV σ x)"
by blast
from agrees
have "Vagree ν ω (SFV σ (Inr (Inr xa)))"
using agree_sub[OF sub agrees] by auto
then have agree:"Vagree ν ω (FVF a)"
using some by auto
let ?I' = "⦇Functions = case_sum (Functions I) (λf' _. xaa $ f'), Predicates = Predicates I, Contexts = Contexts I, Programs = Programs I,
ODEs = ODEs I, ODEBV = ODEBV I⦈"
have IA:"⋀S. Iagree ?I' ?I' (SIGF a)" using Iagree_refl by auto
show "?thesis"
using coincidence_formula[of a, OF safes[of xa a, OF some] IA agree] sem by auto
qed
done
done
lemma SIGT_plus1:"Vagree ν ω (⋃i∈SIGT (Plus t1 t2). case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})
⟹ Vagree ν ω (⋃i∈SIGT t1. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})"
unfolding Vagree_def by auto
lemma SIGT_plus2:"Vagree ν ω (⋃i∈SIGT (Plus t1 t2). case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})
⟹ Vagree ν ω (⋃i∈SIGT t2. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})"
unfolding Vagree_def by auto
lemma SIGT_times1:"Vagree ν ω (⋃i∈SIGT (Times t1 t2). case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})
⟹ Vagree ν ω (⋃i∈SIGT t1. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})"
unfolding Vagree_def by auto
lemma SIGT_times2:"Vagree ν ω (⋃i∈SIGT (Times t1 t2). case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})
⟹ Vagree ν ω (⋃i∈SIGT t2. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})"
unfolding Vagree_def by auto
lemma uadmit_sterm_adjoint':
assumes dsafe:"⋀f f'. SFunctions σ f = Some f' ⟹ dsafe f'"
assumes fsafe:"⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f'"
shows "Vagree ν ω (⋃i∈SIGT θ. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⟹ sterm_sem (adjoint I σ ν) θ = sterm_sem (adjoint I σ ω) θ"
proof (induct "θ")
case (Plus θ1 θ2)
assume IH1:"Vagree ν ω (⋃i∈SIGT θ1. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹ sterm_sem (local.adjoint I σ ν) θ1 = sterm_sem (local.adjoint I σ ω) θ1"
assume IH2:"Vagree ν ω (⋃i∈SIGT θ2. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹ sterm_sem (local.adjoint I σ ν) θ2 = sterm_sem (local.adjoint I σ ω) θ2"
assume VA:"Vagree ν ω (⋃i∈SIGT (Plus θ1 θ2). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
then show ?case
using IH1[OF SIGT_plus1[OF VA]] IH2[OF SIGT_plus2[OF VA]] by auto
next
case (Times θ1 θ2)
assume IH1:"Vagree ν ω (⋃i∈SIGT θ1. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹ sterm_sem (local.adjoint I σ ν) θ1 = sterm_sem (local.adjoint I σ ω) θ1"
assume IH2:"Vagree ν ω (⋃i∈SIGT θ2. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹ sterm_sem (local.adjoint I σ ν) θ2 = sterm_sem (local.adjoint I σ ω) θ2"
assume VA:"Vagree ν ω (⋃i∈SIGT (Times θ1 θ2). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
then show ?case
using IH1[OF SIGT_times1[OF VA]] IH2[OF SIGT_times2[OF VA]] by auto
next
case (Function x1a x2a)
assume IH:"⋀x. x ∈ range x2a ⟹ Vagree ν ω (⋃i∈SIGT x. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹
sterm_sem (local.adjoint I σ ν) x = sterm_sem (local.adjoint I σ ω) x"
from IH have IH':"⋀j. Vagree ν ω (⋃i∈SIGT (x2a j). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹
sterm_sem (local.adjoint I σ ν) (x2a j) = sterm_sem (local.adjoint I σ ω) (x2a j)"
using rangeI by auto
assume VA:"Vagree ν ω (⋃i∈SIGT ($f x1a x2a). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
from VA have VAs:"⋀j. Vagree ν ω (⋃i∈SIGT (x2a j). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
unfolding Vagree_def SIGT.simps using rangeI by blast
have SIGT:"x1a ∈ SIGT ($f x1a x2a)" by auto
have VAsub:"⋀a. SFunctions σ x1a = Some a ⟹ (FVT a) ⊆ (⋃i∈SIGT ($f x1a x2a). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
using SIGT by auto
have VAf:"⋀a. SFunctions σ x1a = Some a ⟹ Vagree ν ω (FVT a)"
using agree_sub[OF VAsub VA] by auto
then show ?case
using IH'[OF VAs] apply (auto simp add: fun_eq_iff)
apply(cases "SFunctions σ x1a")
defer
subgoal for x a
proof -
assume VA:"(⋀a. SFunctions σ x1a = Some a ⟹ Vagree ν ω (FVT a))"
assume sems:"(⋀j. ∀x. sterm_sem (local.adjoint I σ ν) (x2a j) x = sterm_sem (local.adjoint I σ ω) (x2a j) x)"
assume some:"SFunctions σ x1a = Some a"
note FVT = VAf[OF some]
have dsem:"⋀R . dterm_sem (extendf I R) a ν = dterm_sem (extendf I R) a ω"
using coincidence_dterm[OF dsafe[OF some] FVT] by auto
have "⋀R. Functions (local.adjoint I σ ν) x1a R = Functions (local.adjoint I σ ω) x1a R"
using dsem some unfolding adjoint_def by auto
then show "Functions (local.adjoint I σ ν) x1a (χ i. sterm_sem (local.adjoint I σ ω) (x2a i) x) =
Functions (local.adjoint I σ ω) x1a (χ i. sterm_sem (local.adjoint I σ ω) (x2a i) x)"
by auto
qed
unfolding adjoint_def apply auto
done
qed (auto)
lemma uadmit_sterm_adjoint:
assumes TUA:"TUadmit σ θ U"
assumes VA:"Vagree ν ω (-U)"
assumes dsafe:"⋀f f'. SFunctions σ f = Some f' ⟹ dsafe f'"
assumes fsafe:"⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f'"
shows "sterm_sem (adjoint I σ ν) θ = sterm_sem (adjoint I σ ω) θ"
proof -
have duh:"⋀A B. A ∩ B = {} ⟹ A ⊆ -B"
by auto
have "⋀x. x ∈ (⋃i∈SIGT θ. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⟹ x ∈ (-U)"
using TUA unfolding TUadmit_def by auto
then have sub1:"(⋃i∈SIGT θ. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ -U"
by auto
then have VA':"Vagree ν ω (⋃i∈SIGT θ. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})"
using agree_sub[OF sub1 VA] by auto
then show "?thesis" using uadmit_sterm_adjoint'[OF dsafe fsafe VA'] by auto
qed
lemma uadmit_sterm_ntadjoint':
assumes dsafe:"⋀i. dsafe (σ i)"
shows "Vagree ν ω ((⋃ i∈{i. Inr i ∈ SIGT θ}. FVT (σ i))) ⟹ sterm_sem (adjointFO I σ ν) θ = sterm_sem (adjointFO I σ ω) θ"
proof (induct "θ")
case (Plus θ1 θ2)
assume IH1:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ1}. FVT (σ i)) ⟹ sterm_sem (adjointFO I σ ν) θ1 = sterm_sem (adjointFO I σ ω) θ1"
assume IH2:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ2}. FVT (σ i)) ⟹ sterm_sem (adjointFO I σ ν) θ2 = sterm_sem (adjointFO I σ ω) θ2"
assume VA:"Vagree ν ω ((⋃ i∈{i. Inr i ∈ SIGT (Plus θ1 θ2)}. FVT (σ i)))"
from VA
have VA1:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ1}. FVT (σ i))"
and VA2:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ2}. FVT (σ i))" unfolding Vagree_def by auto
then show ?case
using IH1[OF VA1] IH2[OF VA2] by auto
next
case (Times θ1 θ2)
assume IH1:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ1}. FVT (σ i)) ⟹ sterm_sem (adjointFO I σ ν) θ1 = sterm_sem (adjointFO I σ ω) θ1"
assume IH2:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ2}. FVT (σ i)) ⟹ sterm_sem (adjointFO I σ ν) θ2 = sterm_sem (adjointFO I σ ω) θ2"
assume VA:"Vagree ν ω ((⋃ i∈{i. Inr i ∈ SIGT (Times θ1 θ2)}. FVT (σ i)))"
from VA
have VA1:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ1}. FVT (σ i))"
and VA2:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ2}. FVT (σ i))" unfolding Vagree_def by auto
then show ?case
using IH1[OF VA1] IH2[OF VA2] by auto
next
case (Function x1a x2a)
assume IH:"⋀x. x ∈ range x2a ⟹ Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT x}. FVT (σ i)) ⟹
sterm_sem (adjointFO I σ ν) x = sterm_sem (adjointFO I σ ω) x"
from IH have IH':"⋀j. Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT (x2a j)}. FVT (σ i)) ⟹
sterm_sem (adjointFO I σ ν) (x2a j) = sterm_sem (adjointFO I σ ω) (x2a j)"
using rangeI by auto
assume VA:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT ($f x1a x2a)}. FVT (σ i)) "
from VA have VAs:"⋀j. Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT (x2a j)}. FVT (σ i))"
unfolding Vagree_def SIGT.simps using rangeI by blast
have SIGT:"x1a ∈ SIGT ($f x1a x2a)" by auto
have VAsub:"⋀a. x1a = Inr a ⟹ (FVT (σ a)) ⊆ (⋃ i∈{i. Inr i ∈ SIGT ($f x1a x2a)}. FVT (σ i))"
using SIGT by auto
have VAf:"⋀a. x1a = Inr a ⟹Vagree ν ω (FVT (σ a))"
using agree_sub[OF VAsub VA] by auto
then show ?case
using IH'[OF VAs] apply (auto simp add: fun_eq_iff)
apply(cases "x1a")
defer
subgoal for x a
proof -
assume VA:"(⋀a. x1a = Inr a ⟹ Vagree ν ω (FVT (σ a)))"
assume sems:"(⋀j. ∀x. sterm_sem (adjointFO I σ ν) (x2a j) x = sterm_sem (adjointFO I σ ω) (x2a j) x)"
assume some:"x1a = Inr a"
note FVT = VAf[OF some]
from dsafe have dsafer:"⋀i. dsafe (σ i)" using dfree_is_dsafe by auto
have dsem:"dterm_sem I (σ a) ν = dterm_sem I (σ a) ω"
using coincidence_dterm[OF dsafer FVT] some by auto
then have "⋀R. Functions (adjointFO I σ ν) x1a R = Functions (adjointFO I σ ω) x1a R"
using some unfolding adjoint_def unfolding adjointFO_def by auto
then show "Functions (adjointFO I σ ν) x1a (χ i. sterm_sem (adjointFO I σ ω) (x2a i) x) =
Functions (adjointFO I σ ω) x1a (χ i. sterm_sem (adjointFO I σ ω) (x2a i) x)"
by auto
qed
unfolding adjointFO_def by auto
qed (auto)
lemma uadmit_sterm_ntadjoint:
assumes TUA:"NTUadmit σ θ U"
assumes VA:"Vagree ν ω (-U)"
assumes dsafe:"⋀i . dsafe (σ i)"
assumes good_interp:"is_interp I"
shows "sterm_sem (adjointFO I σ ν) θ = sterm_sem (adjointFO I σ ω) θ"
proof -
have duh:"⋀A B. A ∩ B = {} ⟹ A ⊆ -B"
by auto
have "⋀x. x ∈ ((⋃ i∈{i. Inr i ∈ SIGT θ}. FVT (σ i))) ⟹ x ∈ (-U)"
using TUA unfolding NTUadmit_def by auto
then have sub1:"(⋃i∈{i. Inr i ∈ SIGT θ}. FVT (σ i)) ⊆ -U"
by auto
then have VA':"Vagree ν ω (⋃i∈{i. Inr i ∈ SIGT θ}. FVT (σ i))"
using agree_sub[OF sub1 VA] by auto
then show "?thesis" using uadmit_sterm_ntadjoint'[OF dsafe VA'] by auto
qed
lemma uadmit_dterm_adjoint':
assumes dfree:"⋀f f'. SFunctions σ f = Some f' ⟹ dfree f'"
assumes fsafe:"⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f'"
assumes good_interp:"is_interp I"
shows "⋀ν ω. Vagree ν ω (⋃i∈SIGT θ. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⟹ dsafe θ ⟹ dterm_sem (adjoint I σ ν) θ = dterm_sem (adjoint I σ ω) θ"
proof (induct "θ")
case (Plus θ1 θ2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃i∈SIGT θ1. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹ dsafe θ1 ⟹ dterm_sem (local.adjoint I σ ν) θ1 = dterm_sem (local.adjoint I σ ω) θ1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃i∈SIGT θ2. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹ dsafe θ2 ⟹ dterm_sem (local.adjoint I σ ν) θ2 = dterm_sem (local.adjoint I σ ω) θ2"
assume VA:"Vagree ν ω (⋃i∈SIGT (Plus θ1 θ2). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
assume safe:"dsafe (Plus θ1 θ2)"
then show ?case
using IH1[OF SIGT_plus1[OF VA]] IH2[OF SIGT_plus2[OF VA]] by auto
next
case (Times θ1 θ2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃i∈SIGT θ1. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹ dsafe θ1 ⟹ dterm_sem (local.adjoint I σ ν) θ1 = dterm_sem (local.adjoint I σ ω) θ1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃i∈SIGT θ2. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹ dsafe θ2 ⟹ dterm_sem (local.adjoint I σ ν) θ2 = dterm_sem (local.adjoint I σ ω) θ2"
assume VA:"Vagree ν ω (⋃i∈SIGT (Times θ1 θ2). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
assume safe:"dsafe (Times θ1 θ2)"
then show ?case
using IH1[OF SIGT_times1[OF VA]] IH2[OF SIGT_times2[OF VA]] by auto
next
case (Function x1a x2a)
assume IH:"⋀x. ⋀ν ω. x ∈ range x2a ⟹ Vagree ν ω (⋃i∈SIGT x. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹
dsafe x ⟹ dterm_sem (local.adjoint I σ ν) x = dterm_sem (local.adjoint I σ ω) x"
assume safe:"dsafe (Function x1a x2a)"
from safe have safes:"⋀j. dsafe (x2a j)" by auto
from IH have IH':"⋀j. Vagree ν ω (⋃i∈SIGT (x2a j). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹
dterm_sem (local.adjoint I σ ν) (x2a j) = dterm_sem (local.adjoint I σ ω) (x2a j)"
using rangeI safes by auto
assume VA:"Vagree ν ω (⋃i∈SIGT ($f x1a x2a). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
from VA have VAs:"⋀j. Vagree ν ω (⋃i∈SIGT (x2a j). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
unfolding Vagree_def SIGT.simps using rangeI by blast
have SIGT:"x1a ∈ SIGT ($f x1a x2a)" by auto
have VAsub:"⋀a. SFunctions σ x1a = Some a ⟹ (FVT a) ⊆ (⋃i∈SIGT ($f x1a x2a). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
using SIGT by auto
have VAf:"⋀a. SFunctions σ x1a = Some a ⟹ Vagree ν ω (FVT a)"
using agree_sub[OF VAsub VA] by auto
then show ?case
using IH'[OF VAs] apply (auto simp add: fun_eq_iff)
apply(cases "SFunctions σ x1a")
defer
subgoal for x1 x2 a
proof -
assume VA:"(⋀a. SFunctions σ x1a = Some a ⟹ Vagree ν ω (FVT a))"
assume sems:"(⋀j. ∀x1 x2. dterm_sem (local.adjoint I σ ν) (x2a j) (x1,x2) = dterm_sem (local.adjoint I σ ω) (x2a j) (x1,x2))"
assume some:"SFunctions σ x1a = Some a"
note FVT = VAf[OF some]
have dsafe:"⋀f f'. SFunctions σ f = Some f' ⟹ dsafe f'"
using dfree dfree_is_dsafe by auto
have dsem:"⋀R . dterm_sem (extendf I R) a ν = dterm_sem (extendf I R) a ω"
using coincidence_dterm[OF dsafe[OF some] FVT] by auto
have "⋀R. Functions (local.adjoint I σ ν) x1a R = Functions (local.adjoint I σ ω) x1a R"
using dsem some unfolding adjoint_def by auto
then show "Functions (local.adjoint I σ ν) x1a (χ i. dterm_sem (local.adjoint I σ ω) (x2a i) (x1,x2)) =
Functions (local.adjoint I σ ω) x1a (χ i. dterm_sem (local.adjoint I σ ω) (x2a i) (x1,x2))"
by auto
qed
unfolding adjoint_def apply auto
done
next
case (Differential θ)
assume IH:"⋀ν ω. Vagree ν ω (⋃i∈SIGT θ. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {}) ⟹ dsafe θ ⟹ dterm_sem (local.adjoint I σ ν) θ = dterm_sem (local.adjoint I σ ω) θ"
assume VA:"Vagree ν ω (⋃i∈SIGT (Differential θ). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
assume safe:"dsafe (Differential θ)"
then have free:"dfree θ" by (auto dest: dsafe.cases)
from VA have VA':"Vagree ν ω (⋃i∈SIGT θ. case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
by auto
have dsafe:"⋀f f'. SFunctions σ f = Some f' ⟹ dsafe f'"
using dfree dfree_is_dsafe by auto
have sem:"sterm_sem (local.adjoint I σ ν) θ = sterm_sem (local.adjoint I σ ω) θ"
using uadmit_sterm_adjoint'[OF dsafe fsafe VA', of "λ x y. x" "λ x y. x" I] by auto
have good1:"is_interp (adjoint I σ ν)" using adjoint_safe[OF good_interp dfree] by auto
have good2:"is_interp (adjoint I σ ω)" using adjoint_safe[OF good_interp dfree] by auto
have frech:"frechet (local.adjoint I σ ν) θ = frechet (local.adjoint I σ ω) θ"
apply (auto simp add: fun_eq_iff)
subgoal for a b
using sterm_determines_frechet [OF good1 good2 free free sem, of "(a,b)"] by auto
done
then show "dterm_sem (local.adjoint I σ ν) (Differential θ) = dterm_sem (local.adjoint I σ ω) (Differential θ)"
by (auto simp add: directional_derivative_def)
qed (auto)
lemma uadmit_dterm_adjoint:
assumes TUA:"TUadmit σ θ U"
assumes VA:"Vagree ν ω (-U)"
assumes dfree:"⋀f f'. SFunctions σ f = Some f' ⟹ dfree f'"
assumes fsafe:"⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f'"
assumes dsafe:"dsafe θ"
assumes good_interp:"is_interp I"
shows "dterm_sem (adjoint I σ ν) θ = dterm_sem (adjoint I σ ω) θ"
proof -
have duh:"⋀A B. A ∩ B = {} ⟹ A ⊆ -B"
by auto
have "⋀x. x ∈ (⋃i∈SIGT θ. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⟹ x ∈ (-U)"
using TUA unfolding TUadmit_def by auto
then have sub1:"(⋃i∈SIGT θ. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ -U"
by auto
then have VA':"Vagree ν ω (⋃i∈SIGT θ. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})"
using agree_sub[OF sub1 VA] by auto
then show "?thesis" using uadmit_dterm_adjoint'[OF dfree fsafe good_interp VA' dsafe]
by auto
qed
lemma uadmit_dterm_ntadjoint':
assumes dfree:"⋀i. dsafe (σ i)"
assumes good_interp:"is_interp I"
shows "⋀ν ω. Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ}. FVT (σ i)) ⟹ dsafe θ ⟹ dterm_sem (adjointFO I σ ν) θ = dterm_sem (adjointFO I σ ω) θ"
proof (induct "θ")
case (Plus θ1 θ2 ν ω)
assume IH1:"⋀ν ω. Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ1}. FVT (σ i)) ⟹ dsafe θ1 ⟹ dterm_sem (adjointFO I σ ν) θ1 = dterm_sem (adjointFO I σ ω) θ1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ2}. FVT (σ i)) ⟹ dsafe θ2 ⟹ dterm_sem (adjointFO I σ ν) θ2 = dterm_sem (adjointFO I σ ω) θ2"
assume VA:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT (Plus θ1 θ2)}. FVT (σ i))"
then have VA1:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ1}. FVT (σ i))"
and VA2:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ2}. FVT (σ i))"
unfolding Vagree_def by auto
assume safe:"dsafe (Plus θ1 θ2)"
show ?case
using IH1[OF VA1] IH2[OF VA2] safe by auto
next
case (Times θ1 θ2 ν ω)
assume IH1:"⋀ν ω. Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ1}. FVT (σ i)) ⟹ dsafe θ1 ⟹ dterm_sem (adjointFO I σ ν) θ1 = dterm_sem (adjointFO I σ ω) θ1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ2}. FVT (σ i)) ⟹ dsafe θ2 ⟹ dterm_sem (adjointFO I σ ν) θ2 = dterm_sem (adjointFO I σ ω) θ2"
assume VA:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT (Times θ1 θ2)}. FVT (σ i))"
then have VA1:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ1}. FVT (σ i))"
and VA2:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ2}. FVT (σ i))"
unfolding Vagree_def by auto
assume safe:"dsafe (Times θ1 θ2)"
show ?case
using IH1[OF VA1] IH2[OF VA2] safe by auto
next
case (Function x1a x2a)
assume IH:"⋀x. ⋀ν ω. x ∈ range x2a ⟹ Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT x}. FVT (σ i)) ⟹
dsafe x ⟹ dterm_sem (adjointFO I σ ν) x = dterm_sem (adjointFO I σ ω) x"
assume safe:"dsafe (Function x1a x2a)"
from safe have safes:"⋀j. dsafe (x2a j)" by auto
from IH have IH':"⋀j. Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT (x2a j)}. FVT (σ i)) ⟹
dterm_sem (adjointFO I σ ν) (x2a j) = dterm_sem (adjointFO I σ ω) (x2a j)"
using rangeI safes by auto
assume VA:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT ($f x1a x2a)}. FVT (σ i))"
from VA have VAs:"⋀j. Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT (x2a j)}. FVT (σ i))"
unfolding Vagree_def SIGT.simps using rangeI by blast
have SIGT:"x1a ∈ SIGT ($f x1a x2a)" by auto
have VAsub:"⋀a. x1a = Inr a⟹ (FVT (σ a)) ⊆ (⋃ i∈{i. Inr i ∈ SIGT ($f x1a x2a)}. FVT (σ i))"
using SIGT by auto
have VAf:"⋀a. x1a = Inr a ⟹ Vagree ν ω (FVT (σ a))"
using agree_sub[OF VAsub VA] by auto
then show ?case
using IH'[OF VAs] apply (auto simp add: fun_eq_iff)
apply(cases "x1a")
defer
subgoal for x1 x2 a
proof -
assume VA:"(⋀a. x1a = Inr a ⟹ Vagree ν ω (FVT (σ a)))"
assume sems:"(⋀j. ∀x1 x2. dterm_sem (adjointFO I σ ν) (x2a j) (x1,x2) = dterm_sem (adjointFO I σ ω) (x2a j) (x1,x2))"
assume some:"x1a = Inr a"
note FVT = VAf[OF some]
have dsafe:"⋀i. dsafe (σ i)"
using dfree dfree_is_dsafe by auto
have dsem:"⋀R . dterm_sem I (σ a) ν = dterm_sem I (σ a) ω"
using coincidence_dterm[OF dsafe FVT] by auto
have "⋀R. Functions (adjointFO I σ ν) x1a R = Functions (adjointFO I σ ω) x1a R"
using dsem some unfolding adjointFO_def by auto
then show "Functions (adjointFO I σ ν) x1a (χ i. dterm_sem (adjointFO I σ ω) (x2a i) (x1,x2)) =
Functions (adjointFO I σ ω) x1a (χ i. dterm_sem (adjointFO I σ ω) (x2a i) (x1,x2))"
by auto
qed
unfolding adjointFO_def apply auto
done
next
case (Differential θ)
assume IH:"⋀ν ω. Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ}. FVT (σ i)) ⟹ dsafe θ ⟹ dterm_sem (adjointFO I σ ν) θ = dterm_sem (adjointFO I σ ω) θ"
assume VA:"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT (Differential θ)}. FVT (σ i))"
assume safe:"dsafe (Differential θ)"
then have free:"dfree θ" by (auto dest: dsafe.cases)
from VA have VA':"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ}. FVT (σ i))"
by auto
have dsafe:"⋀i. dsafe (σ i)"
using dfree dfree_is_dsafe by auto
have sem:"sterm_sem (adjointFO I σ ν) θ = sterm_sem (adjointFO I σ ω) θ"
using uadmit_sterm_ntadjoint'[OF dsafe VA'] by auto
have good1:"is_interp (adjointFO I σ ν)" using adjointFO_safe[OF good_interp dsafe, of "λi. i"] by auto
have good2:"is_interp (adjointFO I σ ω)" using adjointFO_safe[OF good_interp dsafe, of "λi. i"] by auto
have frech:"frechet (adjointFO I σ ν) θ = frechet (adjointFO I σ ω) θ"
apply (auto simp add: fun_eq_iff)
subgoal for a b
using sterm_determines_frechet [OF good1 good2 free free sem, of "(a,b)"] by auto
done
then show "dterm_sem (adjointFO I σ ν) (Differential θ) = dterm_sem (adjointFO I σ ω) (Differential θ)"
by (auto simp add: directional_derivative_def)
qed (auto)
lemma uadmit_dterm_ntadjoint:
assumes TUA:"NTUadmit σ θ U"
assumes VA:"Vagree ν ω (-U)"
assumes dfree:"⋀i . dsafe (σ i)"
assumes dsafe:"dsafe θ"
assumes good_interp:"is_interp I"
shows "dterm_sem (adjointFO I σ ν) θ = dterm_sem (adjointFO I σ ω) θ"
proof -
have duh:"⋀A B. A ∩ B = {} ⟹ A ⊆ -B"
by auto
have duh:"⋀A B. A ∩ B = {} ⟹ A ⊆ -B"
by auto
have "⋀x. x ∈ (⋃ i∈{i. Inr i ∈ SIGT θ}. FVT (σ i)) ⟹ x ∈ (-U)"
using TUA unfolding NTUadmit_def by auto
then have sub1:"(⋃ i∈{i. Inr i ∈ SIGT θ}. FVT (σ i)) ⊆ -U"
by auto
then have VA':"Vagree ν ω (⋃ i∈{i. Inr i ∈ SIGT θ}. FVT (σ i))"
using agree_sub[OF sub1 VA] by auto
then show "?thesis" using uadmit_dterm_ntadjoint'[OF dfree good_interp VA' dsafe]
by auto
qed
definition ssafe ::"('sf, 'sc, 'sz) subst ⇒ bool"
where "ssafe σ ≡
(∀ i f'. SFunctions σ i = Some f' ⟶ dfree f') ∧
(∀ f f'. SPredicates σ f = Some f' ⟶ fsafe f') ∧
(∀ f f'. SPrograms σ f = Some f' ⟶ hpsafe f') ∧
(∀ f f'. SODEs σ f = Some f' ⟶ osafe f') ∧
(∀ C C'. SContexts σ C = Some C' ⟶ fsafe C')"
lemma uadmit_dterm_adjointS:
assumes ssafe:"ssafe σ"
assumes good_interp:"is_interp I"
fixes ν ω
assumes VA:"Vagree ν ω (⋃i∈SIGT θ. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})"
assumes dsafe:"dsafe θ"
shows "dterm_sem (adjoint I σ ν) θ = dterm_sem (adjoint I σ ω) θ"
proof -
show "?thesis"
apply(rule uadmit_dterm_adjoint')
using good_interp ssafe VA dsafe unfolding ssafe_def by auto
qed
lemma adj_sub_assign_fact:"⋀i j e. i∈SIGT e ⟹ j ∈ (case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⟹ Inl i ∈({Inl x |x. x ∈ dom (SFunctions σ)} ∪ {Inr (Inl x) |x. x ∈ dom (SContexts σ)} ∪ {Inr (Inr x) |x. x ∈ dom (SPredicates σ)} ∪
{Inr (Inr x) |x. x ∈ dom (SPrograms σ)}) ∩
{Inl x |x. x ∈ SIGT e}"
unfolding SDom_def apply auto
subgoal for i j
apply (cases "SFunctions σ i")
by auto
done
lemma adj_sub_geq1_fact:"⋀i j x1 x2. i∈SIGT x1 ⟹ j ∈ (case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⟹ Inl i ∈({Inl x |x. x ∈ dom (SFunctions σ)} ∪ {Inr (Inl x) |x. x ∈ dom (SContexts σ)} ∪ {Inr (Inr x) |x. x ∈ dom (SPredicates σ)} ∪
{Inr (Inr x) |x. x ∈ dom (SPrograms σ)}) ∩
{Inl x |x. x ∈ SIGT x1 ∨ x ∈ SIGT x2}"
unfolding SDom_def apply auto
subgoal for i j
apply (cases "SFunctions σ i")
by auto
done
lemma adj_sub_geq2_fact:"⋀i j x1 x2. i∈SIGT x2 ⟹ j ∈ (case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⟹ Inl i ∈({Inl x |x. x ∈ dom (SFunctions σ)} ∪ {Inr (Inl x) |x. x ∈ dom (SContexts σ)} ∪ {Inr (Inr x) |x. x ∈ dom (SPredicates σ)} ∪
{Inr (Inr x) |x. x ∈ dom (SPrograms σ)}) ∩
{Inl x |x. x ∈ SIGT x1 ∨ x ∈ SIGT x2}"
unfolding SDom_def apply auto
subgoal for i j
apply (cases "SFunctions σ i")
by auto
done
lemma adj_sub_prop_fact:"⋀i j x1 x2 k. i∈SIGT (x2 k) ⟹ j ∈ (case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⟹ Inl i ∈({Inl x |x. x ∈ dom (SFunctions σ)} ∪ {Inr (Inl x) |x. x ∈ dom (SContexts σ)} ∪ {Inr (Inr x) |x. x ∈ dom (SPredicates σ)} ∪
{Inr (Inr x) |x. x ∈ dom (SPrograms σ)}) ∩
insert (Inr (Inr x1)) {Inl x |x. ∃xa. x ∈ SIGT (x2 xa)}"
unfolding SDom_def apply auto
subgoal for i j
apply (cases "SFunctions σ i")
by auto
done
lemma adj_sub_ode_fact:"⋀i j x1 x2. Inl i ∈ SIGO x1 ⟹ j ∈ (case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⟹ Inl i ∈({Inl x |x. x ∈ dom (SFunctions σ)} ∪ {Inr (Inl x) |x. x ∈ dom (SContexts σ)} ∪ {Inr (Inr x) |x. x ∈ dom (SPredicates σ)} ∪
{Inr (Inr x) |x. x ∈ dom (SPrograms σ)}) ∩
(SIGF x2 ∪ {Inl x |x. Inl x ∈ SIGO x1} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO x1})"
unfolding SDom_def apply auto
subgoal for i j
apply (cases "SFunctions σ i")
by auto
done
lemma adj_sub_assign:"⋀e σ x. (⋃i∈SIGT e. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ (⋃a∈SDom σ ∩ SIGP (x := e). SFV σ a)"
subgoal for e σ x
unfolding SDom_def apply auto
subgoal for i j
apply (cases "SFunctions σ j")
apply auto
subgoal for a
using adj_sub_assign_fact[of j e i]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
done
done
done
lemma adj_sub_diff_assign:"⋀e σ x. (⋃i∈SIGT e. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ (⋃a∈SDom σ ∩ SIGP (DiffAssign x e). SFV σ a)"
subgoal for e σ x
unfolding SDom_def apply auto
subgoal for i j
apply (cases "SFunctions σ j")
apply auto
subgoal for a
using adj_sub_assign_fact[of j e i]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
done
done
done
lemma adj_sub_geq1:"⋀σ x1 x2. (⋃i∈SIGT x1. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ (⋃a∈SDom σ ∩ SIGF (Geq x1 x2). SFV σ a)"
subgoal for σ x1 x2
unfolding SDom_def apply auto
subgoal for x i
apply (cases "SFunctions σ i")
apply auto
subgoal for a
using adj_sub_geq1_fact[of i x1 x σ]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
done
done
done
lemma adj_sub_geq2:"⋀σ x1 x2. (⋃i∈SIGT x2. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ (⋃a∈SDom σ ∩ SIGF (Geq x1 x2). SFV σ a)"
subgoal for σ x1 x2
unfolding SDom_def apply auto
subgoal for x i
apply (cases "SFunctions σ i")
apply auto
subgoal for a
using adj_sub_geq2_fact[of i x2 x σ]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
done
done
done
lemma adj_sub_prop:"⋀σ x1 x2 j . (⋃i∈SIGT (x2 j). case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ (⋃a∈SDom σ ∩ SIGF ($φ x1 x2). SFV σ a)"
subgoal for σ x1 x2 j
unfolding SDom_def apply auto
subgoal for x i
apply (cases "SFunctions σ i")
apply auto
subgoal for a
using adj_sub_prop_fact[of i x2 j x σ x1]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
done
done
done
lemma adj_sub_ode:"⋀σ x1 x2. (⋃i∈{i |i. Inl i ∈ SIGO x1}. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x) ⊆ (⋃a∈SDom σ ∩ SIGP (EvolveODE x1 x2). SFV σ a)"
subgoal for σ x1 x2
unfolding SDom_def apply auto
subgoal for x i
apply (cases "SFunctions σ i")
apply auto
subgoal for a
using adj_sub_ode_fact[of i x1 x σ x2]
by (metis (mono_tags, lifting) SFV.simps(1) option.simps(5))
done
done
done
lemma uadmit_ode_adjoint':
fixes σ I
assumes ssafe:"ssafe σ"
assumes good_interp:"is_interp I"
shows"⋀ν ω. Vagree ν ω (⋃i∈{i |i. Inl i ∈ SIGO ODE}. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x)⟹ osafe ODE ⟹ ODE_sem (adjoint I σ ν) ODE = ODE_sem (adjoint I σ ω) ODE"
proof (induction ODE)
case (OVar x)
then show ?case unfolding adjoint_def by auto
next
case (OSing x1a x2)
assume VA:"Vagree ν ω (⋃i∈{i |i. Inl i ∈ SIGO (OSing x1a x2)}. case SFunctions σ i of None ⇒ {} | Some a ⇒ FVT a)"
assume osafe:"osafe (OSing x1a x2)"
then have dfree:"dfree x2" by (auto dest: osafe.cases)
have safes:"(⋀f f'. SFunctions σ f = Some f' ⟹ dsafe f')"
"(⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f')"
using ssafe unfolding ssafe_def using dfree_is_dsafe by auto
have sem:"sterm_sem (local.adjoint I σ ν) x2 = sterm_sem (local.adjoint I σ ω) x2"
using uadmit_sterm_adjoint'[of σ ν ω x2 I, OF safes, of "(λ x y. x)" "(λ x y. x)"] VA
by auto
show ?case
apply auto
apply (rule ext)
subgoal for x
apply (rule vec_extensionality)
using sem by auto
done
next
case (OProd ODE1 ODE2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃i∈{i |i. Inl i ∈ SIGO ODE1}. case SFunctions σ i of None ⇒ {} | Some a ⇒ FVT a) ⟹
osafe ODE1 ⟹ ODE_sem (local.adjoint I σ ν) ODE1 = ODE_sem (local.adjoint I σ ω) ODE1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃i∈{i |i. Inl i ∈ SIGO ODE2}. case SFunctions σ i of None ⇒ {} | Some a ⇒ FVT a) ⟹
osafe ODE2 ⟹ ODE_sem (local.adjoint I σ ν) ODE2 = ODE_sem (local.adjoint I σ ω) ODE2"
assume VA:"Vagree ν ω (⋃i∈{i |i. Inl i ∈ SIGO (OProd ODE1 ODE2)}. case SFunctions σ i of None ⇒ {} | Some a ⇒ FVT a)"
assume safe:"osafe (OProd ODE1 ODE2)"
from safe have safe1:"osafe ODE1" and safe2:"osafe ODE2" by (auto dest: osafe.cases)
have sub1:"(⋃i∈{i |i. Inl i ∈ SIGO ODE1}. case SFunctions σ i of None ⇒ {} | Some a ⇒ FVT a) ⊆ (⋃i∈{i |i. Inl i ∈ SIGO (OProd ODE1 ODE2)}. case SFunctions σ i of None ⇒ {} | Some a ⇒ FVT a)"
by auto
have sub2:"(⋃i∈{i |i. Inl i ∈ SIGO ODE2}. case SFunctions σ i of None ⇒ {} | Some a ⇒ FVT a) ⊆ (⋃i∈{i |i. Inl i ∈ SIGO (OProd ODE1 ODE2)}. case SFunctions σ i of None ⇒ {} | Some a ⇒ FVT a)"
by auto
then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
qed
lemma uadmit_ode_ntadjoint':
fixes σ I
assumes ssafe:"⋀i. dsafe (σ i)"
assumes good_interp:"is_interp I"
shows"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGO ODE}. FVT (σ y)) ⟹ osafe ODE ⟹ ODE_sem (adjointFO I σ ν) ODE = ODE_sem (adjointFO I σ ω) ODE"
proof (induction ODE)
case (OVar x)
then show ?case unfolding adjointFO_def by auto
next
case (OSing x1a x2)
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGO (OSing x1a x2)}. FVT (σ y))"
assume osafe:"osafe (OSing x1a x2)"
then have dfree:"dfree x2" by (auto dest: osafe.cases)
have sem:"sterm_sem (adjointFO I σ ν) x2 = sterm_sem (adjointFO I σ ω) x2"
using uadmit_sterm_ntadjoint'[of σ ν ω x2 I, OF ssafe] VA
by auto
show ?case
apply auto
apply (rule ext)
subgoal for x
apply (rule vec_extensionality)
using sem by auto
done
next
case (OProd ODE1 ODE2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGO ODE1}. FVT (σ y)) ⟹
osafe ODE1 ⟹ ODE_sem (adjointFO I σ ν) ODE1 = ODE_sem (adjointFO I σ ω) ODE1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGO ODE2}. FVT (σ y)) ⟹
osafe ODE2 ⟹ ODE_sem (adjointFO I σ ν) ODE2 = ODE_sem (adjointFO I σ ω) ODE2"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGO (OProd ODE1 ODE2)}. FVT (σ y))"
assume safe:"osafe (OProd ODE1 ODE2)"
from safe have safe1:"osafe ODE1" and safe2:"osafe ODE2" by (auto dest: osafe.cases)
have sub1:"(⋃y∈{y. Inl (Inr y) ∈ SIGO ODE1}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGO (OProd ODE1 ODE2)}. FVT (σ y))"
by auto
have sub2:"(⋃y∈{y. Inl (Inr y) ∈ SIGO ODE2}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGO (OProd ODE1 ODE2)}. FVT (σ y))"
by auto
then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
qed
lemma adjoint_ode_vars:
shows "ODE_vars (local.adjoint I σ ν) ODE = ODE_vars (local.adjoint I σ ω) ODE"
apply(induction ODE)
unfolding adjoint_def by auto
lemma uadmit_mkv_adjoint:
assumes ssafe:"ssafe σ"
assumes good_interp:"is_interp I"
assumes VA:"Vagree ν ω (⋃i ∈ {i | i. (Inl i∈SIGO ODE)}. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {})"
assumes osafe:"osafe ODE"
shows "mk_v (adjoint I σ ν) ODE = mk_v (adjoint I σ ω) ODE"
apply(rule ext)
subgoal for R
apply(rule ext)
subgoal for solt
apply(rule agree_UNIV_eq)
using mk_v_agree[of "(adjoint I σ ν)" ODE "R" solt]
using mk_v_agree[of "(adjoint I σ ω)" ODE "R" solt]
using uadmit_ode_adjoint'[OF ssafe good_interp VA osafe]
unfolding Vagree_def
apply auto
subgoal for i
apply (cases "Inl i ∈ Inl ` ODE_vars (adjoint I σ ω) ODE")
proof -
assume sem_eq:"ODE_sem (local.adjoint I σ ν) ODE = ODE_sem (local.adjoint I σ ω) ODE"
have vars_eq:"ODE_vars (local.adjoint I σ ν) ODE = ODE_vars (local.adjoint I σ ω) ODE"
apply(induction ODE)
unfolding adjoint_def by auto
assume thing1:"
∀i. (Inl i ∈ Inl ` ODE_vars (local.adjoint I σ ν) ODE ⟶ fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = solt $ i) ∧
(Inl i ∈ Inr ` ODE_vars (local.adjoint I σ ν) ODE ⟶ fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = solt $ i)"
assume thing2:"
∀i. (Inl i ∈ Inl ` ODE_vars (local.adjoint I σ ω) ODE ⟶ fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i = solt $ i) ∧
(Inl i ∈ Inr ` ODE_vars (local.adjoint I σ ω) ODE ⟶ fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i = solt $ i)"
assume inl:"Inl i ∈ Inl ` ODE_vars (local.adjoint I σ ω) ODE"
from thing1 and inl have eq1: "fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = solt $ i"
using vars_eq by auto
from thing2 and inl have eq2: "fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i = solt $ i"
using vars_eq by auto
show "fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i"
using eq1 eq2 by auto
next
assume sem_eq:"ODE_sem (local.adjoint I σ ν) ODE = ODE_sem (local.adjoint I σ ω) ODE"
assume thing1:"∀i. Inl i ∉ Inl ` ODE_vars (local.adjoint I σ ν) ODE ∧ Inl i ∉ Inr ` ODE_vars (local.adjoint I σ ν) ODE ⟶
fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = fst R $ i"
assume thing2:"∀i. Inl i ∉ Inl ` ODE_vars (local.adjoint I σ ω) ODE ∧ Inl i ∉ Inr ` ODE_vars (local.adjoint I σ ω) ODE ⟶
fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i = fst R $ i"
assume inl:"Inl i ∉ Inl ` ODE_vars (local.adjoint I σ ω) ODE"
have vars_eq:"ODE_vars (local.adjoint I σ ν) ODE = ODE_vars (local.adjoint I σ ω) ODE"
apply(induction ODE)
unfolding adjoint_def by auto
from thing1 and inl have eq1: "fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = fst R $ i"
using vars_eq by auto
from thing2 and inl have eq2: "fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i = fst R $ i"
using vars_eq by auto
show "fst (mk_v (local.adjoint I σ ν) ODE R solt) $ i = fst (mk_v (local.adjoint I σ ω) ODE R solt) $ i"
using eq1 eq2 by auto
qed
subgoal for i
apply (cases "Inr i ∈ Inr ` ODE_vars (adjoint I σ ω) ODE")
proof -
assume sem_eq:"ODE_sem (local.adjoint I σ ν) ODE = ODE_sem (local.adjoint I σ ω) ODE"
assume thing1:"∀i. (Inr i ∈ Inl ` ODE_vars (local.adjoint I σ ν) ODE ⟶
snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = ODE_sem (local.adjoint I σ ω) ODE solt $ i) ∧
(Inr i ∈ Inr ` ODE_vars (local.adjoint I σ ν) ODE ⟶
snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = ODE_sem (local.adjoint I σ ω) ODE solt $ i)"
assume thing2:"∀i. (Inr i ∈ Inl ` ODE_vars (local.adjoint I σ ω) ODE ⟶
snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i = ODE_sem (local.adjoint I σ ω) ODE solt $ i) ∧
(Inr i ∈ Inr ` ODE_vars (local.adjoint I σ ω) ODE ⟶
snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i = ODE_sem (local.adjoint I σ ω) ODE solt $ i)"
assume inr:"Inr i ∈ Inr ` ODE_vars (local.adjoint I σ ω) ODE"
have vars_eq:"ODE_vars (local.adjoint I σ ν) ODE = ODE_vars (local.adjoint I σ ω) ODE"
apply(induction ODE)
unfolding adjoint_def by auto
show "snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i"
using thing1 thing2 vars_eq inr by auto
next
assume sem_eq:"ODE_sem (local.adjoint I σ ν) ODE = ODE_sem (local.adjoint I σ ω) ODE"
assume thing1:"∀i. Inr i ∉ Inl ` ODE_vars (local.adjoint I σ ν) ODE ∧ Inr i ∉ Inr ` ODE_vars (local.adjoint I σ ν) ODE ⟶
snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = snd R $ i"
assume thing2:"∀i. Inr i ∉ Inl ` ODE_vars (local.adjoint I σ ω) ODE ∧ Inr i ∉ Inr ` ODE_vars (local.adjoint I σ ω) ODE ⟶
snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i = snd R $ i"
assume inr:"Inr i ∉ Inr ` ODE_vars (local.adjoint I σ ω) ODE"
have vars_eq:"ODE_vars (local.adjoint I σ ν) ODE = ODE_vars (local.adjoint I σ ω) ODE"
apply(induction ODE)
unfolding adjoint_def by auto
have eq1:"snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = snd R $ i"
using thing1 sem_eq vars_eq inr by auto
have eq2:"snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i = snd R $ i"
using thing2 sem_eq vars_eq inr by auto
show "snd (mk_v (local.adjoint I σ ν) ODE R solt) $ i = snd (mk_v (local.adjoint I σ ω) ODE R solt) $ i"
using eq1 eq2 by auto
qed
done
done
done
lemma adjointFO_ode_vars:
shows "ODE_vars (adjointFO I σ ν) ODE = ODE_vars (adjointFO I σ ω) ODE"
apply(induction ODE)
unfolding adjointFO_def by auto
lemma uadmit_mkv_ntadjoint:
assumes ssafe:"⋀i. dsafe (σ i)"
assumes good_interp:"is_interp I"
assumes VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGO ODE}. FVT (σ y))"
assumes osafe:"osafe ODE"
shows "mk_v (adjointFO I σ ν) ODE = mk_v (adjointFO I σ ω) ODE"
apply(rule ext)
subgoal for R
apply(rule ext)
subgoal for solt
apply(rule agree_UNIV_eq)
using mk_v_agree[of "(adjointFO I σ ν)" ODE "R" solt]
using mk_v_agree[of "(adjointFO I σ ω)" ODE "R" solt]
using uadmit_ode_ntadjoint'[OF ssafe good_interp VA osafe]
unfolding Vagree_def
apply auto
using adjointFO_ode_vars by metis+
done
done
lemma uadmit_prog_fml_adjoint':
fixes σ I
assumes ssafe:"ssafe σ"
assumes good_interp:"is_interp I"
shows "⋀ν ω. Vagree ν ω (⋃x∈SDom σ ∩ SIGP α. SFV σ x) ⟹ hpsafe α ⟹ prog_sem (adjoint I σ ν) α = prog_sem (adjoint I σ ω) α"
and "⋀ν ω. Vagree ν ω (⋃x∈SDom σ ∩ SIGF φ. SFV σ x) ⟹ fsafe φ ⟹ fml_sem (adjoint I σ ν) φ = fml_sem (adjoint I σ ω) φ"
proof (induct "α" and "φ")
case (Pvar x)
then show ?case unfolding adjoint_def by auto
next
case (Assign x e)
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGP (x := e). SFV σ a)"
assume safe:"hpsafe (x := e)"
from safe have dsafe:"dsafe e" by (auto dest: hpsafe.cases)
have sub:"(⋃i∈SIGT e. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ (⋃a∈SDom σ ∩ SIGP (x := e). SFV σ a)"
using adj_sub_assign[of σ e x] by auto
have "dterm_sem (local.adjoint I σ ν) e = dterm_sem (local.adjoint I σ ω) e"
by (rule uadmit_dterm_adjointS[OF ssafe good_interp agree_sub[OF sub VA] dsafe])
then show ?case by (auto simp add: vec_eq_iff)
next
case (DiffAssign x e)
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGP (DiffAssign x e). SFV σ a)"
assume safe:"hpsafe (DiffAssign x e)"
from safe have dsafe:"dsafe e" by (auto dest: hpsafe.cases)
have sub:"(⋃i∈SIGT e. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ (⋃a∈SDom σ ∩ SIGP (DiffAssign x e). SFV σ a)"
using adj_sub_diff_assign[of σ e] by auto
have "dterm_sem (local.adjoint I σ ν) e = dterm_sem (local.adjoint I σ ω) e"
by (rule uadmit_dterm_adjointS[OF ssafe good_interp agree_sub[OF sub VA] dsafe])
then show ?case by (auto simp add: vec_eq_iff)
next
case (Test x)
assume IH:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGF x. SFV σ a) ⟹ fsafe x ⟹ fml_sem (adjoint I σ ν) x = fml_sem (adjoint I σ ω) x"
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGP (? x). SFV σ a)"
assume hpsafe:"hpsafe (? x)"
then have fsafe:"fsafe x" by (auto dest: hpsafe.cases)
have sub:"(⋃a∈SDom σ ∩ SIGF x. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGP (? x). SFV σ a)"
by auto
have "fml_sem (adjoint I σ ν) x = fml_sem (adjoint I σ ω) x"
using IH[OF agree_sub[OF sub VA] fsafe] by auto
then show ?case by auto
next
case (EvolveODE x1 x2)
assume IH:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGF x2. SFV σ a) ⟹ fsafe x2 ⟹ fml_sem (local.adjoint I σ ν) x2 = fml_sem (local.adjoint I σ ω) x2"
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGP (EvolveODE x1 x2). SFV σ a)"
assume safe:"hpsafe (EvolveODE x1 x2)"
then have osafe:"osafe x1" and fsafe:"fsafe x2" by (auto dest: hpsafe.cases)
have sub1:"(⋃a∈SDom σ ∩ SIGF x2. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGP (EvolveODE x1 x2). SFV σ a)"
by auto
then have VAF:"Vagree ν ω (⋃a∈SDom σ ∩ SIGF x2. SFV σ a)"
using agree_sub[OF sub1 VA] by auto
note IH' = IH[OF VAF fsafe]
have sub:"(⋃i∈{i |i. Inl i ∈ SIGO x1}. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x) ⊆ (⋃a∈SDom σ ∩ SIGP (EvolveODE x1 x2). SFV σ a)"
using adj_sub_ode[of σ x1 x2] by auto
moreover have IH2:"ODE_sem (local.adjoint I σ ν) x1 = ODE_sem (local.adjoint I σ ω) x1"
apply (rule uadmit_ode_adjoint')
subgoal by (rule ssafe)
subgoal by (rule good_interp)
subgoal using agree_sub[OF sub VA] by auto
subgoal by (rule osafe)
done
have mkv:"mk_v (adjoint I σ ν) x1 = mk_v (adjoint I σ ω) x1"
apply (rule uadmit_mkv_adjoint)
using ssafe good_interp osafe agree_sub[OF sub VA] by auto
show ?case
apply auto
subgoal for aa ba bb sol t
apply(rule exI[where x = sol])
apply(rule conjI)
subgoal by auto
apply(rule exI[where x=t])
apply(rule conjI)
subgoal using mkv by auto
apply(rule conjI)
subgoal by auto using IH2 mkv IH' by auto
subgoal for aa ba bb sol t
apply(rule exI[where x = sol])
apply(rule conjI)
subgoal by auto
apply(rule exI[where x=t])
apply(rule conjI)
subgoal using mkv by auto
apply(rule conjI)
subgoal by auto using IH2 mkv IH' by auto
done
next
case (Choice x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGP x1. SFV σ a) ⟹ hpsafe x1 ⟹ prog_sem (local.adjoint I σ ν) x1 = prog_sem (local.adjoint I σ ω) x1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGP x2. SFV σ a) ⟹ hpsafe x2 ⟹ prog_sem (local.adjoint I σ ν) x2 = prog_sem (local.adjoint I σ ω) x2"
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGP (x1 ∪∪ x2). SFV σ a)"
assume safe:"hpsafe (x1 ∪∪ x2)"
from safe have
safe1:"hpsafe x1"
and safe2:"hpsafe x2"
by (auto dest: hpsafe.cases)
have sub1:"(⋃a∈SDom σ ∩ SIGP x1. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGP (x1 ∪∪ x2). SFV σ a)"
by auto
have sub2:"(⋃a∈SDom σ ∩ SIGP x2. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGP (x1 ∪∪ x2). SFV σ a)"
by auto
then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
case (Sequence x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGP x1. SFV σ a) ⟹ hpsafe x1 ⟹ prog_sem (local.adjoint I σ ν) x1 = prog_sem (local.adjoint I σ ω) x1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGP x2. SFV σ a) ⟹ hpsafe x2 ⟹ prog_sem (local.adjoint I σ ν) x2 = prog_sem (local.adjoint I σ ω) x2"
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGP (x1 ;; x2). SFV σ a)"
assume safe:"hpsafe (x1 ;; x2)"
from safe have
safe1:"hpsafe x1"
and safe2:"hpsafe x2"
by (auto dest: hpsafe.cases)
have sub1:"(⋃a∈SDom σ ∩ SIGP x1. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGP (x1 ;; x2). SFV σ a)"
by auto
have sub2:"(⋃a∈SDom σ ∩ SIGP x2. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGP (x1 ;; x2). SFV σ a)"
by auto
then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
case (Loop x)
assume IH:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGP x. SFV σ a) ⟹ hpsafe x ⟹ prog_sem (local.adjoint I σ ν) x = prog_sem (local.adjoint I σ ω) x"
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGP (x**). SFV σ a)"
assume safe:"hpsafe (x**)"
from safe have
safe:"hpsafe x"
by (auto dest: hpsafe.cases)
have sub:"(⋃a∈SDom σ ∩ SIGP x. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGP (x**). SFV σ a)"
by auto
show ?case using IH[OF agree_sub[OF sub VA] safe] by auto
next
case (Geq x1 x2)
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGF (Geq x1 x2). SFV σ a)"
assume safe:"fsafe (Geq x1 x2)"
then have dsafe1:"dsafe x1" and dsafe2:"dsafe x2" by (auto dest: fsafe.cases)
have sub1:"(⋃i∈SIGT x1. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ (⋃a∈SDom σ ∩ SIGF (Geq x1 x2). SFV σ a)"
using adj_sub_geq1[of σ x1 x2] by auto
have sub2:"(⋃i∈SIGT x2. case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ (⋃a∈SDom σ ∩ SIGF (Geq x1 x2). SFV σ a)"
using adj_sub_geq2[of σ x2 x1] by auto
have "dterm_sem (local.adjoint I σ ν) x1 = dterm_sem (local.adjoint I σ ω) x1"
by (rule uadmit_dterm_adjointS[OF ssafe good_interp agree_sub[OF sub1 VA] dsafe1])
moreover have "dterm_sem (local.adjoint I σ ν) x2 = dterm_sem (local.adjoint I σ ω) x2"
by (rule uadmit_dterm_adjointS[OF ssafe good_interp agree_sub[OF sub2 VA] dsafe2])
ultimately show ?case by auto
next
case (Prop x1 x2 ν ω)
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGF ($φ x1 x2). SFV σ a)"
assume safe:"fsafe ($φ x1 x2)"
then have safes:"⋀i. dsafe (x2 i)" using dfree_is_dsafe by auto
have subs:"⋀j. (⋃i∈SIGT (x2 j). case SFunctions σ i of Some x ⇒ FVT x | None ⇒ {}) ⊆ (⋃a∈SDom σ ∩ SIGF ($φ x1 x2). SFV σ a)"
subgoal for j using adj_sub_prop[of σ x2 j x1] by auto
done
have "⋀i. dterm_sem (local.adjoint I σ ν) (x2 i) = dterm_sem (local.adjoint I σ ω) (x2 i)"
by (rule uadmit_dterm_adjointS[OF ssafe good_interp agree_sub[OF subs VA] safes])
then have vec_eq:"⋀R. (χ i. dterm_sem (local.adjoint I σ ν) (x2 i) R) = (χ i. dterm_sem (local.adjoint I σ ω) (x2 i) R)"
by (auto simp add: vec_eq_iff)
from VA have VAs:"⋀j. Vagree ν ω (⋃i∈SIGT (x2 j). case SFunctions σ i of Some a ⇒ FVT a | None ⇒ {})"
unfolding Vagree_def SIGT.simps using rangeI
by (metis (no_types, lifting) subsetD subs)
have SIGF:"⋀a. SPredicates σ x1 = Some a ⟹ Inr (Inr x1) ∈ SDom σ ∩ SIGF ($φ x1 x2)" unfolding SDom_def
by auto
have VAsub:"⋀a. SPredicates σ x1 = Some a ⟹ (FVF a) ⊆ (⋃i∈SDom σ ∩ SIGF ($φ x1 x2). SFV σ i)"
using SIGF by auto
have VAf:"⋀a. SPredicates σ x1 = Some a ⟹ Vagree ν ω (FVF a)"
using agree_sub[OF VAsub VA] by auto
then show ?case
apply(cases "SPredicates σ x1")
defer
subgoal for a
proof -
assume some:"SPredicates σ x1 = Some a"
note FVF = VAf[OF some]
have dsafe:"⋀f f'. SFunctions σ f = Some f' ⟹ dsafe f'"
using ssafe dfree_is_dsafe unfolding ssafe_def by auto
have dsem:"⋀R . (ν ∈ fml_sem (extendf I R) a) = (ω ∈ fml_sem (extendf I R) a)"
subgoal for R
apply (rule coincidence_formula)
subgoal using ssafe unfolding ssafe_def using some by auto
subgoal unfolding Iagree_def by auto
subgoal by (rule FVF)
done
done
have pred_eq:"⋀R. Predicates (local.adjoint I σ ν) x1 R = Predicates (local.adjoint I σ ω) x1 R"
using dsem some unfolding adjoint_def by auto
show "fml_sem (local.adjoint I σ ν) ($φ x1 x2) = fml_sem (local.adjoint I σ ω) ($φ x1 x2)"
apply auto
subgoal for a b using pred_eq[of "(χ i. dterm_sem (local.adjoint I σ ν) (x2 i) (a, b))"] vec_eq by auto
subgoal for a b using pred_eq[of "(χ i. dterm_sem (local.adjoint I σ ν) (x2 i) (a, b))"] vec_eq by auto
done
qed
unfolding adjoint_def using local.adjoint_def local.vec_eq apply auto
done
next
case (Not x)
assume IH:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGF x. SFV σ a) ⟹ fsafe x ⟹ fml_sem (local.adjoint I σ ν) x = fml_sem (local.adjoint I σ ω) x"
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGF (Not x). SFV σ a)"
assume safe:"fsafe (Not x)"
from safe have
safe:"fsafe x"
by (auto dest: fsafe.cases)
have sub:"(⋃a∈SDom σ ∩ SIGF x. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGF (Not x). SFV σ a)"
by auto
show ?case using IH[OF agree_sub[OF sub VA] safe] by auto
next
case (And x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGF x1. SFV σ a) ⟹ fsafe x1 ⟹ fml_sem (local.adjoint I σ ν) x1 = fml_sem (local.adjoint I σ ω) x1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGF x2. SFV σ a) ⟹ fsafe x2 ⟹ fml_sem (local.adjoint I σ ν) x2 = fml_sem (local.adjoint I σ ω) x2"
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGF (And x1 x2). SFV σ a)"
assume safe:"fsafe (And x1 x2)"
from safe have
safe1:"fsafe x1"
and safe2:"fsafe x2"
by (auto dest: fsafe.cases)
have sub1:"(⋃a∈SDom σ ∩ SIGF x1. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGF (And x1 x2). SFV σ a)"
by auto
have sub2:"(⋃a∈SDom σ ∩ SIGF x2. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGF (And x1 x2). SFV σ a)"
by auto
show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
case (Exists x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGF x2. SFV σ a) ⟹ fsafe x2 ⟹ fml_sem (local.adjoint I σ ν) x2 = fml_sem (local.adjoint I σ ω) x2"
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGF (Exists x1 x2). SFV σ a)"
assume safe:"fsafe (Exists x1 x2)"
from safe have safe1:"fsafe x2"
by (auto dest: fsafe.cases)
have sub1:"(⋃a∈SDom σ ∩ SIGF x2. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGF (Exists x1 x2). SFV σ a)"
by auto
show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] by auto
next
case (Diamond x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGP x1. SFV σ a) ⟹ hpsafe x1 ⟹ prog_sem (local.adjoint I σ ν) x1 = prog_sem (local.adjoint I σ ω) x1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGF x2. SFV σ a) ⟹ fsafe x2 ⟹ fml_sem (local.adjoint I σ ν) x2 = fml_sem (local.adjoint I σ ω) x2"
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGF (Diamond x1 x2). SFV σ a)"
assume safe:"fsafe (Diamond x1 x2)"
from safe have
safe1:"hpsafe x1"
and safe2:"fsafe x2"
by (auto dest: fsafe.cases)
have sub1:"(⋃a∈SDom σ ∩ SIGP x1. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGF (Diamond x1 x2). SFV σ a)"
by auto
have sub2:"(⋃a∈SDom σ ∩ SIGF x2. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGF (Diamond x1 x2). SFV σ a)"
by auto
show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
case (InContext x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃a∈SDom σ ∩ SIGF x2. SFV σ a) ⟹ fsafe x2 ⟹ fml_sem (local.adjoint I σ ν) x2 = fml_sem (local.adjoint I σ ω) x2"
assume VA:"Vagree ν ω (⋃a∈SDom σ ∩ SIGF (InContext x1 x2). SFV σ a)"
assume safe:"fsafe (InContext x1 x2)"
from safe have safe1:"fsafe x2"
by (auto dest: fsafe.cases)
have sub:"(⋃a∈SDom σ ∩ SIGF x2. SFV σ a) ⊆ (⋃a∈SDom σ ∩ SIGF (InContext x1 x2). SFV σ a)"
by auto
show ?case using IH1[OF agree_sub[OF sub VA] safe1]
unfolding adjoint_def by auto
qed
lemma uadmit_prog_adjoint:
assumes PUA:"PUadmit σ a U"
assumes VA:"Vagree ν ω (-U)"
assumes hpsafe:"hpsafe a"
assumes ssafe:"ssafe σ"
assumes good_interp:"is_interp I"
shows "prog_sem (adjoint I σ ν) a = prog_sem (adjoint I σ ω) a"
proof -
have sub:"(⋃x∈SDom σ ∩ SIGP a. SFV σ x) ⊆ -U" using PUA unfolding PUadmit_def by auto
have VA':"Vagree ν ω (⋃x∈SDom σ ∩ SIGP a. SFV σ x)" using agree_sub[OF sub VA] by auto
show ?thesis
apply(rule uadmit_prog_fml_adjoint'[OF ssafe good_interp])
subgoal by (rule VA')
subgoal by (rule hpsafe)
done
qed
lemma uadmit_fml_adjoint:
assumes FUA:"FUadmit σ φ U"
assumes VA:"Vagree ν ω (-U)"
assumes fsafe:"fsafe φ"
assumes ssafe:"ssafe σ"
assumes good_interp:"is_interp I"
shows "fml_sem (adjoint I σ ν) φ = fml_sem (adjoint I σ ω) φ"
proof -
have sub:"(⋃x∈SDom σ ∩ SIGF φ. SFV σ x) ⊆ -U" using FUA unfolding FUadmit_def by auto
have VA':"Vagree ν ω (⋃x∈SDom σ ∩ SIGF φ. SFV σ x)" using agree_sub[OF sub VA] by auto
show ?thesis
apply(rule uadmit_prog_fml_adjoint'[OF ssafe good_interp])
subgoal by (rule VA')
subgoal by (rule fsafe)
done
qed
lemma ntadj_sub_assign:"⋀e σ x. (⋃y∈{y. Inr y ∈ SIGT e}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (Assign x e)}. FVT (σ y))"
by auto
lemma ntadj_sub_diff_assign:"⋀e σ x. (⋃y∈{y. Inl y ∈ SIGT e}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inl y) ∈ SIGP (DiffAssign x e)}. FVT (σ y))"
by auto
lemma ntadj_sub_geq1:"⋀σ x1 x2. (⋃y∈{y. Inl y ∈ SIGT x1}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inl y) ∈ SIGF (Geq x1 x2)}. FVT (σ y))"
by auto
lemma ntadj_sub_geq2:"⋀σ x1 x2. (⋃y∈{y. Inl y ∈ SIGT x2}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inl y) ∈ SIGF (Geq x1 x2)}. FVT (σ y))"
by auto
lemma ntadj_sub_prop:"⋀σ x1 x2 j. (⋃y∈{y. Inl y ∈ SIGT (x2 j)}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inl y) ∈ SIGF ($φ x1 x2)}.FVT (σ y))"
by auto
lemma ntadj_sub_ode:"⋀σ x1 x2. (⋃y∈{y. Inl (Inl y) ∈ SIGO x1}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inl y) ∈ SIGP (EvolveODE x1 x2)}. FVT (σ y))"
by auto
lemma uadmit_prog_fml_ntadjoint':
fixes σ I
assumes ssafe:"⋀i. dsafe (σ i)"
assumes good_interp:"is_interp I"
shows "⋀ν ω. Vagree ν ω (⋃x∈{x. Inl (Inr x) ∈ SIGP α}. FVT (σ x)) ⟹ hpsafe α ⟹ prog_sem (adjointFO I σ ν) α = prog_sem (adjointFO I σ ω) α"
and "⋀ν ω. Vagree ν ω (⋃x∈{x. Inl (Inr x) ∈ SIGF φ}. FVT (σ x)) ⟹ fsafe φ ⟹ fml_sem (adjointFO I σ ν) φ = fml_sem (adjointFO I σ ω) φ"
proof (induct "α" and "φ")
case (Pvar x)
then show ?case unfolding adjointFO_def by auto
next
case (Assign x e)
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP (Assign x e)}. FVT (σ y))"
assume safe:"hpsafe (x := e)"
from safe have dsafe:"dsafe e" by (auto dest: hpsafe.cases)
have sub:"(⋃y∈{y. Inr y ∈ SIGT e}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (Assign x e)}. FVT (σ y))"
using ntadj_sub_assign[of σ e x] by auto
have VA':"(Vagree ν ω (⋃i∈{i. Inr i ∈ SIGT e}. FVT (σ i)))"
using agree_sub[OF sub VA] by auto
have "dterm_sem (adjointFO I σ ν) e = dterm_sem (adjointFO I σ ω) e"
using uadmit_dterm_ntadjoint'[of σ I ν ω e] ssafe good_interp agree_sub[OF sub VA] dsafe by auto
then show ?case by (auto simp add: vec_eq_iff)
next
case (DiffAssign x e)
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP (DiffAssign x e)}. FVT (σ y))"
assume safe:"hpsafe (DiffAssign x e)"
from safe have dsafe:"dsafe e" by (auto dest: hpsafe.cases)
have sub:"(⋃y∈{y. Inr y ∈ SIGT e}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (DiffAssign x e)}. FVT (σ y))"
using ntadj_sub_assign[of σ e x] by auto
have VA':"(Vagree ν ω (⋃i∈{i. Inr i ∈ SIGT e}. FVT (σ i)))"
using agree_sub[OF sub VA] by auto
have "dterm_sem (adjointFO I σ ν) e = dterm_sem (adjointFO I σ ω) e"
using uadmit_dterm_ntadjoint'[of σ I ν ω e] ssafe good_interp agree_sub[OF sub VA] dsafe by auto
then show ?case by (auto simp add: vec_eq_iff)
next
case (Test x)
assume IH:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF x}. FVT (σ y)) ⟹ fsafe x ⟹ fml_sem (adjointFO I σ ν) x = fml_sem (adjointFO I σ ω) x"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP (? x)}. FVT (σ y))"
assume hpsafe:"hpsafe (? x)"
then have fsafe:"fsafe x" by (auto dest: hpsafe.cases)
have sub:"(⋃y∈{y. Inl (Inr y) ∈ SIGF x}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (? x)}. FVT (σ y))"
by auto
have "fml_sem (adjointFO I σ ν) x = fml_sem (adjointFO I σ ω) x"
using IH[OF agree_sub[OF sub VA] fsafe] by auto
then show ?case by auto
next
case (EvolveODE x1 x2)
assume IH:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y)) ⟹ fsafe x2 ⟹ fml_sem (adjointFO I σ ν) x2 = fml_sem (adjointFO I σ ω) x2"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP (EvolveODE x1 x2)}. FVT (σ y))"
assume safe:"hpsafe (EvolveODE x1 x2)"
then have osafe:"osafe x1" and fsafe:"fsafe x2" by (auto dest: hpsafe.cases)
have sub1:"(⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (EvolveODE x1 x2)}. FVT (σ y))"
by auto
then have VAF:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y))"
using agree_sub[OF sub1 VA] by auto
note IH' = IH[OF VAF fsafe]
have sub:"(⋃y∈{y. Inl (Inr y) ∈ SIGO x1}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (EvolveODE x1 x2)}. FVT (σ y))"
by auto
moreover have IH2:"ODE_sem (adjointFO I σ ν) x1 = ODE_sem (adjointFO I σ ω) x1"
apply (rule uadmit_ode_ntadjoint')
subgoal by (rule ssafe)
subgoal by (rule good_interp)
defer subgoal by (rule osafe)
using agree_sub[OF sub VA] by auto
have mkv:"mk_v (adjointFO I σ ν) x1 = mk_v (adjointFO I σ ω) x1"
apply (rule uadmit_mkv_ntadjoint)
using ssafe good_interp osafe agree_sub[OF sub VA] by auto
show ?case
apply auto
subgoal for aa ba bb sol t
apply(rule exI[where x = sol])
apply(rule conjI)
subgoal by auto
apply(rule exI[where x=t])
apply(rule conjI)
subgoal using mkv by auto
apply(rule conjI)
subgoal by auto using IH2 mkv IH' by auto
subgoal for aa ba bb sol t
apply(rule exI[where x = sol])
apply(rule conjI)
subgoal by auto
apply(rule exI[where x=t])
apply(rule conjI)
subgoal using mkv by auto
apply(rule conjI)
subgoal by auto using IH2 mkv IH' by auto
done
next
case (Choice x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP x1}. FVT (σ y)) ⟹ hpsafe x1 ⟹ prog_sem (adjointFO I σ ν) x1 = prog_sem (adjointFO I σ ω) x1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP x2}. FVT (σ y)) ⟹ hpsafe x2 ⟹ prog_sem (adjointFO I σ ν) x2 = prog_sem (adjointFO I σ ω) x2"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP (x1 ∪∪ x2)}. FVT (σ y))"
assume safe:"hpsafe (x1 ∪∪ x2)"
from safe have
safe1:"hpsafe x1"
and safe2:"hpsafe x2"
by (auto dest: hpsafe.cases)
have sub1:"(⋃y∈{y. Inl (Inr y) ∈ SIGP (x1)}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (x1 ∪∪ x2)}. FVT (σ y))"
by auto
have sub2:"(⋃y∈{y. Inl (Inr y) ∈ SIGP (x2)}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (x1 ∪∪ x2)}. FVT (σ y))"
by auto
then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
case (Sequence x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP x1}. FVT (σ y)) ⟹ hpsafe x1 ⟹ prog_sem (adjointFO I σ ν) x1 = prog_sem (adjointFO I σ ω) x1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP x2}. FVT (σ y)) ⟹ hpsafe x2 ⟹ prog_sem (adjointFO I σ ν) x2 = prog_sem (adjointFO I σ ω) x2"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP (x1 ;; x2)}. FVT (σ y))"
assume safe:"hpsafe (x1 ;; x2)"
from safe have
safe1:"hpsafe x1"
and safe2:"hpsafe x2"
by (auto dest: hpsafe.cases)
have sub1:"(⋃y∈{y. Inl (Inr y) ∈ SIGP x1}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (x1 ;; x2)}. FVT (σ y))"
by auto
have sub2:"(⋃y∈{y. Inl (Inr y) ∈ SIGP x2}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (x1 ;; x2)}. FVT (σ y))"
by auto
then show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
case (Loop x)
assume IH:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP x}. FVT (σ y)) ⟹ hpsafe x ⟹ prog_sem (adjointFO I σ ν) x = prog_sem (adjointFO I σ ω) x"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP (x** )}. FVT (σ y))"
assume safe:"hpsafe (x** )"
from safe have
safe:"hpsafe x"
by (auto dest: hpsafe.cases)
have sub:"(⋃y∈{y. Inl (Inr y) ∈ SIGP (x )}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGP (x** )}. FVT (σ y))"
by auto
show ?case using IH[OF agree_sub[OF sub VA] safe] by auto
next
case (Geq x1 x2)
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF (Geq x1 x2)}. FVT (σ y))"
assume safe:"fsafe (Geq x1 x2)"
then have dsafe1:"dsafe x1" and dsafe2:"dsafe x2" by (auto dest: fsafe.cases)
have sub1:"(⋃y∈{y. Inr y ∈ SIGT x1}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGF (Geq x1 x2)}. FVT (σ y))"
by auto
have sub2:"(⋃y∈{y. Inr y ∈ SIGT x2}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGF (Geq x1 x2)}. FVT (σ y))"
by auto
have "dterm_sem (adjointFO I σ ν) x1 = dterm_sem (adjointFO I σ ω) x1"
by (rule uadmit_dterm_ntadjoint'[OF ssafe good_interp agree_sub[OF sub1 VA] dsafe1])
moreover have "dterm_sem (adjointFO I σ ν) x2 = dterm_sem (adjointFO I σ ω) x2"
by (rule uadmit_dterm_ntadjoint'[OF ssafe good_interp agree_sub[OF sub2 VA] dsafe2])
ultimately show ?case by auto
next
case (Prop x1 x2 ν ω)
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF ($φ x1 x2)}. FVT (σ y))"
assume safe:"fsafe ($φ x1 x2)"
then have safes:"⋀i. dsafe (x2 i)" using dfree_is_dsafe by auto
have subs:"⋀j. (⋃y∈{y. Inr y ∈ SIGT (x2 j)}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGF ($φ x1 x2)}. FVT (σ y))"
subgoal for j by auto
done
have "⋀i. dterm_sem (adjointFO I σ ν) (x2 i) = dterm_sem (adjointFO I σ ω) (x2 i)"
by (rule uadmit_dterm_ntadjoint'[OF ssafe good_interp agree_sub[OF subs VA] safes])
then have vec_eq:"⋀R. (χ i. dterm_sem (adjointFO I σ ν) (x2 i) R) = (χ i. dterm_sem (adjointFO I σ ω) (x2 i) R)"
by (auto simp add: vec_eq_iff)
from VA have VAs:"⋀j. Vagree ν ω (⋃y∈{y. Inr y ∈ SIGT (x2 j)}. FVT (σ y))"
subgoal for j
using agree_sub[OF subs[of j] VA] by auto
done
then show ?case
using vec_eq by (auto simp add: adjointFO_def)
next
case (Not x)
assume IH:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF x}. FVT (σ y)) ⟹ fsafe x ⟹ fml_sem (adjointFO I σ ν) x = fml_sem (adjointFO I σ ω) x"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF (Not x)}. FVT (σ y))"
assume safe:"fsafe (Not x)"
from safe have
safe:"fsafe x"
by (auto dest: fsafe.cases)
have sub:"(⋃y∈{y. Inl (Inr y) ∈ SIGF x}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGF (Not x)}. FVT (σ y))"
by auto
show ?case using IH[OF agree_sub[OF sub VA] safe] by auto
next
case (And x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF x1}. FVT (σ y)) ⟹ fsafe x1 ⟹ fml_sem (adjointFO I σ ν) x1 = fml_sem (adjointFO I σ ω) x1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y)) ⟹ fsafe x2 ⟹ fml_sem (adjointFO I σ ν) x2 = fml_sem (adjointFO I σ ω) x2"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF (And x1 x2)}. FVT (σ y))"
assume safe:"fsafe (And x1 x2)"
from safe have
safe1:"fsafe x1"
and safe2:"fsafe x2"
by (auto dest: fsafe.cases)
have sub1:"(⋃y∈{y. Inl (Inr y) ∈ SIGF x1}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGF (And x1 x2)}. FVT (σ y))"
by auto
have sub2:"(⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGF (And x1 x2)}. FVT (σ y))"
by auto
show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
case (Exists x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y)) ⟹ fsafe x2 ⟹ fml_sem (adjointFO I σ ν) x2 = fml_sem (adjointFO I σ ω) x2"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF (Exists x1 x2)}. FVT (σ y))"
assume safe:"fsafe (Exists x1 x2)"
from safe have safe1:"fsafe x2"
by (auto dest: fsafe.cases)
have sub1:"(⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGF (Exists x1 x2)}. FVT (σ y))"
by auto
show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] by auto
next
case (Diamond x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGP x1}. FVT (σ y)) ⟹ hpsafe x1 ⟹ prog_sem (adjointFO I σ ν) x1 = prog_sem (adjointFO I σ ω) x1"
assume IH2:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y)) ⟹ fsafe x2 ⟹ fml_sem (adjointFO I σ ν) x2 = fml_sem (adjointFO I σ ω) x2"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF (Diamond x1 x2)}. FVT (σ y))"
assume safe:"fsafe (Diamond x1 x2)"
from safe have
safe1:"hpsafe x1"
and safe2:"fsafe x2"
by (auto dest: fsafe.cases)
have sub1:"(⋃y∈{y. Inl (Inr y) ∈ SIGP x1}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGF (Diamond x1 x2)}. FVT (σ y))"
by auto
have sub2:"(⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGF (Diamond x1 x2)}. FVT (σ y))"
by auto
show ?case using IH1[OF agree_sub[OF sub1 VA] safe1] IH2[OF agree_sub[OF sub2 VA] safe2] by auto
next
case (InContext x1 x2)
assume IH1:"⋀ν ω. Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y)) ⟹ fsafe x2 ⟹ fml_sem (adjointFO I σ ν) x2 = fml_sem (adjointFO I σ ω) x2"
assume VA:"Vagree ν ω (⋃y∈{y. Inl (Inr y) ∈ SIGF (InContext x1 x2)}. FVT (σ y))"
assume safe:"fsafe (InContext x1 x2)"
from safe have safe1:"fsafe x2"
by (auto dest: fsafe.cases)
have sub:"(⋃y∈{y. Inl (Inr y) ∈ SIGF x2}. FVT (σ y)) ⊆ (⋃y∈{y. Inl (Inr y) ∈ SIGF (InContext x1 x2)}. FVT (σ y))"
by auto
show ?case using IH1[OF agree_sub[OF sub VA] safe1]
unfolding adjointFO_def by auto
qed
lemma uadmit_prog_ntadjoint:
assumes TUA:"PUadmitFO σ α U"
assumes VA:"Vagree ν ω (-U)"
assumes dfree:"⋀i . dsafe (σ i)"
assumes hpsafe:"hpsafe α"
assumes good_interp:"is_interp I"
shows "prog_sem (adjointFO I σ ν) α = prog_sem (adjointFO I σ ω) α"
proof -
have sub:"(⋃x∈{x. Inl (Inr x) ∈ SIGP α}. FVT (σ x)) ⊆ -U" using TUA unfolding PUadmitFO_def by auto
have VA':"Vagree ν ω (⋃x∈{x. Inl (Inr x) ∈ SIGP α}. FVT (σ x))" using agree_sub[OF sub VA] by auto
show ?thesis
apply(rule uadmit_prog_fml_ntadjoint'[OF dfree good_interp])
subgoal by (rule VA')
subgoal by (rule hpsafe)
done
qed
lemma uadmit_fml_ntadjoint:
assumes TUA:"FUadmitFO σ φ U"
assumes VA:"Vagree ν ω (-U)"
assumes dfree:"⋀i . dsafe (σ i)"
assumes fsafe:"fsafe φ"
assumes good_interp:"is_interp I"
shows "fml_sem (adjointFO I σ ν) φ = fml_sem (adjointFO I σ ω) φ"
proof -
have sub:"(⋃x∈{x. Inl (Inr x) ∈ SIGF φ}. FVT (σ x)) ⊆ -U" using TUA unfolding FUadmitFO_def by auto
have VA':"Vagree ν ω (⋃x∈{x. Inl (Inr x) ∈ SIGF φ}. FVT (σ x))" using agree_sub[OF sub VA] by auto
show ?thesis
apply(rule uadmit_prog_fml_ntadjoint'[OF dfree good_interp])
subgoal by (rule VA')
subgoal by (rule fsafe)
done
qed
subsection‹Substitution theorems for terms›
lemma nsubst_sterm:
fixes I::"('sf, 'sc, 'sz) interp"
fixes ν::"'sz state"
shows "TadmitFFO σ θ ⟹ (⋀i. dsafe (σ i)) ⟹ sterm_sem I (TsubstFO θ σ) (fst ν) = sterm_sem (adjointFO I σ ν) θ (fst ν)"
proof (induction rule: TadmitFFO.induct)
case (TadmitFFO_Fun1 σ args f)
then show ?case by(auto simp add: adjointFO_def)
next
case (TadmitFFO_Fun2 σ args f)
then show ?case
apply(auto simp add: adjointFO_def)
by (simp add: dsem_to_ssem)
qed (auto)
lemma nsubst_sterm':
fixes I::"('sf, 'sc, 'sz) interp"
fixes a b::"'sz simple_state"
shows "TadmitFFO σ θ ⟹ (⋀i. dsafe (σ i)) ⟹ sterm_sem I (TsubstFO θ σ) a = sterm_sem (adjointFO I σ (a,b)) θ a"
using nsubst_sterm by (metis fst_conv)
lemma ntsubst_preserves_free:
"dfree θ ⟹ (⋀i. dfree (σ i)) ⟹ dfree(TsubstFO θ σ)"
proof (induction rule: dfree.induct)
case (dfree_Fun args i) then show "?case"
by (cases "i") (auto intro:dfree.intros)
qed (auto intro: dfree.intros)
lemma tsubst_preserves_free:
"dfree θ ⟹ (⋀i f'. SFunctions σ i = Some f' ⟹ dfree f') ⟹ dfree(Tsubst θ σ)"
proof (induction rule: dfree.induct)
case (dfree_Fun args i) then show "?case"
by (cases "SFunctions σ i") (auto intro:dfree.intros ntsubst_preserves_free)
qed (auto intro: dfree.intros)
lemma subst_sterm:
fixes I::"('sf, 'sc, 'sz) interp"
fixes ν::"'sz state"
shows "
TadmitF σ θ ⟹
(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f') ⟹
sterm_sem I (Tsubst θ σ) (fst ν) = sterm_sem (adjoint I σ ν) θ (fst ν)"
proof (induction rule: TadmitF.induct)
case (TadmitF_Fun1 σ args f f') then
have subFree:" TadmitFFO (λi. Tsubst (args i) σ) f'"
and frees:"⋀i. dfree (Tsubst (args i) σ)"
and TFA:"⋀i. TadmitF σ (args i)"
and NTFA:"TadmitFFO (λi. Tsubst (args i) σ) f'"
and theIH:"⋀i. sterm_sem I (Tsubst (args i) σ) (fst ν) = sterm_sem (local.adjoint I σ ν) (args i) (fst ν)"
by auto
from frees have safes:"⋀i. dsafe (Tsubst (args i) σ)"
by (simp add: dfree_is_dsafe)
assume subFreeer:"(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f')"
note admit = TadmitF_Fun1.hyps(1) and sfree = TadmitF_Fun1.prems(1)
have IH:"(⋀i. sterm_sem I (Tsubst (args i) σ) (fst ν) = sterm_sem (adjoint I σ ν) (args i) (fst ν))"
using admit TadmitF_Fun1.prems TadmitF_Fun1.IH by auto
have vec_eq:"(χ i. sterm_sem (local.adjoint I σ ν) (args i) (fst ν)) = (χ i. sterm_sem I (Tsubst (args i) σ) (fst ν))"
apply(rule vec_extensionality)
using IH by auto
assume some:"SFunctions σ f = Some f'"
let ?sub = "(λ i. Tsubst (args i) σ)"
have IH2:"sterm_sem I (TsubstFO f' ?sub) (fst ν) = sterm_sem (adjointFO I ?sub ν) f' (fst ν)"
apply(rule nsubst_sterm)
apply(rule subFree)
by (rule safes)
show "?case"
apply (simp add: some)
unfolding vec_eq IH2
by (auto simp add: some adjoint_free[OF subFreeer, of σ "(λ x y. x)" I ν] adjointFO_free[OF frees])
next
case (TadmitF_Fun2 σ args f)
assume none:"SFunctions σ f = None"
note admit = TadmitF_Fun2.hyps(1) and sfree = TadmitF_Fun2.prems(1)
have IH:"(⋀i. TadmitF σ (args i) ⟹
sterm_sem I (Tsubst (args i) σ) (fst ν) = sterm_sem (adjoint I σ ν) (args i) (fst ν))"
using TadmitF_Fun2.prems TadmitF_Fun2.IH by auto
have eqs:"⋀i. sterm_sem I (Tsubst (args i) σ) (fst ν) = sterm_sem (adjoint I σ ν) (args i) (fst ν)"
by (auto simp add: IH admit)
show "?case"
by(auto simp add: none IH adjoint_def vec_extensionality eqs)
qed auto
lemma nsubst_dterm':
fixes I::"('sf, 'sc, 'sz) interp"
fixes ν::"'sz state"
assumes good_interp:"is_interp I"
shows "TadmitFO σ θ ⟹ dfree θ ⟹ (⋀i. dsafe (σ i)) ⟹ dterm_sem I (TsubstFO θ σ) ν = dterm_sem (adjointFO I σ ν) θ ν"
proof (induction rule: TadmitFO.induct)
case (TadmitFO_Fun σ args f)
assume admit:"⋀i. TadmitFO σ (args i)"
assume IH:"⋀i. dfree (args i) ⟹ (⋀i. dsafe (σ i)) ⟹ dterm_sem I (TsubstFO (args i) σ) ν = dterm_sem (adjointFO I σ ν) (args i) ν"
assume free:"dfree ($f f args)"
assume safe:"⋀i. dsafe (σ i)"
from free have frees: "⋀i. dfree (args i)" by (auto dest: dfree.cases)
have sem:"⋀i. dterm_sem I (TsubstFO (args i) σ) ν = dterm_sem (adjointFO I σ ν) (args i) ν"
using IH[OF frees safe] by auto
have vecEq:" (χ i. dterm_sem (adjointFO I σ ν) (args i) ν) =
(χ i. dterm_sem
⦇Functions = case_sum (Functions I) (λf' _. dterm_sem I (σ f') ν), Predicates = Predicates I, Contexts = Contexts I,
Programs = Programs I, ODEs = ODEs I, ODEBV = ODEBV I⦈
(args i) ν) "
apply(rule vec_extensionality)
by (auto simp add: adjointFO_def)
show " dterm_sem I (TsubstFO ($f f args) σ) ν = dterm_sem (adjointFO I σ ν) ($f f args) ν"
apply (cases "f")
apply (auto simp add: vec_extensionality adjointFO_def)
using sem apply auto
subgoal for a using vecEq by auto
done
next
case (TadmitFO_Diff σ θ)
hence admit:"TadmitFFO σ θ"
and admitU:"NTUadmit σ θ UNIV"
and safe: "dfree (Differential θ)"
and freeSub:"⋀i. dsafe (σ i)"
by auto
from safe have "False" by (auto dest: dfree.cases)
then show "dterm_sem I (TsubstFO (Differential θ) σ) ν = dterm_sem (adjointFO I σ ν) (Differential θ) ν"
by auto
qed (auto simp add: TadmitFO.cases)
lemma ntsubst_free_to_safe:
"dfree θ ⟹ (⋀i. dsafe (σ i)) ⟹ dsafe (TsubstFO θ σ)"
proof (induction rule: dfree.induct)
case (dfree_Fun args i) then show "?case"
by (cases "i") (auto intro:dsafe.intros ntsubst_preserves_free)
qed (auto intro: dsafe.intros)
lemma ntsubst_preserves_safe:
"dsafe θ ⟹ (⋀i. dfree (σ i)) ⟹ dsafe (TsubstFO θ σ)"
proof (induction rule: dsafe.induct)
case (dsafe_Fun args i) then show "?case"
by (cases "i") (auto intro:dsafe.intros ntsubst_preserves_free dfree_is_dsafe)
next
case (dsafe_Diff θ) then show "?case"
by (auto intro:dsafe.intros ntsubst_preserves_free)
qed (auto simp add: ntsubst_preserves_free intro: dsafe.intros)
lemma tsubst_preserves_safe:
"dsafe θ ⟹ (⋀i f'. SFunctions σ i = Some f' ⟹ dfree f') ⟹ dsafe(Tsubst θ σ)"
proof (induction rule: dsafe.induct)
case (dsafe_Fun args i)
assume dsafes:"⋀i. dsafe (args i)"
assume IH:"⋀j. (⋀i f'. SFunctions σ i = Some f' ⟹ dfree f') ⟹ dsafe (Tsubst (args j) σ)"
assume frees:"⋀i f. SFunctions σ i = Some f ⟹ dfree f"
have IH':"⋀i. dsafe (Tsubst (args i) σ)"
using frees IH by auto
then show "?case"
apply auto
apply(cases "SFunctions σ i")
subgoal using IH frees by auto
subgoal for a using frees[of i a] ntsubst_free_to_safe[of a] IH' by auto
done
qed (auto intro: dsafe.intros tsubst_preserves_free)
lemma subst_dterm:
fixes I::"('sf, 'sc, 'sz) interp"
assumes good_interp:"is_interp I"
shows "
Tadmit σ θ ⟹
dsafe θ ⟹
(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f') ⟹
(⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f') ⟹
(⋀ν. dterm_sem I (Tsubst θ σ) ν = dterm_sem (adjoint I σ ν) θ ν)"
proof (induction rule: Tadmit.induct)
case (Tadmit_Fun1 σ args f f' ν)
note safe = Tadmit_Fun1.prems(1) and sfree = Tadmit_Fun1.prems(2) and TA = Tadmit_Fun1.hyps(1)
and some = Tadmit_Fun1.hyps(2) and NTA = Tadmit_Fun1.hyps(3)
hence safes:"⋀i. dsafe (args i)" by auto
have IH:"(⋀ν'. ⋀i. dsafe (args i) ⟹
dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν)"
using Tadmit_Fun1.prems Tadmit_Fun1.IH by auto
have eqs:"⋀i ν'. dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν"
by (auto simp add: IH safes)
let ?sub = "(λ i. Tsubst (args i) σ)"
have subSafe:"(⋀i. dsafe (?sub i))"
using tsubst_preserves_safe[OF safes sfree]
by (simp add: safes sfree tsubst_preserves_safe)
have freef:"dfree f'" using sfree some by auto
have IH2:"dterm_sem I (TsubstFO f' ?sub) ν = dterm_sem (adjointFO I ?sub ν) f' ν"
by (simp add: nsubst_dterm'[OF good_interp NTA freef subSafe])
have vec:"(χ i. dterm_sem I (Tsubst (args i) σ) ν) = (χ i. dterm_sem (local.adjoint I σ ν) (args i) ν)"
apply(auto simp add: vec_eq_iff)
subgoal for i
using IH[of i, OF safes[of i]]
by auto
done
show "?case"
using IH safes eqs apply (auto simp add: IH2 some good_interp)
using some unfolding adjoint_def adjointFO_def by auto
next
case (Tadmit_Fun2 σ args f ν)
note safe = Tadmit_Fun2.prems(1) and sfree = Tadmit_Fun2.prems(2) and TA = Tadmit_Fun2.hyps(1)
and none = Tadmit_Fun2.hyps(2)
hence safes:"⋀i. dsafe (args i)" by auto
have IH:"(⋀ν'. ⋀i. dsafe (args i) ⟹
dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν)"
using Tadmit_Fun2.prems Tadmit_Fun2.IH by auto
have Ieq:"Functions I f = Functions (adjoint I σ ν) f"
using none unfolding adjoint_def by auto
have vec:"(χ i. dterm_sem I (Tsubst (args i) σ) ν) = (χ i. dterm_sem (adjoint I σ ν) (args i) ν)"
apply(auto simp add: vec_eq_iff)
subgoal for i using IH[of i, OF safes[of i]] by auto
done
show "?case" using none IH Ieq vec by auto
next
case (Tadmit_Diff σ θ) then
have TA:"Tadmit σ θ"
and TUA:"TUadmit σ θ UNIV"
and IH:"dsafe θ ⟹ (⋀i f'. SFunctions σ i = Some f' ⟹ dfree f') ⟹ (⋀ν. dterm_sem I (Tsubst θ σ) ν = dterm_sem (local.adjoint I σ ν) θ ν)"
and safe:"dsafe (Differential θ)"
and sfree:"⋀i f'1. SFunctions σ i = Some f'1 ⟹ dfree f'1"
and spsafe:"⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f'"
by auto
from sfree have sdsafe:"⋀f f'. SFunctions σ f = Some f' ⟹ dsafe f'"
using dfree_is_dsafe by auto
have VA:"⋀ν ω. Vagree ν ω (-UNIV)" unfolding Vagree_def by auto
from safe have free:"dfree θ" by (auto dest: dsafe.cases intro: dfree.intros)
from free have tsafe:"dsafe θ" using dfree_is_dsafe by auto
have freeSubst:"dfree (Tsubst θ σ)"
using tsubst_preserves_free[OF free sfree]
using Tadmit_Diff.prems(2) free tsubst_preserves_free by blast
have IH':"⋀ν. dterm_sem I (Tsubst θ σ) ν = dterm_sem (local.adjoint I σ ν) θ ν"
using IH[OF tsafe sfree] by auto
have sem_eq:"⋀ν'. dsafe θ ⟹ is_interp I ⟹ dterm_sem (local.adjoint I σ ν) θ = dterm_sem (local.adjoint I σ ν') θ"
subgoal for ν'
using uadmit_dterm_adjoint[OF TUA VA sfree spsafe, of "(λ x y. x)" "(λ x y. x)" I ν ν']
by auto
done
have IH'':"⋀ν'. dterm_sem I (Tsubst θ σ) ν' = dterm_sem (local.adjoint I σ ν) θ ν'"
subgoal for ν'
using sem_eq[OF tsafe good_interp, of ν'] IH'[of ν'] by auto
done
have sem_eq:"sterm_sem I (Tsubst θ σ) = sterm_sem (local.adjoint I σ ν) θ"
apply (auto simp add: fun_eq_iff)
subgoal for ν'
apply (cases "ν'")
subgoal for ν''
apply auto
using dsem_to_ssem[OF free, of "(local.adjoint I σ ν)" "(ν',ν')"] dsem_to_ssem[OF freeSubst, of I "(ν',ν')"] IH'[of "(ν)"]
apply auto
using IH'' by auto
done
done
show "?case"
apply (auto simp add: directional_derivative_def fun_eq_iff)
using sterm_determines_frechet[OF
good_interp
adjoint_safe[OF good_interp sfree]
tsubst_preserves_free[OF free sfree]
free sem_eq]
by auto
qed auto
subsection‹Substitution theorems for ODEs›
lemma osubst_preserves_safe:
assumes ssafe:"ssafe σ"
shows "(osafe ODE ⟹ Oadmit σ ODE U ⟹ osafe (Osubst ODE σ))"
proof (induction rule: osafe.induct)
case (osafe_Var c)
then show ?case using ssafe unfolding ssafe_def by (cases "SODEs σ c", auto intro: osafe.intros)
next
case (osafe_Sing θ x)
then show ?case
using tsubst_preserves_free ssafe unfolding ssafe_def by (auto intro: osafe.intros)
next
case (osafe_Prod ODE1 ODE2)
moreover have "Oadmit σ ODE1 U" "Oadmit σ ODE2 U" "ODE_dom (Osubst ODE1 σ) ∩ ODE_dom (Osubst ODE2 σ) = {}"
using osafe_Prod.prems by (auto dest: Oadmit.cases)
ultimately show ?case by (auto intro: osafe.intros)
qed
lemma nosubst_preserves_safe:
assumes sfree:"⋀i. dfree (σ i)"
fixes α ::"('a + 'd, 'b, 'c) hp" and φ ::"('a + 'd, 'b, 'c) formula"
shows "(osafe ODE ⟹ OUadmitFO σ ODE U ⟹ osafe (OsubstFO ODE σ))"
proof (induction rule: osafe.induct)
case (osafe_Var c)
then show ?case by (auto intro: osafe.intros)
next
case (osafe_Sing θ x)
then show ?case using sfree ntsubst_preserves_free[of θ σ] unfolding OUadmitFO_def by (auto intro: osafe.intros)
next
case (osafe_Prod ODE1 ODE2)
assume safe1:"osafe ODE1"
and safe2:"osafe ODE2"
and disj:"ODE_dom ODE1 ∩ ODE_dom ODE2 = {}"
and IH1:"OUadmitFO σ ODE1 U ⟹ osafe (OsubstFO ODE1 σ)"
and IH2:"OUadmitFO σ ODE2 U ⟹ osafe (OsubstFO ODE2 σ)"
and NOUA:"OUadmitFO σ (OProd ODE1 ODE2) U"
have nosubst_preserves_ODE_dom:"⋀ODE. ODE_dom (OsubstFO ODE σ) = ODE_dom ODE"
subgoal for ODE
apply(induction "ODE")
by auto
done
have disj':"ODE_dom (OsubstFO ODE1 σ) ∩ ODE_dom (OsubstFO ODE2 σ) = {}"
using disj nosubst_preserves_ODE_dom by auto
from NOUA have NOUA1:"OUadmitFO σ ODE1 U" and NOUA2:"OUadmitFO σ ODE2 U" unfolding OUadmitFO_def by auto
then show ?case using IH1[OF NOUA1] IH2[OF NOUA2] disj' by (auto intro: osafe.intros)
qed
lemma nsubst_dterm:
fixes I::"('sf, 'sc, 'sz) interp"
fixes ν::"'sz state"
fixes ν'::"'sz state"
assumes good_interp:"is_interp I"
shows "TadmitFO σ θ ⟹ dsafe θ ⟹ (⋀i. dsafe (σ i)) ⟹ dterm_sem I (TsubstFO θ σ) ν = dterm_sem (adjointFO I σ ν) θ ν"
proof (induction rule: TadmitFO.induct)
case (TadmitFO_Diff σ θ) then
have subFree:"(⋀i. dsafe (σ i))"
and NTFA:"TadmitFFO σ θ"
and substFree:"dfree (TsubstFO θ σ)"
and dsafe:"dsafe (Differential θ)"
and subSafe:"⋀i. dsafe (σ i)"
and NTU:"NTUadmit σ θ UNIV"
by auto
have dfree:"dfree θ" using dsafe by auto
then show ?case
apply auto
apply (unfold directional_derivative_def)
apply (rule sterm_determines_frechet)
subgoal using good_interp by auto
subgoal using adjointFO_safe[OF good_interp, of σ] subSafe by auto
subgoal using substFree by auto
subgoal using dfree by auto
subgoal
apply(rule ext)
subgoal for x
using nsubst_sterm'[of σ θ I "(fst ν)" "(snd ν)", OF NTFA subSafe] apply auto
proof -
assume sem:"sterm_sem I (TsubstFO θ σ) (fst ν) = sterm_sem (adjointFO I σ ν) θ (fst ν)"
have VA:"⋀ν ω. Vagree ν (x,snd ν) (-UNIV)" unfolding Vagree_def by auto
show "sterm_sem I (TsubstFO θ σ) x = sterm_sem (adjointFO I σ ν) θ x"
using uadmit_sterm_ntadjoint[OF NTU VA subSafe, OF good_interp, of "(x, snd ν)"]
nsubst_sterm[OF NTFA subSafe, of I ν ]
apply auto
using NTU VA dfree_is_dsafe dsafe subSafe substFree good_interp uadmit_sterm_ntadjoint
by (metis NTFA fst_eqD nsubst_sterm)
qed
done
done
next
case (TadmitFO_Fun σ args f)
then show ?case apply auto apply(cases f) unfolding adjointFO_def by auto
qed (auto)
lemma nsubst_ode:
fixes I::"('sf, 'sc, 'sz) interp"
fixes ν::"'sz state"
fixes ν'::"'sz state"
assumes good_interp:"is_interp I"
shows "osafe ODE ⟹ OadmitFO σ ODE U ⟹ (⋀i. dsafe (σ i)) ⟹ ODE_sem I (OsubstFO ODE σ) (fst ν)= ODE_sem (adjointFO I σ ν) ODE (fst ν)"
proof (induction rule: osafe.induct)
case (osafe_Var c)
then show ?case unfolding OUadmitFO_def adjointFO_def by auto
next
case (osafe_Sing θ x)
then show ?case apply auto
using nsubst_sterm' [of σ θ I "(fst ν)" "(snd ν)"] by auto
next
case (osafe_Prod ODE1 ODE2) then
have NO1:"OadmitFO σ ODE1 U" and NO2:"OadmitFO σ ODE2 U"
unfolding OUadmitFO_def by auto
have "ODE_sem I (OsubstFO ODE1 σ) (fst ν) = ODE_sem (adjointFO I σ ν) ODE1 (fst ν)"
"ODE_sem I (OsubstFO ODE2 σ) (fst ν) = ODE_sem (adjointFO I σ ν) ODE2 (fst ν)" using osafe_Prod.IH osafe_Prod.prems osafe_Prod.hyps
using NO1 NO2 by auto
then show ?case by auto
qed
lemma osubst_preserves_BVO:
shows "BVO (OsubstFO ODE σ) = BVO ODE"
proof (induction "ODE")
qed (auto)
lemma osubst_preserves_ODE_vars:
shows "ODE_vars I (OsubstFO ODE σ) = ODE_vars (adjointFO I σ ν) ODE"
proof (induction "ODE")
qed (auto simp add: adjointFO_def)
lemma osubst_preserves_semBV:
shows "semBV I (OsubstFO ODE σ) = semBV (adjointFO I σ ν) ODE"
proof (induction "ODE")
qed (auto simp add: adjointFO_def)
lemma nsubst_mkv:
fixes I::"('sf, 'sc, 'sz) interp"
fixes ν::"'sz state"
fixes ν'::"'sz state"
assumes good_interp:"is_interp I"
assumes NOU:"OadmitFO σ ODE U"
assumes osafe:"osafe ODE "
assumes frees:"(⋀i. dsafe (σ i))"
shows "(mk_v I (OsubstFO ODE σ) ν (fst ν'))
= (mk_v (adjointFO I σ ν') ODE ν (fst ν'))"
apply(rule agree_UNIV_eq)
using mk_v_agree[of "adjointFO I σ ν'" "ODE" ν "fst ν'"]
using mk_v_agree[of "I" "OsubstFO ODE σ" ν "fst ν'"]
unfolding Vagree_def
using nsubst_ode[OF good_interp osafe NOU frees, of ν']
apply auto
subgoal for i
apply(erule allE[where x=i])+
apply(cases "Inl i ∈ semBV I (OsubstFO ODE σ)")
using osubst_preserves_ODE_vars
by (metis (full_types))+
subgoal for i
apply(erule allE[where x=i])+
apply(cases "Inr i ∈ BVO ODE")
using osubst_preserves_ODE_vars
by (metis (full_types))+
done
lemma ODE_unbound_zero:
fixes i
shows "Inl i ∉ BVO ODE ⟹ ODE_sem I ODE x $ i = 0"
proof (induction ODE)
qed (auto)
lemma ODE_bound_effect:
fixes s t sol ODE X b
assumes s:"s ∈ {0..t}"
assumes sol:"(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} X"
shows "Vagree (sol 0,b) (sol s, b) (-(BVO ODE))"
proof -
have "⋀i. Inl i ∉ BVO ODE ⟹ (∀ s. s ∈ {0..t} ⟶ sol s $ i = sol 0 $ i)"
apply auto
apply (rule constant_when_zero)
using s sol apply auto
using ODE_unbound_zero solves_ode_subset
by fastforce+
then show "Vagree (sol 0, b) (sol s, b) (- BVO ODE)"
unfolding Vagree_def
using s by (metis Compl_iff fst_conv snd_conv)
qed
lemma NO_sub:"OadmitFO σ ODE A ⟹ B ⊆ A ⟹ OadmitFO σ ODE B"
by(induction ODE, auto simp add: OUadmitFO_def)
lemma NO_to_NOU:"OadmitFO σ ODE S ⟹ OUadmitFO σ ODE S"
by(induction ODE, auto simp add: OUadmitFO_def)
subsection‹Substitution theorems for formulas and programs›
lemma nsubst_hp_fml:
fixes I::"('sf, 'sc, 'sz) interp"
assumes good_interp:"is_interp I"
shows " (NPadmit σ α ⟶ (hpsafe α ⟶ (∀i. dsafe (σ i)) ⟶ (∀ ν ω. ((ν, ω) ∈ prog_sem I (PsubstFO α σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) α)))) ∧
(NFadmit σ φ ⟶ (fsafe φ ⟶ (∀i. dsafe (σ i)) ⟶ (∀ ν. (ν ∈ fml_sem I (FsubstFO φ σ)) = (ν ∈ fml_sem (adjointFO I σ ν) φ))))"
proof (induction rule: NPadmit_NFadmit.induct)
case (NPadmit_Pvar σ a)
then show ?case unfolding adjointFO_def by auto
next
case (NPadmit_ODE σ ODE φ) then
have NOU:"OadmitFO σ ODE (BVO ODE)"
and NFA:"NFadmit σ φ"
and NFU:"FUadmitFO σ φ (BVO ODE)"
and fsafe:"fsafe (FsubstFO φ σ)"
and IH:"fsafe φ ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν. (ν ∈ fml_sem I (FsubstFO φ σ)) = (ν ∈ fml_sem (adjointFO I σ ν) φ))"
and osafe':"osafe (OsubstFO ODE σ)"
by auto
have "hpsafe (EvolveODE ODE φ) ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PsubstFO (EvolveODE ODE φ) σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) (EvolveODE ODE φ)))"
proof -
assume safe:"hpsafe (EvolveODE ODE φ)"
then have osafe:"osafe ODE" and fsafe:"fsafe φ" by auto
assume frees:"(⋀i. dsafe (σ i))"
fix ν ω
show "((ν, ω) ∈ prog_sem I (PsubstFO (EvolveODE ODE φ) σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) (EvolveODE ODE φ))"
proof (auto)
fix b
and sol :: "real ⇒(real, 'sz) vec"
and t :: real
assume eq1:"ν = (sol 0, b)"
assume eq2:"ω = mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t)"
assume t:"0 ≤ t"
assume sol:"(sol solves_ode (λa. ODE_sem I (OsubstFO ODE σ))) {0..t}
{x. mk_v I (OsubstFO ODE σ) (sol 0, b) x ∈ fml_sem I (FsubstFO φ σ)}"
have agree_sem:"⋀t. Vagree (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t)) (sol 0, b) (- (Inl ` ODE_vars I (OsubstFO ODE σ) ∪ Inr ` ODE_vars I (OsubstFO ODE σ)))"
subgoal for t
using mk_v_agree[of I "OsubstFO ODE σ" "(sol 0, b)" "sol t"] unfolding Vagree_def apply auto
done
done
have bv_sub:"(-BVO ODE) ⊆ - (Inl ` ODE_vars I (OsubstFO ODE σ) ∪ Inr ` ODE_vars I (OsubstFO ODE σ))"
by(induction ODE, auto)
have agree:"⋀t. Vagree (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t)) (sol 0, b) (- BVO ODE)"
using agree_sub[OF bv_sub agree_sem] by auto
have mkv:"⋀t. mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t) = mk_v (adjointFO I σ (sol t, b)) ODE (sol 0, b) (sol t)"
using nsubst_mkv[OF good_interp NOU osafe frees]
by auto
have hmm:"⋀s. s ∈ {0..t} ⟹ Vagree (sol 0,b) (sol s, b) (-(BVO ODE))"
using ODE_bound_effect sol
by (metis osubst_preserves_BVO)
have FVT_sub:"(⋃y∈{y. Inl (Inr y) ∈ SIGO ODE}. FVT (σ y)) ⊆ (-(BVO ODE))"
using NOU NO_to_NOU OUadmitFO_def
by fastforce
have agrees:"⋀s. s ∈ {0..t} ⟹ Vagree (sol 0,b) (sol s, b) (⋃y∈{y. Inl (Inr y) ∈ SIGO ODE}. FVT (σ y))"
subgoal for s using agree_sub[OF FVT_sub hmm[of s]] by auto done
have "⋀s. s ∈ {0..t} ⟹ mk_v (adjointFO I σ (sol s, b)) ODE = mk_v (adjointFO I σ (sol 0, b)) ODE"
subgoal for s
apply (rule uadmit_mkv_ntadjoint)
prefer 3
using NOU hmm[of s] NO_to_NOU unfolding OUadmitFO_def Vagree_def
apply fastforce
using frees good_interp osafe by auto
done
then have mkva:"⋀s. s ∈ {0..t} ⟹ mk_v (adjointFO I σ (sol s, b)) ODE (sol 0, b) (sol s) = mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol s)"
by presburger
have main_eq:"⋀s. s ∈ {0..t} ⟹ mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) = mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol s) "
using mkv mkva by auto
note mkvt = main_eq[of t]
have fml_eq1:"⋀s. s ∈ {0..t} ⟹
(mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem I (FsubstFO φ σ))
= (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s))) φ)"
using IH[OF fsafe frees] by auto
have fml_eq2:"⋀s. s ∈ {0..t} ⟹
((mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s))) φ)
=(mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (sol 0, b)) φ))"
subgoal for s
using NFU frees fsafe good_interp mk_v_agree osubst_preserves_ODE_vars uadmit_fml_ntadjoint
using agree by blast
done
have fml_eq3:"⋀s. s ∈ {0..t} ⟹
(mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (sol 0, b)) φ) = (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (sol 0, b)) φ) "
using main_eq by auto
have fml_eq: "⋀s. s ∈ {0..t} ⟹
(mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem I (FsubstFO φ σ))
= (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (sol 0, b)) φ)"
using fml_eq1 fml_eq2 fml_eq3 by meson
have sem_eq:"⋀t. ODE_sem I (OsubstFO ODE σ) (sol t) = ODE_sem (adjointFO I σ (sol t, b)) ODE (sol t)"
subgoal for t
using nsubst_ode[OF good_interp osafe NOU frees, of "(sol t,b)"] by auto
done
have sem_fact:"⋀s. s ∈ {0..t} ⟹ ODE_sem I (OsubstFO ODE σ) (sol s) = ODE_sem (adjointFO I σ (sol 0, b)) ODE (sol s)"
subgoal for s
using nsubst_ode[OF good_interp osafe NOU frees, of "(sol s, b)"]
uadmit_ode_ntadjoint'[OF frees good_interp agrees[of s] osafe]
by auto
done
have sol':"(sol solves_ode (λ_. ODE_sem (adjointFO I σ (sol 0, b)) ODE)) {0..t}
{x. mk_v I (OsubstFO ODE σ) (sol 0, b) x ∈ fml_sem I (FsubstFO φ σ)}"
apply (rule solves_ode_congI)
apply (rule sol)
subgoal for ta by auto
subgoal for ta by (rule sem_fact[of ta])
subgoal by (rule refl)
subgoal by (rule refl)
done
have sub:"⋀s. s ∈ {0..t}
⟹ sol s ∈ {x. (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) x ∈ fml_sem (adjointFO I σ (sol 0, b)) φ)}"
using fml_eq rangeI t sol solves_ode_domainD by fastforce
have sol'':"(sol solves_ode (λc. ODE_sem (adjointFO I σ (sol 0, b)) ODE)) {0..t}
{x. mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) x ∈ fml_sem (adjointFO I σ (sol 0, b)) φ}"
apply (rule solves_odeI)
subgoal using sol' solves_ode_vderivD by blast
using sub by auto
show "∃sola. sol 0 = sola 0 ∧
(∃ta. mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t) = mk_v (adjointFO I σ (sol 0, b)) ODE (sola 0, b) (sola ta) ∧
0 ≤ ta ∧
(sola solves_ode (λa. ODE_sem (adjointFO I σ (sol 0, b)) ODE)) {0..ta}
{x. mk_v (adjointFO I σ (sol 0, b)) ODE (sola 0, b) x ∈ fml_sem (adjointFO I σ (sol 0, b)) φ})"
apply(rule exI[where x=sol])
apply(rule conjI)
subgoal by (rule refl)
apply(rule exI[where x=t])
apply(rule conjI)
subgoal using mkvt t by auto
apply(rule conjI)
subgoal by (rule t)
subgoal by (rule sol'')
done
next
fix b
and sol::"real ⇒ (real, 'sz) vec"
and t::real
assume eq1:"ν = (sol 0, b)"
assume eq2:"ω = mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol t)"
assume t:"0 ≤ t"
assume sol:"(sol solves_ode (λa. ODE_sem (adjointFO I σ (sol 0, b)) ODE)) {0..t}
{x. mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) x ∈ fml_sem (adjointFO I σ (sol 0, b)) φ}"
have agree_sem:"⋀t. Vagree (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t)) (sol 0, b) (- (Inl ` ODE_vars I (OsubstFO ODE σ) ∪ Inr ` ODE_vars I (OsubstFO ODE σ)))"
subgoal for t
using mk_v_agree[of I "OsubstFO ODE σ" "(sol 0, b)" "sol t"] unfolding Vagree_def apply auto
done
done
have bv_sub:"(-BVO ODE) ⊆ - (Inl ` ODE_vars I (OsubstFO ODE σ) ∪ Inr ` ODE_vars I (OsubstFO ODE σ))"
by(induction ODE, auto)
have agree:"⋀t. Vagree (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t)) (sol 0, b) (- BVO ODE)"
using agree_sub[OF bv_sub agree_sem] by auto
have mkv:"⋀t. mk_v I (OsubstFO ODE σ) (sol 0, b) (sol t) = mk_v (adjointFO I σ (sol t, b)) ODE (sol 0, b) (sol t)"
using nsubst_mkv[OF good_interp NOU osafe frees]
by auto
have hmm:"⋀s. s ∈ {0..t} ⟹ Vagree (sol 0,b) (sol s, b) (-(BVO ODE))"
using ODE_bound_effect sol
by (metis osubst_preserves_ODE_vars)
have FVT_sub:"(⋃y∈{y. Inl (Inr y) ∈ SIGO ODE}. FVT (σ y)) ⊆ (-(BVO ODE))"
using NOU NO_to_NOU unfolding OUadmitFO_def by fastforce
have agrees:"⋀s. s ∈ {0..t} ⟹ Vagree (sol 0,b) (sol s, b) (⋃y∈{y. Inl (Inr y) ∈ SIGO ODE}. FVT (σ y))"
subgoal for s using agree_sub[OF FVT_sub hmm[of s]] by auto done
have "⋀s. s ∈ {0..t} ⟹ mk_v (adjointFO I σ (sol s, b)) ODE = mk_v (adjointFO I σ (sol 0, b)) ODE"
subgoal for s
apply (rule uadmit_mkv_ntadjoint)
prefer 3
using NOU hmm[of s] NO_to_NOU unfolding OUadmitFO_def Vagree_def
apply fastforce
using frees good_interp osafe by auto
done
then have mkva:"⋀s. s ∈ {0..t} ⟹ mk_v (adjointFO I σ (sol s, b)) ODE (sol 0, b) (sol s) = mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol s)"
by presburger
have main_eq:"⋀s. s ∈ {0..t} ⟹ mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) = mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol s) "
using mkv mkva by auto
note mkvt = main_eq[of t]
have fml_eq1:"⋀s. s ∈ {0..t} ⟹
(mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem I (FsubstFO φ σ))
= (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s))) φ)"
using IH[OF fsafe frees] by auto
have fml_eq2:"⋀s. s ∈ {0..t} ⟹
((mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s))) φ)
=(mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (sol 0, b)) φ))"
using NFU frees fsafe good_interp mk_v_agree osubst_preserves_ODE_vars uadmit_fml_ntadjoint agree by blast
have fml_eq3:"⋀s. s ∈ {0..t} ⟹
(mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (sol 0, b)) φ) = (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (sol 0, b)) φ) "
using main_eq by auto
have fml_eq: "⋀s. s ∈ {0..t} ⟹
(mk_v I (OsubstFO ODE σ) (sol 0, b) (sol s) ∈ fml_sem I (FsubstFO φ σ))
= (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) (sol s) ∈ fml_sem (adjointFO I σ (sol 0, b)) φ)"
using fml_eq1 fml_eq2 fml_eq3 by meson
have sem_eq:"⋀t. ODE_sem I (OsubstFO ODE σ) (sol t) = ODE_sem (adjointFO I σ (sol t, b)) ODE (sol t)"
subgoal for t
using nsubst_ode[OF good_interp osafe NOU frees, of "(sol t,b)"] by auto
done
have sem_fact:"⋀s. s ∈ {0..t} ⟹ ODE_sem I (OsubstFO ODE σ) (sol s) = ODE_sem (adjointFO I σ (sol 0, b)) ODE (sol s)"
subgoal for s
using nsubst_ode[OF good_interp osafe NOU frees, of "(sol s, b)"]
uadmit_ode_ntadjoint'[OF frees good_interp agrees[of s] osafe]
by auto
done
have sol':"
(sol solves_ode (λa. ODE_sem I (OsubstFO ODE σ))) {0..t} {x. mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) x ∈ fml_sem (adjointFO I σ (sol 0, b)) φ}"
apply (rule solves_ode_congI)
apply (rule sol)
subgoal for ta by auto
subgoal for ta using sem_fact[of ta] by auto
subgoal by (rule refl)
subgoal by (rule refl)
done
have sub:"⋀s. s ∈ {0..t}
⟹ sol s ∈ {x. (mk_v (adjointFO I σ (sol 0,b)) ODE (sol 0, b) x ∈ fml_sem (adjointFO I σ (sol 0, b)) φ)}"
using fml_eq rangeI t sol solves_ode_domainD by fastforce
have sol'':"(sol solves_ode (λa. ODE_sem I (OsubstFO ODE σ))) {0..t} {x. mk_v I (OsubstFO ODE σ) (sol 0, b) x ∈ fml_sem I (FsubstFO φ σ)}"
apply (rule solves_odeI)
subgoal using sol' solves_ode_vderivD by blast
using sub fml_eq by blast
show "∃sola. sol 0 = sola 0 ∧
(∃ta. mk_v (adjointFO I σ (sol 0, b)) ODE (sol 0, b) (sol t) = mk_v I (OsubstFO ODE σ) (sola 0, b) (sola ta) ∧
0 ≤ ta ∧
(sola solves_ode (λa. ODE_sem I (OsubstFO ODE σ))) {0..ta} {x. mk_v I (OsubstFO ODE σ) (sola 0, b) x ∈ fml_sem I (FsubstFO φ σ)})"
apply(rule exI[where x=sol])
apply(rule conjI)
subgoal by (rule refl)
apply(rule exI[where x=t])
apply(rule conjI)
subgoal using t mkvt by auto
apply(rule conjI)
subgoal by (rule t)
subgoal by (rule sol'')
done
qed
qed
then show ?case by auto
next
case (NPadmit_Assign σ θ x)
then show ?case using nsubst_dterm[OF good_interp, of σ θ] by auto
next
case (NPadmit_DiffAssign σ θ x)
then show ?case using nsubst_dterm[OF good_interp, of σ θ] by auto
next
case (NFadmit_Geq σ θ1 θ2)
then show ?case
using nsubst_dterm[OF good_interp, of σ θ1]
using nsubst_dterm[OF good_interp, of σ θ2] by auto
next
case (NFadmit_Prop σ args f)
assume NTA:"⋀i. TadmitFO σ (args i)"
have "⋀ν. fsafe ($φ f args) ⟹ (⋀i. dsafe (σ i)) ⟹ (ν ∈ fml_sem I (FsubstFO ($φ f args) σ)) = (ν ∈ fml_sem (adjointFO I σ ν) ($φ f args))"
proof -
fix ν
assume safe:"fsafe ($φ f args)"
from safe have safes:"⋀i. dsafe (args i)" using dfree_is_dsafe by auto
assume subFree:"(⋀i. dsafe (σ i))"
have vec_eq:"(χ i. dterm_sem (adjointFO I σ ν) (args i) ν) = (χ i. dterm_sem I (TsubstFO (args i) σ) ν)"
apply(rule vec_extensionality)
using nsubst_dterm[OF good_interp NTA safes subFree] by auto
then show "?thesis ν" unfolding adjointFO_def by auto
qed
then show ?case by auto
next
case (NPadmit_Sequence σ a b) then
have PUA:"PUadmitFO σ b (BVP (PsubstFO a σ))"
and PA:"NPadmit σ a"
and IH1:"hpsafe a ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PsubstFO a σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) a))"
and IH2:"hpsafe b ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PsubstFO b σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) b))"
and hpsafeS:"hpsafe (PsubstFO a σ)"
by auto
have "hpsafe (a ;; b) ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PsubstFO (a ;; b) σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) (a ;; b)))"
proof -
assume hpsafe:"hpsafe (a ;; b)"
assume ssafe:"(⋀i. dsafe (σ i))"
from hpsafe have safe1:"hpsafe a" and safe2:"hpsafe b" by (auto dest: hpsafe.cases)
fix ν ω
have agree:"⋀μ. (ν, μ) ∈ prog_sem I (PsubstFO a σ) ⟹ Vagree ν μ (-BVP(PsubstFO a σ))"
subgoal for μ
using bound_effect[OF good_interp, of "(PsubstFO a σ)" ν , OF hpsafeS] by auto
done
have sem_eq:"⋀μ. (ν, μ) ∈ prog_sem I (PsubstFO a σ) ⟹
((μ, ω) ∈ prog_sem (adjointFO I σ ν) b) =
((μ, ω) ∈ prog_sem (adjointFO I σ μ) b)"
subgoal for μ
proof -
assume assm:"(ν, μ) ∈ prog_sem I (PsubstFO a σ)"
show "((μ, ω) ∈ prog_sem (adjointFO I σ ν) b) = ((μ, ω) ∈ prog_sem (adjointFO I σ μ) b)"
using uadmit_prog_ntadjoint [OF PUA agree[OF assm] ssafe safe2 good_interp]
by auto
qed
done
have "((ν, ω) ∈ prog_sem I (PsubstFO (a ;; b) σ)) = (∃ μ. (ν, μ) ∈ prog_sem I (PsubstFO a σ) ∧ (μ, ω) ∈ prog_sem I (PsubstFO b σ))"
by auto
moreover have "... = (∃ μ. (ν, μ) ∈ prog_sem I (PsubstFO a σ) ∧ (μ, ω) ∈ prog_sem (adjointFO I σ μ) b)"
using IH2[OF safe2 ssafe] by auto
moreover have "... = (∃ μ. (ν, μ) ∈ prog_sem I (PsubstFO a σ) ∧ (μ, ω) ∈ prog_sem (adjointFO I σ ν) b)"
using sem_eq by auto
moreover have "... = (∃ μ. (ν, μ) ∈ prog_sem (adjointFO I σ ν) a ∧ (μ, ω) ∈ prog_sem (adjointFO I σ ν) b)"
using IH1[OF safe1 ssafe] by auto
ultimately
show "((ν, ω) ∈ prog_sem I (PsubstFO (a ;; b) σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) (a ;; b))"
by auto
qed
then show ?case by auto
next
case (NPadmit_Loop σ a) then
have PA:"NPadmit σ a"
and PUA:"PUadmitFO σ a (BVP (PsubstFO a σ))"
and IH:"hpsafe a ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PsubstFO a σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) a))"
and hpsafeS:"hpsafe (PsubstFO a σ)"
by auto
have "hpsafe (a**) ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PsubstFO (a**) σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) (a**)))"
proof -
assume "hpsafe (a**)"
then have hpsafe:"hpsafe a" by (auto dest: hpsafe.cases)
assume ssafe:"(⋀i. dsafe (σ i))"
have agree:"⋀ν μ. (ν, μ) ∈ prog_sem I (PsubstFO a σ) ⟹ Vagree ν μ (-BVP(PsubstFO a σ))"
subgoal for ν μ
using bound_effect[OF good_interp, of "(PsubstFO a σ)" ν, OF hpsafeS]
by auto
done
have sem_eq:"⋀ν μ ω. (ν, μ) ∈ prog_sem I (PsubstFO a σ) ⟹
((μ, ω) ∈ prog_sem (adjointFO I σ ν) a) =
((μ, ω) ∈ prog_sem (adjointFO I σ μ) a)"
subgoal for ν μ ω
proof -
assume assm:"(ν, μ) ∈ prog_sem I (PsubstFO a σ)"
show "((μ, ω) ∈ prog_sem (adjointFO I σ ν) a) = ((μ, ω) ∈ prog_sem (adjointFO I σ μ) a)"
using uadmit_prog_ntadjoint[OF PUA agree[OF assm] ssafe hpsafe good_interp] by auto
qed
done
fix ν ω
have UN_rule:"⋀ a S S'. (⋀n b. (a,b) ∈ S n ⟷ (a,b) ∈ S' n) ⟹ (⋀b. (a,b) ∈ (⋃n. S n) ⟷ (a,b) ∈ (⋃n. S' n))"
by auto
have eqL:"((ν, ω) ∈ prog_sem I (PsubstFO (a**) σ)) = ((ν, ω) ∈ (⋃n. (prog_sem I (PsubstFO a σ)) ^^ n))"
using rtrancl_is_UN_relpow by auto
moreover have eachEq:"⋀n. ((⋀ν ω. ((ν, ω) ∈ (prog_sem I (PsubstFO a σ)) ^^ n) = ((ν, ω) ∈ (prog_sem (adjointFO I σ ν) a)^^ n)))"
proof -
fix n
show "((⋀ν ω. ((ν, ω) ∈ (prog_sem I (PsubstFO a σ)) ^^ n) = ((ν, ω) ∈ (prog_sem (adjointFO I σ ν) a)^^ n)))"
proof (induct n)
case 0
then show ?case by auto
next
case (Suc n) then
have IH2:"⋀ν ω. ((ν, ω) ∈ prog_sem I (PsubstFO a σ) ^^ n) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) a ^^ n)"
by auto
have relpow:"⋀R n. R ^^ Suc n = R O R ^^ n"
using relpow.simps(2) relpow_commute by metis
show ?case
apply (simp only: relpow[of n "prog_sem I (PsubstFO a σ)"] relpow[of n "prog_sem (adjointFO I σ ν) a"])
apply(unfold relcomp_unfold)
apply auto
subgoal for ab b
apply(rule exI[where x=ab])
apply(rule exI[where x=b])
using IH2 IH[OF hpsafe ssafe] sem_eq[of ν "(ab,b)" ω] apply auto
using uadmit_prog_ntadjoint[OF PUA agree ssafe hpsafe good_interp] IH[OF hpsafe ssafe]
apply (metis (no_types, lifting))
using uadmit_prog_ntadjoint[OF PUA agree ssafe hpsafe good_interp] IH[OF hpsafe ssafe]
apply (metis (no_types, lifting))
done
subgoal for ab b
apply(rule exI[where x=ab])
apply(rule exI[where x=b])
using IH2 IH[OF hpsafe ssafe] sem_eq[of ν "(ab,b)" ω] apply auto
using uadmit_prog_ntadjoint[OF PUA agree ssafe hpsafe good_interp] IH[OF hpsafe ssafe]
apply (metis (no_types, lifting))
using uadmit_prog_ntadjoint[OF PUA agree ssafe hpsafe good_interp] IH[OF hpsafe ssafe]
apply (metis (no_types, lifting))
done
done
qed
qed
moreover have "((ν, ω) ∈ (⋃n. (prog_sem I (PsubstFO a σ)) ^^ n)) = ((ν, ω) ∈ (⋃ n.(prog_sem (adjointFO I σ ν) a)^^ n))"
apply(rule UN_rule)
using eachEq by auto
moreover have eqR:"((ν, ω) ∈ prog_sem (adjointFO I σ ν) (a**)) = ((ν, ω) ∈ (⋃n. (prog_sem (adjointFO I σ ν) a) ^^ n))"
using rtrancl_is_UN_relpow by auto
ultimately show "((ν, ω) ∈ prog_sem I (PsubstFO (a**) σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) (a**))"
by auto
qed
then show ?case by auto
next
case (NFadmit_Exists σ φ x)
then have IH:"fsafe φ ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν. (ν ∈ fml_sem I (FsubstFO φ σ)) = (ν ∈ fml_sem (adjointFO I σ ν) φ))"
and FUA:"FUadmitFO σ φ {Inl x}"
by blast+
have fsafe:"fsafe (Exists x φ) ⟹ fsafe φ"
by (auto dest: fsafe.cases)
have eq:"fsafe (Exists x φ) ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν. (ν ∈ fml_sem I (FsubstFO (Exists x φ) σ)) = (ν ∈ fml_sem (adjointFO I σ ν) (Exists x φ)))"
proof -
assume fsafe:"fsafe (Exists x φ)"
from fsafe have fsafe':"fsafe φ" by (auto dest: fsafe.cases)
assume ssafe:"(⋀i. dsafe (σ i))"
fix ν
have agree:"⋀r. Vagree ν (repv ν x r) (- {Inl x})"
unfolding Vagree_def by auto
have sem_eq:"⋀r. ((repv ν x r) ∈ fml_sem (adjointFO I σ (repv ν x r)) φ) =
((repv ν x r) ∈ fml_sem (adjointFO I σ ν) φ)"
using uadmit_fml_ntadjoint[OF FUA agree ssafe fsafe' good_interp] by auto
have "(ν ∈ fml_sem I (FsubstFO (Exists x φ) σ)) = (∃r. (repv ν x r) ∈ fml_sem I (FsubstFO φ σ))"
by auto
moreover have "... = (∃r. (repv ν x r) ∈ fml_sem (adjointFO I σ (repv ν x r)) φ)"
using IH[OF fsafe' ssafe] by auto
moreover have "... = (∃r. (repv ν x r) ∈ fml_sem (adjointFO I σ ν) φ)"
using sem_eq by auto
moreover have "... = (ν ∈ fml_sem (adjointFO I σ ν) (Exists x φ))"
by auto
ultimately show "(ν ∈ fml_sem I (FsubstFO (Exists x φ) σ)) = (ν ∈ fml_sem (adjointFO I σ ν) (Exists x φ))"
by auto
qed
then show ?case by auto
next
case (NFadmit_Diamond σ φ a) then
have PA:"NPadmit σ a"
and FUA:"FUadmitFO σ φ (BVP (PsubstFO a σ))"
and IH1:"fsafe φ ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν. (ν ∈ fml_sem I (FsubstFO φ σ)) = (ν ∈ fml_sem (adjointFO I σ ν) φ))"
and IH2:"hpsafe a ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PsubstFO a σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) a))"
and hpsafeF:"hpsafe (PsubstFO a σ)"
by auto
have "fsafe (⟨ a ⟩ φ) ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν. (ν ∈ fml_sem I (FsubstFO (⟨ a ⟩ φ) σ)) = (ν ∈ fml_sem (adjointFO I σ ν) (⟨ a ⟩ φ)))"
proof -
assume fsafe:"fsafe (⟨ a ⟩ φ)"
assume ssafe:"(⋀i. dsafe (σ i))"
from fsafe have fsafe':"fsafe φ" and hpsafe:"hpsafe a" by (auto dest: fsafe.cases)
fix ν
have agree:"⋀ω. (ν, ω) ∈ prog_sem I (PsubstFO a σ) ⟹ Vagree ν ω (-BVP(PsubstFO a σ))"
using bound_effect[OF good_interp, of "(PsubstFO a σ)" ν, OF hpsafeF] by auto
have sem_eq:"⋀ω. (ν, ω) ∈ prog_sem I (PsubstFO a σ) ⟹
(ω ∈ fml_sem (adjointFO I σ ν) φ) =
(ω ∈ fml_sem (adjointFO I σ ω) φ)"
using uadmit_fml_ntadjoint [OF FUA agree ssafe fsafe' good_interp] by auto
have "(ν ∈ fml_sem I (FsubstFO (⟨ a ⟩ φ) σ)) = (∃ ω. (ν, ω) ∈ prog_sem I (PsubstFO a σ) ∧ ω ∈ fml_sem I (FsubstFO φ σ))"
by auto
moreover have "... = (∃ ω. (ν, ω) ∈ prog_sem (adjointFO I σ ν) a ∧ ω ∈ fml_sem (adjointFO I σ ω) φ)"
using IH1[OF fsafe' ssafe] IH2[OF hpsafe ssafe, of ν] by auto
moreover have "... = (∃ ω. (ν, ω) ∈ prog_sem (adjointFO I σ ν) a ∧ ω ∈ fml_sem (adjointFO I σ ν) φ)"
using sem_eq IH2 hpsafe ssafe by blast
moreover have "... = (ν ∈ fml_sem (adjointFO I σ ν) (⟨ a ⟩ φ))"
by auto
ultimately show "?thesis ν" by auto
qed
then show ?case by auto
next
case (NFadmit_Context σ φ C) then
have FA:"NFadmit σ φ"
and FUA:"FUadmitFO σ φ UNIV"
and IH:"fsafe φ ⟹ (⋀i. dsafe (σ i)) ⟹ (⋀ν. (ν ∈ fml_sem I (FsubstFO φ σ)) = (ν ∈ fml_sem (adjointFO I σ ν) φ))"
by auto
have "fsafe (InContext C φ) ⟹
(⋀i. dsafe (σ i))⟹ (⋀ν. (ν ∈ fml_sem I (FsubstFO (InContext C φ) σ)) = (ν ∈ fml_sem (adjointFO I σ ν) (InContext C φ)))"
proof -
assume safe:"fsafe (InContext C φ)"
then have fsafe:"fsafe φ" by (auto dest: fsafe.cases)
assume ssafe:"⋀i. dsafe (σ i)"
fix ν
have Ieq:" Contexts (adjointFO I σ ν) C = Contexts I C"
unfolding adjointFO_def by auto
have IH':"⋀ν. (ν ∈ fml_sem I (FsubstFO φ σ)) = (ν ∈ fml_sem (adjointFO I σ ν) φ)"
using IH[OF fsafe ssafe] by auto
have agree:"⋀ω. Vagree ν ω (-UNIV)" unfolding Vagree_def by auto
have adj_eq:"⋀ω. fml_sem (adjointFO I σ ν) φ = fml_sem (adjointFO I σ ω) φ"
using uadmit_fml_ntadjoint[OF FUA agree ssafe fsafe good_interp] by auto
then have sem:"fml_sem I (FsubstFO φ σ) = fml_sem (adjointFO I σ ν) φ"
using IH' agree adj_eq by auto
show "?thesis ν" using Ieq sem by auto
qed
then show ?case by auto
qed (auto)
lemma nsubst_fml:
fixes I::"('sf, 'sc, 'sz) interp"
fixes ν::"'sz state"
assumes good_interp:"is_interp I"
assumes NFA:"NFadmit σ φ"
assumes fsafe:"fsafe φ"
assumes frees:"(∀i. dsafe (σ i))"
shows "(ν ∈ fml_sem I (FsubstFO φ σ)) = (ν ∈ fml_sem (adjointFO I σ ν) φ)"
using good_interp NFA fsafe frees
by (auto simp add: nsubst_hp_fml)
lemma nsubst_hp:
fixes I::"('sf, 'sc, 'sz) interp"
fixes ν::"'sz state"
assumes good_interp:"is_interp I"
assumes NPA:"NPadmit σ α"
assumes hpsafe:"hpsafe α"
assumes frees:"⋀i. dsafe (σ i)"
shows "((ν, ω) ∈ prog_sem I (PsubstFO α σ)) = ((ν, ω) ∈ prog_sem (adjointFO I σ ν) α)"
using good_interp NPA hpsafe frees nsubst_hp_fml by blast
lemma psubst_sterm:
fixes I::"('sf, 'sc, 'sz) interp"
assumes good_interp:"is_interp I"
shows "(sterm_sem I θ = sterm_sem (PFadjoint I σ) θ)"
proof (induction θ)
qed (auto simp add: PFadjoint_def)
lemma psubst_dterm:
fixes I::"('sf, 'sc, 'sz) interp"
assumes good_interp:"is_interp I"
shows "(dsafe θ ⟹ dterm_sem I θ = dterm_sem (PFadjoint I σ) θ)"
proof (induction θ)
case (Differential θ)
assume safe:"dsafe (Differential θ)"
from safe have free:"dfree θ" by auto
assume sem:"dsafe θ ⟹ dterm_sem I θ = dterm_sem (PFadjoint I σ) θ"
have "⋀ν. frechet I θ (fst ν) (snd ν) = frechet (PFadjoint I σ) θ (fst ν) (snd ν)"
apply(rule sterm_determines_frechet)
using good_interp free apply auto
subgoal unfolding is_interp_def PFadjoint_def by auto
using psubst_sterm[of I θ] by auto
then show "?case"
by (auto simp add: directional_derivative_def)
qed (auto simp add: PFadjoint_def)
lemma psubst_ode:
assumes good_interp:"is_interp I"
shows "ODE_sem I ODE = ODE_sem (PFadjoint I σ) ODE"
proof (induction "ODE")
case (OVar x)
then show ?case unfolding PFadjoint_def by auto
next
case (OSing x1a x2)
then show ?case apply auto apply (rule ext) apply (rule vec_extensionality) using psubst_sterm[OF good_interp, of x2 σ] by auto
next
case (OProd ODE1 ODE2)
then show ?case by auto
qed
lemma psubst_fml:
fixes I::"('sf, 'sc, 'sz) interp"
assumes good_interp:"is_interp I"
shows "(PPadmit σ α ⟶ hpsafe α ⟶ (∀i. fsafe (σ i)) ⟶ (∀ ν ω. (ν,ω) ∈ prog_sem I (PPsubst α σ) = ((ν,ω) ∈ prog_sem (PFadjoint I σ) α))) ∧
(PFadmit σ φ ⟶ fsafe φ ⟶ (∀i. fsafe (σ i)) ⟶ (∀ ν. ν ∈ fml_sem I (PFsubst φ σ) = (ν ∈ fml_sem (PFadjoint I σ) φ)))"
proof (induction rule: PPadmit_PFadmit.induct)
case (PPadmit_ODE σ φ ODE)
assume PF:"PFadmit σ φ"
assume PFU:"PFUadmit σ φ (BVO ODE)"
assume IH:"fsafe φ ⟶ (∀i. fsafe (σ i)) ⟶ (∀ν. (ν ∈ fml_sem I (PFsubst φ σ)) = (ν ∈ fml_sem (PFadjoint I σ) φ))"
have "hpsafe (EvolveODE ODE φ) ⟹
(∀i. fsafe (σ i)) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PPsubst (EvolveODE ODE φ) σ)) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) (EvolveODE ODE φ)))"
proof -
assume safe:"hpsafe (EvolveODE ODE φ)"
from safe have fsafe:"fsafe φ" by auto
assume ssafe:"(∀i. fsafe (σ i))"
have fml_eq:"⋀ν. (ν ∈ fml_sem I (PFsubst φ σ)) = (ν ∈ fml_sem (PFadjoint I σ) φ)"
using IH ssafe fsafe by auto
fix ν ω
show "((ν, ω) ∈ prog_sem I (PPsubst (EvolveODE ODE φ) σ)) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) (EvolveODE ODE φ))"
apply auto
proof -
fix b sol t
assume eq1:"ν = (sol 0, b)"
and eq2:"ω = mk_v I ODE (sol 0, b) (sol t)"
and t:"0 ≤ t"
and sol:"(sol solves_ode (λa. ODE_sem I ODE)) {0..t} {x. mk_v I ODE (sol 0, b) x ∈ fml_sem I (PFsubst φ σ)}"
have var:"ODE_vars I ODE = ODE_vars (PFadjoint I σ) ODE"
by(induction ODE, auto simp add: PFadjoint_def)
have mkv_eq:"⋀s. s ∈ {0..t} ⟹ mk_v I ODE (sol 0, b) (sol s) = mk_v (PFadjoint I σ) ODE (sol 0, b) (sol s)"
apply(rule agree_UNIV_eq)
unfolding Vagree_def apply auto
subgoal for s i
using mk_v_agree[of I ODE "(sol 0, b)" "sol s"] mk_v_agree[of "PFadjoint I σ" ODE "(sol 0, b)" "sol s"]
unfolding Vagree_def var
apply (cases "Inl i ∈ Inl ` ODE_vars I ODE", auto simp add: var)
by force
subgoal for s i
using mk_v_agree[of I ODE "(sol 0, b)" "sol s"] mk_v_agree[of "PFadjoint I σ" ODE "(sol 0, b)" "sol s"]
unfolding Vagree_def var
apply (cases "Inr i ∈ Inr ` ODE_vars I ODE", auto simp add: var psubst_ode)
using psubst_ode[OF good_interp, of ODE σ] apply auto
using psubst_ode[OF good_interp, of ODE σ] by force
done
have sol':"(sol solves_ode (λ_. ODE_sem (PFadjoint I σ) ODE)) {0..t}
{x. mk_v I ODE (sol 0, b) x ∈ fml_sem I (PFsubst φ σ)}"
apply (rule solves_ode_congI)
apply (rule sol)
subgoal for ta by auto
subgoal for ta using psubst_ode[OF good_interp, of ODE σ] by auto
subgoal by (rule refl)
subgoal by (rule refl)
done
have sub:"⋀s. s ∈ {0..t}
⟹ sol s ∈ {x. (mk_v (PFadjoint I σ ) ODE (sol 0, b) x ∈ fml_sem (PFadjoint I σ ) φ)}"
subgoal for s
using solves_ode_domainD[OF sol, of s] mkv_eq[of s] fml_eq[of "mk_v (PFadjoint I σ ) ODE (sol 0, b) (sol s)"]
by auto
done
have sol'':"(sol solves_ode (λc. ODE_sem (PFadjoint I σ ) ODE)) {0..t}
{x. mk_v (PFadjoint I σ) ODE (sol 0, b) x ∈ fml_sem (PFadjoint I σ ) φ}"
apply (rule solves_odeI)
subgoal using sol' solves_ode_vderivD by blast
using sub by auto
show"∃sola. sol 0 = sola 0 ∧
(∃ta. mk_v I ODE (sol 0, b) (sol t) = mk_v (PFadjoint I σ) ODE (sola 0, b) (sola ta) ∧
0 ≤ ta ∧
(sola solves_ode (λa. ODE_sem (PFadjoint I σ) ODE)) {0..ta}
{x. mk_v (PFadjoint I σ) ODE (sola 0, b) x ∈ fml_sem (PFadjoint I σ) φ})"
apply(rule exI[where x=sol])
apply(rule conjI)
apply(rule refl)
apply(rule exI[where x=t])
apply(rule conjI)
subgoal using mkv_eq t by auto
apply(rule conjI)
apply(rule t)
apply(rule sol'')
done
next
fix b sol t
assume eq1:"ν = (sol 0, b)"
and eq2:"ω = mk_v (PFadjoint I σ) ODE (sol 0, b) (sol t)"
and t:"0 ≤ t"
and sol:"(sol solves_ode (λa. ODE_sem (PFadjoint I σ) ODE)) {0..t} {x. mk_v (PFadjoint I σ) ODE (sol 0, b) x ∈ fml_sem (PFadjoint I σ) φ}"
have var:"ODE_vars I ODE = ODE_vars (PFadjoint I σ) ODE"
by(induction ODE, auto simp add: PFadjoint_def)
have mkv_eq:"⋀s. s ∈ {0..t} ⟹ mk_v I ODE (sol 0, b) (sol s) = mk_v (PFadjoint I σ) ODE (sol 0, b) (sol s)"
apply(rule agree_UNIV_eq)
unfolding Vagree_def apply auto
subgoal for s i
using mk_v_agree[of I ODE "(sol 0, b)" "sol s"] mk_v_agree[of "PFadjoint I σ" ODE "(sol 0, b)" "sol s"]
unfolding Vagree_def var
apply (cases "Inl i ∈ Inl ` ODE_vars I ODE", auto simp add: var)
by force
subgoal for s i
using mk_v_agree[of I ODE "(sol 0, b)" "sol s"] mk_v_agree[of "PFadjoint I σ" ODE "(sol 0, b)" "sol s"]
unfolding Vagree_def var
apply (cases "Inr i ∈ Inr ` ODE_vars I ODE", auto simp add: var psubst_ode)
using psubst_ode[OF good_interp, of ODE σ] apply auto
using psubst_ode[OF good_interp, of ODE σ] by force
done
have sol':"(sol solves_ode (λ_. ODE_sem I ODE)) {0..t}
{x. mk_v (PFadjoint I σ) ODE (sol 0, b) x ∈ fml_sem (PFadjoint I σ) φ}"
apply (rule solves_ode_congI)
apply (rule sol)
subgoal for ta by auto
subgoal for ta using psubst_ode[OF good_interp, of ODE σ] by auto
subgoal by (rule refl)
subgoal by (rule refl)
done
have sub:"⋀s. s ∈ {0..t}
⟹ sol s ∈ {x. (mk_v I ODE (sol 0, b) x ∈ fml_sem I (PFsubst φ σ))}"
subgoal for s
using solves_ode_domainD[OF sol, of s] mkv_eq[of s] fml_eq[of "mk_v (PFadjoint I σ ) ODE (sol 0, b) (sol s)"]
by auto
done
have sol'':"(sol solves_ode (λc. ODE_sem I ODE)) {0..t}
{x. mk_v I ODE (sol 0, b) x ∈ fml_sem I (PFsubst φ σ)}"
apply (rule solves_odeI)
subgoal using sol' solves_ode_vderivD by blast
using sub by auto
show "∃sola. sol 0 = sola 0 ∧
(∃ta. mk_v (PFadjoint I σ) ODE (sol 0, b) (sol t) = mk_v I ODE (sola 0, b) (sola ta) ∧
0 ≤ ta ∧ (sola solves_ode (λa. ODE_sem I ODE)) {0..ta} {x. mk_v I ODE (sola 0, b) x ∈ fml_sem I (PFsubst φ σ)})"
apply(rule exI[where x=sol])
by (metis dual_order.refl intervalE mkv_eq sol'' t)
qed
qed
then show ?case
by auto
next
case (PPadmit_Assign σ x θ)
have "hpsafe (x := θ) ⟹ (∀i. fsafe (σ i)) ⟹ (∀ ν ω. ((ν, ω) ∈ prog_sem I (PPsubst (x := θ) σ)) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) (x := θ)))"
proof -
assume safe:"hpsafe (x := θ)"
then have dsafe:"dsafe θ" by auto
assume safes:"(∀i. fsafe (σ i))"
show "?thesis"
using psubst_dterm[OF good_interp dsafe, of σ] by auto
qed
then show "?case" by auto
next
case (PPadmit_DiffAssign σ x θ)
have "hpsafe (DiffAssign x θ) ⟹ (∀i. fsafe (σ i)) ⟹ (∀ ν ω. ((ν, ω) ∈ prog_sem I (PPsubst (DiffAssign x θ) σ)) = (((ν, ω) ∈ prog_sem (PFadjoint I σ) (DiffAssign x θ))))"
proof -
assume safe:"hpsafe (DiffAssign x θ)"
then have dsafe:"dsafe θ" by auto
assume safes:"(∀i. fsafe (σ i))"
show "?thesis"
using psubst_dterm[OF good_interp dsafe, of σ] by auto
qed
then show ?case by auto
next
case (PFadmit_Geq σ θ1 θ2) then
have "fsafe (Geq θ1 θ2) ⟹ (∀i. fsafe (σ i)) ⟹ (∀ ν. (ν ∈ fml_sem I (PFsubst (Geq θ1 θ2) σ)) = (ν ∈ fml_sem (PFadjoint I σ) (Geq θ1 θ2)))"
proof -
assume safe:"fsafe (Geq θ1 θ2)"
then have safe1:"dsafe θ1"
and safe2:"dsafe θ2" by auto
assume safes:"(∀i. fsafe (σ i))"
show "?thesis"
using psubst_dterm[OF good_interp safe1, of σ] psubst_dterm[OF good_interp safe2, of σ] by auto
qed
then show ?case by auto
next
case (PFadmit_Prop σ p args) then
have "fsafe (Prop p args) ⟹ (⋀i. fsafe (σ i)) ⟹ (⋀ν.(ν ∈ fml_sem I (PFsubst ($φ p args) σ)) = (ν ∈ fml_sem (PFadjoint I σ) ($φ p args)))"
proof -
assume safe:"fsafe (Prop p args)" and ssafe:" (⋀i. fsafe (σ i))"
fix ν
from safe have safes:"⋀i. dsafe (args i)" using dfree_is_dsafe by auto
have Ieq:"Predicates I p = Predicates (PFadjoint I σ) p"
unfolding PFadjoint_def by auto
have vec:"(χ i. dterm_sem I (args i) ν) = (χ i. dterm_sem (PFadjoint I σ) (args i) ν)"
apply(auto simp add: vec_eq_iff)
subgoal for i using safes[of i]
by (metis good_interp psubst_dterm)
done
show "?thesis ν" using Ieq vec by auto
qed
then show "?case" by auto
next
case (PPadmit_Sequence σ a b) then
have PUA:"PPUadmit σ b (BVP (PPsubst a σ))"
and PA:"PPadmit σ a"
and IH1:"hpsafe a ⟹ (⋀i. fsafe (σ i)) ⟹ (∀ ν ω. ((ν, ω) ∈ prog_sem I (PPsubst a σ)) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) a))"
and IH2:"hpsafe b ⟹ (⋀i. fsafe (σ i)) ⟹ (∀ ν ω. ((ν, ω) ∈ prog_sem I (PPsubst b σ)) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) b))"
and substSafe:"hpsafe (PPsubst a σ)"
by auto
have "hpsafe (a ;; b) ⟹ (⋀i. fsafe (σ i)) ⟹ (⋀ ν ω. ((ν, ω) ∈ prog_sem I (PPsubst (a ;; b) σ)) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) (a ;; b)))"
proof -
assume hpsafe:"hpsafe (a ;; b)"
assume ssafe:"(⋀i. fsafe (σ i))"
from hpsafe have safe1:"hpsafe a" and safe2:"hpsafe b" by (auto dest: hpsafe.cases)
fix ν ω
have agree:"⋀μ. (ν, μ) ∈ prog_sem I (PPsubst a σ) ⟹ Vagree ν μ (-BVP(PPsubst a σ))"
subgoal for μ
using bound_effect[OF good_interp, of "(PPsubst a σ)" ν, OF substSafe] by auto
done
have sem_eq:"⋀μ. (ν, μ) ∈ prog_sem I (PPsubst a σ) ⟹
((μ, ω) ∈ prog_sem (PFadjoint I σ) b) =
((μ, ω) ∈ prog_sem (PFadjoint I σ) b)"
subgoal for μ
proof -
assume assm:"(ν, μ) ∈ prog_sem I (PPsubst a σ)"
show "((μ, ω) ∈ prog_sem (PFadjoint I σ) b) = ((μ, ω) ∈ prog_sem (PFadjoint I σ) b)"
using PUA agree[OF assm] safe2 ssafe good_interp by auto
qed
done
have "((ν, ω) ∈ prog_sem I (PPsubst (a ;; b) σ)) = (∃ μ. (ν, μ) ∈ prog_sem I (PPsubst a σ) ∧ (μ, ω) ∈ prog_sem I (PPsubst b σ))"
by auto
moreover have "... = (∃ μ. (ν, μ) ∈ prog_sem I (PPsubst a σ) ∧ (μ, ω) ∈ prog_sem (PFadjoint I σ) b)"
using IH2[OF safe2 ssafe] by blast
moreover have "... = (∃ μ. (ν, μ) ∈ prog_sem (PFadjoint I σ) a ∧ (μ, ω) ∈ prog_sem (PFadjoint I σ) b)"
using IH1[OF safe1 ssafe] sem_eq by blast
ultimately
show "((ν, ω) ∈ prog_sem I (PPsubst (a ;; b) σ)) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) (a ;; b))"
by auto
qed
then show ?case by auto
next
case (PPadmit_Loop σ a) then
have PA:"PPadmit σ a"
and PUA:"PPUadmit σ a (BVP (PPsubst a σ))"
and IH:"hpsafe a ⟹ (⋀i. fsafe (σ i)) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PPsubst a σ)) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) a))"
and substSafe:"hpsafe (PPsubst a σ)"
by auto
have "hpsafe (a**) ⟹ (⋀i. fsafe (σ i)) ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (PPsubst (a**) σ)) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) (a**)))"
proof -
assume "hpsafe (a**)"
then have hpsafe:"hpsafe a" by (auto dest: hpsafe.cases)
assume ssafe:"⋀i. fsafe (σ i)"
have agree:"⋀ν μ. (ν, μ) ∈ prog_sem I (PPsubst a σ) ⟹ Vagree ν μ (-BVP(PPsubst a σ))"
subgoal for ν μ
using bound_effect[OF good_interp, of "(PPsubst a σ)" ν, OF substSafe] by auto
done
fix ν ω
have UN_rule:"⋀ a S S'. (⋀n b. (a,b) ∈ S n ⟷ (a,b) ∈ S' n) ⟹ (⋀b. (a,b) ∈ (⋃n. S n) ⟷ (a,b) ∈ (⋃n. S' n))"
by auto
have eqL:"((ν, ω) ∈ prog_sem I (PPsubst (a**) σ)) = ((ν, ω) ∈ (⋃n. (prog_sem I (PPsubst a σ)) ^^ n))"
using rtrancl_is_UN_relpow by auto
moreover have eachEq:"⋀n. ((⋀ν ω. ((ν, ω) ∈ (prog_sem I (PPsubst a σ)) ^^ n) = ((ν, ω) ∈ (prog_sem (PFadjoint I σ) a)^^ n)))"
proof -
fix n
show "((⋀ν ω. ((ν, ω) ∈ (prog_sem I (PPsubst a σ)) ^^ n) = ((ν, ω) ∈ (prog_sem (PFadjoint I σ) a)^^ n)))"
proof (induct n)
case 0
then show ?case by auto
next
case (Suc n) then
have IH2:"⋀ν ω. ((ν, ω) ∈ prog_sem I (PPsubst a σ) ^^ n) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) a ^^ n)"
by auto
have relpow:"⋀R n. R ^^ Suc n = R O R ^^ n"
using relpow.simps(2) relpow_commute by metis
show ?case
apply (simp only: relpow[of n "prog_sem I (PPsubst a σ)"] relpow[of n "prog_sem (PFadjoint I σ) a"])
apply(unfold relcomp_unfold)
apply auto
subgoal for ab b
apply(rule exI[where x=ab])
apply(rule exI[where x=b])
using IH2 IH[OF hpsafe ssafe] by auto
subgoal for ab b
apply(rule exI[where x=ab])
apply(rule exI[where x=b])
using IH2 IH[OF hpsafe ssafe] by auto
done
qed
qed
moreover have "((ν, ω) ∈ (⋃n. (prog_sem I (PPsubst a σ)) ^^ n)) = ((ν, ω) ∈ (⋃ n.(prog_sem (PFadjoint I σ) a)^^ n))"
apply(rule UN_rule)
using eachEq by auto
moreover have eqR:"((ν, ω) ∈ prog_sem (PFadjoint I σ) (a**)) = ((ν, ω) ∈ (⋃n. (prog_sem (PFadjoint I σ) a) ^^ n))"
using rtrancl_is_UN_relpow by auto
ultimately show "((ν, ω) ∈ prog_sem I (PPsubst (a**) σ)) = ((ν, ω) ∈ prog_sem (PFadjoint I σ) (a**))"
by auto
qed
then show ?case by auto
next
next
case (PFadmit_Context σ φ C) then
have FA:"PFadmit σ φ"
and FUA:"PFUadmit σ φ UNIV"
and IH:"fsafe φ ⟹ (⋀i. fsafe (σ i)) ⟹ (⋀ν. (ν ∈ fml_sem I (PFsubst φ σ)) = (ν ∈ fml_sem (PFadjoint I σ) φ))"
by auto
have "fsafe (InContext C φ) ⟹
(⋀i. fsafe (σ i)) ⟹ (⋀ν. (ν ∈ fml_sem I (PFsubst (InContext C φ) σ)) = (ν ∈ fml_sem (PFadjoint I σ) (InContext C φ)))"
proof -
assume safe:"fsafe (InContext C φ)"
then have fsafe:"fsafe φ" by (auto dest: fsafe.cases)
assume ssafe:"(⋀i. fsafe (σ i))"
fix ν :: "(real, 'sz) vec × (real, 'sz) vec"
have IH':"⋀ν. (ν ∈ fml_sem I (PFsubst φ σ)) = (ν ∈ fml_sem (PFadjoint I σ) φ)"
using IH[OF fsafe ssafe] by auto
have agree:"⋀ω. Vagree ν ω (-UNIV)" unfolding Vagree_def by auto
then have sem:"fml_sem I (PFsubst φ σ) = fml_sem (PFadjoint I σ) φ"
using IH' agree by auto
show "?thesis ν" using sem
apply auto
apply(cases C)
unfolding PFadjoint_def apply auto
apply(cases C)
by auto
qed
then show ?case by auto
qed (auto simp add: PFadjoint_def)
lemma subst_ode:
fixes I:: "('sf, 'sc, 'sz) interp" and ν :: "'sz state"
assumes good_interp:"is_interp I"
shows "osafe ODE ⟹
ssafe σ ⟹
Oadmit σ ODE (BVO ODE) ⟹
ODE_sem I (Osubst ODE σ) (fst ν) = ODE_sem (adjoint I σ ν) ODE (fst ν)"
proof (induction rule: osafe.induct)
case (osafe_Var c)
then show ?case unfolding adjoint_def by (cases "SODEs σ c", auto)
next
case (osafe_Sing θ x)
then show ?case
using subst_sterm [of σ θ I "ν"]
unfolding ssafe_def by auto
next
case (osafe_Prod ODE1 ODE2) then
have NOU1:"Oadmit σ ODE1 (BVO (OProd ODE1 ODE2))" and NOU2:"Oadmit σ ODE2 (BVO (OProd ODE1 ODE2))"
by auto
have TUA_sub:"⋀σ θ A B. TUadmit σ θ B ⟹ A ⊆ B ⟹ TUadmit σ θ A"
unfolding TUadmit_def by auto
have OA_sub:"⋀ODE A B. Oadmit σ ODE B ⟹ A ⊆ B ⟹ Oadmit σ ODE A"
subgoal for ODE A B
proof (induction rule: Oadmit.induct)
case (Oadmit_Var σ c U)
then show ?case by auto
next
case (Oadmit_Sing σ θ U x)
then show ?case using TUA_sub[of σ θ U A] by auto
next
case (Oadmit_Prod σ ODE1 U ODE2)
then show ?case by auto
qed
done
have sub1:"(BVO ODE1) ⊆ (BVO (OProd ODE1 ODE2))"
by auto
have sub2: "(BVO ODE2) ⊆ (BVO (OProd ODE1 ODE2))"
by auto
have "ODE_sem I (Osubst ODE1 σ) (fst ν) = ODE_sem (adjoint I σ ν) ODE1 (fst ν)"
"ODE_sem I (Osubst ODE2 σ) (fst ν) = ODE_sem (adjoint I σ ν) ODE2 (fst ν)" using osafe_Prod.IH osafe_Prod.prems osafe_Prod.hyps
using OA_sub[OF NOU1 sub1] OA_sub[OF NOU2 sub2] by auto
then show ?case by auto
qed
lemma osubst_eq_ODE_vars: "ODE_vars I (Osubst ODE σ) = ODE_vars (adjoint I σ ν) ODE"
proof (induction ODE)
case (OVar x)
then show ?case by (cases "SODEs σ x", auto simp add: adjoint_def)
qed (auto)
lemma subst_semBV:"semBV (adjoint I σ ν') ODE = (semBV I (Osubst ODE σ))"
proof (induction ODE)
case (OVar x)
then show ?case by (cases "SODEs σ x", auto simp add: adjoint_def)
qed (auto)
lemma subst_mkv:
fixes I::"('sf, 'sc, 'sz) interp"
fixes ν::"'sz state"
fixes ν'::"'sz state"
assumes good_interp:"is_interp I"
assumes NOU:"Oadmit σ ODE (BVO ODE)"
assumes osafe:"osafe ODE "
assumes frees:"ssafe σ"
shows "(mk_v I (Osubst ODE σ) ν (fst ν'))
= (mk_v (adjoint I σ ν') ODE ν (fst ν'))"
apply(rule agree_UNIV_eq)
using mk_v_agree[of "adjoint I σ ν'" "ODE" ν "fst ν'"]
using mk_v_agree[of "I" "Osubst ODE σ" ν "fst ν'"]
unfolding Vagree_def
using subst_ode[OF good_interp osafe frees NOU, of ν']
apply auto
subgoal for i
apply(erule allE[where x=i])+
apply(cases "Inl i ∈ Inl ` ODE_vars (adjoint I σ ν') ODE")
using osubst_eq_ODE_vars[of I ODE σ ν']
apply force
proof -
assume "ODE_sem I (Osubst ODE σ) (fst ν') = ODE_sem (local.adjoint I σ ν') ODE (fst ν')"
"Inl i ∉ Inl ` ODE_vars (local.adjoint I σ ν') ODE ∧ Inl i ∉ Inr ` ODE_vars (local.adjoint I σ ν') ODE ⟶
fst (mk_v (local.adjoint I σ ν') ODE ν (fst ν')) $ i = fst ν $ i"
"Inl i ∉ Inl ` ODE_vars I (Osubst ODE σ) ∧ Inl i ∉ Inr ` ODE_vars I (Osubst ODE σ) ⟶
fst (mk_v I (Osubst ODE σ) ν (fst ν')) $ i = fst ν $ i"
"Inl i ∉ Inl ` ODE_vars (local.adjoint I σ ν') ODE"
then show
"fst (mk_v I (Osubst ODE σ) ν (fst ν')) $ i = fst (mk_v (local.adjoint I σ ν') ODE ν (fst ν')) $ i"
using osubst_eq_ODE_vars[of I ODE σ ν'] by force
qed
subgoal for i
apply(erule allE[where x=i])+
apply(cases "Inr i ∈ Inr ` ODE_vars (adjoint I σ ν') ODE")
using osubst_eq_ODE_vars[of I ODE σ ν']
apply force
proof -
assume "ODE_sem I (Osubst ODE σ) (fst ν') = ODE_sem (local.adjoint I σ ν') ODE (fst ν')"
"Inr i ∉ Inl ` ODE_vars (local.adjoint I σ ν') ODE ∧ Inr i ∉ Inr ` ODE_vars (local.adjoint I σ ν') ODE ⟶
snd (mk_v (local.adjoint I σ ν') ODE ν (fst ν')) $ i = snd ν $ i"
"Inr i ∉ Inl ` ODE_vars I (Osubst ODE σ) ∧ Inr i ∉ Inr ` ODE_vars I (Osubst ODE σ) ⟶
snd (mk_v I (Osubst ODE σ) ν (fst ν')) $ i = snd ν $ i"
"Inr i ∉ Inr ` ODE_vars (local.adjoint I σ ν') ODE"
then show "snd (mk_v I (Osubst ODE σ) ν (fst ν')) $ i = snd (mk_v (local.adjoint I σ ν') ODE ν (fst ν')) $ i"
using osubst_eq_ODE_vars[of I ODE σ ν'] by force
qed
done
lemma subst_fml_hp:
fixes I::"('sf, 'sc, 'sz) interp"
assumes good_interp:"is_interp I"
shows
"(Padmit σ α ⟶
(hpsafe α ⟶
ssafe σ ⟶
(∀ ν ω. ((ν, ω) ∈ prog_sem I (Psubst α σ)) = ((ν, ω) ∈ prog_sem (adjoint I σ ν) α))))
∧
(Fadmit σ φ ⟶
(fsafe φ ⟶
ssafe σ ⟶
(∀ ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (adjoint I σ ν) φ))))"
proof (induction rule: Padmit_Fadmit.induct)
case (Padmit_Pvar σ a) then
have "hpsafe ($α a) ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst ($α a) σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) ($α a)))"
apply (cases "SPrograms σ a")
unfolding adjoint_def by auto
then show ?case by auto
next
case (Padmit_Sequence σ a b) then
have PUA:"PUadmit σ b (BVP (Psubst a σ))"
and PA:"Padmit σ a"
and IH1:"hpsafe a ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst a σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) a))"
and IH2:"hpsafe b ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst b σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) b))"
and substSafe:"hpsafe (Psubst a σ)"
by auto
have "hpsafe (a ;; b) ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst (a ;; b) σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) (a ;; b)))"
proof -
assume hpsafe:"hpsafe (a ;; b)"
assume ssafe:"ssafe σ"
from hpsafe have safe1:"hpsafe a" and safe2:"hpsafe b" by (auto dest: hpsafe.cases)
fix ν ω
have agree:"⋀μ. (ν, μ) ∈ prog_sem I (Psubst a σ) ⟹ Vagree ν μ (-BVP(Psubst a σ))"
subgoal for μ
using bound_effect[OF good_interp, of "(Psubst a σ)" ν, OF substSafe] by auto
done
have sem_eq:"⋀μ. (ν, μ) ∈ prog_sem I (Psubst a σ) ⟹
((μ, ω) ∈ prog_sem (local.adjoint I σ ν) b) =
((μ, ω) ∈ prog_sem (local.adjoint I σ μ) b)"
subgoal for μ
proof -
assume assm:"(ν, μ) ∈ prog_sem I (Psubst a σ)"
show "((μ, ω) ∈ prog_sem (local.adjoint I σ ν) b) = ((μ, ω) ∈ prog_sem (local.adjoint I σ μ) b)"
using uadmit_prog_adjoint[OF PUA agree[OF assm] safe2 ssafe good_interp] by auto
qed
done
have "((ν, ω) ∈ prog_sem I (Psubst (a ;; b) σ)) = (∃ μ. (ν, μ) ∈ prog_sem I (Psubst a σ) ∧ (μ, ω) ∈ prog_sem I (Psubst b σ))"
by auto
moreover have "... = (∃ μ. (ν, μ) ∈ prog_sem I (Psubst a σ) ∧ (μ, ω) ∈ prog_sem (adjoint I σ μ) b)"
using IH2[OF safe2 ssafe] by auto
moreover have "... = (∃ μ. (ν, μ) ∈ prog_sem I (Psubst a σ) ∧ (μ, ω) ∈ prog_sem (adjoint I σ ν) b)"
using sem_eq by auto
moreover have "... = (∃ μ. (ν, μ) ∈ prog_sem (adjoint I σ ν) a ∧ (μ, ω) ∈ prog_sem (adjoint I σ ν) b)"
using IH1[OF safe1 ssafe] by auto
ultimately
show "((ν, ω) ∈ prog_sem I (Psubst (a ;; b) σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) (a ;; b))"
by auto
qed
then show ?case by auto
next
case (Padmit_Loop σ a) then
have PA:"Padmit σ a"
and PUA:"PUadmit σ a (BVP (Psubst a σ))"
and IH:"hpsafe a ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst a σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) a))"
and substSafe:"hpsafe (Psubst a σ)"
by auto
have "hpsafe (a**) ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst (a**) σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) (a**)))"
proof -
assume "hpsafe (a**)"
then have hpsafe:"hpsafe a" by (auto dest: hpsafe.cases)
assume ssafe:"ssafe σ"
have agree:"⋀ν μ. (ν, μ) ∈ prog_sem I (Psubst a σ) ⟹ Vagree ν μ (-BVP(Psubst a σ))"
subgoal for ν μ
using bound_effect[OF good_interp, of "(Psubst a σ)" ν, OF substSafe] by auto
done
have sem_eq:"⋀ν μ ω. (ν, μ) ∈ prog_sem I (Psubst a σ) ⟹
((μ, ω) ∈ prog_sem (local.adjoint I σ ν) a) =
((μ, ω) ∈ prog_sem (local.adjoint I σ μ) a)"
subgoal for ν μ ω
proof -
assume assm:"(ν, μ) ∈ prog_sem I (Psubst a σ)"
show "((μ, ω) ∈ prog_sem (local.adjoint I σ ν) a) = ((μ, ω) ∈ prog_sem (local.adjoint I σ μ) a)"
using uadmit_prog_adjoint[OF PUA agree[OF assm] hpsafe ssafe good_interp] by auto
qed
done
fix ν ω
have UN_rule:"⋀ a S S'. (⋀n b. (a,b) ∈ S n ⟷ (a,b) ∈ S' n) ⟹ (⋀b. (a,b) ∈ (⋃n. S n) ⟷ (a,b) ∈ (⋃n. S' n))"
by auto
have eqL:"((ν, ω) ∈ prog_sem I (Psubst (a**) σ)) = ((ν, ω) ∈ (⋃n. (prog_sem I (Psubst a σ)) ^^ n))"
using rtrancl_is_UN_relpow by auto
moreover have eachEq:"⋀n. ((⋀ν ω. ((ν, ω) ∈ (prog_sem I (Psubst a σ)) ^^ n) = ((ν, ω) ∈ (prog_sem (adjoint I σ ν) a)^^ n)))"
proof -
fix n
show "((⋀ν ω. ((ν, ω) ∈ (prog_sem I (Psubst a σ)) ^^ n) = ((ν, ω) ∈ (prog_sem (adjoint I σ ν) a)^^ n)))"
proof (induct n)
case 0
then show ?case by auto
next
case (Suc n) then
have IH2:"⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst a σ) ^^ n) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) a ^^ n)"
by auto
have relpow:"⋀R n. R ^^ Suc n = R O R ^^ n"
using relpow.simps(2) relpow_commute by metis
show ?case
apply (simp only: relpow[of n "prog_sem I (Psubst a σ)"] relpow[of n "prog_sem (adjoint I σ ν) a"])
apply(unfold relcomp_unfold)
apply auto
subgoal for ab b
apply(rule exI[where x=ab])
apply(rule exI[where x=b])
using IH2 IH[OF hpsafe ssafe] sem_eq[of ν "(ab,b)" ω] apply auto
using uadmit_prog_adjoint[OF PUA agree hpsafe ssafe good_interp] IH[OF hpsafe ssafe]
apply (metis (no_types, lifting))
using uadmit_prog_adjoint[OF PUA agree hpsafe ssafe good_interp] IH[OF hpsafe ssafe]
apply (metis (no_types, lifting))
done
subgoal for ab b
apply(rule exI[where x=ab])
apply(rule exI[where x=b])
using IH2 IH[OF hpsafe ssafe] sem_eq[of ν "(ab,b)" ω] apply auto
using uadmit_prog_adjoint[OF PUA agree hpsafe ssafe good_interp] IH[OF hpsafe ssafe]
apply (metis (no_types, lifting))
using uadmit_prog_adjoint[OF PUA agree hpsafe ssafe good_interp] IH[OF hpsafe ssafe]
apply (metis (no_types, lifting))
done
done
qed
qed
moreover have "((ν, ω) ∈ (⋃n. (prog_sem I (Psubst a σ)) ^^ n)) = ((ν, ω) ∈ (⋃ n.(prog_sem (adjoint I σ ν) a)^^ n))"
apply(rule UN_rule)
using eachEq by auto
moreover have eqR:"((ν, ω) ∈ prog_sem (adjoint I σ ν) (a**)) = ((ν, ω) ∈ (⋃n. (prog_sem (adjoint I σ ν) a) ^^ n))"
using rtrancl_is_UN_relpow by auto
ultimately show "((ν, ω) ∈ prog_sem I (Psubst (a**) σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) (a**))"
by auto
qed
then show ?case by auto
next
case (Padmit_ODE σ ODE φ) then
have OA:"Oadmit σ ODE (BVO ODE)"
and FA:"Fadmit σ φ"
and FUA:"FUadmit σ φ (BVO ODE)"
and IH:"fsafe φ ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) φ))"
by auto
have "hpsafe (EvolveODE ODE φ) ⟹
ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst (EvolveODE ODE φ) σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) (EvolveODE ODE φ)))"
proof (auto)
fix aa ba bb
and sol :: "real ⇒(real, 'sz) vec"
and t :: real
assume ssafe:"ssafe σ"
assume osafe:"osafe ODE"
assume fsafe:"fsafe φ"
assume t:"0 ≤ t"
assume eq:"(aa,ba) = mk_v I (Osubst ODE σ) (sol 0, bb) (sol t)"
assume sol:"(sol solves_ode (λa. ODE_sem I (Osubst ODE σ))) {0..t}
{x. mk_v I (Osubst ODE σ) (sol 0, bb) x ∈ fml_sem I (Fsubst φ σ)}"
have silly:"
⋀t. mk_v I (Osubst ODE σ) (sol 0, bb) (sol t) = mk_v (local.adjoint I σ (sol t, bb)) ODE (sol 0, bb) (sol t)"
subgoal for t using subst_mkv[OF good_interp OA osafe ssafe, of "(sol 0, bb)" "(sol t, bb)"] by auto done
have hmmsubst:"⋀s. s ∈ {0..t} ⟹ Vagree (sol 0,bb) (sol s, bb) (-(BVO (Osubst ODE σ)))"
subgoal for s
apply (rule ODE_bound_effect[of s])
apply auto[1]
by (rule sol)
done
have sub:"(-(BVO ODE)) ⊆ (-(BVO (Osubst ODE σ)))"
by(induction ODE, auto)
have hmm:"⋀s. s ∈ {0..t} ⟹ Vagree (sol 0,bb) (sol s, bb) (-(BVO ODE))"
subgoal for s
using agree_sub[OF sub hmmsubst[of s]] by auto
done
from hmm have hmm':"⋀s. s ∈ {0..t} ⟹ VSagree (sol 0) (sol s) {x. Inl x ∈ (-(BVO ODE))}"
unfolding VSagree_def Vagree_def by auto
note hmmm = hmmsubst
from hmmm have hmmm':"⋀s. s ∈ {0..t} ⟹ VSagree (sol 0) (sol s) {x. Inl x ∈ (-(BVO (Osubst ODE σ)))}"
unfolding VSagree_def Vagree_def by auto
have Vagree_of_VSagree:"⋀ν1 ν2 ω1 ω2 S. VSagree ν1 ν2 {x. Inl x ∈ S} ⟹ VSagree ω1 ω2 {x. Inr x ∈ S} ⟹ Vagree (ν1, ω1) (ν2, ω2) S"
unfolding VSagree_def Vagree_def by auto
have mkv:"⋀s. s ∈ {0..t} ⟹ mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol s, bb)) ODE (sol 0, bb) (sol s)"
subgoal for s by (rule silly[of s])
done
have lem:"⋀ODE. Oadmit σ ODE (BVO ODE) ⟹ (⋃i∈{i |i. Inl i ∈ SIGO ODE}. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x) ⊆ (-(BVO ODE))"
subgoal for ODE
apply(induction rule: Oadmit.induct)
apply auto
subgoal for σ θ U x xa
apply (cases "SFunctions σ xa")
apply auto
unfolding TUadmit_def
proof -
fix a
assume un:"(⋃i∈SIGT θ. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x) ∩ U = {}"
assume sig:"xa ∈ SIGT θ"
assume some:"SFunctions σ xa = Some a"
assume fvt:"x ∈ FVT a"
assume xU:"x ∈ U"
from un sig have "(case SFunctions σ xa of None ⇒ {} | Some x ⇒ FVT x) ∩ U = {}"
by auto
then have "(FVT a) ∩ U = {}"
using some by auto
then show "False" using fvt xU by auto
qed
done
done
have FVT_sub:"(⋃i∈{i |i. Inl i ∈ SIGO ODE}. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x) ⊆ (-(BVO ODE))"
using lem[OF OA] by auto
have agrees: "⋀s. s ∈ {0..t} ⟹ Vagree (sol 0,bb) (sol s, bb) (⋃i∈{i |i. Inl i ∈ SIGO ODE}. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x)"
subgoal for s using agree_sub[OF FVT_sub hmm[of s]] by auto done
have "⋀s. s ∈ {0..t} ⟹ mk_v (adjoint I σ (sol 0, bb)) ODE = mk_v (adjoint I σ (sol s, bb)) ODE"
subgoal for s
apply (rule uadmit_mkv_adjoint)
prefer 3
subgoal using agrees by auto
using OA hmm[of s] unfolding Vagree_def
using ssafe good_interp osafe by auto
done
then have mkva:"⋀s. s ∈ {0..t} ⟹ mk_v (adjoint I σ (sol s, bb)) ODE (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s)"
by presburger
have main_eq:"⋀s. s ∈ {0..t} ⟹ mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s) "
using mkv mkva by auto
note mkvt = main_eq[of t]
have fml_eq1:"⋀s. s ∈ {0..t} ⟹
(mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem I (Fsubst φ σ))
= (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ)"
using IH[OF fsafe ssafe] by auto
have fml_vagree:"⋀s. s ∈ {0..t} ⟹ Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- semBV I (Osubst ODE σ))"
subgoal for s
using mk_v_agree[of I "Osubst ODE σ" "(sol 0,bb)" "sol s"] osubst_eq_ODE_vars[of I ODE σ]
unfolding Vagree_def
by auto
done
have sembv_eq:"semBV I (Osubst ODE σ) = semBV (adjoint I σ (sol 0, bb)) ODE"
using subst_semBV by auto
have fml_vagree':"⋀s. s ∈ {0..t} ⟹ Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- semBV (adjoint I σ (sol 0,bb)) ODE)"
using sembv_eq fml_vagree by auto
have mysub:"-BVO ODE ⊆ -(semBV I (Osubst ODE σ))"
by(induction ODE,auto)
have fml_vagree:"⋀s. s ∈ {0..t} ⟹ Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- BVO ODE)"
subgoal for s using agree_sub[OF mysub fml_vagree[of s]] by auto done
have fml_sem_eq:"⋀s. s ∈ {0..t} ⟹ fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ = fml_sem (adjoint I σ (sol 0, bb)) φ"
apply (rule uadmit_fml_adjoint)
using FUA fsafe ssafe good_interp fml_vagree by auto
have fml_eq2:"⋀s. s ∈ {0..t} ⟹
((mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ)
=(mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (sol 0, bb)) φ))"
using fml_sem_eq by auto
have fml_eq3:"⋀s. s ∈ {0..t} ⟹
(mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (sol 0, bb)) φ) = (mk_v (adjoint I σ (sol 0,bb)) ODE (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (sol 0, bb)) φ) "
using main_eq by auto
have fml_eq: "⋀s. s ∈ {0..t} ⟹
(mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem I (Fsubst φ σ))
= (mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (sol 0, bb)) φ)"
using fml_eq1 fml_eq2 fml_eq3 by meson
have sem_eq:"⋀t. ODE_sem I (Osubst ODE σ) (sol t) = ODE_sem (adjoint I σ (sol t, bb)) ODE (sol t)"
subgoal for t
using subst_ode[OF good_interp osafe ssafe OA, of "(sol t,bb)"] by auto
done
have sem_fact:"⋀s. s ∈ {0..t} ⟹ ODE_sem I (Osubst ODE σ) (sol s) = ODE_sem (adjoint I σ (sol 0, bb)) ODE (sol s)"
subgoal for s
using subst_ode[OF good_interp osafe ssafe OA, of "(sol s, bb)"]
uadmit_ode_adjoint'[OF ssafe good_interp agrees[of s] osafe]
by auto
done
have sol':"(sol solves_ode (λ_. ODE_sem (adjoint I σ (sol 0, bb)) ODE)) {0..t}
{x. mk_v I (Osubst ODE σ) (sol 0, bb) x ∈ fml_sem I (Fsubst φ σ)}"
apply (rule solves_ode_congI)
apply (rule sol)
subgoal for ta by auto
subgoal for ta by (rule sem_fact[of ta])
subgoal by (rule refl)
subgoal by (rule refl)
done
have sub:"⋀s. s ∈ {0..t}
⟹ sol s ∈ {x. (mk_v (adjoint I σ (sol 0,bb)) ODE (sol 0, bb) x ∈ fml_sem (adjoint I σ (sol 0, bb)) φ)}"
using fml_eq rangeI t sol solves_ode_domainD by fastforce
have sol'':"(sol solves_ode (λc. ODE_sem (adjoint I σ (sol 0, bb)) ODE)) {0..t}
{x. mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) x ∈ fml_sem (adjoint I σ (sol 0, bb)) φ}"
apply (rule solves_odeI)
subgoal using sol' solves_ode_vderivD by blast
using sub by auto
show "∃sola. sol 0 = sola 0 ∧
(∃ta. mk_v I (Osubst ODE σ) (sol 0, bb) (sol t) = mk_v (local.adjoint I σ (sol 0, bb)) ODE (sola 0, bb) (sola ta) ∧
0 ≤ ta ∧
(sola solves_ode (λa. ODE_sem (local.adjoint I σ (sol 0, bb)) ODE)) {0..ta}
{x. mk_v (local.adjoint I σ (sol 0, bb)) ODE (sola 0, bb) x ∈ fml_sem (local.adjoint I σ (sol 0, bb)) φ})"
apply(rule exI[where x=sol])
apply(rule conjI)
subgoal by (rule refl)
apply(rule exI[where x=t])
apply(rule conjI)
subgoal using mkvt t by auto
apply(rule conjI)
subgoal by (rule t)
subgoal by (rule sol'')
done
next
fix aa ba bb
and sol::"real ⇒ (real, 'sz) vec"
and t::real
assume ssafe:"ssafe σ"
assume osafe:"osafe ODE"
assume fsafe:"fsafe φ"
assume eq:"(aa,ba) = mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol t)"
assume t:"0 ≤ t"
assume sol:"(sol solves_ode (λa. ODE_sem (adjoint I σ (sol 0, bb)) ODE)) {0..t}
{x. mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) x ∈ fml_sem (adjoint I σ (sol 0, bb)) φ}"
have silly:"
⋀t. mk_v I (Osubst ODE σ) (sol 0, bb) (sol t) = mk_v (local.adjoint I σ (sol t, bb)) ODE (sol 0, bb) (sol t)"
subgoal for t using subst_mkv[OF good_interp OA osafe ssafe, of "(sol 0, bb)" "(sol t, bb)"] by auto done
have hmm:"⋀s. s ∈ {0..t} ⟹ Vagree (sol 0,bb) (sol s, bb) (-(BVO ODE))"
subgoal for s
apply (rule ODE_bound_effect[of s])
apply auto[1]
by (rule sol)
done
from hmm have hmm':"⋀s. s ∈ {0..t} ⟹ VSagree (sol 0) (sol s) {x. Inl x ∈ (-(BVO ODE))}"
unfolding VSagree_def Vagree_def by auto
have Vagree_of_VSagree:"⋀ν1 ν2 ω1 ω2 S. VSagree ν1 ν2 {x. Inl x ∈ S} ⟹ VSagree ω1 ω2 {x. Inr x ∈ S} ⟹ Vagree (ν1, ω1) (ν2, ω2) S"
unfolding VSagree_def Vagree_def by auto
have mkv:"⋀s. s ∈ {0..t} ⟹ mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol s, bb)) ODE (sol 0, bb) (sol s)"
subgoal for s by (rule silly[of s])
done
have lem:"⋀ODE. Oadmit σ ODE (BVO ODE) ⟹ (⋃i∈{i |i. Inl i ∈ SIGO ODE}. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x) ⊆ (-(BVO ODE))"
subgoal for ODE
apply(induction rule: Oadmit.induct)
apply auto
subgoal for σ θ U x xa
apply (cases "SFunctions σ xa")
apply auto
unfolding TUadmit_def
proof -
fix a
assume un:"(⋃i∈SIGT θ. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x) ∩ U = {}"
assume sig:"xa ∈ SIGT θ"
assume some:"SFunctions σ xa = Some a"
assume fvt:"x ∈ FVT a"
assume xU:"x ∈ U"
from un sig have "(case SFunctions σ xa of None ⇒ {} | Some x ⇒ FVT x) ∩ U = {}"
by auto
then have "(FVT a) ∩ U = {}"
using some by auto
then show "False" using fvt xU by auto
qed
done
done
have FVT_sub:"(⋃i∈{i |i. Inl i ∈ SIGO ODE}. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x) ⊆ (-(BVO ODE))"
using lem[OF OA] by auto
have agrees: "⋀s. s ∈ {0..t} ⟹ Vagree (sol 0,bb) (sol s, bb) (⋃i∈{i |i. Inl i ∈ SIGO ODE}. case SFunctions σ i of None ⇒ {} | Some x ⇒ FVT x)"
subgoal for s using agree_sub[OF FVT_sub hmm[of s]] by auto done
have "⋀s. s ∈ {0..t} ⟹ mk_v (adjoint I σ (sol 0, bb)) ODE = mk_v (adjoint I σ (sol s, bb)) ODE"
subgoal for s
apply (rule uadmit_mkv_adjoint)
prefer 3
subgoal using agrees by auto
using OA hmm[of s] unfolding Vagree_def
using ssafe good_interp osafe by auto
done
then have mkva:"⋀s. s ∈ {0..t} ⟹ mk_v (adjoint I σ (sol s, bb)) ODE (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s)"
by presburger
have main_eq:"⋀s. s ∈ {0..t} ⟹ mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) = mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s) "
using mkv mkva by auto
note mkvt = main_eq[of t]
have fml_eq1:"⋀s. s ∈ {0..t} ⟹
(mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem I (Fsubst φ σ))
= (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ)"
using IH[OF fsafe ssafe] by auto
have fml_vagree:"⋀s. s ∈ {0..t} ⟹ Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- semBV I (Osubst ODE σ))"
subgoal for s
using mk_v_agree[of I "Osubst ODE σ" "(sol 0,bb)" "sol s"] osubst_eq_ODE_vars[of I ODE σ]
unfolding Vagree_def
by auto
done
have sembv_eq:"semBV I (Osubst ODE σ) = semBV (adjoint I σ (sol 0, bb)) ODE"
using subst_semBV by auto
have fml_vagree':"⋀s. s ∈ {0..t} ⟹ Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- semBV (adjoint I σ (sol 0,bb)) ODE)"
using sembv_eq fml_vagree by auto
have mysub:"-BVO ODE ⊆ -(semBV I (Osubst ODE σ))"
by(induction ODE,auto)
have fml_vagree:"⋀s. s ∈ {0..t} ⟹ Vagree (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s)) (sol 0, bb) (- BVO ODE)"
subgoal for s using agree_sub[OF mysub fml_vagree[of s]] by auto done
have fml_sem_eq:"⋀s. s ∈ {0..t} ⟹ fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ = fml_sem (adjoint I σ (sol 0, bb)) φ"
apply (rule uadmit_fml_adjoint)
using FUA fsafe ssafe good_interp fml_vagree by auto
have fml_eq2:"⋀s. s ∈ {0..t} ⟹
((mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (mk_v I (Osubst ODE σ) (sol 0, bb) (sol s))) φ)
=(mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (sol 0, bb)) φ))"
using fml_sem_eq by auto
have fml_eq3:"⋀s. s ∈ {0..t} ⟹
(mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (sol 0, bb)) φ) = (mk_v (adjoint I σ (sol 0,bb)) ODE (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (sol 0, bb)) φ) "
using main_eq by auto
have fml_eq: "⋀s. s ∈ {0..t} ⟹
(mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem I (Fsubst φ σ))
= (mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol s) ∈ fml_sem (adjoint I σ (sol 0, bb)) φ)"
using fml_eq1 fml_eq2 fml_eq3 by meson
have sem_eq:"⋀t. ODE_sem I (Osubst ODE σ) (sol t) = ODE_sem (adjoint I σ (sol t, bb)) ODE (sol t)"
subgoal for t
using subst_ode[OF good_interp osafe ssafe OA, of "(sol t,bb)"] by auto
done
have sem_fact:"⋀s. s ∈ {0..t} ⟹ ODE_sem I (Osubst ODE σ) (sol s) = ODE_sem (adjoint I σ (sol 0, bb)) ODE (sol s)"
subgoal for s
using subst_ode[OF good_interp osafe ssafe OA, of "(sol s, bb)"]
uadmit_ode_adjoint'[OF ssafe good_interp agrees[of s] osafe]
by auto
done
have sub:"⋀s. s ∈ {0..t}
⟹ sol s ∈ {x. mk_v I (Osubst ODE σ) (sol 0, bb) (sol s) ∈ fml_sem I (Fsubst φ σ)}"
using fml_eq rangeI t sol solves_ode_domainD by fastforce
have sol':"(sol solves_ode (λa. ODE_sem I (Osubst ODE σ))) {0..t} {x. mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) x ∈ fml_sem (adjoint I σ (sol 0, bb)) φ}"
apply (rule solves_ode_congI)
apply (rule sol)
subgoal for ta by auto
subgoal for ta using sem_fact[of ta] by auto
subgoal by (rule refl)
subgoal by (rule refl)
done
have sol'':"(sol solves_ode (λa. ODE_sem I (Osubst ODE σ))) {0..t} {x. mk_v I (Osubst ODE σ) (sol 0, bb) x ∈ fml_sem I (Fsubst φ σ)}"
apply (rule solves_odeI)
subgoal using sol' solves_ode_vderivD by blast
subgoal for ta using sub[of ta] apply auto
by (meson empty_iff)
done
show "∃sola. sol 0 = sola 0 ∧
(∃ta. mk_v (adjoint I σ (sol 0, bb)) ODE (sol 0, bb) (sol t) = mk_v I (Osubst ODE σ) (sola 0, bb) (sola ta) ∧
0 ≤ ta ∧
(sola solves_ode (λa. ODE_sem I (Osubst ODE σ))) {0..ta} {x. mk_v I (Osubst ODE σ) (sola 0, bb) x ∈ fml_sem I (Fsubst φ σ)})"
apply(rule exI[where x=sol])
apply(rule conjI)
subgoal by (rule refl)
apply(rule exI[where x=t])
apply(rule conjI)
subgoal using mkvt t by auto
apply(rule conjI)
subgoal by (rule t)
subgoal using sol'' by auto
done
qed
then show "?case" by auto
next
case (Padmit_Choice σ a b) then
have IH1:"hpsafe a ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst a σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) a))"
and IH2:"hpsafe b ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst b σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) b))"
by blast+
have hpsafe1:"hpsafe (a ∪∪ b) ⟹ hpsafe a"
and hpsafe2:"hpsafe (a ∪∪ b) ⟹ hpsafe b"
by (auto dest: hpsafe.cases)
show ?case using IH1[OF hpsafe1] IH2[OF hpsafe2] by auto
next
case (Padmit_Assign σ θ x) then
have TA:"Tadmit σ θ" by auto
have "hpsafe (Assign x θ) ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst (Assign x θ) σ)) = ((ν, ω) ∈ prog_sem (adjoint I σ ν) (Assign x θ)))"
proof -
assume hpsafe:"hpsafe (Assign x θ)"
assume ssafe:"ssafe σ"
from ssafe have ssafes:"(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f')"
"(⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f')"
unfolding ssafe_def by auto
from hpsafe have dsafe:"dsafe θ" by (auto elim: hpsafe.cases)
fix ν ω
show "?thesis ν ω"
using subst_dterm[OF good_interp TA dsafe ssafes]
by auto
qed
then show ?case by auto
next
case (Padmit_DiffAssign σ θ x) then
have TA:"Tadmit σ θ" by auto
have "hpsafe (DiffAssign x θ) ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst (DiffAssign x θ) σ)) = ((ν, ω) ∈ prog_sem (adjoint I σ ν) (DiffAssign x θ)))"
proof -
assume hpsafe:"hpsafe (DiffAssign x θ)"
assume ssafe:"ssafe σ"
from ssafe have ssafes:"(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f')"
"(⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f')"
unfolding ssafe_def by auto
from hpsafe have dsafe:"dsafe θ" by (auto elim: hpsafe.cases)
fix ν ω
show "?thesis ν ω"
using subst_dterm[OF good_interp TA dsafe ssafes]
by auto
qed
then show ?case by auto
next
case (Padmit_Test σ φ) then
have IH:"fsafe φ ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) φ))"
by auto
have "hpsafe (? φ) ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst (? φ) σ)) = ((ν, ω) ∈ prog_sem (local.adjoint I σ ν) (? φ)))"
proof -
assume hpsafe:"hpsafe (? φ)"
from hpsafe have fsafe:"fsafe φ" by (auto dest: hpsafe.cases)
assume ssafe:"ssafe σ"
fix ν ω
show "?thesis ν ω" using IH[OF fsafe ssafe] by auto
qed
then show ?case by auto
next
case (Fadmit_Geq σ θ1 θ2) then
have TA1:"Tadmit σ θ1" and TA2:"Tadmit σ θ2"
by auto
have "fsafe (Geq θ1 θ2) ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst (Geq θ1 θ2) σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) (Geq θ1 θ2)))"
proof -
assume fsafe:"fsafe (Geq θ1 θ2)"
assume ssafe:"ssafe σ"
from fsafe have dsafe1:"dsafe θ1" and dsafe2:"dsafe θ2"
by (auto dest: fsafe.cases)
from ssafe have ssafes:"(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f')"
"(⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f')"
unfolding ssafe_def by auto
fix ν
show "?thesis ν" using
subst_dterm[OF good_interp TA1 dsafe1 ssafes]
subst_dterm[OF good_interp TA2 dsafe2 ssafes]
by auto
qed
then show ?case by auto
next
case (Fadmit_Prop1 σ args p p') then
have TA:"⋀i. Tadmit σ (args i)"
and some:"SPredicates σ p = Some p'"
and NFA:"NFadmit (λi. Tsubst (args i) σ) p'"
and substSafes:"⋀i. dsafe (Tsubst (args i) σ)"
by auto
have "fsafe ($φ p args) ⟹
ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst ($φ p args) σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) ($φ p args)))"
proof -
assume fsafe:"fsafe ($φ p args)"
assume ssafe:"ssafe σ"
from ssafe have ssafes:"(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f')"
"(⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f')"
unfolding ssafe_def by auto
fix ν
from fsafe have safes:"⋀i. dsafe (args i)" using dfree_is_dsafe by auto
have IH:"(⋀ν'. ⋀i. dsafe (args i) ⟹
dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν)"
using subst_dterm[OF good_interp TA safes ssafes] by auto
have eqs:"⋀i ν'. dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν"
by (auto simp add: IH safes)
let ?sub = "(λ i. Tsubst (args i) σ)"
have freef:"fsafe p'" using ssafe some unfolding ssafe_def by auto
have IH2:"(ν ∈ fml_sem I (FsubstFO p' ?sub)) = (ν ∈ fml_sem (adjointFO I ?sub ν) p')"
using nsubst_fml good_interp NFA freef substSafes
by blast
have vec:"(χ i. dterm_sem I (Tsubst (args i) σ) ν) = (χ i. dterm_sem (local.adjoint I σ ν) (args i) ν)"
apply(auto simp add: vec_eq_iff)
subgoal for i
using IH[of i, OF safes[of i]]
by auto
done
show "?thesis ν"
using IH safes eqs apply (auto simp add: IH2 some good_interp)
using some unfolding adjoint_def adjointFO_def by auto
qed
then show "?case" by auto
next
case (Fadmit_Prop2 σ args p)
note TA = Fadmit_Prop2.hyps(1)
and none = Fadmit_Prop2.hyps(2)
have "fsafe (Prop p args) ⟹ ssafe σ ⟹ (⋀ν.(ν ∈ fml_sem I (Fsubst ($φ p args) σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) ($φ p args)))"
proof -
assume safe:"fsafe (Prop p args)" and ssafe:"ssafe σ"
from ssafe have ssafes:"(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f')"
"(⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f')"
unfolding ssafe_def by auto
fix ν
from safe have safes:"⋀i. dsafe (args i)" using dfree_is_dsafe by auto
have IH:"(⋀ν'. ⋀i. dsafe (args i) ⟹
dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν)"
using subst_dterm[OF good_interp TA safes ssafes] by auto
have Ieq:"Predicates I p = Predicates (adjoint I σ ν) p"
using none unfolding adjoint_def by auto
have vec:"(χ i. dterm_sem I (Tsubst (args i) σ) ν) = (χ i. dterm_sem (adjoint I σ ν) (args i) ν)"
apply(auto simp add: vec_eq_iff)
subgoal for i using IH[of i, OF safes[of i]] by auto
done
show "?thesis ν" using none IH Ieq vec by auto
qed
then show "?case" by auto
next
case (Fadmit_Not σ φ) then
have IH:"fsafe φ ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) φ))"
by blast
have fsafe:"fsafe (Not φ) ⟹ fsafe φ"
by (auto dest: fsafe.cases)
show ?case using IH[OF fsafe] by auto
next
case (Fadmit_And σ φ ψ) then
have IH1:"fsafe φ ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) φ))"
and IH2:"fsafe ψ ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst ψ σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) ψ))"
by (blast)+
have fsafe1:"fsafe (φ && ψ) ⟹ fsafe φ" and fsafe2:"fsafe (φ && ψ) ⟹ fsafe ψ"
by (auto dest: fsafe.cases)
show ?case using IH1[OF fsafe1] IH2[OF fsafe2] by auto
next
case (Fadmit_Exists σ φ x)
then have IH:"fsafe φ ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) φ))"
and FUA:"FUadmit σ φ {Inl x}"
by blast+
have fsafe:"fsafe (Exists x φ) ⟹ fsafe φ"
by (auto dest: fsafe.cases)
have eq:"fsafe (Exists x φ) ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst (Exists x φ) σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) (Exists x φ)))"
proof -
assume fsafe:"fsafe (Exists x φ)"
from fsafe have fsafe':"fsafe φ" by (auto dest: fsafe.cases)
assume ssafe:"ssafe σ"
fix ν
have agree:"⋀r. Vagree ν (repv ν x r) (- {Inl x})"
unfolding Vagree_def by auto
have sem_eq:"⋀r. ((repv ν x r) ∈ fml_sem (local.adjoint I σ (repv ν x r)) φ) =
((repv ν x r) ∈ fml_sem (local.adjoint I σ ν) φ)"
using uadmit_fml_adjoint[OF FUA agree fsafe' ssafe good_interp] by auto
have "(ν ∈ fml_sem I (Fsubst (Exists x φ) σ)) = (∃r. (repv ν x r) ∈ fml_sem I (Fsubst φ σ))"
by auto
moreover have "... = (∃r. (repv ν x r) ∈ fml_sem (local.adjoint I σ (repv ν x r)) φ)"
using IH[OF fsafe' ssafe] by auto
moreover have "... = (∃r. (repv ν x r) ∈ fml_sem (local.adjoint I σ ν) φ)"
using sem_eq by auto
moreover have "... = (ν ∈ fml_sem (adjoint I σ ν) (Exists x φ))"
by auto
ultimately show "(ν ∈ fml_sem I (Fsubst (Exists x φ) σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) (Exists x φ))"
by auto
qed
then show ?case by auto
next
case (Fadmit_Diamond σ φ a) then
have PA:"Padmit σ a"
and FUA:"FUadmit σ φ (BVP (Psubst a σ))"
and IH1:"fsafe φ ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (adjoint I σ ν) φ))"
and IH2:"hpsafe a ⟹ ssafe σ ⟹ (⋀ν ω. ((ν, ω) ∈ prog_sem I (Psubst a σ)) = ((ν, ω) ∈ prog_sem (adjoint I σ ν) a))"
and substSafe:"hpsafe (Psubst a σ)"
by auto
have "fsafe (⟨ a ⟩ φ) ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst (⟨ a ⟩ φ) σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) (⟨ a ⟩ φ)))"
proof -
assume fsafe:"fsafe (⟨ a ⟩ φ)"
assume ssafe:"ssafe σ"
from fsafe have fsafe':"fsafe φ" and hpsafe:"hpsafe a" by (auto dest: fsafe.cases)
fix ν
have agree:"⋀ω. (ν, ω) ∈ prog_sem I (Psubst a σ) ⟹ Vagree ν ω (-BVP(Psubst a σ))"
using bound_effect[OF good_interp, of "(Psubst a σ)" ν, OF substSafe] by auto
have sem_eq:"⋀ω. (ν, ω) ∈ prog_sem I (Psubst a σ) ⟹
(ω ∈ fml_sem (local.adjoint I σ ν) φ) =
(ω ∈ fml_sem (local.adjoint I σ ω) φ)"
using uadmit_fml_adjoint[OF FUA agree fsafe' ssafe good_interp] by auto
have "(ν ∈ fml_sem I (Fsubst (⟨ a ⟩ φ) σ)) = (∃ ω. (ν, ω) ∈ prog_sem I (Psubst a σ) ∧ ω ∈ fml_sem I (Fsubst φ σ))"
by auto
moreover have "... = (∃ ω. (ν, ω) ∈ prog_sem (adjoint I σ ν) a ∧ ω ∈ fml_sem (adjoint I σ ω) φ)"
using IH1[OF fsafe' ssafe] IH2[OF hpsafe ssafe, of ν] by auto
moreover have "... = (∃ ω. (ν, ω) ∈ prog_sem (adjoint I σ ν) a ∧ ω ∈ fml_sem (adjoint I σ ν) φ)"
using sem_eq IH2 hpsafe ssafe by blast
moreover have "... = (ν ∈ fml_sem (adjoint I σ ν) (⟨ a ⟩ φ))"
by auto
ultimately show "?thesis ν" by auto
qed
then show ?case by auto
next
case (Fadmit_Prop1 σ args p p')
have "fsafe(Prop p args) ⟹ ssafe σ ⟹ (⋀ν.(ν ∈ fml_sem I (Fsubst ($φ p args) σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) ($φ p args)))"
proof -
assume fsafe:"fsafe (Prop p args)"
and ssafe:"ssafe σ"
from ssafe have ssafes:"(⋀i f'. SFunctions σ i = Some f' ⟹ dfree f')"
"(⋀f f'. SPredicates σ f = Some f' ⟹ fsafe f')"
unfolding ssafe_def by auto
fix ν
note TA = Fadmit_Prop1.hyps(1)
and some = Fadmit_Prop1.hyps(2) and NFA = Fadmit_Prop1.hyps(3)
from fsafe have safes:"⋀i. dsafe (args i)" using dfree_is_dsafe by auto
have IH:"(⋀ν'. ⋀i. dsafe (args i) ⟹
dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν)"
using subst_dterm[OF good_interp TA safes ssafes] by auto
have eqs:"⋀i ν'. dterm_sem I (Tsubst (args i) σ) ν = dterm_sem (adjoint I σ ν) (args i) ν"
by (auto simp add: IH safes)
let ?sub = "(λ i. Tsubst (args i) σ)"
have subSafe:"(∀ i. dsafe (?sub i))"
by (simp add: safes ssafes tsubst_preserves_safe)
have freef:"fsafe p'" using ssafe some unfolding ssafe_def by auto
have IH2:"(ν ∈ fml_sem I (FsubstFO p' ?sub)) = (ν ∈ fml_sem (adjointFO I ?sub ν) p')"
by (simp add: nsubst_fml [OF good_interp NFA freef subSafe])
have vec:"(χ i. dterm_sem I (Tsubst (args i) σ) ν) = (χ i. dterm_sem (local.adjoint I σ ν) (args i) ν)"
apply(auto simp add: vec_eq_iff)
subgoal for i
using IH[of i, OF safes[of i]]
by auto
done
show "?thesis ν"
using IH safes eqs apply (auto simp add: IH2 some good_interp)
using some unfolding adjoint_def adjointFO_def by auto
qed
next
case (Fadmit_Context1 σ φ C C') then
have FA:"Fadmit σ φ"
and FUA:"FUadmit σ φ UNIV"
and some:"SContexts σ C = Some C'"
and PFA:"PFadmit (λ_. Fsubst φ σ) C'"
and IH:"fsafe φ ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) φ))"
and substSafe:"fsafe(Fsubst φ σ)"
by auto
have "fsafe (InContext C φ) ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst (InContext C φ) σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) (InContext C φ)))"
proof -
assume safe:"fsafe (InContext C φ)"
from safe have fsafe:"fsafe φ" by (auto dest: fsafe.cases)
assume ssafe:"ssafe σ"
fix ν :: "'sz state"
have agree:"⋀ω. Vagree ν ω (-UNIV)" unfolding Vagree_def by auto
have adj_eq:"⋀ω. fml_sem (adjoint I σ ν) φ = fml_sem (adjoint I σ ω) φ"
using uadmit_fml_adjoint[OF FUA agree fsafe ssafe good_interp] by auto
have eq:"(ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) φ)"
using adj_eq IH[OF fsafe ssafe] by auto
let ?sub = "(λ_. Fsubst φ σ)"
let ?R1 = "fml_sem I (Fsubst φ σ)"
let ?R2 = "fml_sem (adjoint I σ ν) φ"
have eq':"?R1 = ?R2"
using adj_eq IH[OF fsafe ssafe] by auto
have freef:"fsafe C'" using ssafe some unfolding ssafe_def by auto
have IH2:"(ν ∈ fml_sem I (PFsubst C' ?sub)) = (ν ∈ fml_sem (PFadjoint I ?sub) C')"
using psubst_fml good_interp PFA fsafe substSafe freef by blast
have IH':"(⋀ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (adjoint I σ ν) φ))"
using IH[OF fsafe ssafe] by auto
then have IH:"fml_sem I (Fsubst φ σ) = fml_sem (adjoint I σ ν) φ"
using eq' by blast
have duh:" (λf' _. fml_sem I (case () of () ⇒ Fsubst φ σ)) = (λ x (). fml_sem (local.adjoint I σ ν) φ)"
by (simp add: case_unit_Unity eq' ext)
have extend_PF:"(PFadjoint I ?sub) = (extendc I ?R2)"
unfolding PFadjoint_def using IH apply (simp)
by (metis old.unit.case old.unit.exhaust)
have "(ν ∈ fml_sem I (Fsubst (InContext C φ) σ)) = (ν ∈ fml_sem I (PFsubst C' (λ_. Fsubst φ σ)))"
using some by simp
moreover have "... = (ν ∈ fml_sem (PFadjoint I ?sub) C')"
using IH2 by auto
moreover have "... = (ν ∈ fml_sem (extendc I ?R2) C')"
using extend_PF by simp
moreover have "... = (ν ∈ fml_sem (extendc I ?R1) C')"
using eq' by auto
moreover have "... = (ν ∈ Contexts (adjoint I σ ν) C (fml_sem (adjoint I σ ν) φ))"
using some unfolding adjoint_def apply auto
apply (simp add: eq' local.adjoint_def)
by (simp add: eq' local.adjoint_def)
moreover have "... = (ν ∈ fml_sem (adjoint I σ ν) (InContext C φ))"
by auto
ultimately
show "(ν ∈ fml_sem I (Fsubst (InContext C φ) σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) (InContext C φ))"
by blast
qed
then show ?case by auto
next
case (Fadmit_Context2 σ φ C) then
have FA:"Fadmit σ φ"
and FUA:"FUadmit σ φ UNIV"
and none:"SContexts σ C = None"
and IH:"fsafe φ ⟹ ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) φ))"
by auto
have "fsafe (InContext C φ) ⟹
ssafe σ ⟹ (⋀ν. (ν ∈ fml_sem I (Fsubst (InContext C φ) σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) (InContext C φ)))"
proof -
assume safe:"fsafe (InContext C φ)"
then have fsafe:"fsafe φ" by (auto dest: fsafe.cases)
assume ssafe:"ssafe σ"
fix ν
have Ieq:" Contexts (local.adjoint I σ ν) C = Contexts I C"
using none unfolding adjoint_def by auto
have IH':"⋀ν. (ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (local.adjoint I σ ν) φ)"
using IH[OF fsafe ssafe] by auto
have agree:"⋀ω. Vagree ν ω (-UNIV)" unfolding Vagree_def by auto
have adj_eq:"⋀ω. fml_sem (adjoint I σ ν) φ = fml_sem (adjoint I σ ω) φ"
using uadmit_fml_adjoint[OF FUA agree fsafe ssafe good_interp] by auto
then have sem:"fml_sem I (Fsubst φ σ) = fml_sem (local.adjoint I σ ν) φ"
using IH' agree adj_eq by auto
show "?thesis ν" using none Ieq sem by auto
qed
then show ?case by auto
qed
lemma subst_fml:
fixes I::"('sf, 'sc, 'sz) interp" and ν::"'sz state"
assumes good_interp:"is_interp I"
assumes Fadmit:"Fadmit σ φ"
assumes fsafe:"fsafe φ"
assumes ssafe:"ssafe σ"
shows "(ν ∈ fml_sem I (Fsubst φ σ)) = (ν ∈ fml_sem (adjoint I σ ν) φ)"
using subst_fml_hp[OF good_interp] Fadmit fsafe ssafe by blast
lemma subst_fml_valid:
fixes I::"('sf, 'sc, 'sz) interp" and ν::"'sz state"
assumes Fadmit:"Fadmit σ φ"
assumes fsafe:"fsafe φ"
assumes ssafe:"ssafe σ"
assumes valid:"valid φ"
shows "valid (Fsubst φ σ)"
proof -
have sub_sem:"⋀I ν. is_interp I ⟹ ν ∈ fml_sem I (Fsubst φ σ)"
proof -
fix I::"('sf,'sc,'sz) interp" and ν::"'sz state"
assume good_interp:"is_interp I"
have good_adj:"is_interp (adjoint I σ ν)"
apply(rule adjoint_safe[OF good_interp])
using ssafe unfolding ssafe_def by auto
have φsem:"ν ∈ fml_sem (adjoint I σ ν) φ" using valid using good_adj unfolding valid_def by blast
then show "?thesis I ν"
using subst_fml[OF good_interp Fadmit fsafe ssafe]
by auto
qed
then show ?thesis unfolding valid_def by blast
qed
lemma subst_sequent:
fixes I::"('sf, 'sc, 'sz) interp" and ν::"'sz state"
assumes good_interp:"is_interp I"
assumes Sadmit:"Sadmit σ (Γ,Δ)"
assumes Ssafe:"Ssafe (Γ,Δ)"
assumes ssafe:"ssafe σ"
shows "(ν ∈ seq_sem I (Ssubst (Γ,Δ) σ)) = (ν ∈ seq_sem (adjoint I σ ν) (Γ,Δ))"
proof -
let ?f = "(seq2fml (Γ, Δ))"
have subst_eqG:"Fsubst (foldr (&&) Γ TT) σ = foldr (&&) (map (λφ. Fsubst φ σ) Γ) TT"
by(induction Γ, auto simp add: TT_def)
have subst_eqD:"Fsubst (foldr (||) Δ FF) σ = foldr (||) (map (λφ. Fsubst φ σ) Δ) FF"
by(induction Δ, auto simp add: FF_def Or_def)
have subst_eq:"Fsubst ?f σ = (seq2fml (Ssubst (Γ, Δ) σ))"
using subst_eqG subst_eqD
by (auto simp add: Implies_def Or_def)
have fsafeG:"fsafe (foldr (&&) Γ TT)"
using Ssafe apply(induction Γ, auto simp add: Ssafe_def TT_def)
by fastforce
have fsafeD:"fsafe (foldr (||) Δ FF)"
using Ssafe Or_def apply(induction Δ, auto simp add: Ssafe_def FF_def Or_def)
by fastforce
have fsafe:"fsafe ?f"
using fsafeD fsafeG by (auto simp add: Implies_def Or_def)
have FadmitG:"Fadmit σ (foldr (&&) Γ TT)"
using Sadmit Or_def apply(induction Γ, auto simp add: Sadmit_def TT_def Or_def)
by fastforce
have FadmitD:"Fadmit σ (foldr (||) Δ FF)"
using Sadmit Or_def apply(induction Δ, auto simp add: Sadmit_def FF_def Or_def)
by fastforce
have Fadmit:"Fadmit σ ?f"
using FadmitG FadmitD unfolding Implies_def
by (simp add: Implies_def Or_def)
have "(ν ∈ fml_sem I (Fsubst ?f σ))
=(ν ∈ fml_sem (adjoint I σ ν) (seq2fml (Γ, Δ)))"
using subst_fml[OF good_interp Fadmit fsafe ssafe]
by auto
then show ?thesis
using subst_eq by auto
qed
subsection ‹Soundness of substitution rule›
theorem subst_rule:
assumes sound:"sound R"
assumes Radmit:"Radmit σ R"
assumes FVS:"FVS σ = {}"
assumes Rsafe:"Rsafe R"
assumes ssafe:"ssafe σ"
shows "sound (Rsubst R σ)"
proof -
obtain SG and C where Rdef:"R = (SG,C)" by (cases R, auto)
obtain SG' and C' where Rdef':"Rsubst R σ = (SG',C')" by (cases R, auto)
obtain ΓC and ΔC where Cdef:"C = (ΓC, ΔC)" by (cases C, auto)
obtain ΓC' and ΔC' where C'def:"C' = (ΓC', ΔC')" by (cases C', auto)
have CC':"(Ssubst (ΓC, ΔC) σ) = (ΓC', ΔC')"
using Rdef Rdef' Cdef C'def by auto
have "⋀I ν. is_interp I ⟹ (⋀Γ Δ ω . List.member SG' (Γ, Δ) ⟹ ω ∈ seq_sem I (Γ, Δ)) ⟹ ν ∈ seq_sem I C'"
proof -
fix I::"('sf,'sc,'sz) interp" and ν::"'sz state"
assume good_interp:"is_interp I"
assume prems:"(⋀Γ Δ ω. List.member SG' (Γ, Δ) ⟹ ω ∈ seq_sem I (Γ, Δ))"
have good_interp':"⋀ω. is_interp (adjoint I σ ω)"
using adjoint_safe[OF good_interp ] ssafe[unfolded ssafe_def] by auto
have sound:"⋀ω. (⋀φ ν . List.member SG φ ⟹ ν ∈ seq_sem (adjoint I σ ω) φ) ⟹ ω ∈ seq_sem (adjoint I σ ω) (ΓC, ΔC)"
using soundD_memv[of SG C] sound good_interp' Rdef Cdef by auto
have SadmitC:"Sadmit σ (ΓC, ΔC)"
using Radmit unfolding Radmit_def Rdef Cdef by auto
have SsafeC:"Ssafe (ΓC, ΔC)"
using Rsafe unfolding Rsafe_def Rdef Cdef by auto
have seq_sem:"ν ∈ seq_sem (adjoint I σ ν) (ΓC, ΔC)"
proof(rule sound)
fix S :: "('sf,'sc,'sz) sequent" and ν'
assume mem:"List.member SG S"
obtain ΓS ΔS where Sdef:"S = (ΓS, ΔS)" by (cases S, auto)
from mem obtain di where di:"di < length SG ∧ SG ! di = S"
by (meson in_set_conv_nth in_set_member)
have SadmitS:"Sadmit σ (ΓS, ΔS)"
using Rdef Sdef di Radmit Radmit_def by auto
have SsafeS:"Ssafe (ΓS, ΔS)"
using Rsafe unfolding Rsafe_def Rdef Cdef using Sdef mem di by auto
have map_mem:"⋀f L x. List.member L x ⟹ List.member (map f L) (f x)"
subgoal for f L x
by (induction L, auto simp add: member_rec)
done
let ?S' = "(Ssubst (ΓS, ΔS) σ)"
have eq:"Ssubst S σ = (map (λφ. Fsubst φ σ) ΓS, map (λφ. Fsubst φ σ) ΔS)"
using Sdef by auto
from Sdef have mem':"List.member SG' (fst ?S', snd ?S')"
using mem Rdef Rdef' eq map_mem[of SG S "(λx. Ssubst x σ)"] by auto
have "ν' ∈ seq_sem I (fst ?S', snd ?S')" by (rule prems[OF mem', of ν'])
then have "ν' ∈ seq_sem (adjoint I σ ν') S"
using subst_sequent[OF good_interp SadmitS SsafeS ssafe, of ν']
Sdef by auto
have VA:"Vagree ν ν' (FVS σ)" using FVS unfolding Vagree_def by auto
show "ν' ∈ seq_sem (local.adjoint I σ ν) S"
using adjoint_consequence VA ssafe[unfolded ssafe_def]
by (metis ‹ν' ∈ seq_sem (local.adjoint I σ ν') S› dfree_is_dsafe)
qed
have "ν ∈ seq_sem I (ΓC', ΔC')"
using subst_sequent[OF good_interp SadmitC SsafeC ssafe, of ν] seq_sem Cdef C'def CC'
by auto
then show "ν ∈ seq_sem I C'" using C'def by auto
qed
then show ?thesis
apply(rule soundI_memv')
using Rdef' by auto
qed
end end