wenzelm@43022
|
1 |
(* Title: HOL/HOLCF/IOA/meta_theory/Seq.thy
|
wenzelm@41193
|
2 |
Author: Olaf Müller
|
wenzelm@17233
|
3 |
*)
|
mueller@3071
|
4 |
|
wenzelm@17233
|
5 |
header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
|
mueller@3071
|
6 |
|
wenzelm@17233
|
7 |
theory Seq
|
wenzelm@17233
|
8 |
imports HOLCF
|
wenzelm@17233
|
9 |
begin
|
mueller@3071
|
10 |
|
huffman@40567
|
11 |
default_sort pcpo
|
huffman@40567
|
12 |
|
huffman@40567
|
13 |
domain (unsafe) 'a seq = nil ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65)
|
mueller@3071
|
14 |
|
huffman@35286
|
15 |
(*
|
wenzelm@17233
|
16 |
sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
|
mueller@3071
|
17 |
smap :: "('a -> 'b) -> 'a seq -> 'b seq"
|
mueller@3071
|
18 |
sforall :: "('a -> tr) => 'a seq => bool"
|
mueller@3071
|
19 |
sforall2 :: "('a -> tr) -> 'a seq -> tr"
|
mueller@3071
|
20 |
slast :: "'a seq -> 'a"
|
mueller@3071
|
21 |
sconc :: "'a seq -> 'a seq -> 'a seq"
|
huffman@35286
|
22 |
sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq"
|
huffman@35286
|
23 |
stakewhile :: "('a -> tr) -> 'a seq -> 'a seq"
|
huffman@35286
|
24 |
szip :: "'a seq -> 'b seq -> ('a*'b) seq"
|
mueller@3071
|
25 |
sflat :: "('a seq) seq -> 'a seq"
|
mueller@3071
|
26 |
|
mueller@3071
|
27 |
sfinite :: "'a seq set"
|
huffman@35286
|
28 |
Partial :: "'a seq => bool"
|
huffman@35286
|
29 |
Infinite :: "'a seq => bool"
|
mueller@3071
|
30 |
|
mueller@3071
|
31 |
nproj :: "nat => 'a seq => 'a"
|
mueller@4282
|
32 |
sproj :: "nat => 'a seq => 'a seq"
|
huffman@35286
|
33 |
*)
|
mueller@3071
|
34 |
|
berghofe@23778
|
35 |
inductive
|
berghofe@23778
|
36 |
Finite :: "'a seq => bool"
|
berghofe@23778
|
37 |
where
|
berghofe@23778
|
38 |
sfinite_0: "Finite nil"
|
berghofe@23778
|
39 |
| sfinite_n: "[| Finite tr; a~=UU |] ==> Finite (a##tr)"
|
mueller@3071
|
40 |
|
huffman@35286
|
41 |
declare Finite.intros [simp]
|
mueller@3071
|
42 |
|
huffman@35286
|
43 |
definition
|
huffman@35286
|
44 |
Partial :: "'a seq => bool"
|
huffman@35286
|
45 |
where
|
mueller@3071
|
46 |
"Partial x == (seq_finite x) & ~(Finite x)"
|
mueller@3071
|
47 |
|
huffman@35286
|
48 |
definition
|
huffman@35286
|
49 |
Infinite :: "'a seq => bool"
|
huffman@35286
|
50 |
where
|
mueller@3071
|
51 |
"Infinite x == ~(seq_finite x)"
|
mueller@3071
|
52 |
|
mueller@3071
|
53 |
|
huffman@19550
|
54 |
subsection {* recursive equations of operators *}
|
huffman@19550
|
55 |
|
huffman@19550
|
56 |
subsubsection {* smap *}
|
huffman@19550
|
57 |
|
huffman@35286
|
58 |
fixrec
|
huffman@35286
|
59 |
smap :: "('a -> 'b) -> 'a seq -> 'b seq"
|
huffman@35286
|
60 |
where
|
huffman@35286
|
61 |
smap_nil: "smap$f$nil=nil"
|
huffman@35286
|
62 |
| smap_cons: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"
|
huffman@19550
|
63 |
|
huffman@19550
|
64 |
lemma smap_UU [simp]: "smap$f$UU=UU"
|
huffman@35286
|
65 |
by fixrec_simp
|
huffman@19550
|
66 |
|
huffman@19550
|
67 |
subsubsection {* sfilter *}
|
huffman@19550
|
68 |
|
huffman@35286
|
69 |
fixrec
|
huffman@35286
|
70 |
sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
|
huffman@35286
|
71 |
where
|
huffman@35286
|
72 |
sfilter_nil: "sfilter$P$nil=nil"
|
huffman@35286
|
73 |
| sfilter_cons:
|
huffman@35286
|
74 |
"x~=UU ==> sfilter$P$(x##xs)=
|
huffman@40560
|
75 |
(If P$x then x##(sfilter$P$xs) else sfilter$P$xs)"
|
huffman@19550
|
76 |
|
huffman@19550
|
77 |
lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
|
huffman@35286
|
78 |
by fixrec_simp
|
huffman@19550
|
79 |
|
huffman@19550
|
80 |
subsubsection {* sforall2 *}
|
huffman@19550
|
81 |
|
huffman@35286
|
82 |
fixrec
|
huffman@35286
|
83 |
sforall2 :: "('a -> tr) -> 'a seq -> tr"
|
huffman@35286
|
84 |
where
|
huffman@35286
|
85 |
sforall2_nil: "sforall2$P$nil=TT"
|
huffman@35286
|
86 |
| sforall2_cons:
|
huffman@35286
|
87 |
"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)"
|
huffman@19550
|
88 |
|
huffman@19550
|
89 |
lemma sforall2_UU [simp]: "sforall2$P$UU=UU"
|
huffman@35286
|
90 |
by fixrec_simp
|
huffman@19550
|
91 |
|
huffman@35286
|
92 |
definition
|
huffman@35286
|
93 |
sforall_def: "sforall P t == (sforall2$P$t ~=FF)"
|
huffman@19550
|
94 |
|
huffman@19550
|
95 |
subsubsection {* stakewhile *}
|
huffman@19550
|
96 |
|
huffman@35286
|
97 |
fixrec
|
huffman@35286
|
98 |
stakewhile :: "('a -> tr) -> 'a seq -> 'a seq"
|
huffman@35286
|
99 |
where
|
huffman@35286
|
100 |
stakewhile_nil: "stakewhile$P$nil=nil"
|
huffman@35286
|
101 |
| stakewhile_cons:
|
huffman@35286
|
102 |
"x~=UU ==> stakewhile$P$(x##xs) =
|
huffman@40560
|
103 |
(If P$x then x##(stakewhile$P$xs) else nil)"
|
huffman@19550
|
104 |
|
huffman@19550
|
105 |
lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
|
huffman@35286
|
106 |
by fixrec_simp
|
huffman@19550
|
107 |
|
huffman@19550
|
108 |
subsubsection {* sdropwhile *}
|
huffman@19550
|
109 |
|
huffman@35286
|
110 |
fixrec
|
huffman@35286
|
111 |
sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq"
|
huffman@35286
|
112 |
where
|
huffman@35286
|
113 |
sdropwhile_nil: "sdropwhile$P$nil=nil"
|
huffman@35286
|
114 |
| sdropwhile_cons:
|
huffman@35286
|
115 |
"x~=UU ==> sdropwhile$P$(x##xs) =
|
huffman@40560
|
116 |
(If P$x then sdropwhile$P$xs else x##xs)"
|
huffman@19550
|
117 |
|
huffman@19550
|
118 |
lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
|
huffman@35286
|
119 |
by fixrec_simp
|
huffman@19550
|
120 |
|
huffman@19550
|
121 |
subsubsection {* slast *}
|
huffman@19550
|
122 |
|
huffman@35286
|
123 |
fixrec
|
huffman@35286
|
124 |
slast :: "'a seq -> 'a"
|
huffman@35286
|
125 |
where
|
huffman@35286
|
126 |
slast_nil: "slast$nil=UU"
|
huffman@35286
|
127 |
| slast_cons:
|
huffman@40560
|
128 |
"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs)"
|
huffman@19550
|
129 |
|
huffman@19550
|
130 |
lemma slast_UU [simp]: "slast$UU=UU"
|
huffman@35286
|
131 |
by fixrec_simp
|
huffman@19550
|
132 |
|
huffman@19550
|
133 |
subsubsection {* sconc *}
|
huffman@19550
|
134 |
|
huffman@35286
|
135 |
fixrec
|
huffman@35286
|
136 |
sconc :: "'a seq -> 'a seq -> 'a seq"
|
huffman@35286
|
137 |
where
|
huffman@35286
|
138 |
sconc_nil: "sconc$nil$y = y"
|
huffman@35286
|
139 |
| sconc_cons':
|
huffman@35286
|
140 |
"x~=UU ==> sconc$(x##xs)$y = x##(sconc$xs$y)"
|
huffman@19550
|
141 |
|
huffman@35286
|
142 |
abbreviation
|
huffman@35286
|
143 |
sconc_syn :: "'a seq => 'a seq => 'a seq" (infixr "@@" 65) where
|
huffman@35286
|
144 |
"xs @@ ys == sconc $ xs $ ys"
|
huffman@19550
|
145 |
|
huffman@19550
|
146 |
lemma sconc_UU [simp]: "UU @@ y=UU"
|
huffman@35286
|
147 |
by fixrec_simp
|
huffman@19550
|
148 |
|
huffman@19550
|
149 |
lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)"
|
huffman@35286
|
150 |
apply (cases "x=UU")
|
huffman@19550
|
151 |
apply simp_all
|
huffman@19550
|
152 |
done
|
huffman@19550
|
153 |
|
huffman@35286
|
154 |
declare sconc_cons' [simp del]
|
huffman@19550
|
155 |
|
huffman@19550
|
156 |
subsubsection {* sflat *}
|
huffman@19550
|
157 |
|
huffman@35286
|
158 |
fixrec
|
huffman@35286
|
159 |
sflat :: "('a seq) seq -> 'a seq"
|
huffman@35286
|
160 |
where
|
huffman@35286
|
161 |
sflat_nil: "sflat$nil=nil"
|
huffman@35286
|
162 |
| sflat_cons': "x~=UU ==> sflat$(x##xs)= x@@(sflat$xs)"
|
huffman@19550
|
163 |
|
huffman@19550
|
164 |
lemma sflat_UU [simp]: "sflat$UU=UU"
|
huffman@35286
|
165 |
by fixrec_simp
|
huffman@19550
|
166 |
|
huffman@19550
|
167 |
lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)"
|
huffman@35286
|
168 |
by (cases "x=UU", simp_all)
|
huffman@19550
|
169 |
|
huffman@35286
|
170 |
declare sflat_cons' [simp del]
|
huffman@19550
|
171 |
|
huffman@19550
|
172 |
subsubsection {* szip *}
|
huffman@19550
|
173 |
|
huffman@35286
|
174 |
fixrec
|
huffman@35286
|
175 |
szip :: "'a seq -> 'b seq -> ('a*'b) seq"
|
huffman@35286
|
176 |
where
|
huffman@35286
|
177 |
szip_nil: "szip$nil$y=nil"
|
huffman@35286
|
178 |
| szip_cons_nil: "x~=UU ==> szip$(x##xs)$nil=UU"
|
huffman@35286
|
179 |
| szip_cons:
|
huffman@35924
|
180 |
"[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = (x,y)##szip$xs$ys"
|
huffman@19550
|
181 |
|
huffman@19550
|
182 |
lemma szip_UU1 [simp]: "szip$UU$y=UU"
|
huffman@35286
|
183 |
by fixrec_simp
|
huffman@19550
|
184 |
|
huffman@19550
|
185 |
lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU"
|
huffman@35286
|
186 |
by (cases x, simp_all, fixrec_simp)
|
huffman@19550
|
187 |
|
huffman@19550
|
188 |
|
huffman@19550
|
189 |
subsection "scons, nil"
|
huffman@19550
|
190 |
|
huffman@19550
|
191 |
lemma scons_inject_eq:
|
huffman@19550
|
192 |
"[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)"
|
huffman@35207
|
193 |
by simp
|
huffman@19550
|
194 |
|
huffman@19550
|
195 |
lemma nil_less_is_nil: "nil<<x ==> nil=x"
|
huffman@35518
|
196 |
apply (cases x)
|
huffman@19550
|
197 |
apply simp
|
huffman@19550
|
198 |
apply simp
|
huffman@19550
|
199 |
apply simp
|
huffman@19550
|
200 |
done
|
huffman@19550
|
201 |
|
huffman@19550
|
202 |
subsection "sfilter, sforall, sconc"
|
huffman@19550
|
203 |
|
huffman@19550
|
204 |
lemma if_and_sconc [simp]: "(if b then tr1 else tr2) @@ tr
|
huffman@19550
|
205 |
= (if b then tr1 @@ tr else tr2 @@ tr)"
|
huffman@19550
|
206 |
by simp
|
huffman@19550
|
207 |
|
huffman@19550
|
208 |
|
huffman@19550
|
209 |
lemma sfiltersconc: "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)"
|
huffman@35781
|
210 |
apply (induct x)
|
huffman@19550
|
211 |
(* adm *)
|
huffman@19550
|
212 |
apply simp
|
huffman@19550
|
213 |
(* base cases *)
|
huffman@19550
|
214 |
apply simp
|
huffman@19550
|
215 |
apply simp
|
huffman@19550
|
216 |
(* main case *)
|
huffman@19550
|
217 |
apply (rule_tac p="P$a" in trE)
|
huffman@19550
|
218 |
apply simp
|
huffman@19550
|
219 |
apply simp
|
huffman@19550
|
220 |
apply simp
|
huffman@19550
|
221 |
done
|
huffman@19550
|
222 |
|
huffman@19550
|
223 |
lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)"
|
huffman@19550
|
224 |
apply (simp add: sforall_def)
|
huffman@35781
|
225 |
apply (induct x)
|
huffman@19550
|
226 |
(* adm *)
|
huffman@19550
|
227 |
apply simp
|
huffman@19550
|
228 |
(* base cases *)
|
huffman@19550
|
229 |
apply simp
|
huffman@19550
|
230 |
apply simp
|
huffman@19550
|
231 |
(* main case *)
|
huffman@19550
|
232 |
apply (rule_tac p="P$a" in trE)
|
huffman@19550
|
233 |
apply simp
|
huffman@19550
|
234 |
apply simp
|
huffman@19550
|
235 |
apply simp
|
huffman@19550
|
236 |
done
|
huffman@19550
|
237 |
|
huffman@19550
|
238 |
lemma forallPsfilterP: "sforall P (sfilter$P$x)"
|
huffman@19550
|
239 |
apply (simp add: sforall_def)
|
huffman@35781
|
240 |
apply (induct x)
|
huffman@19550
|
241 |
(* adm *)
|
huffman@19550
|
242 |
apply simp
|
huffman@19550
|
243 |
(* base cases *)
|
huffman@19550
|
244 |
apply simp
|
huffman@19550
|
245 |
apply simp
|
huffman@19550
|
246 |
(* main case *)
|
huffman@19550
|
247 |
apply (rule_tac p="P$a" in trE)
|
huffman@19550
|
248 |
apply simp
|
huffman@19550
|
249 |
apply simp
|
huffman@19550
|
250 |
apply simp
|
huffman@19550
|
251 |
done
|
huffman@19550
|
252 |
|
huffman@19550
|
253 |
|
huffman@19550
|
254 |
subsection "Finite"
|
huffman@19550
|
255 |
|
huffman@19550
|
256 |
(* ---------------------------------------------------- *)
|
huffman@19550
|
257 |
(* Proofs of rewrite rules for Finite: *)
|
huffman@19550
|
258 |
(* 1. Finite(nil), (by definition) *)
|
huffman@19550
|
259 |
(* 2. ~Finite(UU), *)
|
huffman@19550
|
260 |
(* 3. a~=UU==> Finite(a##x)=Finite(x) *)
|
huffman@19550
|
261 |
(* ---------------------------------------------------- *)
|
huffman@19550
|
262 |
|
huffman@19550
|
263 |
lemma Finite_UU_a: "Finite x --> x~=UU"
|
huffman@19550
|
264 |
apply (rule impI)
|
berghofe@23778
|
265 |
apply (erule Finite.induct)
|
huffman@19550
|
266 |
apply simp
|
huffman@19550
|
267 |
apply simp
|
huffman@19550
|
268 |
done
|
huffman@19550
|
269 |
|
huffman@19550
|
270 |
lemma Finite_UU [simp]: "~(Finite UU)"
|
huffman@19550
|
271 |
apply (cut_tac x="UU" in Finite_UU_a)
|
huffman@19550
|
272 |
apply fast
|
huffman@19550
|
273 |
done
|
huffman@19550
|
274 |
|
huffman@19550
|
275 |
lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs"
|
huffman@19550
|
276 |
apply (intro strip)
|
berghofe@23778
|
277 |
apply (erule Finite.cases)
|
nipkow@45761
|
278 |
apply fastforce
|
huffman@35207
|
279 |
apply simp
|
huffman@19550
|
280 |
done
|
huffman@19550
|
281 |
|
huffman@19550
|
282 |
lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)"
|
huffman@19550
|
283 |
apply (rule iffI)
|
huffman@19550
|
284 |
apply (erule (1) Finite_cons_a [rule_format])
|
huffman@19550
|
285 |
apply fast
|
huffman@19550
|
286 |
apply simp
|
huffman@19550
|
287 |
done
|
huffman@19550
|
288 |
|
huffman@25803
|
289 |
lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y"
|
huffman@25803
|
290 |
apply (induct arbitrary: y set: Finite)
|
huffman@35518
|
291 |
apply (case_tac y, simp, simp, simp)
|
huffman@35518
|
292 |
apply (case_tac y, simp, simp)
|
huffman@35207
|
293 |
apply simp
|
huffman@25803
|
294 |
done
|
huffman@25803
|
295 |
|
huffman@25803
|
296 |
lemma adm_Finite [simp]: "adm Finite"
|
huffman@25803
|
297 |
by (rule adm_upward, rule Finite_upward)
|
huffman@25803
|
298 |
|
huffman@19550
|
299 |
|
huffman@19550
|
300 |
subsection "induction"
|
huffman@19550
|
301 |
|
huffman@19550
|
302 |
|
huffman@19550
|
303 |
(*-------------------------------- *)
|
huffman@19550
|
304 |
(* Extensions to Induction Theorems *)
|
huffman@19550
|
305 |
(*-------------------------------- *)
|
huffman@19550
|
306 |
|
huffman@19550
|
307 |
|
huffman@19550
|
308 |
lemma seq_finite_ind_lemma:
|
huffman@19550
|
309 |
assumes "(!!n. P(seq_take n$s))"
|
huffman@19550
|
310 |
shows "seq_finite(s) -->P(s)"
|
huffman@19550
|
311 |
apply (unfold seq.finite_def)
|
huffman@19550
|
312 |
apply (intro strip)
|
huffman@19550
|
313 |
apply (erule exE)
|
huffman@19550
|
314 |
apply (erule subst)
|
wenzelm@41777
|
315 |
apply (rule assms)
|
huffman@19550
|
316 |
done
|
huffman@19550
|
317 |
|
huffman@19550
|
318 |
|
huffman@19550
|
319 |
lemma seq_finite_ind: "!!P.[|P(UU);P(nil);
|
huffman@19550
|
320 |
!! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)
|
huffman@19550
|
321 |
|] ==> seq_finite(s) --> P(s)"
|
huffman@19550
|
322 |
apply (rule seq_finite_ind_lemma)
|
huffman@35781
|
323 |
apply (erule seq.finite_induct)
|
huffman@19550
|
324 |
apply assumption
|
huffman@19550
|
325 |
apply simp
|
huffman@19550
|
326 |
done
|
huffman@19550
|
327 |
|
mueller@3071
|
328 |
end
|