author  paulson 
Tue, 08 Jun 1999 10:59:02 +0200  
changeset 6801  9e0037839d63 
parent 6536  281d44905cab 
child 7346  dace49c16aca 
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 

6536  20 

21 
consts 

22 

23 
ensures :: "['a set, 'a set] => 'a program set" (infixl 60) 

5648  24 

6536  25 
(*LEADSTO constant for the inductive definition*) 
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

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

6536  28 
(*visible version of the LEADSTO relation*) 
29 
leadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) 

30 

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

31 

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

32 
inductive "leads F" 
4776  33 
intrs 
34 

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

35 
Basis "F : A ensures B ==> (A,B) : leads F" 
4776  36 

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

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

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

40 
(!!A. A : S ==> (A,B) : leads F) ==> (Union S, B) : leads F 
5155  41 
*) 
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset

42 
Union "(UN A:S. {(A,B)}) : Pow (leads F) ==> (Union S, B) : leads F" 
4776  43 

5721  44 
monos Pow_mono 
4776  45 

5155  46 

5648  47 

6536  48 
defs 
49 
ensures_def "A ensures B == (AB co A Un B) Int transient (AB)" 

50 

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

51 
leadsTo_def "A leadsTo B == {F. (A,B) : leads F}" 
6536  52 

53 
constdefs 

5648  54 

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

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

6536  57 
"wlt F B == Union {A. F: A leadsTo B}" 
4776  58 

59 
end 