15 |
15 |
16 types state = "(vertex*vertex)set" |
16 types state = "(vertex*vertex)set" |
17 types command = "vertex=>(state*state)set" |
17 types command = "vertex=>(state*state)set" |
18 |
18 |
19 consts |
19 consts |
20 (* the initial state *) |
|
21 init :: "(vertex*vertex)set" |
20 init :: "(vertex*vertex)set" |
|
21 --{* the initial state *} |
|
22 |
|
23 text{*Following the definitions given in section 4.4 *} |
22 |
24 |
23 constdefs |
25 constdefs |
24 (* from the definitions given in section 4.4 *) |
|
25 (* i has highest priority in r *) |
|
26 highest :: "[vertex, (vertex*vertex)set]=>bool" |
26 highest :: "[vertex, (vertex*vertex)set]=>bool" |
27 "highest i r == A i r = {}" |
27 "highest i r == A i r = {}" |
28 |
28 --{* i has highest priority in r *} |
29 (* i has lowest priority in r *) |
29 |
30 lowest :: "[vertex, (vertex*vertex)set]=>bool" |
30 lowest :: "[vertex, (vertex*vertex)set]=>bool" |
31 "lowest i r == R i r = {}" |
31 "lowest i r == R i r = {}" |
|
32 --{* i has lowest priority in r *} |
32 |
33 |
33 act :: command |
34 act :: command |
34 "act i == {(s, s'). s'=reverse i s & highest i s}" |
35 "act i == {(s, s'). s'=reverse i s & highest i s}" |
35 |
36 |
36 (* All components start with the same initial state *) |
|
37 Component :: "vertex=>state program" |
37 Component :: "vertex=>state program" |
38 "Component i == mk_total_program({init}, {act i}, UNIV)" |
38 "Component i == mk_total_program({init}, {act i}, UNIV)" |
39 |
39 --{* All components start with the same initial state *} |
40 (* Abbreviations *) |
40 |
|
41 |
|
42 text{*Some Abbreviations *} |
|
43 constdefs |
41 Highest :: "vertex=>state set" |
44 Highest :: "vertex=>state set" |
42 "Highest i == {s. highest i s}" |
45 "Highest i == {s. highest i s}" |
43 |
46 |
44 Lowest :: "vertex=>state set" |
47 Lowest :: "vertex=>state set" |
45 "Lowest i == {s. lowest i s}" |
48 "Lowest i == {s. lowest i s}" |
46 |
49 |
47 Acyclic :: "state set" |
50 Acyclic :: "state set" |
48 "Acyclic == {s. acyclic s}" |
51 "Acyclic == {s. acyclic s}" |
49 |
52 |
50 (* Every above set has a maximal vertex: two equivalent defs. *) |
|
51 |
53 |
52 Maximal :: "state set" |
54 Maximal :: "state set" |
|
55 --{* Every ``above'' set has a maximal vertex*} |
53 "Maximal == \<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i s. highest j s)}" |
56 "Maximal == \<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i s. highest j s)}" |
54 |
57 |
55 Maximal' :: "state set" |
58 Maximal' :: "state set" |
|
59 --{* Maximal vertex: equivalent definition*} |
56 "Maximal' == \<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j)" |
60 "Maximal' == \<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j)" |
57 |
61 |
58 |
62 |
59 Safety :: "state set" |
63 Safety :: "state set" |
60 "Safety == \<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)}" |
64 "Safety == \<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)}" |
76 |
80 |
77 |
81 |
78 |
82 |
79 subsection{*Component correctness proofs*} |
83 subsection{*Component correctness proofs*} |
80 |
84 |
81 (* neighbors is stable *) |
85 text{* neighbors is stable *} |
82 lemma Component_neighbors_stable: "Component i \<in> stable {s. neighbors k s = n}" |
86 lemma Component_neighbors_stable: "Component i \<in> stable {s. neighbors k s = n}" |
83 by (simp add: Component_def, constrains, auto) |
87 by (simp add: Component_def, constrains, auto) |
84 |
88 |
85 (* property 4 *) |
89 text{* property 4 *} |
86 lemma Component_waits_priority: "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}" |
90 lemma Component_waits_priority: "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}" |
87 by (simp add: Component_def, constrains) |
91 by (simp add: Component_def, constrains) |
88 |
92 |
89 (* property 5: charpentier and Chandy mistakenly express it as |
93 text{* property 5: charpentier and Chandy mistakenly express it as |
90 'transient Highest i'. Consider the case where i has neighbors *) |
94 'transient Highest i'. Consider the case where i has neighbors *} |
91 lemma Component_yields_priority: |
95 lemma Component_yields_priority: |
92 "Component i: {s. neighbors i s \<noteq> {}} Int Highest i |
96 "Component i: {s. neighbors i s \<noteq> {}} Int Highest i |
93 ensures - Highest i" |
97 ensures - Highest i" |
94 apply (simp add: Component_def) |
98 apply (simp add: Component_def) |
95 apply (ensures_tac "act i", blast+) |
99 apply (ensures_tac "act i", blast+) |
96 done |
100 done |
97 |
101 |
98 (* or better *) |
102 text{* or better *} |
99 lemma Component_yields_priority': "Component i \<in> Highest i ensures Lowest i" |
103 lemma Component_yields_priority': "Component i \<in> Highest i ensures Lowest i" |
100 apply (simp add: Component_def) |
104 apply (simp add: Component_def) |
101 apply (ensures_tac "act i", blast+) |
105 apply (ensures_tac "act i", blast+) |
102 done |
106 done |
103 |
107 |
104 (* property 6: Component doesn't introduce cycle *) |
108 text{* property 6: Component doesn't introduce cycle *} |
105 lemma Component_well_behaves: "Component i \<in> Highest i co Highest i Un Lowest i" |
109 lemma Component_well_behaves: "Component i \<in> Highest i co Highest i Un Lowest i" |
106 by (simp add: Component_def, constrains, fast) |
110 by (simp add: Component_def, constrains, fast) |
107 |
111 |
108 (* property 7: local axiom *) |
112 text{* property 7: local axiom *} |
109 lemma locality: "Component i \<in> stable {s. \<forall>j k. j\<noteq>i & k\<noteq>i--> ((j,k):s) = b j k}" |
113 lemma locality: "Component i \<in> stable {s. \<forall>j k. j\<noteq>i & k\<noteq>i--> ((j,k):s) = b j k}" |
110 by (simp add: Component_def, constrains) |
114 by (simp add: Component_def, constrains) |
111 |
115 |
112 |
116 |
113 subsection{*System properties*} |
117 subsection{*System properties*} |
114 (* property 8: strictly universal *) |
118 text{* property 8: strictly universal *} |
115 |
119 |
116 lemma Safety: "system \<in> stable Safety" |
120 lemma Safety: "system \<in> stable Safety" |
117 apply (unfold Safety_def) |
121 apply (unfold Safety_def) |
118 apply (rule stable_INT) |
122 apply (rule stable_INT) |
119 apply (simp add: system_def, constrains, fast) |
123 apply (simp add: system_def, constrains, fast) |
120 done |
124 done |
121 |
125 |
122 (* property 13: universal *) |
126 text{* property 13: universal *} |
123 lemma p13: "system \<in> {s. s = q} co {s. s=q} Un {s. \<exists>i. derive i q s}" |
127 lemma p13: "system \<in> {s. s = q} co {s. s=q} Un {s. \<exists>i. derive i q s}" |
124 by (simp add: system_def Component_def mk_total_program_def totalize_JN, constrains, blast) |
128 by (simp add: system_def Component_def mk_total_program_def totalize_JN, constrains, blast) |
125 |
129 |
126 (* property 14: the 'above set' of a Component that hasn't got |
130 text{* property 14: the 'above set' of a Component that hasn't got |
127 priority doesn't increase *) |
131 priority doesn't increase *} |
128 lemma above_not_increase: |
132 lemma above_not_increase: |
129 "system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}" |
133 "system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}" |
130 apply (insert reach_lemma [of concl: j]) |
134 apply (insert reach_lemma [of concl: j]) |
131 apply (simp add: system_def Component_def mk_total_program_def totalize_JN, |
135 apply (simp add: system_def Component_def mk_total_program_def totalize_JN, |
132 constrains) |
136 constrains) |
167 lemma Acyclic_subset_Maximal: "Acyclic <= Maximal" |
171 lemma Acyclic_subset_Maximal: "Acyclic <= Maximal" |
168 apply (unfold Acyclic_def Maximal_def, clarify) |
172 apply (unfold Acyclic_def Maximal_def, clarify) |
169 apply (drule above_lemma_b, auto) |
173 apply (drule above_lemma_b, auto) |
170 done |
174 done |
171 |
175 |
172 (* property 17: original one is an invariant *) |
176 text{* property 17: original one is an invariant *} |
173 lemma Acyclic_Maximal_stable: "system \<in> stable (Acyclic Int Maximal)" |
177 lemma Acyclic_Maximal_stable: "system \<in> stable (Acyclic Int Maximal)" |
174 by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable) |
178 by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable) |
175 |
179 |
176 |
180 |
177 (* propert 5: existential property *) |
181 text{* property 5: existential property *} |
178 |
182 |
179 lemma Highest_leadsTo_Lowest: "system \<in> Highest i leadsTo Lowest i" |
183 lemma Highest_leadsTo_Lowest: "system \<in> Highest i leadsTo Lowest i" |
180 apply (simp add: system_def Component_def mk_total_program_def totalize_JN) |
184 apply (simp add: system_def Component_def mk_total_program_def totalize_JN) |
181 apply (ensures_tac "act i", auto) |
185 apply (ensures_tac "act i", auto) |
182 done |
186 done |
183 |
187 |
184 (* a lowest i can never be in any abover set *) |
188 text{* a lowest i can never be in any abover set *} |
185 lemma Lowest_above_subset: "Lowest i <= (\<Inter>k. {s. i\<notin>above k s})" |
189 lemma Lowest_above_subset: "Lowest i <= (\<Inter>k. {s. i\<notin>above k s})" |
186 by (auto simp add: image0_r_iff_image0_trancl trancl_converse) |
190 by (auto simp add: image0_r_iff_image0_trancl trancl_converse) |
187 |
191 |
188 (* property 18: a simpler proof than the original, one which uses psp *) |
192 text{* property 18: a simpler proof than the original, one which uses psp *} |
189 lemma Highest_escapes_above: "system \<in> Highest i leadsTo (\<Inter>k. {s. i\<notin>above k s})" |
193 lemma Highest_escapes_above: "system \<in> Highest i leadsTo (\<Inter>k. {s. i\<notin>above k s})" |
190 apply (rule leadsTo_weaken_R) |
194 apply (rule leadsTo_weaken_R) |
191 apply (rule_tac [2] Lowest_above_subset) |
195 apply (rule_tac [2] Lowest_above_subset) |
192 apply (rule Highest_leadsTo_Lowest) |
196 apply (rule Highest_leadsTo_Lowest) |
193 done |
197 done |
194 |
198 |
195 lemma Highest_escapes_above': |
199 lemma Highest_escapes_above': |
196 "system \<in> Highest j Int {s. j \<in> above i s} leadsTo {s. j\<notin>above i s}" |
200 "system \<in> Highest j Int {s. j \<in> above i s} leadsTo {s. j\<notin>above i s}" |
197 by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower]) |
201 by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower]) |
198 |
202 |
199 (*** The main result: above set decreases ***) |
203 subsection{*The main result: above set decreases*} |
200 (* The original proof of the following formula was wrong *) |
204 |
|
205 text{* The original proof of the following formula was wrong *} |
201 |
206 |
202 lemma Highest_iff_above0: "Highest i = {s. above i s ={}}" |
207 lemma Highest_iff_above0: "Highest i = {s. above i s ={}}" |
203 by (auto simp add: image0_trancl_iff_image0_r) |
208 by (auto simp add: image0_trancl_iff_image0_r) |
204 |
209 |
205 lemmas above_decreases_lemma = |
210 lemmas above_decreases_lemma = |