author | paulson |
Thu, 29 Apr 1999 10:51:58 +0200 | |
changeset 6536 | 281d44905cab |
parent 5931 | 325300576da7 |
child 6801 | 9e0037839d63 |
permissions | -rw-r--r-- |
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 higher-level 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 |
(*LEADS-TO constant for the inductive definition*) |
26 |
leadsto :: "'a program => ('a set * 'a set) set" |
|
5648 | 27 |
|
6536 | 28 |
(*visible version of the LEADS-TO relation*) |
29 |
leadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) |
|
30 |
||
4776 | 31 |
|
5648 | 32 |
inductive "leadsto F" |
4776 | 33 |
intrs |
34 |
||
6536 | 35 |
Basis "F : A ensures B ==> (A,B) : leadsto F" |
4776 | 36 |
|
5648 | 37 |
Trans "[| (A,B) : leadsto F; (B,C) : leadsto F |] |
38 |
==> (A,C) : leadsto F" |
|
4776 | 39 |
|
5155 | 40 |
(*Encoding using powerset of the desired axiom |
5648 | 41 |
(!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F |
5155 | 42 |
*) |
5648 | 43 |
Union "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F" |
4776 | 44 |
|
5721 | 45 |
monos Pow_mono |
4776 | 46 |
|
5155 | 47 |
|
5648 | 48 |
|
6536 | 49 |
defs |
50 |
ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)" |
|
51 |
||
52 |
leadsTo_def "A leadsTo B == {F. (A,B) : leadsto F}" |
|
53 |
||
54 |
constdefs |
|
5648 | 55 |
|
56 |
(*wlt F B is the largest set that leads to B*) |
|
57 |
wlt :: "['a program, 'a set] => 'a set" |
|
6536 | 58 |
"wlt F B == Union {A. F: A leadsTo B}" |
4776 | 59 |
|
60 |
end |