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