src/HOL/UNITY/WFair.thy

Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them

(*  Title:      HOL/UNITY/WFair
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Weak Fairness versions of transient, ensures, leadsTo.

From Misra, "A Logic for Concurrent Programming", 1994
*)

WFair = UNITY +

constdefs

  (*This definition specifies weak fairness.  The rest of the theory
    is generic to all forms of fairness.*)
  transient :: "[('a * 'a)set set, 'a set] => bool"
    "transient acts A == EX act:acts. A <= Domain act & act^^A <= Compl A"

  ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
    "ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)"
			(*(unless acts A B) would be equivalent*)

consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
       leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
  
translations
  "leadsTo acts A B" == "(A,B) : leadsto acts"

inductive "leadsto acts"
  intrs 

    Basis  "ensures acts A B ==> leadsTo acts A B"

    Trans  "[| leadsTo acts A B;  leadsTo acts B C |]
	   ==> leadsTo acts A C"

    (*Encoding using powerset of the desired axiom
       (!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B
    *)
    Union  "(UN A:S. {(A,B)}) : Pow (leadsto acts)
	   ==> leadsTo acts (Union S) B"

  monos "[Pow_mono]"


(*wlt acts B is the largest set that leads to B*)
constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
  "wlt acts B == Union {A. leadsTo acts A B}"

end