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