Theory expstab

(*  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
    Copyright    2010 University of Cambridge
*)

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