20 init :: "(vertex*vertex)set" |
19 init :: "(vertex*vertex)set" |
21 --{* the initial state *} |
20 --{* the initial state *} |
22 |
21 |
23 text{*Following the definitions given in section 4.4 *} |
22 text{*Following the definitions given in section 4.4 *} |
24 |
23 |
25 constdefs |
24 definition highest :: "[vertex, (vertex*vertex)set]=>bool" where |
26 highest :: "[vertex, (vertex*vertex)set]=>bool" |
|
27 "highest i r == A i r = {}" |
25 "highest i r == A i r = {}" |
28 --{* i has highest priority in r *} |
26 --{* i has highest priority in r *} |
29 |
27 |
30 lowest :: "[vertex, (vertex*vertex)set]=>bool" |
28 definition lowest :: "[vertex, (vertex*vertex)set]=>bool" where |
31 "lowest i r == R i r = {}" |
29 "lowest i r == R i r = {}" |
32 --{* i has lowest priority in r *} |
30 --{* i has lowest priority in r *} |
33 |
31 |
34 act :: command |
32 definition act :: command where |
35 "act i == {(s, s'). s'=reverse i s & highest i s}" |
33 "act i == {(s, s'). s'=reverse i s & highest i s}" |
36 |
34 |
37 Component :: "vertex=>state program" |
35 definition Component :: "vertex=>state program" where |
38 "Component i == mk_total_program({init}, {act i}, UNIV)" |
36 "Component i == mk_total_program({init}, {act i}, UNIV)" |
39 --{* All components start with the same initial state *} |
37 --{* All components start with the same initial state *} |
40 |
38 |
41 |
39 |
42 text{*Some Abbreviations *} |
40 text{*Some Abbreviations *} |
43 constdefs |
41 definition Highest :: "vertex=>state set" where |
44 Highest :: "vertex=>state set" |
|
45 "Highest i == {s. highest i s}" |
42 "Highest i == {s. highest i s}" |
46 |
43 |
47 Lowest :: "vertex=>state set" |
44 definition Lowest :: "vertex=>state set" where |
48 "Lowest i == {s. lowest i s}" |
45 "Lowest i == {s. lowest i s}" |
49 |
46 |
50 Acyclic :: "state set" |
47 definition Acyclic :: "state set" where |
51 "Acyclic == {s. acyclic s}" |
48 "Acyclic == {s. acyclic s}" |
52 |
49 |
53 |
50 |
54 Maximal :: "state set" |
51 definition Maximal :: "state set" where |
55 --{* Every ``above'' set has a maximal vertex*} |
52 --{* Every ``above'' set has a maximal vertex*} |
56 "Maximal == \<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i s. highest j s)}" |
53 "Maximal == \<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i s. highest j s)}" |
57 |
54 |
58 Maximal' :: "state set" |
55 definition Maximal' :: "state set" where |
59 --{* Maximal vertex: equivalent definition*} |
56 --{* Maximal vertex: equivalent definition*} |
60 "Maximal' == \<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j)" |
57 "Maximal' == \<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j)" |
61 |
58 |
62 |
59 |
63 Safety :: "state set" |
60 definition Safety :: "state set" where |
64 "Safety == \<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)}" |
61 "Safety == \<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)}" |
65 |
62 |
66 |
63 |
67 (* Composition of a finite set of component; |
64 (* Composition of a finite set of component; |
68 the vertex 'UNIV' is finite by assumption *) |
65 the vertex 'UNIV' is finite by assumption *) |
69 |
66 |
70 system :: "state program" |
67 definition system :: "state program" where |
71 "system == JN i. Component i" |
68 "system == JN i. Component i" |
72 |
69 |
73 |
70 |
74 declare highest_def [simp] lowest_def [simp] |
71 declare highest_def [simp] lowest_def [simp] |
75 declare Highest_def [THEN def_set_simp, simp] |
72 declare Highest_def [THEN def_set_simp, simp] |