Theory Invariants

(*  Title:       Invariants.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Reachability and Invariance"

theory Invariants
imports Lib TransitionSystems
begin

subsection Reachability

text ‹
  A state is `reachable' under @{term I} if either it is the initial state, or it is the
  destination of a transition whose action satisfies @{term I} from a reachable state.
  The `standard' definition of reachability is recovered by setting @{term I} to @{term TT}.
›

inductive_set reachable
  for A :: "('s, 'a) automaton"
  and I :: "'a  bool"
where
    reachable_init: "s  init A  s  reachable A I"
  | reachable_step: " s  reachable A I; (s, a, s')  trans A; I a   s'  reachable A I"

inductive_cases reachable_icases: "s  reachable A I"

lemma reachable_pair_induct [consumes, case_names init step]:
  assumes "(ξ, p)  reachable A I"
      and "ξ p. (ξ, p)  init A  P ξ p"
      and "(ξ p ξ' p' a.  (ξ, p)  reachable A I; P ξ p;
                            ((ξ, p), a, (ξ', p'))  trans A; I a   P ξ' p')"
    shows "P ξ p"
  using assms(1) proof (induction "(ξ, p)" arbitrary: ξ p)
    fix ξ p
    assume "(ξ, p)  init A"
    with assms(2) show "P ξ p" .
  next
    fix s a ξ' p'
    assume "s  reachable A I"
       and tr: "(s, a, (ξ', p'))  trans A"
       and "I a"
       and IH: "ξ p. s = (ξ, p)  P ξ p"
    from this(1) obtain ξ p where "s = (ξ, p)"
                              and "(ξ, p)  reachable A I"
      by (metis prod.collapse)
    note this(2)
    moreover from IH and s = (ξ, p) have "P ξ p" .
    moreover from tr and s = (ξ, p) have "((ξ, p), a, (ξ', p'))  trans A" by simp
    ultimately show "P ξ' p'"
      using I a by (rule assms(3))
  qed

