Session Differential_Dynamic_Logic

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)"
  by (simp add: vec_eq_iff)

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. x2"] 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)"
    by (vector add)
  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 * (iUNIV. 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)"
  by (simp add: continuous_on_vec_lambda)  

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 xR. f x  + g x)  (SUP xR. f x) + (SUP xR. g x)"
proof -
  have bddfg:"bdd_above((λx. f x + g x ) ` R)" 
    using bddf bddg apply (auto simp add: bdd_above_def)
    using add_mono_thms_linordered_semiring(1) by blast
  have eq:"(SUP xR. f x + g x)  (SUP xR. f x) + (SUP xR. g x)
     (xR. (f x + g x)  (SUP xR. f x) + (SUP xR. g x))"
    apply(rule cSUP_le_iff)
     subgoal by (rule nonempty)
    subgoal by (rule bddfg)
    done
  have fs:"x. x  R  f x  (SUP xR. f x)"
    using bddf 
    by (simp add: cSUP_upper)
  have gs:"x. x  R  g x  (SUP xR. g x)"
    using bddg
    by (simp add: cSUP_upper)
  have "(xR. (f x + g x)  (SUP xR. f x) + (SUP xR. 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)"
      by (simp add: norm_vec_def)
    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 xS. f x)  (SUP xS. 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 xR . (i  S. f i x))  (i  S. (SUP xR. 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. iF. (?bound i))"
      have bddG:"i::'a. F. bdd_above ((λx. iF. 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 xR. i{}. f i x)::real)  (i{}. SUP aR. f i a)"   by (simp add: non)
        then show ?case by auto
      next
        case (insert x F)
        have "((SUP xaR. iinsert x F. f i xa)::real)  (SUP xaR. f x xa +  (iF. f i xa))"
          using insert.hyps(2) by auto
        moreover have "...   (SUP xa R. f x xa) + (SUP xaR. (iF. f i xa))"
          by(rule sup_plus, rule non, rule bddF, rule bddG)
        moreover have "...  (SUP xa R. f x xa) + (iF. SUP aR. f i a)"
          using add_le_cancel_left conts insert.hyps(3) by blast
        moreover have "...  (i(insert x F). SUP aR. f i a)"
          by (simp add: insert.hyps(2))
        ultimately have "((SUP xaR. iinsert x F. f i xa)::real)  (i(insert x F). SUP aR. 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 xR . (i  S. norm(f i y1 x - f i y2 x)/norm(x)))  (i  S. (SUP xR. 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)  (xS. f x) < (xS. 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)  (iUNIV. 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]
        by (auto simp add: divide_right_mono)
      done
    have "i. (SUP yUNIV.  norm((f i x1 - f i x2) y)/norm(y)) = norm(f i x1 - f i x2)"
      by (simp add: onorm_def norm_blinfun.rep_eq)
    then have each_norm:"i. (SUP yUNIV.  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)" 
      by (simp add: blinfun.bounded_linear_right bounded_linear_sub)
    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. rarange (λ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. (iUNIV. 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. (iUNIV. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x)  M"
        apply(rule exI[where x= ?bigBound])
        by(auto simp add: bounds sum_mono) 
    qed
    have bdd_above:"(bdd_above ((λy. (iUNIV. 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. (iUNIV. ¦blinfun_apply (f i x1) x - blinfun_apply (f i x2) x¦ / norm x)  M"
      { fix bb :: "real  'b"
        have "b. (aUNIV. ¦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. (aUNIV. ¦blinfun_apply (f a x1) (bb r) - blinfun_apply (f a x2) (bb r)¦) / norm (bb r)  r"
          by blast }
      then show "r. b. (aUNIV. ¦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))"
      by (simp add: dist_blinfun_def)
    moreover have "... = (SUP yUNIV. 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 yUNIV. (L2_set (λi. norm(f i x1 y - f i x2 y)) UNIV)/norm(y))"
      using  euclid by auto
    moreover have "...  (SUP yUNIV. (iUNIV. norm(f i x1 y - f i x2 y))/norm(y))"
      using L2' SUP_cong SUP_leq bdd_above by auto
    moreover have "... = (SUP yUNIV. (iUNIV. norm(f i x1 y - f i x2 y)/norm(y)))"
      by (simp add: sum_divide_distrib)
    moreover have "...  (iUNIV. (SUP yUNIV.  norm(f i x1 y - f i x2 y)/norm(y)))"
      by(rule SUP_sum_comm[OF finite  nonemptyB, of x1 x2]) 
    moreover have "... = (iUNIV. norm(f i x1 - f i x2))"
      using each_norm by simp
    moreover have "... = (iUNIV. dist(f i x1) (f i x2))"
      by (simp add: dist_blinfun_def)
    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)"]
      by (simp add: dist_commute)
    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) = (iUNIV. axis i (f i x))" "(χ i. f' i x) = (iUNIV. 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)"
    by (simp add: bounded_linear_vec_nth)
  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: "tBasis  {0<..<1}" and
    mvt: "f (a + u) - f a = (iBasis. (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›
― ‹readable.›
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 ν ω {}"
  by (auto simp add: Vagree_def)

lemma agree_supset:"A  B  Vagree ν ν' A  Vagree ν ν' B"
  by (auto simp add: Vagree_def)

lemma VSagree_nil:"VSagree ν ω {}"
  by (auto simp add: VSagree_def)

lemma VSagree_supset:"A  B  VSagree ν ν' A  VSagree ν ν' B"
  by (auto simp add: VSagree_def)

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)"
  by (auto simp add: Vagree_def)

lemma agree_refl:"Vagree ν ν A"
  by (auto simp add: Vagree_def)

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

lemma VSagree_refl:"VSagree ν ν A"
  by (auto simp add: VSagree_def)

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 
  (iV.
    (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"
  by (auto simp add: Iagree_def)

― ‹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 ψ"
  by (auto simp add: Or_def)

lemma iff_sem [simp]: "(ν  fml_sem I (A  B))
   ((ν  fml_sem I A)  (ν  fml_sem I B))"
  by (auto simp add: Equiv_def)

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))"
  by (auto simp add: Implies_def)

lemma equals_sem [simp]: "(ν  fml_sem I (Equals θ θ'))
  = (dterm_sem I θ ν = dterm_sem I θ' ν)"
  by (auto simp add: Equals_def)

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)"
  apply (auto simp add: sound_def)
  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)"
  apply (auto simp add: sound_def)
  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  ( vid1Predicational 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)+
  apply(auto simp add: empty_def)
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"
  by (simp add: Skolem_holds_def valid_def)

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)+
  apply(simp add: CT_lemma)
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
  us the axioms we want for differential terms essentially for free.
 ›
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. {}"])
  apply(auto simp add: is_interp_def)
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)"
    by (simp add: eq)
  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)"
    by (simp add: eq)
  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)"
    by (simp add: eq')
  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])
    by(auto simp add: eq' blin)
 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
    using bounded_linear_add by (blast)
next
  case (dfree_Times θ1 θ2)
  then show ?case
    by (auto simp add: bounded_linear_add bounded_linear_const_mult bounded_linear_mult_const)
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)"
    by (auto simp add: bounded_linear_vec_nth)
  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 oL 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)) oL 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)
    by (simp add: blinfun.add_left free1 free2 simple_term_inverse) 
  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_add)
    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_add)
     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"
  by (auto simp add:  primify_contains)

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 ν ν' ((iFVT t1. primify i)  (iFVT t2. primify i))"
    using fvdiff_plus1 FVDiff.simps agree by (auto)
  have agreeL:"Vagree ν ν' ((iFVT 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 ν ν' ((iFVT t1. primify i)  (iFVT t2. primify i))"
    using fvdiff_plus1 FVDiff.simps agree by (auto)
  have agreeR:"Vagree ν ν' ((iFVT 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 ν ν' ((iFVT t1. primify i)  (iFVT t2. primify i))"
    using fvdiff_plus1 FVDiff.simps agree by (auto)
  have agreeL:"Vagree ν ν' ((iFVT 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 ν ν' ((iFVT t1. primify i)  (iFVT t2. primify i))"
    using fvdiff_plus1 FVDiff.simps agree by (auto)
  have agreeR:"Vagree ν ν' ((iFVT 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 *)
  apply(auto simp add: Vagree_def)
  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)
      by(auto simp add: Vagree_def)
    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