Theory Stability

(*<*)
theory Stability
imports
  Galois
  Lifted_Predicates
begin

(*>*)
section‹ Stability \label{sec:stability} ›

text‹

The essence of rely/guarantee reasoning is that sequential assertions must be ∗‹stable› with respect
to interfering transitions as expressed in a ∗‹rely› relation. Formally an assertion ‹P› is stable if it becomes
no less true for each transition in the rely ‹r›. This is essentially monotonicity, or that the extension of ‹P›
is ‹r›-closed.

References:
 ▪ \<^citet>‹‹\S3.1.3› in "Vafeiadis:2008"› has a def for stability in terms of separation logic

›

definition stable :: "'a rel ⇒ 'a pred ⇒ bool" where
  "stable r P = monotone (λx y. (x, y) ∈ r) (≤) P"

setup ‹Sign.mandatory_path "stable"›

named_theorems intro "stability intro rules"

lemma singleton_conv:
  shows "stable {(s, s')} P ⟷ (P s ⟶ P s')"
by (simp add: stable_def monotone_def le_bool_def)

lemma closed:
  shows "stable r P ⟷ r `` Collect P ⊆ Collect P"
unfolding stable_def monotone_def le_bool_def by auto

lemma rtrancl_conv:
  shows "stable (r⇧*) = stable r"
by (auto simp: stable_def monotone_def le_bool_def fun_eq_iff elim!: rtrancl_induct)

lemma reflcl_conv:
  shows "stable (r⇧=) = stable r"
unfolding stable_def monotone_def by simp

lemma empty[stable.intro]:
  shows "stable {} P"
unfolding stable_def by simp

lemma [stable.intro]:
  shows Id: "stable Id P"
    and Id_fst: "⋀P. stable (Id ×⇩R A) (λs. P (fst s))"
    and Id_fst_fst_snd: "⋀P. stable (Id ×⇩R Id ×⇩R A) (λs. P (fst s) (fst (snd s)))"
by (simp_all add: stable_def monotone_def)

lemma UNIV:
  shows "stable UNIV P ⟷ (∃c. P = ⟨c⟩)"
unfolding stable_def monotone_def le_bool_def by simp meson

lemma antimono_rel:
  shows "antimono (λr. stable r P)"
unfolding stable_def monotone_def using subset_iff by (fastforce intro: antimonoI)

lemmas strengthen_rel[strg] = st_ord_antimono[OF stable.antimono_rel, unfolded le_bool_def]

lemma infI:
  assumes "stable r P"
  shows infI1: "stable (r ∩ s) P"
    and infI2: "stable (s ∩ r) P"
using assms unfolding stable_def monotone_def by simp_all

lemma UNION_conv:
  shows "stable (⋃x∈X. r x) P ⟷ (∀x∈X. stable (r x) P)"
unfolding stable_def monotone_def by blast

lemmas UNIONI[stable.intro] = iffD2[OF stable.UNION_conv, rule_format]

lemma Union_conv:
  shows "stable (⋃X) P ⟷ (∀x∈X. stable x P)"
unfolding stable_def monotone_def by blast

lemma union_conv:
  shows "stable (r ∪ s) P ⟷ stable r P ∧ stable s P"
unfolding stable_def monotone_def by blast

lemmas UnionI[stable.intro] = iffD2[OF stable.Union_conv, rule_format]
lemmas unionI[stable.intro] = iffD2[OF stable.union_conv, rule_format, unfolded conj_explode]


paragraph‹ Properties of \<^const>‹stable› with respect to the predicate ›

lemma const[stable.intro]:
  shows "stable r ⟨c⟩"
    and "stable r ⊥"
    and "stable r ⊤"
by (simp_all add: stable_def monotone_def)

lemma conjI[stable.intro]:
  assumes "stable r P"
  assumes "stable r Q"
  shows "stable r (P ❙∧ Q)"
using assms by (simp add: stable_def)

