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) = (∀s∈reachable 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 ⟶ (∀s∈reachable 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'. ⟦ s∈reachable 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 "s∈reachable 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 "s∈reachable 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 ‹s∈reachable A I› and ‹(s, a, s')∈trans A› and ‹I a› have "Q (s, a, s')" ..
      with ‹s∈reachable A I› and ‹P s› show "P s'" using ‹I a› by (rule step)
    qed
  qed

end