author  berghofe 
Wed, 21 Oct 1998 17:57:02 +0200  
changeset 5721  458a67fd5461 
parent 5648  fe887910e32e 
child 5931  325300576da7 
permissions  rwrr 
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 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset

11 
WFair = UNITY + 
4776  12 

13 
constdefs 

14 

5155  15 
(*This definition specifies weak fairness. The rest of the theory 
16 
is generic to all forms of fairness.*) 

5648  17 
transient :: "'a set => 'a program set" 
18 
"transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}" 

4776  19 

5648  20 
ensures :: "['a set, 'a set] => 'a program set" 
21 
"ensures A B == constrains (AB) (A Un B) Int transient (AB)" 

22 

23 

24 
consts leadsto :: "'a program => ('a set * 'a set) set" 

4776  25 

5648  26 
inductive "leadsto F" 
4776  27 
intrs 
28 

5648  29 
Basis "F : ensures A B ==> (A,B) : leadsto F" 
4776  30 

5648  31 
Trans "[ (A,B) : leadsto F; (B,C) : leadsto F ] 
32 
==> (A,C) : leadsto F" 

4776  33 

5155  34 
(*Encoding using powerset of the desired axiom 
5648  35 
(!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F 
5155  36 
*) 
5648  37 
Union "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F" 
4776  38 

5721  39 
monos Pow_mono 
4776  40 

5155  41 

5648  42 

43 
constdefs (*visible version of the relation*) 

44 
leadsTo :: "['a set, 'a set] => 'a program set" 

45 
"leadsTo A B == {F. (A,B) : leadsto F}" 

46 

47 
(*wlt F B is the largest set that leads to B*) 

48 
wlt :: "['a program, 'a set] => 'a set" 

49 
"wlt F B == Union {A. F: leadsTo A B}" 

4776  50 

51 
end 