# Theory expstab

theory expstab
imports Main

```(*  Title:       expstab.thy
Author:      John Wickerson, University of Cambridge Computer Laboratory
Description: A formalisation of several properties of Explicit
Stabilisation, as presented in Section 3 of the ESOP 2010
paper `Explicit Stabilisation for Modular Rely-Guarantee
Reasoning' by John Wickerson, Mike Dodds and Matthew
Parkinson
*)

theory expstab imports Main begin

typedecl state

types
rely = "state => state => bool"
ass  = "state => bool" (* NB: This is a shallow embedding *)

constdefs
tt :: ass
"tt ≡ λs. True"
ff :: ass
"ff ≡ λs. False"
TT :: rely
"TT ≡ λs. λs'. True"
FF :: rely
"FF ≡ λs. λs'. False"
conj :: "ass => ass => ass" (infixr "∧" 60)
"p ∧ p' ≡ λs. p s ∧ p' s"
disj :: "ass => ass => ass" (infixr "∨" 60)
"p ∨ p' ≡ λs. p s ∨ p' s"
not_ass :: "ass => ass" ("¬ _" [70] 70)
"¬ p ≡ λs. ¬ p s"
floor :: "ass => rely => ass" ("⌊_⌋_" [50, 90] 80)
"⌊p⌋R ≡ λs. ∀s'. R^** s s' --> p s'"
ceil :: "ass => rely => ass" ("⌈_⌉_" [50, 90] 80)
"⌈p⌉R ≡ λs. ∃s'. R^** s' s ∧ p s'"
(* Remark on syntax: the Transitive_Closure library writes
R^** for the transitive closure of a binary predicate
R :: 'a => 'a => bool, while R^* denotes the transitive
closure of a relation R :: ('a × 'a) set.   *)

definition
stronger :: "ass => ass => bool" (infixr "-->" 20)
where "p --> q ≡ (∀s. p s --> q s)"

definition
samestrength :: "ass => ass => bool" (infixr "<->" 20)
where "p <-> q ≡ (∀s. p s = q s)"

definition
stab :: "ass => rely => bool" (infix "stab" 30)
where "(p stab R) ≡ (∀s s'. p s --> R s s' --> p s')"

(* Here is an equivalent formulation of the stab
predicate that uses R^** instead of R    *)
lemma stab_def_manystep:
"(p stab R) = (∀s s'. p s --> R^** s s' --> p s')"
unfolding stab_def
proof(intro iffI)
assume "∀s s'. p s --> R s s' --> p s'"
thus "∀s s'. p s --> R^** s s' --> p s'"
proof(intro allI impI)
fix s::state and s'::state
assume a1:"∀s s'. p s --> R s s' --> p s'"
and a2:"p s" and a3:"R^** s s'"
thus "p s'"
using rtranclp_induct[OF a3, of p] by auto
qed
qed(auto)

(* alternative definition of samestrength in
terms of stronger    *)
lemma samestrength_def_symstronger:
"((p::ass) <-> (q::ass)) = ((p --> q) ∧ (q --> p))"
unfolding samestrength_def and stronger_def by auto

lemma samestrength_sym:
"(p::ass) <-> (q::ass) ==> q <-> p"
unfolding samestrength_def by auto

(* - - - - - - - - - - -  *)
(* FUNDAMENTAL PROPERTIES *)

lemma floor_stronger: "⌊p⌋R --> p"
unfolding floor_def and stronger_def by auto

lemma ceil_weaker: "p --> ⌈p⌉R"
unfolding ceil_def and stronger_def by auto

lemma floor_is_stab: "⌊p⌋R stab R"
unfolding stab_def and floor_def
proof(intro allI impI)
fix s::state and s'::state and s''::state
assume a1: "∀s'. R^** s s' --> p s'"
and a2: "R s s'" and a3: "R^** s' s''"
from a2 and a3 have "R^** s s''" by auto
with a1 show "p s''" by auto
qed