lemma reachable_weakenE [elim]:
  assumes "s  reachable A P"
      and PQ: "a. P a  Q a"
    shows "s  reachable A Q"
  using assms(1)
  proof (induction)
    fix s assume "s  init A"
    thus "s  reachable A Q" ..
  next
    fix s a s'
    assume "s  reachable A P"
       and "s  reachable A Q"
       and "(s, a, s')  trans A"
       and "P a"
    from P a have "Q a" by (rule PQ)
    with s  reachable A Q and (s, a, s')  trans A show "s'  reachable A Q" ..
  qed

lemma reachable_weaken_TT [elim]:
  assumes "s  reachable A I"
    shows "s  reachable A TT"
  using assms by rule simp

lemma init_empty_reachable_empty:
  assumes "init A = {}"
    shows "reachable A I = {}"
  proof (rule ccontr)
    assume "reachable A I  {}"
    then obtain s where "s  reachable A I" by auto
    thus False
    proof (induction rule: reachable.induct)
      fix s
      assume "s  init A"
      with init A = {} show False by simp
    qed
  qed

subsection Invariance

definition invariant
  :: "('s, 'a) automaton  ('a  bool)  ('s  bool)  bool"
  ("_  (1'(_ →')/ _)" [100, 0, 9] 8)
where
  "(A  (I →) P) = (sreachable A I. P s)"

abbreviation
  any_invariant
  :: "('s, 'a) automaton  ('s  bool)  bool"
  ("_  _" [100, 9] 8)
where
  "(A  P)  (A  (TT →) P)"

lemma invariantI [intro]:
  assumes init: "s. s  init A  P s"
      and step: "s a s'.  s  reachable A I; P s; (s, a, s')  trans A; I a   P s'"
    shows "A  (I →) P"
  unfolding invariant_def
  proof
       fix s
    assume "s  reachable A I"
      thus "P s"
    proof induction
      fix s assume "s  init A"
      thus "P s" by (rule init)
    next
      fix s a s'
      assume "s  reachable A I"
         and "P s"
         and "(s, a, s')  trans A"
         and "I a"
        thus "P s'" by (rule step)
    qed
  qed

lemma invariant_pairI [intro]:
  assumes init: "ξ p. (ξ, p)  init A  P (ξ, p)"
      and step: "ξ p ξ' p' a.
                    (ξ, p)  reachable A I; P (ξ, p); ((ξ, p), a, (ξ', p'))  trans A; I a 
                    P (ξ', p')"
    shows "A  (I →) P"
  using assms by auto

lemma invariant_arbitraryI:
  assumes "s. s  reachable A I  P s"
    shows "A  (I →) P"
  using assms unfolding invariant_def by simp

lemma invariantD [dest]:
  assumes "A  (I →) P"
      and "s  reachable A I"
    shows "P s"
  using assms unfolding invariant_def by blast

lemma invariant_initE [elim]:
  assumes invP: "A  (I →) P"
      and init: "s  init A"
    shows "P s"
  proof -
    from init have "s  reachable A I" ..
    with invP show ?thesis ..
  qed

lemma invariant_weakenE [elim]:
  fixes T σ P Q
  assumes invP: "A  (PI →) P"
      and PQ:   "s. P s  Q s"
      and QIPI: "a. QI a  PI a"
    shows       "A  (QI →) Q"
  proof
    fix s
    assume "s  init A"
    with invP have "P s" ..
    thus "Q s" by (rule PQ)
  next
    fix s a s'
    assume "s  reachable A QI"
       and "(s, a, s')  trans A"
       and "QI a"
    from QI a have "PI a" by (rule QIPI)
    from s  reachable A QI and QIPI have "s  reachable A PI" ..
    hence "s'  reachable A PI" using (s, a, s')  trans A and PI a ..
    with invP have "P s'" ..
    thus "Q s'" by (rule PQ)
  qed

definition
  step_invariant
  :: "('s, 'a) automaton  ('a  bool)  (('s, 'a) transition  bool)  bool"
  ("_ A (1'(_ →')/ _)" [100, 0, 0] 8)
where
  "(A A (I →) P) = (a. I a  (sreachable A I. (s'.(s, a, s')  trans A  P (s, a, s'))))"

lemma invariant_restrict_inD [dest]:
  assumes "A  (TT →) P"
    shows "A  (QI →) P"
  using assms by auto

abbreviation
  any_step_invariant
  :: "('s, 'a) automaton  (('s, 'a) transition  bool)  bool"
  ("_ A _" [100, 9] 8)
where
  "(A A P)  (A A (TT →) P)"

lemma step_invariant_true:
  "p A (λ(s, a, s'). True)"
  unfolding step_invariant_def by simp

lemma step_invariantI [intro]:
  assumes *: "s a s'.  sreachable A I; (s, a, s')trans A; I a   P (s, a, s')"
    shows "A A (I →) P"
  unfolding step_invariant_def
  using assms by auto

lemma step_invariantD [dest]:
  assumes "A A (I →) P"
      and "sreachable A I"
      and "(s, a, s')  trans A"
      and "I a"
    shows "P (s, a, s')"
  using assms unfolding step_invariant_def by blast

lemma step_invariantE [elim]:
    fixes T σ P I s a s'
  assumes "A A (I →) P"
      and "sreachable A I"
      and "(s, a, s')  trans A"
      and "I a"
      and "P (s, a, s')  Q"
    shows "Q"
  using assms by auto

lemma step_invariant_pairI [intro]:
  assumes *: "ξ p ξ' p' a.
               (ξ, p)  reachable A I; ((ξ, p), a, (ξ', p'))  trans A; I a 
                                                        P ((ξ, p), a, (ξ', p'))"
    shows "A A (I →) P"
  using assms by auto

lemma step_invariant_arbitraryI:
  assumes "ξ p a ξ' p'.  (ξ, p)  reachable A I; ((ξ, p), a, (ξ', p'))  trans A; I a 
            P ((ξ, p), a, (ξ', p'))"
    shows "A A (I →) P"
  using assms by auto

lemma step_invariant_weakenE [elim!]:
  fixes T σ P Q
  assumes invP: "A A (PI →) P"
      and PQ:   "t. P t  Q t"
      and QIPI: "a. QI a  PI a"
    shows       "A A (QI →) Q"
  proof
    fix s a s'
    assume "s  reachable A QI"
       and "(s, a, s')  trans A"
       and "QI a"
    from QI a have "PI a" by (rule QIPI)
    from s  reachable A QI have "s  reachable A PI" using QIPI ..
    with invP have "P (s, a, s')" using (s, a, s')  trans A PI a ..
    thus "Q (s, a, s')" by (rule PQ)
  qed

lemma step_invariant_weaken_with_invariantE [elim]:
  assumes pinv: "A  (I →) P"
      and qinv: "A A (I →) Q"
      and wr: "s a s'.  P s; P s'; Q (s, a, s'); I a   R (s, a, s')"
    shows "A A (I →) R"
  proof
    fix s a s'
    assume sr: "s  reachable A I"
       and tr: "(s, a, s')  trans A"
       and "I a"
    hence "s'  reachable A I" ..
    with pinv have "P s'" ..
    from pinv and sr have "P s" ..
    from qinv sr tr I a have "Q (s, a, s')" ..
    with P s and P s' show "R (s, a, s')" using I a by (rule wr)
  qed

lemma step_to_invariantI:
  assumes sinv: "A A (I →) Q"
      and init: "s. s  init A  P s"
      and step: "s s' a.
                    s  reachable A I;
                     P s;
                     Q (s, a, s');
                     I a   P s'"
    shows "A  (I →) P"
  proof
    fix s assume "s  init A" thus "P s" by (rule init)
  next
    fix s s' a
    assume "s  reachable A I"
       and "P s"
       and "(s, a, s')  trans A"
       and "I a"
      show "P s'"
    proof -
      from sinv and sreachable A I and (s, a, s')trans A and I a have "Q (s, a, s')" ..
      with sreachable A I and P s show "P s'" using I a by (rule step)
    qed
  qed

end