lemma disjI[stable.intro]:
  assumes "stable r P"
  assumes "stable r Q"
  shows "stable r (P ❙∨ Q)"
using assms by (simp add: stable_def monotone_def le_bool_def)

lemma implies_constI[stable.intro]:
  assumes "P ⟹ stable r Q"
  shows "stable r (λs. P ⟶ Q s)"
using assms by (auto simp: stable_def monotone_def le_bool_def)

lemma allI[stable.intro]:
  assumes "⋀x. stable r (P x)"
  shows "stable r (❙∀x. P x)"
using assms by (simp add: stable_def monotone_def le_bool_def)

lemma ballI[stable.intro]:
  assumes "⋀x. x ∈ X ⟹ stable r (P x)"
  shows "stable r (λs. ∀x∈X. P x s)"
using assms by (simp add: stable_def monotone_def le_bool_def)

lemma stable_relprod_fstI[stable.intro]:
  assumes "stable r P"
  shows "stable (r ×⇩R s) (λs. P (fst s))"
using assms by (clarsimp simp: stable_def monotone_def)

lemma stable_relprod_sndI[stable.intro]:
  assumes "stable s P"
  shows "stable (r ×⇩R s) (λs. P (snd s))"
using assms by (clarsimp simp: stable_def monotone_def)

lemma local_only: ―‹ for predicates that are insensitive to the shared state ›
  assumes "⋀ls s s'. P (ls, s) ⟷ P (ls, s')"
  shows "stable (Id ×⇩R UNIV) P"
using assms by (fastforce simp: stable_def monotone_def le_bool_def)

lemma Id_on_proj:
  assumes "⋀v. stable Id⇘f⇙ (λs. P v s)"
  shows "stable Id⇘f⇙ (λs. P (f s) s)"
using assms unfolding stable_def by (rule monotone_Id_on_proj)

lemma if_const_conv:
  shows "stable r (if c then P else Q) ⟷ stable r (λs. c ⟶ P s) ∧ stable r (λs. ¬c ⟶ Q s)"
by (simp add: stable_def)

lemma ifI[stable.intro]:
  assumes "stable r (λs. c s ⟶ P s)"
  assumes "stable r (λs. ¬c s ⟶ Q s)"
  shows "stable r (λs. if c s then P s else Q s)"
using assms by (simp add: stable.intro)

lemma ifI2[stable.intro]:
  assumes "stable r (λs. c s ⟶ P s s)"
  assumes "stable r (λs. ¬c s ⟶ Q s s)"
  shows "stable r (λs. (if c s then P s else Q s) s)"
using assms by (simp add: stable.intro)

lemma case_optionI[stable.intro]:
  assumes "stable r (λs. opt s = None ⟶ none s)"
  assumes "⋀v. stable r (λs. opt s = Some v ⟶ some v s)"
  shows "stable r (λs. case opt s of None ⇒ none s | Some v ⇒ some v s)"
using assms by (simp add: stable.intro split: option.split)

lemma case_optionI2[stable.intro]:
  assumes "opt = None ⟹ stable r none"
  assumes "⋀v. opt = Some v ⟹ stable r (some v)"
  shows "stable r (case opt of None ⇒ none | Some v ⇒ some v)"
using assms by (simp add: stable.intro split: option.split)

text‹ In practice the following rules are often too weak ›

lemma impliesI:
  assumes "stable r (❙¬P)"
  assumes "stable r Q"
  shows "stable r (P ❙⟶ Q)"
using assms by (auto simp: stable_def monotone_def le_bool_def)

lemma exI:
  assumes "⋀x. stable r (P x)"
  shows "stable r (❙∃x. P x)"
using assms by (auto simp: stable_def monotone_def le_bool_def)

lemma bexI:
  assumes "⋀x. x ∈ X ⟹ stable r (P x)"
  shows "stable r (λs. ∃x∈X. P x s)"
using assms by (auto simp: stable_def monotone_def le_bool_def)

setup ‹Sign.parent_path›
(*<*)

end
(*>*)