6 |
6 |
7 open Hoare; |
7 open Hoare; |
8 |
8 |
9 (* --------- pure HOLCF logic, some little lemmas ------ *) |
9 (* --------- pure HOLCF logic, some little lemmas ------ *) |
10 |
10 |
11 qed_goal "hoare_lemma2" HOLCF.thy "~b=TT ==> b=FF | b=UU" |
11 val hoare_lemma2 = prove_goal HOLCF.thy "~b=TT ==> b=FF | b=UU" |
12 (fn prems => |
12 (fn prems => |
13 [ |
13 [ |
14 (cut_facts_tac prems 1), |
14 (cut_facts_tac prems 1), |
15 (rtac (Exh_tr RS disjE) 1), |
15 (rtac (Exh_tr RS disjE) 1), |
16 (fast_tac HOL_cs 1), |
16 (fast_tac HOL_cs 1), |
17 (etac disjE 1), |
17 (etac disjE 1), |
18 (contr_tac 1), |
18 (contr_tac 1), |
19 (fast_tac HOL_cs 1) |
19 (fast_tac HOL_cs 1) |
20 ]); |
20 ]); |
21 |
21 |
22 qed_goal "hoare_lemma3" HOLCF.thy |
22 val hoare_lemma3 = prove_goal HOLCF.thy |
23 " (!k.b1[iterate(k,g,x)]=TT) | (? k.~ b1[iterate(k,g,x)]=TT)" |
23 " (!k.b1[iterate(k,g,x)]=TT) | (? k.~ b1[iterate(k,g,x)]=TT)" |
24 (fn prems => |
24 (fn prems => |
25 [ |
25 [ |
26 (fast_tac HOL_cs 1) |
26 (fast_tac HOL_cs 1) |
27 ]); |
27 ]); |
28 |
28 |
29 qed_goal "hoare_lemma4" HOLCF.thy |
29 val hoare_lemma4 = prove_goal HOLCF.thy |
30 "(? k.~ b1[iterate(k,g,x)]=TT) ==> \ |
30 "(? k.~ b1[iterate(k,g,x)]=TT) ==> \ |
31 \ ? k.b1[iterate(k,g,x)]=FF | b1[iterate(k,g,x)]=UU" |
31 \ ? k.b1[iterate(k,g,x)]=FF | b1[iterate(k,g,x)]=UU" |
32 (fn prems => |
32 (fn prems => |
33 [ |
33 [ |
34 (cut_facts_tac prems 1), |
34 (cut_facts_tac prems 1), |
36 (rtac exI 1), |
36 (rtac exI 1), |
37 (rtac hoare_lemma2 1), |
37 (rtac hoare_lemma2 1), |
38 (atac 1) |
38 (atac 1) |
39 ]); |
39 ]); |
40 |
40 |
41 qed_goal "hoare_lemma5" HOLCF.thy |
41 val hoare_lemma5 = prove_goal HOLCF.thy |
42 "[|(? k.~ b1[iterate(k,g,x)]=TT);\ |
42 "[|(? k.~ b1[iterate(k,g,x)]=TT);\ |
43 \ k=theleast(%n.~ b1[iterate(n,g,x)]=TT)|] ==> \ |
43 \ k=theleast(%n.~ b1[iterate(n,g,x)]=TT)|] ==> \ |
44 \ b1[iterate(k,g,x)]=FF | b1[iterate(k,g,x)]=UU" |
44 \ b1[iterate(k,g,x)]=FF | b1[iterate(k,g,x)]=UU" |
45 (fn prems => |
45 (fn prems => |
46 [ |
46 [ |
49 (rtac hoare_lemma2 1), |
49 (rtac hoare_lemma2 1), |
50 (etac exE 1), |
50 (etac exE 1), |
51 (etac theleast1 1) |
51 (etac theleast1 1) |
52 ]); |
52 ]); |
53 |
53 |
54 qed_goal "hoare_lemma6" HOLCF.thy "b=UU ==> ~b=TT" |
54 val hoare_lemma6 = prove_goal HOLCF.thy "b=UU ==> ~b=TT" |
55 (fn prems => |
55 (fn prems => |
56 [ |
56 [ |
57 (cut_facts_tac prems 1), |
57 (cut_facts_tac prems 1), |
58 (hyp_subst_tac 1), |
58 (hyp_subst_tac 1), |
59 (resolve_tac dist_eq_tr 1) |
59 (resolve_tac dist_eq_tr 1) |
60 ]); |
60 ]); |
61 |
61 |
62 qed_goal "hoare_lemma7" HOLCF.thy "b=FF ==> ~b=TT" |
62 val hoare_lemma7 = prove_goal HOLCF.thy "b=FF ==> ~b=TT" |
63 (fn prems => |
63 (fn prems => |
64 [ |
64 [ |
65 (cut_facts_tac prems 1), |
65 (cut_facts_tac prems 1), |
66 (hyp_subst_tac 1), |
66 (hyp_subst_tac 1), |
67 (resolve_tac dist_eq_tr 1) |
67 (resolve_tac dist_eq_tr 1) |
68 ]); |
68 ]); |
69 |
69 |
70 qed_goal "hoare_lemma8" HOLCF.thy |
70 val hoare_lemma8 = prove_goal HOLCF.thy |
71 "[|(? k.~ b1[iterate(k,g,x)]=TT);\ |
71 "[|(? k.~ b1[iterate(k,g,x)]=TT);\ |
72 \ k=theleast(%n.~ b1[iterate(n,g,x)]=TT)|] ==> \ |
72 \ k=theleast(%n.~ b1[iterate(n,g,x)]=TT)|] ==> \ |
73 \ !m. m<k --> b1[iterate(m,g,x)]=TT" |
73 \ !m. m<k --> b1[iterate(m,g,x)]=TT" |
74 (fn prems => |
74 (fn prems => |
75 [ |
75 [ |
87 (atac 2), |
87 (atac 2), |
88 (rtac theleast2 1), |
88 (rtac theleast2 1), |
89 (etac hoare_lemma7 1) |
89 (etac hoare_lemma7 1) |
90 ]); |
90 ]); |
91 |
91 |
92 qed_goal "hoare_lemma28" HOLCF.thy |
92 val hoare_lemma28 = prove_goal HOLCF.thy |
93 "b1[y::'a]=(UU::tr) ==> b1[UU] = UU" |
93 "b1[y::'a]=(UU::tr) ==> b1[UU] = UU" |
94 (fn prems => |
94 (fn prems => |
95 [ |
95 [ |
96 (cut_facts_tac prems 1), |
96 (cut_facts_tac prems 1), |
97 (etac (flat_tr RS flat_codom RS disjE) 1), |
97 (etac (flat_tr RS flat_codom RS disjE) 1), |
100 ]); |
100 ]); |
101 |
101 |
102 |
102 |
103 (* ----- access to definitions ----- *) |
103 (* ----- access to definitions ----- *) |
104 |
104 |
105 qed_goalw "p_def2" Hoare.thy [p_def] |
105 val p_def2 = prove_goalw Hoare.thy [p_def] |
106 "p = fix[LAM f x. If b1[x] then f[g[x]] else x fi]" |
106 "p = fix[LAM f x. If b1[x] then f[g[x]] else x fi]" |
107 (fn prems => |
107 (fn prems => |
108 [ |
108 [ |
109 (rtac refl 1) |
109 (rtac refl 1) |
110 ]); |
110 ]); |
111 |
111 |
112 qed_goalw "q_def2" Hoare.thy [q_def] |
112 val q_def2 = prove_goalw Hoare.thy [q_def] |
113 "q = fix[LAM f x. If b1[x] orelse b2[x] then \ |
113 "q = fix[LAM f x. If b1[x] orelse b2[x] then \ |
114 \ f[g[x]] else x fi]" |
114 \ f[g[x]] else x fi]" |
115 (fn prems => |
115 (fn prems => |
116 [ |
116 [ |
117 (rtac refl 1) |
117 (rtac refl 1) |
118 ]); |
118 ]); |
119 |
119 |
120 |
120 |
121 qed_goal "p_def3" Hoare.thy |
121 val p_def3 = prove_goal Hoare.thy |
122 "p[x] = If b1[x] then p[g[x]] else x fi" |
122 "p[x] = If b1[x] then p[g[x]] else x fi" |
123 (fn prems => |
123 (fn prems => |
124 [ |
124 [ |
125 (fix_tac3 p_def 1), |
125 (fix_tac3 p_def 1), |
126 (simp_tac HOLCF_ss 1) |
126 (simp_tac HOLCF_ss 1) |
127 ]); |
127 ]); |
128 |
128 |
129 qed_goal "q_def3" Hoare.thy |
129 val q_def3 = prove_goal Hoare.thy |
130 "q[x] = If b1[x] orelse b2[x] then q[g[x]] else x fi" |
130 "q[x] = If b1[x] orelse b2[x] then q[g[x]] else x fi" |
131 (fn prems => |
131 (fn prems => |
132 [ |
132 [ |
133 (fix_tac3 q_def 1), |
133 (fix_tac3 q_def 1), |
134 (simp_tac HOLCF_ss 1) |
134 (simp_tac HOLCF_ss 1) |
135 ]); |
135 ]); |
136 |
136 |
137 (** --------- proves about iterations of p and q ---------- **) |
137 (** --------- proves about iterations of p and q ---------- **) |
138 |
138 |
139 qed_goal "hoare_lemma9" Hoare.thy |
139 val hoare_lemma9 = prove_goal Hoare.thy |
140 "(! m. m<Suc(k) --> b1[iterate(m,g,x)]=TT) -->\ |
140 "(! m. m<Suc(k) --> b1[iterate(m,g,x)]=TT) -->\ |
141 \ p[iterate(k,g,x)]=p[x]" |
141 \ p[iterate(k,g,x)]=p[x]" |
142 (fn prems => |
142 (fn prems => |
143 [ |
143 [ |
144 (nat_ind_tac "k" 1), |
144 (nat_ind_tac "k" 1), |
194 [| ? k. ~ b1[iterate(k,g,?x1)] = TT; |
194 [| ? k. ~ b1[iterate(k,g,?x1)] = TT; |
195 Suc(?k3) = theleast(%n. ~ b1[iterate(n,g,?x1)] = TT) |] ==> |
195 Suc(?k3) = theleast(%n. ~ b1[iterate(n,g,?x1)] = TT) |] ==> |
196 p[iterate(?k3,g,?x1)] = p[?x1] |
196 p[iterate(?k3,g,?x1)] = p[?x1] |
197 *) |
197 *) |
198 |
198 |
199 qed_goal "hoare_lemma11" Hoare.thy |
199 val hoare_lemma11 = prove_goal Hoare.thy |
200 "(? n.b1[iterate(n,g,x)]~=TT) ==>\ |
200 "(? n.b1[iterate(n,g,x)]~=TT) ==>\ |
201 \ k=theleast(%n.b1[iterate(n,g,x)]~=TT) & b1[iterate(k,g,x)]=FF \ |
201 \ k=theleast(%n.b1[iterate(n,g,x)]~=TT) & b1[iterate(k,g,x)]=FF \ |
202 \ --> p[x] = iterate(k,g,x)" |
202 \ --> p[x] = iterate(k,g,x)" |
203 (fn prems => |
203 (fn prems => |
204 [ |
204 [ |
233 (simp_tac (HOLCF_ss addsimps [iterate_Suc RS sym]) 1), |
233 (simp_tac (HOLCF_ss addsimps [iterate_Suc RS sym]) 1), |
234 (eres_inst_tac [("s","FF")] ssubst 1), |
234 (eres_inst_tac [("s","FF")] ssubst 1), |
235 (simp_tac HOLCF_ss 1) |
235 (simp_tac HOLCF_ss 1) |
236 ]); |
236 ]); |
237 |
237 |
238 qed_goal "hoare_lemma12" Hoare.thy |
238 val hoare_lemma12 = prove_goal Hoare.thy |
239 "(? n.~ b1[iterate(n,g,x)]=TT) ==>\ |
239 "(? n.~ b1[iterate(n,g,x)]=TT) ==>\ |
240 \ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \ |
240 \ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \ |
241 \ --> p[x] = UU" |
241 \ --> p[x] = UU" |
242 (fn prems => |
242 (fn prems => |
243 [ |
243 [ |
271 (asm_simp_tac HOLCF_ss 1) |
271 (asm_simp_tac HOLCF_ss 1) |
272 ]); |
272 ]); |
273 |
273 |
274 (* -------- results about p for case (! k. b1[iterate(k,g,x)]=TT) ------- *) |
274 (* -------- results about p for case (! k. b1[iterate(k,g,x)]=TT) ------- *) |
275 |
275 |
276 qed_goal "fernpass_lemma" Hoare.thy |
276 val fernpass_lemma = prove_goal Hoare.thy |
277 "(! k. b1[iterate(k,g,x)]=TT) ==> !k.p[iterate(k,g,x)] = UU" |
277 "(! k. b1[iterate(k,g,x)]=TT) ==> !k.p[iterate(k,g,x)] = UU" |
278 (fn prems => |
278 (fn prems => |
279 [ |
279 [ |
280 (cut_facts_tac prems 1), |
280 (cut_facts_tac prems 1), |
281 (rtac (p_def2 RS ssubst) 1), |
281 (rtac (p_def2 RS ssubst) 1), |
294 (asm_simp_tac HOLCF_ss 1), |
294 (asm_simp_tac HOLCF_ss 1), |
295 (rtac (iterate_Suc RS subst) 1), |
295 (rtac (iterate_Suc RS subst) 1), |
296 (etac spec 1) |
296 (etac spec 1) |
297 ]); |
297 ]); |
298 |
298 |
299 qed_goal "hoare_lemma16" Hoare.thy |
299 val hoare_lemma16 = prove_goal Hoare.thy |
300 "(! k. b1[iterate(k,g,x)]=TT) ==> p[x] = UU" |
300 "(! k. b1[iterate(k,g,x)]=TT) ==> p[x] = UU" |
301 (fn prems => |
301 (fn prems => |
302 [ |
302 [ |
303 (cut_facts_tac prems 1), |
303 (cut_facts_tac prems 1), |
304 (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
304 (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
305 (etac (fernpass_lemma RS spec) 1) |
305 (etac (fernpass_lemma RS spec) 1) |
306 ]); |
306 ]); |
307 |
307 |
308 (* -------- results about q for case (! k. b1[iterate(k,g,x)]=TT) ------- *) |
308 (* -------- results about q for case (! k. b1[iterate(k,g,x)]=TT) ------- *) |
309 |
309 |
310 qed_goal "hoare_lemma17" Hoare.thy |
310 val hoare_lemma17 = prove_goal Hoare.thy |
311 "(! k. b1[iterate(k,g,x)]=TT) ==> !k.q[iterate(k,g,x)] = UU" |
311 "(! k. b1[iterate(k,g,x)]=TT) ==> !k.q[iterate(k,g,x)] = UU" |
312 (fn prems => |
312 (fn prems => |
313 [ |
313 [ |
314 (cut_facts_tac prems 1), |
314 (cut_facts_tac prems 1), |
315 (rtac (q_def2 RS ssubst) 1), |
315 (rtac (q_def2 RS ssubst) 1), |
328 (asm_simp_tac HOLCF_ss 1), |
328 (asm_simp_tac HOLCF_ss 1), |
329 (rtac (iterate_Suc RS subst) 1), |
329 (rtac (iterate_Suc RS subst) 1), |
330 (etac spec 1) |
330 (etac spec 1) |
331 ]); |
331 ]); |
332 |
332 |
333 qed_goal "hoare_lemma18" Hoare.thy |
333 val hoare_lemma18 = prove_goal Hoare.thy |
334 "(! k. b1[iterate(k,g,x)]=TT) ==> q[x] = UU" |
334 "(! k. b1[iterate(k,g,x)]=TT) ==> q[x] = UU" |
335 (fn prems => |
335 (fn prems => |
336 [ |
336 [ |
337 (cut_facts_tac prems 1), |
337 (cut_facts_tac prems 1), |
338 (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
338 (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
339 (etac (hoare_lemma17 RS spec) 1) |
339 (etac (hoare_lemma17 RS spec) 1) |
340 ]); |
340 ]); |
341 |
341 |
342 qed_goal "hoare_lemma19" Hoare.thy |
342 val hoare_lemma19 = prove_goal Hoare.thy |
343 "(!k. (b1::'a->tr)[iterate(k,g,x)]=TT) ==> b1[UU::'a] = UU | (!y.b1[y::'a]=TT)" |
343 "(!k. (b1::'a->tr)[iterate(k,g,x)]=TT) ==> b1[UU::'a] = UU | (!y.b1[y::'a]=TT)" |
344 (fn prems => |
344 (fn prems => |
345 [ |
345 [ |
346 (cut_facts_tac prems 1), |
346 (cut_facts_tac prems 1), |
347 (rtac (flat_tr RS flat_codom) 1), |
347 (rtac (flat_tr RS flat_codom) 1), |
348 (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1), |
348 (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1), |
349 (etac spec 1) |
349 (etac spec 1) |
350 ]); |
350 ]); |
351 |
351 |
352 qed_goal "hoare_lemma20" Hoare.thy |
352 val hoare_lemma20 = prove_goal Hoare.thy |
353 "(! y. b1[y::'a]=TT) ==> !k.q[iterate(k,g,x::'a)] = UU" |
353 "(! y. b1[y::'a]=TT) ==> !k.q[iterate(k,g,x::'a)] = UU" |
354 (fn prems => |
354 (fn prems => |
355 [ |
355 [ |
356 (cut_facts_tac prems 1), |
356 (cut_facts_tac prems 1), |
357 (rtac (q_def2 RS ssubst) 1), |
357 (rtac (q_def2 RS ssubst) 1), |
370 (asm_simp_tac HOLCF_ss 1), |
370 (asm_simp_tac HOLCF_ss 1), |
371 (rtac (iterate_Suc RS subst) 1), |
371 (rtac (iterate_Suc RS subst) 1), |
372 (etac spec 1) |
372 (etac spec 1) |
373 ]); |
373 ]); |
374 |
374 |
375 qed_goal "hoare_lemma21" Hoare.thy |
375 val hoare_lemma21 = prove_goal Hoare.thy |
376 "(! y. b1[y::'a]=TT) ==> q[x::'a] = UU" |
376 "(! y. b1[y::'a]=TT) ==> q[x::'a] = UU" |
377 (fn prems => |
377 (fn prems => |
378 [ |
378 [ |
379 (cut_facts_tac prems 1), |
379 (cut_facts_tac prems 1), |
380 (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
380 (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
381 (etac (hoare_lemma20 RS spec) 1) |
381 (etac (hoare_lemma20 RS spec) 1) |
382 ]); |
382 ]); |
383 |
383 |
384 qed_goal "hoare_lemma22" Hoare.thy |
384 val hoare_lemma22 = prove_goal Hoare.thy |
385 "b1[UU::'a]=UU ==> q[UU::'a] = UU" |
385 "b1[UU::'a]=UU ==> q[UU::'a] = UU" |
386 (fn prems => |
386 (fn prems => |
387 [ |
387 [ |
388 (cut_facts_tac prems 1), |
388 (cut_facts_tac prems 1), |
389 (rtac (q_def3 RS ssubst) 1), |
389 (rtac (q_def3 RS ssubst) 1), |
397 [| ? k. ~ ?b1.1[iterate(k,?g1,?x1)] = TT; |
397 [| ? k. ~ ?b1.1[iterate(k,?g1,?x1)] = TT; |
398 Suc(?k3) = theleast(%n. ~ ?b1.1[iterate(n,?g1,?x1)] = TT) |] ==> |
398 Suc(?k3) = theleast(%n. ~ ?b1.1[iterate(n,?g1,?x1)] = TT) |] ==> |
399 q[iterate(?k3,?g1,?x1)] = q[?x1] |
399 q[iterate(?k3,?g1,?x1)] = q[?x1] |
400 *) |
400 *) |
401 |
401 |
402 qed_goal "hoare_lemma26" Hoare.thy |
402 val hoare_lemma26 = prove_goal Hoare.thy |
403 "(? n.~ b1[iterate(n,g,x)]=TT) ==>\ |
403 "(? n.~ b1[iterate(n,g,x)]=TT) ==>\ |
404 \ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=FF \ |
404 \ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=FF \ |
405 \ --> q[x] = q[iterate(k,g,x)]" |
405 \ --> q[x] = q[iterate(k,g,x)]" |
406 (fn prems => |
406 (fn prems => |
407 [ |
407 [ |
426 (simp_tac nat_ss 1), |
426 (simp_tac nat_ss 1), |
427 (simp_tac (HOLCF_ss addsimps [iterate_Suc]) 1) |
427 (simp_tac (HOLCF_ss addsimps [iterate_Suc]) 1) |
428 ]); |
428 ]); |
429 |
429 |
430 |
430 |
431 qed_goal "hoare_lemma27" Hoare.thy |
431 val hoare_lemma27 = prove_goal Hoare.thy |
432 "(? n.~ b1[iterate(n,g,x)]=TT) ==>\ |
432 "(? n.~ b1[iterate(n,g,x)]=TT) ==>\ |
433 \ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \ |
433 \ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \ |
434 \ --> q[x] = UU" |
434 \ --> q[x] = UU" |
435 (fn prems => |
435 (fn prems => |
436 [ |
436 [ |
463 (asm_simp_tac HOLCF_ss 1) |
463 (asm_simp_tac HOLCF_ss 1) |
464 ]); |
464 ]); |
465 |
465 |
466 (* ------- (! k. b1[iterate(k,g,x)]=TT) ==> q o p = q ----- *) |
466 (* ------- (! k. b1[iterate(k,g,x)]=TT) ==> q o p = q ----- *) |
467 |
467 |
468 qed_goal "hoare_lemma23" Hoare.thy |
468 val hoare_lemma23 = prove_goal Hoare.thy |
469 "(! k. b1[iterate(k,g,x)]=TT) ==> q[p[x]] = q[x]" |
469 "(! k. b1[iterate(k,g,x)]=TT) ==> q[p[x]] = q[x]" |
470 (fn prems => |
470 (fn prems => |
471 [ |
471 [ |
472 (cut_facts_tac prems 1), |
472 (cut_facts_tac prems 1), |
473 (rtac (hoare_lemma16 RS ssubst) 1), |
473 (rtac (hoare_lemma16 RS ssubst) 1), |
486 (rtac refl 1) |
486 (rtac refl 1) |
487 ]); |
487 ]); |
488 |
488 |
489 (* ------------ ? k. ~ b1[iterate(k,g,x)] = TT ==> q o p = q ----- *) |
489 (* ------------ ? k. ~ b1[iterate(k,g,x)] = TT ==> q o p = q ----- *) |
490 |
490 |
491 qed_goal "hoare_lemma29" Hoare.thy |
491 val hoare_lemma29 = prove_goal Hoare.thy |
492 "? k. ~ b1[iterate(k,g,x)] = TT ==> q[p[x]] = q[x]" |
492 "? k. ~ b1[iterate(k,g,x)] = TT ==> q[p[x]] = q[x]" |
493 (fn prems => |
493 (fn prems => |
494 [ |
494 [ |
495 (cut_facts_tac prems 1), |
495 (cut_facts_tac prems 1), |
496 (rtac (hoare_lemma5 RS disjE) 1), |
496 (rtac (hoare_lemma5 RS disjE) 1), |