13 constdefs |
13 constdefs |
14 |
14 |
15 (*This definition specifies weak fairness. The rest of the theory |
15 (*This definition specifies weak fairness. The rest of the theory |
16 is generic to all forms of fairness.*) |
16 is generic to all forms of fairness.*) |
17 transient :: "[('a * 'a)set set, 'a set] => bool" |
17 transient :: "[('a * 'a)set set, 'a set] => bool" |
18 "transient Acts A == EX act:Acts. A <= Domain act & act^^A <= Compl A" |
18 "transient acts A == EX act:acts. A <= Domain act & act^^A <= Compl A" |
19 |
19 |
20 ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
20 ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
21 "ensures Acts A B == constrains Acts (A-B) (A Un B) & transient Acts (A-B)" |
21 "ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)" |
22 (*(unless Acts A B) would be equivalent*) |
22 (*(unless acts A B) would be equivalent*) |
23 |
23 |
24 consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
24 consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
25 leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set" |
25 leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set" |
26 |
26 |
27 translations |
27 translations |
28 "leadsTo Acts A B" == "(A,B) : leadsto Acts" |
28 "leadsTo acts A B" == "(A,B) : leadsto acts" |
29 |
29 |
30 inductive "leadsto Acts" |
30 inductive "leadsto acts" |
31 intrs |
31 intrs |
32 |
32 |
33 Basis "ensures Acts A B ==> leadsTo Acts A B" |
33 Basis "ensures acts A B ==> leadsTo acts A B" |
34 |
34 |
35 Trans "[| leadsTo Acts A B; leadsTo Acts B C |] |
35 Trans "[| leadsTo acts A B; leadsTo acts B C |] |
36 ==> leadsTo Acts A C" |
36 ==> leadsTo acts A C" |
37 |
37 |
38 (*Encoding using powerset of the desired axiom |
38 (*Encoding using powerset of the desired axiom |
39 (!!A. A : S ==> leadsTo Acts A B) ==> leadsTo Acts (Union S) B |
39 (!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B |
40 *) |
40 *) |
41 Union "(UN A:S. {(A,B)}) : Pow (leadsto Acts) |
41 Union "(UN A:S. {(A,B)}) : Pow (leadsto acts) |
42 ==> leadsTo Acts (Union S) B" |
42 ==> leadsTo acts (Union S) B" |
43 |
43 |
44 monos "[Pow_mono]" |
44 monos "[Pow_mono]" |
45 |
45 |
46 |
46 |
47 (*wlt Acts B is the largest set that leads to B*) |
47 (*wlt acts B is the largest set that leads to B*) |
48 constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set" |
48 constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set" |
49 "wlt Acts B == Union {A. leadsTo Acts A B}" |
49 "wlt acts B == Union {A. leadsTo acts A B}" |
50 |
50 |
51 end |
51 end |