(*  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 \<Rightarrow> state \<Rightarrow> bool"
  ass  = "state \<Rightarrow> bool" (* NB: This is a shallow embedding *)

constdefs
  tt :: ass
  "tt \<equiv> \<lambda>s. True"
  ff :: ass
  "ff \<equiv> \<lambda>s. False"
  TT :: rely
  "TT \<equiv> \<lambda>s. \<lambda>s'. True"
  FF :: rely
  "FF \<equiv> \<lambda>s. \<lambda>s'. False"
  conj :: "ass \<Rightarrow> ass \<Rightarrow> ass" (infixr "\<and>" 60)
  "p \<and> p' \<equiv> \<lambda>s. p s \<and> p' s"
  disj :: "ass \<Rightarrow> ass \<Rightarrow> ass" (infixr "\<or>" 60)
  "p \<or> p' \<equiv> \<lambda>s. p s \<or> p' s"
  not_ass :: "ass \<Rightarrow> ass" ("\<not> _" [70] 70)
  "\<not> p \<equiv> \<lambda>s. \<not> p s"
  floor :: "ass \<Rightarrow> rely \<Rightarrow> ass" ("\<lfloor>_\<rfloor>_" [50, 90] 80)
  "\<lfloor>p\<rfloor>R \<equiv> \<lambda>s. \<forall>s'. R^** s s' \<longrightarrow> p s'"
  ceil :: "ass \<Rightarrow> rely \<Rightarrow> ass" ("\<lceil>_\<rceil>_" [50, 90] 80)
  "\<lceil>p\<rceil>R \<equiv> \<lambda>s. \<exists>s'. R^** s' s \<and> p s'"
(* Remark on syntax: the Transitive_Closure library writes
   R^** for the transitive closure of a binary predicate 
   R :: 'a \<Rightarrow> 'a \<Rightarrow> bool, while R^* denotes the transitive 
   closure of a relation R :: ('a \<times> 'a) set.   *)

definition 
  stronger :: "ass \<Rightarrow> ass \<Rightarrow> bool" (infixr "\<longrightarrow>" 20)
where "p \<longrightarrow> q \<equiv> (\<forall>s. p s \<longrightarrow> q s)" 

definition 
  samestrength :: "ass \<Rightarrow> ass \<Rightarrow> bool" (infixr "\<longleftrightarrow>" 20)
where "p \<longleftrightarrow> q \<equiv> (\<forall>s. p s = q s)"

definition 
  stab :: "ass \<Rightarrow> rely \<Rightarrow> bool" (infix "stab" 30)
where "(p stab R) \<equiv> (\<forall>s s'. p s \<longrightarrow> R s s' \<longrightarrow> p s')"
  
(* Here is an equivalent formulation of the stab 
   predicate that uses R^** instead of R    *)
lemma stab_def_manystep: 
  "(p stab R) = (\<forall>s s'. p s \<longrightarrow> R^** s s' \<longrightarrow> p s')" 
  unfolding stab_def
proof(intro iffI)
  assume "\<forall>s s'. p s \<longrightarrow> R s s' \<longrightarrow> p s'"
  thus "\<forall>s s'. p s \<longrightarrow> R^** s s' \<longrightarrow> p s'"
  proof(intro allI impI)
    fix s::state and s'::state
    assume a1:"\<forall>s s'. p s \<longrightarrow> R s s' \<longrightarrow> 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) \<longleftrightarrow> (q::ass)) = ((p \<longrightarrow> q) \<and> (q \<longrightarrow> p))" 
  unfolding samestrength_def and stronger_def by auto 

lemma samestrength_sym: 
  "(p::ass) \<longleftrightarrow> (q::ass) \<Longrightarrow> q \<longleftrightarrow> p" 
  unfolding samestrength_def by auto

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

lemma floor_stronger: "\<lfloor>p\<rfloor>R \<longrightarrow> p" 
  unfolding floor_def and stronger_def by auto

lemma ceil_weaker: "p \<longrightarrow> \<lceil>p\<rceil>R" 
  unfolding ceil_def and stronger_def by auto

lemma floor_is_stab: "\<lfloor>p\<rfloor>R stab R" 
  unfolding stab_def and floor_def 
proof(intro allI impI)
  fix s::state and s'::state and s''::state
  assume a1: "\<forall>s'. R^** s s' \<longrightarrow> 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: "\<lceil>p\<rceil>R stab R" 
  unfolding stab_def and ceil_def 
proof (intro allI impI)
  fix s::state and s'::state
  assume "\<exists>s''. R^** s'' s \<and> p s''" and "R s s'"
  hence "\<exists>s''. R^** s'' s \<and> R^** s s' \<and> p s''" by auto
  thus "\<exists>s''. R^** s'' s' \<and> p s''" 
    using rtranclp_trans[of R] by auto
qed

lemma floor_weakest: 
  "q \<longrightarrow> p \<Longrightarrow> q stab R \<Longrightarrow> q \<longrightarrow> \<lfloor>p\<rfloor>R" 
  unfolding stab_def_manystep 
    and floor_def and stronger_def by auto
 
lemma ceil_weakest: 
  "p \<longrightarrow> q \<Longrightarrow> q stab R \<Longrightarrow> \<lceil>p\<rceil>R \<longrightarrow> 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: 
  "\<lbrakk>p stab R; q stab R\<rbrakk> \<Longrightarrow> p \<and> q stab R" 
  unfolding stab_def and conj_def by auto

lemma disj_pres_stab: 
  "\<lbrakk>p stab R; q stab R\<rbrakk> \<Longrightarrow> p \<or> q stab R" 
  unfolding stab_def and disj_def by auto

lemma floor_mono: 
  "p \<longrightarrow> p' \<Longrightarrow> \<lfloor>p\<rfloor>R \<longrightarrow> \<lfloor>p'\<rfloor>R" 
  unfolding floor_def and stronger_def by auto

lemma ceil_mono: 
  "p \<longrightarrow> p' \<Longrightarrow> \<lceil>p\<rceil>R \<longrightarrow> \<lceil>p'\<rceil>R" 
  unfolding ceil_def and stronger_def by auto

lemma duality_floor_ceil: 
  "(\<lceil>(\<not> p)\<rceil>R) \<longleftrightarrow> \<not>(\<lfloor>p\<rfloor>(R^--1))" 
  unfolding samestrength_def 
    and not_ass_def and ceil_def and floor_def
proof(intro allI iffI)
  fix s::state
  assume "\<exists>s'. R^** s' s \<and> \<not> p s'"
  thus "\<not> (\<forall>s'. (R^--1)^** s s' \<longrightarrow> p s')" 
    using rtranclp_converseI [of R] by auto
next
  fix s::state
  assume "\<not> (\<forall>s'. (R^--1)^** s s' \<longrightarrow> p s')"
  thus "\<exists>s'. R^** s' s \<and> \<not> p s'" 
    using rtranclp_converseD [of R] by auto
qed

lemma floor_of_stab: "p stab R \<Longrightarrow> p \<longleftrightarrow> \<lfloor>p\<rfloor>R" 
  unfolding samestrength_def 
  and stab_def_manystep and floor_def by auto

lemma ceil_of_stab: "p stab R \<Longrightarrow> p \<longleftrightarrow> \<lceil>p\<rceil>R" 
unfolding samestrength_def 
  and stab_def_manystep and ceil_def by auto

lemma floor_of_FF: "\<lfloor>p\<rfloor>FF \<longleftrightarrow> 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 "(\<lambda>s s'. False)^** s s' \<longrightarrow> p s'" 
  proof(intro impI)
    assume a2: "(\<lambda>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: "\<lceil>p\<rceil>FF \<longleftrightarrow> p" 
  unfolding samestrength_def and FF_def and ceil_def
proof(intro allI iffI)
  fix s::state
  assume "\<exists>s'. (\<lambda>s s'. False)^** s' s \<and> p s'"
  then obtain s' 
    where a:"(\<lambda>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: "\<lfloor>p \<and> q\<rfloor>R \<longleftrightarrow> \<lfloor>p\<rfloor>R \<and> \<lfloor>q\<rfloor>R" 
  unfolding floor_def and conj_def and samestrength_def by auto

lemma dist_ceil_conj: "\<lceil>p \<and> q\<rceil>R \<longrightarrow> \<lceil>p\<rceil>R \<and> \<lceil>q\<rceil>R" 
  unfolding ceil_def and conj_def and stronger_def by auto

lemma dist_floor_disj: "\<lfloor>p\<rfloor>R \<or> \<lfloor>q\<rfloor>R \<longrightarrow> \<lfloor>p \<or> q\<rfloor>R" 
  unfolding floor_def and disj_def and stronger_def by auto

lemma dist_ceil_disj: "\<lceil>p \<or> q\<rceil>R \<longleftrightarrow> \<lceil>p\<rceil>R \<or> \<lceil>q\<rceil>R" 
  unfolding ceil_def and disj_def and samestrength_def by auto

lemma stab_antitone: "R \<le> R' \<Longrightarrow> p stab R' \<longrightarrow> p stab R" 
  unfolding stab_def by auto

lemma ceil_rely: "R \<le> R' \<Longrightarrow> \<lceil>p\<rceil>R \<longrightarrow> \<lceil>p\<rceil>R'" 
  unfolding ceil_def and stronger_def using rtranclp_mono by auto

lemma floor_rely: "R \<le> R' \<Longrightarrow> \<lfloor>p\<rfloor>R' \<longrightarrow> \<lfloor>p\<rfloor>R" 
  unfolding floor_def and stronger_def using rtranclp_mono by auto

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

lemma floor_floor1: "R \<le> R' \<Longrightarrow> \<lfloor>\<lfloor>p\<rfloor>R\<rfloor>R' \<longleftrightarrow> \<lfloor>p\<rfloor>R'"
proof -
  assume a: "R \<le> R'"
  have "\<lfloor>\<lfloor>p\<rfloor>R\<rfloor>R' \<longrightarrow> \<lfloor>p\<rfloor>R'" 
    using floor_stronger[of p R]
      and floor_mono[of "\<lfloor>p\<rfloor>R" p R'] by auto
  moreover have "\<lfloor>p\<rfloor>R' \<longrightarrow> \<lfloor>\<lfloor>p\<rfloor>R\<rfloor>R'" 
    using floor_rely[OF a, of p]
      and floor_weakest[of "\<lfloor>p\<rfloor>R'" "\<lfloor>p\<rfloor>R" R'] 
      and floor_is_stab[of p R'] by auto
  ultimately show "\<lfloor>\<lfloor>p\<rfloor>R\<rfloor>R' \<longleftrightarrow> \<lfloor>p\<rfloor>R'" 
    using samestrength_def_symstronger by auto
qed

lemma floor_floor2: "R \<le> R' \<Longrightarrow> \<lfloor>\<lfloor>p\<rfloor>R'\<rfloor>R \<longleftrightarrow> \<lfloor>p\<rfloor>R'"
proof -
  assume a:"R \<le> R'"
  thus "\<lfloor>\<lfloor>p\<rfloor>R'\<rfloor>R \<longleftrightarrow> \<lfloor>p\<rfloor>R'" 
    using floor_of_stab[of "\<lfloor>p\<rfloor>R'" R] 
      and floor_is_stab[of p R'] 
      and stab_antitone[OF a, of "\<lfloor>p\<rfloor>R'"] 
      and samestrength_sym
    by auto
qed

lemma ceil_floor: "R \<le> R' \<Longrightarrow> \<lceil>\<lfloor>p\<rfloor>R'\<rceil>R \<longleftrightarrow> \<lfloor>p\<rfloor>R'"
proof -
  assume a:"R \<le> R'"
  thus "\<lceil>\<lfloor>p\<rfloor>R'\<rceil>R \<longleftrightarrow>\<lfloor>p\<rfloor>R'"
    using ceil_of_stab[of "\<lfloor>p\<rfloor>R'" R] 
      and floor_is_stab[of p R'] 
      and stab_antitone[OF a, of "\<lfloor>p\<rfloor>R'"]
      and samestrength_sym
    by auto
qed

lemma ceil_ceil1: "R \<le> R' \<Longrightarrow> \<lceil>\<lceil>p\<rceil>R\<rceil>R' \<longleftrightarrow> \<lceil>p\<rceil>R'"
proof -
  assume a: "R \<le> R'"
  have "\<lceil>p\<rceil>R' \<longrightarrow> \<lceil>\<lceil>p\<rceil>R\<rceil>R'"
    using ceil_mono[OF ceil_weaker, of p R' R] by auto
  moreover have "\<lceil>\<lceil>p\<rceil>R\<rceil>R' \<longrightarrow> \<lceil>p\<rceil>R'"
    using ceil_weakest[of "\<lceil>p\<rceil>R" "\<lceil>p\<rceil>R'" R']
    and ceil_rely[OF a, of p]
    and ceil_is_stab[of p R'] by auto
  ultimately show "\<lceil>\<lceil>p\<rceil>R\<rceil>R' \<longleftrightarrow> \<lceil>p\<rceil>R'" 
    using samestrength_def_symstronger by auto
qed

lemma ceil_ceil2: "R \<le> R' \<Longrightarrow> \<lceil>\<lceil>p\<rceil>R'\<rceil>R \<longleftrightarrow> \<lceil>p\<rceil>R'"
proof -
  assume a: "R \<le> R'"
  thus "\<lceil>\<lceil>p\<rceil>R'\<rceil>R \<longleftrightarrow> \<lceil>p\<rceil>R'"
    using ceil_of_stab[of "\<lceil>p\<rceil>R'" R]
      and ceil_is_stab[of p R']
      and stab_antitone[OF a, of "\<lceil>p\<rceil>R'"]
      and samestrength_sym
    by auto
qed

lemma floor_ceil: "R \<le> R' \<Longrightarrow> \<lfloor>\<lceil>p\<rceil>R'\<rfloor>R \<longleftrightarrow> \<lceil>p\<rceil>R'"
proof -
  assume a: "R \<le> R'"
  thus "\<lfloor>\<lceil>p\<rceil>R'\<rfloor>R \<longleftrightarrow> \<lceil>p\<rceil>R'"
    using floor_of_stab[of "\<lceil>p\<rceil>R'" R]
      and ceil_is_stab[of p R']
      and stab_antitone[OF a, of "\<lceil>p\<rceil>R'"]
      and samestrength_sym
    by auto
qed

end