author | wenzelm |
Mon, 25 Jul 2016 21:50:04 +0200 | |
changeset 63549 | b0d31c7def86 |
parent 62116 | bc178c0fe1a1 |
child 63648 | f9f3006a5579 |
permissions | -rw-r--r-- |
62008 | 1 |
(* Title: HOL/HOLCF/IOA/Seq.thy |
40945 | 2 |
Author: Olaf Müller |
17233 | 3 |
*) |
3071 | 4 |
|
62002 | 5 |
section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close> |
3071 | 6 |
|
17233 | 7 |
theory Seq |
56073
29e308b56d23
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
nipkow
parents:
44890
diff
changeset
|
8 |
imports "../../HOLCF" |
17233 | 9 |
begin |
3071 | 10 |
|
40329
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40322
diff
changeset
|
11 |
default_sort pcpo |
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40322
diff
changeset
|
12 |
|
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40322
diff
changeset
|
13 |
domain (unsafe) 'a seq = nil ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65) |
3071 | 14 |
|
62116 | 15 |
inductive Finite :: "'a seq \<Rightarrow> bool" |
16 |
where |
|
17 |
sfinite_0: "Finite nil" |
|
18 |
| sfinite_n: "Finite tr \<Longrightarrow> a \<noteq> UU \<Longrightarrow> Finite (a ## tr)" |
|
3071 | 19 |
|
35286 | 20 |
declare Finite.intros [simp] |
3071 | 21 |
|
62116 | 22 |
definition Partial :: "'a seq \<Rightarrow> bool" |
23 |
where "Partial x \<longleftrightarrow> seq_finite x \<and> \<not> Finite x" |
|
24 |
||
25 |
definition Infinite :: "'a seq \<Rightarrow> bool" |
|
26 |
where "Infinite x \<longleftrightarrow> \<not> seq_finite x" |
|
27 |
||
28 |
||
29 |
subsection \<open>Recursive equations of operators\<close> |
|
30 |
||
31 |
subsubsection \<open>\<open>smap\<close>\<close> |
|
32 |
||
33 |
fixrec smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a seq \<rightarrow> 'b seq" |
|
35286 | 34 |
where |
63549 | 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" |
|
62116 | 37 |
|
63549 | 38 |
lemma smap_UU [simp]: "smap \<cdot> f \<cdot> UU = UU" |
62116 | 39 |
by fixrec_simp |
40 |
||
41 |
||
42 |
subsubsection \<open>\<open>sfilter\<close>\<close> |
|
3071 | 43 |
|
62116 | 44 |
fixrec sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq" |
35286 | 45 |
where |
63549 | 46 |
sfilter_nil: "sfilter \<cdot> P \<cdot> nil = nil" |
62116 | 47 |
| sfilter_cons: |
48 |
"x \<noteq> UU \<Longrightarrow> |
|
63549 | 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)" |
|
62116 | 51 |
|
63549 | 52 |
lemma sfilter_UU [simp]: "sfilter \<cdot> P \<cdot> UU = UU" |
62116 | 53 |
by fixrec_simp |
54 |
||
55 |
||
56 |
subsubsection \<open>\<open>sforall2\<close>\<close> |
|
57 |
||
58 |
fixrec sforall2 :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> tr" |
|
59 |
where |
|
63549 | 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)" |
|
62116 | 62 |
|
63549 | 63 |
lemma sforall2_UU [simp]: "sforall2 \<cdot> P \<cdot> UU = UU" |
62116 | 64 |
by fixrec_simp |
65 |
||
63549 | 66 |
definition "sforall P t \<longleftrightarrow> sforall2 \<cdot> P \<cdot> t \<noteq> FF" |
3071 | 67 |
|
68 |
||
62116 | 69 |
subsubsection \<open>\<open>stakewhile\<close>\<close> |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
70 |
|
62116 | 71 |
fixrec stakewhile :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq" |
35286 | 72 |
where |
63549 | 73 |
stakewhile_nil: "stakewhile \<cdot> P \<cdot> nil = nil" |
35286 | 74 |
| stakewhile_cons: |
63549 | 75 |
"x \<noteq> UU \<Longrightarrow> stakewhile \<cdot> P \<cdot> (x ## xs) = (If P \<cdot> x then x ## (stakewhile \<cdot> P \<cdot> xs) else nil)" |
62116 | 76 |
|
63549 | 77 |
lemma stakewhile_UU [simp]: "stakewhile \<cdot> P \<cdot> UU = UU" |
62116 | 78 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
79 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
80 |
|
62116 | 81 |
subsubsection \<open>\<open>sdropwhile\<close>\<close> |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
82 |
|
62116 | 83 |
fixrec sdropwhile :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq" |
35286 | 84 |
where |
63549 | 85 |
sdropwhile_nil: "sdropwhile \<cdot> P \<cdot> nil = nil" |
35286 | 86 |
| sdropwhile_cons: |
63549 | 87 |
"x \<noteq> UU \<Longrightarrow> sdropwhile \<cdot> P \<cdot> (x ## xs) = (If P \<cdot> x then sdropwhile \<cdot> P \<cdot> xs else x ## xs)" |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
88 |
|
63549 | 89 |
lemma sdropwhile_UU [simp]: "sdropwhile \<cdot> P \<cdot> UU = UU" |
62116 | 90 |
by fixrec_simp |
91 |
||
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
92 |
|
62116 | 93 |
subsubsection \<open>\<open>slast\<close>\<close> |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
94 |
|
62116 | 95 |
fixrec slast :: "'a seq \<rightarrow> 'a" |
35286 | 96 |
where |
63549 | 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)" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
99 |
|
63549 | 100 |
lemma slast_UU [simp]: "slast \<cdot> UU = UU" |
62116 | 101 |
by fixrec_simp |
102 |
||
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
103 |
|
62116 | 104 |
subsubsection \<open>\<open>sconc\<close>\<close> |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
105 |
|
62116 | 106 |
fixrec sconc :: "'a seq \<rightarrow> 'a seq \<rightarrow> 'a seq" |
35286 | 107 |
where |
63549 | 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)" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
110 |
|
63549 | 111 |
abbreviation sconc_syn :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq" (infixr "@@" 65) |
112 |
where "xs @@ ys \<equiv> sconc \<cdot> xs \<cdot> ys" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
113 |
|
62116 | 114 |
lemma sconc_UU [simp]: "UU @@ y = UU" |
115 |
by fixrec_simp |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
116 |
|
62116 | 117 |
lemma sconc_cons [simp]: "(x ## xs) @@ y = x ## (xs @@ y)" |
118 |
by (cases "x = UU") simp_all |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
119 |
|
35286 | 120 |
declare sconc_cons' [simp del] |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
121 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
122 |
|
62116 | 123 |
subsubsection \<open>\<open>sflat\<close>\<close> |
124 |
||
125 |
fixrec sflat :: "'a seq seq \<rightarrow> 'a seq" |
|
35286 | 126 |
where |
63549 | 127 |
sflat_nil: "sflat \<cdot> nil = nil" |
128 |
| sflat_cons': "x \<noteq> UU \<Longrightarrow> sflat \<cdot> (x ## xs) = x @@ (sflat \<cdot> xs)" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
129 |
|
63549 | 130 |
lemma sflat_UU [simp]: "sflat \<cdot> UU = UU" |
62116 | 131 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
132 |
|
63549 | 133 |
lemma sflat_cons [simp]: "sflat \<cdot> (x ## xs) = x @@ (sflat \<cdot> xs)" |
62116 | 134 |
by (cases "x = UU") simp_all |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
135 |
|
35286 | 136 |
declare sflat_cons' [simp del] |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
137 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
138 |
|
62116 | 139 |
subsubsection \<open>\<open>szip\<close>\<close> |
140 |
||
141 |
fixrec szip :: "'a seq \<rightarrow> 'b seq \<rightarrow> ('a \<times> 'b) seq" |
|
35286 | 142 |
where |
63549 | 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" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
146 |
|
63549 | 147 |
lemma szip_UU1 [simp]: "szip \<cdot> UU \<cdot> y = UU" |
62116 | 148 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
149 |
|
63549 | 150 |
lemma szip_UU2 [simp]: "x \<noteq> nil \<Longrightarrow> szip \<cdot> x \<cdot> UU = UU" |
62116 | 151 |
by (cases x) (simp_all, fixrec_simp) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
152 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
153 |
|
62116 | 154 |
subsection \<open>\<open>scons\<close>, \<open>nil\<close>\<close> |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
155 |
|
62116 | 156 |
lemma scons_inject_eq: "x \<noteq> UU \<Longrightarrow> y \<noteq> UU \<Longrightarrow> x ## xs = y ## ys \<longleftrightarrow> x = y \<and> xs = ys" |
157 |
by simp |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
158 |
|
62116 | 159 |
lemma nil_less_is_nil: "nil \<sqsubseteq> x \<Longrightarrow> nil = x" |
160 |
by (cases x) simp_all |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
161 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
162 |
|
62116 | 163 |
subsection \<open>\<open>sfilter\<close>, \<open>sforall\<close>, \<open>sconc\<close>\<close> |
164 |
||
165 |
lemma if_and_sconc [simp]: |
|
166 |
"(if b then tr1 else tr2) @@ tr = (if b then tr1 @@ tr else tr2 @@ tr)" |
|
167 |
by simp |
|
168 |
||
63549 | 169 |
lemma sfiltersconc: "sfilter \<cdot> P \<cdot> (x @@ y) = (sfilter \<cdot> P \<cdot> x @@ sfilter \<cdot> P \<cdot> y)" |
62116 | 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> |
|
63549 | 177 |
apply (rule_tac p = "P\<cdot>a" in trE) |
62116 | 178 |
apply simp |
179 |
apply simp |
|
180 |
apply simp |
|
181 |
done |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
182 |
|
63549 | 183 |
lemma sforallPstakewhileP: "sforall P (stakewhile \<cdot> P \<cdot> x)" |
62116 | 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> |
|
63549 | 192 |
apply (rule_tac p = "P\<cdot>a" in trE) |
62116 | 193 |
apply simp |
194 |
apply simp |
|
195 |
apply simp |
|
196 |
done |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
197 |
|
63549 | 198 |
lemma forallPsfilterP: "sforall P (sfilter \<cdot> P \<cdot> x)" |
62116 | 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> |
|
63549 | 207 |
apply (rule_tac p="P\<cdot>a" in trE) |
62116 | 208 |
apply simp |
209 |
apply simp |
|
210 |
apply simp |
|
211 |
done |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
212 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
213 |
|
62116 | 214 |
subsection \<open>Finite\<close> |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
215 |
|
62116 | 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 |
*) |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
222 |
|
62116 | 223 |
lemma 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 |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
229 |
|
62116 | 230 |
lemma Finite_UU [simp]: "\<not> Finite UU" |
231 |
using Finite_UU_a [where x = UU] by fast |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
232 |
|
62116 | 233 |
lemma 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 |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
239 |
|
62116 | 240 |
lemma 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 |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
246 |
|
62116 | 247 |
lemma 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 |
|
25803 | 253 |
|
254 |
lemma adm_Finite [simp]: "adm Finite" |
|
62116 | 255 |
by (rule adm_upward) (rule Finite_upward) |
25803 | 256 |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
257 |
|
62116 | 258 |
subsection \<open>Induction\<close> |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
259 |
|
62116 | 260 |
text \<open>Extensions to Induction Theorems.\<close> |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
261 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
262 |
lemma seq_finite_ind_lemma: |
63549 | 263 |
assumes "\<And>n. P (seq_take n \<cdot> s)" |
62116 | 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 |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
271 |
|
62116 | 272 |
lemma 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 |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
283 |
|
3071 | 284 |
end |