Theory Invariance

section ‹Invariance›
theory Invariance
  imports ODE_Misc
begin

context auto_ll_on_open begin

definition "invariant M  (xM. trapped x M)"

definition "positively_invariant M  (xM. trapped_forward x M)"

definition "negatively_invariant M  (xM. trapped_backward x M)"

lemma positively_invariant_iff:
  "positively_invariant M 
  (xM. flow0 x ` (existence_ivl0 x  {0..}))  M"
  unfolding positively_invariant_def trapped_forward_def
  by auto

lemma negatively_invariant_iff:
  "negatively_invariant M 
  (xM. flow0 x ` (existence_ivl0 x  {..0}))  M"
  unfolding negatively_invariant_def trapped_backward_def
  by auto

lemma invariant_iff_pos_and_neg_invariant:
  "invariant M  positively_invariant M  negatively_invariant M"
  unfolding invariant_def trapped_def positively_invariant_def negatively_invariant_def
  by blast

lemma invariant_iff:
  "invariant M  (xM. flow0 x ` (existence_ivl0 x))   M"
  unfolding invariant_iff_pos_and_neg_invariant positively_invariant_iff negatively_invariant_iff
  by (metis (mono_tags) SUP_le_iff invariant_def invariant_iff_pos_and_neg_invariant negatively_invariant_iff positively_invariant_iff trapped_iff_on_existence_ivl0)

lemma positively_invariant_restrict_dom: "positively_invariant M = positively_invariant (M  X)"
  unfolding positively_invariant_def trapped_forward_def
  by (auto intro!: flow_in_domain dest: mem_existence_ivl_iv_defined)

lemma negatively_invariant_restrict_dom: "negatively_invariant M = negatively_invariant (M  X)"
  unfolding negatively_invariant_def trapped_backward_def
  by (auto intro!: flow_in_domain dest: mem_existence_ivl_iv_defined)

lemma invariant_restrict_dom: "invariant M = invariant (M  X)"
  using invariant_iff_pos_and_neg_invariant
    negatively_invariant_restrict_dom
    positively_invariant_restrict_dom by auto
    (*
lemma positively_invariant_imp_subset:
  "M ⊆ X" if "positively_invariant M"
  using positively_invariant_iff that by blast

lemma negatively_invariant_imp_subset:
  "M ⊆ X" if "negatively_invariant M"
  using negatively_invariant_iff that by blast

lemma invariant_imp_subset:
  "M ⊆ X" if "invariant M"
  using invariant_iff that by blast
*)

end context auto_ll_on_open begin

lemma positively_invariant_eq_rev: "positively_invariant M = rev.negatively_invariant M"
  unfolding positively_invariant_def rev.negatively_invariant_def
  by (simp add: rev.trapped_backward_iff_rev_trapped_forward)

lemma negatively_invariant_eq_rev: "negatively_invariant M = rev.positively_invariant M"
  unfolding negatively_invariant_def rev.positively_invariant_def
  by (simp add: trapped_backward_iff_rev_trapped_forward)

lemma invariant_eq_rev: "invariant M = rev.invariant M"
  unfolding invariant_iff_pos_and_neg_invariant rev.invariant_iff_pos_and_neg_invariant
    positively_invariant_eq_rev negatively_invariant_eq_rev by auto

lemma negatively_invariant_complI: "negatively_invariant (X-M)" if "positively_invariant M"
  unfolding negatively_invariant_def trapped_backward_def
proof clarsimp
  fix x t
  assume x: "x  X" "x  M" "t  existence_ivl0 x" "t  0"
  have a1:"flow0 x t  X" using x
    using flow_in_domain by blast
  have a2:"flow0 x t  M"
  proof (rule ccontr)
    assume "¬ flow0 x t  M"
    then have "trapped_forward (flow0 x t) M"
      using positively_invariant_def that by auto
    moreover have "flow0 (flow0 x t) (-t) = x"
      using t  existence_ivl0 x flows_reverse by auto
    moreover have "-t  existence_ivl0 (flow0 x t)  {0..}"
      using existence_ivl_reverse x(3) x(4) by auto
    ultimately have "x  M" unfolding trapped_forward_def
      by (metis image_subset_iff)
    thus False using x(2) by auto
  qed
  show "flow0 x t  X  flow0 x t  M" using a1 a2 by auto
qed

end context auto_ll_on_open begin

lemma negatively_invariant_complD: "positively_invariant M" if "negatively_invariant (X-M)"
proof -
  have "rev.positively_invariant (X-M)" using that
    by (simp add: negatively_invariant_eq_rev)
  then have "rev.negatively_invariant (X-(X-M))"
    by (simp add: rev.negatively_invariant_complI)
  then have "positively_invariant (X-(X-M))"
    using rev.negatively_invariant_eq_rev by auto
  thus ?thesis using Diff_Diff_Int
    by (metis inf_commute positively_invariant_restrict_dom) 
