# Theory Ids

theory "Ids"
imports Complex_Main
begin
section ‹Identifier locale›
text ‹The differential dynamic logic formalization is parameterized by the type of identifiers.
The identifier type(s) must be finite and have at least 3-4 distinct elements.
Distinctness is required for soundness of some axioms. ›
locale ids =
fixes vid1 :: "('sz::{finite,linorder})"
fixes vid2 :: 'sz
fixes vid3 :: 'sz
fixes fid1 :: "('sf::finite)"
fixes fid2 :: 'sf
fixes fid3 :: 'sf
fixes pid1 :: "('sc::finite)"
fixes pid2 :: 'sc
fixes pid3 :: 'sc
fixes pid4 :: 'sc
assumes vne12:"vid1 ≠ vid2"
assumes vne23:"vid2 ≠ vid3"
assumes vne13:"vid1 ≠ vid3"
assumes fne12:"fid1 ≠ fid2"
assumes fne23:"fid2 ≠ fid3"
assumes fne13:"fid1 ≠ fid3"
assumes pne12:"pid1 ≠ pid2"
assumes pne23:"pid2 ≠ pid3"
assumes pne13:"pid1 ≠ pid3"
assumes pne14:"pid1 ≠ pid4"
assumes pne24:"pid2 ≠ pid4"
assumes pne34:"pid3 ≠ pid4"
context ids begin
lemma id_simps:
"(vid1 = vid2) = False" "(vid2 = vid3) = False" "(vid1 = vid3) = False"
"(fid1 = fid2) = False" "(fid2 = fid3) = False" "(fid1 = fid3) = False"
"(pid1 = pid2) = False" "(pid2 = pid3) = False" "(pid1 = pid3) = False"
"(pid1 = pid4) = False" "(pid2 = pid4) = False" "(pid3 = pid4) = False"
"(vid2 = vid1) = False" "(vid3 = vid2) = False" "(vid3 = vid1) = False"
"(fid2 = fid1) = False" "(fid3 = fid2) = False" "(fid3 = fid1) = False"
"(pid2 = pid1) = False" "(pid3 = pid2) = False" "(pid3 = pid1) = False"
"(pid4 = pid1) = False" "(pid4 = pid2) = False" "(pid4 = pid3) = False"
using vne12 vne23 vne13 fne12 fne23 fne13 pne12 pne23 pne13 pne14 pne24 pne34 by auto
end
end


# Theory Lib

theory Lib
imports
Ordinary_Differential_Equations.ODE_Analysis
begin
section ‹Generic Mathematical Lemmas›
text‹General lemmas that don't have anything to do with dL specifically and could be fit for
general-purpose libraries, mostly dealing with derivatives, ODEs and vectors.›

lemma vec_extensionality:"(⋀i. v$i = w$i) ⟹ (v = w)"

lemma norm_axis: "norm (axis i x) = norm x"
unfolding axis_def norm_vec_def
unfolding L2_set_def
by(clarsimp simp add: if_distrib[where f=norm] if_distrib[where f="λx. x⇧2"] sum.If_cases)

lemma bounded_linear_axis: "bounded_linear (axis i)"
proof
show "axis i (x + y) = axis i x + axis i y" "axis i (r *⇩R x) = r *⇩R axis i x" for x y :: "'a" and r
by (auto simp: vec_eq_iff axis_def)
show "∃K. ∀x::'a. norm (axis i x) ≤ norm x * K"
by (auto simp add: norm_axis intro!: exI[of _ 1])
qed

lemma bounded_linear_vec:
fixes f::"('a::finite) ⇒ 'b::real_normed_vector ⇒ 'c::real_normed_vector"
assumes bounds:"⋀i. bounded_linear (f i)"
shows "bounded_linear (λx. χ i. f i x)"
proof unfold_locales
fix r x y
interpret bounded_linear "f i" for i by fact
show "(χ i. f i (x + y)) = (χ i. f i x) + (χ i. f i y)"
show "(χ i. f i (r *⇩R x)) = r *⇩R (χ i. f i x)"
by (vector scaleR)
obtain K where "norm (f i x) ≤ norm x * K i" for x i
using bounded by metis
then have "norm (χ i. f i x) ≤ norm x * (∑i∈UNIV. K i)" (is "?lhs ≤ ?rhs") for x
unfolding sum_distrib_left
unfolding norm_vec_def
by (auto intro!: L2_set_le_sum_abs[THEN order_trans] sum_mono simp: abs_mult)
then show "∃K. ∀x. norm (χ i. f i x) ≤ norm x * K"
by blast
qed

lift_definition blinfun_vec::"('a::finite ⇒ 'b::real_normed_vector ⇒⇩L real) ⇒ 'b ⇒⇩L (real ^ 'a)" is "(λ(f::('a ⇒ 'b ⇒ real)) (x::'b). χ (i::'a). f i x)"
by(rule bounded_linear_vec, simp)

lemmas blinfun_vec_simps[simp] = blinfun_vec.rep_eq

lemma continuous_blinfun_vec:"(⋀i. continuous_on UNIV (blinfun_apply (g i))) ⟹ continuous_on UNIV (blinfun_vec g)"

lemma blinfun_elim:"⋀g. (blinfun_apply (blinfun_vec g)) = (λx. χ i. g i x)"
using blinfun_vec.rep_eq by auto

lemma sup_plus:
fixes f g::"('b::metric_space) ⇒ real"
assumes nonempty:"R ≠ {}"
assumes bddf:"bdd_above (f  R)"
assumes bddg:"bdd_above (g  R)"
shows "(SUP x∈R. f x  + g x) ≤ (SUP x∈R. f x) + (SUP x∈R. g x)"
proof -
have bddfg:"bdd_above((λx. f x + g x )  R)"
using bddf bddg apply (auto simp add: bdd_above_def)
have eq:"(SUP x∈R. f x + g x) ≤ (SUP x∈R. f x) + (SUP x∈R. g x)
⟷ (∀x∈R. (f x + g x) ≤ (SUP x∈R. f x) + (SUP x∈R. g x))"
apply(rule cSUP_le_iff)
subgoal by (rule nonempty)
subgoal by (rule bddfg)
done
have fs:"⋀x. x ∈ R ⟹ f x ≤ (SUP x∈R. f x)"
using bddf
have gs:"⋀x. x ∈ R ⟹ g x ≤ (SUP x∈R. g x)"
using bddg
have "(∀x∈R. (f x + g x) ≤ (SUP x∈R. f x) + (SUP x∈R. g x))"
apply auto
subgoal for x using fs[of x] gs[of x] by auto
done
then show ?thesis by (auto simp add: eq)
qed

lemma continuous_blinfun_vec':
fixes f::"'a::{finite,linorder} ⇒ 'b::{metric_space, real_normed_vector,abs} ⇒ 'b ⇒⇩L real"
fixes S::"'b set"
assumes conts:"⋀i. continuous_on UNIV (f i)"
shows "continuous_on UNIV (λx. blinfun_vec (λ i. f i x))"
proof (auto simp add:  LIM_def continuous_on_def)
fix x1 and ε::real
assume ε:"0 < ε"
let ?n = "card (UNIV::'a set)"
have conts':" ⋀i x1 ε. 0 < ε ⟹ ∃δ>0. ∀x2. x2 ≠ x1 ∧ dist x2 x1 < δ ⟶ dist (f i  x2) (f i x1) < ε"
using conts by(auto simp add: LIM_def continuous_on_def)
have conts'':"⋀i. ∃δ>0. ∀x2. x2 ≠ x1 ∧ dist x2 x1 < δ ⟶ dist (f i  x2) (f i x1) < (ε/?n)"
subgoal for i using conts'[of "ε / ?n"  x1 i] ε by auto done
let ?f = "(λx. blinfun_vec (λ i. f i x))"
let ?Pδ = "(λ i δ. (δ>0 ∧ (∀x2. x2 ≠ x1 ∧ dist x2 x1 < δ ⟶ dist (f i  x2) (f i x1) < (ε/?n))))"
let ?δi = "(λi. SOME δ. ?Pδ i δ)"
have Ps:"⋀i. ∃δ. ?Pδ i δ" using conts'' by auto
have Pδi:"⋀i. ?Pδ i (?δi i)"
subgoal for i using someI[of "?Pδ i" ] Ps[of i] by auto done
have finU:"finite (UNIV::'a set)" by auto
let ?δ = "linorder_class.Min  (?δi  UNIV)"
have δ0s:"⋀i. ?δi i > 0" using Pδi by blast
then have δ0s':"⋀i. 0 < ?δi i" by auto
have bounds:"bdd_below (?δi  UNIV)"
unfolding bdd_below_def
using δ0s less_eq_real_def by blast
have δs:"⋀i. ?δ ≤ ?δi i"
using bounds cINF_lower[of ?δi] by auto
have finite:"finite ((?δi  UNIV))" by auto
have nonempty:"((?δi  UNIV)) ≠ {}" by auto
have δ:"?δ > 0 " using Min_gr_iff[OF finite nonempty] δ0s'
by blast
have conts''':"⋀i x2. x2 ≠ x1 ⟹ dist x2 x1 < ?δi i ⟹ dist (f i  x2) (f i x1) < (ε/?n)"
subgoal for i x2
using conts''[of i] apply auto
subgoal for δ
apply(erule allE[where x=x2])
using Pδi  δs[of i] apply (auto simp add: δs[of i])
done
done
done
have "⋀x2. x2 ≠ x1 ∧ dist x2 x1 < ?δ ⟹ dist (blinfun_vec (λi. f i x2)) (blinfun_vec (λi. f i x1)) < ε"
proof (auto)
fix x2
assume ne:"x2 ≠ x1"
assume dist:"∀i. dist x2 x1 < ?δi i"
have dists:"⋀i. dist x2 x1 < ?δi i"
subgoal for i using dist δs[of i] by auto done
have euclid:"⋀y. norm(?f x1 y - ?f x2 y) = (L2_set (λi. norm(f i x1 y - f i x2 y)) UNIV)"
have finite:"finite (UNIV::'a set)" by auto
have nonempty: "(UNIV::'a set) ≠ {}" by auto
have nonemptyB: "(UNIV::'b set) ≠ {}" by auto
have nonemptyR: "(UNIV::real set) ≠ {}" by auto
have SUP_leq:"⋀f::('b ⇒ real). ⋀ g::('b ⇒ real). ⋀ S::'b set. S ≠ {} ⟹ bdd_above (g  S) ⟹ (⋀x. x ∈ (S::'b set) ⟹ ((f x)::real) ≤ ((g x)::real)) ⟹ (SUP x∈S. f x) ≤ (SUP x∈S. g x)"
by(rule cSup_mono, auto)
have SUP_sum_comm':"⋀R S f . finite (S::'a set) ⟹ (R::'d::metric_space set) ≠ {} ⟹
(⋀i x. ((f i x)::real) ≥ 0) ⟹
(⋀i. bdd_above (f i  R)) ⟹
(SUP x∈R . (∑i ∈ S. f i x)) ≤ (∑i ∈ S. (SUP x∈R. f i x))"
proof -
fix  R::"'d set" and S ::"('a)set"  and f  ::"'a ⇒ 'd ⇒ real"
assume non:"R ≠ {} "
assume fin:"finite S"
assume every:"(⋀i x. 0 ≤ f i x)"
assume bddF:"⋀i. bdd_above (f i  R)"
then have bddF':"⋀i. ∃M. ∀x ∈R. f i x ≤ M "
unfolding bdd_above_def by auto
let ?boundP = "(λi M. ∀x ∈R. f i x ≤ M)"
let ?bound = "(λi::'a. SOME M. ∀x ∈R. f i x ≤ M)"
have "⋀i. ∃M. ?boundP i M" using bddF' by auto
then have each_bound:"⋀i. ?boundP i (?bound i)"
subgoal for i using someI[of "?boundP i"] by blast done
let ?bigBound = "(λF. ∑i∈F. (?bound i))"
have bddG:"⋀i::'a. ⋀F. bdd_above ((λx. ∑i∈F. f i x)  R)"
subgoal for i F
using bddF[of i] unfolding bdd_above_def apply auto
apply(rule exI[where x="?bigBound F"])
subgoal for M
apply auto
subgoal for x
using each_bound by (simp add: sum_mono)
done
done
done
show "?thesis R S f" using fin assms
proof (induct)
case empty
have "((SUP x∈R. ∑i∈{}. f i x)::real) ≤ (∑i∈{}. SUP a∈R. f i a)"   by (simp add: non)
then show ?case by auto
next
case (insert x F)
have "((SUP xa∈R. ∑i∈insert x F. f i xa)::real) ≤ (SUP xa∈R. f x xa +  (∑i∈F. f i xa))"
using insert.hyps(2) by auto
moreover have "...  ≤ (SUP xa∈ R. f x xa) + (SUP xa∈R. (∑i∈F. f i xa))"
by(rule sup_plus, rule non, rule bddF, rule bddG)
moreover have "... ≤ (SUP xa∈ R. f x xa) + (∑i∈F. SUP a∈R. f i a)"
using add_le_cancel_left conts insert.hyps(3) by blast
moreover have "... ≤ (∑i∈(insert x F). SUP a∈R. f i a)"
ultimately have "((SUP xa∈R. ∑i∈insert x F. f i xa)::real) ≤ (∑i∈(insert x F). SUP a∈R. f i a)"
by linarith
then show ?case by auto
qed
qed
have SUP_sum_comm:"⋀R S y1 y2 . finite (S::'a set) ⟹ (R::'b set) ≠ {} ⟹ (SUP x∈R . (∑i ∈ S. norm(f i y1 x - f i y2 x)/norm(x))) ≤ (∑i ∈ S. (SUP x∈R. norm(f i y1 x - f i y2 x)/norm(x)))"
apply(rule SUP_sum_comm')
apply(auto)[3]
proof (unfold bdd_above_def)
fix R S y1 y2 i
{ fix rr :: "real ⇒ real"
obtain bb :: "real ⇒ ('b ⇒ real) ⇒ 'b set ⇒ 'b" where
ff1: "⋀r f B. r ∉ f  B ∨ f (bb r f B) = r"
by moura
{ assume "∃r. ¬ rr r ≤ norm (f i y1 - f i y2)"
then have "∃r. norm (blinfun_apply (f i y1) (bb (rr r) (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) R) - blinfun_apply (f i y2) (bb (rr r) (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) R)) / norm (bb (rr r) (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b) R) ≠ rr r"
by (metis (no_types) le_norm_blinfun minus_blinfun.rep_eq)
then have "∃r. rr r ≤ r ∨ rr r ∉ (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b)  R"
using ff1 by meson }
then have "∃r. rr r ≤ r ∨ rr r ∉ (λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b)  R"
by blast }
then show "∃r. ∀ra∈(λb. norm (blinfun_apply (f i y1) b - blinfun_apply (f i y2) b) / norm b)  R. ra ≤ r"
by meson
qed
have SUM_leq:"⋀S::('a) set. ⋀ f g ::('a ⇒ real). S ≠ {} ⟹ finite S ⟹ (⋀x. x ∈ S ⟹ f x < g x) ⟹ (∑x∈S. f x) < (∑x∈S. g x)"
by(rule sum_strict_mono, auto)
have L2:"⋀f S. L2_set (λx. norm(f x)) S ≤ (∑x ∈ S. norm(f x))"
using L2_set_le_sum norm_ge_zero by metis
have L2':"⋀y. (L2_set (λi. norm(f i x1 y - f i x2 y)) UNIV)/norm(y) ≤ (∑i∈UNIV. norm(f i x1 y - f i x2 y))/norm(y)"
subgoal for y
using L2[of "(λ x. f x x1 y - f x x2 y)" UNIV]
done
have "⋀i. (SUP y∈UNIV.  norm((f i x1 - f i x2) y)/norm(y)) = norm(f i x1 - f i x2)"
then have each_norm:"⋀i. (SUP y∈UNIV.  norm(f i x1 y - f i x2 y)/norm(y)) = norm(f i x1 - f i x2)"
by (metis (no_types, lifting) SUP_cong blinfun.diff_left)
have bounded_linear:"⋀i. bounded_linear (λy. f i x1 y - f i x2 y)"
have each_bound:"⋀i. bdd_above ((λy. norm(f i x1 y - f i x2 y)/norm(y))  UNIV)"
using bounded_linear unfolding bdd_above_def
proof -
fix i :: 'a
{ fix rr :: "real ⇒ real"
have "⋀a r. norm (blinfun_apply (f a x1) r - blinfun_apply (f a x2) r) / norm r ≤ norm (f a x1 - f a x2)"
by (metis le_norm_blinfun minus_blinfun.rep_eq)
then have "⋀r R. r ∉ (λr. norm (blinfun_apply (f i x1) r - blinfun_apply (f i x2) r) / norm r)  R ∨ r ≤ norm (f i x1 - f i x2)"
by blast
then have "∃r. rr r ≤ r ∨ rr r ∉ range (λr. norm (blinfun_apply (f i x1) r - blinfun_apply (f i x2) r) / norm r)"
by blast }
then show "∃r. ∀ra∈range (λr. norm (blinfun_apply (f i x1) r - blinfun_apply (f i x2) r) / norm r). ra ≤ r"
by meson
qed
have bdd_above:"(bdd_above ((λy. (∑i∈UNIV. norm(f i x1 y - f i x2 y)/norm(y)))  UNIV))"
using each_bound unfolding bdd_above_def apply auto
proof -
assume each:"(⋀i. ∃M. ∀x. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x ≤ M)"
let ?boundP = "(λi M. ∀x. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x ≤ M)"
let ?bound = "(λi. SOME x. ?boundP i x)"
have bounds:"⋀i. ?boundP i (?bound i)"
subgoal for i using each someI[of "?boundP i"] by blast done
let ?bigBound = "∑i∈(UNIV::'a set). ?bound i"
show "∃M. ∀x. (∑i∈UNIV. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x) ≤ M"
apply(rule exI[where x= ?bigBound])
qed
have bdd_above:"(bdd_above ((λy. (∑i∈UNIV. norm(f i x1 y - f i x2 y))/norm(y))  UNIV))"
using bdd_above unfolding bdd_above_def apply auto
proof -
fix M :: real
assume a1: "∀x. (∑i∈UNIV. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x) ≤ M"
{ fix bb :: "real ⇒ 'b"
have "⋀b. (∑a∈UNIV. ¦blinfun_apply (f a x1) b - blinfun_apply (f a x2) b¦) / norm b ≤ M"
using a1 by (simp add: sum_divide_distrib)
then have "∃r. (∑a∈UNIV. ¦blinfun_apply (f a x1) (bb r) - blinfun_apply (f a x2) (bb r)¦) / norm (bb r) ≤ r"
by blast }
then show "∃r. ∀b. (∑a∈UNIV. ¦blinfun_apply (f a x1) b - blinfun_apply (f a x2) b¦) / norm b ≤ r"
by meson
qed
have "dist (?f x2) (?f x1) = norm((?f x2) - (?f x1))"
moreover have "... = (SUP y∈UNIV. norm(?f x1 y - ?f x2 y)/norm(y))"
by (metis (no_types, lifting) SUP_cong blinfun.diff_left norm_blinfun.rep_eq norm_minus_commute onorm_def)
moreover have "... = (SUP y∈UNIV. (L2_set (λi. norm(f i x1 y - f i x2 y)) UNIV)/norm(y))"
using  euclid by auto
moreover have "... ≤ (SUP y∈UNIV. (∑i∈UNIV. norm(f i x1 y - f i x2 y))/norm(y))"
using L2' SUP_cong SUP_leq bdd_above by auto
moreover have "... = (SUP y∈UNIV. (∑i∈UNIV. norm(f i x1 y - f i x2 y)/norm(y)))"
moreover have "... ≤ (∑i∈UNIV. (SUP y∈UNIV.  norm(f i x1 y - f i x2 y)/norm(y)))"
by(rule SUP_sum_comm[OF finite  nonemptyB, of x1 x2])
moreover have "... = (∑i∈UNIV. norm(f i x1 - f i x2))"
using each_norm by simp
moreover have "... = (∑i∈UNIV. dist(f i x1) (f i x2))"
moreover have "... < (∑i∈(UNIV::'a set). ε / ?n)"
using conts'''[OF ne dists] using SUM_leq[OF nonempty, of "(λi.  dist (f i x1) (f i x2))" "(λi.  ε / ?n)"]
moreover have "... = ε"
by(auto)
ultimately show "dist (?f x2) (?f x1) < ε"
by linarith
qed
then show "∃s>0. ∀x2. x2 ≠ x1 ∧ dist x2 x1 < s ⟶ dist (blinfun_vec (λi. f i x2)) (blinfun_vec (λi. f i x1)) < ε"
using δ by blast
qed

lemma has_derivative_vec[derivative_intros]:
assumes "⋀i. ((λx. f i x) has_derivative (λh. f' i h)) F"
shows "((λx. χ i. f i x) has_derivative (λh. χ i. f' i h)) F"
proof -
have *: "(χ i. f i x) = (∑i∈UNIV. axis i (f i x))" "(χ i. f' i x) = (∑i∈UNIV. axis i (f' i x))" for x
by (simp_all add: axis_def sum.If_cases vec_eq_iff)
show ?thesis
unfolding *
by (intro has_derivative_sum bounded_linear.has_derivative[OF bounded_linear_axis] assms)
qed

