author  paulson 
Thu, 11 Nov 1999 10:25:29 +0100  
changeset 8006  299127ded09d 
parent 7346  dace49c16aca 
child 9685  6d123a7e30bd 
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" 
5931  18 
"transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= A}" 
4776  19 

8006  20 
ensures :: "['a set, 'a set] => 'a program set" (infixl 60) 
21 
"A ensures B == (AB co A Un B) Int transient (AB)" 

22 

6536  23 

24 
consts 

25 

26 
(*LEADSTO constant for the inductive definition*) 

6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

27 
leads :: "'a program => ('a set * 'a set) set" 
5648  28 

6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

29 

9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

30 
inductive "leads F" 
4776  31 
intrs 
32 

6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

33 
Basis "F : A ensures B ==> (A,B) : leads F" 
4776  34 

6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

35 
Trans "[ (A,B) : leads F; (B,C) : leads F ] ==> (A,C) : leads F" 
4776  36 

5155  37 
(*Encoding using powerset of the desired axiom 
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

38 
(!!A. A : S ==> (A,B) : leads F) ==> (Union S, B) : leads F 
5155  39 
*) 
7346
dace49c16aca
arguably clearer definition of the inductive case of
paulson
parents:
6801
diff
changeset

40 
Union "{(A,B)  A. A: S} : Pow (leads F) ==> (Union S, B) : leads F" 
4776  41 

5721  42 
monos Pow_mono 
4776  43 

5155  44 

8006  45 
constdefs 
6536  46 

8006  47 
(*visible version of the LEADSTO relation*) 
48 
leadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) 

49 
"A leadsTo B == {F. (A,B) : leads F}" 

5648  50 

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

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

6536  53 
"wlt F B == Union {A. F: A leadsTo B}" 
4776  54 

55 
end 