author | paulson |
Wed, 19 Dec 2001 11:13:27 +0100 | |
changeset 12552 | d2d2ab3f1f37 |
parent 12195 | ed2893765a08 |
child 14077 | 37c964462747 |
permissions | -rw-r--r-- |
11479 | 1 |
(* Title: HOL/UNITY/WFair.thy |
2 |
ID: $Id$ |
|
3 |
Author: Sidi Ehmety, 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 |
Theory ported from HOL. |
|
11 |
*) |
|
12 |
||
12552
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
12195
diff
changeset
|
13 |
WFair = UNITY + Main_ZFC + |
11479 | 14 |
constdefs |
15 |
||
12195 | 16 |
(* This definition specifies weak fairness. The rest of the theory |
11479 | 17 |
is generic to all forms of fairness.*) |
18 |
transient :: "i=>i" |
|
12195 | 19 |
"transient(A) =={F:program. (EX act: Acts(F). A<=domain(act) & |
20 |
act``A <= state-A) & st_set(A)}" |
|
11479 | 21 |
|
22 |
ensures :: "[i,i] => i" (infixl 60) |
|
23 |
"A ensures B == ((A-B) co (A Un B)) Int transient(A-B)" |
|
24 |
||
25 |
consts |
|
26 |
||
27 |
(*LEADS-TO constant for the inductive definition*) |
|
12195 | 28 |
leads :: "[i, i]=>i" |
11479 | 29 |
|
12195 | 30 |
inductive |
11479 | 31 |
domains |
12195 | 32 |
"leads(D, F)" <= "Pow(D)*Pow(D)" |
11479 | 33 |
intrs |
12195 | 34 |
Basis "[| F:A ensures B; A:Pow(D); B:Pow(D) |] ==> <A,B>:leads(D, F)" |
35 |
Trans "[| <A,B> : leads(D, F); <B,C> : leads(D, F) |] ==> <A,C>:leads(D, F)" |
|
36 |
Union "[| S:Pow({A:S. <A, B>:leads(D, F)}); B:Pow(D); S:Pow(Pow(D)) |] ==> |
|
37 |
<Union(S),B>:leads(D, F)" |
|
11479 | 38 |
|
39 |
monos Pow_mono |
|
12195 | 40 |
type_intrs "[Union_PowI, UnionI, PowI]" |
11479 | 41 |
|
42 |
constdefs |
|
43 |
||
12195 | 44 |
(* The Visible version of the LEADS-TO relation*) |
11479 | 45 |
leadsTo :: "[i, i] => i" (infixl 60) |
12195 | 46 |
"A leadsTo B == {F:program. <A,B>:leads(state, F)}" |
11479 | 47 |
|
12195 | 48 |
(* wlt(F, B) is the largest set that leads to B*) |
11479 | 49 |
wlt :: "[i, i] => i" |
12195 | 50 |
"wlt(F, B) == Union({A:Pow(state). F: A leadsTo B})" |
11479 | 51 |
|
52 |
syntax (xsymbols) |
|
53 |
"op leadsTo" :: "[i, i] => i" (infixl "\\<longmapsto>" 60) |
|
54 |
||
55 |
end |