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
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. x⇧2"] sum.If_cases)

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

lemma bounded_linear_vec:
  fixes f::"('a::finite) ⇒ 'b::real_normed_vector ⇒ 'c::real_normed_vector"
  assumes bounds:"⋀i. bounded_linear (f i)"
  shows "bounded_linear (λx. χ i. f i x)"
proof unfold_locales
  fix r x y
  interpret bounded_linear "f i" for i by fact
  show "(χ i. f i (x + y)) = (χ i. f i x) + (χ i. f i y)"
    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 * (∑i∈UNIV. K i)" (is "?lhs ≤ ?rhs") for x
    unfolding sum_distrib_left
    unfolding norm_vec_def
    by (auto intro!: L2_set_le_sum_abs[THEN order_trans] sum_mono simp: abs_mult)
  then show "∃K. ∀x. norm (χ i. f i x) ≤ norm x * K"
    by blast
qed

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

lemmas blinfun_vec_simps[simp] = blinfun_vec.rep_eq

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

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

lemma has_derivative_proj':
  fixes i::"'a::finite"
  shows "∀x. ((λ x. x $ i) has_derivative (λx::(real^'a). x $ i)) (at x)"
proof -
  have bounded_proj:"bounded_linear (λ x::(real^'a). x $ i)"
    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: "t∈Basis → {0<..<1}" and
    mvt: "f (a + u) - f a = (∑i∈Basis. (J (a + t i *⇩R u) u ∙ i) *⇩R i)"
    by auto
  note mvt
  also have "… ≥ J0"
  proof -
    have J: "⋀i. i ∈ Basis ⟹ J0 ≤ J (a + t i *⇩R u) u"
      using J_ivl t line_in by (auto simp: Pi_iff)
    show ?thesis
      using J
      unfolding atLeastAtMost_iff eucl_le[where 'a='b]
      by auto
  qed
  finally show ?thesis .
qed

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

theory Syntax
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