4776

1 
(* Title: HOL/UNITY/WFair


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1998 University of Cambridge


5 


6 
Weak Fairness versions of transient, ensures, leadsTo.


7 


8 
From Misra, "A Logic for Concurrent Programming", 1994


9 
*)


10 


11 
WFair = Traces + Vimage +


12 


13 
constdefs


14 


15 
transient :: "[('a * 'a)set set, 'a set] => bool"


16 
"transient Acts A == EX act:Acts. A <= Domain act & act^^A <= Compl A"


17 


18 
ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"


19 
"ensures Acts A B == constrains Acts (AB) (A Un B) & transient Acts (AB)"


20 


21 
consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"


22 
leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"


23 


24 
translations


25 
"leadsTo Acts A B" == "(A,B) : leadsto Acts"


26 


27 
inductive "leadsto Acts"


28 
intrs


29 


30 
Basis "ensures Acts A B ==> leadsTo Acts A B"


31 


32 
Trans "[ leadsTo Acts A B; leadsTo Acts B C ]


33 
==> leadsTo Acts A C"


34 


35 
Union "(UN A:S. {(A,B)}) : Pow (leadsto Acts)


36 
==> leadsTo Acts (Union S) B"


37 


38 
monos "[Pow_mono]"


39 


40 
constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"


41 
"wlt Acts B == Union {A. leadsTo Acts A B}"


42 


43 
end
