author | paulson |
Wed, 24 Dec 1997 10:02:30 +0100 | |
changeset 4477 | b3e5857d8d99 |
parent 4098 | 71e05eb27fb6 |
child 5068 | fb28eaa07e01 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/Seq.ML |
3275 | 2 |
ID: $Id$ |
3071 | 3 |
Author: Olaf M"uller |
4 |
Copyright 1996 TU Muenchen |
|
5 |
||
6 |
*) |
|
7 |
||
8 |
Addsimps (sfinite.intrs @ seq.rews); |
|
9 |
||
10 |
||
11 |
(* Instead of adding UU_neq_nil every equation UU~=x could be changed to x~=UU *) |
|
12 |
goal thy "UU ~=nil"; |
|
13 |
by (res_inst_tac [("s1","UU"),("t1","nil")] (sym RS rev_contrapos) 1); |
|
14 |
by (REPEAT (Simp_tac 1)); |
|
15 |
qed"UU_neq_nil"; |
|
16 |
||
17 |
Addsimps [UU_neq_nil]; |
|
18 |
||
3275 | 19 |
|
20 |
||
21 |
||
3071 | 22 |
(* ------------------------------------------------------------------------------------- *) |
23 |
||
24 |
||
25 |
(* ---------------------------------------------------- *) |
|
26 |
section "recursive equations of operators"; |
|
27 |
(* ---------------------------------------------------- *) |
|
28 |
||
29 |
||
30 |
(* ----------------------------------------------------------- *) |
|
31 |
(* smap *) |
|
32 |
(* ----------------------------------------------------------- *) |
|
33 |
||
34 |
bind_thm ("smap_unfold", fix_prover2 thy smap_def |
|
35 |
"smap = (LAM f tr. case tr of \ |
|
3361 | 36 |
\ nil => nil \ |
3071 | 37 |
\ | x##xs => f`x ## smap`f`xs)"); |
38 |
||
39 |
goal thy "smap`f`nil=nil"; |
|
40 |
by (stac smap_unfold 1); |
|
41 |
by (Simp_tac 1); |
|
42 |
qed"smap_nil"; |
|
43 |
||
44 |
goal thy "smap`f`UU=UU"; |
|
45 |
by (stac smap_unfold 1); |
|
46 |
by (Simp_tac 1); |
|
47 |
qed"smap_UU"; |
|
48 |
||
49 |
goal thy |
|
50 |
"!!x.[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; |
|
3457 | 51 |
by (rtac trans 1); |
3071 | 52 |
by (stac smap_unfold 1); |
53 |
by (Asm_full_simp_tac 1); |
|
3457 | 54 |
by (rtac refl 1); |
3071 | 55 |
qed"smap_cons"; |
56 |
||
57 |
(* ----------------------------------------------------------- *) |
|
58 |
(* sfilter *) |
|
59 |
(* ----------------------------------------------------------- *) |
|
60 |
||
61 |
bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def |
|
62 |
"sfilter = (LAM P tr. case tr of \ |
|
63 |
\ nil => nil \ |
|
64 |
\ | x##xs => If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)"); |
|
65 |
||
66 |
goal thy "sfilter`P`nil=nil"; |
|
67 |
by (stac sfilter_unfold 1); |
|
68 |
by (Simp_tac 1); |
|
69 |
qed"sfilter_nil"; |
|
70 |
||
71 |
goal thy "sfilter`P`UU=UU"; |
|
72 |
by (stac sfilter_unfold 1); |
|
73 |
by (Simp_tac 1); |
|
74 |
qed"sfilter_UU"; |
|
75 |
||
76 |
goal thy |
|
3847 | 77 |
"!!x. x~=UU ==> sfilter`P`(x##xs)= \ |
3071 | 78 |
\ (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)"; |
3457 | 79 |
by (rtac trans 1); |
3071 | 80 |
by (stac sfilter_unfold 1); |
81 |
by (Asm_full_simp_tac 1); |
|
3457 | 82 |
by (rtac refl 1); |
3071 | 83 |
qed"sfilter_cons"; |
84 |
||
85 |
(* ----------------------------------------------------------- *) |
|
86 |
(* sforall2 *) |
|
87 |
(* ----------------------------------------------------------- *) |
|
88 |
||
89 |
bind_thm ("sforall2_unfold", fix_prover2 thy sforall2_def |
|
90 |
"sforall2 = (LAM P tr. case tr of \ |
|
91 |
\ nil => TT \ |
|
92 |
\ | x##xs => (P`x andalso sforall2`P`xs))"); |
|
93 |
||
94 |
goal thy "sforall2`P`nil=TT"; |
|
95 |
by (stac sforall2_unfold 1); |
|
96 |
by (Simp_tac 1); |
|
97 |
qed"sforall2_nil"; |
|
98 |
||
99 |
goal thy "sforall2`P`UU=UU"; |
|
100 |
by (stac sforall2_unfold 1); |
|
101 |
by (Simp_tac 1); |
|
102 |
qed"sforall2_UU"; |
|
103 |
||
104 |
goal thy |
|
3847 | 105 |
"!!x. x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)"; |
3457 | 106 |
by (rtac trans 1); |
3071 | 107 |
by (stac sforall2_unfold 1); |
108 |
by (Asm_full_simp_tac 1); |
|
3457 | 109 |
by (rtac refl 1); |
3071 | 110 |
qed"sforall2_cons"; |
111 |
||
112 |
||
113 |
(* ----------------------------------------------------------- *) |
|
114 |
(* stakewhile *) |
|
115 |
(* ----------------------------------------------------------- *) |
|
116 |
||
117 |
||
118 |
bind_thm ("stakewhile_unfold", fix_prover2 thy stakewhile_def |
|
119 |
"stakewhile = (LAM P tr. case tr of \ |
|
120 |
\ nil => nil \ |
|
121 |
\ | x##xs => (If P`x then x##(stakewhile`P`xs) else nil fi))"); |
|
122 |
||
123 |
goal thy "stakewhile`P`nil=nil"; |
|
124 |
by (stac stakewhile_unfold 1); |
|
125 |
by (Simp_tac 1); |
|
126 |
qed"stakewhile_nil"; |
|
127 |
||
128 |
goal thy "stakewhile`P`UU=UU"; |
|
129 |
by (stac stakewhile_unfold 1); |
|
130 |
by (Simp_tac 1); |
|
131 |
qed"stakewhile_UU"; |
|
132 |
||
133 |
goal thy |
|
3847 | 134 |
"!!x. x~=UU ==> stakewhile`P`(x##xs) = \ |
3071 | 135 |
\ (If P`x then x##(stakewhile`P`xs) else nil fi)"; |
3457 | 136 |
by (rtac trans 1); |
3071 | 137 |
by (stac stakewhile_unfold 1); |
138 |
by (Asm_full_simp_tac 1); |
|
3457 | 139 |
by (rtac refl 1); |
3071 | 140 |
qed"stakewhile_cons"; |
141 |
||
142 |
(* ----------------------------------------------------------- *) |
|
143 |
(* sdropwhile *) |
|
144 |
(* ----------------------------------------------------------- *) |
|
145 |
||
146 |
||
147 |
bind_thm ("sdropwhile_unfold", fix_prover2 thy sdropwhile_def |
|
148 |
"sdropwhile = (LAM P tr. case tr of \ |
|
149 |
\ nil => nil \ |
|
150 |
\ | x##xs => (If P`x then sdropwhile`P`xs else tr fi))"); |
|
151 |
||
152 |
goal thy "sdropwhile`P`nil=nil"; |
|
153 |
by (stac sdropwhile_unfold 1); |
|
154 |
by (Simp_tac 1); |
|
155 |
qed"sdropwhile_nil"; |
|
156 |
||
157 |
goal thy "sdropwhile`P`UU=UU"; |
|
158 |
by (stac sdropwhile_unfold 1); |
|
159 |
by (Simp_tac 1); |
|
160 |
qed"sdropwhile_UU"; |
|
161 |
||
162 |
goal thy |
|
3847 | 163 |
"!!x. x~=UU ==> sdropwhile`P`(x##xs) = \ |
3071 | 164 |
\ (If P`x then sdropwhile`P`xs else x##xs fi)"; |
3457 | 165 |
by (rtac trans 1); |
3071 | 166 |
by (stac sdropwhile_unfold 1); |
167 |
by (Asm_full_simp_tac 1); |
|
3457 | 168 |
by (rtac refl 1); |
3071 | 169 |
qed"sdropwhile_cons"; |
170 |
||
171 |
||
172 |
(* ----------------------------------------------------------- *) |
|
173 |
(* slast *) |
|
174 |
(* ----------------------------------------------------------- *) |
|
175 |
||
176 |
||
177 |
bind_thm ("slast_unfold", fix_prover2 thy slast_def |
|
178 |
"slast = (LAM tr. case tr of \ |
|
179 |
\ nil => UU \ |
|
180 |
\ | x##xs => (If is_nil`xs then x else slast`xs fi))"); |
|
181 |
||
182 |
||
183 |
goal thy "slast`nil=UU"; |
|
184 |
by (stac slast_unfold 1); |
|
185 |
by (Simp_tac 1); |
|
186 |
qed"slast_nil"; |
|
187 |
||
188 |
goal thy "slast`UU=UU"; |
|
189 |
by (stac slast_unfold 1); |
|
190 |
by (Simp_tac 1); |
|
191 |
qed"slast_UU"; |
|
192 |
||
193 |
goal thy |
|
3847 | 194 |
"!!x. x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)"; |
3457 | 195 |
by (rtac trans 1); |
3071 | 196 |
by (stac slast_unfold 1); |
197 |
by (Asm_full_simp_tac 1); |
|
3457 | 198 |
by (rtac refl 1); |
3071 | 199 |
qed"slast_cons"; |
200 |
||
201 |
||
202 |
(* ----------------------------------------------------------- *) |
|
203 |
(* sconc *) |
|
204 |
(* ----------------------------------------------------------- *) |
|
205 |
||
206 |
bind_thm ("sconc_unfold", fix_prover2 thy sconc_def |
|
207 |
"sconc = (LAM t1 t2. case t1 of \ |
|
208 |
\ nil => t2 \ |
|
209 |
\ | x##xs => x ## (xs @@ t2))"); |
|
210 |
||
211 |
||
212 |
goal thy "nil @@ y = y"; |
|
213 |
by (stac sconc_unfold 1); |
|
214 |
by (Simp_tac 1); |
|
215 |
qed"sconc_nil"; |
|
216 |
||
217 |
goal thy "UU @@ y=UU"; |
|
218 |
by (stac sconc_unfold 1); |
|
219 |
by (Simp_tac 1); |
|
220 |
qed"sconc_UU"; |
|
221 |
||
222 |
goal thy "(x##xs) @@ y=x##(xs @@ y)"; |
|
3457 | 223 |
by (rtac trans 1); |
3071 | 224 |
by (stac sconc_unfold 1); |
225 |
by (Asm_full_simp_tac 1); |
|
226 |
by (case_tac "x=UU" 1); |
|
227 |
by (REPEAT (Asm_full_simp_tac 1)); |
|
228 |
qed"sconc_cons"; |
|
229 |
||
3275 | 230 |
Addsimps [sconc_nil,sconc_UU,sconc_cons]; |
3071 | 231 |
|
232 |
||
233 |
(* ----------------------------------------------------------- *) |
|
234 |
(* sflat *) |
|
235 |
(* ----------------------------------------------------------- *) |
|
236 |
||
237 |
bind_thm ("sflat_unfold", fix_prover2 thy sflat_def |
|
238 |
"sflat = (LAM tr. case tr of \ |
|
239 |
\ nil => nil \ |
|
240 |
\ | x##xs => x @@ sflat`xs)"); |
|
241 |
||
242 |
goal thy "sflat`nil=nil"; |
|
243 |
by (stac sflat_unfold 1); |
|
244 |
by (Simp_tac 1); |
|
245 |
qed"sflat_nil"; |
|
246 |
||
247 |
goal thy "sflat`UU=UU"; |
|
248 |
by (stac sflat_unfold 1); |
|
249 |
by (Simp_tac 1); |
|
250 |
qed"sflat_UU"; |
|
251 |
||
252 |
goal thy "sflat`(x##xs)= x@@(sflat`xs)"; |
|
3457 | 253 |
by (rtac trans 1); |
3071 | 254 |
by (stac sflat_unfold 1); |
255 |
by (Asm_full_simp_tac 1); |
|
256 |
by (case_tac "x=UU" 1); |
|
257 |
by (REPEAT (Asm_full_simp_tac 1)); |
|
258 |
qed"sflat_cons"; |
|
259 |
||
260 |
||
261 |
||
262 |
||
263 |
(* ----------------------------------------------------------- *) |
|
264 |
(* szip *) |
|
265 |
(* ----------------------------------------------------------- *) |
|
266 |
||
267 |
bind_thm ("szip_unfold", fix_prover2 thy szip_def |
|
268 |
"szip = (LAM t1 t2. case t1 of \ |
|
269 |
\ nil => nil \ |
|
270 |
\ | x##xs => (case t2 of \ |
|
271 |
\ nil => UU \ |
|
272 |
\ | y##ys => <x,y>##(szip`xs`ys)))"); |
|
273 |
||
274 |
goal thy "szip`nil`y=nil"; |
|
275 |
by (stac szip_unfold 1); |
|
276 |
by (Simp_tac 1); |
|
277 |
qed"szip_nil"; |
|
278 |
||
279 |
goal thy "szip`UU`y=UU"; |
|
280 |
by (stac szip_unfold 1); |
|
281 |
by (Simp_tac 1); |
|
282 |
qed"szip_UU1"; |
|
283 |
||
284 |
goal thy "!!x. x~=nil ==> szip`x`UU=UU"; |
|
285 |
by (stac szip_unfold 1); |
|
286 |
by (Asm_full_simp_tac 1); |
|
4042 | 287 |
by (res_inst_tac [("x","x")] seq.casedist 1); |
3071 | 288 |
by (REPEAT (Asm_full_simp_tac 1)); |
289 |
qed"szip_UU2"; |
|
290 |
||
3847 | 291 |
goal thy "!!x. x~=UU ==> szip`(x##xs)`nil=UU"; |
3457 | 292 |
by (rtac trans 1); |
3071 | 293 |
by (stac szip_unfold 1); |
294 |
by (REPEAT (Asm_full_simp_tac 1)); |
|
295 |
qed"szip_cons_nil"; |
|
296 |
||
297 |
goal thy "!!x.[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys"; |
|
3457 | 298 |
by (rtac trans 1); |
3071 | 299 |
by (stac szip_unfold 1); |
300 |
by (REPEAT (Asm_full_simp_tac 1)); |
|
301 |
qed"szip_cons"; |
|
302 |
||
303 |
||
304 |
Addsimps [sfilter_UU,sfilter_nil,sfilter_cons, |
|
305 |
smap_UU,smap_nil,smap_cons, |
|
306 |
sforall2_UU,sforall2_nil,sforall2_cons, |
|
307 |
slast_UU,slast_nil,slast_cons, |
|
308 |
stakewhile_UU, stakewhile_nil, stakewhile_cons, |
|
309 |
sdropwhile_UU, sdropwhile_nil, sdropwhile_cons, |
|
310 |
sflat_UU,sflat_nil,sflat_cons, |
|
311 |
szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons]; |
|
312 |
||
313 |
||
314 |
||
315 |
(* ------------------------------------------------------------------------------------- *) |
|
316 |
||
3275 | 317 |
section "scons, nil"; |
3071 | 318 |
|
319 |
goal thy |
|
320 |
"!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)"; |
|
321 |
by (rtac iffI 1); |
|
322 |
by (etac (hd seq.injects) 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
323 |
by Auto_tac; |
3071 | 324 |
qed"scons_inject_eq"; |
325 |
||
3275 | 326 |
goal thy "!!x. nil<<x ==> nil=x"; |
4042 | 327 |
by (res_inst_tac [("x","x")] seq.casedist 1); |
3275 | 328 |
by (hyp_subst_tac 1); |
329 |
by (etac antisym_less 1); |
|
330 |
by (Asm_full_simp_tac 1); |
|
331 |
by (Asm_full_simp_tac 1); |
|
332 |
by (hyp_subst_tac 1); |
|
333 |
by (Asm_full_simp_tac 1); |
|
334 |
qed"nil_less_is_nil"; |
|
3071 | 335 |
|
336 |
(* ------------------------------------------------------------------------------------- *) |
|
337 |
||
338 |
section "sfilter, sforall, sconc"; |
|
339 |
||
340 |
||
341 |
goal thy "(if b then tr1 else tr2) @@ tr \ |
|
342 |
\= (if b then tr1 @@ tr else tr2 @@ tr)"; |
|
343 |
by (res_inst_tac [("P","b"),("Q","b")] impCE 1); |
|
344 |
by (fast_tac HOL_cs 1); |
|
345 |
by (REPEAT (Asm_full_simp_tac 1)); |
|
346 |
qed"if_and_sconc"; |
|
347 |
||
348 |
Addsimps [if_and_sconc]; |
|
349 |
||
350 |
||
351 |
goal thy "sfilter`P`(x @@ y) = (sfilter`P`x @@ sfilter`P`y)"; |
|
352 |
||
353 |
by (res_inst_tac[("x","x")] seq.ind 1); |
|
354 |
(* adm *) |
|
355 |
by (Simp_tac 1); |
|
356 |
(* base cases *) |
|
357 |
by (Simp_tac 1); |
|
358 |
by (Simp_tac 1); |
|
359 |
(* main case *) |
|
4098 | 360 |
by (asm_full_simp_tac (simpset() setloop split_If_tac) 1); |
3071 | 361 |
qed"sfiltersconc"; |
362 |
||
363 |
goal thy "sforall P (stakewhile`P`x)"; |
|
4098 | 364 |
by (simp_tac (simpset() addsimps [sforall_def]) 1); |
3071 | 365 |
by (res_inst_tac[("x","x")] seq.ind 1); |
366 |
(* adm *) |
|
4098 | 367 |
by (simp_tac (simpset() addsimps [adm_trick_1]) 1); |
3071 | 368 |
(* base cases *) |
369 |
by (Simp_tac 1); |
|
370 |
by (Simp_tac 1); |
|
371 |
(* main case *) |
|
4098 | 372 |
by (asm_full_simp_tac (simpset() setloop split_If_tac) 1); |
3071 | 373 |
qed"sforallPstakewhileP"; |
374 |
||
375 |
goal thy "sforall P (sfilter`P`x)"; |
|
4098 | 376 |
by (simp_tac (simpset() addsimps [sforall_def]) 1); |
3071 | 377 |
by (res_inst_tac[("x","x")] seq.ind 1); |
378 |
(* adm *) |
|
379 |
(* FIX should be refined in _one_ tactic *) |
|
4098 | 380 |
by (simp_tac (simpset() addsimps [adm_trick_1]) 1); |
3071 | 381 |
(* base cases *) |
382 |
by (Simp_tac 1); |
|
383 |
by (Simp_tac 1); |
|
384 |
(* main case *) |
|
4098 | 385 |
by (asm_full_simp_tac (simpset() setloop split_If_tac) 1); |
3071 | 386 |
qed"forallPsfilterP"; |
387 |
||
388 |
||
389 |
||
390 |
(* ------------------------------------------------------------------------------------- *) |
|
391 |
||
392 |
section "Finite"; |
|
393 |
||
394 |
(* ---------------------------------------------------- *) |
|
395 |
(* Proofs of rewrite rules for Finite: *) |
|
396 |
(* 1. Finite(nil), (by definition) *) |
|
397 |
(* 2. ~Finite(UU), *) |
|
398 |
(* 3. a~=UU==> Finite(a##x)=Finite(x) *) |
|
399 |
(* ---------------------------------------------------- *) |
|
400 |
||
401 |
goal thy "Finite x --> x~=UU"; |
|
3457 | 402 |
by (rtac impI 1); |
403 |
by (etac sfinite.induct 1); |
|
3071 | 404 |
by (Asm_full_simp_tac 1); |
405 |
by (Asm_full_simp_tac 1); |
|
406 |
qed"Finite_UU_a"; |
|
407 |
||
408 |
goal thy "~(Finite UU)"; |
|
409 |
by (cut_inst_tac [("x","UU")]Finite_UU_a 1); |
|
410 |
by (fast_tac HOL_cs 1); |
|
411 |
qed"Finite_UU"; |
|
412 |
||
413 |
goal thy "Finite x --> a~=UU --> x=a##xs --> Finite xs"; |
|
414 |
by (strip_tac 1); |
|
3457 | 415 |
by (etac sfinite.elim 1); |
4098 | 416 |
by (fast_tac (HOL_cs addss simpset()) 1); |
3071 | 417 |
by (fast_tac (HOL_cs addSDs seq.injects) 1); |
418 |
qed"Finite_cons_a"; |
|
419 |
||
3847 | 420 |
goal thy "!!x. a~=UU ==>(Finite (a##x)) = (Finite x)"; |
3071 | 421 |
by (rtac iffI 1); |
422 |
by (rtac (Finite_cons_a RS mp RS mp RS mp) 1); |
|
423 |
by (REPEAT (assume_tac 1)); |
|
424 |
by (fast_tac HOL_cs 1); |
|
425 |
by (Asm_full_simp_tac 1); |
|
426 |
qed"Finite_cons"; |
|
427 |
||
428 |
Addsimps [Finite_UU]; |
|
429 |
||
430 |
||
431 |
(* ------------------------------------------------------------------------------------- *) |
|
432 |
||
433 |
section "induction"; |
|
434 |
||
435 |
||
436 |
(*-------------------------------- *) |
|
437 |
(* Extensions to Induction Theorems *) |
|
438 |
(*-------------------------------- *) |
|
439 |
||
440 |
||
441 |
qed_goalw "seq_finite_ind_lemma" thy [seq.finite_def] |
|
3847 | 442 |
"(!!n. P(seq_take n`s)) ==> seq_finite(s) -->P(s)" |
3071 | 443 |
(fn prems => |
444 |
[ |
|
445 |
(strip_tac 1), |
|
446 |
(etac exE 1), |
|
447 |
(etac subst 1), |
|
448 |
(resolve_tac prems 1) |
|
449 |
]); |
|
450 |
||
451 |
||
452 |
goal thy |
|
453 |
"!!P.[|P(UU);P(nil);\ |
|
454 |
\ !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\ |
|
455 |
\ |] ==> seq_finite(s) --> P(s)"; |
|
456 |
by (rtac seq_finite_ind_lemma 1); |
|
3457 | 457 |
by (etac seq.finite_ind 1); |
458 |
by (assume_tac 1); |
|
3071 | 459 |
by (Asm_full_simp_tac 1); |
460 |
qed"seq_finite_ind"; |
|
461 |
||
462 |
||
463 |
||
464 |
||
465 |
(* |
|
466 |
(* ----------------------------------------------------------------- |
|
467 |
Fr"uhere Herleitung des endlichen Induktionsprinzips |
|
468 |
aus dem seq_finite Induktionsprinzip. |
|
469 |
Problem bei admissibility von Finite-->seq_finite! |
|
470 |
Deshalb Finite jetzt induktiv und nicht mehr rekursiv definiert! |
|
471 |
------------------------------------------------------------------ *) |
|
472 |
||
473 |
goal thy "seq_finite nil"; |
|
4098 | 474 |
by (simp_tac (simpset() addsimps [seq.sfinite_def]) 1); |
3071 | 475 |
by (res_inst_tac [("x","Suc 0")] exI 1); |
4098 | 476 |
by (simp_tac (simpset() addsimps seq.rews) 1); |
3071 | 477 |
qed"seq_finite_nil"; |
478 |
||
479 |
goal thy "seq_finite UU"; |
|
4098 | 480 |
by (simp_tac (simpset() addsimps [seq.sfinite_def]) 1); |
3071 | 481 |
qed"seq_finite_UU"; |
482 |
||
483 |
Addsimps[seq_finite_nil,seq_finite_UU]; |
|
484 |
||
485 |
goal HOL.thy "(B-->A) --> (A--> (B-->C))--> (B--> C)"; |
|
486 |
by (fast_tac HOL_cs 1); |
|
487 |
qed"logic_lemma"; |
|
488 |
||
489 |
||
490 |
goal thy "!!P.[| P nil; \ |
|
491 |
\ !!a t. [|a~=UU;Finite t; P t|] ==> P (a##t)|]\ |
|
492 |
\ ==> Finite x --> P x"; |
|
493 |
||
494 |
by (rtac (logic_lemma RS mp RS mp) 1); |
|
495 |
by (rtac trf_impl_tf 1); |
|
496 |
by (rtac seq_finite_ind 1); |
|
4098 | 497 |
by (simp_tac (simpset() addsimps [Finite_def]) 1); |
498 |
by (simp_tac (simpset() addsimps [Finite_def]) 1); |
|
499 |
by (asm_full_simp_tac (simpset() addsimps [Finite_def]) 1); |
|
3071 | 500 |
qed"Finite_ind"; |
501 |
||
502 |
||
503 |
goal thy "Finite tr --> seq_finite tr"; |
|
504 |
by (rtac seq.ind 1); |
|
505 |
(* adm *) |
|
506 |
(* hier grosses Problem !!!!!!!!!!!!!!! *) |
|
507 |
||
4098 | 508 |
by (simp_tac (simpset() addsimps [Finite_def]) 2); |
509 |
by (simp_tac (simpset() addsimps [Finite_def]) 2); |
|
3071 | 510 |
|
511 |
(* main case *) |
|
4098 | 512 |
by (asm_full_simp_tac (simpset() addsimps [Finite_def,seq.sfinite_def]) 2); |
3071 | 513 |
by (rtac impI 2); |
514 |
by (rotate_tac 2 2); |
|
515 |
by (Asm_full_simp_tac 2); |
|
516 |
by (etac exE 2); |
|
517 |
by (res_inst_tac [("x","Suc n")] exI 2); |
|
4098 | 518 |
by (asm_full_simp_tac (simpset() addsimps seq.rews) 2); |
3071 | 519 |
qed"tf_is_trf"; |
520 |
||
521 |
*) |
|
522 |