qed

lemma pos_invariant_iff_compl_neg_invariant: "positively_invariant M  negatively_invariant (X - M)"
  by (safe intro!: negatively_invariant_complI dest!: negatively_invariant_complD)

lemma neg_invariant_iff_compl_pos_invariant:
  shows "negatively_invariant M  positively_invariant (X - M)"
  by (simp add: auto_ll_on_open.pos_invariant_iff_compl_neg_invariant negatively_invariant_eq_rev positively_invariant_eq_rev rev.auto_ll_on_open_axioms)

lemma invariant_iff_compl_invariant:
  shows "invariant M  invariant (X - M)"
  using invariant_iff_pos_and_neg_invariant neg_invariant_iff_compl_pos_invariant pos_invariant_iff_compl_neg_invariant by blast

lemma invariant_iff_pos_invariant_and_compl_pos_invariant:
  shows "invariant M  positively_invariant M  positively_invariant (X-M)"
  by (simp add: invariant_iff_pos_and_neg_invariant neg_invariant_iff_compl_pos_invariant)

end

subsection ‹Tools for proving invariance›

context auto_ll_on_open begin

lemma positively_invariant_left_inter:
  assumes "positively_invariant C"
  assumes "x  C  D. trapped_forward x D"
  shows "positively_invariant (C  D)"
  using assms positively_invariant_def trapped_forward_def by auto

lemma trapped_forward_le:
  fixes V :: "'a  real"
  assumes "V x  0"
  assumes contg: "continuous_on (flow0 x ` (existence_ivl0 x  {0..})) g"
  assumes "x. (V has_derivative V' x) (at x)"
  assumes "s. s  existence_ivl0 x  {0..}  V' (flow0 x s) (f (flow0 x s))  g (flow0 x s) * V (flow0 x s)"
  shows "trapped_forward x {x. V x  0}"
  unfolding trapped_forward_def
