36 If b1$x then f$(g$x) else x fi)" |
36 If b1$x then f$(g$x) else x fi)" |
37 |
37 |
38 q_def: "q == fix$(LAM f. LAM x. |
38 q_def: "q == fix$(LAM f. LAM x. |
39 If b1$x orelse b2$x then f$(g$x) else x fi)" |
39 If b1$x orelse b2$x then f$(g$x) else x fi)" |
40 |
40 |
41 ML {* use_legacy_bindings (the_context ()) *} |
41 |
|
42 (* --------- pure HOLCF logic, some little lemmas ------ *) |
|
43 |
|
44 lemma hoare_lemma2: "b~=TT ==> b=FF | b=UU" |
|
45 apply (rule Exh_tr [THEN disjE]) |
|
46 apply blast+ |
|
47 done |
|
48 |
|
49 lemma hoare_lemma3: " (ALL k. b1$(iterate k$g$x) = TT) | (EX k. b1$(iterate k$g$x)~=TT)" |
|
50 apply blast |
|
51 done |
|
52 |
|
53 lemma hoare_lemma4: "(EX k. b1$(iterate k$g$x) ~= TT) ==> |
|
54 EX k. b1$(iterate k$g$x) = FF | b1$(iterate k$g$x) = UU" |
|
55 apply (erule exE) |
|
56 apply (rule exI) |
|
57 apply (rule hoare_lemma2) |
|
58 apply assumption |
|
59 done |
|
60 |
|
61 lemma hoare_lemma5: "[|(EX k. b1$(iterate k$g$x) ~= TT); |
|
62 k=Least(%n. b1$(iterate n$g$x) ~= TT)|] ==> |
|
63 b1$(iterate k$g$x)=FF | b1$(iterate k$g$x)=UU" |
|
64 apply hypsubst |
|
65 apply (rule hoare_lemma2) |
|
66 apply (erule exE) |
|
67 apply (erule LeastI) |
|
68 done |
|
69 |
|
70 lemma hoare_lemma6: "b=UU ==> b~=TT" |
|
71 apply hypsubst |
|
72 apply (rule dist_eq_tr) |
|
73 done |
|
74 |
|
75 lemma hoare_lemma7: "b=FF ==> b~=TT" |
|
76 apply hypsubst |
|
77 apply (rule dist_eq_tr) |
|
78 done |
|
79 |
|
80 lemma hoare_lemma8: "[|(EX k. b1$(iterate k$g$x) ~= TT); |
|
81 k=Least(%n. b1$(iterate n$g$x) ~= TT)|] ==> |
|
82 ALL m. m < k --> b1$(iterate m$g$x)=TT" |
|
83 apply hypsubst |
|
84 apply (erule exE) |
|
85 apply (intro strip) |
|
86 apply (rule_tac p = "b1$ (iterate m$g$x) " in trE) |
|
87 prefer 2 apply (assumption) |
|
88 apply (rule le_less_trans [THEN less_irrefl]) |
|
89 prefer 2 apply (assumption) |
|
90 apply (rule Least_le) |
|
91 apply (erule hoare_lemma6) |
|
92 apply (rule le_less_trans [THEN less_irrefl]) |
|
93 prefer 2 apply (assumption) |
|
94 apply (rule Least_le) |
|
95 apply (erule hoare_lemma7) |
|
96 done |
|
97 |
|
98 |
|
99 lemma hoare_lemma28: "f$(y::'a)=(UU::tr) ==> f$UU = UU" |
|
100 apply (erule flat_codom [THEN disjE]) |
|
101 apply auto |
|
102 done |
|
103 |
|
104 |
|
105 (* ----- access to definitions ----- *) |
|
106 |
|
107 lemma p_def3: "p$x = If b1$x then p$(g$x) else x fi" |
|
108 apply (rule trans) |
|
109 apply (rule p_def [THEN fix_eq3]) |
|
110 apply simp |
|
111 done |
|
112 |
|
113 lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x fi" |
|
114 apply (rule trans) |
|
115 apply (rule q_def [THEN fix_eq3]) |
|
116 apply simp |
|
117 done |
|
118 |
|
119 (** --------- proofs about iterations of p and q ---------- **) |
|
120 |
|
121 lemma hoare_lemma9: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) --> |
|
122 p$(iterate k$g$x)=p$x" |
|
123 apply (induct_tac k) |
|
124 apply (simp (no_asm)) |
|
125 apply (simp (no_asm)) |
|
126 apply (intro strip) |
|
127 apply (rule_tac s = "p$ (iterate n$g$x) " in trans) |
|
128 apply (rule trans) |
|
129 apply (rule_tac [2] p_def3 [symmetric]) |
|
130 apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst) |
|
131 apply (rule mp) |
|
132 apply (erule spec) |
|
133 apply (simp (no_asm) add: less_Suc_eq) |
|
134 apply simp |
|
135 apply (erule mp) |
|
136 apply (intro strip) |
|
137 apply (rule mp) |
|
138 apply (erule spec) |
|
139 apply (erule less_trans) |
|
140 apply simp |
|
141 done |
|
142 |
|
143 lemma hoare_lemma24: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) --> |
|
144 q$(iterate k$g$x)=q$x" |
|
145 apply (induct_tac k) |
|
146 apply (simp (no_asm)) |
|
147 apply (simp (no_asm) add: less_Suc_eq) |
|
148 apply (intro strip) |
|
149 apply (rule_tac s = "q$ (iterate n$g$x) " in trans) |
|
150 apply (rule trans) |
|
151 apply (rule_tac [2] q_def3 [symmetric]) |
|
152 apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst) |
|
153 apply blast |
|
154 apply simp |
|
155 apply (erule mp) |
|
156 apply (intro strip) |
|
157 apply (fast dest!: less_Suc_eq [THEN iffD1]) |
|
158 done |
|
159 |
|
160 (* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *) |
|
161 |
|
162 thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard, no_vars] |
|
163 |
|
164 lemma hoare_lemma10: |
|
165 "EX k. b1$(iterate k$g$x) ~= TT |
|
166 ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> p$(iterate k$g$x) = p$x" |
|
167 by (rule hoare_lemma8 [THEN hoare_lemma9 [THEN mp]]) |
|
168 |
|
169 lemma hoare_lemma11: "(EX n. b1$(iterate n$g$x) ~= TT) ==> |
|
170 k=(LEAST n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x)=FF |
|
171 --> p$x = iterate k$g$x" |
|
172 apply (case_tac "k") |
|
173 apply hypsubst |
|
174 apply (simp (no_asm)) |
|
175 apply (intro strip) |
|
176 apply (erule conjE) |
|
177 apply (rule trans) |
|
178 apply (rule p_def3) |
|
179 apply simp |
|
180 apply hypsubst |
|
181 apply (intro strip) |
|
182 apply (erule conjE) |
|
183 apply (rule trans) |
|
184 apply (erule hoare_lemma10 [symmetric]) |
|
185 apply assumption |
|
186 apply (rule trans) |
|
187 apply (rule p_def3) |
|
188 apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst) |
|
189 apply (rule hoare_lemma8 [THEN spec, THEN mp]) |
|
190 apply assumption |
|
191 apply assumption |
|
192 apply (simp (no_asm)) |
|
193 apply (tactic "simp_tac HOLCF_ss 1") |
|
194 apply (rule trans) |
|
195 apply (rule p_def3) |
|
196 apply (simp (no_asm) del: iterate_Suc add: iterate_Suc [symmetric]) |
|
197 apply (erule_tac s = "FF" in ssubst) |
|
198 apply simp |
|
199 done |
|
200 |
|
201 lemma hoare_lemma12: "(EX n. b1$(iterate n$g$x) ~= TT) ==> |
|
202 k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU |
|
203 --> p$x = UU" |
|
204 apply (case_tac "k") |
|
205 apply hypsubst |
|
206 apply (simp (no_asm)) |
|
207 apply (intro strip) |
|
208 apply (erule conjE) |
|
209 apply (rule trans) |
|
210 apply (rule p_def3) |
|
211 apply simp |
|
212 apply hypsubst |
|
213 apply (simp (no_asm)) |
|
214 apply (intro strip) |
|
215 apply (erule conjE) |
|
216 apply (rule trans) |
|
217 apply (rule hoare_lemma10 [symmetric]) |
|
218 apply assumption |
|
219 apply assumption |
|
220 apply (rule trans) |
|
221 apply (rule p_def3) |
|
222 apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst) |
|
223 apply (rule hoare_lemma8 [THEN spec, THEN mp]) |
|
224 apply assumption |
|
225 apply assumption |
|
226 apply (simp (no_asm)) |
|
227 apply (tactic "asm_simp_tac HOLCF_ss 1") |
|
228 apply (rule trans) |
|
229 apply (rule p_def3) |
|
230 apply simp |
|
231 done |
|
232 |
|
233 (* -------- results about p for case (ALL k. b1$(iterate k$g$x)=TT) ------- *) |
|
234 |
|
235 lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU" |
|
236 apply (rule p_def [THEN def_fix_ind]) |
|
237 apply (rule adm_all) |
|
238 apply (rule allI) |
|
239 apply (rule adm_eq) |
|
240 apply (tactic "cont_tacR 1") |
|
241 apply (rule allI) |
|
242 apply (subst Rep_CFun_strict1) |
|
243 apply (rule refl) |
|
244 apply (simp (no_asm)) |
|
245 apply (rule allI) |
|
246 apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst) |
|
247 apply (erule spec) |
|
248 apply (tactic "asm_simp_tac HOLCF_ss 1") |
|
249 apply (rule iterate_Suc [THEN subst]) |
|
250 apply (erule spec) |
|
251 done |
|
252 |
|
253 lemma hoare_lemma16: "(ALL k. b1$(iterate k$g$x)=TT) ==> p$x = UU" |
|
254 apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst]) |
|
255 apply (erule fernpass_lemma [THEN spec]) |
|
256 done |
|
257 |
|
258 (* -------- results about q for case (ALL k. b1$(iterate k$g$x)=TT) ------- *) |
|
259 |
|
260 lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU" |
|
261 apply (rule q_def [THEN def_fix_ind]) |
|
262 apply (rule adm_all) |
|
263 apply (rule allI) |
|
264 apply (rule adm_eq) |
|
265 apply (tactic "cont_tacR 1") |
|
266 apply (rule allI) |
|
267 apply (subst Rep_CFun_strict1) |
|
268 apply (rule refl) |
|
269 apply (rule allI) |
|
270 apply (simp (no_asm)) |
|
271 apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst) |
|
272 apply (erule spec) |
|
273 apply (tactic "asm_simp_tac HOLCF_ss 1") |
|
274 apply (rule iterate_Suc [THEN subst]) |
|
275 apply (erule spec) |
|
276 done |
|
277 |
|
278 lemma hoare_lemma18: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$x = UU" |
|
279 apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst]) |
|
280 apply (erule hoare_lemma17 [THEN spec]) |
|
281 done |
|
282 |
|
283 lemma hoare_lemma19: |
|
284 "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)" |
|
285 apply (rule flat_codom) |
|
286 apply (rule_tac t = "x1" in iterate_0 [THEN subst]) |
|
287 apply (erule spec) |
|
288 done |
|
289 |
|
290 lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU" |
|
291 apply (rule q_def [THEN def_fix_ind]) |
|
292 apply (rule adm_all) |
|
293 apply (rule allI) |
|
294 apply (rule adm_eq) |
|
295 apply (tactic "cont_tacR 1") |
|
296 apply (rule allI) |
|
297 apply (subst Rep_CFun_strict1) |
|
298 apply (rule refl) |
|
299 apply (rule allI) |
|
300 apply (simp (no_asm)) |
|
301 apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst) |
|
302 apply (erule spec) |
|
303 apply (tactic "asm_simp_tac HOLCF_ss 1") |
|
304 apply (rule iterate_Suc [THEN subst]) |
|
305 apply (erule spec) |
|
306 done |
|
307 |
|
308 lemma hoare_lemma21: "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU" |
|
309 apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst]) |
|
310 apply (erule hoare_lemma20 [THEN spec]) |
|
311 done |
|
312 |
|
313 lemma hoare_lemma22: "b1$(UU::'a)=UU ==> q$(UU::'a) = UU" |
|
314 apply (subst q_def3) |
|
315 apply simp |
|
316 done |
|
317 |
|
318 (* -------- results about q for case (EX k. b1$(iterate k$g$x) ~= TT) ------- *) |
|
319 |
|
320 lemma hoare_lemma25: "EX k. b1$(iterate k$g$x) ~= TT |
|
321 ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> q$(iterate k$g$x) = q$x" |
|
322 by (rule hoare_lemma8 [THEN hoare_lemma24 [THEN mp]]) |
|
323 |
|
324 lemma hoare_lemma26: "(EX n. b1$(iterate n$g$x)~=TT) ==> |
|
325 k=Least(%n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x) =FF |
|
326 --> q$x = q$(iterate k$g$x)" |
|
327 apply (case_tac "k") |
|
328 apply hypsubst |
|
329 apply (intro strip) |
|
330 apply (simp (no_asm)) |
|
331 apply hypsubst |
|
332 apply (intro strip) |
|
333 apply (erule conjE) |
|
334 apply (rule trans) |
|
335 apply (rule hoare_lemma25 [symmetric]) |
|
336 apply assumption |
|
337 apply assumption |
|
338 apply (rule trans) |
|
339 apply (rule q_def3) |
|
340 apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst) |
|
341 apply (rule hoare_lemma8 [THEN spec, THEN mp]) |
|
342 apply assumption |
|
343 apply assumption |
|
344 apply (simp (no_asm)) |
|
345 apply (simp (no_asm)) |
|
346 done |
|
347 |
|
348 |
|
349 lemma hoare_lemma27: "(EX n. b1$(iterate n$g$x) ~= TT) ==> |
|
350 k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU |
|
351 --> q$x = UU" |
|
352 apply (case_tac "k") |
|
353 apply hypsubst |
|
354 apply (simp (no_asm)) |
|
355 apply (intro strip) |
|
356 apply (erule conjE) |
|
357 apply (subst q_def3) |
|
358 apply (tactic "asm_simp_tac HOLCF_ss 1") |
|
359 apply hypsubst |
|
360 apply (simp (no_asm)) |
|
361 apply (intro strip) |
|
362 apply (erule conjE) |
|
363 apply (rule trans) |
|
364 apply (rule hoare_lemma25 [symmetric]) |
|
365 apply assumption |
|
366 apply assumption |
|
367 apply (rule trans) |
|
368 apply (rule q_def3) |
|
369 apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst) |
|
370 apply (rule hoare_lemma8 [THEN spec, THEN mp]) |
|
371 apply assumption |
|
372 apply assumption |
|
373 apply (simp (no_asm)) |
|
374 apply (tactic "asm_simp_tac HOLCF_ss 1") |
|
375 apply (rule trans) |
|
376 apply (rule q_def3) |
|
377 apply (tactic "asm_simp_tac HOLCF_ss 1") |
|
378 done |
|
379 |
|
380 (* ------- (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q ----- *) |
|
381 |
|
382 lemma hoare_lemma23: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$(p$x) = q$x" |
|
383 apply (subst hoare_lemma16) |
|
384 apply assumption |
|
385 apply (rule hoare_lemma19 [THEN disjE]) |
|
386 apply assumption |
|
387 apply (simplesubst hoare_lemma18) |
|
388 apply assumption |
|
389 apply (simplesubst hoare_lemma22) |
|
390 apply assumption |
|
391 apply (rule refl) |
|
392 apply (simplesubst hoare_lemma21) |
|
393 apply assumption |
|
394 apply (simplesubst hoare_lemma21) |
|
395 apply assumption |
|
396 apply (rule refl) |
|
397 done |
|
398 |
|
399 (* ------------ EX k. b1~(iterate k$g$x) ~= TT ==> q o p = q ----- *) |
|
400 |
|
401 lemma hoare_lemma29: "EX k. b1$(iterate k$g$x) ~= TT ==> q$(p$x) = q$x" |
|
402 apply (rule hoare_lemma5 [THEN disjE]) |
|
403 apply assumption |
|
404 apply (rule refl) |
|
405 apply (subst hoare_lemma11 [THEN mp]) |
|
406 apply assumption |
|
407 apply (rule conjI) |
|
408 apply (rule refl) |
|
409 apply assumption |
|
410 apply (rule hoare_lemma26 [THEN mp, THEN subst]) |
|
411 apply assumption |
|
412 apply (rule conjI) |
|
413 apply (rule refl) |
|
414 apply assumption |
|
415 apply (rule refl) |
|
416 apply (subst hoare_lemma12 [THEN mp]) |
|
417 apply assumption |
|
418 apply (rule conjI) |
|
419 apply (rule refl) |
|
420 apply assumption |
|
421 apply (subst hoare_lemma22) |
|
422 apply (subst hoare_lemma28) |
|
423 apply assumption |
|
424 apply (rule refl) |
|
425 apply (rule sym) |
|
426 apply (subst hoare_lemma27 [THEN mp]) |
|
427 apply assumption |
|
428 apply (rule conjI) |
|
429 apply (rule refl) |
|
430 apply assumption |
|
431 apply (rule refl) |
|
432 done |
|
433 |
|
434 (* ------ the main proof q o p = q ------ *) |
|
435 |
|
436 theorem hoare_main: "q oo p = q" |
|
437 apply (rule ext_cfun) |
|
438 apply (subst cfcomp2) |
|
439 apply (rule hoare_lemma3 [THEN disjE]) |
|
440 apply (erule hoare_lemma23) |
|
441 apply (erule hoare_lemma29) |
|
442 done |
42 |
443 |
43 end |
444 end |