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
|
|
77 |
"!!x.x~=UU ==> sfilter`P`(x##xs)= \
|
|
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
|
|
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
|
|
134 |
"!!x.x~=UU ==> stakewhile`P`(x##xs) = \
|
|
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
|
|
163 |
"!!x.x~=UU ==> sdropwhile`P`(x##xs) = \
|
|
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
|
|
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);
|
|
287 |
by (res_inst_tac [("x","x")] seq.cases 1);
|
|
288 |
by (REPEAT (Asm_full_simp_tac 1));
|
|
289 |
qed"szip_UU2";
|
|
290 |
|
|
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);
|
3457
|
323 |
by (Auto_tac());
|
3071
|
324 |
qed"scons_inject_eq";
|
|
325 |
|
3275
|
326 |
goal thy "!!x. nil<<x ==> nil=x";
|
|
327 |
by (res_inst_tac [("x","x")] seq.cases 1);
|
|
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 *)
|
|
360 |
by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
|
|
361 |
qed"sfiltersconc";
|
|
362 |
|
|
363 |
goal thy "sforall P (stakewhile`P`x)";
|
|
364 |
by (simp_tac (!simpset addsimps [sforall_def]) 1);
|
|
365 |
by (res_inst_tac[("x","x")] seq.ind 1);
|
|
366 |
(* adm *)
|
|
367 |
by (simp_tac (!simpset addsimps [adm_trick_1]) 1);
|
|
368 |
(* base cases *)
|
|
369 |
by (Simp_tac 1);
|
|
370 |
by (Simp_tac 1);
|
|
371 |
(* main case *)
|
|
372 |
by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
|
|
373 |
qed"sforallPstakewhileP";
|
|
374 |
|
|
375 |
goal thy "sforall P (sfilter`P`x)";
|
|
376 |
by (simp_tac (!simpset addsimps [sforall_def]) 1);
|
|
377 |
by (res_inst_tac[("x","x")] seq.ind 1);
|
|
378 |
(* adm *)
|
|
379 |
(* FIX should be refined in _one_ tactic *)
|
|
380 |
by (simp_tac (!simpset addsimps [adm_trick_1]) 1);
|
|
381 |
(* base cases *)
|
|
382 |
by (Simp_tac 1);
|
|
383 |
by (Simp_tac 1);
|
|
384 |
(* main case *)
|
|
385 |
by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
|
|
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);
|
3071
|
416 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
|
417 |
by (fast_tac (HOL_cs addSDs seq.injects) 1);
|
|
418 |
qed"Finite_cons_a";
|
|
419 |
|
|
420 |
goal thy "!!x.a~=UU ==>(Finite (a##x)) = (Finite x)";
|
|
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]
|
|
442 |
"(!!n.P(seq_take n`s)) ==> seq_finite(s) -->P(s)"
|
|
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";
|
|
474 |
by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1);
|
|
475 |
by (res_inst_tac [("x","Suc 0")] exI 1);
|
|
476 |
by (simp_tac (!simpset addsimps seq.rews) 1);
|
|
477 |
qed"seq_finite_nil";
|
|
478 |
|
|
479 |
goal thy "seq_finite UU";
|
|
480 |
by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1);
|
|
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);
|
|
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);
|
|
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 |
|
|
508 |
by (simp_tac (!simpset addsimps [Finite_def]) 2);
|
|
509 |
by (simp_tac (!simpset addsimps [Finite_def]) 2);
|
|
510 |
|
|
511 |
(* main case *)
|
|
512 |
by (asm_full_simp_tac (!simpset addsimps [Finite_def,seq.sfinite_def]) 2);
|
|
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);
|
|
518 |
by (asm_full_simp_tac (!simpset addsimps seq.rews) 2);
|
|
519 |
qed"tf_is_trf";
|
|
520 |
|
|
521 |
*)
|
|
522 |
|