1 (* Title: HOL/UNITY/Priority |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 The priority system |
|
7 |
|
8 From Charpentier and Chandy, |
|
9 Examples of Program Composition Illustrating the Use of Universal Properties |
|
10 In J. Rolim (editor), Parallel and Distributed Processing, |
|
11 Spriner LNCS 1586 (1999), pages 1215-1227. |
|
12 *) |
|
13 |
|
14 Addsimps [Component_def RS def_prg_Init]; |
|
15 program_defs_ref := [Component_def, system_def]; |
|
16 Addsimps [highest_def, lowest_def]; |
|
17 Addsimps [simp_of_act act_def]; |
|
18 Addsimps (map simp_of_set [Highest_def, Lowest_def]); |
|
19 |
|
20 |
|
21 |
|
22 |
|
23 (**** Component correctness proofs ****) |
|
24 |
|
25 (* neighbors is stable *) |
|
26 Goal "Component i: stable {s. neighbors k s = n}"; |
|
27 by (constrains_tac 1); |
|
28 by Auto_tac; |
|
29 qed "Component_neighbors_stable"; |
|
30 |
|
31 (* property 4 *) |
|
32 Goal |
|
33 "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}"; |
|
34 by (constrains_tac 1); |
|
35 qed "Component_waits_priority"; |
|
36 |
|
37 (* property 5: charpentier and Chandy mistakenly express it as |
|
38 'transient Highest i'. Consider the case where i has neighbors *) |
|
39 Goal |
|
40 "Component i: {s. neighbors i s ~= {}} Int Highest i \ |
|
41 \ ensures - Highest i"; |
|
42 by (ensures_tac "act i" 1); |
|
43 by (REPEAT(Fast_tac 1)); |
|
44 qed "Component_yields_priority"; |
|
45 |
|
46 (* or better *) |
|
47 Goal "Component i: Highest i ensures Lowest i"; |
|
48 by (ensures_tac "act i" 1); |
|
49 by (REPEAT(Fast_tac 1)); |
|
50 qed "Component_yields_priority'"; |
|
51 |
|
52 (* property 6: Component doesn't introduce cycle *) |
|
53 Goal "Component i: Highest i co Highest i Un Lowest i"; |
|
54 by (constrains_tac 1); |
|
55 by (Fast_tac 1); |
|
56 qed "Component_well_behaves"; |
|
57 |
|
58 (* property 7: local axiom *) |
|
59 Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}"; |
|
60 by (constrains_tac 1); |
|
61 qed "locality"; |
|
62 |
|
63 |
|
64 (**** System properties ****) |
|
65 (* property 8: strictly universal *) |
|
66 |
|
67 Goalw [Safety_def] |
|
68 "system: stable Safety"; |
|
69 by (rtac stable_INT 1); |
|
70 by (constrains_tac 1); |
|
71 by (Fast_tac 1); |
|
72 qed "Safety"; |
|
73 |
|
74 (* property 13: universal *) |
|
75 Goal |
|
76 "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}"; |
|
77 by (constrains_tac 1); |
|
78 by (Blast_tac 1); |
|
79 qed "p13"; |
|
80 |
|
81 (* property 14: the 'above set' of a Component that hasn't got |
|
82 priority doesn't increase *) |
|
83 Goal |
|
84 "ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}"; |
|
85 by (Clarify_tac 1); |
|
86 by (cut_inst_tac [("i", "j")] reach_lemma 1); |
|
87 by (constrains_tac 1); |
|
88 by (auto_tac (claset(), simpset() addsimps [trancl_converse])); |
|
89 qed "above_not_increase"; |
|
90 |
|
91 Goal |
|
92 "system: -Highest i Int {s. above i s = x} co {s. above i s <= x}"; |
|
93 by (cut_inst_tac [("i", "i")] above_not_increase 1); |
|
94 by (asm_full_simp_tac (simpset() addsimps |
|
95 [trancl_converse, constrains_def]) 1); |
|
96 by (Blast_tac 1); |
|
97 qed "above_not_increase'"; |
|
98 |
|
99 |
|
100 |
|
101 (* p15: universal property: all Components well behave *) |
|
102 Goal "ALL i. system: Highest i co Highest i Un Lowest i"; |
|
103 by (Clarify_tac 1); |
|
104 by (constrains_tac 1); |
|
105 by Auto_tac; |
|
106 qed "system_well_behaves"; |
|
107 |
|
108 |
|
109 Goal "Acyclic = (INT i. {s. i~:above i s})"; |
|
110 by (auto_tac (claset(), simpset() |
|
111 addsimps [Acyclic_def, acyclic_def, trancl_converse])); |
|
112 qed "Acyclic_eq"; |
|
113 |
|
114 |
|
115 val lemma = [above_not_increase RS spec, |
|
116 system_well_behaves RS spec] MRS constrains_Un; |
|
117 Goal |
|
118 "system: stable Acyclic"; |
|
119 by (auto_tac (claset() addSIs [stable_INT, stableI, |
|
120 lemma RS constrains_weaken], |
|
121 simpset() addsimps [Acyclic_eq, |
|
122 image0_r_iff_image0_trancl,trancl_converse])); |
|
123 qed "Acyclic_stable"; |
|
124 |
|
125 |
|
126 Goalw [Acyclic_def, Maximal_def] |
|
127 "Acyclic <= Maximal"; |
|
128 by (Clarify_tac 1); |
|
129 by (dtac above_lemma_b 1); |
|
130 by Auto_tac; |
|
131 qed "Acyclic_subset_Maximal"; |
|
132 |
|
133 (* property 17: original one is an invariant *) |
|
134 Goal |
|
135 "system: stable (Acyclic Int Maximal)"; |
|
136 by (simp_tac (simpset() addsimps |
|
137 [Acyclic_subset_Maximal RS Int_absorb2, Acyclic_stable]) 1); |
|
138 qed "Acyclic_Maximal_stable"; |
|
139 |
|
140 |
|
141 (* propert 5: existential property *) |
|
142 |
|
143 Goal "system: Highest i leadsTo Lowest i"; |
|
144 by (ensures_tac "act i" 1); |
|
145 by (auto_tac (claset(), simpset() addsimps [Component_def])); |
|
146 qed "Highest_leadsTo_Lowest"; |
|
147 |
|
148 (* a lowest i can never be in any abover set *) |
|
149 Goal "Lowest i <= (INT k. {s. i~:above k s})"; |
|
150 by (auto_tac (claset(), |
|
151 simpset() addsimps [image0_r_iff_image0_trancl, trancl_converse])); |
|
152 qed "Lowest_above_subset"; |
|
153 |
|
154 (* property 18: a simpler proof than the original, one which uses psp *) |
|
155 Goal "system: Highest i leadsTo (INT k. {s. i~:above k s})"; |
|
156 by (rtac leadsTo_weaken_R 1); |
|
157 by (rtac Lowest_above_subset 2); |
|
158 by (rtac Highest_leadsTo_Lowest 1); |
|
159 qed "Highest_escapes_above"; |
|
160 |
|
161 Goal |
|
162 "system: Highest j Int {s. j:above i s} leadsTo {s. j~:above i s}"; |
|
163 by (blast_tac (claset() addIs |
|
164 [[Highest_escapes_above, Int_lower1, INT_lower] MRS leadsTo_weaken]) 1); |
|
165 qed "Highest_escapes_above'"; |
|
166 |
|
167 (*** The main result: above set decreases ***) |
|
168 (* The original proof of the following formula was wrong *) |
|
169 val above_decreases_lemma = |
|
170 [Highest_escapes_above', above_not_increase'] MRS psp RS leadsTo_weaken; |
|
171 |
|
172 Goal "Highest i = {s. above i s ={}}"; |
|
173 by (auto_tac (claset(), |
|
174 simpset() addsimps [image0_trancl_iff_image0_r])); |
|
175 qed "Highest_iff_above0"; |
|
176 |
|
177 |
|
178 Goal |
|
179 "system: (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j) \ |
|
180 \ leadsTo {s. above i s < x}"; |
|
181 by (rtac leadsTo_UN 1); |
|
182 by (rtac single_leadsTo_I 1); |
|
183 by (Clarify_tac 1); |
|
184 by (res_inst_tac [("x2", "above i x")] above_decreases_lemma 1); |
|
185 by (ALLGOALS(full_simp_tac (simpset() delsimps [Highest_def] |
|
186 addsimps [Highest_iff_above0]))); |
|
187 by (REPEAT(Blast_tac 1)); |
|
188 qed "above_decreases"; |
|
189 |
|
190 (** Just a massage of conditions to have the desired form ***) |
|
191 Goalw [Maximal_def, Maximal'_def, Highest_def] |
|
192 "Maximal = Maximal'"; |
|
193 by (Blast_tac 1); |
|
194 qed "Maximal_eq_Maximal'"; |
|
195 |
|
196 Goal "x~={} ==> \ |
|
197 \ Acyclic Int {s. above i s = x} <= \ |
|
198 \ (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j)"; |
|
199 by (res_inst_tac [("B", "Maximal' Int {s. above i s = x}")] subset_trans 1); |
|
200 by (simp_tac (simpset() addsimps [Maximal_eq_Maximal' RS sym]) 1); |
|
201 by (blast_tac (claset() addIs [Acyclic_subset_Maximal RS subsetD]) 1); |
|
202 by (simp_tac (simpset() delsimps [above_def] addsimps [Maximal'_def, Highest_iff_above0]) 1); |
|
203 by (Blast_tac 1); |
|
204 qed "Acyclic_subset"; |
|
205 |
|
206 val above_decreases' = [above_decreases, Acyclic_subset] MRS leadsTo_weaken_L; |
|
207 val above_decreases_psp = [above_decreases', Acyclic_stable] MRS psp_stable; |
|
208 |
|
209 Goal |
|
210 "x~={}==> \ |
|
211 \ system: Acyclic Int {s. above i s = x} leadsTo Acyclic Int {s. above i s < x}"; |
|
212 by (etac (above_decreases_psp RS leadsTo_weaken) 1); |
|
213 by (Blast_tac 1); |
|
214 by Auto_tac; |
|
215 qed "above_decreases_psp'"; |
|
216 |
|
217 |
|
218 val finite_psubset_induct = wf_finite_psubset RS leadsTo_wf_induct; |
|
219 val leadsTo_weaken_L' = rotate_prems 1 leadsTo_weaken_L; |
|
220 |
|
221 |
|
222 Goal "system: Acyclic leadsTo Highest i"; |
|
223 by (res_inst_tac [("f", "%s. above i s")] finite_psubset_induct 1); |
|
224 by (asm_simp_tac (simpset() delsimps [Highest_def, above_def] |
|
225 addsimps [Highest_iff_above0, |
|
226 vimage_def, finite_psubset_def]) 1); |
|
227 by (Clarify_tac 1); |
|
228 by (case_tac "m={}" 1); |
|
229 by (rtac (Int_lower2 RS leadsTo_weaken_L') 1); |
|
230 by (force_tac (claset(), simpset() addsimps [leadsTo_refl]) 1); |
|
231 by (res_inst_tac [("A'", "Acyclic Int {x. above i x < m}")] |
|
232 leadsTo_weaken_R 1); |
|
233 by (REPEAT(blast_tac (claset() addIs [above_decreases_psp']) 1)); |
|
234 qed "Progress"; |
|
235 |
|
236 (* We have proved all (relevant) theorems given in the paper *) |
|
237 (* We didn't assume any thing about the relation r *) |
|
238 (* It is not necessary that r be a priority relation as assumed in the original proof *) |
|
239 (* It suffices that we start from a state which is finite and acyclic *) |
|