5 |
5 |
6 The Lift-Control Example |
6 The Lift-Control Example |
7 *) |
7 *) |
8 |
8 |
9 |
9 |
10 (*To move 0 < metric n s out of the assumptions for case splitting*) |
10 (*split_all_tac causes a big blow-up*) |
11 val rev_mp' = read_instantiate_sg (sign_of thy) |
11 claset_ref() := claset() delSWrapper "split_all_tac"; |
12 [("P", "0 < metric ?n ?s")] rev_mp; |
12 |
|
13 |
|
14 (** Rules to move "metric n s" out of the assumptions, for case splitting **) |
|
15 val mov_metric1 = read_instantiate_sg (sign_of thy) |
|
16 [("P", "?x < metric ?n ?s")] rev_mp; |
|
17 |
|
18 val mov_metric2 = read_instantiate_sg (sign_of thy) |
|
19 [("P", "?x = metric ?n ?s")] rev_mp; |
|
20 |
|
21 val mov_metric3 = read_instantiate_sg (sign_of thy) |
|
22 [("P", "~ (?x < metric ?n ?s)")] rev_mp; |
|
23 |
|
24 (*The order in which they are applied seems to be critical...*) |
|
25 val mov_metrics = [mov_metric2, mov_metric3, mov_metric1]; |
|
26 |
13 |
27 |
14 val Suc_lessD_contra = Suc_lessD COMP rev_contrapos; |
28 val Suc_lessD_contra = Suc_lessD COMP rev_contrapos; |
15 val Suc_lessD_contra' = less_not_sym RS Suc_lessD_contra; |
29 val Suc_lessD_contra' = less_not_sym RS Suc_lessD_contra; |
16 |
30 |
|
31 Addsimps [Lprg_def RS def_prg_simps]; |
|
32 |
|
33 Addsimps (map simp_of_act |
|
34 [request_act_def, open_act_def, close_act_def, |
|
35 req_up_def, req_down_def, move_up_def, move_down_def, |
|
36 button_press_def]); |
|
37 |
17 val always_defs = [above_def, below_def, queueing_def, |
38 val always_defs = [above_def, below_def, queueing_def, |
18 goingup_def, goingdown_def, ready_def]; |
39 goingup_def, goingdown_def, ready_def]; |
19 |
40 |
20 val cmd_defs = [Lprg_def, |
41 Addsimps (map simp_of_set always_defs); |
21 request_act_def, open_act_def, close_act_def, |
|
22 req_up_def, req_down_def, move_up_def, move_down_def, |
|
23 button_press_def]; |
|
24 |
42 |
25 Goalw [Lprg_def] "id : Acts Lprg"; |
43 Goalw [Lprg_def] "id : Acts Lprg"; |
26 by (Simp_tac 1); |
44 by (Simp_tac 1); |
27 qed "id_in_Acts"; |
45 qed "id_in_Acts"; |
28 AddIffs [id_in_Acts]; |
46 AddIffs [id_in_Acts]; |
38 not_less_less_Suc_eq, less_not_sym RS not_less_less_Suc_eq, |
56 not_less_less_Suc_eq, less_not_sym RS not_less_less_Suc_eq, |
39 Suc_lessD_contra, Suc_lessD_contra', |
57 Suc_lessD_contra, Suc_lessD_contra', |
40 less_not_refl2, less_not_refl3]; |
58 less_not_refl2, less_not_refl3]; |
41 |
59 |
42 |
60 |
43 |
61 (*Hoping to be faster than |
44 (*split_all_tac causes a big blow-up*) |
62 asm_simp_tac (simpset() addsimps metric_simps |
45 claset_ref() := claset() delSWrapper "split_all_tac"; |
63 but sometimes it's slower*) |
|
64 val metric_simp_tac = |
|
65 asm_simp_tac (simpset() addsimps [metric_def, vimage_def]) THEN' |
|
66 asm_simp_tac (simpset() addsimps metric_simps); |
|
67 |
46 |
68 |
47 (*Simplification for records*) |
69 (*Simplification for records*) |
48 Addsimps (thms"state.update_defs"); |
70 Addsimps (thms"state.update_defs"); |
49 |
71 |
50 Addsimps [Suc_le_eq]; |
72 Addsimps [Suc_le_eq]; |
63 |
85 |
64 Goal "m < n ==> m <= n-1"; |
86 Goal "m < n ==> m <= n-1"; |
65 by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1); |
87 by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1); |
66 qed "less_imp_le_pred"; |
88 qed "less_imp_le_pred"; |
67 |
89 |
68 Goalw [Lprg_def] "Invariant Lprg open_stop"; |
90 Goal "Invariant Lprg open_stop"; |
69 by (rtac InvariantI 1); |
91 by (rtac InvariantI 1); |
70 by (Force_tac 1); |
92 by (Force_tac 1); |
71 by (constrains_tac (cmd_defs@always_defs) 1); |
93 by (constrains_tac 1); |
72 qed "open_stop"; |
94 qed "open_stop"; |
73 |
95 |
74 Goalw [Lprg_def] "Invariant Lprg stop_floor"; |
96 Goal "Invariant Lprg stop_floor"; |
75 by (rtac InvariantI 1); |
97 by (rtac InvariantI 1); |
76 by (Force_tac 1); |
98 by (Force_tac 1); |
77 by (constrains_tac (cmd_defs@always_defs) 1); |
99 by (constrains_tac 1); |
78 qed "stop_floor"; |
100 qed "stop_floor"; |
79 |
101 |
80 (*This one needs open_stop, which was proved above*) |
102 (*This one needs open_stop, which was proved above*) |
81 Goal "Invariant Lprg open_move"; |
103 Goal "Invariant Lprg open_move"; |
82 by (rtac InvariantI 1); |
104 by (rtac InvariantI 1); |
83 br (open_stop RS Invariant_ConstrainsI RS StableI) 2; |
105 by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2); |
84 bw Lprg_def; |
106 by (Force_tac 1); |
85 by (Force_tac 1); |
107 by (constrains_tac 1); |
86 by (constrains_tac (cmd_defs@always_defs) 1); |
|
87 qed "open_move"; |
108 qed "open_move"; |
88 |
109 |
89 Goalw [Lprg_def] "Invariant Lprg moving_up"; |
110 Goal "Invariant Lprg moving_up"; |
90 by (rtac InvariantI 1); |
111 by (rtac InvariantI 1); |
91 by (Force_tac 1); |
112 by (Force_tac 1); |
92 by (constrains_tac (cmd_defs@always_defs) 1); |
113 by (constrains_tac 1); |
93 by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1); |
114 by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1); |
94 qed "moving_up"; |
115 qed "moving_up"; |
95 |
116 |
96 Goalw [Lprg_def] "Invariant Lprg moving_down"; |
117 Goal "Invariant Lprg moving_down"; |
97 by (rtac InvariantI 1); |
118 by (rtac InvariantI 1); |
98 by (Force_tac 1); |
119 by (Force_tac 1); |
99 by (constrains_tac (cmd_defs@always_defs) 1); |
120 by (constrains_tac 1); |
100 by Safe_tac; |
121 by Safe_tac; |
101 by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3); |
122 by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3); |
102 by (auto_tac (claset(), |
123 by (auto_tac (claset(), |
103 simpset() addsimps [gr_implies_gr0 RS le_pred_eq])); |
124 simpset() addsimps [gr_implies_gr0 RS le_pred_eq])); |
104 qed "moving_down"; |
125 qed "moving_down"; |
105 |
126 |
106 Goal "Invariant Lprg bounded"; |
127 Goal "Invariant Lprg bounded"; |
107 by (rtac InvariantI 1); |
128 by (rtac InvariantI 1); |
108 br (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2; |
129 by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2); |
109 bw Lprg_def; |
130 by (Force_tac 1); |
110 by (Force_tac 1); |
131 by (constrains_tac 1); |
111 by (constrains_tac (cmd_defs@always_defs) 1); |
|
112 by Safe_tac; |
132 by Safe_tac; |
113 by (TRYALL (resolve_tac [nat_exhaust_le_pred, nat_exhaust_pred_le])); |
133 by (TRYALL (resolve_tac [nat_exhaust_le_pred, nat_exhaust_pred_le])); |
114 by (auto_tac (claset(), simpset() addsimps [less_Suc_eq])); |
134 by (auto_tac (claset(), simpset() addsimps [less_Suc_eq])); |
115 by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, le_eq_less_or_eq])); |
135 by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, le_eq_less_or_eq])); |
116 qed "bounded"; |
136 qed "bounded"; |
121 |
141 |
122 |
142 |
123 val abbrev_defs = [moving_def, stopped_def, |
143 val abbrev_defs = [moving_def, stopped_def, |
124 opened_def, closed_def, atFloor_def, Req_def]; |
144 opened_def, closed_def, atFloor_def, Req_def]; |
125 |
145 |
126 val defs = cmd_defs@always_defs@abbrev_defs; |
146 Addsimps (map simp_of_set abbrev_defs); |
127 |
147 |
128 |
148 |
129 (** The HUG'93 paper mistakenly omits the Req n from these! **) |
149 (** The HUG'93 paper mistakenly omits the Req n from these! **) |
130 |
150 |
131 (** Lift_1 **) |
151 (** Lift_1 **) |
132 |
152 |
133 (*lem_lift_1_5*) |
|
134 Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)"; |
153 Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)"; |
135 by (cut_facts_tac [stop_floor] 1); |
154 by (cut_facts_tac [stop_floor] 1); |
136 by (ensures_tac defs "open_act" 1); |
155 by (ensures_tac "open_act" 1); |
137 by Auto_tac; |
156 qed "E_thm01"; (*lem_lift_1_5*) |
138 qed "E_thm01"; |
157 |
139 |
|
140 (*lem_lift_1_1*) |
|
141 Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \ |
158 Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \ |
142 \ (Req n Int opened - atFloor n)"; |
159 \ (Req n Int opened - atFloor n)"; |
143 by (cut_facts_tac [stop_floor] 1); |
160 by (cut_facts_tac [stop_floor] 1); |
144 by (ensures_tac defs "open_act" 1); |
161 by (ensures_tac "open_act" 1); |
145 by Auto_tac; |
162 qed "E_thm02"; (*lem_lift_1_1*) |
146 qed "E_thm02"; |
163 |
147 |
|
148 (*lem_lift_1_2*) |
|
149 Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \ |
164 Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \ |
150 \ (Req n Int closed - (atFloor n - queueing))"; |
165 \ (Req n Int closed - (atFloor n - queueing))"; |
151 by (ensures_tac defs "close_act" 1); |
166 by (ensures_tac "close_act" 1); |
152 by Auto_tac; |
167 qed "E_thm03"; (*lem_lift_1_2*) |
153 qed "E_thm03"; |
168 |
154 |
|
155 |
|
156 (*lem_lift_1_7*) |
|
157 Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \ |
169 Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \ |
158 \ (opened Int atFloor n)"; |
170 \ (opened Int atFloor n)"; |
159 by (ensures_tac defs "open_act" 1); |
171 by (ensures_tac "open_act" 1); |
160 by Auto_tac; |
172 qed "E_thm04"; (*lem_lift_1_7*) |
161 qed "E_thm04"; |
|
162 |
173 |
163 |
174 |
164 (** Lift 2. Statements of thm05a and thm05b were wrong! **) |
175 (** Lift 2. Statements of thm05a and thm05b were wrong! **) |
165 |
176 |
166 Open_locale "floor"; |
177 Open_locale "floor"; |
180 NOT an ensures property, but a mere inclusion; |
191 NOT an ensures property, but a mere inclusion; |
181 don't know why script lift_2.uni says ENSURES*) |
192 don't know why script lift_2.uni says ENSURES*) |
182 Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \ |
193 Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \ |
183 \ ((closed Int goingup Int Req n) Un \ |
194 \ ((closed Int goingup Int Req n) Un \ |
184 \ (closed Int goingdown Int Req n))"; |
195 \ (closed Int goingdown Int Req n))"; |
185 br subset_imp_LeadsTo 1; |
196 by (rtac subset_imp_LeadsTo 1); |
186 by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs)); |
197 by (auto_tac (claset() addSEs [nat_neqE], simpset())); |
187 qed "E_thm05c"; |
198 qed "E_thm05c"; |
188 |
199 |
189 (*lift_2*) |
200 (*lift_2*) |
190 Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \ |
201 Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \ |
191 \ (moving Int Req n)"; |
202 \ (moving Int Req n)"; |
192 br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1; |
203 by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
193 by (ensures_tac defs "req_down" 2); |
204 by (ensures_tac "req_down" 2); |
194 by (ensures_tac defs "req_up" 1); |
205 by (ensures_tac "req_up" 1); |
195 by Auto_tac; |
206 by Auto_tac; |
196 qed "lift_2"; |
207 qed "lift_2"; |
197 |
208 |
198 |
209 |
199 (** Towards lift_4 ***) |
210 (** Towards lift_4 ***) |
210 |
221 |
211 (*lem_lift_4_1 *) |
222 (*lem_lift_4_1 *) |
212 Goal "0 < N ==> \ |
223 Goal "0 < N ==> \ |
213 \ LeadsTo Lprg \ |
224 \ LeadsTo Lprg \ |
214 \ (moving Int Req n Int (metric n -`` {N}) Int \ |
225 \ (moving Int Req n Int (metric n -`` {N}) Int \ |
215 \ {s. floor s ~: req s} Int {s. up s}) \ |
226 \ {s. floor s ~: req s} Int {s. up s}) \ |
216 \ (moving Int Req n Int (metric n -`` lessThan N))"; |
227 \ (moving Int Req n Int (metric n -`` lessThan N))"; |
217 by (cut_facts_tac [moving_up] 1); |
228 by (cut_facts_tac [moving_up] 1); |
218 by (ensures_tac defs "move_up" 1); |
229 by (ensures_tac "move_up" 1); |
219 by Auto_tac; |
230 by Safe_tac; |
220 (*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
231 (*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
221 be (leI RS le_anti_sym RS sym) 1; |
232 by (etac (leI RS le_anti_sym RS sym) 1); |
222 by (eres_inst_tac [("P", "?x < metric n s")] notE 2); |
233 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
223 by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3); |
234 by (REPEAT_FIRST distinct_tac); |
224 by (REPEAT_FIRST (etac rev_mp')); |
235 by (ALLGOALS metric_simp_tac); |
225 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); |
|
226 by (distinct_tac 1); |
|
227 by (auto_tac |
236 by (auto_tac |
228 (claset() addEs [diff_Suc_less_diff RS less_not_refl3 RSN (2, rev_notE)] |
237 (claset() addEs [diff_Suc_less_diff RS less_not_refl3 RSN (2, rev_notE)] |
229 addIs [diff_Suc_less_diff], |
238 addIs [diff_Suc_less_diff], |
230 simpset())); |
239 simpset())); |
231 qed "E_thm12a"; |
240 qed "E_thm12a"; |
240 \ LeadsTo Lprg \ |
249 \ LeadsTo Lprg \ |
241 \ (moving Int Req n Int (metric n -`` {N}) Int \ |
250 \ (moving Int Req n Int (metric n -`` {N}) Int \ |
242 \ {s. floor s ~: req s} - {s. up s}) \ |
251 \ {s. floor s ~: req s} - {s. up s}) \ |
243 \ (moving Int Req n Int (metric n -`` lessThan N))"; |
252 \ (moving Int Req n Int (metric n -`` lessThan N))"; |
244 by (cut_facts_tac [moving_down] 1); |
253 by (cut_facts_tac [moving_down] 1); |
245 by (ensures_tac defs "move_down" 1); |
254 by (ensures_tac "move_down" 1); |
246 by Auto_tac; |
255 by Safe_tac; |
247 by (ALLGOALS distinct_tac); |
256 by (ALLGOALS distinct_tac); |
248 by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac)); |
257 by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac)); |
249 (*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
258 (*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
250 be (leI RS le_anti_sym RS sym) 1; |
259 by (etac (leI RS le_anti_sym RS sym) 1); |
251 by (eres_inst_tac [("P", "?x < metric n s")] notE 2); |
260 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
252 by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3); |
261 by (ALLGOALS metric_simp_tac); |
253 by (REPEAT_FIRST (etac rev_mp')); |
|
254 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); |
|
255 by (auto_tac |
262 by (auto_tac |
256 (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)] |
263 (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)] |
257 addIs [diff_le_Suc_diff, diff_less_Suc_diff], |
264 addIs [diff_le_Suc_diff, diff_less_Suc_diff], |
258 simpset() addsimps [trans_le_add1])); |
265 simpset() addsimps [trans_le_add1])); |
259 qed "E_thm12b"; |
266 qed "E_thm12b"; |
276 (*lem_lift_5_3*) |
283 (*lem_lift_5_3*) |
277 Goal "0<N \ |
284 Goal "0<N \ |
278 \ ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingup) \ |
285 \ ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingup) \ |
279 \ (moving Int Req n Int (metric n -`` lessThan N))"; |
286 \ (moving Int Req n Int (metric n -`` lessThan N))"; |
280 by (cut_facts_tac [bounded] 1); |
287 by (cut_facts_tac [bounded] 1); |
281 by (ensures_tac defs "req_up" 1); |
288 by (ensures_tac "req_up" 1); |
282 by Auto_tac; |
289 by Auto_tac; |
283 by (ALLGOALS (eres_inst_tac [("P", "?x < metric n s")] notE)); |
290 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
284 by (REPEAT_FIRST (etac rev_mp')); |
|
285 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); |
291 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); |
|
292 (*faster than metric_simp_tac or than using just metric_def*) |
286 by (auto_tac (claset() addIs [diff_Suc_less_diff], |
293 by (auto_tac (claset() addIs [diff_Suc_less_diff], |
287 simpset() addsimps [arith1, arith2])); |
294 simpset() addsimps [arith1, arith2])); |
288 qed "E_thm16a"; |
295 qed "E_thm16a"; |
289 |
296 |
290 (*arith1 comes from |
297 (*arith1 comes from |
309 (*lem_lift_5_1 has ~goingup instead of goingdown*) |
316 (*lem_lift_5_1 has ~goingup instead of goingdown*) |
310 Goal "0<N ==> \ |
317 Goal "0<N ==> \ |
311 \ LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingdown) \ |
318 \ LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingdown) \ |
312 \ (moving Int Req n Int (metric n -`` lessThan N))"; |
319 \ (moving Int Req n Int (metric n -`` lessThan N))"; |
313 by (cut_facts_tac [bounded] 1); |
320 by (cut_facts_tac [bounded] 1); |
314 by (ensures_tac defs "req_down" 1); |
321 by (ensures_tac "req_down" 1); |
315 by Auto_tac; |
322 by Auto_tac; |
316 by (ALLGOALS (eres_inst_tac [("P", "?x < metric n s")] notE)); |
|
317 by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac)); |
323 by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac)); |
318 by (REPEAT_FIRST (etac rev_mp')); |
324 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
319 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); |
325 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps))); |
|
326 (*faster and better than metric_simp_tac *) |
320 by (auto_tac (claset() addIs [diff_Suc_less_diff, diff_less_Suc_diff], |
327 by (auto_tac (claset() addIs [diff_Suc_less_diff, diff_less_Suc_diff], |
321 simpset() addsimps [trans_le_add1, arith3, arith4])); |
328 simpset() addsimps [trans_le_add1, arith3, arith4])); |
322 qed "E_thm16b"; |
329 qed "E_thm16b"; |
323 |
330 |
324 (*arith3 comes from |
331 (*arith3 comes from |
344 |
351 |
345 |
352 |
346 (*lem_lift_5_0 proves an intersection involving ~goingup and goingup, |
353 (*lem_lift_5_0 proves an intersection involving ~goingup and goingup, |
347 i.e. the trivial disjunction, leading to an asymmetrical proof.*) |
354 i.e. the trivial disjunction, leading to an asymmetrical proof.*) |
348 Goal "0<N ==> Req n Int (metric n -``{N}) <= goingup Un goingdown"; |
355 Goal "0<N ==> Req n Int (metric n -``{N}) <= goingup Un goingdown"; |
349 by (asm_simp_tac (simpset() addsimps (defs@metric_simps)) 1); |
356 by (asm_simp_tac |
350 by (Blast_tac 1); |
357 (simpset() addsimps (always_defs@abbrev_defs@[metric_def,vimage_def])) 1); |
|
358 by (auto_tac (claset(), simpset() addsimps metric_simps)); |
351 qed "E_thm16c"; |
359 qed "E_thm16c"; |
352 |
360 |
353 |
361 |
354 (*lift_5*) |
362 (*lift_5*) |
355 Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N})) \ |
363 Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N})) \ |
356 \ (moving Int Req n Int (metric n -`` lessThan N))"; |
364 \ (moving Int Req n Int (metric n -`` lessThan N))"; |
357 br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1; |
365 by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
358 by (etac E_thm16b 4); |
366 by (etac E_thm16b 4); |
359 by (etac E_thm16a 3); |
367 by (etac E_thm16a 3); |
360 by (rtac id_in_Acts 2); |
368 by (rtac id_in_Acts 2); |
361 bd E_thm16c 1; |
369 by (dtac E_thm16c 1); |
362 by (Blast_tac 1); |
370 by (Blast_tac 1); |
363 qed "lift_5"; |
371 qed "lift_5"; |
364 |
372 |
365 |
373 |
366 (** towards lift_3 **) |
374 (** towards lift_3 **) |
367 |
375 |
368 (*lemma used to prove lem_lift_3_1*) |
376 (*lemma used to prove lem_lift_3_1*) |
369 Goal "[| metric n s = 0; Min <= floor s; floor s <= Max |] ==> floor s = n"; |
377 Goal "[| metric n s = 0; Min <= floor s; floor s <= Max |] ==> floor s = n"; |
370 be rev_mp 1; |
378 by (etac rev_mp 1); |
371 by (asm_simp_tac (simpset() addsimps metric_simps) 1); |
379 (*MUCH faster than metric_simps*) |
372 by Auto_tac; |
380 by (asm_simp_tac (simpset() addsimps [metric_def]) 1); |
|
381 by (auto_tac (claset(), simpset() addsimps metric_simps)); |
373 qed "metric_eq_0D"; |
382 qed "metric_eq_0D"; |
374 |
383 |
375 AddDs [metric_eq_0D]; |
384 AddDs [metric_eq_0D]; |
376 |
385 |
377 |
386 |
378 (*lem_lift_3_1*) |
387 (*lem_lift_3_1*) |
379 Goal "LeadsTo Lprg (moving Int Req n Int (metric n -`` {0})) \ |
388 Goal "LeadsTo Lprg (moving Int Req n Int (metric n -`` {0})) \ |
380 \ (stopped Int atFloor n)"; |
389 \ (stopped Int atFloor n)"; |
381 by (cut_facts_tac [bounded] 1); |
390 by (cut_facts_tac [bounded] 1); |
382 by (ensures_tac defs "request_act" 1); |
391 by (ensures_tac "request_act" 1); |
383 by Auto_tac; |
392 by Auto_tac; |
384 qed "E_thm11"; |
393 qed "E_thm11"; |
385 |
394 |
386 (*lem_lift_3_5*) |
395 (*lem_lift_3_5*) |
387 Goal "LeadsTo Lprg \ |
396 Goal "LeadsTo Lprg \ |
388 \ (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \ |
397 \ (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \ |
389 \ (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})"; |
398 \ (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})"; |
390 by (ensures_tac defs "request_act" 1); |
399 by (ensures_tac "request_act" 1); |
391 by (auto_tac (claset(), simpset() addsimps metric_simps)); |
400 by (auto_tac (claset(), simpset() addsimps metric_simps)); |
392 qed "E_thm13"; |
401 qed "E_thm13"; |
393 |
402 |
394 (*lem_lift_3_6*) |
403 (*lem_lift_3_6*) |
395 Goal "0 < N ==> \ |
404 Goal "0 < N ==> \ |
396 \ LeadsTo Lprg \ |
405 \ LeadsTo Lprg \ |
397 \ (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \ |
406 \ (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \ |
398 \ (opened Int Req n Int (metric n -`` {N}))"; |
407 \ (opened Int Req n Int (metric n -`` {N}))"; |
399 by (ensures_tac defs "open_act" 1); |
408 by (ensures_tac "open_act" 1); |
400 by (REPEAT_FIRST (etac rev_mp')); |
409 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
401 by (auto_tac (claset(), simpset() addsimps metric_simps)); |
410 by (auto_tac (claset(), simpset() addsimps metric_simps)); |
402 qed "E_thm14"; |
411 qed "E_thm14"; |
403 |
412 |
404 (*lem_lift_3_7*) |
413 (*lem_lift_3_7*) |
405 Goal "LeadsTo Lprg \ |
414 Goal "LeadsTo Lprg \ |
406 \ (opened Int Req n Int (metric n -`` {N})) \ |
415 \ (opened Int Req n Int (metric n -`` {N})) \ |
407 \ (closed Int Req n Int (metric n -`` {N}))"; |
416 \ (closed Int Req n Int (metric n -`` {N}))"; |
408 by (ensures_tac defs "close_act" 1); |
417 by (ensures_tac "close_act" 1); |
409 by (auto_tac (claset(), simpset() addsimps metric_simps)); |
418 by (auto_tac (claset(), simpset() addsimps metric_simps)); |
410 qed "E_thm15"; |
419 qed "E_thm15"; |
411 |
420 |
412 |
421 |
413 (** the final steps **) |
422 (** the final steps **) |
421 addIs [LeadsTo_Trans]) 1); |
430 addIs [LeadsTo_Trans]) 1); |
422 qed "lift_3_Req"; |
431 qed "lift_3_Req"; |
423 |
432 |
424 |
433 |
425 Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)"; |
434 Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)"; |
426 br (allI RS LessThan_induct) 1; |
435 by (rtac (allI RS LessThan_induct) 1); |
427 by (exhaust_tac "m" 1); |
436 by (exhaust_tac "m" 1); |
428 auto(); |
437 by Auto_tac; |
429 br E_thm11 1; |
438 by (rtac E_thm11 1); |
430 br ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1; |
439 by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1); |
431 br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1; |
440 by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
432 br lift_3_Req 4; |
441 by (rtac lift_3_Req 4); |
433 br lift_4 3; |
442 by (rtac lift_4 3); |
434 auto(); |
443 by Auto_tac; |
435 qed "lift_3"; |
444 qed "lift_3"; |
436 |
445 |
437 |
446 |
438 Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)"; |
447 Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)"; |
439 br LeadsTo_Trans 1; |
448 by (rtac LeadsTo_Trans 1); |
440 br (E_thm04 RS LeadsTo_Un) 2; |
449 by (rtac (E_thm04 RS LeadsTo_Un) 2); |
441 br LeadsTo_Un_post' 2; |
450 by (rtac LeadsTo_Un_post' 2); |
442 br (E_thm01 RS LeadsTo_Trans_Un') 2; |
451 by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2); |
443 br (lift_3 RS LeadsTo_Trans_Un') 2; |
452 by (rtac (lift_3 RS LeadsTo_Trans_Un') 2); |
444 br (lift_2 RS LeadsTo_Trans_Un') 2; |
453 by (rtac (lift_2 RS LeadsTo_Trans_Un') 2); |
445 br (E_thm03 RS LeadsTo_Trans_Un') 2; |
454 by (rtac (E_thm03 RS LeadsTo_Trans_Un') 2); |
446 br E_thm02 2; |
455 by (rtac E_thm02 2); |
447 br (open_move RS Invariant_LeadsToI) 1; |
456 by (rtac (open_move RS Invariant_LeadsToI) 1); |
448 br (open_stop RS Invariant_LeadsToI) 1; |
457 by (rtac (open_stop RS Invariant_LeadsToI) 1); |
449 br subset_imp_LeadsTo 1; |
458 by (rtac subset_imp_LeadsTo 1); |
450 by (rtac id_in_Acts 2); |
459 by (rtac id_in_Acts 2); |
451 bws defs; |
|
452 by (Clarify_tac 1); |
460 by (Clarify_tac 1); |
453 (*stops simplification from looping*) |
461 (*stops simplification from looping*) |
454 by (Full_simp_tac 1); |
462 by (Full_simp_tac 1); |
455 by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1)); |
463 by (Blast_tac 1); |
456 qed "lift_1"; |
464 qed "lift_1"; |
457 |
465 |
458 Close_locale; |
466 Close_locale; |
459 |
467 |
460 |
468 |