4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 The Lift-Control Example |
6 The Lift-Control Example |
7 *) |
7 *) |
8 |
8 |
9 Lift = SubstAx + |
9 theory Lift = UNITY_Main: |
10 |
10 |
11 record state = |
11 record state = |
12 floor :: int (*current position of the lift*) |
12 floor :: "int" (*current position of the lift*) |
13 open :: bool (*whether the door is open at floor*) |
13 "open" :: "bool" (*whether the door is opened at floor*) |
14 stop :: bool (*whether the lift is stopped at floor*) |
14 stop :: "bool" (*whether the lift is stopped at floor*) |
15 req :: int set (*for each floor, whether the lift is requested*) |
15 req :: "int set" (*for each floor, whether the lift is requested*) |
16 up :: bool (*current direction of movement*) |
16 up :: "bool" (*current direction of movement*) |
17 move :: bool (*whether moving takes precedence over opening*) |
17 move :: "bool" (*whether moving takes precedence over opening*) |
18 |
18 |
19 consts |
19 consts |
20 Min, Max :: int (*least and greatest floors*) |
20 Min :: "int" (*least and greatest floors*) |
21 |
21 Max :: "int" (*least and greatest floors*) |
22 rules |
22 |
23 Min_le_Max "Min <= Max" |
23 axioms |
|
24 Min_le_Max [iff]: "Min <= Max" |
24 |
25 |
25 constdefs |
26 constdefs |
26 |
27 |
27 (** Abbreviations: the "always" part **) |
28 (** Abbreviations: the "always" part **) |
28 |
29 |
29 above :: state set |
30 above :: "state set" |
30 "above == {s. EX i. floor s < i & i <= Max & i : req s}" |
31 "above == {s. EX i. floor s < i & i <= Max & i : req s}" |
31 |
32 |
32 below :: state set |
33 below :: "state set" |
33 "below == {s. EX i. Min <= i & i < floor s & i : req s}" |
34 "below == {s. EX i. Min <= i & i < floor s & i : req s}" |
34 |
35 |
35 queueing :: state set |
36 queueing :: "state set" |
36 "queueing == above Un below" |
37 "queueing == above Un below" |
37 |
38 |
38 goingup :: state set |
39 goingup :: "state set" |
39 "goingup == above Int ({s. up s} Un -below)" |
40 "goingup == above Int ({s. up s} Un -below)" |
40 |
41 |
41 goingdown :: state set |
42 goingdown :: "state set" |
42 "goingdown == below Int ({s. ~ up s} Un -above)" |
43 "goingdown == below Int ({s. ~ up s} Un -above)" |
43 |
44 |
44 ready :: state set |
45 ready :: "state set" |
45 "ready == {s. stop s & ~ open s & move s}" |
46 "ready == {s. stop s & ~ open s & move s}" |
46 |
|
47 |
47 |
48 (** Further abbreviations **) |
48 (** Further abbreviations **) |
49 |
49 |
50 moving :: state set |
50 moving :: "state set" |
51 "moving == {s. ~ stop s & ~ open s}" |
51 "moving == {s. ~ stop s & ~ open s}" |
52 |
52 |
53 stopped :: state set |
53 stopped :: "state set" |
54 "stopped == {s. stop s & ~ open s & ~ move s}" |
54 "stopped == {s. stop s & ~ open s & ~ move s}" |
55 |
55 |
56 opened :: state set |
56 opened :: "state set" |
57 "opened == {s. stop s & open s & move s}" |
57 "opened == {s. stop s & open s & move s}" |
58 |
58 |
59 closed :: state set (*but this is the same as ready!!*) |
59 closed :: "state set" (*but this is the same as ready!!*) |
60 "closed == {s. stop s & ~ open s & move s}" |
60 "closed == {s. stop s & ~ open s & move s}" |
61 |
61 |
62 atFloor :: int => state set |
62 atFloor :: "int => state set" |
63 "atFloor n == {s. floor s = n}" |
63 "atFloor n == {s. floor s = n}" |
64 |
64 |
65 Req :: int => state set |
65 Req :: "int => state set" |
66 "Req n == {s. n : req s}" |
66 "Req n == {s. n : req s}" |
67 |
67 |
68 |
68 |
69 |
69 |
70 (** The program **) |
70 (** The program **) |
116 "button_press == |
116 "button_press == |
117 {(s,s'). EX n. s' = s (|req := insert n (req s)|) |
117 {(s,s'). EX n. s' = s (|req := insert n (req s)|) |
118 & Min <= n & n <= Max}" |
118 & Min <= n & n <= Max}" |
119 |
119 |
120 |
120 |
121 Lift :: state program |
121 Lift :: "state program" |
122 (*for the moment, we OMIT button_press*) |
122 (*for the moment, we OMIT button_press*) |
123 "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s & |
123 "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s & |
124 ~ open s & req s = {}}, |
124 ~ open s & req s = {}}, |
125 {request_act, open_act, close_act, |
125 {request_act, open_act, close_act, |
126 req_up, req_down, move_up, move_down}, |
126 req_up, req_down, move_up, move_down}, |
127 UNIV)" |
127 UNIV)" |
128 |
128 |
129 |
129 |
130 (** Invariants **) |
130 (** Invariants **) |
131 |
131 |
132 bounded :: state set |
132 bounded :: "state set" |
133 "bounded == {s. Min <= floor s & floor s <= Max}" |
133 "bounded == {s. Min <= floor s & floor s <= Max}" |
134 |
134 |
135 open_stop :: state set |
135 open_stop :: "state set" |
136 "open_stop == {s. open s --> stop s}" |
136 "open_stop == {s. open s --> stop s}" |
137 |
137 |
138 open_move :: state set |
138 open_move :: "state set" |
139 "open_move == {s. open s --> move s}" |
139 "open_move == {s. open s --> move s}" |
140 |
140 |
141 stop_floor :: state set |
141 stop_floor :: "state set" |
142 "stop_floor == {s. stop s & ~ move s --> floor s : req s}" |
142 "stop_floor == {s. stop s & ~ move s --> floor s : req s}" |
143 |
143 |
144 moving_up :: state set |
144 moving_up :: "state set" |
145 "moving_up == {s. ~ stop s & up s --> |
145 "moving_up == {s. ~ stop s & up s --> |
146 (EX f. floor s <= f & f <= Max & f : req s)}" |
146 (EX f. floor s <= f & f <= Max & f : req s)}" |
147 |
147 |
148 moving_down :: state set |
148 moving_down :: "state set" |
149 "moving_down == {s. ~ stop s & ~ up s --> |
149 "moving_down == {s. ~ stop s & ~ up s --> |
150 (EX f. Min <= f & f <= floor s & f : req s)}" |
150 (EX f. Min <= f & f <= floor s & f : req s)}" |
151 |
151 |
152 metric :: [int,state] => int |
152 metric :: "[int,state] => int" |
153 "metric == |
153 "metric == |
154 %n s. if floor s < n then (if up s then n - floor s |
154 %n s. if floor s < n then (if up s then n - floor s |
155 else (floor s - Min) + (n-Min)) |
155 else (floor s - Min) + (n-Min)) |
156 else |
156 else |
157 if n < floor s then (if up s then (Max - floor s) + (Max-n) |
157 if n < floor s then (if up s then (Max - floor s) + (Max-n) |
158 else floor s - n) |
158 else floor s - n) |
159 else 0" |
159 else 0" |
160 |
160 |
161 locale floor = |
161 locale Floor = |
162 fixes |
162 fixes n |
163 n :: int |
163 assumes Min_le_n [iff]: "Min <= n" |
164 assumes |
164 and n_le_Max [iff]: "n <= Max" |
165 Min_le_n "Min <= n" |
165 |
166 n_le_Max "n <= Max" |
166 lemma not_mem_distinct: "[| x ~: A; y : A |] ==> x ~= y" |
167 defines |
167 by blast |
|
168 |
|
169 |
|
170 declare Lift_def [THEN def_prg_Init, simp] |
|
171 |
|
172 declare request_act_def [THEN def_act_simp, simp] |
|
173 declare open_act_def [THEN def_act_simp, simp] |
|
174 declare close_act_def [THEN def_act_simp, simp] |
|
175 declare req_up_def [THEN def_act_simp, simp] |
|
176 declare req_down_def [THEN def_act_simp, simp] |
|
177 declare move_up_def [THEN def_act_simp, simp] |
|
178 declare move_down_def [THEN def_act_simp, simp] |
|
179 declare button_press_def [THEN def_act_simp, simp] |
|
180 |
|
181 (*The ALWAYS properties*) |
|
182 declare above_def [THEN def_set_simp, simp] |
|
183 declare below_def [THEN def_set_simp, simp] |
|
184 declare queueing_def [THEN def_set_simp, simp] |
|
185 declare goingup_def [THEN def_set_simp, simp] |
|
186 declare goingdown_def [THEN def_set_simp, simp] |
|
187 declare ready_def [THEN def_set_simp, simp] |
|
188 |
|
189 (*Basic definitions*) |
|
190 declare bounded_def [simp] |
|
191 open_stop_def [simp] |
|
192 open_move_def [simp] |
|
193 stop_floor_def [simp] |
|
194 moving_up_def [simp] |
|
195 moving_down_def [simp] |
|
196 |
|
197 lemma open_stop: "Lift : Always open_stop" |
|
198 apply (rule AlwaysI, force) |
|
199 apply (unfold Lift_def, constrains) |
|
200 done |
|
201 |
|
202 lemma stop_floor: "Lift : Always stop_floor" |
|
203 apply (rule AlwaysI, force) |
|
204 apply (unfold Lift_def, constrains) |
|
205 done |
|
206 |
|
207 (*This one needs open_stop, which was proved above*) |
|
208 lemma open_move: "Lift : Always open_move" |
|
209 apply (cut_tac open_stop) |
|
210 apply (rule AlwaysI, force) |
|
211 apply (unfold Lift_def, constrains) |
|
212 done |
|
213 |
|
214 lemma moving_up: "Lift : Always moving_up" |
|
215 apply (rule AlwaysI, force) |
|
216 apply (unfold Lift_def, constrains) |
|
217 apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq) |
|
218 done |
|
219 |
|
220 lemma moving_down: "Lift : Always moving_down" |
|
221 apply (rule AlwaysI, force) |
|
222 apply (unfold Lift_def, constrains) |
|
223 apply (blast dest: zle_imp_zless_or_eq) |
|
224 done |
|
225 |
|
226 lemma bounded: "Lift : Always bounded" |
|
227 apply (cut_tac moving_up moving_down) |
|
228 apply (rule AlwaysI, force) |
|
229 apply (unfold Lift_def, constrains, auto) |
|
230 apply (drule not_mem_distinct, assumption, arith)+ |
|
231 done |
|
232 |
|
233 |
|
234 subsection{*Progress*} |
|
235 |
|
236 declare moving_def [THEN def_set_simp, simp] |
|
237 declare stopped_def [THEN def_set_simp, simp] |
|
238 declare opened_def [THEN def_set_simp, simp] |
|
239 declare closed_def [THEN def_set_simp, simp] |
|
240 declare atFloor_def [THEN def_set_simp, simp] |
|
241 declare Req_def [THEN def_set_simp, simp] |
|
242 |
|
243 |
|
244 (** The HUG'93 paper mistakenly omits the Req n from these! **) |
|
245 |
|
246 (** Lift_1 **) |
|
247 lemma E_thm01: "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)" |
|
248 apply (cut_tac stop_floor) |
|
249 apply (unfold Lift_def, ensures_tac "open_act") |
|
250 done (*lem_lift_1_5*) |
|
251 |
|
252 lemma E_thm02: "Lift : (Req n Int stopped - atFloor n) LeadsTo |
|
253 (Req n Int opened - atFloor n)" |
|
254 apply (cut_tac stop_floor) |
|
255 apply (unfold Lift_def, ensures_tac "open_act") |
|
256 done (*lem_lift_1_1*) |
|
257 |
|
258 lemma E_thm03: "Lift : (Req n Int opened - atFloor n) LeadsTo |
|
259 (Req n Int closed - (atFloor n - queueing))" |
|
260 apply (unfold Lift_def, ensures_tac "close_act") |
|
261 done (*lem_lift_1_2*) |
|
262 |
|
263 lemma E_thm04: "Lift : (Req n Int closed Int (atFloor n - queueing)) |
|
264 LeadsTo (opened Int atFloor n)" |
|
265 apply (unfold Lift_def, ensures_tac "open_act") |
|
266 done (*lem_lift_1_7*) |
|
267 |
|
268 |
|
269 (** Lift 2. Statements of thm05a and thm05b were wrong! **) |
|
270 |
|
271 lemmas linorder_leI = linorder_not_less [THEN iffD1] |
|
272 |
|
273 lemmas (in Floor) le_MinD = Min_le_n [THEN order_antisym] |
|
274 and Max_leD = n_le_Max [THEN [2] order_antisym] |
|
275 |
|
276 declare (in Floor) le_MinD [dest!] |
|
277 and linorder_leI [THEN le_MinD, dest!] |
|
278 and Max_leD [dest!] |
|
279 and linorder_leI [THEN Max_leD, dest!] |
|
280 |
|
281 |
|
282 (*lem_lift_2_0 |
|
283 NOT an ensures_tac property, but a mere inclusion |
|
284 don't know why script lift_2.uni says ENSURES*) |
|
285 lemma (in Floor) E_thm05c: |
|
286 "Lift : (Req n Int closed - (atFloor n - queueing)) |
|
287 LeadsTo ((closed Int goingup Int Req n) Un |
|
288 (closed Int goingdown Int Req n))" |
|
289 by (auto intro!: subset_imp_LeadsTo elim!: int_neqE) |
|
290 |
|
291 (*lift_2*) |
|
292 lemma (in Floor) lift_2: "Lift : (Req n Int closed - (atFloor n - queueing)) |
|
293 LeadsTo (moving Int Req n)" |
|
294 apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un]) |
|
295 apply (unfold Lift_def) |
|
296 apply (ensures_tac [2] "req_down") |
|
297 apply (ensures_tac "req_up", auto) |
|
298 done |
|
299 |
|
300 |
|
301 (** Towards lift_4 ***) |
|
302 |
|
303 declare split_if_asm [split] |
|
304 |
|
305 |
|
306 (*lem_lift_4_1 *) |
|
307 lemma (in Floor) E_thm12a: |
|
308 "0 < N ==> |
|
309 Lift : (moving Int Req n Int {s. metric n s = N} Int |
|
310 {s. floor s ~: req s} Int {s. up s}) |
|
311 LeadsTo |
|
312 (moving Int Req n Int {s. metric n s < N})" |
|
313 apply (cut_tac moving_up) |
|
314 apply (unfold Lift_def, ensures_tac "move_up", safe) |
|
315 (*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
|
316 apply (erule linorder_leI [THEN order_antisym, symmetric]) |
|
317 apply (auto simp add: metric_def) |
|
318 done |
|
319 |
|
320 |
|
321 (*lem_lift_4_3 *) |
|
322 lemma (in Floor) E_thm12b: "0 < N ==> |
|
323 Lift : (moving Int Req n Int {s. metric n s = N} Int |
|
324 {s. floor s ~: req s} - {s. up s}) |
|
325 LeadsTo (moving Int Req n Int {s. metric n s < N})" |
|
326 apply (cut_tac moving_down) |
|
327 apply (unfold Lift_def, ensures_tac "move_down", safe) |
|
328 (*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
|
329 apply (erule linorder_leI [THEN order_antisym, symmetric]) |
|
330 apply (auto simp add: metric_def) |
|
331 done |
|
332 |
|
333 (*lift_4*) |
|
334 lemma (in Floor) lift_4: |
|
335 "0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int |
|
336 {s. floor s ~: req s}) LeadsTo |
|
337 (moving Int Req n Int {s. metric n s < N})" |
|
338 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo |
|
339 LeadsTo_Un [OF E_thm12a E_thm12b]], auto) |
|
340 done |
|
341 |
|
342 |
|
343 (** towards lift_5 **) |
|
344 |
|
345 (*lem_lift_5_3*) |
|
346 lemma (in Floor) E_thm16a: "0<N |
|
347 ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo |
|
348 (moving Int Req n Int {s. metric n s < N})" |
|
349 apply (cut_tac bounded) |
|
350 apply (unfold Lift_def, ensures_tac "req_up") |
|
351 apply (auto simp add: metric_def) |
|
352 done |
|
353 |
|
354 |
|
355 (*lem_lift_5_1 has ~goingup instead of goingdown*) |
|
356 lemma (in Floor) E_thm16b: "0<N ==> |
|
357 Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo |
|
358 (moving Int Req n Int {s. metric n s < N})" |
|
359 apply (cut_tac bounded) |
|
360 apply (unfold Lift_def, ensures_tac "req_down") |
|
361 apply (auto simp add: metric_def) |
|
362 done |
|
363 |
|
364 |
|
365 (*lem_lift_5_0 proves an intersection involving ~goingup and goingup, |
|
366 i.e. the trivial disjunction, leading to an asymmetrical proof.*) |
|
367 lemma (in Floor) E_thm16c: |
|
368 "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown" |
|
369 by (force simp add: metric_def) |
|
370 |
|
371 |
|
372 (*lift_5*) |
|
373 lemma (in Floor) lift_5: |
|
374 "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo |
|
375 (moving Int Req n Int {s. metric n s < N})" |
|
376 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo |
|
377 LeadsTo_Un [OF E_thm16a E_thm16b]]) |
|
378 apply (drule E_thm16c, auto) |
|
379 done |
|
380 |
|
381 |
|
382 (** towards lift_3 **) |
|
383 |
|
384 (*lemma used to prove lem_lift_3_1*) |
|
385 lemma (in Floor) metric_eq_0D [dest]: |
|
386 "[| metric n s = 0; Min <= floor s; floor s <= Max |] ==> floor s = n" |
|
387 by (force simp add: metric_def) |
|
388 |
|
389 |
|
390 (*lem_lift_3_1*) |
|
391 lemma (in Floor) E_thm11: "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo |
|
392 (stopped Int atFloor n)" |
|
393 apply (cut_tac bounded) |
|
394 apply (unfold Lift_def, ensures_tac "request_act", auto) |
|
395 done |
|
396 |
|
397 (*lem_lift_3_5*) |
|
398 lemma (in Floor) E_thm13: |
|
399 "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) |
|
400 LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})" |
|
401 apply (unfold Lift_def, ensures_tac "request_act") |
|
402 apply (auto simp add: metric_def) |
|
403 done |
|
404 |
|
405 (*lem_lift_3_6*) |
|
406 lemma (in Floor) E_thm14: "0 < N ==> |
|
407 Lift : |
|
408 (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) |
|
409 LeadsTo (opened Int Req n Int {s. metric n s = N})" |
|
410 apply (unfold Lift_def, ensures_tac "open_act") |
|
411 apply (auto simp add: metric_def) |
|
412 done |
|
413 |
|
414 (*lem_lift_3_7*) |
|
415 lemma (in Floor) E_thm15: "Lift : (opened Int Req n Int {s. metric n s = N}) |
|
416 LeadsTo (closed Int Req n Int {s. metric n s = N})" |
|
417 apply (unfold Lift_def, ensures_tac "close_act") |
|
418 apply (auto simp add: metric_def) |
|
419 done |
|
420 |
|
421 |
|
422 (** the final steps **) |
|
423 |
|
424 lemma (in Floor) lift_3_Req: "0 < N ==> |
|
425 Lift : |
|
426 (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) |
|
427 LeadsTo (moving Int Req n Int {s. metric n s < N})" |
|
428 apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans) |
|
429 done |
|
430 |
|
431 |
|
432 (*Now we observe that our integer metric is really a natural number*) |
|
433 lemma (in Floor) Always_nonneg: "Lift : Always {s. 0 <= metric n s}" |
|
434 apply (rule bounded [THEN Always_weaken]) |
|
435 apply (auto simp add: metric_def) |
|
436 done |
|
437 |
|
438 lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11] |
|
439 |
|
440 lemma (in Floor) lift_3: |
|
441 "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)" |
|
442 apply (rule Always_nonneg [THEN integ_0_le_induct]) |
|
443 apply (case_tac "0 < z") |
|
444 (*If z <= 0 then actually z = 0*) |
|
445 prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less) |
|
446 apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1]) |
|
447 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo |
|
448 LeadsTo_Un [OF lift_4 lift_3_Req]], auto) |
|
449 done |
|
450 |
|
451 |
|
452 lemma (in Floor) lift_1: "Lift : (Req n) LeadsTo (opened Int atFloor n)" |
|
453 apply (rule LeadsTo_Trans) |
|
454 prefer 2 |
|
455 apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post]) |
|
456 apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un]) |
|
457 apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un]) |
|
458 apply (rule lift_2 [THEN [2] LeadsTo_Trans_Un]) |
|
459 apply (rule LeadsTo_Trans_Un [OF E_thm02 E_thm03]) |
|
460 apply (rule open_move [THEN Always_LeadsToI]) |
|
461 apply (rule Always_LeadsToI [OF open_stop subset_imp_LeadsTo], clarify) |
|
462 (*The case split is not essential but makes the proof much faster.*) |
|
463 apply (case_tac "open x", auto) |
|
464 done |
|
465 |
168 |
466 |
169 end |
467 end |