8 |
8 |
9 header{*Weak Safety*} |
9 header{*Weak Safety*} |
10 |
10 |
11 theory Constrains imports UNITY begin |
11 theory Constrains imports UNITY begin |
12 |
12 |
13 consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" |
|
14 |
|
15 (*Initial states and program => (final state, reversed trace to it)... |
13 (*Initial states and program => (final state, reversed trace to it)... |
16 Arguments MUST be curried in an inductive definition*) |
14 Arguments MUST be curried in an inductive definition*) |
17 |
15 |
18 inductive "traces init acts" |
16 inductive_set |
19 intros |
17 traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" |
|
18 for init :: "'a set" and acts :: "('a * 'a)set set" |
|
19 where |
20 (*Initial trace is empty*) |
20 (*Initial trace is empty*) |
21 Init: "s \<in> init ==> (s,[]) \<in> traces init acts" |
21 Init: "s \<in> init ==> (s,[]) \<in> traces init acts" |
22 |
22 |
23 Acts: "[| act: acts; (s,evs) \<in> traces init acts; (s,s'): act |] |
23 | Acts: "[| act: acts; (s,evs) \<in> traces init acts; (s,s'): act |] |
24 ==> (s', s#evs) \<in> traces init acts" |
24 ==> (s', s#evs) \<in> traces init acts" |
25 |
25 |
26 |
26 |
27 consts reachable :: "'a program => 'a set" |
27 inductive_set |
28 |
28 reachable :: "'a program => 'a set" |
29 inductive "reachable F" |
29 for F :: "'a program" |
30 intros |
30 where |
31 Init: "s \<in> Init F ==> s \<in> reachable F" |
31 Init: "s \<in> Init F ==> s \<in> reachable F" |
32 |
32 |
33 Acts: "[| act: Acts F; s \<in> reachable F; (s,s'): act |] |
33 | Acts: "[| act: Acts F; s \<in> reachable F; (s,s'): act |] |
34 ==> s' \<in> reachable F" |
34 ==> s' \<in> reachable F" |
35 |
35 |
36 constdefs |
36 constdefs |
37 Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) |
37 Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) |
38 "A Co B == {F. F \<in> (reachable F \<inter> A) co B}" |
38 "A Co B == {F. F \<in> (reachable F \<inter> A) co B}" |