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