author | clasohm |
Tue, 24 Oct 1995 14:45:35 +0100 | |
changeset 1294 | 1358dc040edb |
parent 1274 | ea0668a1c0ba |
child 1461 | 6bcb44e4d6e5 |
permissions | -rw-r--r-- |
244 | 1 |
(* Title: HOLCF/ex/hoare.ML |
2 |
ID: $Id$ |
|
3 |
Author: Franz Regensburger |
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
|
5 |
*) |
|
6 |
||
7 |
open Hoare; |
|
8 |
||
9 |
(* --------- pure HOLCF logic, some little lemmas ------ *) |
|
10 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
11 |
val hoare_lemma2 = prove_goal HOLCF.thy "b~=TT ==> b=FF | b=UU" |
244 | 12 |
(fn prems => |
13 |
[ |
|
14 |
(cut_facts_tac prems 1), |
|
15 |
(rtac (Exh_tr RS disjE) 1), |
|
16 |
(fast_tac HOL_cs 1), |
|
17 |
(etac disjE 1), |
|
18 |
(contr_tac 1), |
|
19 |
(fast_tac HOL_cs 1) |
|
20 |
]); |
|
21 |
||
1043 | 22 |
val hoare_lemma3 = prove_goal HOLCF.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
23 |
" (!k.b1`(iterate k g x) = TT) | (? k. b1`(iterate k g x)~=TT)" |
244 | 24 |
(fn prems => |
25 |
[ |
|
26 |
(fast_tac HOL_cs 1) |
|
27 |
]); |
|
28 |
||
1043 | 29 |
val hoare_lemma4 = prove_goal HOLCF.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
30 |
"(? k. b1`(iterate k g x) ~= TT) ==> \ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
31 |
\ ? k. b1`(iterate k g x) = FF | b1`(iterate k g x) = UU" |
244 | 32 |
(fn prems => |
33 |
[ |
|
34 |
(cut_facts_tac prems 1), |
|
35 |
(etac exE 1), |
|
36 |
(rtac exI 1), |
|
37 |
(rtac hoare_lemma2 1), |
|
38 |
(atac 1) |
|
39 |
]); |
|
40 |
||
1043 | 41 |
val hoare_lemma5 = prove_goal HOLCF.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
42 |
"[|(? k. b1`(iterate k g x) ~= TT);\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
43 |
\ k=theleast(%n. b1`(iterate n g x) ~= TT)|] ==> \ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
44 |
\ b1`(iterate k g x)=FF | b1`(iterate k g x)=UU" |
244 | 45 |
(fn prems => |
46 |
[ |
|
47 |
(cut_facts_tac prems 1), |
|
48 |
(hyp_subst_tac 1), |
|
49 |
(rtac hoare_lemma2 1), |
|
50 |
(etac exE 1), |
|
51 |
(etac theleast1 1) |
|
52 |
]); |
|
53 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
54 |
val hoare_lemma6 = prove_goal HOLCF.thy "b=UU ==> b~=TT" |
244 | 55 |
(fn prems => |
56 |
[ |
|
57 |
(cut_facts_tac prems 1), |
|
58 |
(hyp_subst_tac 1), |
|
59 |
(resolve_tac dist_eq_tr 1) |
|
60 |
]); |
|
61 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
62 |
val hoare_lemma7 = prove_goal HOLCF.thy "b=FF ==> b~=TT" |
244 | 63 |
(fn prems => |
64 |
[ |
|
65 |
(cut_facts_tac prems 1), |
|
66 |
(hyp_subst_tac 1), |
|
67 |
(resolve_tac dist_eq_tr 1) |
|
68 |
]); |
|
69 |
||
1043 | 70 |
val hoare_lemma8 = prove_goal HOLCF.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
71 |
"[|(? k. b1`(iterate k g x) ~= TT);\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
72 |
\ k=theleast(%n. b1`(iterate n g x) ~= TT)|] ==> \ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
73 |
\ !m. m < k --> b1`(iterate m g x)=TT" |
244 | 74 |
(fn prems => |
75 |
[ |
|
76 |
(cut_facts_tac prems 1), |
|
77 |
(hyp_subst_tac 1), |
|
78 |
(etac exE 1), |
|
79 |
(strip_tac 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
80 |
(res_inst_tac [("p","b1`(iterate m g x)")] trE 1), |
244 | 81 |
(atac 2), |
82 |
(rtac (le_less_trans RS less_anti_refl) 1), |
|
83 |
(atac 2), |
|
84 |
(rtac theleast2 1), |
|
85 |
(etac hoare_lemma6 1), |
|
86 |
(rtac (le_less_trans RS less_anti_refl) 1), |
|
87 |
(atac 2), |
|
88 |
(rtac theleast2 1), |
|
89 |
(etac hoare_lemma7 1) |
|
90 |
]); |
|
91 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
92 |
|
1043 | 93 |
val hoare_lemma28 = prove_goal HOLCF.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
94 |
"b1`(y::'a)=(UU::tr) ==> b1`UU = UU" |
244 | 95 |
(fn prems => |
96 |
[ |
|
97 |
(cut_facts_tac prems 1), |
|
98 |
(etac (flat_tr RS flat_codom RS disjE) 1), |
|
99 |
(atac 1), |
|
100 |
(etac spec 1) |
|
101 |
]); |
|
102 |
||
103 |
||
104 |
(* ----- access to definitions ----- *) |
|
105 |
||
1043 | 106 |
val p_def2 = prove_goalw Hoare.thy [p_def] |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
107 |
"p = fix`(LAM f x. If b1`x then f`(g`x) else x fi)" |
244 | 108 |
(fn prems => |
109 |
[ |
|
110 |
(rtac refl 1) |
|
111 |
]); |
|
112 |
||
1043 | 113 |
val q_def2 = prove_goalw Hoare.thy [q_def] |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
114 |
"q = fix`(LAM f x. If b1`x orelse b2`x then \ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
115 |
\ f`(g`x) else x fi)" |
244 | 116 |
(fn prems => |
117 |
[ |
|
118 |
(rtac refl 1) |
|
119 |
]); |
|
120 |
||
121 |
||
1043 | 122 |
val p_def3 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
123 |
"p`x = If b1`x then p`(g`x) else x fi" |
244 | 124 |
(fn prems => |
125 |
[ |
|
126 |
(fix_tac3 p_def 1), |
|
1267 | 127 |
(Simp_tac 1) |
244 | 128 |
]); |
129 |
||
1043 | 130 |
val q_def3 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
131 |
"q`x = If b1`x orelse b2`x then q`(g`x) else x fi" |
244 | 132 |
(fn prems => |
133 |
[ |
|
134 |
(fix_tac3 q_def 1), |
|
1267 | 135 |
(Simp_tac 1) |
244 | 136 |
]); |
137 |
||
138 |
(** --------- proves about iterations of p and q ---------- **) |
|
139 |
||
1043 | 140 |
val hoare_lemma9 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
141 |
"(! m. m< Suc k --> b1`(iterate m g x)=TT) -->\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
142 |
\ p`(iterate k g x)=p`x" |
244 | 143 |
(fn prems => |
144 |
[ |
|
145 |
(nat_ind_tac "k" 1), |
|
1267 | 146 |
(simp_tac (!simpset delsimps [less_Suc_eq]) 1), |
147 |
(simp_tac (!simpset delsimps [less_Suc_eq]) 1), |
|
244 | 148 |
(strip_tac 1), |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
149 |
(res_inst_tac [("s","p`(iterate k1 g x)")] trans 1), |
244 | 150 |
(rtac trans 1), |
151 |
(rtac (p_def3 RS sym) 2), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
152 |
(res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1), |
244 | 153 |
(rtac mp 1), |
154 |
(etac spec 1), |
|
1267 | 155 |
(Simp_tac 1), |
244 | 156 |
(simp_tac HOLCF_ss 1), |
157 |
(etac mp 1), |
|
158 |
(strip_tac 1), |
|
159 |
(rtac mp 1), |
|
160 |
(etac spec 1), |
|
161 |
(etac less_trans 1), |
|
1267 | 162 |
(Simp_tac 1) |
244 | 163 |
]); |
1267 | 164 |
trace_simp := false; |
1043 | 165 |
val hoare_lemma24 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
166 |
"(! m. m< Suc k --> b1`(iterate m g x)=TT) --> \ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
167 |
\ q`(iterate k g x)=q`x" |
244 | 168 |
(fn prems => |
169 |
[ |
|
170 |
(nat_ind_tac "k" 1), |
|
1267 | 171 |
(simp_tac (!simpset delsimps [less_Suc_eq]) 1), |
172 |
(simp_tac (!simpset delsimps [less_Suc_eq]) 1), |
|
244 | 173 |
(strip_tac 1), |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
174 |
(res_inst_tac [("s","q`(iterate k1 g x)")] trans 1), |
244 | 175 |
(rtac trans 1), |
176 |
(rtac (q_def3 RS sym) 2), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
177 |
(res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1), |
244 | 178 |
(rtac mp 1), |
179 |
(etac spec 1), |
|
1267 | 180 |
(Simp_tac 1), |
244 | 181 |
(simp_tac HOLCF_ss 1), |
182 |
(etac mp 1), |
|
183 |
(strip_tac 1), |
|
184 |
(rtac mp 1), |
|
185 |
(etac spec 1), |
|
186 |
(etac less_trans 1), |
|
1267 | 187 |
(Simp_tac 1) |
244 | 188 |
]); |
189 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
190 |
(* -------- results about p for case (? k. b1`(iterate k g x)~=TT) ------- *) |
244 | 191 |
|
192 |
||
193 |
val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp)); |
|
194 |
(* |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
195 |
val hoare_lemma10 = "[| ? k. b1`(iterate k g ?x1) ~= TT; |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
196 |
Suc ?k3 = theleast (%n. b1`(iterate n g ?x1) ~= TT) |] ==> |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
197 |
p`(iterate ?k3 g ?x1) = p`?x1" : thm |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
198 |
|
244 | 199 |
*) |
200 |
||
1043 | 201 |
val hoare_lemma11 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
202 |
"(? n.b1`(iterate n g x) ~= TT) ==>\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
203 |
\ k=theleast(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
204 |
\ --> p`x = iterate k g x" |
244 | 205 |
(fn prems => |
206 |
[ |
|
207 |
(cut_facts_tac prems 1), |
|
208 |
(res_inst_tac [("n","k")] natE 1), |
|
209 |
(hyp_subst_tac 1), |
|
1267 | 210 |
(Simp_tac 1), |
244 | 211 |
(strip_tac 1), |
212 |
(etac conjE 1), |
|
213 |
(rtac trans 1), |
|
214 |
(rtac p_def3 1), |
|
1267 | 215 |
(asm_simp_tac HOLCF_ss 1), |
216 |
(eres_inst_tac |
|
217 |
[("s","0"),("t","theleast(%n. b1`(iterate n g x) ~= TT)")] subst 1), |
|
218 |
(Simp_tac 1), |
|
244 | 219 |
(hyp_subst_tac 1), |
220 |
(strip_tac 1), |
|
221 |
(etac conjE 1), |
|
222 |
(rtac trans 1), |
|
223 |
(etac (hoare_lemma10 RS sym) 1), |
|
224 |
(atac 1), |
|
225 |
(rtac trans 1), |
|
226 |
(rtac p_def3 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
227 |
(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1), |
244 | 228 |
(rtac (hoare_lemma8 RS spec RS mp) 1), |
229 |
(atac 1), |
|
230 |
(atac 1), |
|
1267 | 231 |
(Simp_tac 1), |
244 | 232 |
(simp_tac HOLCF_ss 1), |
233 |
(rtac trans 1), |
|
234 |
(rtac p_def3 1), |
|
1267 | 235 |
(simp_tac (!simpset delsimps [iterate_Suc] |
236 |
addsimps [iterate_Suc RS sym]) 1), |
|
237 |
(eres_inst_tac [("s","FF")] ssubst 1), |
|
244 | 238 |
(simp_tac HOLCF_ss 1) |
239 |
]); |
|
240 |
||
1043 | 241 |
val hoare_lemma12 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
242 |
"(? n. b1`(iterate n g x) ~= TT) ==>\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
243 |
\ k=theleast(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
244 |
\ --> p`x = UU" |
244 | 245 |
(fn prems => |
246 |
[ |
|
247 |
(cut_facts_tac prems 1), |
|
248 |
(res_inst_tac [("n","k")] natE 1), |
|
249 |
(hyp_subst_tac 1), |
|
1267 | 250 |
(Simp_tac 1), |
244 | 251 |
(strip_tac 1), |
252 |
(etac conjE 1), |
|
253 |
(rtac trans 1), |
|
254 |
(rtac p_def3 1), |
|
1267 | 255 |
(asm_simp_tac HOLCF_ss 1), |
244 | 256 |
(hyp_subst_tac 1), |
1267 | 257 |
(Simp_tac 1), |
244 | 258 |
(strip_tac 1), |
259 |
(etac conjE 1), |
|
260 |
(rtac trans 1), |
|
261 |
(rtac (hoare_lemma10 RS sym) 1), |
|
262 |
(atac 1), |
|
263 |
(atac 1), |
|
264 |
(rtac trans 1), |
|
265 |
(rtac p_def3 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
266 |
(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1), |
244 | 267 |
(rtac (hoare_lemma8 RS spec RS mp) 1), |
268 |
(atac 1), |
|
269 |
(atac 1), |
|
1267 | 270 |
(Simp_tac 1), |
271 |
(asm_simp_tac HOLCF_ss 1), |
|
244 | 272 |
(rtac trans 1), |
273 |
(rtac p_def3 1), |
|
1267 | 274 |
(asm_simp_tac HOLCF_ss 1) |
244 | 275 |
]); |
276 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
277 |
(* -------- results about p for case (! k. b1`(iterate k g x)=TT) ------- *) |
244 | 278 |
|
1043 | 279 |
val fernpass_lemma = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
280 |
"(! k. b1`(iterate k g x)=TT) ==> !k.p`(iterate k g x) = UU" |
244 | 281 |
(fn prems => |
282 |
[ |
|
283 |
(cut_facts_tac prems 1), |
|
284 |
(rtac (p_def2 RS ssubst) 1), |
|
285 |
(rtac fix_ind 1), |
|
286 |
(rtac adm_all 1), |
|
287 |
(rtac allI 1), |
|
288 |
(rtac adm_eq 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
289 |
(cont_tacR 1), |
244 | 290 |
(rtac allI 1), |
291 |
(rtac (strict_fapp1 RS ssubst) 1), |
|
292 |
(rtac refl 1), |
|
1267 | 293 |
(Simp_tac 1), |
244 | 294 |
(rtac allI 1), |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
295 |
(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1), |
244 | 296 |
(etac spec 1), |
297 |
(asm_simp_tac HOLCF_ss 1), |
|
298 |
(rtac (iterate_Suc RS subst) 1), |
|
299 |
(etac spec 1) |
|
300 |
]); |
|
301 |
||
1043 | 302 |
val hoare_lemma16 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
303 |
"(! k. b1`(iterate k g x)=TT) ==> p`x = UU" |
244 | 304 |
(fn prems => |
305 |
[ |
|
306 |
(cut_facts_tac prems 1), |
|
307 |
(res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
|
308 |
(etac (fernpass_lemma RS spec) 1) |
|
309 |
]); |
|
310 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
311 |
(* -------- results about q for case (! k. b1`(iterate k g x)=TT) ------- *) |
244 | 312 |
|
1043 | 313 |
val hoare_lemma17 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
314 |
"(! k. b1`(iterate k g x)=TT) ==> !k.q`(iterate k g x) = UU" |
244 | 315 |
(fn prems => |
316 |
[ |
|
317 |
(cut_facts_tac prems 1), |
|
318 |
(rtac (q_def2 RS ssubst) 1), |
|
319 |
(rtac fix_ind 1), |
|
320 |
(rtac adm_all 1), |
|
321 |
(rtac allI 1), |
|
322 |
(rtac adm_eq 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
323 |
(cont_tacR 1), |
244 | 324 |
(rtac allI 1), |
325 |
(rtac (strict_fapp1 RS ssubst) 1), |
|
326 |
(rtac refl 1), |
|
327 |
(rtac allI 1), |
|
1267 | 328 |
(Simp_tac 1), |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
329 |
(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1), |
244 | 330 |
(etac spec 1), |
1267 | 331 |
(asm_simp_tac HOLCF_ss 1), |
244 | 332 |
(rtac (iterate_Suc RS subst) 1), |
333 |
(etac spec 1) |
|
334 |
]); |
|
335 |
||
1043 | 336 |
val hoare_lemma18 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
337 |
"(! k. b1`(iterate k g x)=TT) ==> q`x = UU" |
244 | 338 |
(fn prems => |
339 |
[ |
|
340 |
(cut_facts_tac prems 1), |
|
341 |
(res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
|
342 |
(etac (hoare_lemma17 RS spec) 1) |
|
343 |
]); |
|
344 |
||
1043 | 345 |
val hoare_lemma19 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
346 |
"(!k. (b1::'a->tr)`(iterate k g x)=TT) ==> b1`(UU::'a) = UU | (!y.b1`(y::'a)=TT)" |
244 | 347 |
(fn prems => |
348 |
[ |
|
349 |
(cut_facts_tac prems 1), |
|
350 |
(rtac (flat_tr RS flat_codom) 1), |
|
351 |
(res_inst_tac [("t","x1")] (iterate_0 RS subst) 1), |
|
352 |
(etac spec 1) |
|
353 |
]); |
|
354 |
||
1043 | 355 |
val hoare_lemma20 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
356 |
"(! y. b1`(y::'a)=TT) ==> !k.q`(iterate k g (x::'a)) = UU" |
244 | 357 |
(fn prems => |
358 |
[ |
|
359 |
(cut_facts_tac prems 1), |
|
360 |
(rtac (q_def2 RS ssubst) 1), |
|
361 |
(rtac fix_ind 1), |
|
362 |
(rtac adm_all 1), |
|
363 |
(rtac allI 1), |
|
364 |
(rtac adm_eq 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
365 |
(cont_tacR 1), |
244 | 366 |
(rtac allI 1), |
367 |
(rtac (strict_fapp1 RS ssubst) 1), |
|
368 |
(rtac refl 1), |
|
369 |
(rtac allI 1), |
|
1267 | 370 |
(Simp_tac 1), |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
371 |
(res_inst_tac [("s","TT"),("t","b1`(iterate k g (x::'a))")] ssubst 1), |
244 | 372 |
(etac spec 1), |
1267 | 373 |
(asm_simp_tac HOLCF_ss 1), |
244 | 374 |
(rtac (iterate_Suc RS subst) 1), |
375 |
(etac spec 1) |
|
376 |
]); |
|
377 |
||
1043 | 378 |
val hoare_lemma21 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
379 |
"(! y. b1`(y::'a)=TT) ==> q`(x::'a) = UU" |
244 | 380 |
(fn prems => |
381 |
[ |
|
382 |
(cut_facts_tac prems 1), |
|
383 |
(res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
|
384 |
(etac (hoare_lemma20 RS spec) 1) |
|
385 |
]); |
|
386 |
||
1043 | 387 |
val hoare_lemma22 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
388 |
"b1`(UU::'a)=UU ==> q`(UU::'a) = UU" |
244 | 389 |
(fn prems => |
390 |
[ |
|
391 |
(cut_facts_tac prems 1), |
|
392 |
(rtac (q_def3 RS ssubst) 1), |
|
1267 | 393 |
(asm_simp_tac HOLCF_ss 1) |
244 | 394 |
]); |
395 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
396 |
(* -------- results about q for case (? k. b1`(iterate k g x) ~= TT) ------- *) |
244 | 397 |
|
398 |
val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) ); |
|
399 |
(* |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
400 |
val hoare_lemma25 = "[| ? k. b1`(iterate k g ?x1) ~= TT; |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
401 |
Suc ?k3 = theleast (%n. b1`(iterate n g ?x1) ~= TT) |] ==> |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
402 |
q`(iterate ?k3 g ?x1) = q`?x1" : thm |
244 | 403 |
*) |
404 |
||
1043 | 405 |
val hoare_lemma26 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
406 |
"(? n. b1`(iterate n g x)~=TT) ==>\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
407 |
\ k=theleast(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
408 |
\ --> q`x = q`(iterate k g x)" |
244 | 409 |
(fn prems => |
410 |
[ |
|
411 |
(cut_facts_tac prems 1), |
|
412 |
(res_inst_tac [("n","k")] natE 1), |
|
413 |
(hyp_subst_tac 1), |
|
414 |
(strip_tac 1), |
|
1267 | 415 |
(Simp_tac 1), |
244 | 416 |
(hyp_subst_tac 1), |
417 |
(strip_tac 1), |
|
418 |
(etac conjE 1), |
|
419 |
(rtac trans 1), |
|
420 |
(rtac (hoare_lemma25 RS sym) 1), |
|
421 |
(atac 1), |
|
422 |
(atac 1), |
|
423 |
(rtac trans 1), |
|
424 |
(rtac q_def3 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
425 |
(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1), |
244 | 426 |
(rtac (hoare_lemma8 RS spec RS mp) 1), |
427 |
(atac 1), |
|
428 |
(atac 1), |
|
1267 | 429 |
(Simp_tac 1), |
430 |
(simp_tac HOLCF_ss 1) |
|
244 | 431 |
]); |
432 |
||
433 |
||
1043 | 434 |
val hoare_lemma27 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
435 |
"(? n. b1`(iterate n g x) ~= TT) ==>\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
436 |
\ k=theleast(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
437 |
\ --> q`x = UU" |
244 | 438 |
(fn prems => |
439 |
[ |
|
440 |
(cut_facts_tac prems 1), |
|
441 |
(res_inst_tac [("n","k")] natE 1), |
|
442 |
(hyp_subst_tac 1), |
|
1267 | 443 |
(Simp_tac 1), |
244 | 444 |
(strip_tac 1), |
445 |
(etac conjE 1), |
|
446 |
(rtac (q_def3 RS ssubst) 1), |
|
1267 | 447 |
(asm_simp_tac HOLCF_ss 1), |
244 | 448 |
(hyp_subst_tac 1), |
1267 | 449 |
(Simp_tac 1), |
244 | 450 |
(strip_tac 1), |
451 |
(etac conjE 1), |
|
452 |
(rtac trans 1), |
|
453 |
(rtac (hoare_lemma25 RS sym) 1), |
|
454 |
(atac 1), |
|
455 |
(atac 1), |
|
456 |
(rtac trans 1), |
|
457 |
(rtac q_def3 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
458 |
(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1), |
244 | 459 |
(rtac (hoare_lemma8 RS spec RS mp) 1), |
460 |
(atac 1), |
|
461 |
(atac 1), |
|
1267 | 462 |
(Simp_tac 1), |
244 | 463 |
(asm_simp_tac HOLCF_ss 1), |
464 |
(rtac trans 1), |
|
465 |
(rtac q_def3 1), |
|
1267 | 466 |
(asm_simp_tac HOLCF_ss 1) |
244 | 467 |
]); |
468 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
469 |
(* ------- (! k. b1`(iterate k g x)=TT) ==> q o p = q ----- *) |
244 | 470 |
|
1043 | 471 |
val hoare_lemma23 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
472 |
"(! k. b1`(iterate k g x)=TT) ==> q`(p`x) = q`x" |
244 | 473 |
(fn prems => |
474 |
[ |
|
475 |
(cut_facts_tac prems 1), |
|
476 |
(rtac (hoare_lemma16 RS ssubst) 1), |
|
477 |
(atac 1), |
|
478 |
(rtac (hoare_lemma19 RS disjE) 1), |
|
479 |
(atac 1), |
|
480 |
(rtac (hoare_lemma18 RS ssubst) 1), |
|
481 |
(atac 1), |
|
482 |
(rtac (hoare_lemma22 RS ssubst) 1), |
|
483 |
(atac 1), |
|
484 |
(rtac refl 1), |
|
485 |
(rtac (hoare_lemma21 RS ssubst) 1), |
|
486 |
(atac 1), |
|
487 |
(rtac (hoare_lemma21 RS ssubst) 1), |
|
488 |
(atac 1), |
|
489 |
(rtac refl 1) |
|
490 |
]); |
|
491 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
492 |
(* ------------ ? k. b1~(iterate k g x) ~= TT ==> q o p = q ----- *) |
244 | 493 |
|
1043 | 494 |
val hoare_lemma29 = prove_goal Hoare.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
495 |
"? k. b1`(iterate k g x) ~= TT ==> q`(p`x) = q`x" |
244 | 496 |
(fn prems => |
497 |
[ |
|
498 |
(cut_facts_tac prems 1), |
|
499 |
(rtac (hoare_lemma5 RS disjE) 1), |
|
500 |
(atac 1), |
|
501 |
(rtac refl 1), |
|
502 |
(rtac (hoare_lemma11 RS mp RS ssubst) 1), |
|
503 |
(atac 1), |
|
504 |
(rtac conjI 1), |
|
505 |
(rtac refl 1), |
|
506 |
(atac 1), |
|
507 |
(rtac (hoare_lemma26 RS mp RS subst) 1), |
|
508 |
(atac 1), |
|
509 |
(rtac conjI 1), |
|
510 |
(rtac refl 1), |
|
511 |
(atac 1), |
|
512 |
(rtac refl 1), |
|
513 |
(rtac (hoare_lemma12 RS mp RS ssubst) 1), |
|
514 |
(atac 1), |
|
515 |
(rtac conjI 1), |
|
516 |
(rtac refl 1), |
|
517 |
(atac 1), |
|
518 |
(rtac (hoare_lemma22 RS ssubst) 1), |
|
519 |
(rtac (hoare_lemma28 RS ssubst) 1), |
|
520 |
(atac 1), |
|
521 |
(rtac refl 1), |
|
522 |
(rtac sym 1), |
|
523 |
(rtac (hoare_lemma27 RS mp RS ssubst) 1), |
|
524 |
(atac 1), |
|
525 |
(rtac conjI 1), |
|
526 |
(rtac refl 1), |
|
527 |
(atac 1), |
|
528 |
(rtac refl 1) |
|
529 |
]); |
|
530 |
||
531 |
(* ------ the main prove q o p = q ------ *) |
|
532 |
||
1043 | 533 |
val hoare_main = prove_goal Hoare.thy "q oo p = q" |
244 | 534 |
(fn prems => |
535 |
[ |
|
536 |
(rtac ext_cfun 1), |
|
537 |
(rtac (cfcomp2 RS ssubst) 1), |
|
538 |
(rtac (hoare_lemma3 RS disjE) 1), |
|
539 |
(etac hoare_lemma23 1), |
|
540 |
(etac hoare_lemma29 1) |
|
541 |
]); |
|
542 |
||
543 |