lemma has_derivative_proj:
fixes j::"('a::finite)"
fixes f::"'a ⇒ real ⇒ real"
assumes assm:"((λx. χ i. f i x) has_derivative (λh. χ i. f' i h)) F"
shows "((λx. f j x) has_derivative (λh. f' j h)) F"
proof -
have bounded_proj:"bounded_linear (λ x::(real^'a). x $j)" by (simp add: bounded_linear_vec_nth) show "?thesis" using bounded_linear.has_derivative[OF bounded_proj, of "(λx. χ i. f i x)" "(λh. χ i. f' i h)", OF assm] by auto qed lemma has_derivative_proj': fixes i::"'a::finite" shows "∀x. ((λ x. x$ i) has_derivative (λx::(real^'a). x $i)) (at x)" proof - have bounded_proj:"bounded_linear (λ x::(real^'a). x$ i)"
show "?thesis"
using bounded_proj unfolding has_derivative_def by auto
qed

lemma constant_when_zero:
fixes v::"real ⇒ (real, 'i::finite) vec"
assumes x0: "(v t0) $i = x0" assumes sol: "(v solves_ode f) T S" assumes f0: "⋀s x. s ∈ T ⟹ f s x$ i = 0"
assumes t0:"t0 ∈ T"
assumes t:"t ∈ T"
assumes convex:"convex T"
shows "v t $i = x0" proof - from solves_odeD[OF sol] have deriv: "(v has_vderiv_on (λt. f t (v t))) T" by simp then have "((λt. v t$ i) has_vderiv_on (λt. 0)) T"
using f0
by (auto simp: has_vderiv_on_def has_vector_derivative_def cart_eq_inner_axis
intro!: derivative_eq_intros)
from has_vderiv_on_zero_constant[OF convex this]
obtain c where c:"⋀x. x ∈ T ⟹ v x $i = c" by blast with x0 have "c = x0" "v t$ i = c"
using t t0 c x0 by blast+
then show ?thesis by simp
qed

lemma
solves_ode_subset:
assumes x: "(x solves_ode f) T X"
assumes s: "S ⊆ T"
shows "(x solves_ode f) S X"
apply(rule solves_odeI)
using has_vderiv_on_subset s solves_ode_vderivD x apply force
using assms by (auto intro!: solves_odeI dest!: solves_ode_domainD)

lemma
solves_ode_supset_range:
assumes x: "(x solves_ode f) T X"
assumes y: "X ⊆ Y"
shows "(x solves_ode f) T Y"
apply(rule solves_odeI)
using has_vderiv_on_subset y solves_ode_vderivD x apply force
using assms by (auto intro!: solves_odeI dest!: solves_ode_domainD)

lemma
usolves_ode_subset:
assumes x: "(x usolves_ode f from t0) T X"
assumes s: "S ⊆ T"
assumes t0: "t0 ∈ S"
assumes S: "is_interval S"
shows "(x usolves_ode f from t0) S X"
proof (rule usolves_odeI)
note usolves_odeD[OF x]
show "(x solves_ode f) S X" by (rule solves_ode_subset; fact)
show "t0 ∈ S" "is_interval S" by(fact+)
fix z t
assume s: "{t0 -- t} ⊆ S" and z: "(z solves_ode f) {t0 -- t} X" and z0: "z t0 = x t0"
then have "t0 ∈ {t0 -- t}" "is_interval {t0 -- t}"
by auto
moreover note s
moreover have "(z solves_ode f) {t0--t} X"
using solves_odeD[OF z] ‹S ⊆ T›
by (intro solves_ode_subset_range[OF z]) force
moreover note z0
moreover have "t ∈ {t0 -- t}" by simp
ultimately show "z t = x t"
by (meson ‹⋀z ta T'. ⟦t0 ∈ T'; is_interval T'; T' ⊆ T; (z solves_ode f) T' X; z t0 = x t0; ta ∈ T'⟧ ⟹ z ta = x ta› assms(2) dual_order.trans)
qed

― ‹Example of using lemmas above to show a lemma that could be useful for dL: The constant ODE›
― ‹0 does not change the state.›
lemma example:
fixes x t::real and i::"('sz::finite)"
assumes "t > 0"
shows "x = (ll_on_open.flow UNIV (λt. λx. χ (i::('sz::finite)). 0) UNIV 0 (χ i. x) t) $i" proof - let ?T = UNIV let ?f = "(λt. λx. χ i::('sz::finite). 0)" let ?X = UNIV let ?t0.0 = 0 let ?x0.0 = "χ i::('sz::finite). x" interpret ll: ll_on_open "UNIV" "(λt x. χ i::('sz::finite). 0)" UNIV using gt_ex by unfold_locales (auto simp: interval_def continuous_on_def local_lipschitz_def intro!: lipschitz_intros) have foo1:"?t0.0 ∈ ?T" by auto have foo2:"?x0.0 ∈ ?X" by auto let ?v = "ll.flow ?t0.0 ?x0.0" from ll.flow_solves_ode[OF foo1 foo2] have solves:"(ll.flow ?t0.0 ?x0.0 solves_ode ?f) (ll.existence_ivl ?t0.0 ?x0.0) ?X" by (auto) then have solves:"(?v solves_ode ?f) (ll.existence_ivl ?t0.0 ?x0.0) ?X" by auto have thex0: "(?v ?t0.0)$ (i::('sz::finite)) = x" by auto
have sol_help: "(?v solves_ode ?f) (ll.existence_ivl  ?t0.0 ?x0.0) ?X" using solves by auto
have ivl:"ll.existence_ivl ?t0.0 ?x0.0 = UNIV"
by (rule ll.existence_ivl_eq_domain)
(auto intro!: exI[where x=0] simp: vec_eq_iff)
have sol: "(?v solves_ode ?f) UNIV ?X" using solves ivl by auto
have thef0: "⋀t x. ?f t x $i = 0" by auto from constant_when_zero [OF thex0 sol thef0] have "?v t$ i = x"
by auto
thus ?thesis by auto
qed

lemma MVT_ivl:
fixes f::"'a::ordered_euclidean_space⇒'b::ordered_euclidean_space"
assumes fderiv: "⋀x. x ∈ D ⟹ (f has_derivative J x) (at x within D)"
assumes J_ivl: "⋀x. x ∈ D ⟹ J x u ≥ J0"
assumes line_in: "⋀x. x ∈ {0..1} ⟹ a + x *⇩R u ∈ D"
shows "f (a + u) - f a ≥ J0"
proof -
from MVT_corrected[OF fderiv line_in] obtain t where
t: "t∈Basis → {0<..<1}" and
mvt: "f (a + u) - f a = (∑i∈Basis. (J (a + t i *⇩R u) u ∙ i) *⇩R i)"
by auto
note mvt
also have "… ≥ J0"
proof -
have J: "⋀i. i ∈ Basis ⟹ J0 ≤ J (a + t i *⇩R u) u"
using J_ivl t line_in by (auto simp: Pi_iff)
show ?thesis
using J
unfolding atLeastAtMost_iff eucl_le[where 'a='b]
by auto
qed
finally show ?thesis .
qed

lemma MVT_ivl':
fixes f::"'a::ordered_euclidean_space⇒'b::ordered_euclidean_space"
assumes fderiv: "(⋀x. x ∈ D ⟹ (f has_derivative J x) (at x within D))"
assumes J_ivl: "⋀x. x ∈ D ⟹ J x (a - b) ≥ J0"
assumes line_in: "⋀x. x ∈ {0..1} ⟹ b + x *⇩R (a - b) ∈ D"
shows "f a ≥ f b + J0"
proof -
have "f (b + (a - b)) - f b ≥ J0"
apply (rule MVT_ivl[OF fderiv ])
apply assumption
apply (rule J_ivl) apply assumption
using line_in
apply (auto simp: diff_le_eq le_diff_eq ac_simps)
done
thus ?thesis
by (auto simp: diff_le_eq le_diff_eq ac_simps)
qed
end


# Theory Syntax

theory Syntax
imports
Complex_Main
"Ids"
begin
section ‹Syntax›
text ‹
We define the syntax of dL terms, formulas and hybrid programs. As in
CADE'15, the syntax allows arbitrarily nested differentials. However,
the semantics of such terms is very surprising (e.g. (x')' is zero in
every state), so we define predicates dfree and dsafe to describe terms
with no differentials and no nested differentials, respectively.

In keeping with the CADE'15 presentation we currently make the simplifying
assumption that all terms are smooth, and thus division and arbitrary
exponentiation are absent from the syntax. Several other standard logical
constructs are implemented as derived forms to reduce the soundness burden.

The types of formulas and programs are parameterized by three finite types
('a, 'b, 'c) used as identifiers for function constants, context constants, and
everything else, respectively. These type variables are distinct because some
substitution operations affect one type variable while leaving the others unchanged.
Because these types will be finite in practice, it is more useful to think of them
as natural numbers that happen to be represented as types (due to HOL's lack of dependent types).
The types of terms and ODE systems follow the same approach, but have only two type
variables because they cannot contain contexts.
›
datatype ('a, 'c) trm =
― ‹Real-valued variables given meaning by the state and modified by programs.›
Var 'c
― ‹N.B. This is technically more expressive than true dL since most reals›
― ‹can't be written down.›
| Const real
― ‹A function (applied to its arguments) consists of an identifier for the function›
― ‹and a function ‹'c ⇒ ('a, 'c) trm› (where ‹'c› is a finite type) which specifies one›
― ‹argument of the function for each element of type ‹'c›. To simulate a function with›
― ‹less than ‹'c› arguments, set the remaining arguments to a constant, such as ‹Const 0››
| Function 'a "'c ⇒ ('a, 'c) trm" ("$f") | Plus "('a, 'c) trm" "('a, 'c) trm" | Times "('a, 'c) trm" "('a, 'c) trm" ― ‹A (real-valued) variable standing for a differential, such as ‹x'›, given meaning by the state› ― ‹and modified by programs.› | DiffVar 'c ("$''")
― ‹The differential of an arbitrary term ‹(θ)'››
| Differential "('a, 'c) trm"

datatype('a, 'c) ODE =
― ‹Variable standing for an ODE system, given meaning by the interpretation›
OVar 'c
― ‹Singleton ODE defining ‹x' = θ›, where ‹θ› may or may not contain ‹x››
― ‹(but must not contain differentials)›
| OSing 'c "('a, 'c) trm"
― ‹The product ‹OProd ODE1 ODE2› composes two ODE systems in parallel, e.g.›
― ‹‹OProd (x' = y) (y' = -x)› is the system ‹{x' = y, y' = -x}››
| OProd "('a, 'c) ODE" "('a, 'c) ODE"

datatype ('a, 'b, 'c) hp =
― ‹Variables standing for programs, given meaning by the interpretation.›
Pvar 'c                           ("$α") ― ‹Assignment to a real-valued variable ‹x := θ›› | Assign 'c "('a, 'c) trm" (infixr ":=" 10) ― ‹Assignment to a differential variable› | DiffAssign 'c "('a, 'c) trm" ― ‹Program ‹?φ› succeeds iff ‹φ› holds in current state.› | Test "('a, 'b, 'c) formula" ("?") ― ‹An ODE program is an ODE system with some evolution domain.› | EvolveODE "('a, 'c) ODE" "('a, 'b, 'c) formula" ― ‹Non-deterministic choice between two programs ‹a› and ‹b›› | Choice "('a, 'b, 'c) hp" "('a, 'b, 'c) hp" (infixl "∪∪" 10) ― ‹Sequential composition of two programs ‹a› and ‹b›› | Sequence "('a, 'b, 'c) hp" "('a, 'b, 'c) hp" (infixr ";;" 8) ― ‹Nondeterministic repetition of a program ‹a›, zero or more times.› | Loop "('a, 'b, 'c) hp" ("_**") and ('a, 'b, 'c) formula = Geq "('a, 'c) trm" "('a, 'c) trm" | Prop 'c "'c ⇒ ('a, 'c) trm" ("$φ")
| Not "('a, 'b, 'c) formula"            ("!")
| And "('a, 'b, 'c) formula" "('a, 'b, 'c) formula"    (infixl "&&" 8)
| Exists 'c "('a, 'b, 'c) formula"
― ‹‹⟨α⟩φ› iff exists run of ‹α› where ‹φ› is true in end state›
| Diamond "('a, 'b, 'c) hp" "('a, 'b, 'c) formula"         ("(⟨ _ ⟩ _)" 10)
― ‹Contexts ‹C› are symbols standing for functions from (the semantics of) formulas to›
― ‹(the semantics of) formulas, thus ‹C(φ)› is another formula. While not necessary›
― ‹in terms of expressiveness, contexts allow for more efficient reasoning principles.›
| InContext 'b "('a, 'b, 'c) formula"

― ‹Derived forms›
definition Or :: "('a, 'b, 'c) formula ⇒ ('a, 'b, 'c) formula ⇒ ('a, 'b, 'c) formula" (infixl "||" 7)
where "Or P Q = Not (And (Not P) (Not Q))"

definition Implies :: "('a, 'b, 'c) formula ⇒ ('a, 'b, 'c) formula ⇒ ('a, 'b, 'c) formula" (infixr "→" 10)
where "Implies P Q = Or Q (Not P)"

definition Equiv :: "('a, 'b, 'c) formula ⇒ ('a, 'b, 'c) formula ⇒ ('a, 'b, 'c) formula" (infixl "↔" 10)
where "Equiv P Q = Or (And P Q) (And (Not P) (Not Q))"

definition Forall :: "'c ⇒ ('a, 'b, 'c) formula ⇒ ('a, 'b, 'c) formula"
where "Forall x P = Not (Exists x (Not P))"

definition Equals :: "('a, 'c) trm ⇒ ('a, 'c) trm ⇒ ('a, 'b, 'c) formula"
where "Equals θ θ' = ((Geq θ θ') && (Geq θ' θ))"

definition Greater :: "('a, 'c) trm ⇒ ('a, 'c) trm ⇒ ('a, 'b, 'c) formula"
where "Greater θ θ' = ((Geq θ θ') && (Not (Geq θ' θ)))"

definition Box :: "('a, 'b, 'c) hp ⇒ ('a, 'b, 'c) formula ⇒ ('a, 'b, 'c) formula" ("([[_]]_)" 10)
where "Box α P = Not (Diamond α (Not P))"

definition TT ::"('a,'b,'c) formula"
where "TT = Geq (Const 0) (Const 0)"

definition FF ::"('a,'b,'c) formula"
where "FF = Geq (Const 0) (Const 1)"

type_synonym ('a,'b,'c) sequent = "('a,'b,'c) formula list * ('a,'b,'c) formula list"
― ‹Rule: assumptions, then conclusion›
type_synonym ('a,'b,'c) rule = "('a,'b,'c) sequent list * ('a,'b,'c) sequent"

― ‹silliness to enable proving disequality lemmas›
primrec sizeF::"('sf,'sc, 'sz) formula ⇒ nat"
and   sizeP::"('sf,'sc, 'sz) hp ⇒ nat"
where
"sizeP (Pvar a) = 1"
| "sizeP (Assign x θ) = 1"
| "sizeP (DiffAssign x θ) = 1"
| "sizeP (Test φ) = Suc (sizeF φ)"
| "sizeP (EvolveODE ODE φ) = Suc (sizeF φ)"
| "sizeP (Choice α β) = Suc (sizeP α + sizeP β)"
| "sizeP (Sequence α β) = Suc (sizeP α + sizeP β)"
| "sizeP (Loop α) = Suc (sizeP α)"
| "sizeF (Geq p q) = 1"
| "sizeF (Prop p args) = 1"
| "sizeF (Not p) = Suc (sizeF p)"
| "sizeF (And p q) = sizeF p + sizeF q"
| "sizeF (Exists x p) = Suc (sizeF p)"
| "sizeF (Diamond p q) = Suc (sizeP p + sizeF q)"
| "sizeF (InContext C φ) = Suc (sizeF φ)"

lemma sizeF_diseq:"sizeF p ≠ sizeF q ⟹ p ≠ q" by auto

named_theorems "expr_diseq" "Structural disequality rules for expressions"
lemma [expr_diseq]:"p ≠ And p q" by(induction p, auto)
lemma [expr_diseq]:"q ≠ And p q" by(induction q, auto)
lemma [expr_diseq]:"p ≠ Not p" by(induction p, auto)
lemma [expr_diseq]:"p ≠ Or p q" by(rule sizeF_diseq, auto simp add: Or_def)
lemma [expr_diseq]:"q ≠ Or p q" by(rule sizeF_diseq, auto simp add: Or_def)
lemma [expr_diseq]:"p ≠ Implies p q" by(rule sizeF_diseq, auto simp add: Implies_def Or_def)
lemma [expr_diseq]:"q ≠ Implies p q" by(rule sizeF_diseq, auto simp add: Implies_def Or_def)
lemma [expr_diseq]:"p ≠ Equiv p q" by(rule sizeF_diseq, auto simp add: Equiv_def Or_def)
lemma [expr_diseq]:"q ≠ Equiv p q" by(rule sizeF_diseq, auto simp add: Equiv_def Or_def)
lemma [expr_diseq]:"p ≠ Exists x p" by(induction p, auto)
lemma [expr_diseq]:"p ≠ Diamond a p" by(induction p, auto)
lemma [expr_diseq]:"p ≠ InContext C p" by(induction p, auto)

― ‹A predicational is like a context with no argument, i.e. a variable standing for a›
― ‹state-dependent formula, given meaning by the interpretation. This differs from a predicate›
― ‹because predicates depend only on their arguments (which might then indirectly depend on the state).›
― ‹We encode a predicational as a context applied to a formula whose truth value is constant with›
― ‹respect to the state (specifically, always true)›
fun Predicational :: "'b ⇒ ('a, 'b, 'c) formula" ("Pc")
where "Predicational P = InContext P (Geq (Const 0) (Const 0))"

― ‹Abbreviations for common syntactic constructs in order to make axiom definitions, etc. more›
context ids begin
― ‹"Empty" function argument tuple, encoded as tuple where all arguments assume a constant value.›
definition empty::" 'b ⇒ ('a, 'b) trm"
where "empty ≡ λi.(Const 0)"

― ‹Function argument tuple with (effectively) one argument, where all others have a constant value.›
fun singleton :: "('a, 'sz) trm ⇒ ('sz ⇒ ('a, 'sz) trm)"
where "singleton t i = (if i = vid1 then t else (Const 0))"

lemma expand_singleton:"singleton t = (λi. (if i = vid1 then t else (Const 0)))"
by auto

― ‹Function applied to one argument›
definition f1::"'sf ⇒ 'sz ⇒ ('sf,'sz) trm"
where "f1 f x = Function f (singleton (Var x))"

― ‹Function applied to zero arguments (simulates a constant symbol given meaning by the interpretation)›
definition f0::"'sf ⇒ ('sf,'sz) trm"
where "f0 f = Function f empty"

― ‹Predicate applied to one argument›
definition p1::"'sz ⇒ 'sz ⇒ ('sf, 'sc, 'sz) formula"
where "p1 p x = Prop p (singleton (Var x))"

― ‹Predicational›
definition P::"'sc ⇒ ('sf, 'sc, 'sz) formula"
where "P p = Predicational p"
end

subsection ‹Well-Formedness predicates›
inductive dfree :: "('a, 'c) trm ⇒ bool"
where
dfree_Var: "dfree (Var i)"
| dfree_Const: "dfree (Const r)"
| dfree_Fun: "(⋀i. dfree (args i)) ⟹ dfree (Function i args)"
| dfree_Plus: "dfree θ⇩1 ⟹ dfree θ⇩2 ⟹ dfree (Plus θ⇩1 θ⇩2)"
| dfree_Times: "dfree θ⇩1 ⟹ dfree θ⇩2 ⟹ dfree (Times θ⇩1 θ⇩2)"

inductive dsafe :: "('a, 'c) trm ⇒ bool"
where
dsafe_Var: "dsafe (Var i)"
| dsafe_Const: "dsafe (Const r)"
| dsafe_Fun: "(⋀i. dsafe (args i)) ⟹ dsafe (Function i args)"
| dsafe_Plus: "dsafe θ⇩1 ⟹ dsafe θ⇩2 ⟹ dsafe (Plus θ⇩1 θ⇩2)"
| dsafe_Times: "dsafe θ⇩1 ⟹ dsafe θ⇩2 ⟹ dsafe (Times θ⇩1 θ⇩2)"
| dsafe_Diff: "dfree θ ⟹ dsafe (Differential θ)"
| dsafe_DiffVar: "dsafe ($' i)" ― ‹Explictly-written variables that are bound by the ODE. Needed to compute whether› ― ‹ODE's are valid (e.g. whether they bind the same variable twice)› fun ODE_dom::"('a, 'c) ODE ⇒ 'c set" where "ODE_dom (OVar c) = {}" | "ODE_dom (OSing x θ) = {x}" | "ODE_dom (OProd ODE1 ODE2) = ODE_dom ODE1 ∪ ODE_dom ODE2" inductive osafe:: "('a, 'c) ODE ⇒ bool" where osafe_Var:"osafe (OVar c)" | osafe_Sing:"dfree θ ⟹ osafe (OSing x θ)" | osafe_Prod:"osafe ODE1 ⟹ osafe ODE2 ⟹ ODE_dom ODE1 ∩ ODE_dom ODE2 = {} ⟹ osafe (OProd ODE1 ODE2)" ― ‹Programs/formulas without any differential terms. This definition not currently used but may› ― ‹be useful in the future.› inductive hpfree:: "('a, 'b, 'c) hp ⇒ bool" and ffree:: "('a, 'b, 'c) formula ⇒ bool" where "hpfree (Pvar x)" | "dfree e ⟹ hpfree (Assign x e)" ― ‹Differential programs allowed but not differential terms› | "dfree e ⟹ hpfree (DiffAssign x e)" | "ffree P ⟹ hpfree (Test P)" ― ‹Differential programs allowed but not differential terms› | "osafe ODE ⟹ ffree P ⟹ hpfree (EvolveODE ODE P)" | "hpfree a ⟹ hpfree b ⟹ hpfree (Choice a b )" | "hpfree a ⟹ hpfree b ⟹ hpfree (Sequence a b)" | "hpfree a ⟹ hpfree (Loop a)" | "ffree f ⟹ ffree (InContext C f)" | "(⋀arg. arg ∈ range args ⟹ dfree arg) ⟹ ffree (Prop p args)" | "ffree p ⟹ ffree (Not p)" | "ffree p ⟹ ffree q ⟹ ffree (And p q)" | "ffree p ⟹ ffree (Exists x p)" | "hpfree a ⟹ ffree p ⟹ ffree (Diamond a p)" | "ffree (Predicational P)" | "dfree t1 ⟹ dfree t2 ⟹ ffree (Geq t1 t2)" inductive hpsafe:: "('a, 'b, 'c) hp ⇒ bool" and fsafe:: "('a, 'b, 'c) formula ⇒ bool" where hpsafe_Pvar:"hpsafe (Pvar x)" | hpsafe_Assign:"dsafe e ⟹ hpsafe (Assign x e)" | hpsafe_DiffAssign:"dsafe e ⟹ hpsafe (DiffAssign x e)" | hpsafe_Test:"fsafe P ⟹ hpsafe (Test P)" | hpsafe_Evolve:"osafe ODE ⟹ fsafe P ⟹ hpsafe (EvolveODE ODE P)" | hpsafe_Choice:"hpsafe a ⟹ hpsafe b ⟹ hpsafe (Choice a b )" | hpsafe_Sequence:"hpsafe a ⟹ hpsafe b ⟹ hpsafe (Sequence a b)" | hpsafe_Loop:"hpsafe a ⟹ hpsafe (Loop a)" | fsafe_Geq:"dsafe t1 ⟹ dsafe t2 ⟹ fsafe (Geq t1 t2)" | fsafe_Prop:"(⋀i. dsafe (args i)) ⟹ fsafe (Prop p args)" | fsafe_Not:"fsafe p ⟹ fsafe (Not p)" | fsafe_And:"fsafe p ⟹ fsafe q ⟹ fsafe (And p q)" | fsafe_Exists:"fsafe p ⟹ fsafe (Exists x p)" | fsafe_Diamond:"hpsafe a ⟹ fsafe p ⟹ fsafe (Diamond a p)" | fsafe_InContext:"fsafe f ⟹ fsafe (InContext C f)" ― ‹Auto-generated simplifier rules for safety predicates› inductive_simps dfree_Plus_simps[simp]: "dfree (Plus a b)" and dfree_Times_simps[simp]: "dfree (Times a b)" and dfree_Var_simps[simp]: "dfree (Var x)" and dfree_DiffVar_simps[simp]: "dfree (DiffVar x)" and dfree_Differential_simps[simp]: "dfree (Differential x)" and dfree_Fun_simps[simp]: "dfree (Function i args)" and dfree_Const_simps[simp]: "dfree (Const r)" inductive_simps dsafe_Plus_simps[simp]: "dsafe (Plus a b)" and dsafe_Times_simps[simp]: "dsafe (Times a b)" and dsafe_Var_simps[simp]: "dsafe (Var x)" and dsafe_DiffVar_simps[simp]: "dsafe (DiffVar x)" and dsafe_Fun_simps[simp]: "dsafe (Function i args)" and dsafe_Diff_simps[simp]: "dsafe (Differential a)" and dsafe_Const_simps[simp]: "dsafe (Const r)" inductive_simps osafe_OVar_simps[simp]:"osafe (OVar c)" and osafe_OSing_simps[simp]:"osafe (OSing x θ)" and osafe_OProd_simps[simp]:"osafe (OProd ODE1 ODE2)" inductive_simps hpsafe_Pvar_simps[simp]: "hpsafe (Pvar a)" and hpsafe_Sequence_simps[simp]: "hpsafe (a ;; b)" and hpsafe_Loop_simps[simp]: "hpsafe (a**)" and hpsafe_ODE_simps[simp]: "hpsafe (EvolveODE ODE p)" and hpsafe_Choice_simps[simp]: "hpsafe (a ∪∪ b)" and hpsafe_Assign_simps[simp]: "hpsafe (Assign x e)" and hpsafe_DiffAssign_simps[simp]: "hpsafe (DiffAssign x e)" and hpsafe_Test_simps[simp]: "hpsafe (? p)" and fsafe_Geq_simps[simp]: "fsafe (Geq t1 t2)" and fsafe_Prop_simps[simp]: "fsafe (Prop p args)" and fsafe_Not_simps[simp]: "fsafe (Not p)" and fsafe_And_simps[simp]: "fsafe (And p q)" and fsafe_Exists_simps[simp]: "fsafe (Exists x p)" and fsafe_Diamond_simps[simp]: "fsafe (Diamond a p)" and fsafe_Context_simps[simp]: "fsafe (InContext C p)" definition Ssafe::"('sf,'sc,'sz) sequent ⇒ bool" where "Ssafe S ⟷((∀i. i ≥ 0 ⟶ i < length (fst S) ⟶ fsafe (nth (fst S) i)) ∧(∀i. i ≥ 0 ⟶ i < length (snd S) ⟶ fsafe (nth (snd S) i)))" definition Rsafe::"('sf,'sc,'sz) rule ⇒ bool" where "Rsafe R ⟷ ((∀i. i ≥ 0 ⟶ i < length (fst R) ⟶ Ssafe (nth (fst R) i)) ∧ Ssafe (snd R))" ― ‹Basic reasoning principles about syntactic constructs, including inductive principles› lemma dfree_is_dsafe: "dfree θ ⟹ dsafe θ" by (induction rule: dfree.induct) (auto intro: dsafe.intros) lemma hp_induct [case_names Var Assign DiffAssign Test Evolve Choice Compose Star]: "(⋀x. P ($α x)) ⟹
(⋀x1 x2. P (x1 := x2)) ⟹
(⋀x1 x2. P (DiffAssign x1 x2)) ⟹
(⋀x. P (? x)) ⟹
(⋀x1 x2. P (EvolveODE x1 x2)) ⟹
(⋀x1 x2. P x1 ⟹ P x2 ⟹ P (x1 ∪∪ x2)) ⟹
(⋀x1 x2. P x1 ⟹ P x2 ⟹ P (x1 ;; x2)) ⟹
(⋀x. P x ⟹ P x**) ⟹
P hp"
by(induction rule: hp.induct) (auto)

lemma fml_induct:
"(⋀t1 t2. P (Geq t1 t2))
⟹ (⋀p args. P (Prop p args))
⟹ (⋀p. P p ⟹ P (Not p))
⟹ (⋀p q. P p ⟹ P q ⟹ P (And p q))
⟹ (⋀x p. P p ⟹ P (Exists x p))
⟹ (⋀a p. P p ⟹ P (Diamond a p))
⟹ (⋀C p. P p ⟹ P (InContext C p))
⟹ P φ"
by (induction rule: formula.induct) (auto)

context ids begin
lemma proj_sing1:"(singleton θ vid1) = θ"
by (auto)

lemma proj_sing2:"vid1 ≠ y  ⟹ (singleton θ y) = (Const 0)"
by (auto)
end

end


# Theory Denotational_Semantics

theory "Denotational_Semantics"
imports
Ordinary_Differential_Equations.ODE_Analysis
"Lib"
"Ids"
"Syntax"
begin
subsection ‹Denotational Semantics›
text ‹
The canonical dynamic semantics of dL are given as a denotational semantics.
The important definitions for the denotational semantics are states $\nu$,
interpretations I and the semantic functions $[[\psi]]I$, $[[\theta]]I\nu$,
$[[\alpha]]I$, which are represented by the Isabelle functions \verb|fml_sem|,
\verb|dterm_sem| and \verb|prog_sem|, respectively.
›
subsection ‹States›
text ‹We formalize a state S as a pair $(S_V, S_V') : R^n \times R^n$, where $S_V$ assigns
values to the program variables and $S_V$' assigns values to their
differentials. Function constants are also formalized as having a fixed arity
m \verb|(Rvec_dim)| which may differ from n. If a function does not need to
have m arguments, any remaining arguments can be uniformly set to 0,
which simulates the affect of having functions of less arguments.

Most semantic proofs need to reason about states agreeing on variables.
We say Vagree A B V if states A and B have the same values on all variables in V,
similarly with VSagree A B V for simple states A and B and Iagree I J V for interpretations
I and J.
›

― ‹Vector of reals of length ‹'a››
type_synonym 'a Rvec = "real^('a::finite)"
― ‹A state specifies one vector of values for unprimed variables ‹x› and a second vector for ‹x'››
type_synonym 'a state = "'a Rvec × 'a Rvec"
― ‹‹'a simple_state› is half a state - either the ‹x›s or the ‹x'›s›
type_synonym 'a simple_state = "'a Rvec"

definition Vagree :: "'c::finite state ⇒ 'c state ⇒ ('c + 'c) set ⇒ bool"
where "Vagree ν ν' V ≡
(∀i. Inl i ∈ V ⟶ fst ν $i = fst ν'$ i)
∧ (∀i. Inr i ∈ V ⟶ snd ν $i = snd ν'$ i)"

definition VSagree :: "'c::finite simple_state ⇒ 'c simple_state ⇒ 'c set ⇒ bool"
where "VSagree ν ν' V ⟷ (∀i ∈ V. (ν $i) = (ν'$ i))"

― ‹Agreement lemmas›
lemma agree_nil:"Vagree ν ω {}"

lemma agree_supset:"A ⊇ B ⟹ Vagree ν ν' A ⟹ Vagree ν ν' B"

lemma VSagree_nil:"VSagree ν ω {}"

lemma VSagree_supset:"A ⊇ B ⟹ VSagree ν ν' A ⟹ VSagree ν ν' B"

lemma VSagree_UNIV_eq:"VSagree A B UNIV ⟹ A = B"
unfolding VSagree_def by (auto simp add: vec_eq_iff)

lemma agree_comm:"⋀A B V. Vagree A B V ⟹ Vagree B A V" unfolding Vagree_def by auto

lemma agree_sub:"⋀ν ω A B . A ⊆ B ⟹ Vagree ν ω B ⟹ Vagree ν ω A"
unfolding Vagree_def by auto

lemma agree_UNIV_eq:"⋀ν ω. Vagree ν ω UNIV ⟹ ν = ω"
unfolding Vagree_def by (auto simp add: vec_eq_iff)

lemma agree_UNIV_fst:"⋀ν ω. Vagree ν ω (Inl  UNIV) ⟹ (fst ν) = (fst ω)"
unfolding Vagree_def by (auto simp add: vec_eq_iff)

lemma agree_UNIV_snd:"⋀ν ω. Vagree ν ω (Inr  UNIV) ⟹ (snd ν) = (snd ω)"
unfolding Vagree_def by (auto simp add: vec_eq_iff)

lemma Vagree_univ:"⋀a b c d. Vagree (a,b) (c,d) UNIV ⟹ a = c ∧ b = d"
by (auto simp add: Vagree_def vec_eq_iff)

lemma agree_union:"⋀ν ω A B. Vagree ν ω A ⟹ Vagree ν ω B ⟹ Vagree ν ω (A ∪ B)"
unfolding Vagree_def by (auto simp add: vec_eq_iff)

lemma agree_trans:"Vagree ν μ A ⟹ Vagree μ ω B ⟹ Vagree ν ω (A ∩ B)"

lemma agree_refl:"Vagree ν ν A"

lemma VSagree_sub:"⋀ν ω A B . A ⊆ B ⟹ VSagree ν ω B ⟹ VSagree ν ω A"
unfolding VSagree_def by auto

lemma VSagree_refl:"VSagree ν ν A"

subsection Interpretations
text‹
For convenience we pretend interpretations contain an extra field called
FunctionFrechet specifying the Frechet derivative \verb|(FunctionFrechet f ν)| : $R^m \rightarrow R$
for every function in every state. The proposition \verb|(is_interp I)| says that such a
derivative actually exists and is continuous (i.e. all functions are C1-continuous)
without saying what the exact derivative is.

The type parameters 'a, 'b, 'c are finite types whose cardinalities indicate the maximum number
of functions, contexts, and <everything else defined by the interpretation>, respectively.
›
record ('a, 'b, 'c) interp =
Functions       :: "'a ⇒ 'c Rvec ⇒ real"
Predicates      :: "'c ⇒ 'c Rvec ⇒ bool"
Contexts        :: "'b ⇒ 'c state set ⇒ 'c state set"
Programs        :: "'c ⇒ ('c state * 'c state) set"
ODEs            :: "'c ⇒ 'c simple_state ⇒ 'c simple_state"
ODEBV           :: "'c ⇒ 'c set"

fun FunctionFrechet :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ 'a ⇒ 'c Rvec ⇒ 'c Rvec ⇒ real"
where "FunctionFrechet I i = (THE f'. ∀ x. (Functions I i has_derivative f' x) (at x))"

― ‹For an interpretation to be valid, all functions must be differentiable everywhere.›
definition is_interp :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ bool"
where "is_interp I ≡
∀x. ∀i. ((FDERIV (Functions I i) x :> (FunctionFrechet I i x)) ∧ continuous_on UNIV (λx. Blinfun (FunctionFrechet I i x)))"

lemma is_interpD:"is_interp I ⟹ ∀x. ∀i. (FDERIV (Functions I i) x :> (FunctionFrechet I i x))"
unfolding is_interp_def by auto

― ‹Agreement between interpretations.›
definition Iagree :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a + 'b + 'c) set ⇒ bool"
where "Iagree I J V ≡
(∀i∈V.
(∀x. i = Inl x ⟶ Functions I x = Functions J x) ∧
(∀x. i = Inr (Inl x) ⟶ Contexts I x = Contexts J x) ∧
(∀x. i = Inr (Inr x) ⟶ Predicates I x = Predicates J x) ∧
(∀x. i = Inr (Inr x) ⟶ Programs I x = Programs J x) ∧
(∀x. i = Inr (Inr x) ⟶ ODEs I x = ODEs J x) ∧
(∀x. i = Inr (Inr x) ⟶ ODEBV I x = ODEBV J x))"

lemma Iagree_Func:"Iagree I J V ⟹ Inl f ∈ V ⟹ Functions I f = Functions J f"
unfolding Iagree_def by auto

lemma Iagree_Contexts:"Iagree I J V ⟹ Inr (Inl C) ∈ V ⟹ Contexts I C = Contexts J C"
unfolding Iagree_def by auto

lemma Iagree_Pred:"Iagree I J V ⟹ Inr (Inr p) ∈ V ⟹ Predicates I p = Predicates J p"
unfolding Iagree_def by auto

lemma Iagree_Prog:"Iagree I J V ⟹ Inr (Inr a) ∈ V ⟹ Programs I a = Programs J a"
unfolding Iagree_def by auto

lemma Iagree_ODE:"Iagree I J V ⟹ Inr (Inr a) ∈ V ⟹ ODEs I a = ODEs J a"
unfolding Iagree_def by auto

lemma Iagree_comm:"⋀A B V. Iagree A B V ⟹ Iagree B A V"
unfolding Iagree_def by auto

lemma Iagree_sub:"⋀I J A B . A ⊆ B ⟹ Iagree I J B ⟹ Iagree I J A"
unfolding Iagree_def by auto

lemma Iagree_refl:"Iagree I I A"

― ‹Semantics for differential-free terms. Because there are no differentials, depends only on the ‹x› variables›
― ‹and not the ‹x'› variables.›
primrec sterm_sem :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a, 'c) trm ⇒ 'c simple_state ⇒ real"
where
"sterm_sem I (Var x) v = v $x" | "sterm_sem I (Function f args) v = Functions I f (χ i. sterm_sem I (args i) v)" | "sterm_sem I (Plus t1 t2) v = sterm_sem I t1 v + sterm_sem I t2 v" | "sterm_sem I (Times t1 t2) v = sterm_sem I t1 v * sterm_sem I t2 v" | "sterm_sem I (Const r) v = r" | "sterm_sem I ($' c) v = undefined"
| "sterm_sem I (Differential d) v = undefined"

― ‹‹frechet I θ ν› syntactically computes the frechet derivative of the term ‹θ› in the interpretation›
― ‹‹I› at state ‹ν› (containing only the unprimed variables). The frechet derivative is a›
― ‹linear map from the differential state ‹ν› to reals.›
primrec frechet :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a, 'c) trm ⇒ 'c simple_state ⇒ 'c simple_state ⇒ real"
where
"frechet I (Var x) v = (λv'. v' ∙ axis x 1)"
| "frechet I (Function f args) v =
(λv'. FunctionFrechet I f (χ i. sterm_sem I (args i) v) (χ i. frechet I (args i) v v'))"
| "frechet I (Plus t1 t2) v = (λv'. frechet I t1 v v' + frechet I t2 v v')"
| "frechet I (Times t1 t2) v =
(λv'. sterm_sem I t1 v * frechet I t2 v v' + frechet I t1 v v' * sterm_sem I t2 v)"
| "frechet I (Const r) v = (λv'. 0)"
| "frechet I ($' c) v = undefined" | "frechet I (Differential d) v = undefined" definition directional_derivative :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a, 'c) trm ⇒ 'c state ⇒ real" where "directional_derivative I t = (λv. frechet I t (fst v) (snd v))" ― ‹Sem for terms that are allowed to contain differentials.› ― ‹Note there is some duplication with ‹sterm_sem›.› primrec dterm_sem :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a, 'c) trm ⇒ 'c state ⇒ real" where "dterm_sem I (Var x) = (λv. fst v$ x)"
| "dterm_sem I (DiffVar x) = (λv. snd v $x)" | "dterm_sem I (Function f args) = (λv. Functions I f (χ i. dterm_sem I (args i) v))" | "dterm_sem I (Plus t1 t2) = (λv. (dterm_sem I t1 v) + (dterm_sem I t2 v))" | "dterm_sem I (Times t1 t2) = (λv. (dterm_sem I t1 v) * (dterm_sem I t2 v))" | "dterm_sem I (Differential t) = (λv. directional_derivative I t v)" | "dterm_sem I (Const c) = (λv. c)" text‹ The semantics of an ODE is the vector field at a given point. ODE's are all time-independent so no time variable is necessary. Terms on the RHS of an ODE must be differential-free, so depends only on the xs. The safety predicate \texttt{osafe} ensures the domains of ODE1 and ODE2 are disjoint, so vector addition is equivalent to saying "take things defined from ODE1 from ODE1, take things defined by ODE2 from ODE2"› fun ODE_sem:: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a, 'c) ODE ⇒ 'c Rvec ⇒ 'c Rvec" where ODE_sem_OVar:"ODE_sem I (OVar x) = ODEs I x" | ODE_sem_OSing:"ODE_sem I (OSing x θ) = (λν. (χ i. if i = x then sterm_sem I θ ν else 0))" ― ‹Note: Could define using ‹SOME› operator in a way that more closely matches above description,› ― ‹but that gets complicated in the ‹OVar› case because not all variables are bound by the ‹OVar›› | ODE_sem_OProd:"ODE_sem I (OProd ODE1 ODE2) = (λν. ODE_sem I ODE1 ν + ODE_sem I ODE2 ν)" ― ‹The bound variables of an ODE› fun ODE_vars :: "('a,'b,'c) interp ⇒ ('a, 'c) ODE ⇒ 'c set" where "ODE_vars I (OVar c) = ODEBV I c" | "ODE_vars I (OSing x θ) = {x}" | "ODE_vars I (OProd ODE1 ODE2) = ODE_vars I ODE1 ∪ ODE_vars I ODE2" fun semBV ::"('a, 'b,'c) interp ⇒ ('a, 'c) ODE ⇒ ('c + 'c) set" where "semBV I ODE = Inl  (ODE_vars I ODE) ∪ Inr  (ODE_vars I ODE)" lemma ODE_vars_lr: fixes x::"'sz" and ODE::"('sf,'sz) ODE" and I::"('sf,'sc,'sz) interp" shows "Inl x ∈ semBV I ODE ⟷ Inr x ∈ semBV I ODE" by (induction "ODE", auto) fun mk_xode::"('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'c::finite) ODE ⇒ 'c::finite simple_state ⇒ 'c::finite state" where "mk_xode I ODE sol = (sol, ODE_sem I ODE sol)" text‹ Given an initial state$\nu$and solution to an ODE at some point, construct the resulting state$\omega$. This is defined using the SOME operator because the concrete definition is unwieldy. › definition mk_v::"('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'c::finite) ODE ⇒ 'c::finite state ⇒ 'c::finite simple_state ⇒ 'c::finite state" where "mk_v I ODE ν sol = (THE ω. Vagree ω ν (- semBV I ODE) ∧ Vagree ω (mk_xode I ODE sol) (semBV I ODE))" ― ‹‹repv ν x r› replaces the value of (unprimed) variable ‹x› in the state ‹ν› with r› fun repv :: "'c::finite state ⇒ 'c ⇒ real ⇒ 'c state" where "repv v x r = ((χ y. if x = y then r else vec_nth (fst v) y), snd v)" ― ‹‹repd ν x' r› replaces the value of (primed) variable ‹x'› in the state ‹ν› with ‹r›› fun repd :: "'c::finite state ⇒ 'c ⇒ real ⇒ 'c state" where "repd v x r = (fst v, (χ y. if x = y then r else vec_nth (snd v) y))" ― ‹Semantics for formulas, differential formulas, programs.› fun fml_sem :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'b::finite, 'c::finite) formula ⇒ 'c::finite state set" and prog_sem :: "('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'b::finite, 'c::finite) hp ⇒ ('c::finite state * 'c::finite state) set" where "fml_sem I (Geq t1 t2) = {v. dterm_sem I t1 v ≥ dterm_sem I t2 v}" | "fml_sem I (Prop P terms) = {ν. Predicates I P (χ i. dterm_sem I (terms i) ν)}" | "fml_sem I (Not φ) = {v. v ∉ fml_sem I φ}" | "fml_sem I (And φ ψ) = fml_sem I φ ∩ fml_sem I ψ" | "fml_sem I (Exists x φ) = {v | v r. (repv v x r) ∈ fml_sem I φ}" | "fml_sem I (Diamond α φ) = {ν | ν ω. (ν, ω) ∈ prog_sem I α ∧ ω ∈ fml_sem I φ}" | "fml_sem I (InContext c φ) = Contexts I c (fml_sem I φ)" | "prog_sem I (Pvar p) = Programs I p" | "prog_sem I (Assign x t) = {(ν, ω). ω = repv ν x (dterm_sem I t ν)}" | "prog_sem I (DiffAssign x t) = {(ν, ω). ω = repd ν x (dterm_sem I t ν)}" | "prog_sem I (Test φ) = {(ν, ν) | ν. ν ∈ fml_sem I φ}" | "prog_sem I (Choice α β) = prog_sem I α ∪ prog_sem I β" | "prog_sem I (Sequence α β) = prog_sem I α O prog_sem I β" | "prog_sem I (Loop α) = (prog_sem I α)⇧*" | "prog_sem I (EvolveODE ODE φ) = ({(ν, mk_v I ODE ν (sol t)) | ν sol t. t ≥ 0 ∧ (sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I φ} ∧ sol 0 = fst ν})" context ids begin definition valid :: "('sf, 'sc, 'sz) formula ⇒ bool" where "valid φ ≡ (∀ I. ∀ ν. is_interp I ⟶ ν ∈ fml_sem I φ)" end text‹ Because mk\_v is defined with the SOME operator, need to construct a state that satisfies${\tt Vagree} \omega \nu (- {\tt ODE\_vars\ ODE})
\wedge {\tt Vagree} \omega {\tt (mk\_xode\ I\ ODE\ sol)\ (ODE\_vars\ ODE)})$to do anything useful › fun concrete_v::"('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'c::finite) ODE ⇒ 'c::finite state ⇒ 'c::finite simple_state ⇒ 'c::finite state" where "concrete_v I ODE ν sol = ((χ i. (if Inl i ∈ semBV I ODE then sol else (fst ν))$ i),
(χ i. (if Inr i ∈ semBV I ODE then ODE_sem I ODE sol else (snd ν)) $i))" lemma mk_v_exists:"∃ω. Vagree ω ν (- semBV I ODE) ∧ Vagree ω (mk_xode I ODE sol) (semBV I ODE)" by(rule exI[where x="(concrete_v I ODE ν sol)"], auto simp add: Vagree_def) lemma mk_v_agree:"Vagree (mk_v I ODE ν sol) ν (- semBV I ODE) ∧ Vagree (mk_v I ODE ν sol) (mk_xode I ODE sol) (semBV I ODE)" unfolding mk_v_def apply(rule theI[where a= "((χ i. (if Inl i ∈ semBV I ODE then sol else (fst ν))$ i),
(χ i. (if Inr i ∈ semBV I ODE then ODE_sem I ODE sol else (snd ν)) $i))"]) using exE[OF mk_v_exists, of ν I ODE sol] by (auto simp add: Vagree_def vec_eq_iff) lemma mk_v_concrete:"mk_v I ODE ν sol = ((χ i. (if Inl i ∈ semBV I ODE then sol else (fst ν))$ i),
(χ i. (if Inr i ∈ semBV I ODE then ODE_sem I ODE sol else (snd ν)) $i))" apply(rule agree_UNIV_eq) using mk_v_agree[of I ODE ν sol] unfolding Vagree_def by auto subsection ‹Trivial Simplification Lemmas› text ‹ We often want to pretend the definitions in the semantics are written slightly differently than they are. Since the simplifier has some trouble guessing that these are the right simplifications to do, we write them all out explicitly as lemmas, even though they prove trivially. › lemma svar_case: "sterm_sem I (Var x) = (λv. v$ x)"
by auto

lemma sconst_case:
"sterm_sem I (Const r) = (λv. r)"
by auto

lemma sfunction_case:
"sterm_sem I (Function f args) = (λv. Functions I f (χ i. sterm_sem I (args i) v))"
by auto

lemma splus_case:
"sterm_sem I (Plus t1 t2) = (λv. (sterm_sem I t1 v) + (sterm_sem I t2 v))"
by auto

lemma stimes_case:
"sterm_sem I (Times t1 t2) = (λv. (sterm_sem I t1 v) * (sterm_sem I t2 v))"
by auto

lemma or_sem [simp]:
"fml_sem I (Or φ ψ) = fml_sem I φ ∪ fml_sem I ψ"

lemma iff_sem [simp]: "(ν ∈ fml_sem I (A ↔ B))
⟷ ((ν ∈ fml_sem I A) ⟷ (ν ∈ fml_sem I B))"

lemma box_sem [simp]:"fml_sem I (Box α φ) = {ν. ∀ ω. (ν, ω) ∈ prog_sem I α ⟶ ω ∈ fml_sem I φ}"
unfolding Box_def fml_sem.simps
using Collect_cong by (auto)

lemma forall_sem [simp]:"fml_sem I (Forall x φ) = {v. ∀r. (repv v x r) ∈ fml_sem I φ}"
unfolding Forall_def fml_sem.simps
using Collect_cong by (auto)

lemma greater_sem[simp]:"fml_sem I (Greater θ θ') = {v. dterm_sem I θ v > dterm_sem I θ' v}"
unfolding Greater_def by auto

lemma loop_sem:"prog_sem I (Loop α) = (prog_sem I α)⇧*"
by (auto)

lemma impl_sem [simp]: "(ν ∈ fml_sem I (A → B))
= ((ν ∈ fml_sem I A) ⟶ (ν ∈ fml_sem I B))"

lemma equals_sem [simp]: "(ν ∈ fml_sem I (Equals θ θ'))
= (dterm_sem I θ ν = dterm_sem I θ' ν)"

lemma diamond_sem [simp]: "fml_sem I (Diamond α φ)
= {ν. ∃ ω. (ν, ω) ∈ prog_sem I α ∧ ω ∈ fml_sem I φ}"
by auto

lemma tt_sem [simp]:"fml_sem I TT = UNIV" unfolding TT_def by auto
lemma ff_sem [simp]:"fml_sem I FF = {}" unfolding FF_def by auto

lemma iff_to_impl: "((ν ∈ fml_sem I A) ⟷ (ν ∈ fml_sem I B))
⟷ (((ν ∈ fml_sem I A) ⟶ (ν ∈ fml_sem I B))
∧ ((ν ∈ fml_sem I B) ⟶ (ν ∈ fml_sem I A)))"
by (auto)

fun seq2fml :: "('a,'b,'c) sequent ⇒ ('a,'b,'c) formula"
where
"seq2fml (ante,succ) = Implies (foldr And ante TT) (foldr Or succ FF)"

context ids begin
fun seq_sem ::"('sf, 'sc, 'sz) interp ⇒ ('sf, 'sc, 'sz) sequent ⇒ 'sz state set"
where "seq_sem I S = fml_sem I (seq2fml S)"

lemma and_foldl_sem:"ν ∈ fml_sem I (foldr And Γ TT) ⟹ (⋀φ. List.member Γ φ ⟹ ν ∈ fml_sem I φ)"
by(induction Γ, auto simp add: member_rec)

lemma and_foldl_sem_conv:"(⋀φ. List.member Γ φ ⟹ ν ∈ fml_sem I φ) ⟹ ν ∈ fml_sem I (foldr And Γ TT)"
by(induction Γ, auto simp add: member_rec)

lemma or_foldl_sem:"List.member Γ φ ⟹ ν ∈ fml_sem I φ ⟹ ν ∈ fml_sem I (foldr Or Γ FF)"
by(induction Γ, auto simp add: member_rec)

lemma or_foldl_sem_conv:"ν ∈ fml_sem I (foldr Or Γ FF) ⟹ ∃ φ. ν ∈ fml_sem I φ ∧ List.member Γ φ"
by(induction Γ, auto simp add: member_rec)

lemma seq_semI':"(ν ∈ fml_sem I (foldr And Γ TT) ⟹ ν ∈ fml_sem I (foldr Or Δ FF)) ⟹ ν ∈ seq_sem I (Γ,Δ)"
by auto

lemma seq_semD':"⋀P. ν ∈ seq_sem I (Γ,Δ) ⟹ ((ν ∈ fml_sem I (foldr And Γ TT) ⟹ ν ∈ fml_sem I (foldr Or Δ FF)) ⟹ P) ⟹ P"
by simp

definition sublist::"'a list ⇒ 'a list ⇒ bool"
where "sublist A B ≡ (∀x. List.member A x ⟶ List.member B x)"

lemma sublistI:"(⋀x. List.member A x ⟹ List.member B x) ⟹ sublist A B"
unfolding sublist_def by auto

lemma Γ_sub_sem:"sublist Γ1 Γ2 ⟹ ν ∈ fml_sem I (foldr And Γ2 TT) ⟹ ν ∈ fml_sem I (foldr And Γ1 TT)"
unfolding sublist_def
by (metis and_foldl_sem and_foldl_sem_conv)

lemma seq_semI:"List.member Δ ψ ⟹((⋀φ. List.member Γ φ ⟹ ν ∈ fml_sem I φ) ⟹ ν ∈ fml_sem I ψ) ⟹ ν ∈ seq_sem I (Γ,Δ)"
apply(rule seq_semI')
using and_foldl_sem[of ν I Γ] or_foldl_sem by blast

lemma seq_semD:"ν ∈ seq_sem I (Γ,Δ) ⟹ (⋀φ. List.member Γ φ ⟹ ν ∈ fml_sem I φ) ⟹ ∃φ. (List.member Δ φ) ∧ν ∈ fml_sem I φ "
apply(rule seq_semD')
using and_foldl_sem_conv or_foldl_sem_conv
by blast+

lemma seq_MP:"ν ∈ seq_sem I (Γ,Δ) ⟹ ν ∈ fml_sem I (foldr And Γ TT) ⟹ ν ∈ fml_sem I (foldr Or Δ FF)"
by(induction Δ, auto)

definition seq_valid
where "seq_valid S ≡ ∀I. is_interp I ⟶ seq_sem I S = UNIV"

text‹ Soundness for derived rules is local soundness, i.e. if the premisses are all true in the same interpretation,
then the conclusion is also true in that same interpretation. ›
definition sound :: "('sf, 'sc, 'sz) rule ⇒ bool"
where "sound R ⟷ (∀I. is_interp I ⟶ (∀i. i ≥ 0 ⟶ i < length (fst R) ⟶ seq_sem I (nth (fst R) i) = UNIV) ⟶ seq_sem I (snd R) = UNIV)"

lemma soundI:"(⋀I. is_interp I ⟹ (⋀i. i ≥ 0 ⟹ i < length SG ⟹ seq_sem I (nth SG i) = UNIV) ⟹ seq_sem I G = UNIV) ⟹ sound (SG,G)"
unfolding sound_def by auto

lemma soundI':"(⋀I ν. is_interp I ⟹ (⋀i . i ≥ 0 ⟹ i < length SG ⟹ ν ∈ seq_sem I (nth SG i)) ⟹ ν ∈ seq_sem I G) ⟹ sound (SG,G)"
unfolding sound_def by auto

lemma soundI_mem:"(⋀I. is_interp I ⟹ (⋀φ. List.member SG φ ⟹ seq_sem I φ = UNIV) ⟹ seq_sem I C = UNIV) ⟹ sound (SG,C)"
by (metis in_set_conv_nth in_set_member iso_tuple_UNIV_I seq2fml.simps)

lemma soundI_memv:"(⋀I. is_interp I ⟹ (⋀φ ν. List.member SG φ ⟹ ν ∈ seq_sem I φ) ⟹ (⋀ν. ν ∈ seq_sem I C)) ⟹ sound (SG,C)"
apply(rule soundI_mem)
using impl_sem by blast

lemma soundI_memv':"(⋀I. is_interp I ⟹ (⋀φ ν. List.member SG φ ⟹ ν ∈ seq_sem I φ) ⟹ (⋀ν. ν ∈ seq_sem I C)) ⟹ R = (SG,C) ⟹ sound R"
using  soundI_mem
using impl_sem by blast

lemma soundD_mem:"sound (SG,C) ⟹ (⋀I. is_interp I ⟹ (⋀φ. List.member SG φ ⟹ seq_sem I φ = UNIV) ⟹ seq_sem I C = UNIV)"
using in_set_conv_nth in_set_member iso_tuple_UNIV_I seq2fml.simps
by (metis seq2fml.elims)

lemma soundD_memv:"sound (SG,C) ⟹ (⋀I. is_interp I ⟹ (⋀φ ν. List.member SG φ ⟹ ν ∈ seq_sem I φ) ⟹ (⋀ν. ν ∈ seq_sem I C))"
using soundD_mem
by (metis UNIV_I UNIV_eq_I)

end
end


# Theory Axioms

theory "Axioms"
imports
Ordinary_Differential_Equations.ODE_Analysis
"Ids"
"Lib"
"Syntax"
"Denotational_Semantics"
begin context ids begin

section ‹Axioms›
text ‹
The uniform substitution calculus is based on a finite list of concrete
axioms, which are defined and proved valid (as in sound) in this section. When axioms apply
to arbitrary programs or formulas, they mention concrete program or formula
variables, which are then instantiated by uniform substitution, as opposed
metavariables.

This section contains axioms and rules for propositional connectives and programs other than
ODE's. Differential axioms are handled separately because the proofs are significantly more involved.
›
named_theorems axiom_defs "Axiom definitions"

definition assign_axiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"assign_axiom ≡
([[vid1 := ($f fid1 empty)]] (Prop vid1 (singleton (Var vid1)))) ↔ Prop vid1 (singleton ($f fid1 empty))"

definition diff_assign_axiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"diff_assign_axiom ≡
([[DiffAssign vid1  ($f fid1 empty)]] (Prop vid1 (singleton (DiffVar vid1)))) ↔ Prop vid1 (singleton ($f fid1 empty))"

definition loop_iterate_axiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"loop_iterate_axiom ≡ ([[$α vid1**]]Predicational pid1) ↔ ((Predicational pid1) && ([[$α vid1]][[$α vid1**]]Predicational pid1))" definition test_axiom :: "('sf, 'sc, 'sz) formula" where [axiom_defs]:"test_axiom ≡ ([[?($φ vid2 empty)]]$φ vid1 empty) ↔ (($φ vid2 empty) → ($φ vid1 empty))" definition box_axiom :: "('sf, 'sc, 'sz) formula" where [axiom_defs]:"box_axiom ≡ (⟨$α vid1⟩Predicational pid1) ↔ !([[$α vid1]]!(Predicational pid1))" definition choice_axiom :: "('sf, 'sc, 'sz) formula" where [axiom_defs]:"choice_axiom ≡ ([[$α vid1 ∪∪ $α vid2]]Predicational pid1) ↔ (([[$α vid1]]Predicational pid1) && ([[$α vid2]]Predicational pid1))" definition compose_axiom :: "('sf, 'sc, 'sz) formula" where [axiom_defs]:"compose_axiom ≡ ([[$α vid1 ;; $α vid2]]Predicational pid1) ↔ ([[$α vid1]][[ $α vid2]]Predicational pid1)" definition Kaxiom :: "('sf, 'sc, 'sz) formula" where [axiom_defs]:"Kaxiom ≡ ([[$α vid1]]((Predicational pid1) → (Predicational pid2)))
→ ([[$α vid1]]Predicational pid1) → ([[$α vid1]]Predicational pid2)"

(* Here is an example of an old version of the induction axiom that was too weak
* and thus very easy to prove: it used predicates when it should have used predicationals.
* This serves as a reminder to be careful whether other axioms are also too weak. *)
(*
definition Ibroken :: "('sf, 'sc, 'sz) formula"
where "Ibroken ≡ ([[$$a]](P [] → ([[$$a]]$P [])) → ($P [] → ([[(a)**]]$P [])))"*) definition Iaxiom :: "('sf, 'sc, 'sz) formula" where [axiom_defs]:"Iaxiom ≡ ([[($α vid1)**]](Predicational pid1 → ([[$α vid1]]Predicational pid1))) →((Predicational pid1 → ([[($α vid1)**]]Predicational pid1)))"

definition Vaxiom :: "('sf, 'sc, 'sz) formula"
where [axiom_defs]:"Vaxiom ≡ ($φ vid1 empty) → ([[$α vid1]]($φ vid1 empty))" subsection ‹Validity proofs for axioms› text ‹Because an axiom in a uniform substitution calculus is an individual formula, proving the validity of that formula suffices to prove soundness› theorem test_valid: "valid test_axiom" by (auto simp add: valid_def test_axiom_def) lemma assign_lem1: "dterm_sem I (if i = vid1 then Var vid1 else (Const 0)) (vec_lambda (λy. if vid1 = y then Functions I fid1 (vec_lambda (λi. dterm_sem I (empty i) ν)) else vec_nth (fst ν) y), snd ν) = dterm_sem I (if i = vid1 then$f fid1 empty else (Const 0)) ν"
by (cases "i = vid1") (auto simp: proj_sing1)

lemma diff_assign_lem1:
"dterm_sem I (if i = vid1 then DiffVar vid1 else (Const 0))
(fst ν, vec_lambda (λy. if vid1 = y then Functions I fid1 (vec_lambda (λi. dterm_sem I (empty i) ν)) else  vec_nth (snd ν) y))
=
dterm_sem I (if i = vid1 then $f fid1 empty else (Const 0)) ν " by (cases "i = vid1") (auto simp: proj_sing1) theorem assign_valid: "valid assign_axiom" unfolding valid_def assign_axiom_def by (simp add: assign_lem1) theorem diff_assign_valid: "valid diff_assign_axiom" unfolding valid_def diff_assign_axiom_def by (simp add: diff_assign_lem1) lemma mem_to_nonempty: "ω ∈ S ⟹ (S ≠ {})" by (auto) lemma loop_forward: "ν ∈ fml_sem I ([[$α id1**]]Predicational pid1)
⟶ ν ∈ fml_sem I (Predicational pid1&&[[$α id1]][[$α id1**]]Predicational pid1)"
by (cases ν) (auto intro: converse_rtrancl_into_rtrancl simp add: box_sem)

lemma loop_backward:
"ν ∈ fml_sem I (Predicational pid1 && [[$α id1]][[$α id1**]]Predicational pid1)
⟶ ν ∈ fml_sem I ([[$α id1**]]Predicational pid1)" by (auto elim: converse_rtranclE simp add: box_sem) theorem loop_valid: "valid loop_iterate_axiom" apply(simp only: valid_def loop_iterate_axiom_def) apply(simp only: iff_sem) apply(simp only: HOL.iff_conv_conj_imp) apply(rule allI | rule impI)+ apply(rule conjI) apply(rule loop_forward) apply(rule loop_backward) done theorem box_valid: "valid box_axiom" unfolding valid_def box_axiom_def by(auto) theorem choice_valid: "valid choice_axiom" unfolding valid_def choice_axiom_def by (auto) theorem compose_valid: "valid compose_axiom" unfolding valid_def compose_axiom_def by (auto) theorem K_valid: "valid Kaxiom" unfolding valid_def Kaxiom_def by (auto) lemma I_axiom_lemma: fixes I::"('sf,'sc,'sz) interp" and ν assumes "is_interp I" assumes IS:"ν ∈ fml_sem I ([[$α vid1**]](Predicational pid1 →
[[$α vid1]]Predicational pid1))" assumes BC:"ν ∈ fml_sem I (Predicational pid1)" shows "ν ∈ fml_sem I ([[$α vid1**]](Predicational pid1))"
proof -
have IS':"⋀ν2. (ν, ν2) ∈ (prog_sem I ($α vid1))⇧* ⟹ ν2 ∈ fml_sem I (Predicational pid1 → [[$α vid1]](Predicational pid1))"
using IS by (auto simp add: box_sem)
have res:"⋀ν3. ((ν, ν3) ∈ (prog_sem I ($α vid1))⇧*) ⟹ ν3 ∈ fml_sem I (Predicational pid1)" proof - fix ν3 show "((ν, ν3) ∈ (prog_sem I ($α vid1))⇧*) ⟹ ν3 ∈ fml_sem I (Predicational pid1)"
apply(induction rule:rtrancl_induct)
apply(rule BC)
proof -
fix y z
assume vy:"(ν, y) ∈ (prog_sem I ($α vid1))⇧*" assume yz:"(y, z) ∈ prog_sem I ($α vid1)"
assume yPP:"y ∈ fml_sem I (Predicational pid1)"
have imp3:"y ∈ fml_sem I (Predicational pid1 → [[$α vid1 ]](Predicational pid1))" using IS' vy by (simp) have imp4:"y ∈ fml_sem I (Predicational pid1) ⟹ y ∈ fml_sem I ([[$α vid1]](Predicational pid1))"
using imp3 impl_sem by (auto)
have yaPP:"y ∈ fml_sem I ([[$α vid1]]Predicational pid1)" using imp4 yPP by auto have zPP:"z ∈ fml_sem I (Predicational pid1)" using yaPP box_sem yz mem_Collect_eq by blast show " (ν, y) ∈ (prog_sem I ($α vid1))⇧* ⟹
(y, z) ∈ prog_sem I ($α vid1) ⟹ y ∈ fml_sem I (Predicational pid1) ⟹ z ∈ fml_sem I (Predicational pid1)" using zPP by simp qed qed show "ν ∈ fml_sem I ([[$α vid1**]]Predicational pid1)"
using res by (simp add: mem_Collect_eq box_sem loop_sem)
qed

theorem I_valid: "valid Iaxiom"
apply(unfold Iaxiom_def valid_def)
apply(rule impI | rule allI)+
apply(simp only: impl_sem)
using I_axiom_lemma by blast

theorem V_valid: "valid Vaxiom"
apply(simp only: valid_def Vaxiom_def impl_sem box_sem)
apply(rule allI | rule impI)+
done

definition G_holds :: "('sf, 'sc, 'sz) formula ⇒ ('sf, 'sc, 'sz) hp ⇒ bool"
where "G_holds φ α ≡ valid φ ⟶ valid ([[α]]φ)"

definition Skolem_holds :: "('sf, 'sc, 'sz) formula ⇒ 'sz ⇒ bool"
where "Skolem_holds φ var ≡ valid φ ⟶ valid (Forall var φ)"

definition MP_holds :: "('sf, 'sc, 'sz) formula ⇒ ('sf, 'sc, 'sz) formula ⇒ bool"
where "MP_holds φ ψ ≡ valid (φ → ψ) ⟶ valid φ ⟶ valid ψ"

definition CT_holds :: "'sf ⇒ ('sf, 'sz) trm ⇒ ('sf, 'sz) trm ⇒ bool"
where "CT_holds g θ θ' ≡ valid (Equals θ θ')
⟶ valid (Equals (Function g (singleton θ)) (Function g (singleton θ')))"

definition CQ_holds :: "'sz ⇒ ('sf, 'sz) trm ⇒ ('sf, 'sz) trm ⇒ bool"
where "CQ_holds p θ θ' ≡ valid (Equals θ θ')
⟶ valid ((Prop p (singleton θ)) ↔ (Prop p (singleton θ')))"

definition CE_holds :: "'sc ⇒ ('sf, 'sc, 'sz) formula ⇒ ('sf, 'sc, 'sz) formula ⇒ bool"
where "CE_holds var φ ψ ≡ valid (φ ↔ ψ)
⟶ valid (InContext var φ ↔ InContext var ψ)"

subsection ‹Soundness proofs for rules›
theorem G_sound: "G_holds φ α"
by (simp add: G_holds_def valid_def box_sem)

theorem Skolem_sound: "Skolem_holds φ var"

theorem MP_sound: "MP_holds φ ψ"
by (auto simp add: MP_holds_def valid_def)

lemma CT_lemma:"⋀I::('sf::finite, 'sc::finite, 'sz::{finite,linorder}) interp. ⋀ a::(real, 'sz) vec. ⋀ b::(real, 'sz) vec. ∀I::('sf,'sc,'sz) interp. is_interp I ⟶ (∀a b. dterm_sem I θ (a, b) = dterm_sem I θ' (a, b)) ⟹
is_interp I ⟹
Functions I var (vec_lambda (λi. dterm_sem I (if i = vid1 then θ else  (Const 0)) (a, b))) =
Functions I var (vec_lambda (λi. dterm_sem I (if i = vid1 then θ' else (Const 0)) (a, b)))"
proof -
fix I :: "('sf::finite, 'sc::finite, 'sz::{finite,linorder}) interp" and a :: "(real, 'sz) vec" and b :: "(real, 'sz) vec"
assume a1: "is_interp I"
assume "∀I::('sf,'sc,'sz) interp. is_interp I ⟶ (∀a b. dterm_sem I θ (a, b) = dterm_sem I θ' (a, b))"
then have "∀i. dterm_sem I (if i = vid1 then θ' else (Const 0)) (a, b) = dterm_sem I (if i = vid1 then θ else (Const 0)) (a, b)"
using a1 by presburger
then show "Functions I var (vec_lambda (λi. dterm_sem I (if i = vid1 then θ else (Const 0)) (a, b)))
= Functions I var (vec_lambda (λi. dterm_sem I (if i = vid1 then θ' else (Const 0)) (a, b)))"
by presburger
qed

theorem CT_sound: "CT_holds var θ θ'"
apply(simp only: CT_holds_def valid_def equals_sem vec_extensionality vec_eq_iff)
apply(simp)
apply(rule allI | rule impI)+
done

theorem CQ_sound: "CQ_holds var θ θ'"
proof (auto simp only: CQ_holds_def valid_def equals_sem vec_extensionality vec_eq_iff singleton.simps mem_Collect_eq)
fix I :: "('sf,'sc,'sz) interp" and a b
assume sem:"∀I::('sf,'sc,'sz) interp. ∀ ν. is_interp I ⟶ dterm_sem I θ ν = dterm_sem I θ' ν"
assume good:"is_interp I"
have sem_eq:"dterm_sem I θ (a,b) = dterm_sem I θ' (a,b)"
using sem good by auto
have feq:"(χ i. dterm_sem I (if i = vid1 then θ else Const 0) (a, b)) = (χ i. dterm_sem I (if i = vid1 then θ' else Const 0) (a, b))"
apply(rule vec_extensionality)
using sem_eq by auto
then show "(a, b) ∈ fml_sem I ($φ var (singleton θ) ↔$φ var (singleton θ'))"
by auto
qed

theorem CE_sound: "CE_holds var φ ψ"
apply(simp only: CE_holds_def valid_def iff_sem)
apply(rule allI | rule impI)+
apply(simp)
apply(metis subsetI subset_antisym surj_pair)
done
end end


# Theory Frechet_Correctness

theory "Frechet_Correctness"
imports
Ordinary_Differential_Equations.ODE_Analysis
"Lib"
"Syntax"
"Denotational_Semantics"
"Ids"
begin
context ids begin
section ‹Characterization of Term Derivatives›
text ‹
This section builds up to a proof that in well-formed interpretations, all
terms have derivatives, and those derivatives agree with the expected rules
of derivatives. In particular, we show the [frechet] function given in the
denotational semantics is the true Frechet derivative of a term. From this
theorem we can recover all the standard derivative identities as corollaries.
›

lemma inner_prod_eq:
fixes i::"'a::finite"
shows "(λ(v::'a Rvec). v ∙ axis i 1) = (λ(v::'a Rvec). v $i)" unfolding cart_eq_inner_axis axis_def by (simp add: eq_commute) theorem svar_deriv: fixes x:: "'sv::finite" and ν:: "'sv Rvec" and F::"real filter" shows "((λv. v$ x) has_derivative (λv'. v' ∙ (χ i. if i = x then 1 else 0))) (at ν)"
proof -
let ?f = "(λv. v)"
let ?f' = "(λv'. v')"
let ?g = "(λv. axis x 1)"
let ?g' = "(λv. 0)"
have id_deriv: "(?f has_derivative ?f') (at ν) "
by (rule has_derivative_ident)
have const_deriv: "(?g has_derivative ?g') (at ν)"
by (rule has_derivative_const)
have inner_deriv:"((λx. inner (?f x) (?g x)) has_derivative
(λh. inner (?f ν) (?g' h) + inner (?f' h) (?g ν))) (at ν)"
by (intro has_derivative_inner [OF id_deriv const_deriv])
from inner_prod_eq
have left_eq: "(λx. inner (?f x) (?g x)) = (λv. vec_nth v x)"
by (auto)
from inner_deriv and inner_prod_eq
have better_deriv:"((λv. vec_nth v x) has_derivative
(λh. inner (?f ν) (?g' h) + inner (?f' h) (?g ν))) (at ν)"
by (metis (no_types, lifting) UNIV_I has_derivative_transform)
have vec_eq:"(χ i. if i = x then 1 else 0) = (χ i. if x = i then 1 else 0)"
by(rule vec_extensionality, auto)
have deriv_eq:"(λh. ν ∙ 0 + h ∙ axis x 1) = (λv'. v' ∙ (χ i. if i = x then 1 else 0))"
by(rule ext, auto simp add: axis_def vec_eq)
show ?thesis
apply(rule has_derivative_eq_rhs[where f'= "(λh. ν ∙ 0 + h ∙ axis x 1)"])
using better_deriv deriv_eq  by auto
qed

lemma function_case_inner:
assumes good_interp:
"(∀x i. (Functions I i has_derivative FunctionFrechet I i x) (at x))"
assumes IH:"((λv. χ i. sterm_sem I (args i) v)
has_derivative (λ v. (χ i. frechet I (args i) ν v))) (at ν)"
shows  "((λv. Functions I f (χ i. sterm_sem I (args i) v))
has_derivative (λv. frechet I ($f f args) ν v)) (at ν)" proof - let ?h = "(λv. Functions I f (χ i. sterm_sem I (args i) v))" let ?h' = "frechet I ($f f args) ν"
let ?g = "(λv. χ i. sterm_sem I (args i) v)"
let ?g' = "(λv. χ i. frechet I (args i) ν v)"
let ?f = "(λy. Functions I f y)"
let ?f' = "FunctionFrechet I f (?g ν)"
have hEqFG:  "?h  = ?f  o ?g" by (auto)
have hEqFG': "?h' = ?f' o ?g'"
proof -
have frechet_def:"frechet I (Function f args) ν
= (λv'. FunctionFrechet I f (?g ν) (χ i. frechet I (args i) ν v'))"
by (auto)
have composition:
"(λv'. FunctionFrechet I f (?g ν) (χ i. frechet I (args i) ν v'))
= (FunctionFrechet I f (?g ν)) o (λ v'. χ i. frechet I (args i) ν v')"
by (auto)
from frechet_def and composition show ?thesis by (auto)
qed
have fDeriv: "(?f has_derivative ?f') (at (?g ν))"
using good_interp is_interp_def by blast
from IH have gDeriv: "(?g has_derivative ?g') (at ν)" by (auto)
from fDeriv and gDeriv
have composeDeriv: "((?f o ?g) has_derivative (?f' o ?g')) (at ν)"
using diff_chain_at good_interp by blast
from hEqFG hEqFG' composeDeriv show ?thesis by (auto)
qed

lemma func_lemma2:"(∀x i. (Functions I i has_derivative (THE f'. ∀x. (Functions I i has_derivative f' x) (at x)) x) (at x) ∧
continuous_on UNIV (λx. Blinfun ((THE f'. ∀x. (Functions I i has_derivative f' x) (at x)) x))) ⟹
(⋀θ. θ ∈ range args ⟹ (sterm_sem I θ has_derivative frechet I θ ν) (at ν)) ⟹
((λv. Functions I f (vec_lambda(λi. sterm_sem I (args i) v))) has_derivative (λv'. (THE f'. ∀x. (Functions I f has_derivative f' x) (at x)) (χ i. sterm_sem I (args i) ν) (χ i. frechet I (args i) ν v'))) (at ν)"
proof -
assume a1: "∀x i. (Functions I i has_derivative (THE f'. ∀x. (Functions I i has_derivative f' x) (at x)) x) (at x) ∧
continuous_on UNIV (λx. Blinfun ((THE f'. ∀x. (Functions I i has_derivative f' x) (at x)) x))"
then have a1':"∀x i. (Functions I i has_derivative (THE f'. ∀x. (Functions I i has_derivative f' x) (at x)) x) (at x)" by auto
assume a2: "⋀θ. θ ∈ range args ⟹ (sterm_sem I θ has_derivative frechet I θ ν) (at ν)"
have "∀f fa v. (∃fb. ¬ (f (fb::'a) has_derivative fa fb (v::(real, 'a) vec)) (at v)) ∨ ((λv. (χ fa. (f fa v::real))) has_derivative (λva. (χ f. fa f v va))) (at v)"
using has_derivative_vec by force
then have "((λv. χ f. sterm_sem I (args f) v) has_derivative (λv. χ f. frechet I (args f) ν v)) (at ν)"
by (auto simp add: a2 has_derivative_vec)
then show "((λv. Functions I f (vec_lambda(λf. sterm_sem I (args f) v))) has_derivative (λv'. (THE f'. ∀x. (Functions I f has_derivative f' x) (at x)) (χ i. sterm_sem I (args i) ν) (χ i. frechet I (args i) ν v'))) (at ν)"
using a1' function_case_inner by auto
qed

lemma func_lemma:
"is_interp I ⟹
(⋀θ :: ('a::finite, 'c::finite) trm. θ ∈ range args ⟹ (sterm_sem I θ has_derivative frechet I θ ν) (at ν)) ⟹
(sterm_sem I ($f f args) has_derivative frechet I ($f f args) ν) (at ν)"
apply(auto simp add: sfunction_case is_interp_def function_case_inner)
apply(erule func_lemma2)
apply(auto)
done

text ‹ The syntactic definition of term derivatives agrees with the semantic definition.
Since the syntactic definition of derivative is total, this gives us that derivatives are "decidable" for
terms (modulo computations on reals) and that they obey all the expected identities, which gives
›
lemma frechet_correctness:
fixes I :: "('a::finite, 'b::finite, 'c::finite) interp" and ν
assumes good_interp: "is_interp I"
shows "dfree θ ⟹ FDERIV (sterm_sem I θ) ν :> (frechet I θ ν)"
proof (induct rule: dfree.induct)
case (dfree_Var i) then show ?case
by (auto simp add: svar_case svar_deriv axis_def)
next
case (dfree_Fun args i) with good_interp show ?case
by (intro func_lemma) auto
qed auto

text ‹If terms are semantically equivalent in all states, so are their derivatives›
lemma sterm_determines_frechet:
fixes I ::"('a1::finite, 'b1::finite, 'c::finite) interp"
and J ::"('a2::finite, 'b2::finite, 'c::finite) interp"
and θ1 :: "('a1::finite, 'c::finite) trm"
and θ2 :: "('a2::finite, 'c::finite) trm"
and ν
assumes good_interp1:"is_interp I"
assumes good_interp2:"is_interp J"
assumes free1:"dfree θ1"
assumes free2:"dfree θ2"
assumes sem:"sterm_sem I θ1 = sterm_sem J θ2"
shows "frechet I θ1 (fst ν) (snd ν) = frechet J θ2 (fst ν) (snd ν)"
proof -
have d1:"(sterm_sem I θ1 has_derivative (frechet I θ1 (fst ν))) (at (fst ν))"
using frechet_correctness[OF good_interp1 free1] by auto
have d2:"(sterm_sem J θ2 has_derivative (frechet J θ2 (fst ν))) (at (fst ν))"
using frechet_correctness[OF good_interp2 free2] by auto
then have d1':"(sterm_sem I θ1 has_derivative (frechet J θ2 (fst ν))) (at (fst ν))"
using sem by auto
thus "?thesis" using has_derivative_unique d1 d1' by metis
qed

lemma the_deriv:
assumes deriv:"(f has_derivative F) (at x)"
shows "(THE G. (f has_derivative G) (at x)) = F"
apply(rule the_equality)
subgoal by (rule deriv)
subgoal for G by (auto simp add: deriv has_derivative_unique)
done

lemma the_all_deriv:
assumes deriv:"∀x. (f has_derivative F x) (at x)"
shows "(THE G. ∀ x. (f has_derivative G x) (at x)) = F"
apply(rule the_equality)
subgoal by (rule deriv)
subgoal for G
apply(rule ext)
subgoal for x
apply(erule allE[where x=x])
by (auto simp add: deriv has_derivative_unique)
done
done

typedef ('a, 'c) strm = "{θ:: ('a,'c) trm. dfree θ}"
morphisms raw_term simple_term
by(rule exI[where x= "Const 0"], auto simp add: dfree_Const)

typedef ('a, 'b, 'c) good_interp = "{I::('a::finite,'b::finite,'c::finite) interp. is_interp I}"
morphisms raw_interp good_interp
apply(rule exI[where x="⦇ Functions = (λf x. 0), Predicates = (λp x. True), Contexts = (λC S. S), Programs = (λa. {}), ODEs = (λc v. (χ i. 0)), ODEBV = λc. {}⦈"])
proof -
fix x ::real
have eq:"(THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) = (λ_ _. 0)"
by(rule the_all_deriv, auto)
have eq':"(THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x = (λ_. 0)"
have deriv:"((λx.0) has_derivative (λx. 0)) (at x)"
by auto
then show "⋀x. ((λx. 0) has_derivative (THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x) (at x)"
by (auto simp add: eq eq' deriv)
next
have eq:"(THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) = (λ_ _. 0)"
by(rule the_all_deriv, auto)
have eq':"∀x. (THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x = (λ_. 0)"
have deriv:"⋀x. ((λx.0) has_derivative (λx. 0)) (at x)"
by auto
have blin:"⋀x. bounded_linear ((THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x)"
show " continuous_on UNIV (λx. Blinfun ((THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x))"
apply(clarsimp simp add: continuous_on_topological[of UNIV "(λx. Blinfun ((THE f'. ∀x. ((λx. 0) has_derivative f' x) (at x)) x))"])
apply(rule exI[where x = UNIV])
qed

lemma frechet_linear:
assumes good_interp:"is_interp I"
fixes v θ
shows " dfree θ ⟹ bounded_linear (frechet I θ v)"
proof(induction rule: dfree.induct)
case (dfree_Var i)
then show ?case by(auto)
next
case (dfree_Const r)
then show ?case by auto
next
case (dfree_Fun args i)
have blin1:"⋀x. bounded_linear(FunctionFrechet I i x)"
using good_interp unfolding is_interp_def using has_derivative_bounded_linear
by blast
have blin2:"bounded_linear (λ a. (χ i. frechet I (args i) v a))"
using dfree_Fun.IH by(rule bounded_linear_vec)
then show ?case
using bounded_linear_compose[of "FunctionFrechet I i (χ i. sterm_sem I (args i) v)" "(λa. (χ i. frechet I (args i) v a))", OF blin1 blin2]
by auto
next
case (dfree_Plus θ⇩1 θ⇩2)
then show ?case
apply auto
next
case (dfree_Times θ⇩1 θ⇩2)
then show ?case
qed

setup_lifting type_definition_good_interp

setup_lifting type_definition_strm

lift_definition blin_frechet::"('sf, 'sc, 'sz) good_interp ⇒ ('sf,'sz) strm ⇒ (real, 'sz) vec  ⇒ (real, 'sz) vec ⇒⇩L real" is "frechet"
using frechet_linear by auto

lemmas [simp] = blin_frechet.rep_eq

lemma frechet_blin:"is_interp I ⟹ dfree θ ⟹ (λv. Blinfun (λv'. frechet I θ v v')) = blin_frechet (good_interp I) (simple_term θ)"
apply(rule ext)
apply(rule blinfun_eqI)
by (simp add: bounded_linear_Blinfun_apply frechet_linear good_interp_inverse simple_term_inverse)

lemma sterm_continuous:
assumes good_interp:"is_interp I"
shows "dfree θ ⟹ continuous_on UNIV (sterm_sem I θ)"
proof(induction rule: dfree.induct)
case (dfree_Fun args i)
assume IH:"⋀i. continuous_on UNIV (sterm_sem I (args i))"
have con1:"continuous_on UNIV (Functions I i)"
using good_interp unfolding is_interp_def
using continuous_on_eq_continuous_within has_derivative_continuous by blast
have con2:"continuous_on UNIV (λ x. (χ i. sterm_sem I (args i) x))"
apply(rule continuous_on_vec_lambda)
using IH by auto
have con:"continuous_on UNIV ((Functions I i) ∘ (λx.  (χ i. sterm_sem I (args i) x)))"
apply(rule continuous_on_compose)
using con1 con2 apply auto
using continuous_on_subset by blast
show ?case
using con comp_def by(simp)
qed (auto intro: continuous_intros)

lemma sterm_continuous':
assumes good_interp:"is_interp I"
shows "dfree θ ⟹ continuous_on S (sterm_sem I θ)"
using sterm_continuous continuous_on_subset good_interp by blast

lemma frechet_continuous:
fixes I :: "('sf, 'sc, 'sz) interp"
assumes good_interp:"is_interp I"
shows "dfree θ ⟹ continuous_on UNIV (blin_frechet (good_interp I) (simple_term θ))"
proof (induction rule: dfree.induct)
case (dfree_Var i)
have free:"dfree (Var i)" by (rule dfree_Var)
have bounded_linear:"bounded_linear (λ ν'. ν' ∙ axis i 1)"
have cont:"continuous_on UNIV (λν. Blinfun(λ ν'. ν' ∙ axis i 1))"
using continuous_on_const by blast
have eq:"⋀ν ν'. (λν. Blinfun(λ ν'. ν' ∙ axis i 1)) ν ν' = (blin_frechet (good_interp I) (simple_term (Var i))) ν ν'"
unfolding axis_def apply(auto)
by (metis (no_types) axis_def blinfun_inner_left.abs_eq blinfun_inner_left.rep_eq dfree_Var_simps frechet.simps(1) mem_Collect_eq simple_term_inverse)
have eq':"(λν. Blinfun(λ ν'. ν' ∙ axis i 1)) = (blin_frechet (good_interp I) (simple_term (Var i)))"
apply(rule ext)
apply(rule blinfun_eqI)
using eq by auto
then show ?case by (metis cont)
next
case (dfree_Const r)
have free:"dfree (Const r)" by (rule dfree_Const)
have bounded_linear:"bounded_linear (λ ν'. 0)" by (simp)
have cont:"continuous_on UNIV (λν. Blinfun(λ ν'. 0))"
using continuous_on_const by blast
have eq':"(λν. Blinfun(λ ν'. 0)) = (blin_frechet (good_interp I) (simple_term (Const r)))"
apply(rule ext)
apply(rule blinfun_eqI)
apply auto
using zero_blinfun.abs_eq zero_blinfun.rep_eq free
by (metis frechet.simps(5) mem_Collect_eq simple_term_inverse)
then show ?case by (metis cont)
next
case (dfree_Fun args f)
assume IH:"⋀i. continuous_on UNIV (blin_frechet (good_interp I) (simple_term (args i)))"
assume frees:"(⋀i. dfree (args i))"
then have free:"dfree ($f f args)" by (auto) have great_interp:"⋀f. continuous_on UNIV (λx. Blinfun (FunctionFrechet I f x))" using good_interp unfolding is_interp_def by auto have cont1:"⋀v. continuous_on UNIV (λv'. (χ i. frechet I (args i) v v'))" apply(rule continuous_on_vec_lambda) using IH by (simp add: frechet_linear frees good_interp linear_continuous_on) have eq:"(λv. Blinfun(λv'. FunctionFrechet I f (χ i. sterm_sem I (args i) v) (χ i. frechet I (args i) v v'))) = (blin_frechet (good_interp I) (simple_term (Function f args)))" using frechet_blin[OF good_interp free] by auto have bounded_linears:"⋀x. bounded_linear (FunctionFrechet I f x)" using good_interp unfolding is_interp_def by blast let ?blin_ff ="(λx. Blinfun (FunctionFrechet I f x))" have some_eq:"(λx. Blinfun (FunctionFrechet I f (χ i. sterm_sem I (args i) x))) = ((?blin_ff) ∘ (λx. (χ i. sterm_sem I (args i) x)))" apply(rule ext) apply(rule blinfun_eqI) unfolding comp_def by blast have sub_cont:"continuous_on UNIV ((?blin_ff) ∘ (λx. (χ i. sterm_sem I (args i) x)))" apply(rule continuous_intros)+ apply (simp add: frees good_interp sterm_continuous') using continuous_on_subset great_interp by blast have blin_frech_vec:"⋀x. bounded_linear (λv'. χ i. frechet I (args i) x v')" by (simp add: bounded_linear_vec frechet_linear frees good_interp) have frech_vec_eq:"(λx. Blinfun (λv'. χ i. frechet I (args i) x v')) = (λx. blinfun_vec (λ i. blin_frechet (good_interp I) (simple_term (args i)) x))" apply(rule ext) apply(rule blinfun_eqI) apply(rule vec_extensionality) subgoal for x i j using blin_frech_vec[of x] apply auto by (metis (no_types, lifting) blin_frechet.rep_eq bounded_linear_Blinfun_apply frechet_blin frechet_linear frees good_interp vec_lambda_beta) done have cont_frech_vec:"continuous_on UNIV (λx. blinfun_vec (λ i. blin_frechet (good_interp I) (simple_term (args i)) x))" apply(rule continuous_blinfun_vec') using IH by blast have cont_intro:"⋀ s f g. 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 (λv. blinfun_compose (Blinfun (FunctionFrechet I f (χ i. sterm_sem I (args i) v))) (Blinfun(λv'. (χ i. frechet I (args i) v v'))))" apply(rule cont_intro) subgoal using sub_cont by simp using frech_vec_eq cont_frech_vec by presburger have best_eq:"(blin_frechet (good_interp I) (simple_term ($f f args))) = (λv. blinfun_compose (Blinfun (FunctionFrechet I f (χ i. sterm_sem I (args i) v))) (Blinfun(λv'.  (χ i. frechet I (args i) v v')))) "
apply(rule ext)
apply(rule blinfun_eqI)
proof -
fix v :: "(real, 'sz) vec" and i :: "(real, 'sz) vec"
have "frechet I ($f f args) v i = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i"
by (metis (no_types) bounded_linear_Blinfun_apply dfree_Fun_simps frechet_blin frechet_linear frees good_interp)
then have "FunctionFrechet I f (χ s. sterm_sem I (args s) v) (blinfun_apply (Blinfun (λva. χ s. frechet I (args s) v va)) i) = blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i" by (simp add: blin_frech_vec bounded_linear_Blinfun_apply) then show "blinfun_apply (blin_frechet (good_interp I) (simple_term ($f f args)) v) i = blinfun_apply (Blinfun (FunctionFrechet I f (χ s. sterm_sem I (args s) v)) o⇩L Blinfun (λva. χ s. frechet I (args s) v va)) i"
by (metis (no_types) blinfun_apply_blinfun_compose bounded_linear_Blinfun_apply bounded_linears)
qed
then show ?case using cont best_eq by auto
next
case (dfree_Plus θ⇩1 θ⇩2)
assume IH1:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term θ⇩1))"
assume IH2:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term θ⇩2))"
assume free1:"dfree θ⇩1"
assume free2:"dfree θ⇩2"
have free:"dfree (Plus θ⇩1 θ⇩2)" using free1 free2 by auto
have bounded_linear:"⋀v. bounded_linear (λv'. frechet I θ⇩1 v v' + frechet I θ⇩2 v v')"
subgoal for v
using frechet_linear[OF good_interp free] by auto
done
have eq2:"(λv. blin_frechet (good_interp I) (simple_term θ⇩1) v + blin_frechet (good_interp I) (simple_term θ⇩2) v) = blin_frechet (good_interp I) (simple_term (Plus θ⇩1 θ⇩2))"
apply(rule ext)
apply(rule blinfun_eqI)
have cont:"continuous_on UNIV (λv. blin_frechet (good_interp I) (simple_term θ⇩1) v + blin_frechet (good_interp I) (simple_term θ⇩2) v)"
using continuous_on_add dfree_Plus.IH(1) dfree_Plus.IH(2) by blast
then show ?case using cont eq2 by metis
next
case (dfree_Times θ⇩1 θ⇩2)
assume IH1:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term θ⇩1))"
assume IH2:"continuous_on UNIV (blin_frechet (good_interp I) (simple_term θ⇩2))"
assume free1:"dfree θ⇩1"
assume free2:"dfree θ⇩2"
have free:"dfree (Times θ⇩1 θ⇩2)" using free1 free2 by auto
have bounded_linear:"⋀v. bounded_linear (λv'. sterm_sem I θ⇩1 v * frechet I θ⇩2 v v' + frechet I θ⇩1 v v' * sterm_sem I θ⇩2 v)"
apply(rule bounded_linear_const_mult)
using frechet_linear[OF good_interp free2] apply auto
apply(rule bounded_linear_mult_const)
using frechet_linear[OF good_interp free1] by auto
then have blin':"⋀v. (λv'. sterm_sem I θ⇩1 v * frechet I θ⇩2 v v' + frechet I θ⇩1 v v' * sterm_sem I θ⇩2 v) ∈ {f. bounded_linear f}" by auto
have blinfun_eq:"⋀v. Blinfun (λv'. sterm_sem I θ⇩1 v * frechet I θ⇩2 v v' + frechet I θ⇩1 v v' * sterm_sem I θ⇩2 v)
=  scaleR (sterm_sem I θ⇩1 v) (blin_frechet (good_interp I) (simple_term θ⇩2) v) + scaleR (sterm_sem I θ⇩2 v) (blin_frechet (good_interp I) (simple_term θ⇩1) v)"
apply(rule blinfun_eqI)
subgoal for v i
using Blinfun_inverse[OF blin', of v] apply auto
using blinfun.add_left[of "sterm_sem I θ⇩1 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩2) v" "sterm_sem I θ⇩2 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩1) v"]
blinfun.scaleR_left[of "sterm_sem I θ⇩1 v" "blin_frechet (good_interp I) (simple_term θ⇩2) v"]
blinfun.scaleR_left[of "sterm_sem I θ⇩2 v" "blin_frechet (good_interp I) (simple_term θ⇩1) v"]
bounded_linear_Blinfun_apply
frechet_blin[OF good_interp free1]
frechet_blin[OF good_interp free2]
frechet_linear[OF good_interp free1]
frechet_linear[OF good_interp free2]
mult.commute
real_scaleR_def
proof -
have f1: "⋀v. blinfun_apply (blin_frechet (good_interp I) (simple_term θ⇩1) v) = frechet I θ⇩1 v"
by (metis (no_types) ‹(λv. Blinfun (frechet I θ⇩1 v)) = blin_frechet (good_interp I) (simple_term θ⇩1)› ‹⋀v. bounded_linear (frechet I θ⇩1 v)› bounded_linear_Blinfun_apply)
have "⋀v. blinfun_apply (blin_frechet (good_interp I) (simple_term θ⇩2) v) = frechet I θ⇩2 v"
by (metis (no_types) ‹(λv. Blinfun (frechet I θ⇩2 v)) = blin_frechet (good_interp I) (simple_term θ⇩2)› ‹⋀v. bounded_linear (frechet I θ⇩2 v)› bounded_linear_Blinfun_apply)
then show "sterm_sem I θ⇩1 v * frechet I θ⇩2 v i + frechet I θ⇩1 v i * sterm_sem I θ⇩2 v = blinfun_apply (sterm_sem I θ⇩1 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩2) v + sterm_sem I θ⇩2 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩1) v) i"
using f1 by (simp add: ‹⋀b. blinfun_apply (sterm_sem I θ⇩1 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩2) v + sterm_sem I θ⇩2 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩1) v) b = blinfun_apply (sterm_sem I θ⇩1 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩2) v) b + blinfun_apply (sterm_sem I θ⇩2 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩1) v) b› ‹⋀b. blinfun_apply (sterm_sem I θ⇩1 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩2) v) b = sterm_sem I θ⇩1 v *⇩R blinfun_apply (blin_frechet (good_interp I) (simple_term θ⇩2) v) b› ‹⋀b. blinfun_apply (sterm_sem I θ⇩2 v *⇩R blin_frechet (good_interp I) (simple_term θ⇩1) v) b = sterm_sem I θ⇩2 v *⇩R blinfun_apply (blin_frechet (good_interp I) (simple_term θ⇩1) v) b›)
qed
done
have cont':"continuous_on UNIV
(λv. scaleR (sterm_sem I θ⇩1 v) (blin_frechet (good_interp I) (simple_term θ⇩2) v)
+ scaleR (sterm_sem I θ⇩2 v) (blin_frechet (good_interp I) (simple_term θ⇩1) v))"
apply(rule continuous_on_scaleR)
apply(rule sterm_continuous[OF good_interp free1])
apply(rule IH2)
apply(rule continuous_on_scaleR)
apply(rule sterm_continuous[OF good_interp free2])
by(rule IH1)
have cont:"continuous_on UNIV (λv. Blinfun (λv'. sterm_sem I θ⇩1 v * frechet I θ⇩2 v v' + frechet I θ⇩1 v v' * sterm_sem I θ⇩2 v))"
using cont' blinfun_eq by auto
have eq:"(λv. Blinfun (λv'. sterm_sem I θ⇩1 v * frechet I θ⇩2 v v' + frechet I θ⇩1 v v' * sterm_sem I θ⇩2 v)) = blin_frechet (good_interp I) (simple_term (Times θ⇩1 θ⇩2))"
using frechet_blin[OF good_interp free]
by auto
then show ?case by (metis cont)
qed
end end



# Theory Static_Semantics

theory "Static_Semantics"
imports
Ordinary_Differential_Equations.ODE_Analysis
"Ids"
"Lib"
"Syntax"
"Denotational_Semantics"
"Frechet_Correctness"
begin
section ‹Static Semantics›
text ‹This section introduces functions for computing properties of the static semantics, specifically
the following dependencies:
\begin{itemize}
\item Signatures: Symbols (from the interpretation) which influence the result of a term, ode, formula, program
\item Free variables: Variables (from the state) which influence the result of a term, ode, formula, program
\item Bound variables: Variables (from the state) that *might* be influenced by a program
\item Must-bound variables: Variables (from the state) that are *always* influenced by a program (i.e.
will never depend on anything other than the free variables of that program)
\end{itemize}

We also prove basic lemmas about these definitions, but their overall correctness is proved elsewhere
in the Bound Effect and Coincidence theorems.
›

subsection ‹Signature Definitions›
primrec SIGT :: "('a, 'c) trm ⇒ 'a set"
where
"SIGT (Var var) = {}"
| "SIGT (Const r) = {}"
| "SIGT (Function var f) = {var} ∪ (⋃i. SIGT (f i))"
| "SIGT (Plus t1 t2) = SIGT t1 ∪ SIGT t2"
| "SIGT (Times t1 t2) = SIGT t1 ∪ SIGT t2"
| "SIGT (DiffVar x) = {}"
| "SIGT (Differential t) = SIGT t"

primrec SIGO   :: "('a, 'c) ODE ⇒ ('a + 'c) set"
where
"SIGO (OVar c) = {Inr c}"
| "SIGO (OSing x θ) =  {Inl x| x. x ∈ SIGT θ}"
| "SIGO (OProd ODE1 ODE2) = SIGO ODE1 ∪ SIGO ODE2"

primrec SIGP   :: "('a, 'b, 'c) hp      ⇒ ('a + 'b + 'c) set"
and     SIGF   :: "('a, 'b, 'c) formula ⇒ ('a + 'b + 'c) set"
where
"SIGP (Pvar var) = {Inr (Inr var)}"
| "SIGP (Assign var t) = {Inl x | x. x ∈ SIGT t}"
| "SIGP (DiffAssign var t) = {Inl x | x. x ∈ SIGT t}"
| "SIGP (Test p) = SIGF p"
| "SIGP (EvolveODE ODE p) = SIGF p ∪ {Inl x | x. Inl x ∈ SIGO ODE} ∪ {Inr (Inr x) | x. Inr x ∈ SIGO ODE}"
| "SIGP (Choice a b) = SIGP a ∪ SIGP b"
| "SIGP (Sequence a b) = SIGP a ∪ SIGP b"
| "SIGP (Loop a) = SIGP a"
| "SIGF (Geq t1 t2) = {Inl x | x. x ∈ SIGT t1 ∪ SIGT t2}"
| "SIGF (Prop var args) = {Inr (Inr var)} ∪ {Inl x | x. x ∈ (⋃i. SIGT (args i))}"
| "SIGF (Not p) = SIGF p"
| "SIGF (And p1 p2) = SIGF p1 ∪ SIGF p2"
| "SIGF (Exists var p) = SIGF p"
| "SIGF (Diamond a p) = SIGP a ∪ SIGF p"
| "SIGF (InContext var p) = {Inr (Inl var)} ∪ SIGF p"

fun primify :: "('a + 'a) ⇒ ('a + 'a) set"
where
"primify (Inl x) = {Inl x, Inr x}"
| "primify (Inr x) = {Inl x, Inr x}"

subsection ‹Variable Binding Definitions›
text‹
We represent the (free or bound or must-bound) variables of a term as an (id + id) set,
where all the (Inl x) elements are unprimed variables x and all the (Inr x) elements are
primed variables x'.
›
text‹Free variables of a term ›
primrec FVT :: "('a, 'c) trm ⇒ ('c + 'c) set"
where
"FVT (Var x) = {Inl x}"
| "FVT (Const x) = {}"
| "FVT (Function f args) = (⋃i. FVT (args i))"
| "FVT (Plus f g) = FVT f ∪ FVT g"
| "FVT (Times f g) = FVT f ∪ FVT g"
| "FVT (Differential f) = (⋃x ∈ (FVT f). primify x)"
| "FVT (DiffVar x) = {Inr x}"

fun FVDiff :: "('a, 'c) trm ⇒ ('c + 'c) set"
where "FVDiff f = (⋃x ∈ (FVT f). primify x)"

text‹ Free variables of an ODE includes both the bound variables and the terms ›
fun FVO :: "('a, 'c) ODE ⇒ 'c set"
where
"FVO (OVar c) = UNIV"
| "FVO (OSing x θ) = {x} ∪ {x . Inl x ∈ FVT θ}"
| "FVO (OProd ODE1 ODE2) = FVO ODE1 ∪ FVO ODE2"

text‹ Bound variables of ODEs, formulas, programs ›
fun BVO :: "('a, 'c) ODE ⇒ ('c + 'c) set"
where
"BVO (OVar c) = UNIV"
| "BVO (OSing x θ) = {Inl x, Inr x}"
| "BVO (OProd ODE1 ODE2) = BVO ODE1 ∪ BVO ODE2"

fun BVF :: "('a, 'b, 'c) formula ⇒ ('c + 'c) set"
and BVP :: "('a, 'b, 'c) hp ⇒ ('c + 'c) set"
where
"BVF (Geq f g) = {}"
| "BVF (Prop p dfun_args) = {}"
| "BVF (Not p) = BVF p"
| "BVF (And p q) = BVF p ∪ BVF q"
| "BVF (Exists x p) = {Inl x} ∪ BVF p"
| "BVF (Diamond α p) = BVP α ∪ BVF p"
| "BVF (InContext C p) = UNIV"

| "BVP (Pvar a) = UNIV"
| "BVP (Assign x θ) = {Inl x}"
| "BVP (DiffAssign x θ) = {Inr x}"
| "BVP (Test φ) = {}"
| "BVP (EvolveODE ODE φ) = BVO ODE"
| "BVP (Choice α β) = BVP α ∪ BVP β"
| "BVP (Sequence α β) = BVP α ∪ BVP β"
| "BVP (Loop α) = BVP α"

text‹ Must-bound variables (of a program)›
fun MBV :: "('a, 'b, 'c) hp ⇒ ('c + 'c) set"
where
"MBV (Pvar a) = {}"
| "MBV (Choice α β) = MBV α ∩ MBV β"
| "MBV (Sequence α β) = MBV α ∪ MBV β"
| "MBV (Loop α) = {}"
| "MBV (EvolveODE ODE _) = (Inl  (ODE_dom ODE)) ∪ (Inr  (ODE_dom ODE))"
| "MBV α = BVP α"

text‹Free variables of a formula,
free variables of a program ›
fun FVF :: "('a, 'b, 'c) formula ⇒ ('c + 'c) set"
and FVP :: "('a, 'b, 'c) hp ⇒ ('c + 'c) set"
where
"FVF (Geq f g) = FVT f ∪ FVT g"
| "FVF (Prop p args) = (⋃i. FVT (args i))"
| "FVF (Not p) = FVF p"
| "FVF (And p q) = FVF p ∪ FVF q"
| "FVF (Exists x p) = FVF p - {Inl x}"
| "FVF (Diamond α p) =   FVP α ∪ (FVF p - MBV α)"
| "FVF (InContext C p) = UNIV"
| "FVP (Pvar a) = UNIV"
| "FVP (Assign x θ) = FVT θ"
| "FVP (DiffAssign x θ) = FVT θ"
| "FVP (Test φ) = FVF φ"
| "FVP (EvolveODE ODE φ) = BVO ODE ∪ (Inl  FVO ODE) ∪ FVF φ"
| "FVP (Choice α β) = FVP α ∪ FVP β"
| "FVP (Sequence α β) = FVP α ∪ (FVP β - MBV α)"
| "FVP (Loop α) = FVP α"

subsection ‹Lemmas for reasoning about static semantics›

lemma primify_contains:"x ∈ primify x"
by (cases "x") auto

lemma FVDiff_sub:"FVT f ⊆ FVDiff f"

lemma fvdiff_plus1:"FVDiff (Plus t1 t2) = FVDiff t1 ∪ FVDiff t2"
by (auto)

lemma agree_func_fvt:"Vagree ν ν' (FVT (Function f args)) ⟹ Vagree ν ν' (FVT (args i))"
by (auto simp add: Set.Un_upper1 agree_supset Vagree_def)

lemma agree_plus1:"Vagree ν ν' (FVDiff (Plus t1 t2)) ⟹ Vagree ν ν' (FVDiff t1)"
proof -
assume agree:"Vagree ν ν' (FVDiff (Plus t1 t2))"
have agree':"Vagree ν ν' ((⋃i∈FVT t1. primify i) ∪ (⋃i∈FVT t2. primify i))"
using fvdiff_plus1 FVDiff.simps agree by (auto)
have agreeL:"Vagree ν ν' ((⋃i∈FVT t1. primify i))"
using agree' agree_supset Set.Un_upper1 by (blast)
show "Vagree ν ν' (FVDiff t1)" using agreeL by (auto)
qed

lemma agree_plus2:"Vagree ν ν' (FVDiff (Plus t1 t2)) ⟹ Vagree ν ν' (FVDiff t2)"
proof -
assume agree:"Vagree ν ν' (FVDiff (Plus t1 t2))"
have agree':"Vagree ν ν' ((⋃i∈FVT t1. primify i) ∪ (⋃i∈FVT t2. primify i))"
using fvdiff_plus1 FVDiff.simps agree by (auto)
have agreeR:"Vagree ν ν' ((⋃i∈FVT t2. primify i))"
using agree' agree_supset Set.Un_upper1 by (blast)
show "Vagree ν ν' (FVDiff t2)" using agreeR by (auto)
qed

lemma agree_times1:"Vagree ν ν' (FVDiff (Times t1 t2)) ⟹ Vagree ν ν' (FVDiff t1)"
proof -
assume agree:"Vagree ν ν' (FVDiff (Times t1 t2))"
have agree':"Vagree ν ν' ((⋃i∈FVT t1. primify i) ∪ (⋃i∈FVT t2. primify i))"
using fvdiff_plus1 FVDiff.simps agree by (auto)
have agreeL:"Vagree ν ν' ((⋃i∈FVT t1. primify i))"
using agree' agree_supset Set.Un_upper1 by (blast)
show "Vagree ν ν' (FVDiff t1)" using agreeL by (auto)
qed

lemma agree_times2:"Vagree ν ν' (FVDiff (Times t1 t2)) ⟹ Vagree ν ν' (FVDiff t2)"
proof -
assume agree:"Vagree ν ν' (FVDiff (Times t1 t2))"
have agree':"Vagree ν ν' ((⋃i∈FVT t1. primify i) ∪ (⋃i∈FVT t2. primify i))"
using fvdiff_plus1 FVDiff.simps agree by (auto)
have agreeR:"Vagree ν ν' ((⋃i∈FVT t2. primify i))"
using agree' agree_supset Set.Un_upper1 by (blast)
show "Vagree ν ν' (FVDiff t2)" using agreeR by (auto)
qed

lemma agree_func:"Vagree ν ν' (FVDiff ($f var args)) ⟹ (⋀i. Vagree ν ν' (FVDiff (args i)))" proof - assume agree:"Vagree ν ν' (FVDiff ($f var args))"
have agree':"Vagree ν ν' ((⋃i. (⋃j ∈(FVT (args i)). primify j)))"
using fvdiff_plus1 FVDiff.simps agree by (auto)
fix i :: 'a
have "⋀S. ¬ S ⊆ (⋃f. ⋃ (primify  FVT (args f))) ∨ Vagree ν ν' S"
using agree' agree_supset by blast
then have "⋀f. f ∉ UNIV ∨ Vagree ν ν' (⋃ (primify  FVT (args f)))"
by blast
then show "Vagree ν ν' (FVDiff (args i))"
by simp
qed

end


# Theory Coincidence

theory "Coincidence"
imports
Ordinary_Differential_Equations.ODE_Analysis
"Ids"
"Lib"
"Syntax"
"Denotational_Semantics"
"Frechet_Correctness"
"Static_Semantics"
begin
section ‹Coincidence Theorems and Corollaries›
text ‹This section proves coincidence: semantics of terms, odes, formulas and programs depend only
on the free variables. This is one of the major lemmas for the correctness of uniform substitutions.
Along the way, we also prove the equivalence between two similar, but different semantics for ODE programs:
It does not matter whether the semantics of ODE's insist on the existence of a solution that agrees
with the start state on all variables vs. one that agrees only on the variables that are actually
relevant to the ODE. This is proven here by simultaneous induction with the coincidence theorem
for the following reason:

The reason for having two different semantics is that some proofs are easier with one semantics
and other proofs are easier with the other definition. The coincidence proof is either with the
more complicated definition, which should not be used as the main definition because it would make
the specification for the dL semantics significantly larger, effectively increasing the size of
the trusted core. However, that the proof of equivalence between the semantics using the coincidence
lemma for formulas. In order to use the coincidence proof in the equivalence proof and the equivalence
proof in the coincidence proof, they are proved by simultaneous induction.
›

context ids begin
subsection ‹Term Coincidence Theorems›
lemma coincidence_sterm:"Vagree ν ν' (FVT θ) ⟹ sterm_sem I  θ (fst ν) = sterm_sem I θ (fst ν')"
apply(induct "θ") (* 7 subgoals *)
by (meson rangeI)

lemma coincidence_sterm':"dfree θ ⟹  Vagree ν ν' (FVT θ) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ} ⟹ sterm_sem I  θ (fst ν) = sterm_sem J θ (fst ν')"
proof (induction rule: dfree.induct)
case (dfree_Fun args i)
then show ?case
proof (auto)
assume free:"(⋀i. dfree (args i))"
and IH:"(⋀i. Vagree ν ν' (FVT (args i)) ⟹ Iagree I J {Inl x |x. x ∈ SIGT (args i)} ⟹ sterm_sem I (args i) (fst ν) = sterm_sem J (args i) (fst ν'))"
and VA:"Vagree ν ν' (⋃i. FVT (args i))"
and IA:"Iagree I J {Inl x |x. x = i ∨ (∃xa. x ∈ SIGT (args xa))}"
from IA have IAorig:"Iagree I J {Inl x |x. x ∈ SIGT (Function i args)}" by auto
from Iagree_Func[OF IAorig] have eqF:"Functions I i = Functions J i" by auto
have Vsubs:"⋀i. FVT (args i) ⊆ (⋃i. FVT (args i))" by auto
from VA
have VAs:"⋀i. Vagree ν ν' (FVT (args i))"
using agree_sub[OF Vsubs] by auto
have Isubs:"⋀j. {Inl x |x. x ∈ SIGT (args j)} ⊆ {Inl x |x. x ∈ SIGT (Function i args)}"
by auto
from IA
have IAs:"⋀i. Iagree I J {Inl x |x. x ∈ SIGT (args i)}"
using Iagree_sub[OF Isubs] by auto
show "Functions I i (χ i. sterm_sem I (args i) (fst ν)) = Functions J i (χ i. sterm_sem J (args i) (fst ν'))"
using IH[OF VAs IAs] eqF by auto
qed
next
case (dfree_Plus θ⇩1 θ⇩2)
then show ?case
proof (auto)
assume "dfree θ⇩1" "dfree θ⇩2"
and IH1:"(Vagree ν ν' (FVT θ⇩1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩1} ⟹ sterm_sem I θ⇩1 (fst ν) = sterm_sem J θ⇩1 (fst ν'))"
and IH2:"(Vagree ν ν' (FVT θ⇩2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩2} ⟹ sterm_sem I θ⇩2 (fst ν) = sterm_sem J θ⇩2 (fst ν'))"
and VA:"Vagree ν ν' (FVT θ⇩1 ∪ FVT θ⇩2)"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1 ∨ x ∈ SIGT θ⇩2}"
from VA
have VAs:"Vagree ν ν' (FVT θ⇩1)" "Vagree ν ν' (FVT θ⇩2)"
unfolding Vagree_def by auto
have Isubs:"{Inl x |x. x ∈ SIGT θ⇩1} ⊆ {Inl x |x. x ∈ SIGT (Plus θ⇩1 θ⇩2)}"
"{Inl x |x. x ∈ SIGT θ⇩2} ⊆ {Inl x |x. x ∈ SIGT (Plus θ⇩1 θ⇩2)}"
by auto
from IA
have IAs:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1}"
"Iagree I J {Inl x |x. x ∈ SIGT θ⇩2}"
using Iagree_sub[OF Isubs(1)] Iagree_sub[OF Isubs(2)] by auto
show "sterm_sem I θ⇩1 (fst ν) + sterm_sem I θ⇩2 (fst ν) = sterm_sem J θ⇩1 (fst ν') + sterm_sem J θ⇩2 (fst ν')"
using IH1[OF VAs(1) IAs(1)] IH2[OF VAs(2) IAs(2)] by auto
qed
next
case (dfree_Times θ⇩1 θ⇩2)
then show ?case
proof (auto)
assume "dfree θ⇩1" "dfree θ⇩2"
and IH1:"(Vagree ν ν' (FVT θ⇩1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩1} ⟹ sterm_sem I θ⇩1 (fst ν) = sterm_sem J θ⇩1 (fst ν'))"
and IH2:"(Vagree ν ν' (FVT θ⇩2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩2} ⟹ sterm_sem I θ⇩2 (fst ν) = sterm_sem J θ⇩2 (fst ν'))"
and VA:"Vagree ν ν' (FVT θ⇩1 ∪ FVT θ⇩2)"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1 ∨ x ∈ SIGT θ⇩2}"
from VA
have VAs:"Vagree ν ν' (FVT θ⇩1)" "Vagree ν ν' (FVT θ⇩2)"
unfolding Vagree_def by auto
have Isubs:"{Inl x |x. x ∈ SIGT θ⇩1} ⊆ {Inl x |x. x ∈ SIGT (Times θ⇩1 θ⇩2)}"
"{Inl x |x. x ∈ SIGT θ⇩2} ⊆ {Inl x |x. x ∈ SIGT (Times θ⇩1 θ⇩2)}"
by auto
from IA
have IAs:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1}"
"Iagree I J {Inl x |x. x ∈ SIGT θ⇩2}"
using Iagree_sub[OF Isubs(1)] Iagree_sub[OF Isubs(2)] by auto
show "sterm_sem I θ⇩1 (fst ν) * sterm_sem I θ⇩2 (fst ν) = sterm_sem J θ⇩1 (fst ν') * sterm_sem J θ⇩2 (fst ν')"
using IH1[OF VAs(1) IAs(1)] IH2[OF VAs(2) IAs(2)] by auto
qed
qed (unfold Vagree_def Iagree_def, auto)