proof clarsimp
  fix t
  assume t: "t  existence_ivl0 x" "0  t"
  then have ex:"{0..t}  existence_ivl0 x"
    by (simp add: local.ivl_subset_existence_ivl)
  have contV: "continuous_on UNIV V"
    using assms(3) has_derivative_continuous_on by blast
  have 1: "continuous_on {0..t} (g  flow0 x)"
    apply (rule continuous_on_compose)
    using continuous_on_subset ex local.flow_continuous_on apply blast
    by (meson Int_subset_iff atLeastAtMost_iff atLeast_iff contg continuous_on_subset ex image_mono subsetI)
  have 2: "(s. s  {0..t} 
         (V  flow0 x has_real_derivative (V' (flow0 x s)  f  flow0 x) s) (at s))"
    apply (auto simp add:o_def has_field_derivative_def)
  proof -                              
    fix s
    assume "0  s" "s  t"
    then have "s  existence_ivl0 x" using ex by auto
    from flow_has_derivative[OF this] have
      "(flow0 x has_derivative (λi. i *R f (flow0 x s))) (at s)" .
    from has_derivative_compose[OF this assms(3)]
    have "((λt. V (flow0 x t)) has_derivative (λt. V' (flow0 x s)  (t *R f (flow0 x s)))) (at s)" .
    moreover have "linear (V' (flow0 x s))"  using assms(3) has_derivative_linear by blast
    ultimately 
    have "((λt. V (flow0 x t)) has_derivative (λt. t *R V' (flow0 x s) (f (flow0 x s)))) (at s)" 
      unfolding linear_cmul[OF linear (V' (flow0 x s))] by blast
    thus "((λt. V (flow0 x t)) has_derivative (*) (V' (flow0 x s) (f (flow0 x s)))) (at s)"
      by (auto intro!: derivative_eq_intros simp add: mult_commute_abs)
  qed
  have 3: "(s. s  {0..t} 
         (V' (flow0 x s)   f  flow0 x) s  (g  flow0 x) s *R (V  flow0 x) s)"
    using ex by (auto intro!:assms(4))
  from comparison_principle_le_linear[OF 1 2 _ 3] assms(1)
  have "s  {0..t}. (V  flow0 x) s  0"
    using local.mem_existence_ivl_iv_defined(2) t(1) by auto
  thus " V (flow0 x t)  0"
    by (simp add: t(2))
qed

lemma positively_invariant_le_domain:
  fixes V :: "'a  real"
  assumes "positively_invariant D"
  assumes contg: "continuous_on D g"
  assumes "x. (V has_derivative V' x) (at x)" (* TODO: domain can be added here too ? *)
  assumes "s. s  D  V' s (f s)  g s * V s"
  shows "positively_invariant (D  {x. V x  0})"
  apply (auto intro!:positively_invariant_left_inter[OF assms(1)])
proof -
  fix x
  assume "x  D" "V x  0"
  have "continuous_on (flow0 x ` (existence_ivl0 x  {0..})) g"
    by (meson x  D assms(1) contg continuous_on_subset positively_invariant_def trapped_forward_def)
  from trapped_forward_le[OF V x  0 this assms(3)]
  show "trapped_forward x {x. V x  0}" using assms(4)
    using x  D assms(1) positively_invariant_def trapped_forward_def by auto
qed

lemma positively_invariant_barrier_domain:
  fixes V :: "'a  real"
  assumes "positively_invariant D"
  assumes "x. (V has_derivative V' x) (at x)"
  assumes "continuous_on D (λx. V' x (f x))"
  assumes "s. s  D  V s = 0  V' s (f s) < 0"
  shows "positively_invariant (D  {x. V x  0})"
  apply (auto intro!:positively_invariant_left_inter[OF assms(1)])
proof -
  fix x
  assume "x  D" "V x  0"
  have contV: "continuous_on UNIV V" using assms(2) has_derivative_continuous_on by blast
  then have *: "continuous_on (flow0 x ` (existence_ivl0 x  {0..})) V"
    using continuous_on_subset by blast
  have sub: "flow0 x ` (existence_ivl0 x  {0..})  D"
    using x  D assms(1) positively_invariant_def trapped_forward_def by auto
  then have contV': "continuous_on (flow0 x ` (existence_ivl0 x  {0..})) (λx. V' x (f x))"
    by (metis assms(3) continuous_on_subset)
  have nz: "i t. t  existence_ivl0 x 
       0  t   max (-V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))2) > 0"
  proof -
    fix i t
    assume "t  existence_ivl0 x" "0  t"
    then have "flow0 x t  D"
      using x  D assms(1) positively_invariant_def trapped_forward_def by auto
    then have "V (flow0 x t) = 0  - V' (flow0 x t) (f (flow0 x t)) > 0" using assms(4) by simp
    then have "(V (flow0 x t))^2 > 0  - V' (flow0 x t) (f (flow0 x t)) > 0" by simp
    thus "max (-V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))2) > 0" unfolding less_max_iff_disj
      by auto
  qed
  have *: "continuous_on (flow0 x ` (existence_ivl0 x  {0..})) (λx. V' x (f x) * V x / max (- V' x (f x)) ((V x)^2))"
    apply (auto intro!:continuous_intros continuous_on_max simp add: * contV')
    using nz by fastforce
  have "(t. t  existence_ivl0 x  {0..} 
        V' (flow0 x t) (f (flow0 x t)) 
        (V' (flow0 x t) (f (flow0 x t)) * V (flow0 x t)
        / max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))2)) * V (flow0 x t))"
  proof clarsimp
    fix t
    assume "t  existence_ivl0 x" "0  t"
    then have p: "max (-V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))2) > 0" using nz by auto
    have " V' (flow0 x t) (f (flow0 x t)) * max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))2)
        V' (flow0 x t) (f (flow0 x t)) * (V (flow0 x t))2"
      by (smt mult_minus_left mult_minus_right power2_eq_square mult_le_cancel_left_pos)
    then have "V' (flow0 x t) (f (flow0 x t))
        V' (flow0 x t) (f (flow0 x t)) * (V (flow0 x t))2
      / max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))2)"
      using p pos_le_divide_eq by blast
    thus " V' (flow0 x t) (f (flow0 x t))
          V' (flow0 x t) (f (flow0 x t)) * (V (flow0 x t)) * V (flow0 x t) /
           max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))2)"
      by (simp add: power2_eq_square)
  qed
  from trapped_forward_le[OF V x  0 * assms(2) this]
  show "trapped_forward x {x. V x  0}" by auto
qed

lemma positively_invariant_UNIV:
  shows "positively_invariant UNIV"
  using positively_invariant_iff by blast

lemma positively_invariant_conj:
  assumes "positively_invariant C"
  assumes "positively_invariant D"
  shows "positively_invariant (C  D)"
  using assms positively_invariant_def
  using positively_invariant_left_inter by auto

lemma positively_invariant_le:
  fixes V :: "'a  real"
  assumes contg: "continuous_on UNIV g"
  assumes "x. (V has_derivative V' x) (at x)"
  assumes "s. V' s (f s)  g s * V s"
  shows "positively_invariant {x. V x  0}"
proof -
  from positively_invariant_le_domain[OF positively_invariant_UNIV assms]  
  have "positively_invariant (UNIV  {x. V x  0})" .
  thus ?thesis by auto
qed

lemma positively_invariant_barrier:
  fixes V :: "'a  real"
  assumes "x. (V has_derivative V' x) (at x)"
  assumes "continuous_on UNIV (λx. V' x (f x))"
  assumes "s. V s = 0  V' s (f s) < 0"
  shows "positively_invariant {x. V x  0}"
proof -
  from positively_invariant_barrier_domain[OF positively_invariant_UNIV assms]  
  have "positively_invariant (UNIV  {x. V x  0})" .
  thus ?thesis by auto
qed

end

end