lemma ceil_is_stab: "⌈p⌉R stab R"
unfolding stab_def and ceil_def
proof (intro allI impI)
fix s::state and s'::state
assume "∃s''. R^** s'' s ∧ p s''" and "R s s'"
hence "∃s''. R^** s'' s ∧ R^** s s' ∧ p s''" by auto
thus "∃s''. R^** s'' s' ∧ p s''"
using rtranclp_trans[of R] by auto
qed

lemma floor_weakest:
"q --> p ==> q stab R ==> q --> ⌊p⌋R"
unfolding stab_def_manystep
and floor_def and stronger_def by auto

lemma ceil_weakest:
"p --> q ==> q stab R ==> ⌈p⌉R --> q"
unfolding ceil_def
and stab_def_manystep and stronger_def by auto

lemma true_stab: "tt stab R"
unfolding stab_def and tt_def by auto

lemma false_stab: "ff stab R"
unfolding ff_def and stab_def by auto

lemma conj_pres_stab:
"[|p stab R; q stab R|] ==> p ∧ q stab R"
unfolding stab_def and conj_def by auto

lemma disj_pres_stab:
"[|p stab R; q stab R|] ==> p ∨ q stab R"
unfolding stab_def and disj_def by auto

lemma floor_mono:
"p --> p' ==> ⌊p⌋R --> ⌊p'⌋R"
unfolding floor_def and stronger_def by auto

lemma ceil_mono:
"p --> p' ==> ⌈p⌉R --> ⌈p'⌉R"
unfolding ceil_def and stronger_def by auto

lemma duality_floor_ceil:
"(⌈(¬ p)⌉R) <-> ¬(⌊p⌋(R^--1))"
unfolding samestrength_def
and not_ass_def and ceil_def and floor_def
proof(intro allI iffI)
fix s::state
assume "∃s'. R^** s' s ∧ ¬ p s'"
thus "¬ (∀s'. (R^--1)^** s s' --> p s')"
using rtranclp_converseI [of R] by auto
next
fix s::state
assume "¬ (∀s'. (R^--1)^** s s' --> p s')"
thus "∃s'. R^** s' s ∧ ¬ p s'"
using rtranclp_converseD [of R] by auto
qed

lemma floor_of_stab: "p stab R ==> p <-> ⌊p⌋R"
unfolding samestrength_def
and stab_def_manystep and floor_def by auto

lemma ceil_of_stab: "p stab R ==> p <-> ⌈p⌉R"
unfolding samestrength_def
and stab_def_manystep and ceil_def by auto

lemma floor_of_FF: "⌊p⌋FF <-> p"
unfolding samestrength_def and FF_def and floor_def
proof(intro allI iffI)
fix s::state and s'::state
assume a1: "p s"
thus "(λs s'. False)^** s s' --> p s'"
proof(intro impI)
assume a2: "(λs s'. False)^** s s'"
with a1 show "p s'"
using converse_rtranclpE[OF a2, of "p s'"]
by auto
qed
qed(auto)

lemma ceil_of_FF: "⌈p⌉FF <-> p"
unfolding samestrength_def and FF_def and ceil_def
proof(intro allI iffI)
fix s::state
assume "∃s'. (λs s'. False)^** s' s ∧ p s'"
then obtain s'
where a:"(λs s'. False)^** s' s" and "p s'" by auto
thus "p s" using converse_rtranclpE[OF a, of "p s"] by auto
qed(auto)

lemma dist_floor_conj: "⌊p ∧ q⌋R <-> ⌊p⌋R ∧ ⌊q⌋R"
unfolding floor_def and conj_def and samestrength_def by auto

lemma dist_ceil_conj: "⌈p ∧ q⌉R --> ⌈p⌉R ∧ ⌈q⌉R"
unfolding ceil_def and conj_def and stronger_def by auto

lemma dist_floor_disj: "⌊p⌋R ∨ ⌊q⌋R --> ⌊p ∨ q⌋R"
unfolding floor_def and disj_def and stronger_def by auto

lemma dist_ceil_disj: "⌈p ∨ q⌉R <-> ⌈p⌉R ∨ ⌈q⌉R"
unfolding ceil_def and disj_def and samestrength_def by auto

