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