1 (* Title: HOLCF/Dlist.ML |
|
2 Author: Franz Regensburger |
|
3 ID: $ $ |
|
4 Copyright 1994 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for dlist.thy |
|
7 *) |
|
8 |
|
9 open Dlist; |
|
10 |
|
11 Delsimps (ex_simps @ all_simps); |
|
12 |
|
13 (* ------------------------------------------------------------------------*) |
|
14 (* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict *) |
|
15 (* ------------------------------------------------------------------------*) |
|
16 |
|
17 val dlist_iso_strict= dlist_rep_iso RS (dlist_abs_iso RS |
|
18 (allI RSN (2,allI RS iso_strict))); |
|
19 |
|
20 val dlist_rews = [dlist_iso_strict RS conjunct1, |
|
21 dlist_iso_strict RS conjunct2]; |
|
22 |
|
23 (* ------------------------------------------------------------------------*) |
|
24 (* Properties of dlist_copy *) |
|
25 (* ------------------------------------------------------------------------*) |
|
26 |
|
27 val temp = prove_goalw Dlist.thy [dlist_copy_def] "dlist_copy`f`UU=UU" |
|
28 (fn prems => |
|
29 [ |
|
30 (asm_simp_tac (!simpset addsimps |
|
31 (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1) |
|
32 ]); |
|
33 |
|
34 val dlist_copy = [temp]; |
|
35 |
|
36 |
|
37 val temp = prove_goalw Dlist.thy [dlist_copy_def,dnil_def] |
|
38 "dlist_copy`f`dnil=dnil" |
|
39 (fn prems => |
|
40 [ |
|
41 (asm_simp_tac (!simpset addsimps |
|
42 (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1) |
|
43 ]); |
|
44 |
|
45 val dlist_copy = temp :: dlist_copy; |
|
46 |
|
47 |
|
48 val temp = prove_goalw Dlist.thy [dlist_copy_def,dcons_def] |
|
49 "xl~=UU ==> dlist_copy`f`(dcons`x`xl)= dcons`x`(f`xl)" |
|
50 (fn prems => |
|
51 [ |
|
52 (cut_facts_tac prems 1), |
|
53 (asm_simp_tac (!simpset addsimps |
|
54 (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1), |
|
55 (case_tac "x=UU" 1), |
|
56 (Asm_simp_tac 1), |
|
57 (asm_simp_tac (!simpset addsimps [defined_spair]) 1) |
|
58 ]); |
|
59 |
|
60 val dlist_copy = temp :: dlist_copy; |
|
61 |
|
62 val dlist_rews = dlist_copy @ dlist_rews; |
|
63 |
|
64 (* ------------------------------------------------------------------------*) |
|
65 (* Exhaustion and elimination for dlists *) |
|
66 (* ------------------------------------------------------------------------*) |
|
67 |
|
68 qed_goalw "Exh_dlist" Dlist.thy [dcons_def,dnil_def] |
|
69 "l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons`x`xl)" |
|
70 (fn prems => |
|
71 [ |
|
72 (Simp_tac 1), |
|
73 (rtac (dlist_rep_iso RS subst) 1), |
|
74 (res_inst_tac [("p","dlist_rep`l")] ssumE 1), |
|
75 (rtac disjI1 1), |
|
76 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
77 (rtac disjI2 1), |
|
78 (rtac disjI1 1), |
|
79 (res_inst_tac [("p","x")] oneE 1), |
|
80 (contr_tac 1), |
|
81 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
82 (rtac disjI2 1), |
|
83 (rtac disjI2 1), |
|
84 (res_inst_tac [("p","y")] sprodE 1), |
|
85 (contr_tac 1), |
|
86 (rtac exI 1), |
|
87 (rtac exI 1), |
|
88 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
89 (fast_tac HOL_cs 1) |
|
90 ]); |
|
91 |
|
92 |
|
93 qed_goal "dlistE" Dlist.thy |
|
94 "[| l=UU ==> Q; l=dnil ==> Q;!!x xl.[|l=dcons`x`xl;x~=UU;xl~=UU|]==>Q|]==>Q" |
|
95 (fn prems => |
|
96 [ |
|
97 (rtac (Exh_dlist RS disjE) 1), |
|
98 (eresolve_tac prems 1), |
|
99 (etac disjE 1), |
|
100 (eresolve_tac prems 1), |
|
101 (etac exE 1), |
|
102 (etac exE 1), |
|
103 (resolve_tac prems 1), |
|
104 (fast_tac HOL_cs 1), |
|
105 (fast_tac HOL_cs 1), |
|
106 (fast_tac HOL_cs 1) |
|
107 ]); |
|
108 |
|
109 (* ------------------------------------------------------------------------*) |
|
110 (* Properties of dlist_when *) |
|
111 (* ------------------------------------------------------------------------*) |
|
112 |
|
113 val temp = prove_goalw Dlist.thy [dlist_when_def] "dlist_when`f1`f2`UU=UU" |
|
114 (fn prems => |
|
115 [ |
|
116 (asm_simp_tac (!simpset addsimps [dlist_iso_strict]) 1) |
|
117 ]); |
|
118 |
|
119 val dlist_when = [temp]; |
|
120 |
|
121 val temp = prove_goalw Dlist.thy [dlist_when_def,dnil_def] |
|
122 "dlist_when`f1`f2`dnil= f1" |
|
123 (fn prems => |
|
124 [ |
|
125 (asm_simp_tac (!simpset addsimps [dlist_abs_iso]) 1) |
|
126 ]); |
|
127 |
|
128 val dlist_when = temp::dlist_when; |
|
129 |
|
130 val temp = prove_goalw Dlist.thy [dlist_when_def,dcons_def] |
|
131 "[|x~=UU;xl~=UU|] ==> dlist_when`f1`f2`(dcons`x`xl)= f2`x`xl" |
|
132 (fn prems => |
|
133 [ |
|
134 (cut_facts_tac prems 1), |
|
135 (asm_simp_tac (!simpset addsimps [dlist_abs_iso,defined_spair]) 1) |
|
136 ]); |
|
137 |
|
138 val dlist_when = temp::dlist_when; |
|
139 |
|
140 val dlist_rews = dlist_when @ dlist_rews; |
|
141 |
|
142 (* ------------------------------------------------------------------------*) |
|
143 (* Rewrites for discriminators and selectors *) |
|
144 (* ------------------------------------------------------------------------*) |
|
145 |
|
146 fun prover defs thm = prove_goalw Dlist.thy defs thm |
|
147 (fn prems => |
|
148 [ |
|
149 (simp_tac (!simpset addsimps dlist_rews) 1) |
|
150 ]); |
|
151 |
|
152 val dlist_discsel = [ |
|
153 prover [is_dnil_def] "is_dnil`UU=UU", |
|
154 prover [is_dcons_def] "is_dcons`UU=UU", |
|
155 prover [dhd_def] "dhd`UU=UU", |
|
156 prover [dtl_def] "dtl`UU=UU" |
|
157 ]; |
|
158 |
|
159 fun prover defs thm = prove_goalw Dlist.thy defs thm |
|
160 (fn prems => |
|
161 [ |
|
162 (cut_facts_tac prems 1), |
|
163 (asm_simp_tac (!simpset addsimps dlist_rews) 1) |
|
164 ]); |
|
165 |
|
166 val dlist_discsel = [ |
|
167 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def] |
|
168 "is_dnil`dnil=TT", |
|
169 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def] |
|
170 "[|x~=UU;xl~=UU|] ==> is_dnil`(dcons`x`xl)=FF", |
|
171 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def] |
|
172 "is_dcons`dnil=FF", |
|
173 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def] |
|
174 "[|x~=UU;xl~=UU|] ==> is_dcons`(dcons`x`xl)=TT", |
|
175 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def] |
|
176 "dhd`dnil=UU", |
|
177 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def] |
|
178 "[|x~=UU;xl~=UU|] ==> dhd`(dcons`x`xl)=x", |
|
179 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def] |
|
180 "dtl`dnil=UU", |
|
181 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def] |
|
182 "[|x~=UU;xl~=UU|] ==> dtl`(dcons`x`xl)=xl"] @ dlist_discsel; |
|
183 |
|
184 val dlist_rews = dlist_discsel @ dlist_rews; |
|
185 |
|
186 (* ------------------------------------------------------------------------*) |
|
187 (* Definedness and strictness *) |
|
188 (* ------------------------------------------------------------------------*) |
|
189 |
|
190 fun prover contr thm = prove_goal Dlist.thy thm |
|
191 (fn prems => |
|
192 [ |
|
193 (res_inst_tac [("P1",contr)] classical2 1), |
|
194 (simp_tac (!simpset addsimps dlist_rews) 1), |
|
195 (dtac sym 1), |
|
196 (Asm_simp_tac 1), |
|
197 (simp_tac (!simpset addsimps (prems @ dlist_rews)) 1) |
|
198 ]); |
|
199 |
|
200 |
|
201 val dlist_constrdef = [ |
|
202 prover "is_dnil`(UU::'a dlist) ~= UU" "dnil~=(UU::'a dlist)", |
|
203 prover "is_dcons`(UU::'a dlist) ~= UU" |
|
204 "[|x~=UU;xl~=UU|]==>dcons`(x::'a)`xl ~= UU" |
|
205 ]; |
|
206 |
|
207 |
|
208 fun prover defs thm = prove_goalw Dlist.thy defs thm |
|
209 (fn prems => |
|
210 [ |
|
211 (simp_tac (!simpset addsimps dlist_rews) 1) |
|
212 ]); |
|
213 |
|
214 val dlist_constrdef = [ |
|
215 prover [dcons_def] "dcons`UU`xl=UU", |
|
216 prover [dcons_def] "dcons`x`UU=UU" |
|
217 ] @ dlist_constrdef; |
|
218 |
|
219 val dlist_rews = dlist_constrdef @ dlist_rews; |
|
220 |
|
221 |
|
222 (* ------------------------------------------------------------------------*) |
|
223 (* Distinctness wrt. << and = *) |
|
224 (* ------------------------------------------------------------------------*) |
|
225 |
|
226 val temp = prove_goal Dlist.thy "~dnil << dcons`(x::'a)`xl" |
|
227 (fn prems => |
|
228 [ |
|
229 (res_inst_tac [("P1","TT << FF")] classical2 1), |
|
230 (resolve_tac dist_less_tr 1), |
|
231 (dres_inst_tac [("fo","is_dnil")] monofun_cfun_arg 1), |
|
232 (etac box_less 1), |
|
233 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
234 (case_tac "(x::'a)=UU" 1), |
|
235 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
236 (case_tac "(xl ::'a dlist)=UU" 1), |
|
237 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
238 (asm_simp_tac (!simpset addsimps dlist_rews) 1) |
|
239 ]); |
|
240 |
|
241 val dlist_dist_less = [temp]; |
|
242 |
|
243 val temp = prove_goal Dlist.thy "[|x~=UU;xl~=UU|]==>~ dcons`x`xl << dnil" |
|
244 (fn prems => |
|
245 [ |
|
246 (cut_facts_tac prems 1), |
|
247 (res_inst_tac [("P1","TT << FF")] classical2 1), |
|
248 (resolve_tac dist_less_tr 1), |
|
249 (dres_inst_tac [("fo","is_dcons")] monofun_cfun_arg 1), |
|
250 (etac box_less 1), |
|
251 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
252 (asm_simp_tac (!simpset addsimps dlist_rews) 1) |
|
253 ]); |
|
254 |
|
255 val dlist_dist_less = temp::dlist_dist_less; |
|
256 |
|
257 val temp = prove_goal Dlist.thy "dnil ~= dcons`x`xl" |
|
258 (fn prems => |
|
259 [ |
|
260 (case_tac "x=UU" 1), |
|
261 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
262 (case_tac "xl=UU" 1), |
|
263 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
264 (res_inst_tac [("P1","TT = FF")] classical2 1), |
|
265 (resolve_tac dist_eq_tr 1), |
|
266 (dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1), |
|
267 (etac box_equals 1), |
|
268 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
269 (asm_simp_tac (!simpset addsimps dlist_rews) 1) |
|
270 ]); |
|
271 |
|
272 val dlist_dist_eq = [temp,temp RS not_sym]; |
|
273 |
|
274 val dlist_rews = dlist_dist_less @ dlist_dist_eq @ dlist_rews; |
|
275 |
|
276 (* ------------------------------------------------------------------------*) |
|
277 (* Invertibility *) |
|
278 (* ------------------------------------------------------------------------*) |
|
279 |
|
280 val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\ |
|
281 \ dcons`x1`x2 << dcons`y1`y2 |] ==> x1<< y1 & x2 << y2" |
|
282 (fn prems => |
|
283 [ |
|
284 (cut_facts_tac prems 1), |
|
285 (rtac conjI 1), |
|
286 (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1), |
|
287 (etac box_less 1), |
|
288 (asm_simp_tac (!simpset addsimps dlist_when) 1), |
|
289 (asm_simp_tac (!simpset addsimps dlist_when) 1), |
|
290 (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1), |
|
291 (etac box_less 1), |
|
292 (asm_simp_tac (!simpset addsimps dlist_when) 1), |
|
293 (asm_simp_tac (!simpset addsimps dlist_when) 1) |
|
294 ]); |
|
295 |
|
296 val dlist_invert =[temp]; |
|
297 |
|
298 (* ------------------------------------------------------------------------*) |
|
299 (* Injectivity *) |
|
300 (* ------------------------------------------------------------------------*) |
|
301 |
|
302 val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\ |
|
303 \ dcons`x1`x2 = dcons`y1`y2 |] ==> x1= y1 & x2 = y2" |
|
304 (fn prems => |
|
305 [ |
|
306 (cut_facts_tac prems 1), |
|
307 (rtac conjI 1), |
|
308 (dres_inst_tac [("f","dlist_when`UU`(LAM x l.x)")] cfun_arg_cong 1), |
|
309 (etac box_equals 1), |
|
310 (asm_simp_tac (!simpset addsimps dlist_when) 1), |
|
311 (asm_simp_tac (!simpset addsimps dlist_when) 1), |
|
312 (dres_inst_tac [("f","dlist_when`UU`(LAM x l.l)")] cfun_arg_cong 1), |
|
313 (etac box_equals 1), |
|
314 (asm_simp_tac (!simpset addsimps dlist_when) 1), |
|
315 (asm_simp_tac (!simpset addsimps dlist_when) 1) |
|
316 ]); |
|
317 |
|
318 val dlist_inject = [temp]; |
|
319 |
|
320 |
|
321 (* ------------------------------------------------------------------------*) |
|
322 (* definedness for discriminators and selectors *) |
|
323 (* ------------------------------------------------------------------------*) |
|
324 |
|
325 fun prover thm = prove_goal Dlist.thy thm |
|
326 (fn prems => |
|
327 [ |
|
328 (cut_facts_tac prems 1), |
|
329 (rtac dlistE 1), |
|
330 (contr_tac 1), |
|
331 (REPEAT (asm_simp_tac (!simpset addsimps dlist_discsel) 1)) |
|
332 ]); |
|
333 |
|
334 val dlist_discsel_def = |
|
335 [ |
|
336 prover "l~=UU ==> is_dnil`l~=UU", |
|
337 prover "l~=UU ==> is_dcons`l~=UU" |
|
338 ]; |
|
339 |
|
340 val dlist_rews = dlist_discsel_def @ dlist_rews; |
|
341 |
|
342 (* ------------------------------------------------------------------------*) |
|
343 (* enhance the simplifier *) |
|
344 (* ------------------------------------------------------------------------*) |
|
345 |
|
346 qed_goal "dhd2" Dlist.thy "xl~=UU ==> dhd`(dcons`x`xl)=x" |
|
347 (fn prems => |
|
348 [ |
|
349 (cut_facts_tac prems 1), |
|
350 (case_tac "x=UU" 1), |
|
351 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
352 (asm_simp_tac (!simpset addsimps dlist_rews) 1) |
|
353 ]); |
|
354 |
|
355 qed_goal "dtl2" Dlist.thy "x~=UU ==> dtl`(dcons`x`xl)=xl" |
|
356 (fn prems => |
|
357 [ |
|
358 (cut_facts_tac prems 1), |
|
359 (case_tac "xl=UU" 1), |
|
360 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
361 (asm_simp_tac (!simpset addsimps dlist_rews) 1) |
|
362 ]); |
|
363 |
|
364 val dlist_rews = dhd2 :: dtl2 :: dlist_rews; |
|
365 |
|
366 (* ------------------------------------------------------------------------*) |
|
367 (* Properties dlist_take *) |
|
368 (* ------------------------------------------------------------------------*) |
|
369 |
|
370 val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take n`UU=UU" |
|
371 (fn prems => |
|
372 [ |
|
373 (res_inst_tac [("n","n")] natE 1), |
|
374 (Asm_simp_tac 1), |
|
375 (Asm_simp_tac 1), |
|
376 (simp_tac (!simpset addsimps dlist_rews) 1) |
|
377 ]); |
|
378 |
|
379 val dlist_take = [temp]; |
|
380 |
|
381 val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take 0`xs=UU" |
|
382 (fn prems => |
|
383 [ |
|
384 (Asm_simp_tac 1) |
|
385 ]); |
|
386 |
|
387 val dlist_take = temp::dlist_take; |
|
388 |
|
389 val temp = prove_goalw Dlist.thy [dlist_take_def] |
|
390 "dlist_take (Suc n)`dnil=dnil" |
|
391 (fn prems => |
|
392 [ |
|
393 (Asm_simp_tac 1), |
|
394 (simp_tac (!simpset addsimps dlist_rews) 1) |
|
395 ]); |
|
396 |
|
397 val dlist_take = temp::dlist_take; |
|
398 |
|
399 val temp = prove_goalw Dlist.thy [dlist_take_def] |
|
400 "dlist_take (Suc n)`(dcons`x`xl)= dcons`x`(dlist_take n`xl)" |
|
401 (fn prems => |
|
402 [ |
|
403 (case_tac "x=UU" 1), |
|
404 (Asm_simp_tac 1), |
|
405 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
406 (case_tac "xl=UU" 1), |
|
407 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
408 (Asm_simp_tac 1), |
|
409 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
410 (res_inst_tac [("n","n")] natE 1), |
|
411 (Asm_simp_tac 1), |
|
412 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
413 (Asm_simp_tac 1), |
|
414 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
415 (Asm_simp_tac 1), |
|
416 (asm_simp_tac (!simpset addsimps dlist_rews) 1) |
|
417 ]); |
|
418 |
|
419 val dlist_take = temp::dlist_take; |
|
420 |
|
421 val dlist_rews = dlist_take @ dlist_rews; |
|
422 |
|
423 (* ------------------------------------------------------------------------*) |
|
424 (* take lemma for dlists *) |
|
425 (* ------------------------------------------------------------------------*) |
|
426 |
|
427 fun prover reach defs thm = prove_goalw Dlist.thy defs thm |
|
428 (fn prems => |
|
429 [ |
|
430 (res_inst_tac [("t","l1")] (reach RS subst) 1), |
|
431 (res_inst_tac [("t","l2")] (reach RS subst) 1), |
|
432 (stac fix_def2 1), |
|
433 (stac contlub_cfun_fun 1), |
|
434 (rtac is_chain_iterate 1), |
|
435 (stac contlub_cfun_fun 1), |
|
436 (rtac is_chain_iterate 1), |
|
437 (rtac lub_equal 1), |
|
438 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
|
439 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
|
440 (rtac allI 1), |
|
441 (resolve_tac prems 1) |
|
442 ]); |
|
443 |
|
444 val dlist_take_lemma = prover dlist_reach [dlist_take_def] |
|
445 "(!!n.dlist_take n`l1 = dlist_take n`l2) ==> l1=l2"; |
|
446 |
|
447 |
|
448 (* ------------------------------------------------------------------------*) |
|
449 (* Co -induction for dlists *) |
|
450 (* ------------------------------------------------------------------------*) |
|
451 |
|
452 qed_goalw "dlist_coind_lemma" Dlist.thy [dlist_bisim_def] |
|
453 "dlist_bisim R ==> ! p q. R p q --> dlist_take n`p = dlist_take n`q" |
|
454 (fn prems => |
|
455 [ |
|
456 (cut_facts_tac prems 1), |
|
457 (nat_ind_tac "n" 1), |
|
458 (simp_tac (!simpset addsimps dlist_rews) 1), |
|
459 (strip_tac 1), |
|
460 ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)), |
|
461 (atac 1), |
|
462 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
463 (etac disjE 1), |
|
464 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
465 (etac exE 1), |
|
466 (etac exE 1), |
|
467 (etac exE 1), |
|
468 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
469 (REPEAT (etac conjE 1)), |
|
470 (rtac cfun_arg_cong 1), |
|
471 (fast_tac HOL_cs 1) |
|
472 ]); |
|
473 |
|
474 qed_goal "dlist_coind" Dlist.thy "[|dlist_bisim R ; R p q |] ==> p = q" |
|
475 (fn prems => |
|
476 [ |
|
477 (rtac dlist_take_lemma 1), |
|
478 (rtac (dlist_coind_lemma RS spec RS spec RS mp) 1), |
|
479 (resolve_tac prems 1), |
|
480 (resolve_tac prems 1) |
|
481 ]); |
|
482 |
|
483 (* ------------------------------------------------------------------------*) |
|
484 (* structural induction *) |
|
485 (* ------------------------------------------------------------------------*) |
|
486 |
|
487 qed_goal "dlist_finite_ind" Dlist.thy |
|
488 "[|P(UU);P(dnil);\ |
|
489 \ !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons`x`l1)\ |
|
490 \ |] ==> !l.P(dlist_take n`l)" |
|
491 (fn prems => |
|
492 [ |
|
493 (nat_ind_tac "n" 1), |
|
494 (simp_tac (!simpset addsimps dlist_rews) 1), |
|
495 (resolve_tac prems 1), |
|
496 (rtac allI 1), |
|
497 (res_inst_tac [("l","l")] dlistE 1), |
|
498 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
499 (resolve_tac prems 1), |
|
500 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
501 (resolve_tac prems 1), |
|
502 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
503 (case_tac "dlist_take n1`xl=UU" 1), |
|
504 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
505 (resolve_tac prems 1), |
|
506 (resolve_tac prems 1), |
|
507 (atac 1), |
|
508 (atac 1), |
|
509 (etac spec 1) |
|
510 ]); |
|
511 |
|
512 qed_goal "dlist_all_finite_lemma1" Dlist.thy |
|
513 "!l.dlist_take n`l=UU |dlist_take n`l=l" |
|
514 (fn prems => |
|
515 [ |
|
516 (nat_ind_tac "n" 1), |
|
517 (simp_tac (!simpset addsimps dlist_rews) 1), |
|
518 (rtac allI 1), |
|
519 (res_inst_tac [("l","l")] dlistE 1), |
|
520 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
521 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
522 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
523 (eres_inst_tac [("x","xl")] allE 1), |
|
524 (etac disjE 1), |
|
525 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
526 (asm_simp_tac (!simpset addsimps dlist_rews) 1) |
|
527 ]); |
|
528 |
|
529 qed_goal "dlist_all_finite_lemma2" Dlist.thy "? n.dlist_take n`l=l" |
|
530 (fn prems => |
|
531 [ |
|
532 (case_tac "l=UU" 1), |
|
533 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
534 (subgoal_tac "(!n.dlist_take n`l=UU) |(? n.dlist_take n`l = l)" 1), |
|
535 (etac disjE 1), |
|
536 (eres_inst_tac [("P","l=UU")] notE 1), |
|
537 (rtac dlist_take_lemma 1), |
|
538 (asm_simp_tac (!simpset addsimps dlist_rews) 1), |
|
539 (atac 1), |
|
540 (subgoal_tac "!n.!l.dlist_take n`l=UU |dlist_take n`l=l" 1), |
|
541 (fast_tac HOL_cs 1), |
|
542 (rtac allI 1), |
|
543 (rtac dlist_all_finite_lemma1 1) |
|
544 ]); |
|
545 |
|
546 qed_goalw "dlist_all_finite" Dlist.thy [dlist_finite_def] "dlist_finite(l)" |
|
547 (fn prems => |
|
548 [ |
|
549 (rtac dlist_all_finite_lemma2 1) |
|
550 ]); |
|
551 |
|
552 qed_goal "dlist_ind" Dlist.thy |
|
553 "[|P(UU);P(dnil);\ |
|
554 \ !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons`x`l1)|] ==> P(l)" |
|
555 (fn prems => |
|
556 [ |
|
557 (rtac (dlist_all_finite_lemma2 RS exE) 1), |
|
558 (etac subst 1), |
|
559 (rtac (dlist_finite_ind RS spec) 1), |
|
560 (REPEAT (resolve_tac prems 1)), |
|
561 (REPEAT (atac 1)) |
|
562 ]); |
|
563 |
|
564 |
|
565 |
|
566 |
|