lemma stab_antitone: "R ≤ R' ==> p stab R' --> p stab R"
unfolding stab_def by auto

lemma ceil_rely: "R ≤ R' ==> ⌈p⌉R --> ⌈p⌉R'"
unfolding ceil_def and stronger_def using rtranclp_mono by auto

lemma floor_rely: "R ≤ R' ==> ⌊p⌋R' --> ⌊p⌋R"
unfolding floor_def and stronger_def using rtranclp_mono by auto

(* - - - - - - - - -  *)
(* DERIVED PROPERTIES *)

lemma floor_floor1: "R ≤ R' ==> ⌊⌊p⌋R⌋R' <-> ⌊p⌋R'"
proof -
assume a: "R ≤ R'"
have "⌊⌊p⌋R⌋R' --> ⌊p⌋R'"
using floor_stronger[of p R]
and floor_mono[of "⌊p⌋R" p R'] by auto
moreover have "⌊p⌋R' --> ⌊⌊p⌋R⌋R'"
using floor_rely[OF a, of p]
and floor_weakest[of "⌊p⌋R'" "⌊p⌋R" R']
and floor_is_stab[of p R'] by auto
ultimately show "⌊⌊p⌋R⌋R' <-> ⌊p⌋R'"
using samestrength_def_symstronger by auto
qed

lemma floor_floor2: "R ≤ R' ==> ⌊⌊p⌋R'⌋R <-> ⌊p⌋R'"
proof -
assume a:"R ≤ R'"
thus "⌊⌊p⌋R'⌋R <-> ⌊p⌋R'"
using floor_of_stab[of "⌊p⌋R'" R]
and floor_is_stab[of p R']
and stab_antitone[OF a, of "⌊p⌋R'"]
and samestrength_sym
by auto
qed

lemma ceil_floor: "R ≤ R' ==> ⌈⌊p⌋R'⌉R <-> ⌊p⌋R'"
proof -
assume a:"R ≤ R'"
thus "⌈⌊p⌋R'⌉R <->⌊p⌋R'"
using ceil_of_stab[of "⌊p⌋R'" R]
and floor_is_stab[of p R']
and stab_antitone[OF a, of "⌊p⌋R'"]
and samestrength_sym
by auto
qed

lemma ceil_ceil1: "R ≤ R' ==> ⌈⌈p⌉R⌉R' <-> ⌈p⌉R'"
proof -
assume a: "R ≤ R'"
have "⌈p⌉R' --> ⌈⌈p⌉R⌉R'"
using ceil_mono[OF ceil_weaker, of p R' R] by auto
moreover have "⌈⌈p⌉R⌉R' --> ⌈p⌉R'"
using ceil_weakest[of "⌈p⌉R" "⌈p⌉R'" R']
and ceil_rely[OF a, of p]
and ceil_is_stab[of p R'] by auto
ultimately show "⌈⌈p⌉R⌉R' <-> ⌈p⌉R'"
using samestrength_def_symstronger by auto
qed

lemma ceil_ceil2: "R ≤ R' ==> ⌈⌈p⌉R'⌉R <-> ⌈p⌉R'"
proof -
assume a: "R ≤ R'"
thus "⌈⌈p⌉R'⌉R <-> ⌈p⌉R'"
using ceil_of_stab[of "⌈p⌉R'" R]
and ceil_is_stab[of p R']
and stab_antitone[OF a, of "⌈p⌉R'"]
and samestrength_sym
by auto
qed

lemma floor_ceil: "R ≤ R' ==> ⌊⌈p⌉R'⌋R <-> ⌈p⌉R'"
proof -
assume a: "R ≤ R'"
thus "⌊⌈p⌉R'⌋R <-> ⌈p⌉R'"
using floor_of_stab[of "⌈p⌉R'" R]
and ceil_is_stab[of p R']
and stab_antitone[OF a, of "⌈p⌉R'"]
and samestrength_sym
by auto
qed

end

```