author  nipkow 
Tue, 09 Jan 2001 15:32:27 +0100  
changeset 10834  a7897aebbffc 
parent 10797  028d22926a41 
child 13797  baefae13ad37 
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" 
10834  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 

10293  37 
Union "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F" 
4776  38 

5155  39 

8006  40 
constdefs 
6536  41 

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

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

5648  45 

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

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

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

9685  50 
syntax (xsymbols) 
51 
"op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\\<longmapsto>" 60) 

52 

4776  53 
end 