author | regensbu |
Thu, 29 Jun 1995 16:28:40 +0200 | |
changeset 1168 | 74be52691d62 |
parent 1043 | ffa68eb2730b |
child 1267 | bca91b4e1710 |
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), |
|
127 |
(simp_tac HOLCF_ss 1) |
|
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), |
|
135 |
(simp_tac HOLCF_ss 1) |
|
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), |
|
146 |
(simp_tac iterate_ss 1), |
|
147 |
(simp_tac iterate_ss 1), |
|
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), |
|
155 |
(simp_tac nat_ss 1), |
|
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), |
|
162 |
(simp_tac nat_ss 1) |
|
163 |
]); |
|
164 |
||
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), |
|
171 |
(simp_tac iterate_ss 1), |
|
172 |
(simp_tac iterate_ss 1), |
|
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), |
|
180 |
(simp_tac nat_ss 1), |
|
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), |
|
187 |
(simp_tac nat_ss 1) |
|
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), |
|
210 |
(simp_tac iterate_ss 1), |
|
211 |
(strip_tac 1), |
|
212 |
(etac conjE 1), |
|
213 |
(rtac trans 1), |
|
214 |
(rtac p_def3 1), |
|
215 |
(asm_simp_tac HOLCF_ss 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
216 |
(eres_inst_tac [("s","0"),("t","theleast(%n. b1`(iterate n g x) ~= TT)")] |
244 | 217 |
subst 1), |
218 |
(simp_tac iterate_ss 1), |
|
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), |
|
231 |
(simp_tac nat_ss 1), |
|
232 |
(simp_tac HOLCF_ss 1), |
|
233 |
(rtac trans 1), |
|
234 |
(rtac p_def3 1), |
|
235 |
(simp_tac (HOLCF_ss addsimps [iterate_Suc RS sym]) 1), |
|
236 |
(eres_inst_tac [("s","FF")] ssubst 1), |
|
237 |
(simp_tac HOLCF_ss 1) |
|
238 |
]); |
|
239 |
||
1043 | 240 |
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
|
241 |
"(? 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
|
242 |
\ 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
|
243 |
\ --> p`x = UU" |
244 | 244 |
(fn prems => |
245 |
[ |
|
246 |
(cut_facts_tac prems 1), |
|
247 |
(res_inst_tac [("n","k")] natE 1), |
|
248 |
(hyp_subst_tac 1), |
|
249 |
(simp_tac iterate_ss 1), |
|
250 |
(strip_tac 1), |
|
251 |
(etac conjE 1), |
|
252 |
(rtac trans 1), |
|
253 |
(rtac p_def3 1), |
|
254 |
(asm_simp_tac HOLCF_ss 1), |
|
255 |
(hyp_subst_tac 1), |
|
256 |
(simp_tac iterate_ss 1), |
|
257 |
(strip_tac 1), |
|
258 |
(etac conjE 1), |
|
259 |
(rtac trans 1), |
|
260 |
(rtac (hoare_lemma10 RS sym) 1), |
|
261 |
(atac 1), |
|
262 |
(atac 1), |
|
263 |
(rtac trans 1), |
|
264 |
(rtac p_def3 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
265 |
(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1), |
244 | 266 |
(rtac (hoare_lemma8 RS spec RS mp) 1), |
267 |
(atac 1), |
|
268 |
(atac 1), |
|
269 |
(simp_tac nat_ss 1), |
|
270 |
(asm_simp_tac HOLCF_ss 1), |
|
271 |
(rtac trans 1), |
|
272 |
(rtac p_def3 1), |
|
273 |
(asm_simp_tac HOLCF_ss 1) |
|
274 |
]); |
|
275 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
276 |
(* -------- results about p for case (! k. b1`(iterate k g x)=TT) ------- *) |
244 | 277 |
|
1043 | 278 |
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
|
279 |
"(! k. b1`(iterate k g x)=TT) ==> !k.p`(iterate k g x) = UU" |
244 | 280 |
(fn prems => |
281 |
[ |
|
282 |
(cut_facts_tac prems 1), |
|
283 |
(rtac (p_def2 RS ssubst) 1), |
|
284 |
(rtac fix_ind 1), |
|
285 |
(rtac adm_all 1), |
|
286 |
(rtac allI 1), |
|
287 |
(rtac adm_eq 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
288 |
(cont_tacR 1), |
244 | 289 |
(rtac allI 1), |
290 |
(rtac (strict_fapp1 RS ssubst) 1), |
|
291 |
(rtac refl 1), |
|
292 |
(simp_tac iterate_ss 1), |
|
293 |
(rtac allI 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
294 |
(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1), |
244 | 295 |
(etac spec 1), |
296 |
(asm_simp_tac HOLCF_ss 1), |
|
297 |
(rtac (iterate_Suc RS subst) 1), |
|
298 |
(etac spec 1) |
|
299 |
]); |
|
300 |
||
1043 | 301 |
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
|
302 |
"(! k. b1`(iterate k g x)=TT) ==> p`x = UU" |
244 | 303 |
(fn prems => |
304 |
[ |
|
305 |
(cut_facts_tac prems 1), |
|
306 |
(res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
|
307 |
(etac (fernpass_lemma RS spec) 1) |
|
308 |
]); |
|
309 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
310 |
(* -------- results about q for case (! k. b1`(iterate k g x)=TT) ------- *) |
244 | 311 |
|
1043 | 312 |
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
|
313 |
"(! k. b1`(iterate k g x)=TT) ==> !k.q`(iterate k g x) = UU" |
244 | 314 |
(fn prems => |
315 |
[ |
|
316 |
(cut_facts_tac prems 1), |
|
317 |
(rtac (q_def2 RS ssubst) 1), |
|
318 |
(rtac fix_ind 1), |
|
319 |
(rtac adm_all 1), |
|
320 |
(rtac allI 1), |
|
321 |
(rtac adm_eq 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
322 |
(cont_tacR 1), |
244 | 323 |
(rtac allI 1), |
324 |
(rtac (strict_fapp1 RS ssubst) 1), |
|
325 |
(rtac refl 1), |
|
326 |
(rtac allI 1), |
|
327 |
(simp_tac iterate_ss 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
328 |
(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1), |
244 | 329 |
(etac spec 1), |
330 |
(asm_simp_tac HOLCF_ss 1), |
|
331 |
(rtac (iterate_Suc RS subst) 1), |
|
332 |
(etac spec 1) |
|
333 |
]); |
|
334 |
||
1043 | 335 |
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
|
336 |
"(! k. b1`(iterate k g x)=TT) ==> q`x = UU" |
244 | 337 |
(fn prems => |
338 |
[ |
|
339 |
(cut_facts_tac prems 1), |
|
340 |
(res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
|
341 |
(etac (hoare_lemma17 RS spec) 1) |
|
342 |
]); |
|
343 |
||
1043 | 344 |
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
|
345 |
"(!k. (b1::'a->tr)`(iterate k g x)=TT) ==> b1`(UU::'a) = UU | (!y.b1`(y::'a)=TT)" |
244 | 346 |
(fn prems => |
347 |
[ |
|
348 |
(cut_facts_tac prems 1), |
|
349 |
(rtac (flat_tr RS flat_codom) 1), |
|
350 |
(res_inst_tac [("t","x1")] (iterate_0 RS subst) 1), |
|
351 |
(etac spec 1) |
|
352 |
]); |
|
353 |
||
1043 | 354 |
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
|
355 |
"(! y. b1`(y::'a)=TT) ==> !k.q`(iterate k g (x::'a)) = UU" |
244 | 356 |
(fn prems => |
357 |
[ |
|
358 |
(cut_facts_tac prems 1), |
|
359 |
(rtac (q_def2 RS ssubst) 1), |
|
360 |
(rtac fix_ind 1), |
|
361 |
(rtac adm_all 1), |
|
362 |
(rtac allI 1), |
|
363 |
(rtac adm_eq 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
364 |
(cont_tacR 1), |
244 | 365 |
(rtac allI 1), |
366 |
(rtac (strict_fapp1 RS ssubst) 1), |
|
367 |
(rtac refl 1), |
|
368 |
(rtac allI 1), |
|
369 |
(simp_tac iterate_ss 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
370 |
(res_inst_tac [("s","TT"),("t","b1`(iterate k g (x::'a))")] ssubst 1), |
244 | 371 |
(etac spec 1), |
372 |
(asm_simp_tac HOLCF_ss 1), |
|
373 |
(rtac (iterate_Suc RS subst) 1), |
|
374 |
(etac spec 1) |
|
375 |
]); |
|
376 |
||
1043 | 377 |
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
|
378 |
"(! y. b1`(y::'a)=TT) ==> q`(x::'a) = UU" |
244 | 379 |
(fn prems => |
380 |
[ |
|
381 |
(cut_facts_tac prems 1), |
|
382 |
(res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1), |
|
383 |
(etac (hoare_lemma20 RS spec) 1) |
|
384 |
]); |
|
385 |
||
1043 | 386 |
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
|
387 |
"b1`(UU::'a)=UU ==> q`(UU::'a) = UU" |
244 | 388 |
(fn prems => |
389 |
[ |
|
390 |
(cut_facts_tac prems 1), |
|
391 |
(rtac (q_def3 RS ssubst) 1), |
|
392 |
(asm_simp_tac HOLCF_ss 1) |
|
393 |
]); |
|
394 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
395 |
(* -------- results about q for case (? k. b1`(iterate k g x) ~= TT) ------- *) |
244 | 396 |
|
397 |
val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) ); |
|
398 |
(* |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
399 |
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
|
400 |
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
|
401 |
q`(iterate ?k3 g ?x1) = q`?x1" : thm |
244 | 402 |
*) |
403 |
||
1043 | 404 |
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
|
405 |
"(? 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
|
406 |
\ 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
|
407 |
\ --> q`x = q`(iterate k g x)" |
244 | 408 |
(fn prems => |
409 |
[ |
|
410 |
(cut_facts_tac prems 1), |
|
411 |
(res_inst_tac [("n","k")] natE 1), |
|
412 |
(hyp_subst_tac 1), |
|
413 |
(strip_tac 1), |
|
414 |
(simp_tac iterate_ss 1), |
|
415 |
(hyp_subst_tac 1), |
|
416 |
(strip_tac 1), |
|
417 |
(etac conjE 1), |
|
418 |
(rtac trans 1), |
|
419 |
(rtac (hoare_lemma25 RS sym) 1), |
|
420 |
(atac 1), |
|
421 |
(atac 1), |
|
422 |
(rtac trans 1), |
|
423 |
(rtac q_def3 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
424 |
(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1), |
244 | 425 |
(rtac (hoare_lemma8 RS spec RS mp) 1), |
426 |
(atac 1), |
|
427 |
(atac 1), |
|
428 |
(simp_tac nat_ss 1), |
|
429 |
(simp_tac (HOLCF_ss addsimps [iterate_Suc]) 1) |
|
430 |
]); |
|
431 |
||
432 |
||
1043 | 433 |
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
|
434 |
"(? 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
|
435 |
\ 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
|
436 |
\ --> q`x = UU" |
244 | 437 |
(fn prems => |
438 |
[ |
|
439 |
(cut_facts_tac prems 1), |
|
440 |
(res_inst_tac [("n","k")] natE 1), |
|
441 |
(hyp_subst_tac 1), |
|
442 |
(simp_tac iterate_ss 1), |
|
443 |
(strip_tac 1), |
|
444 |
(etac conjE 1), |
|
445 |
(rtac (q_def3 RS ssubst) 1), |
|
446 |
(asm_simp_tac HOLCF_ss 1), |
|
447 |
(hyp_subst_tac 1), |
|
448 |
(simp_tac iterate_ss 1), |
|
449 |
(strip_tac 1), |
|
450 |
(etac conjE 1), |
|
451 |
(rtac trans 1), |
|
452 |
(rtac (hoare_lemma25 RS sym) 1), |
|
453 |
(atac 1), |
|
454 |
(atac 1), |
|
455 |
(rtac trans 1), |
|
456 |
(rtac q_def3 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
457 |
(res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1), |
244 | 458 |
(rtac (hoare_lemma8 RS spec RS mp) 1), |
459 |
(atac 1), |
|
460 |
(atac 1), |
|
461 |
(simp_tac nat_ss 1), |
|
462 |
(asm_simp_tac HOLCF_ss 1), |
|
463 |
(rtac trans 1), |
|
464 |
(rtac q_def3 1), |
|
465 |
(asm_simp_tac HOLCF_ss 1) |
|
466 |
]); |
|
467 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
468 |
(* ------- (! k. b1`(iterate k g x)=TT) ==> q o p = q ----- *) |
244 | 469 |
|
1043 | 470 |
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
|
471 |
"(! k. b1`(iterate k g x)=TT) ==> q`(p`x) = q`x" |
244 | 472 |
(fn prems => |
473 |
[ |
|
474 |
(cut_facts_tac prems 1), |
|
475 |
(rtac (hoare_lemma16 RS ssubst) 1), |
|
476 |
(atac 1), |
|
477 |
(rtac (hoare_lemma19 RS disjE) 1), |
|
478 |
(atac 1), |
|
479 |
(rtac (hoare_lemma18 RS ssubst) 1), |
|
480 |
(atac 1), |
|
481 |
(rtac (hoare_lemma22 RS ssubst) 1), |
|
482 |
(atac 1), |
|
483 |
(rtac refl 1), |
|
484 |
(rtac (hoare_lemma21 RS ssubst) 1), |
|
485 |
(atac 1), |
|
486 |
(rtac (hoare_lemma21 RS ssubst) 1), |
|
487 |
(atac 1), |
|
488 |
(rtac refl 1) |
|
489 |
]); |
|
490 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
491 |
(* ------------ ? k. b1~(iterate k g x) ~= TT ==> q o p = q ----- *) |
244 | 492 |
|
1043 | 493 |
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
|
494 |
"? k. b1`(iterate k g x) ~= TT ==> q`(p`x) = q`x" |
244 | 495 |
(fn prems => |
496 |
[ |
|
497 |
(cut_facts_tac prems 1), |
|
498 |
(rtac (hoare_lemma5 RS disjE) 1), |
|
499 |
(atac 1), |
|
500 |
(rtac refl 1), |
|
501 |
(rtac (hoare_lemma11 RS mp RS ssubst) 1), |
|
502 |
(atac 1), |
|
503 |
(rtac conjI 1), |
|
504 |
(rtac refl 1), |
|
505 |
(atac 1), |
|
506 |
(rtac (hoare_lemma26 RS mp RS subst) 1), |
|
507 |
(atac 1), |
|
508 |
(rtac conjI 1), |
|
509 |
(rtac refl 1), |
|
510 |
(atac 1), |
|
511 |
(rtac refl 1), |
|
512 |
(rtac (hoare_lemma12 RS mp RS ssubst) 1), |
|
513 |
(atac 1), |
|
514 |
(rtac conjI 1), |
|
515 |
(rtac refl 1), |
|
516 |
(atac 1), |
|
517 |
(rtac (hoare_lemma22 RS ssubst) 1), |
|
518 |
(rtac (hoare_lemma28 RS ssubst) 1), |
|
519 |
(atac 1), |
|
520 |
(rtac refl 1), |
|
521 |
(rtac sym 1), |
|
522 |
(rtac (hoare_lemma27 RS mp RS ssubst) 1), |
|
523 |
(atac 1), |
|
524 |
(rtac conjI 1), |
|
525 |
(rtac refl 1), |
|
526 |
(atac 1), |
|
527 |
(rtac refl 1) |
|
528 |
]); |
|
529 |
||
530 |
(* ------ the main prove q o p = q ------ *) |
|
531 |
||
1043 | 532 |
val hoare_main = prove_goal Hoare.thy "q oo p = q" |
244 | 533 |
(fn prems => |
534 |
[ |
|
535 |
(rtac ext_cfun 1), |
|
536 |
(rtac (cfcomp2 RS ssubst) 1), |
|
537 |
(rtac (hoare_lemma3 RS disjE) 1), |
|
538 |
(etac hoare_lemma23 1), |
|
539 |
(etac hoare_lemma29 1) |
|
540 |
]); |
|
541 |
||
542 |