author | huffman |
Tue, 12 Oct 2010 09:32:21 -0700 | |
changeset 40009 | f2c78550c0b7 |
parent 39159 | 0dec18004e75 |
child 40087 | 1b5f394866d9 |
permissions | -rw-r--r-- |
17293 | 1 |
(* Title: HOLCF/FOCUS/Fstream.thy |
2 |
Author: David von Oheimb, TU Muenchen |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
3 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30807
diff
changeset
|
4 |
FOCUS streams (with lifted elements). |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30807
diff
changeset
|
5 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30807
diff
changeset
|
6 |
TODO: integrate Fstreams.thy |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
7 |
*) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
8 |
|
17293 | 9 |
header {* FOCUS flat streams *} |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
10 |
|
17293 | 11 |
theory Fstream |
37110
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
36452
diff
changeset
|
12 |
imports Stream |
17293 | 13 |
begin |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
14 |
|
36452 | 15 |
default_sort type |
17293 | 16 |
|
17 |
types 'a fstream = "'a lift stream" |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
18 |
|
19763 | 19 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
20 |
fscons :: "'a \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where |
19763 | 21 |
"fscons a = (\<Lambda> s. Def a && s)" |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
22 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
23 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
24 |
fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where |
19763 | 25 |
"fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))" |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
26 |
|
19763 | 27 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
28 |
emptystream :: "'a fstream" ("<>") where |
19763 | 29 |
"<> == \<bottom>" |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
30 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
31 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
32 |
fscons' :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_~>_)" [66,65] 65) where |
19763 | 33 |
"a~>s == fscons a\<cdot>s" |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
34 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
35 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
36 |
fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63) where |
19763 | 37 |
"A(C)s == fsfilter A\<cdot>s" |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
38 |
|
21210 | 39 |
notation (xsymbols) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
40 |
fscons' ("(_\<leadsto>_)" [66,65] 65) and |
19763 | 41 |
fsfilter' ("(_\<copyright>_)" [64,63] 63) |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
42 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
43 |
|
19759 | 44 |
lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d" |
45 |
apply (rule flat_eq [THEN iffD1, symmetric]) |
|
46 |
apply (rule Def_not_UU) |
|
47 |
apply (drule antisym_less_inverse) |
|
48 |
apply (erule (1) conjunct2 [THEN trans_less]) |
|
49 |
done |
|
50 |
||
51 |
||
52 |
section "fscons" |
|
53 |
||
54 |
lemma fscons_def2: "a~>s = Def a && s" |
|
55 |
apply (unfold fscons_def) |
|
56 |
apply (simp) |
|
57 |
done |
|
58 |
||
59 |
lemma fstream_exhaust: "x = UU | (? a y. x = a~> y)" |
|
60 |
apply (simp add: fscons_def2) |
|
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35532
diff
changeset
|
61 |
apply (cut_tac stream.nchotomy) |
19759 | 62 |
apply (fast dest: not_Undef_is_Def [THEN iffD1]) |
63 |
done |
|
64 |
||
65 |
lemma fstream_cases: "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P" |
|
66 |
apply (cut_tac fstream_exhaust) |
|
67 |
apply (erule disjE) |
|
68 |
apply fast |
|
69 |
apply fast |
|
70 |
done |
|
27148 | 71 |
|
19759 | 72 |
lemma fstream_exhaust_eq: "(x ~= UU) = (? a y. x = a~> y)" |
73 |
apply (simp add: fscons_def2 stream_exhaust_eq) |
|
74 |
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) |
|
75 |
done |
|
76 |
||
77 |
||
78 |
lemma fscons_not_empty [simp]: "a~> s ~= <>" |
|
79 |
by (simp add: fscons_def2) |
|
80 |
||
81 |
||
82 |
lemma fscons_inject [simp]: "(a~> s = b~> t) = (a = b & s = t)" |
|
83 |
by (simp add: fscons_def2) |
|
84 |
||
85 |
lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt & s << tt" |
|
35532
60647586b173
adapt to changed variable name in casedist theorem
huffman
parents:
35215
diff
changeset
|
86 |
apply (cases t) |
19759 | 87 |
apply (cut_tac fscons_not_empty) |
88 |
apply (fast dest: eq_UU_iff [THEN iffD2]) |
|
89 |
apply (simp add: fscons_def2) |
|
90 |
done |
|
91 |
||
92 |
lemma fstream_prefix' [simp]: |
|
93 |
"x << a~> z = (x = <> | (? y. x = a~> y & y << z))" |
|
94 |
apply (simp add: fscons_def2 Def_not_UU [THEN stream_prefix']) |
|
95 |
apply (safe) |
|
96 |
apply (erule_tac [!] contrapos_np) |
|
97 |
prefer 2 apply (fast elim: DefE) |
|
40009 | 98 |
apply (rule lift.exhaust) |
19759 | 99 |
apply (erule (1) notE) |
100 |
apply (safe) |
|
101 |
apply (drule Def_inject_less_eq [THEN iffD1]) |
|
102 |
apply fast |
|
103 |
done |
|
104 |
||
105 |
(* ------------------------------------------------------------------------- *) |
|
106 |
||
107 |
section "ft & rt" |
|
108 |
||
109 |
lemmas ft_empty = stream.sel_rews (1) |
|
110 |
lemma ft_fscons [simp]: "ft\<cdot>(m~> s) = Def m" |
|
111 |
by (simp add: fscons_def) |
|
112 |
||
113 |
lemmas rt_empty = stream.sel_rews (2) |
|
114 |
lemma rt_fscons [simp]: "rt\<cdot>(m~> s) = s" |
|
115 |
by (simp add: fscons_def) |
|
116 |
||
117 |
lemma ft_eq [simp]: "(ft\<cdot>s = Def a) = (? t. s = a~> t)" |
|
118 |
apply (unfold fscons_def) |
|
119 |
apply (simp) |
|
120 |
apply (safe) |
|
121 |
apply (erule subst) |
|
122 |
apply (rule exI) |
|
123 |
apply (rule surjectiv_scons [symmetric]) |
|
124 |
apply (simp) |
|
125 |
done |
|
126 |
||
127 |
lemma surjective_fscons_lemma: "(d\<leadsto>y = x) = (ft\<cdot>x = Def d & rt\<cdot>x = y)" |
|
128 |
by auto |
|
129 |
||
130 |
lemma surjective_fscons: "ft\<cdot>x = Def d \<Longrightarrow> d\<leadsto>rt\<cdot>x = x" |
|
131 |
by (simp add: surjective_fscons_lemma) |
|
132 |
||
133 |
||
134 |
(* ------------------------------------------------------------------------- *) |
|
135 |
||
136 |
section "take" |
|
137 |
||
138 |
lemma fstream_take_Suc [simp]: |
|
139 |
"stream_take (Suc n)\<cdot>(a~> s) = a~> stream_take n\<cdot>s" |
|
140 |
by (simp add: fscons_def) |
|
141 |
||
142 |
||
143 |
(* ------------------------------------------------------------------------- *) |
|
144 |
||
145 |
section "slen" |
|
146 |
||
147 |
lemma slen_fscons: "#(m~> s) = iSuc (#s)" |
|
148 |
by (simp add: fscons_def) |
|
149 |
||
150 |
lemma slen_fscons_eq: |
|
151 |
"(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)" |
|
152 |
apply (simp add: fscons_def2 slen_scons_eq) |
|
153 |
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) |
|
154 |
done |
|
155 |
||
156 |
lemma slen_fscons_eq_rev: |
|
157 |
"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" |
|
158 |
apply (simp add: fscons_def2 slen_scons_eq_rev) |
|
39159 | 159 |
apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) |
160 |
apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) |
|
161 |
apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) |
|
162 |
apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) |
|
163 |
apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) |
|
164 |
apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) |
|
19759 | 165 |
apply (erule contrapos_np) |
166 |
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) |
|
167 |
done |
|
168 |
||
169 |
lemma slen_fscons_less_eq: |
|
170 |
"(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))" |
|
171 |
apply (subst slen_fscons_eq_rev) |
|
172 |
apply (fast dest!: fscons_inject [THEN iffD1]) |
|
173 |
done |
|
174 |
||
175 |
||
176 |
(* ------------------------------------------------------------------------- *) |
|
177 |
||
178 |
section "induction" |
|
179 |
||
180 |
lemma fstream_ind: |
|
181 |
"[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" |
|
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35532
diff
changeset
|
182 |
apply (erule stream.induct) |
19759 | 183 |
apply (assumption) |
184 |
apply (unfold fscons_def2) |
|
185 |
apply (fast dest: not_Undef_is_Def [THEN iffD1]) |
|
186 |
done |
|
187 |
||
188 |
lemma fstream_ind2: |
|
189 |
"[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x" |
|
190 |
apply (erule stream_ind2) |
|
191 |
apply (assumption) |
|
192 |
apply (unfold fscons_def2) |
|
193 |
apply (fast dest: not_Undef_is_Def [THEN iffD1]) |
|
194 |
apply (fast dest: not_Undef_is_Def [THEN iffD1]) |
|
195 |
done |
|
196 |
||
197 |
||
198 |
(* ------------------------------------------------------------------------- *) |
|
199 |
||
200 |
section "fsfilter" |
|
201 |
||
202 |
lemma fsfilter_empty: "A(C)UU = UU" |
|
203 |
apply (unfold fsfilter_def) |
|
204 |
apply (rule sfilter_empty) |
|
205 |
done |
|
206 |
||
207 |
lemma fsfilter_fscons: |
|
208 |
"A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" |
|
209 |
apply (unfold fsfilter_def) |
|
35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
32960
diff
changeset
|
210 |
apply (simp add: fscons_def2 If_and_if) |
19759 | 211 |
done |
212 |
||
213 |
lemma fsfilter_emptys: "{}(C)x = UU" |
|
214 |
apply (rule_tac x="x" in fstream_ind) |
|
215 |
apply (simp) |
|
216 |
apply (rule fsfilter_empty) |
|
217 |
apply (simp add: fsfilter_fscons) |
|
218 |
done |
|
219 |
||
220 |
lemma fsfilter_insert: "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" |
|
221 |
by (simp add: fsfilter_fscons) |
|
222 |
||
223 |
lemma fsfilter_single_in: "{a}(C)a~> x = a~> ({a}(C)x)" |
|
224 |
by (rule fsfilter_insert) |
|
225 |
||
226 |
lemma fsfilter_single_out: "b ~= a ==> {a}(C)b~> x = ({a}(C)x)" |
|
227 |
by (simp add: fsfilter_fscons) |
|
228 |
||
229 |
lemma fstream_lub_lemma1: |
|
27413 | 230 |
"\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t" |
19759 | 231 |
apply (case_tac "max_in_chain i Y") |
232 |
apply (drule (1) lub_finch1 [THEN thelubI, THEN sym]) |
|
233 |
apply (force) |
|
234 |
apply (unfold max_in_chain_def) |
|
235 |
apply auto |
|
25922
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
24327
diff
changeset
|
236 |
apply (frule (1) chain_mono) |
19759 | 237 |
apply (rule_tac x="Y j" in fstream_cases) |
238 |
apply (force) |
|
239 |
apply (drule_tac x="j" in is_ub_thelub) |
|
240 |
apply (force) |
|
241 |
done |
|
242 |
||
243 |
lemma fstream_lub_lemma: |
|
27413 | 244 |
"\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> (\<exists>j t. Y j = a\<leadsto>t) & (\<exists>X. chain X & (!i. ? j. Y j = a\<leadsto>X i) & (\<Squnion>i. X i) = s)" |
19759 | 245 |
apply (frule (1) fstream_lub_lemma1) |
246 |
apply (clarsimp) |
|
247 |
apply (rule_tac x="%i. rt\<cdot>(Y(i+j))" in exI) |
|
248 |
apply (rule conjI) |
|
249 |
apply (erule chain_shift [THEN chain_monofun]) |
|
250 |
apply safe |
|
25922
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
24327
diff
changeset
|
251 |
apply (drule_tac i="j" and j="i+j" in chain_mono) |
19759 | 252 |
apply (simp) |
253 |
apply (simp) |
|
254 |
apply (rule_tac x="i+j" in exI) |
|
255 |
apply (drule fstream_prefix) |
|
256 |
apply (clarsimp) |
|
257 |
apply (subst contlub_cfun [symmetric]) |
|
258 |
apply (rule chainI) |
|
259 |
apply (fast) |
|
260 |
apply (erule chain_shift) |
|
261 |
apply (subst lub_const [THEN thelubI]) |
|
262 |
apply (subst lub_range_shift) |
|
263 |
apply (assumption) |
|
264 |
apply (simp) |
|
265 |
done |
|
266 |
||
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
267 |
end |