author  paulson 
Wed, 19 Aug 1998 10:34:31 +0200  
changeset 5340  d75c03cf77b5 
parent 5277  e4297d03e5d2 
child 5648  fe887910e32e 
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.*) 

4776  17 
transient :: "[('a * 'a)set set, 'a set] => bool" 
5253  18 
"transient acts A == EX act:acts. A <= Domain act & act^^A <= Compl A" 
4776  19 

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

5253  21 
"ensures acts A B == constrains acts (AB) (A Un B) & transient acts (AB)" 
22 
(*(unless acts A B) would be equivalent*) 

4776  23 

5340  24 
syntax leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool" 
25 
consts leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set" 

4776  26 

27 
translations 

5253  28 
"leadsTo acts A B" == "(A,B) : leadsto acts" 
5340  29 
"~ leadsTo acts A B" <= "(A,B) ~: leadsto acts" 
4776  30 

5253  31 
inductive "leadsto acts" 
4776  32 
intrs 
33 

5253  34 
Basis "ensures acts A B ==> leadsTo acts A B" 
4776  35 

5253  36 
Trans "[ leadsTo acts A B; leadsTo acts B C ] 
37 
==> leadsTo acts A C" 

4776  38 

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

4776  44 

45 
monos "[Pow_mono]" 

46 

5155  47 

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

52 
end 