author | nipkow |
Tue, 09 Jan 2001 15:32:27 +0100 | |
changeset 10834 | a7897aebbffc |
parent 10797 | 028d22926a41 |
child 13797 | baefae13ad37 |
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" |
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 == (A-B co A Un B) Int transient (A-B)" |
|
22 |
||
6536 | 23 |
|
24 |
consts |
|
25 |
||
26 |
(*LEADS-TO 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 LEADS-TO 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 |