8 imports HOLCF |
8 imports HOLCF |
9 begin |
9 begin |
10 |
10 |
11 domain 'a seq = nil | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65) |
11 domain 'a seq = nil | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65) |
12 |
12 |
13 consts |
13 (* |
14 sfilter :: "('a -> tr) -> 'a seq -> 'a seq" |
14 sfilter :: "('a -> tr) -> 'a seq -> 'a seq" |
15 smap :: "('a -> 'b) -> 'a seq -> 'b seq" |
15 smap :: "('a -> 'b) -> 'a seq -> 'b seq" |
16 sforall :: "('a -> tr) => 'a seq => bool" |
16 sforall :: "('a -> tr) => 'a seq => bool" |
17 sforall2 :: "('a -> tr) -> 'a seq -> tr" |
17 sforall2 :: "('a -> tr) -> 'a seq -> tr" |
18 slast :: "'a seq -> 'a" |
18 slast :: "'a seq -> 'a" |
19 sconc :: "'a seq -> 'a seq -> 'a seq" |
19 sconc :: "'a seq -> 'a seq -> 'a seq" |
20 sdropwhile ::"('a -> tr) -> 'a seq -> 'a seq" |
20 sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq" |
21 stakewhile ::"('a -> tr) -> 'a seq -> 'a seq" |
21 stakewhile :: "('a -> tr) -> 'a seq -> 'a seq" |
22 szip ::"'a seq -> 'b seq -> ('a*'b) seq" |
22 szip :: "'a seq -> 'b seq -> ('a*'b) seq" |
23 sflat :: "('a seq) seq -> 'a seq" |
23 sflat :: "('a seq) seq -> 'a seq" |
24 |
24 |
25 sfinite :: "'a seq set" |
25 sfinite :: "'a seq set" |
26 Partial ::"'a seq => bool" |
26 Partial :: "'a seq => bool" |
27 Infinite ::"'a seq => bool" |
27 Infinite :: "'a seq => bool" |
28 |
28 |
29 nproj :: "nat => 'a seq => 'a" |
29 nproj :: "nat => 'a seq => 'a" |
30 sproj :: "nat => 'a seq => 'a seq" |
30 sproj :: "nat => 'a seq => 'a seq" |
31 |
31 *) |
32 abbreviation |
|
33 sconc_syn :: "'a seq => 'a seq => 'a seq" (infixr "@@" 65) where |
|
34 "xs @@ ys == sconc $ xs $ ys" |
|
35 |
32 |
36 inductive |
33 inductive |
37 Finite :: "'a seq => bool" |
34 Finite :: "'a seq => bool" |
38 where |
35 where |
39 sfinite_0: "Finite nil" |
36 sfinite_0: "Finite nil" |
40 | sfinite_n: "[| Finite tr; a~=UU |] ==> Finite (a##tr)" |
37 | sfinite_n: "[| Finite tr; a~=UU |] ==> Finite (a##tr)" |
41 |
38 |
42 defs |
39 declare Finite.intros [simp] |
43 |
40 |
44 (* f not possible at lhs, as "pattern matching" only for % x arguments, |
41 definition |
45 f cannot be written at rhs in front, as fix_eq3 does not apply later *) |
42 Partial :: "'a seq => bool" |
46 smap_def: |
43 where |
47 "smap == (fix$(LAM h f tr. case tr of |
|
48 nil => nil |
|
49 | x##xs => f$x ## h$f$xs))" |
|
50 |
|
51 sfilter_def: |
|
52 "sfilter == (fix$(LAM h P t. case t of |
|
53 nil => nil |
|
54 | x##xs => If P$x |
|
55 then x##(h$P$xs) |
|
56 else h$P$xs |
|
57 fi))" |
|
58 sforall_def: |
|
59 "sforall P t == (sforall2$P$t ~=FF)" |
|
60 |
|
61 |
|
62 sforall2_def: |
|
63 "sforall2 == (fix$(LAM h P t. case t of |
|
64 nil => TT |
|
65 | x##xs => P$x andalso h$P$xs))" |
|
66 |
|
67 sconc_def: |
|
68 "sconc == (fix$(LAM h t1 t2. case t1 of |
|
69 nil => t2 |
|
70 | x##xs => x##(h$xs$t2)))" |
|
71 |
|
72 slast_def: |
|
73 "slast == (fix$(LAM h t. case t of |
|
74 nil => UU |
|
75 | x##xs => (If is_nil$xs |
|
76 then x |
|
77 else h$xs fi)))" |
|
78 |
|
79 stakewhile_def: |
|
80 "stakewhile == (fix$(LAM h P t. case t of |
|
81 nil => nil |
|
82 | x##xs => If P$x |
|
83 then x##(h$P$xs) |
|
84 else nil |
|
85 fi))" |
|
86 sdropwhile_def: |
|
87 "sdropwhile == (fix$(LAM h P t. case t of |
|
88 nil => nil |
|
89 | x##xs => If P$x |
|
90 then h$P$xs |
|
91 else t |
|
92 fi))" |
|
93 sflat_def: |
|
94 "sflat == (fix$(LAM h t. case t of |
|
95 nil => nil |
|
96 | x##xs => x @@ (h$xs)))" |
|
97 |
|
98 szip_def: |
|
99 "szip == (fix$(LAM h t1 t2. case t1 of |
|
100 nil => nil |
|
101 | x##xs => (case t2 of |
|
102 nil => UU |
|
103 | y##ys => <x,y>##(h$xs$ys))))" |
|
104 |
|
105 Partial_def: |
|
106 "Partial x == (seq_finite x) & ~(Finite x)" |
44 "Partial x == (seq_finite x) & ~(Finite x)" |
107 |
45 |
108 Infinite_def: |
46 definition |
|
47 Infinite :: "'a seq => bool" |
|
48 where |
109 "Infinite x == ~(seq_finite x)" |
49 "Infinite x == ~(seq_finite x)" |
110 |
50 |
111 |
51 |
112 declare Finite.intros [simp] |
|
113 |
|
114 |
|
115 subsection {* recursive equations of operators *} |
52 subsection {* recursive equations of operators *} |
116 |
53 |
117 subsubsection {* smap *} |
54 subsubsection {* smap *} |
118 |
55 |
119 lemma smap_unfold: |
56 fixrec |
120 "smap = (LAM f tr. case tr of nil => nil | x##xs => f$x ## smap$f$xs)" |
57 smap :: "('a -> 'b) -> 'a seq -> 'b seq" |
121 by (subst fix_eq2 [OF smap_def], simp) |
58 where |
122 |
59 smap_nil: "smap$f$nil=nil" |
123 lemma smap_nil [simp]: "smap$f$nil=nil" |
60 | smap_cons: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs" |
124 by (subst smap_unfold, simp) |
|
125 |
61 |
126 lemma smap_UU [simp]: "smap$f$UU=UU" |
62 lemma smap_UU [simp]: "smap$f$UU=UU" |
127 by (subst smap_unfold, simp) |
63 by fixrec_simp |
128 |
|
129 lemma smap_cons [simp]: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs" |
|
130 apply (rule trans) |
|
131 apply (subst smap_unfold) |
|
132 apply simp |
|
133 apply (rule refl) |
|
134 done |
|
135 |
64 |
136 subsubsection {* sfilter *} |
65 subsubsection {* sfilter *} |
137 |
66 |
138 lemma sfilter_unfold: |
67 fixrec |
139 "sfilter = (LAM P tr. case tr of |
68 sfilter :: "('a -> tr) -> 'a seq -> 'a seq" |
140 nil => nil |
69 where |
141 | x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)" |
70 sfilter_nil: "sfilter$P$nil=nil" |
142 by (subst fix_eq2 [OF sfilter_def], simp) |
71 | sfilter_cons: |
143 |
72 "x~=UU ==> sfilter$P$(x##xs)= |
144 lemma sfilter_nil [simp]: "sfilter$P$nil=nil" |
73 (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)" |
145 by (subst sfilter_unfold, simp) |
|
146 |
74 |
147 lemma sfilter_UU [simp]: "sfilter$P$UU=UU" |
75 lemma sfilter_UU [simp]: "sfilter$P$UU=UU" |
148 by (subst sfilter_unfold, simp) |
76 by fixrec_simp |
149 |
|
150 lemma sfilter_cons [simp]: |
|
151 "x~=UU ==> sfilter$P$(x##xs)= |
|
152 (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)" |
|
153 apply (rule trans) |
|
154 apply (subst sfilter_unfold) |
|
155 apply simp |
|
156 apply (rule refl) |
|
157 done |
|
158 |
77 |
159 subsubsection {* sforall2 *} |
78 subsubsection {* sforall2 *} |
160 |
79 |
161 lemma sforall2_unfold: |
80 fixrec |
162 "sforall2 = (LAM P tr. case tr of |
81 sforall2 :: "('a -> tr) -> 'a seq -> tr" |
163 nil => TT |
82 where |
164 | x##xs => (P$x andalso sforall2$P$xs))" |
83 sforall2_nil: "sforall2$P$nil=TT" |
165 by (subst fix_eq2 [OF sforall2_def], simp) |
84 | sforall2_cons: |
166 |
85 "x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)" |
167 lemma sforall2_nil [simp]: "sforall2$P$nil=TT" |
|
168 by (subst sforall2_unfold, simp) |
|
169 |
86 |
170 lemma sforall2_UU [simp]: "sforall2$P$UU=UU" |
87 lemma sforall2_UU [simp]: "sforall2$P$UU=UU" |
171 by (subst sforall2_unfold, simp) |
88 by fixrec_simp |
172 |
89 |
173 lemma sforall2_cons [simp]: |
90 definition |
174 "x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)" |
91 sforall_def: "sforall P t == (sforall2$P$t ~=FF)" |
175 apply (rule trans) |
|
176 apply (subst sforall2_unfold) |
|
177 apply simp |
|
178 apply (rule refl) |
|
179 done |
|
180 |
|
181 |
92 |
182 subsubsection {* stakewhile *} |
93 subsubsection {* stakewhile *} |
183 |
94 |
184 lemma stakewhile_unfold: |
95 fixrec |
185 "stakewhile = (LAM P tr. case tr of |
96 stakewhile :: "('a -> tr) -> 'a seq -> 'a seq" |
186 nil => nil |
97 where |
187 | x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))" |
98 stakewhile_nil: "stakewhile$P$nil=nil" |
188 by (subst fix_eq2 [OF stakewhile_def], simp) |
99 | stakewhile_cons: |
189 |
100 "x~=UU ==> stakewhile$P$(x##xs) = |
190 lemma stakewhile_nil [simp]: "stakewhile$P$nil=nil" |
101 (If P$x then x##(stakewhile$P$xs) else nil fi)" |
191 apply (subst stakewhile_unfold) |
|
192 apply simp |
|
193 done |
|
194 |
102 |
195 lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU" |
103 lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU" |
196 apply (subst stakewhile_unfold) |
104 by fixrec_simp |
197 apply simp |
|
198 done |
|
199 |
|
200 lemma stakewhile_cons [simp]: |
|
201 "x~=UU ==> stakewhile$P$(x##xs) = |
|
202 (If P$x then x##(stakewhile$P$xs) else nil fi)" |
|
203 apply (rule trans) |
|
204 apply (subst stakewhile_unfold) |
|
205 apply simp |
|
206 apply (rule refl) |
|
207 done |
|
208 |
105 |
209 subsubsection {* sdropwhile *} |
106 subsubsection {* sdropwhile *} |
210 |
107 |
211 lemma sdropwhile_unfold: |
108 fixrec |
212 "sdropwhile = (LAM P tr. case tr of |
109 sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq" |
213 nil => nil |
110 where |
214 | x##xs => (If P$x then sdropwhile$P$xs else tr fi))" |
111 sdropwhile_nil: "sdropwhile$P$nil=nil" |
215 by (subst fix_eq2 [OF sdropwhile_def], simp) |
112 | sdropwhile_cons: |
216 |
113 "x~=UU ==> sdropwhile$P$(x##xs) = |
217 lemma sdropwhile_nil [simp]: "sdropwhile$P$nil=nil" |
114 (If P$x then sdropwhile$P$xs else x##xs fi)" |
218 apply (subst sdropwhile_unfold) |
|
219 apply simp |
|
220 done |
|
221 |
115 |
222 lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU" |
116 lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU" |
223 apply (subst sdropwhile_unfold) |
117 by fixrec_simp |
224 apply simp |
|
225 done |
|
226 |
|
227 lemma sdropwhile_cons [simp]: |
|
228 "x~=UU ==> sdropwhile$P$(x##xs) = |
|
229 (If P$x then sdropwhile$P$xs else x##xs fi)" |
|
230 apply (rule trans) |
|
231 apply (subst sdropwhile_unfold) |
|
232 apply simp |
|
233 apply (rule refl) |
|
234 done |
|
235 |
|
236 |
118 |
237 subsubsection {* slast *} |
119 subsubsection {* slast *} |
238 |
120 |
239 lemma slast_unfold: |
121 fixrec |
240 "slast = (LAM tr. case tr of |
122 slast :: "'a seq -> 'a" |
241 nil => UU |
123 where |
242 | x##xs => (If is_nil$xs then x else slast$xs fi))" |
124 slast_nil: "slast$nil=UU" |
243 by (subst fix_eq2 [OF slast_def], simp) |
125 | slast_cons: |
244 |
126 "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)" |
245 lemma slast_nil [simp]: "slast$nil=UU" |
|
246 apply (subst slast_unfold) |
|
247 apply simp |
|
248 done |
|
249 |
127 |
250 lemma slast_UU [simp]: "slast$UU=UU" |
128 lemma slast_UU [simp]: "slast$UU=UU" |
251 apply (subst slast_unfold) |
129 by fixrec_simp |
252 apply simp |
|
253 done |
|
254 |
|
255 lemma slast_cons [simp]: |
|
256 "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)" |
|
257 apply (rule trans) |
|
258 apply (subst slast_unfold) |
|
259 apply simp |
|
260 apply (rule refl) |
|
261 done |
|
262 |
|
263 |
130 |
264 subsubsection {* sconc *} |
131 subsubsection {* sconc *} |
265 |
132 |
266 lemma sconc_unfold: |
133 fixrec |
267 "sconc = (LAM t1 t2. case t1 of |
134 sconc :: "'a seq -> 'a seq -> 'a seq" |
268 nil => t2 |
135 where |
269 | x##xs => x ## (xs @@ t2))" |
136 sconc_nil: "sconc$nil$y = y" |
270 by (subst fix_eq2 [OF sconc_def], simp) |
137 | sconc_cons': |
271 |
138 "x~=UU ==> sconc$(x##xs)$y = x##(sconc$xs$y)" |
272 lemma sconc_nil [simp]: "nil @@ y = y" |
139 |
273 apply (subst sconc_unfold) |
140 abbreviation |
274 apply simp |
141 sconc_syn :: "'a seq => 'a seq => 'a seq" (infixr "@@" 65) where |
275 done |
142 "xs @@ ys == sconc $ xs $ ys" |
276 |
143 |
277 lemma sconc_UU [simp]: "UU @@ y=UU" |
144 lemma sconc_UU [simp]: "UU @@ y=UU" |
278 apply (subst sconc_unfold) |
145 by fixrec_simp |
279 apply simp |
|
280 done |
|
281 |
146 |
282 lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)" |
147 lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)" |
283 apply (rule trans) |
148 apply (cases "x=UU") |
284 apply (subst sconc_unfold) |
|
285 apply simp |
|
286 apply (case_tac "x=UU") |
|
287 apply simp_all |
149 apply simp_all |
288 done |
150 done |
289 |
151 |
|
152 declare sconc_cons' [simp del] |
290 |
153 |
291 subsubsection {* sflat *} |
154 subsubsection {* sflat *} |
292 |
155 |
293 lemma sflat_unfold: |
156 fixrec |
294 "sflat = (LAM tr. case tr of |
157 sflat :: "('a seq) seq -> 'a seq" |
295 nil => nil |
158 where |
296 | x##xs => x @@ sflat$xs)" |
159 sflat_nil: "sflat$nil=nil" |
297 by (subst fix_eq2 [OF sflat_def], simp) |
160 | sflat_cons': "x~=UU ==> sflat$(x##xs)= x@@(sflat$xs)" |
298 |
|
299 lemma sflat_nil [simp]: "sflat$nil=nil" |
|
300 apply (subst sflat_unfold) |
|
301 apply simp |
|
302 done |
|
303 |
161 |
304 lemma sflat_UU [simp]: "sflat$UU=UU" |
162 lemma sflat_UU [simp]: "sflat$UU=UU" |
305 apply (subst sflat_unfold) |
163 by fixrec_simp |
306 apply simp |
|
307 done |
|
308 |
164 |
309 lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)" |
165 lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)" |
310 apply (rule trans) |
166 by (cases "x=UU", simp_all) |
311 apply (subst sflat_unfold) |
167 |
312 apply simp |
168 declare sflat_cons' [simp del] |
313 apply (case_tac "x=UU") |
|
314 apply simp_all |
|
315 done |
|
316 |
|
317 |
169 |
318 subsubsection {* szip *} |
170 subsubsection {* szip *} |
319 |
171 |
320 lemma szip_unfold: |
172 fixrec |
321 "szip = (LAM t1 t2. case t1 of |
173 szip :: "'a seq -> 'b seq -> ('a*'b) seq" |
322 nil => nil |
174 where |
323 | x##xs => (case t2 of |
175 szip_nil: "szip$nil$y=nil" |
324 nil => UU |
176 | szip_cons_nil: "x~=UU ==> szip$(x##xs)$nil=UU" |
325 | y##ys => <x,y>##(szip$xs$ys)))" |
177 | szip_cons: |
326 by (subst fix_eq2 [OF szip_def], simp) |
178 "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys" |
327 |
|
328 lemma szip_nil [simp]: "szip$nil$y=nil" |
|
329 apply (subst szip_unfold) |
|
330 apply simp |
|
331 done |
|
332 |
179 |
333 lemma szip_UU1 [simp]: "szip$UU$y=UU" |
180 lemma szip_UU1 [simp]: "szip$UU$y=UU" |
334 apply (subst szip_unfold) |
181 by fixrec_simp |
335 apply simp |
|
336 done |
|
337 |
182 |
338 lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU" |
183 lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU" |
339 apply (subst szip_unfold) |
184 by (cases x, simp_all, fixrec_simp) |
340 apply simp |
|
341 apply (rule_tac x="x" in seq.casedist) |
|
342 apply simp_all |
|
343 done |
|
344 |
|
345 lemma szip_cons_nil [simp]: "x~=UU ==> szip$(x##xs)$nil=UU" |
|
346 apply (rule trans) |
|
347 apply (subst szip_unfold) |
|
348 apply simp_all |
|
349 done |
|
350 |
|
351 lemma szip_cons [simp]: |
|
352 "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys" |
|
353 apply (rule trans) |
|
354 apply (subst szip_unfold) |
|
355 apply simp_all |
|
356 done |
|
357 |
185 |
358 |
186 |
359 subsection "scons, nil" |
187 subsection "scons, nil" |
360 |
188 |
361 lemma scons_inject_eq: |
189 lemma scons_inject_eq: |