lemma sum_unique_nonzero:
fixes i::"'sv::finite" and f::"'sv ⇒ real"
assumes restZero:"⋀j. j∈(UNIV::'sv set) ⟹ j ≠ i ⟹ f j = 0"
shows "(∑j∈(UNIV::'sv set). f j) = f i"
proof -
have "(∑j∈(UNIV::'sv set). f j) = (∑j∈{i}. f j)"
using restZero by (intro sum.mono_neutral_cong_right) auto
then show ?thesis
by simp
qed

lemma  coincidence_frechet :
fixes I :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c state" and ν'::"'c state"
shows "dfree θ ⟹ Vagree ν ν' (FVDiff θ) ⟹ frechet I  θ (fst ν) (snd ν) = frechet I  θ (fst ν') (snd ν')"
proof (induction rule: dfree.induct)
case dfree_Var then show ?case
by (auto simp: inner_prod_eq Vagree_def)
next
case dfree_Const then show ?case
by auto
next
case (dfree_Fun args var)
assume free:"(⋀i. dfree (args i))"
assume IH:"(⋀i. Vagree ν ν' (FVDiff (args i)) ⟹ frechet I (args i) (fst ν) (snd ν) = frechet I (args i) (fst ν') (snd ν'))"
have frees:"(⋀i. dfree (args i))" using free by (auto simp add: rangeI)
assume agree:"Vagree ν ν' (FVDiff ($f var args))" have agrees:"⋀i. Vagree ν ν' (FVDiff (args i))" using agree agree_func by metis have agrees':"⋀i. Vagree ν ν' (FVT (args i))" subgoal for i using agrees[of i] FVDiff_sub[of "args i"] unfolding Vagree_def by blast done have sterms:"⋀i. sterm_sem I (args i) (fst ν) = sterm_sem I (args i) (fst ν')" by (rule coincidence_sterm[of "ν" "ν'", OF agrees']) have frechets:"⋀i. frechet I (args i) (fst ν) (snd ν) = frechet I (args i) (fst ν') (snd ν')" using IH agrees frees rangeI by blast show "?case" using agrees sterms frechets by (auto) next case (dfree_Plus t1 t2) assume dfree1:"dfree t1" assume IH1:"(Vagree ν ν' (FVDiff t1) ⟹ frechet I t1 (fst ν) (snd ν) = frechet I t1 (fst ν') (snd ν'))" assume dfree2:"dfree t2" assume IH2:"(Vagree ν ν' (FVDiff t2) ⟹ frechet I t2 (fst ν) (snd ν) = frechet I t2 (fst ν') (snd ν'))" assume agree:"Vagree ν ν' (FVDiff (Plus t1 t2))" have agree1:"Vagree ν ν' (FVDiff t1)" using agree agree_plus1 by (blast) have agree2:"Vagree ν ν' (FVDiff t2)" using agree agree_plus2 by (blast) have IH1':"(frechet I t1 (fst ν) (snd ν) = frechet I t1 (fst ν') (snd ν'))" using IH1 agree1 by (auto) have IH2':"(frechet I t2 (fst ν) (snd ν) = frechet I t2 (fst ν') (snd ν'))" using IH2 agree2 by (auto) show "?case" by (metis FVT.simps(4) IH1' IH2' UnCI Vagree_def coincidence_sterm frechet.simps(3) mem_Collect_eq) next case (dfree_Times t1 t2) assume dfree1:"dfree t1" assume IH1:"(Vagree ν ν' (FVDiff t1) ⟹ frechet I t1 (fst ν) (snd ν) = frechet I t1 (fst ν') (snd ν'))" assume dfree2:"dfree t2" assume IH2:"(Vagree ν ν' (FVDiff t2) ⟹ frechet I t2 (fst ν) (snd ν) = frechet I t2 (fst ν') (snd ν'))" assume agree:"Vagree ν ν' (FVDiff (Times t1 t2))" have agree1:"Vagree ν ν' (FVDiff t1)" using agree agree_times1 by blast have agree2:"Vagree ν ν' (FVDiff t2)" using agree agree_times2 by blast have agree1':"Vagree ν ν' (FVT t1)" using agree1 apply(auto simp add: Vagree_def) using primify_contains by blast+ have agree2':"Vagree ν ν' (FVT t2)" using agree2 apply(auto simp add: Vagree_def) using primify_contains by blast+ have IH1':"(frechet I t1 (fst ν) (snd ν) = frechet I t1 (fst ν') (snd ν'))" using IH1 agree1 by (auto) have IH2':"(frechet I t2 (fst ν) (snd ν) = frechet I t2 (fst ν') (snd ν'))" using IH2 agree2 by (auto) have almost:"Vagree ν ν' (FVT (Times t1 t2)) ⟹ frechet I (Times t1 t2) (fst ν) (snd ν) = frechet I (Times t1 t2) (fst ν') (snd ν')" by (auto simp add: UnCI Vagree_def agree IH1' IH2' coincidence_sterm[OF agree1', of I] coincidence_sterm[OF agree2', of I]) show "?case" using agree FVDiff_sub almost by (metis agree_supset) qed lemma coincidence_frechet' : fixes I J :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c state" and ν'::"'c state" shows "dfree θ ⟹ Vagree ν ν' (FVDiff θ) ⟹ Iagree I J {Inl x | x. x ∈ (SIGT θ)} ⟹ frechet I θ (fst ν) (snd ν) = frechet J θ (fst ν') (snd ν')" proof (induction rule: dfree.induct) case dfree_Var then show ?case by (auto simp: inner_prod_eq Vagree_def) next case dfree_Const then show ?case by auto next case (dfree_Fun args var) assume free:"(⋀i. dfree (args i))" assume IH:"(⋀i. Vagree ν ν' (FVDiff (args i)) ⟹ Iagree I J {Inl x |x. x ∈ SIGT (args i)} ⟹ frechet I (args i) (fst ν) (snd ν) = frechet J (args i) (fst ν') (snd ν'))" have frees:"(⋀i. dfree (args i))" using free by (auto simp add: rangeI) assume agree:"Vagree ν ν' (FVDiff ($f var args))"
assume IA:"Iagree I J {Inl x |x. x ∈ SIGT ($f var args)}" have agrees:"⋀i. Vagree ν ν' (FVDiff (args i))" using agree agree_func by metis then have agrees':"⋀i. Vagree ν ν' (FVT (args i))" using agrees FVDiff_sub by (metis agree_sub) from Iagree_Func [OF IA ]have fEq:"Functions I var = Functions J var" by auto have subs:"⋀i.{Inl x |x. x ∈ SIGT (args i)} ⊆ {Inl x |x. x ∈ SIGT ($f var args)}"
by auto
from IA have IAs:"⋀i. Iagree I J {Inl x |x. x ∈ SIGT (args i)}"
using Iagree_sub[OF subs] by auto
have sterms:"⋀i. sterm_sem I (args i) (fst ν) = sterm_sem J (args i) (fst ν')"
subgoal for i
using frees agrees' coincidence_sterm'[of "args i" ν ν' I J] IAs
by (auto)
done
have frechets:"⋀i. frechet I (args i) (fst ν) (snd ν) = frechet J (args i) (fst ν') (snd ν')"
using IH[OF agrees IAs] agrees frees rangeI by blast
show "?case"
using agrees agrees' sterms frechets fEq by auto
next
case (dfree_Plus t1 t2)
assume dfree1:"dfree t1"
assume dfree2:"dfree t2"
assume IH1:"(Vagree ν ν' (FVDiff t1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT t1} ⟹ frechet I t1 (fst ν) (snd ν) = frechet J t1 (fst ν') (snd ν'))"
assume IH2:"(Vagree ν ν' (FVDiff t2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT t2} ⟹  frechet I t2 (fst ν) (snd ν) = frechet J t2 (fst ν') (snd ν'))"
assume agree:"Vagree ν ν' (FVDiff (Plus t1 t2))"
assume IA:"Iagree I J {Inl x |x. x ∈ SIGT (Plus t1 t2)}"
have subs:"{Inl x |x. x ∈ SIGT t1} ⊆ {Inl x |x. x ∈ SIGT (Plus t1 t2)}" "{Inl x |x. x ∈ SIGT t2} ⊆ {Inl x |x. x ∈ SIGT (Plus t1 t2)}"
by auto
from IA
have IA1:"Iagree I J {Inl x |x. x ∈ SIGT t1}"
and  IA2:"Iagree I J {Inl x |x. x ∈ SIGT t2}"
using Iagree_sub[OF subs(1)] Iagree_sub[OF subs(2)] by auto
have agree1:"Vagree ν ν' (FVDiff t1)" using agree agree_plus1 by (blast)
have agree2:"Vagree ν ν' (FVDiff t2)" using agree agree_plus2 by (blast)
have agree1':"Vagree ν ν' (FVT t1)" using agree1 primify_contains by (auto simp add: Vagree_def, metis)
have agree2':"Vagree ν ν' (FVT t2)" using agree2 primify_contains by (auto simp add: Vagree_def, metis)
have IH1':"(frechet I t1 (fst ν) (snd ν) = frechet J t1 (fst ν') (snd ν'))"
using IH1 agree1 IA1 by (auto)
have IH2':"(frechet I t2 (fst ν) (snd ν) = frechet J t2 (fst ν') (snd ν'))"
using IH2 agree2 IA2 by (auto)
show "?case"
using coincidence_sterm[OF agree1'] coincidence_sterm[OF agree1'] coincidence_sterm[OF agree2']
by (auto simp add: IH1' IH2' UnCI Vagree_def)

next
case (dfree_Times t1 t2)
assume dfree1:"dfree t1"
assume dfree2:"dfree t2"
assume IH1:"(Vagree ν ν' (FVDiff t1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT t1} ⟹ frechet I t1 (fst ν) (snd ν) = frechet J t1 (fst ν') (snd ν'))"
assume IH2:"(Vagree ν ν' (FVDiff t2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT t2} ⟹  frechet I t2 (fst ν) (snd ν) = frechet J t2 (fst ν') (snd ν'))"
assume agree:"Vagree ν ν' (FVDiff (Times t1 t2))"
assume IA:"Iagree I J {Inl x |x. x ∈ SIGT (Times t1 t2)}"
have subs:"{Inl x |x. x ∈ SIGT t1} ⊆ {Inl x |x. x ∈ SIGT (Times t1 t2)}" "{Inl x |x. x ∈ SIGT t2} ⊆ {Inl x |x. x ∈ SIGT (Times t1 t2)}"
by auto
from IA
have IA1:"Iagree I J {Inl x |x. x ∈ SIGT t1}"
and  IA2:"Iagree I J {Inl x |x. x ∈ SIGT t2}"
using Iagree_sub[OF subs(1)] Iagree_sub[OF subs(2)] by auto
have agree1:"Vagree ν ν' (FVDiff t1)" using agree agree_times1 by (blast)
then have agree1':"Vagree ν ν' (FVT t1)"
using agree1 primify_contains by (auto simp add: Vagree_def, metis)
have agree2:"Vagree ν ν' (FVDiff t2)" using agree agree_times2 by (blast)
then have agree2':"Vagree ν ν' (FVT t2)"
using agree2 primify_contains by (auto simp add: Vagree_def, metis)
have IH1':"(frechet I t1 (fst ν) (snd ν) = frechet J t1 (fst ν') (snd ν'))"
using IH1 agree1 IA1 by (auto)
have IH2':"(frechet I t2 (fst ν) (snd ν) = frechet J t2 (fst ν') (snd ν'))"
using IH2 agree2 IA2 by (auto)
note co1 = coincidence_sterm'[of "t1" ν ν' I J] and co2 = coincidence_sterm'[of "t2" ν ν' I J]
show "?case"
using co1 [OF dfree1 agree1' IA1] co2 [OF dfree2 agree2' IA2] IH1' IH2' by auto
qed

lemma coincidence_dterm:
fixes I :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c state" and ν'::"'c state"
shows "dsafe θ ⟹ Vagree ν ν' (FVT θ) ⟹ dterm_sem I θ ν = dterm_sem I θ ν'"
proof (induction rule: dsafe.induct)
case (dsafe_Fun args f)
assume safe:"(⋀i. dsafe (args i))"
assume IH:"⋀i. Vagree ν ν' (FVT (args i)) ⟹ dterm_sem I (args i) ν = dterm_sem I (args i) ν'"
assume agree:"Vagree ν ν' (FVT ($f f args))" then have "⋀i. Vagree ν ν' (FVT (args i))" using agree_func_fvt by (metis) then show "?case" using safe coincidence_sterm IH rangeI by (auto) qed (auto simp: Vagree_def directional_derivative_def coincidence_frechet) lemma coincidence_dterm': fixes I J :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c::finite state" and ν'::"'c::finite state" shows "dsafe θ ⟹ Vagree ν ν' (FVT θ) ⟹ Iagree I J {Inl x | x. x ∈ (SIGT θ)} ⟹ dterm_sem I θ ν = dterm_sem J θ ν'" proof (induction rule: dsafe.induct) case (dsafe_Fun args f) then have safe:"(⋀i. dsafe (args i))" and IH:"⋀i. Vagree ν ν' (FVT (args i)) ⟹ Iagree I J {Inl x | x. x ∈ (SIGT (args i))} ⟹ dterm_sem I (args i) ν = dterm_sem J (args i) ν'" and agree:"Vagree ν ν' (FVT ($f f args))"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT ($f f args)}" by auto have subs:"⋀i. {Inl x |x. x ∈ SIGT (args i)} ⊆ {Inl x |x. x ∈ SIGT ($f f args)}" by auto
from IA have IAs:
"⋀i. Iagree I J {Inl x |x. x ∈ SIGT (args i)}"
using Iagree_sub [OF subs IA] by auto
from agree have agrees:"⋀i. Vagree ν ν' (FVT (args i))"
using agree_func_fvt by (metis)
from Iagree_Func [OF IA] have fEq:"Functions I f = Functions J f" by auto
then show "?case"
using safe coincidence_sterm IH[OF agrees IAs] rangeI agrees fEq
by (auto)
next
case (dsafe_Plus θ⇩1 θ⇩2) then
have safe:"dsafe θ⇩1" "dsafe θ⇩2"
and IH1:"Vagree ν ν' (FVT θ⇩1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩1} ⟹ dterm_sem I θ⇩1 ν = dterm_sem J θ⇩1 ν'"
and IH2:"Vagree ν ν' (FVT θ⇩2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩2} ⟹ dterm_sem I θ⇩2 ν = dterm_sem J θ⇩2 ν'"
and VA:"Vagree ν ν' (FVT (Plus θ⇩1 θ⇩2))"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT (Plus θ⇩1 θ⇩2)}"
by auto
from VA have VA1:"Vagree ν ν' (FVT θ⇩1)" and VA2:"Vagree ν ν' (FVT θ⇩2)"
unfolding Vagree_def by auto
have subs:"{Inl x |x. x ∈ SIGT θ⇩1} ⊆ {Inl x |x. x ∈ SIGT (Plus θ⇩1 θ⇩2)}"
"{Inl x |x. x ∈ SIGT θ⇩2} ⊆ {Inl x |x. x ∈ SIGT (Plus θ⇩1 θ⇩2)}"by auto
from IA have IA1:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1}" and IA2:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩2}"
using Iagree_sub subs by auto
then show ?case
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
next
case (dsafe_Times θ⇩1 θ⇩2) then
have safe:"dsafe θ⇩1" "dsafe θ⇩2"
and IH1:"Vagree ν ν' (FVT θ⇩1) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩1} ⟹ dterm_sem I θ⇩1 ν = dterm_sem J θ⇩1 ν'"
and IH2:"Vagree ν ν' (FVT θ⇩2) ⟹ Iagree I J {Inl x |x. x ∈ SIGT θ⇩2} ⟹ dterm_sem I θ⇩2 ν = dterm_sem J θ⇩2 ν'"
and VA:"Vagree ν ν' (FVT (Times θ⇩1 θ⇩2))"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT (Times θ⇩1 θ⇩2)}"
by auto
from VA have VA1:"Vagree ν ν' (FVT θ⇩1)" and VA2:"Vagree ν ν' (FVT θ⇩2)"
unfolding Vagree_def by auto
have subs:"{Inl x |x. x ∈ SIGT θ⇩1} ⊆ {Inl x |x. x ∈ SIGT (Times θ⇩1 θ⇩2)}"
"{Inl x |x. x ∈ SIGT θ⇩2} ⊆ {Inl x |x. x ∈ SIGT (Times θ⇩1 θ⇩2)}"by auto
from IA have IA1:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩1}" and IA2:"Iagree I J {Inl x |x. x ∈ SIGT θ⇩2}"
using Iagree_sub subs by auto
then show ?case
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
qed (auto simp: Vagree_def directional_derivative_def coincidence_frechet')

subsection ‹ODE Coincidence Theorems›
lemma coincidence_ode:
fixes I J :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c::finite state" and ν'::"'c::finite state"
shows "osafe ODE ⟹
Vagree ν ν' (Inl  FVO ODE) ⟹
Iagree I J ({Inl x | x. Inl x ∈ SIGO ODE}  ∪  {Inr (Inr x) | x. Inr x ∈ SIGO ODE}) ⟹
ODE_sem I ODE (fst ν) = ODE_sem J ODE (fst ν')"
proof (induction rule: osafe.induct)
case (osafe_Var c)
then show ?case
proof (auto)
assume VA:"Vagree ν ν' (range Inl)"
have eqV:"(fst ν) = (fst ν')"
using agree_UNIV_fst[OF VA] by auto
assume IA:"Iagree I J {Inr (Inr c)}"
have eqIJ:"ODEs I c = ODEs J c"
using Iagree_ODE[OF IA] by auto
show "ODEs I c (fst ν) = ODEs J c (fst ν')"
by (auto simp add: eqV eqIJ)
qed
next
case (osafe_Sing θ x)
then show ?case
proof (auto)
assume free:"dfree θ"
and VA:"Vagree ν ν' (insert (Inl x) (Inl  {x. Inl x ∈ FVT θ}))"
and IA:"Iagree I J {Inl x |x. x ∈ SIGT θ}"
from VA have VA':"Vagree ν ν' {Inl x | x. Inl x ∈ FVT θ}" unfolding Vagree_def by auto
have agree_Lem:"⋀θ. dfree θ ⟹ Vagree ν ν' {Inl x | x. Inl x ∈ FVT θ} ⟹ Vagree ν ν' (FVT θ)"
subgoal for θ
apply(induction rule: dfree.induct)
done
have trm:"sterm_sem I  θ (fst ν) = sterm_sem J θ (fst ν')"
using coincidence_sterm' free VA' IA agree_Lem[of θ, OF free] by blast
show "(λi. if i = x then sterm_sem I θ (fst ν) else 0) =
(λi. if i = x then sterm_sem J θ (fst ν') else 0)"
by (auto simp add: vec_eq_iff trm)
qed
next
case (osafe_Prod ODE1 ODE2)
then show ?case
proof (auto)
assume safe1:"osafe ODE1"
and  safe2:"osafe ODE2"
and  disjoint:"ODE_dom ODE1 ∩ ODE_dom ODE2 = {}"
and  IH1:"Vagree ν ν' (Inl  FVO ODE1) ⟹
Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE1} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE1}) ⟹ ODE_sem I ODE1 (fst ν) = ODE_sem J ODE1 (fst ν')"
and  IH2:"Vagree ν ν' (Inl  FVO ODE2) ⟹
Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE2} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE2}) ⟹ ODE_sem I ODE2 (fst ν) = ODE_sem J ODE2 (fst ν')"
and VA:"Vagree ν ν' (Inl  (FVO ODE1 ∪  FVO ODE2))"
and IA:"Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE1 ∨ Inl x ∈ SIGO ODE2} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE1 ∨ Inr x ∈ SIGO ODE2})"
let ?IA = "({Inl x |x. Inl x ∈ SIGO ODE1 ∨ Inl x ∈ SIGO ODE2} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE1 ∨ Inr x ∈ SIGO ODE2})"
have FVsubs:
"Inl  FVO ODE2 ⊆ Inl  (FVO ODE1 ∪ FVO ODE2)"
"Inl  FVO ODE1 ⊆ Inl  (FVO ODE1 ∪ FVO ODE2)"
by auto
from VA
have VA1:"Vagree ν ν' (Inl  FVO ODE1)"
and VA2:"Vagree ν ν' (Inl  FVO ODE2)"
using agree_sub[OF FVsubs(1)] agree_sub[OF FVsubs(2)]
by (auto)
have SIGsubs:
"({Inl x |x. Inl x ∈ SIGO ODE1} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE1}) ⊆ ?IA"
"({Inl x |x. Inl x ∈ SIGO ODE2} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE2}) ⊆ ?IA"
by auto
from IA
have IA1:"Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE1} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE1})"
and IA2:"Iagree I J ({Inl x |x. Inl x ∈ SIGO ODE2} ∪ {Inr (Inr x) |x. Inr x ∈ SIGO ODE2})"
using Iagree_sub[OF SIGsubs(1)] Iagree_sub[OF SIGsubs(2)] by auto
show "ODE_sem I ODE1 (fst ν) + ODE_sem I ODE2 (fst ν) = ODE_sem J ODE1 (fst ν') + ODE_sem J ODE2 (fst ν')"
using IH1[OF VA1 IA1] IH2[OF VA2 IA2] by auto
qed
qed

lemma coincidence_ode':
fixes I J :: "('a::finite, 'b::finite, 'c::finite) interp" and ν :: "'c simple_state" and ν'::"'c simple_state"
shows "osafe ODE ⟹
VSagree ν ν'  (FVO ODE) ⟹
Iagree I J ({Inl x | x. Inl x ∈ SIGO ODE}  ∪  {Inr (Inr x) | x. Inr x ∈ SIGO ODE}) ⟹
ODE_sem I ODE ν = ODE_sem J ODE ν'"
using coincidence_ode[of ODE  "(ν, χ i. 0)" "(ν', χ i. 0)" I J]
apply(auto)
unfolding VSagree_def Vagree_def apply auto
done

lemma alt_sem_lemma:"⋀ I::('a::finite,'b::finite,'c::finite) interp. ⋀  ODE::('a::finite,'c::finite) ODE. ⋀sol. ⋀t::real. ⋀ ab. osafe ODE ⟹
ODE_sem I ODE (sol t) = ODE_sem I ODE (χ i. if i ∈ FVO ODE then sol t $i else ab$ i)"
proof -
fix I::"('a,'b,'c) interp"
and ODE::"('a,'c) ODE"
and sol
and t::real
and ab
assume safe:"osafe ODE"
have VA:"VSagree (sol t) (χ i. if i ∈ FVO ODE then sol t $i else ab$ i) (FVO ODE)"
unfolding VSagree_def Vagree_def by auto
have IA: "Iagree I I ({Inl x | x. Inl x ∈ SIGO ODE}  ∪  {Inr (Inr x) | x. Inr x ∈ SIGO ODE})" unfolding Iagree_def by auto
show "ODE_sem I ODE (sol t) = ODE_sem I ODE (χ i. if  i ∈ FVO ODE then sol t $i else ab$ i)"
using coincidence_ode'[OF safe VA IA] by auto
qed

lemma bvo_to_fvo:"Inl x ∈ BVO ODE ⟹  x ∈ FVO ODE"
proof (induction ODE)
qed auto

lemma ode_to_fvo:"x ∈ ODE_vars I ODE ⟹  x ∈ FVO ODE"
proof (induction ODE)
qed auto

definition coincide_hp :: "('a::finite, 'b::finite, 'c::finite) hp ⇒ ('a::finite, 'b::finite, 'c::finite) interp ⇒ ('a::finite, 'b::finite, 'c::finite) interp ⇒ bool"
where "coincide_hp α I J ⟷ (∀ ν ν' μ V. Iagree I J (SIGP α) ⟶ Vagree ν ν' V ⟶ V ⊇ (FVP α) ⟶ (ν, μ) ∈ prog_sem I α ⟶ (∃μ'. (ν', μ') ∈ prog_sem J α ∧ Vagree μ μ' (MBV α ∪ V)))"

definition ode_sem_equiv ::"('a::finite, 'b::finite, 'c::finite) hp ⇒ ('a::finite, 'b::finite, 'c::finite) interp ⇒ bool"
where "ode_sem_equiv α I ⟷
(∀ODE::('a::finite,'c::finite) ODE. ∀φ::('a::finite,'b::finite,'c::finite)formula. osafe ODE ⟶ fsafe φ  ⟶
(α = EvolveODE ODE φ) ⟶
{(ν, mk_v I ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I φ} ∧
VSagree (sol 0) (fst ν) {x | x. Inl x ∈ FVP (EvolveODE ODE φ)}} =
{(ν, mk_v I ODE ν (sol t)) | ν sol t.
t ≥ 0 ∧
(sol solves_ode (λ_. ODE_sem I ODE)) {0..t} {x. mk_v I ODE ν x ∈ fml_sem I φ} ∧
sol 0 = fst ν})"

definition coincide_hp' :: "('a::finite, 'b::finite, 'c::finite) hp ⇒ bool"
where "coincide_hp' α ⟷ (∀ I J. coincide_hp α I J ∧ ode_sem_equiv α I)"

definition coincide_fml  :: "('a::finite, 'b::finite, 'c::finite) formula ⇒ bool"
where "coincide_fml φ ⟷ (∀ ν ν' I J . Iagree I J (SIGF φ) ⟶ Vagree ν ν' (FVF φ) ⟶ ν ∈ fml_sem I φ ⟷ ν' ∈ fml_sem J φ)"

lemma coinc_fml [simp]: "coincide_fml φ  = (∀ ν ν' I J. Iagree I J (SIGF φ) ⟶ Vagree ν ν' (FVF φ) ⟶ ν ∈ fml_sem I φ ⟷ ν' ∈ fml_sem J φ)"
unfolding coincide_fml_def by auto

subsection ‹Coincidence Theorems for Programs and Formulas›
lemma coincidence_hp_fml:
fixes α::"('a::finite, 'b::finite, 'c::finite) hp"
fixes φ::"('a::finite, 'b::finite, 'c::finite) formula"
shows "(hpsafe α ⟶ coincide_hp' α) ∧ (fsafe φ ⟶ coincide_fml φ)"
proof (induction rule: hpsafe_fsafe.induct)
case (hpsafe_Pvar x)
thus "?case"
apply(unfold coincide_hp'_def | rule allI | rule conjI)+
prefer 2 unfolding ode_sem_equiv_def subgoal by auto
unfolding coincide_hp_def apply(auto)
subgoal for I J a b aa ba ab bb V
proof -
assume IA:"Iagree I J {Inr (Inr x)}"
have Peq:"⋀y. y ∈ Programs I x ⟷ y ∈ Programs J x" using Iagree_Prog[OF IA] by auto
assume agree:"Vagree (a, b) (aa, ba) V"
and sub:"UNIV ⊆ V"
and sem:"((a, b), ab, bb) ∈ Programs I x"
from agree_UNIV_eq[OF agree_sub [OF sub agree]]
have eq:"(a,b) = (aa,ba)" by auto
hence sem':"((aa,ba), (ab,bb)) ∈ Programs I x"
using sem by auto
have triv_sub:"V ⊆ UNIV" by auto
have VA:"Vagree (ab,bb) (ab,bb) V" using agree_sub[OF triv_sub agree_refl[of "(ab,bb)"]] eq
by auto
show "∃a b. ((aa, ba), a, b) ∈ Programs J x ∧ Vagree (ab, bb) (a, b) V"
apply(rule exI[where x="ab"])
apply(rule exI[where x="bb"])
using sem eq VA by (auto simp add: Peq)
qed
done
next
case (hpsafe_Assign e x) then
show "?case"
proof (auto simp only: coincide_hp'_def ode_sem_equiv_def coincide_hp_def)
fix I J :: "('a::finite,'b::finite,'c::finite) interp"
and ν1 ν2 ν'1 ν'2 μ1 μ2 V
assume safe:"dsafe e"
and IA:"Iagree I J (SIGP (x := e))"
and VA:"Vagree (ν1, ν2) (ν'1, ν'2) V"
and sub:"FVP (x := e) ⊆ V"
and sem:"((ν1, ν2), (μ1, μ2)) ∈ prog_sem I (x := e)"
from VA have VA':"Vagree (ν1, ν2) (ν'1, ν'2) (FVT e)" unfolding FVP.simps Vagree_def using sub by auto
have Ssub:"{Inl x | x. x ∈ SIGT e} ⊆ (SIGP (x := e))" by auto
from IA have IA':"Iagree I J {Inl x | x. x ∈ SIGT e}" using Ssub unfolding SIGP.simps by auto
have "((ν1, ν2), repv (ν1, ν2) x (dterm_sem I e (ν1, ν2))) ∈ prog_sem I (x := e)" by auto
then have sem':"((ν'1, ν'2), repv (ν'1, ν'2) x (dterm_sem J e (ν'1, ν'2))) ∈ prog_sem J (x := e)"
using coincidence_dterm' safe VA' IA' by auto
from sem have eq:"(μ1, μ2) = (repv (ν1, ν2) x (dterm_sem I e (ν1, ν2)))" by auto
have VA'':"Vagree (μ1, μ2) (repv (ν'1, ν'2) x (dterm_sem J e (ν'1, ν'2))) (MBV (x := e) ∪ V)"
using coincidence_dterm'[of e "(ν1,ν2)" "(ν'1,ν'2)" I J] safe VA' IA' eq agree_refl VA unfolding MBV.simps Vagree_def
by auto
show "∃μ'. ((ν'1, ν'2), μ') ∈ prog_sem J (x := e) ∧ Vagree (μ1, μ2) μ' (MBV (x := e) ∪ V)"
using VA'' sem' by blast
qed
next
case (hpsafe_DiffAssign e x) then show "?case"
proof (auto simp only: coincide_hp'_def ode_sem_equiv_def coincide_hp_def)
fix I J::"('a,'b,'c) interp"
and ν ν' μ V
assume safe:"dsafe e"
and IA:"Iagree I J (SIGP (DiffAssign x e))"
and VA:"Vagree ν ν' V"
and sub:"FVP (DiffAssign x e) ⊆ V"
and sem:"(ν, μ) ∈ prog_sem I (DiffAssign x e)"
from VA have VA':"Vagree ν ν' (FVT e)" unfolding FVP.simps Vagree_def using sub by auto
have Ssub:"{Inl x | x. x ∈ SIGT e} ⊆ (SIGP (DiffAssign x e))" by auto
from IA have IA':"Iagree I J {Inl x | x. x ∈ SIGT e}" using Ssub unfolding SIGP.simps by auto
have "(ν, repv ν x (dterm_sem I e `