wenzelm@17291
|
1 |
(* Title: HOLCF/ex/Stream.thy
|
paulson@9169
|
2 |
ID: $Id$
|
wenzelm@17291
|
3 |
Author: Franz Regensburger, David von Oheimb, Borislav Gajanovic
|
oheimb@2570
|
4 |
*)
|
oheimb@2570
|
5 |
|
wenzelm@17291
|
6 |
header {* General Stream domain *}
|
wenzelm@17291
|
7 |
|
wenzelm@17291
|
8 |
theory Stream
|
wenzelm@17291
|
9 |
imports HOLCF Nat_Infinity
|
wenzelm@17291
|
10 |
begin
|
oheimb@2570
|
11 |
|
wenzelm@22808
|
12 |
domain 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
|
oheimb@2570
|
13 |
|
wenzelm@19763
|
14 |
definition
|
wenzelm@21404
|
15 |
smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream" where
|
wenzelm@19763
|
16 |
"smap = fix\<cdot>(\<Lambda> h f s. case s of x && xs \<Rightarrow> f\<cdot>x && h\<cdot>f\<cdot>xs)"
|
oheimb@11348
|
17 |
|
wenzelm@21404
|
18 |
definition
|
wenzelm@21404
|
19 |
sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a stream \<rightarrow> 'a stream" where
|
wenzelm@19763
|
20 |
"sfilter = fix\<cdot>(\<Lambda> h p s. case s of x && xs \<Rightarrow>
|
wenzelm@19763
|
21 |
If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs fi)"
|
wenzelm@19763
|
22 |
|
wenzelm@21404
|
23 |
definition
|
wenzelm@21404
|
24 |
slen :: "'a stream \<Rightarrow> inat" ("#_" [1000] 1000) where
|
wenzelm@19763
|
25 |
"#s = (if stream_finite s then Fin (LEAST n. stream_take n\<cdot>s = s) else \<infinity>)"
|
oheimb@11348
|
26 |
|
oheimb@15188
|
27 |
|
oheimb@15188
|
28 |
(* concatenation *)
|
oheimb@15188
|
29 |
|
wenzelm@19763
|
30 |
definition
|
wenzelm@21404
|
31 |
i_rt :: "nat => 'a stream => 'a stream" where (* chops the first i elements *)
|
wenzelm@19763
|
32 |
"i_rt = (%i s. iterate i$rt$s)"
|
wenzelm@17291
|
33 |
|
wenzelm@21404
|
34 |
definition
|
wenzelm@21404
|
35 |
i_th :: "nat => 'a stream => 'a" where (* the i-th element *)
|
wenzelm@19763
|
36 |
"i_th = (%i s. ft$(i_rt i s))"
|
oheimb@15188
|
37 |
|
wenzelm@21404
|
38 |
definition
|
wenzelm@21404
|
39 |
sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) where
|
wenzelm@19763
|
40 |
"s1 ooo s2 = (case #s1 of
|
wenzelm@19763
|
41 |
Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
|
wenzelm@19763
|
42 |
| \<infinity> \<Rightarrow> s1)"
|
wenzelm@19763
|
43 |
|
wenzelm@27361
|
44 |
primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
|
wenzelm@27361
|
45 |
where
|
oheimb@15188
|
46 |
constr_sconc'_0: "constr_sconc' 0 s1 s2 = s2"
|
wenzelm@27361
|
47 |
| constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 &&
|
oheimb@15188
|
48 |
constr_sconc' n (rt$s1) s2"
|
oheimb@15188
|
49 |
|
wenzelm@19763
|
50 |
definition
|
wenzelm@21404
|
51 |
constr_sconc :: "'a stream => 'a stream => 'a stream" where (* constructive *)
|
wenzelm@19763
|
52 |
"constr_sconc s1 s2 = (case #s1 of
|
wenzelm@19763
|
53 |
Fin n \<Rightarrow> constr_sconc' n s1 s2
|
wenzelm@19763
|
54 |
| \<infinity> \<Rightarrow> s1)"
|
wenzelm@19763
|
55 |
|
oheimb@15188
|
56 |
|
oheimb@15188
|
57 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
58 |
(* theorems about scons *)
|
oheimb@15188
|
59 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
60 |
|
oheimb@15188
|
61 |
|
oheimb@15188
|
62 |
section "scons"
|
oheimb@15188
|
63 |
|
oheimb@15188
|
64 |
lemma scons_eq_UU: "(a && s = UU) = (a = UU)"
|
huffman@30913
|
65 |
by simp
|
oheimb@15188
|
66 |
|
oheimb@15188
|
67 |
lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R"
|
huffman@30913
|
68 |
by simp
|
oheimb@15188
|
69 |
|
oheimb@15188
|
70 |
lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)"
|
oheimb@15188
|
71 |
by (auto,insert stream.exhaust [of x],auto)
|
oheimb@15188
|
72 |
|
wenzelm@18109
|
73 |
lemma stream_neq_UU: "x~=UU ==> EX a a_s. x=a&&a_s & a~=UU"
|
oheimb@15188
|
74 |
by (simp add: stream_exhaust_eq,auto)
|
oheimb@15188
|
75 |
|
oheimb@15188
|
76 |
lemma stream_inject_eq [simp]:
|
oheimb@15188
|
77 |
"[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b & s = t)"
|
oheimb@15188
|
78 |
by (insert stream.injects [of a s b t], auto)
|
oheimb@15188
|
79 |
|
wenzelm@17291
|
80 |
lemma stream_prefix:
|
oheimb@15188
|
81 |
"[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt"
|
huffman@30803
|
82 |
by (insert stream.exhaust [of t], auto)
|
oheimb@15188
|
83 |
|
wenzelm@17291
|
84 |
lemma stream_prefix':
|
wenzelm@17291
|
85 |
"b ~= UU ==> x << b && z =
|
oheimb@15188
|
86 |
(x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))"
|
oheimb@15188
|
87 |
apply (case_tac "x=UU",auto)
|
huffman@30803
|
88 |
by (drule stream_exhaust_eq [THEN iffD1],auto)
|
huffman@19550
|
89 |
|
oheimb@15188
|
90 |
|
oheimb@15188
|
91 |
(*
|
oheimb@15188
|
92 |
lemma stream_prefix1: "[| x<<y; xs<<ys |] ==> x&&xs << y&&ys"
|
oheimb@15188
|
93 |
by (insert stream_prefix' [of y "x&&xs" ys],force)
|
oheimb@15188
|
94 |
*)
|
oheimb@15188
|
95 |
|
wenzelm@17291
|
96 |
lemma stream_flat_prefix:
|
oheimb@15188
|
97 |
"[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
|
oheimb@15188
|
98 |
apply (case_tac "y=UU",auto)
|
huffman@25920
|
99 |
by (drule ax_flat,simp)
|
huffman@19550
|
100 |
|
oheimb@15188
|
101 |
|
oheimb@15188
|
102 |
|
oheimb@15188
|
103 |
|
oheimb@15188
|
104 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
105 |
(* theorems about stream_when *)
|
oheimb@15188
|
106 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
107 |
|
oheimb@15188
|
108 |
section "stream_when"
|
oheimb@15188
|
109 |
|
oheimb@15188
|
110 |
|
oheimb@15188
|
111 |
lemma stream_when_strictf: "stream_when$UU$s=UU"
|
oheimb@15188
|
112 |
by (rule stream.casedist [of s], auto)
|
oheimb@15188
|
113 |
|
oheimb@15188
|
114 |
|
oheimb@15188
|
115 |
|
oheimb@15188
|
116 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
117 |
(* theorems about ft and rt *)
|
oheimb@15188
|
118 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
119 |
|
oheimb@15188
|
120 |
|
oheimb@15188
|
121 |
section "ft & rt"
|
oheimb@15188
|
122 |
|
oheimb@15188
|
123 |
|
oheimb@15188
|
124 |
lemma ft_defin: "s~=UU ==> ft$s~=UU"
|
oheimb@15188
|
125 |
by (drule stream_exhaust_eq [THEN iffD1],auto)
|
oheimb@15188
|
126 |
|
oheimb@15188
|
127 |
lemma rt_strict_rev: "rt$s~=UU ==> s~=UU"
|
oheimb@15188
|
128 |
by auto
|
oheimb@15188
|
129 |
|
oheimb@15188
|
130 |
lemma surjectiv_scons: "(ft$s)&&(rt$s)=s"
|
oheimb@15188
|
131 |
by (rule stream.casedist [of s], auto)
|
oheimb@15188
|
132 |
|
huffman@18075
|
133 |
lemma monofun_rt_mult: "x << s ==> iterate i$rt$x << iterate i$rt$s"
|
huffman@18075
|
134 |
by (rule monofun_cfun_arg)
|
oheimb@15188
|
135 |
|
oheimb@15188
|
136 |
|
oheimb@15188
|
137 |
|
oheimb@15188
|
138 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
139 |
(* theorems about stream_take *)
|
oheimb@15188
|
140 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
141 |
|
oheimb@15188
|
142 |
|
wenzelm@17291
|
143 |
section "stream_take"
|
oheimb@15188
|
144 |
|
oheimb@15188
|
145 |
|
oheimb@15188
|
146 |
lemma stream_reach2: "(LUB i. stream_take i$s) = s"
|
oheimb@15188
|
147 |
apply (insert stream.reach [of s], erule subst) back
|
oheimb@15188
|
148 |
apply (simp add: fix_def2 stream.take_def)
|
huffman@18075
|
149 |
apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym])
|
huffman@35169
|
150 |
by simp
|
oheimb@15188
|
151 |
|
oheimb@15188
|
152 |
lemma chain_stream_take: "chain (%i. stream_take i$s)"
|
wenzelm@17291
|
153 |
apply (rule chainI)
|
oheimb@15188
|
154 |
apply (rule monofun_cfun_fun)
|
oheimb@15188
|
155 |
apply (simp add: stream.take_def del: iterate_Suc)
|
huffman@35169
|
156 |
by (rule chainE, simp)
|
oheimb@15188
|
157 |
|
oheimb@15188
|
158 |
lemma stream_take_prefix [simp]: "stream_take n$s << s"
|
oheimb@15188
|
159 |
apply (insert stream_reach2 [of s])
|
oheimb@15188
|
160 |
apply (erule subst) back
|
oheimb@15188
|
161 |
apply (rule is_ub_thelub)
|
oheimb@15188
|
162 |
by (simp only: chain_stream_take)
|
oheimb@15188
|
163 |
|
wenzelm@17291
|
164 |
lemma stream_take_more [rule_format]:
|
oheimb@15188
|
165 |
"ALL x. stream_take n$x = x --> stream_take (Suc n)$x = x"
|
oheimb@15188
|
166 |
apply (induct_tac n,auto)
|
oheimb@15188
|
167 |
apply (case_tac "x=UU",auto)
|
oheimb@15188
|
168 |
by (drule stream_exhaust_eq [THEN iffD1],auto)
|
oheimb@15188
|
169 |
|
wenzelm@17291
|
170 |
lemma stream_take_lemma3 [rule_format]:
|
oheimb@15188
|
171 |
"ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs"
|
oheimb@15188
|
172 |
apply (induct_tac n,clarsimp)
|
huffman@16745
|
173 |
(*apply (drule sym, erule scons_not_empty, simp)*)
|
oheimb@15188
|
174 |
apply (clarify, rule stream_take_more)
|
oheimb@15188
|
175 |
apply (erule_tac x="x" in allE)
|
oheimb@15188
|
176 |
by (erule_tac x="xs" in allE,simp)
|
oheimb@15188
|
177 |
|
wenzelm@17291
|
178 |
lemma stream_take_lemma4:
|
oheimb@15188
|
179 |
"ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs"
|
oheimb@15188
|
180 |
by auto
|
oheimb@15188
|
181 |
|
wenzelm@17291
|
182 |
lemma stream_take_idempotent [rule_format, simp]:
|
oheimb@15188
|
183 |
"ALL s. stream_take n$(stream_take n$s) = stream_take n$s"
|
oheimb@15188
|
184 |
apply (induct_tac n, auto)
|
oheimb@15188
|
185 |
apply (case_tac "s=UU", auto)
|
oheimb@15188
|
186 |
by (drule stream_exhaust_eq [THEN iffD1], auto)
|
oheimb@15188
|
187 |
|
wenzelm@17291
|
188 |
lemma stream_take_take_Suc [rule_format, simp]:
|
wenzelm@17291
|
189 |
"ALL s. stream_take n$(stream_take (Suc n)$s) =
|
oheimb@15188
|
190 |
stream_take n$s"
|
oheimb@15188
|
191 |
apply (induct_tac n, auto)
|
oheimb@15188
|
192 |
apply (case_tac "s=UU", auto)
|
oheimb@15188
|
193 |
by (drule stream_exhaust_eq [THEN iffD1], auto)
|
oheimb@15188
|
194 |
|
wenzelm@17291
|
195 |
lemma mono_stream_take_pred:
|
oheimb@15188
|
196 |
"stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
|
oheimb@15188
|
197 |
stream_take n$s1 << stream_take n$s2"
|
wenzelm@17291
|
198 |
by (insert monofun_cfun_arg [of "stream_take (Suc n)$s1"
|
oheimb@15188
|
199 |
"stream_take (Suc n)$s2" "stream_take n"], auto)
|
oheimb@15188
|
200 |
(*
|
wenzelm@17291
|
201 |
lemma mono_stream_take_pred:
|
oheimb@15188
|
202 |
"stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
|
oheimb@15188
|
203 |
stream_take n$s1 << stream_take n$s2"
|
oheimb@15188
|
204 |
by (drule mono_stream_take [of _ _ n],simp)
|
oheimb@15188
|
205 |
*)
|
oheimb@15188
|
206 |
|
oheimb@15188
|
207 |
lemma stream_take_lemma10 [rule_format]:
|
wenzelm@17291
|
208 |
"ALL k<=n. stream_take n$s1 << stream_take n$s2
|
oheimb@15188
|
209 |
--> stream_take k$s1 << stream_take k$s2"
|
oheimb@15188
|
210 |
apply (induct_tac n,simp,clarsimp)
|
oheimb@15188
|
211 |
apply (case_tac "k=Suc n",blast)
|
oheimb@15188
|
212 |
apply (erule_tac x="k" in allE)
|
oheimb@15188
|
213 |
by (drule mono_stream_take_pred,simp)
|
oheimb@15188
|
214 |
|
oheimb@15188
|
215 |
lemma stream_take_le_mono : "k<=n ==> stream_take k$s1 << stream_take n$s1"
|
oheimb@15188
|
216 |
apply (insert chain_stream_take [of s1])
|
huffman@25922
|
217 |
by (drule chain_mono,auto)
|
oheimb@15188
|
218 |
|
oheimb@15188
|
219 |
lemma mono_stream_take: "s1 << s2 ==> stream_take n$s1 << stream_take n$s2"
|
oheimb@15188
|
220 |
by (simp add: monofun_cfun_arg)
|
oheimb@15188
|
221 |
|
oheimb@15188
|
222 |
(*
|
oheimb@15188
|
223 |
lemma stream_take_prefix [simp]: "stream_take n$s << s"
|
oheimb@15188
|
224 |
apply (subgoal_tac "s=(LUB n. stream_take n$s)")
|
oheimb@15188
|
225 |
apply (erule ssubst, rule is_ub_thelub)
|
oheimb@15188
|
226 |
apply (simp only: chain_stream_take)
|
oheimb@15188
|
227 |
by (simp only: stream_reach2)
|
oheimb@15188
|
228 |
*)
|
oheimb@15188
|
229 |
|
oheimb@15188
|
230 |
lemma stream_take_take_less:"stream_take k$(stream_take n$s) << stream_take k$s"
|
oheimb@15188
|
231 |
by (rule monofun_cfun_arg,auto)
|
oheimb@15188
|
232 |
|
oheimb@15188
|
233 |
|
oheimb@15188
|
234 |
(* ------------------------------------------------------------------------- *)
|
oheimb@15188
|
235 |
(* special induction rules *)
|
oheimb@15188
|
236 |
(* ------------------------------------------------------------------------- *)
|
oheimb@15188
|
237 |
|
oheimb@15188
|
238 |
|
oheimb@15188
|
239 |
section "induction"
|
oheimb@15188
|
240 |
|
wenzelm@17291
|
241 |
lemma stream_finite_ind:
|
oheimb@15188
|
242 |
"[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x"
|
oheimb@15188
|
243 |
apply (simp add: stream.finite_def,auto)
|
oheimb@15188
|
244 |
apply (erule subst)
|
oheimb@15188
|
245 |
by (drule stream.finite_ind [of P _ x], auto)
|
oheimb@15188
|
246 |
|
wenzelm@17291
|
247 |
lemma stream_finite_ind2:
|
wenzelm@17291
|
248 |
"[| P UU; !! x. x ~= UU ==> P (x && UU); !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )|] ==>
|
oheimb@15188
|
249 |
!s. P (stream_take n$s)"
|
paulson@29792
|
250 |
apply (rule nat_less_induct [of _ n],auto)
|
paulson@29792
|
251 |
apply (case_tac n, auto)
|
paulson@29792
|
252 |
apply (case_tac nat, auto)
|
oheimb@15188
|
253 |
apply (case_tac "s=UU",clarsimp)
|
oheimb@15188
|
254 |
apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
|
oheimb@15188
|
255 |
apply (case_tac "s=UU",clarsimp)
|
oheimb@15188
|
256 |
apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
|
oheimb@15188
|
257 |
apply (case_tac "y=UU",clarsimp)
|
oheimb@15188
|
258 |
by (drule stream_exhaust_eq [THEN iffD1],clarsimp)
|
oheimb@15188
|
259 |
|
wenzelm@17291
|
260 |
lemma stream_ind2:
|
oheimb@15188
|
261 |
"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s) |] ==> P x"
|
oheimb@15188
|
262 |
apply (insert stream.reach [of x],erule subst)
|
oheimb@15188
|
263 |
apply (frule adm_impl_admw, rule wfix_ind, auto)
|
oheimb@15188
|
264 |
apply (rule adm_subst [THEN adm_impl_admw],auto)
|
oheimb@15188
|
265 |
apply (insert stream_finite_ind2 [of P])
|
oheimb@15188
|
266 |
by (simp add: stream.take_def)
|
oheimb@15188
|
267 |
|
oheimb@15188
|
268 |
|
oheimb@15188
|
269 |
|
oheimb@15188
|
270 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
271 |
(* simplify use of coinduction *)
|
oheimb@15188
|
272 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
273 |
|
oheimb@15188
|
274 |
|
oheimb@15188
|
275 |
section "coinduction"
|
oheimb@15188
|
276 |
|
oheimb@15188
|
277 |
lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R"
|
huffman@30803
|
278 |
apply (simp add: stream.bisim_def,clarsimp)
|
huffman@30803
|
279 |
apply (case_tac "x=UU",clarsimp)
|
huffman@30803
|
280 |
apply (erule_tac x="UU" in allE,simp)
|
huffman@30803
|
281 |
apply (case_tac "x'=UU",simp)
|
huffman@30803
|
282 |
apply (drule stream_exhaust_eq [THEN iffD1],auto)+
|
huffman@30803
|
283 |
apply (case_tac "x'=UU",auto)
|
huffman@30803
|
284 |
apply (erule_tac x="a && y" in allE)
|
huffman@30803
|
285 |
apply (erule_tac x="UU" in allE)+
|
huffman@30803
|
286 |
apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
|
huffman@30803
|
287 |
apply (erule_tac x="a && y" in allE)
|
huffman@30803
|
288 |
apply (erule_tac x="aa && ya" in allE) back
|
oheimb@15188
|
289 |
by auto
|
oheimb@15188
|
290 |
|
oheimb@15188
|
291 |
|
oheimb@15188
|
292 |
|
oheimb@15188
|
293 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
294 |
(* theorems about stream_finite *)
|
oheimb@15188
|
295 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
296 |
|
oheimb@15188
|
297 |
|
oheimb@15188
|
298 |
section "stream_finite"
|
oheimb@15188
|
299 |
|
oheimb@15188
|
300 |
lemma stream_finite_UU [simp]: "stream_finite UU"
|
oheimb@15188
|
301 |
by (simp add: stream.finite_def)
|
oheimb@15188
|
302 |
|
oheimb@15188
|
303 |
lemma stream_finite_UU_rev: "~ stream_finite s ==> s ~= UU"
|
oheimb@15188
|
304 |
by (auto simp add: stream.finite_def)
|
oheimb@15188
|
305 |
|
oheimb@15188
|
306 |
lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)"
|
oheimb@15188
|
307 |
apply (simp add: stream.finite_def,auto)
|
oheimb@15188
|
308 |
apply (rule_tac x="Suc n" in exI)
|
oheimb@15188
|
309 |
by (simp add: stream_take_lemma4)
|
oheimb@15188
|
310 |
|
oheimb@15188
|
311 |
lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"
|
oheimb@15188
|
312 |
apply (simp add: stream.finite_def, auto)
|
oheimb@15188
|
313 |
apply (rule_tac x="n" in exI)
|
oheimb@15188
|
314 |
by (erule stream_take_lemma3,simp)
|
oheimb@15188
|
315 |
|
oheimb@15188
|
316 |
lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s"
|
oheimb@15188
|
317 |
apply (rule stream.casedist [of s], auto)
|
oheimb@15188
|
318 |
apply (rule stream_finite_lemma1, simp)
|
oheimb@15188
|
319 |
by (rule stream_finite_lemma2,simp)
|
oheimb@15188
|
320 |
|
oheimb@15188
|
321 |
lemma stream_finite_less: "stream_finite s ==> !t. t<<s --> stream_finite t"
|
huffman@19440
|
322 |
apply (erule stream_finite_ind [of s], auto)
|
oheimb@15188
|
323 |
apply (case_tac "t=UU", auto)
|
oheimb@15188
|
324 |
apply (drule stream_exhaust_eq [THEN iffD1],auto)
|
oheimb@15188
|
325 |
apply (erule_tac x="y" in allE, simp)
|
oheimb@15188
|
326 |
by (rule stream_finite_lemma1, simp)
|
oheimb@15188
|
327 |
|
oheimb@15188
|
328 |
lemma stream_take_finite [simp]: "stream_finite (stream_take n$s)"
|
oheimb@15188
|
329 |
apply (simp add: stream.finite_def)
|
oheimb@15188
|
330 |
by (rule_tac x="n" in exI,simp)
|
oheimb@15188
|
331 |
|
oheimb@15188
|
332 |
lemma adm_not_stream_finite: "adm (%x. ~ stream_finite x)"
|
huffman@25833
|
333 |
apply (rule adm_upward)
|
huffman@25833
|
334 |
apply (erule contrapos_nn)
|
huffman@25833
|
335 |
apply (erule (1) stream_finite_less [rule_format])
|
huffman@25833
|
336 |
done
|
oheimb@15188
|
337 |
|
oheimb@15188
|
338 |
|
oheimb@15188
|
339 |
|
oheimb@15188
|
340 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
341 |
(* theorems about stream length *)
|
oheimb@15188
|
342 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
343 |
|
oheimb@15188
|
344 |
|
oheimb@15188
|
345 |
section "slen"
|
oheimb@15188
|
346 |
|
oheimb@15188
|
347 |
lemma slen_empty [simp]: "#\<bottom> = 0"
|
haftmann@27111
|
348 |
by (simp add: slen_def stream.finite_def zero_inat_def Least_equality)
|
oheimb@15188
|
349 |
|
oheimb@15188
|
350 |
lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = iSuc (#xs)"
|
oheimb@15188
|
351 |
apply (case_tac "stream_finite (x && xs)")
|
oheimb@15188
|
352 |
apply (simp add: slen_def, auto)
|
haftmann@27111
|
353 |
apply (simp add: stream.finite_def, auto simp add: iSuc_Fin)
|
haftmann@27111
|
354 |
apply (rule Least_Suc2, auto)
|
huffman@16745
|
355 |
(*apply (drule sym)*)
|
huffman@16745
|
356 |
(*apply (drule sym scons_eq_UU [THEN iffD1],simp)*)
|
oheimb@15188
|
357 |
apply (erule stream_finite_lemma2, simp)
|
oheimb@15188
|
358 |
apply (simp add: slen_def, auto)
|
oheimb@15188
|
359 |
by (drule stream_finite_lemma1,auto)
|
oheimb@15188
|
360 |
|
oheimb@15188
|
361 |
lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \<bottom>)"
|
wenzelm@17291
|
362 |
by (rule stream.casedist [of x], auto simp del: iSuc_Fin
|
oheimb@15188
|
363 |
simp add: Fin_0 iSuc_Fin[THEN sym] i0_iless_iSuc iSuc_mono)
|
oheimb@15188
|
364 |
|
oheimb@15188
|
365 |
lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
|
oheimb@15188
|
366 |
by (rule stream.casedist [of x], auto)
|
oheimb@15188
|
367 |
|
oheimb@15188
|
368 |
lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y & a ~= \<bottom> & Fin n < #y)"
|
oheimb@15188
|
369 |
apply (auto, case_tac "x=UU",auto)
|
oheimb@15188
|
370 |
apply (drule stream_exhaust_eq [THEN iffD1], auto)
|
haftmann@27111
|
371 |
apply (case_tac "#y") apply simp_all
|
haftmann@27111
|
372 |
apply (case_tac "#y") apply simp_all
|
haftmann@27111
|
373 |
done
|
oheimb@15188
|
374 |
|
oheimb@15188
|
375 |
lemma slen_iSuc: "#x = iSuc n --> (? a y. x = a&&y & a ~= \<bottom> & #y = n)"
|
oheimb@15188
|
376 |
by (rule stream.casedist [of x], auto)
|
oheimb@15188
|
377 |
|
oheimb@15188
|
378 |
lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>"
|
oheimb@15188
|
379 |
by (simp add: slen_def)
|
oheimb@15188
|
380 |
|
oheimb@15188
|
381 |
lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < Fin (Suc n))"
|
huffman@30803
|
382 |
apply (rule stream.casedist [of x], auto)
|
huffman@30803
|
383 |
apply (simp add: zero_inat_def)
|
huffman@30803
|
384 |
apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
|
huffman@30803
|
385 |
apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
|
haftmann@27111
|
386 |
done
|
oheimb@15188
|
387 |
|
wenzelm@17291
|
388 |
lemma slen_take_lemma4 [rule_format]:
|
oheimb@15188
|
389 |
"!s. stream_take n$s ~= s --> #(stream_take n$s) = Fin n"
|
haftmann@27111
|
390 |
apply (induct n, auto simp add: Fin_0)
|
haftmann@27111
|
391 |
apply (case_tac "s=UU", simp)
|
haftmann@27111
|
392 |
by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_Fin)
|
oheimb@15188
|
393 |
|
oheimb@15188
|
394 |
(*
|
wenzelm@17291
|
395 |
lemma stream_take_idempotent [simp]:
|
oheimb@15188
|
396 |
"stream_take n$(stream_take n$s) = stream_take n$s"
|
oheimb@15188
|
397 |
apply (case_tac "stream_take n$s = s")
|
oheimb@15188
|
398 |
apply (auto,insert slen_take_lemma4 [of n s]);
|
oheimb@15188
|
399 |
by (auto,insert slen_take_lemma1 [of "stream_take n$s" n],simp)
|
oheimb@15188
|
400 |
|
wenzelm@17291
|
401 |
lemma stream_take_take_Suc [simp]: "stream_take n$(stream_take (Suc n)$s) =
|
oheimb@15188
|
402 |
stream_take n$s"
|
oheimb@15188
|
403 |
apply (simp add: po_eq_conv,auto)
|
oheimb@15188
|
404 |
apply (simp add: stream_take_take_less)
|
oheimb@15188
|
405 |
apply (subgoal_tac "stream_take n$s = stream_take n$(stream_take n$s)")
|
oheimb@15188
|
406 |
apply (erule ssubst)
|
oheimb@15188
|
407 |
apply (rule_tac monofun_cfun_arg)
|
oheimb@15188
|
408 |
apply (insert chain_stream_take [of s])
|
oheimb@15188
|
409 |
by (simp add: chain_def,simp)
|
oheimb@15188
|
410 |
*)
|
oheimb@15188
|
411 |
|
oheimb@15188
|
412 |
lemma slen_take_eq: "ALL x. (Fin n < #x) = (stream_take n\<cdot>x ~= x)"
|
oheimb@15188
|
413 |
apply (induct_tac n, auto)
|
oheimb@15188
|
414 |
apply (simp add: Fin_0, clarsimp)
|
oheimb@15188
|
415 |
apply (drule not_sym)
|
oheimb@15188
|
416 |
apply (drule slen_empty_eq [THEN iffD1], simp)
|
oheimb@15188
|
417 |
apply (case_tac "x=UU", simp)
|
oheimb@15188
|
418 |
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
|
oheimb@15188
|
419 |
apply (erule_tac x="y" in allE, auto)
|
haftmann@27111
|
420 |
apply (simp_all add: not_less iSuc_Fin)
|
haftmann@27111
|
421 |
apply (case_tac "#y") apply simp_all
|
oheimb@15188
|
422 |
apply (case_tac "x=UU", simp)
|
oheimb@15188
|
423 |
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
|
oheimb@15188
|
424 |
apply (erule_tac x="y" in allE, simp)
|
haftmann@27111
|
425 |
apply (case_tac "#y") by simp_all
|
oheimb@15188
|
426 |
|
oheimb@15188
|
427 |
lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\<cdot>x = x)"
|
huffman@26102
|
428 |
by (simp add: linorder_not_less [symmetric] slen_take_eq)
|
oheimb@15188
|
429 |
|
oheimb@15188
|
430 |
lemma slen_take_lemma1: "#x = Fin n ==> stream_take n\<cdot>x = x"
|
oheimb@15188
|
431 |
by (rule slen_take_eq_rev [THEN iffD1], auto)
|
oheimb@15188
|
432 |
|
oheimb@15188
|
433 |
lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)"
|
oheimb@15188
|
434 |
apply (rule stream.casedist [of s1])
|
oheimb@15188
|
435 |
by (rule stream.casedist [of s2],simp+)+
|
oheimb@15188
|
436 |
|
wenzelm@17291
|
437 |
lemma slen_take_lemma5: "#(stream_take n$s) <= Fin n"
|
oheimb@15188
|
438 |
apply (case_tac "stream_take n$s = s")
|
oheimb@15188
|
439 |
apply (simp add: slen_take_eq_rev)
|
oheimb@15188
|
440 |
by (simp add: slen_take_lemma4)
|
oheimb@15188
|
441 |
|
oheimb@15188
|
442 |
lemma slen_take_lemma2: "!x. ~stream_finite x --> #(stream_take i\<cdot>x) = Fin i"
|
oheimb@15188
|
443 |
apply (simp add: stream.finite_def, auto)
|
oheimb@15188
|
444 |
by (simp add: slen_take_lemma4)
|
oheimb@15188
|
445 |
|
oheimb@15188
|
446 |
lemma slen_infinite: "stream_finite x = (#x ~= Infty)"
|
oheimb@15188
|
447 |
by (simp add: slen_def)
|
oheimb@15188
|
448 |
|
oheimb@15188
|
449 |
lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t"
|
oheimb@15188
|
450 |
apply (erule stream_finite_ind [of s], auto)
|
oheimb@15188
|
451 |
apply (case_tac "t=UU", auto)
|
oheimb@15188
|
452 |
apply (drule stream_exhaust_eq [THEN iffD1], auto)
|
huffman@30803
|
453 |
done
|
oheimb@15188
|
454 |
|
oheimb@15188
|
455 |
lemma slen_mono: "s << t ==> #s <= #t"
|
oheimb@15188
|
456 |
apply (case_tac "stream_finite t")
|
wenzelm@17291
|
457 |
apply (frule stream_finite_less)
|
oheimb@15188
|
458 |
apply (erule_tac x="s" in allE, simp)
|
oheimb@15188
|
459 |
apply (drule slen_mono_lemma, auto)
|
oheimb@15188
|
460 |
by (simp add: slen_def)
|
oheimb@15188
|
461 |
|
huffman@18075
|
462 |
lemma iterate_lemma: "F$(iterate n$F$x) = iterate n$F$(F$x)"
|
oheimb@15188
|
463 |
by (insert iterate_Suc2 [of n F x], auto)
|
oheimb@15188
|
464 |
|
huffman@18075
|
465 |
lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i$rt$x)"
|
haftmann@27111
|
466 |
apply (induct i, auto)
|
haftmann@27111
|
467 |
apply (case_tac "x=UU", auto simp add: zero_inat_def)
|
oheimb@15188
|
468 |
apply (drule stream_exhaust_eq [THEN iffD1], auto)
|
oheimb@15188
|
469 |
apply (erule_tac x="y" in allE, auto)
|
haftmann@27111
|
470 |
apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_Fin)
|
oheimb@15188
|
471 |
by (simp add: iterate_lemma)
|
oheimb@15188
|
472 |
|
wenzelm@17291
|
473 |
lemma slen_take_lemma3 [rule_format]:
|
oheimb@15188
|
474 |
"!(x::'a::flat stream) y. Fin n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y"
|
oheimb@15188
|
475 |
apply (induct_tac n, auto)
|
oheimb@15188
|
476 |
apply (case_tac "x=UU", auto)
|
haftmann@27111
|
477 |
apply (simp add: zero_inat_def)
|
oheimb@15188
|
478 |
apply (simp add: Suc_ile_eq)
|
oheimb@15188
|
479 |
apply (case_tac "y=UU", clarsimp)
|
oheimb@15188
|
480 |
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
|
oheimb@15188
|
481 |
apply (erule_tac x="ya" in allE, simp)
|
huffman@25920
|
482 |
by (drule ax_flat, simp)
|
oheimb@15188
|
483 |
|
wenzelm@17291
|
484 |
lemma slen_strict_mono_lemma:
|
oheimb@15188
|
485 |
"stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t"
|
oheimb@15188
|
486 |
apply (erule stream_finite_ind, auto)
|
oheimb@15188
|
487 |
apply (case_tac "sa=UU", auto)
|
oheimb@15188
|
488 |
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
|
huffman@25920
|
489 |
by (drule ax_flat, simp)
|
oheimb@15188
|
490 |
|
oheimb@15188
|
491 |
lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"
|
haftmann@27111
|
492 |
by (auto simp add: slen_mono less_le dest: slen_strict_mono_lemma)
|
oheimb@15188
|
493 |
|
wenzelm@17291
|
494 |
lemma stream_take_Suc_neq: "stream_take (Suc n)$s ~=s ==>
|
oheimb@15188
|
495 |
stream_take n$s ~= stream_take (Suc n)$s"
|
oheimb@15188
|
496 |
apply auto
|
oheimb@15188
|
497 |
apply (subgoal_tac "stream_take n$s ~=s")
|
oheimb@15188
|
498 |
apply (insert slen_take_lemma4 [of n s],auto)
|
oheimb@15188
|
499 |
apply (rule stream.casedist [of s],simp)
|
haftmann@27111
|
500 |
by (simp add: slen_take_lemma4 iSuc_Fin)
|
oheimb@15188
|
501 |
|
oheimb@15188
|
502 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
503 |
(* theorems about smap *)
|
oheimb@15188
|
504 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
505 |
|
oheimb@15188
|
506 |
|
oheimb@15188
|
507 |
section "smap"
|
oheimb@15188
|
508 |
|
oheimb@15188
|
509 |
lemma smap_unfold: "smap = (\<Lambda> f t. case t of x&&xs \<Rightarrow> f$x && smap$f$xs)"
|
huffman@29530
|
510 |
by (insert smap_def [where 'a='a and 'b='b, THEN eq_reflection, THEN fix_eq2], auto)
|
oheimb@15188
|
511 |
|
oheimb@15188
|
512 |
lemma smap_empty [simp]: "smap\<cdot>f\<cdot>\<bottom> = \<bottom>"
|
oheimb@15188
|
513 |
by (subst smap_unfold, simp)
|
oheimb@15188
|
514 |
|
oheimb@15188
|
515 |
lemma smap_scons [simp]: "x~=\<bottom> ==> smap\<cdot>f\<cdot>(x&&xs) = (f\<cdot>x)&&(smap\<cdot>f\<cdot>xs)"
|
oheimb@15188
|
516 |
by (subst smap_unfold, force)
|
oheimb@15188
|
517 |
|
oheimb@15188
|
518 |
|
oheimb@15188
|
519 |
|
oheimb@15188
|
520 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
521 |
(* theorems about sfilter *)
|
oheimb@15188
|
522 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
523 |
|
oheimb@15188
|
524 |
section "sfilter"
|
oheimb@15188
|
525 |
|
wenzelm@17291
|
526 |
lemma sfilter_unfold:
|
oheimb@15188
|
527 |
"sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
|
oheimb@15188
|
528 |
If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs fi)"
|
huffman@29530
|
529 |
by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
|
oheimb@15188
|
530 |
|
oheimb@15188
|
531 |
lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
|
oheimb@15188
|
532 |
apply (rule ext_cfun)
|
oheimb@15188
|
533 |
apply (subst sfilter_unfold, auto)
|
oheimb@15188
|
534 |
apply (case_tac "x=UU", auto)
|
oheimb@15188
|
535 |
by (drule stream_exhaust_eq [THEN iffD1], auto)
|
oheimb@15188
|
536 |
|
oheimb@15188
|
537 |
lemma sfilter_empty [simp]: "sfilter\<cdot>f\<cdot>\<bottom> = \<bottom>"
|
oheimb@15188
|
538 |
by (subst sfilter_unfold, force)
|
oheimb@15188
|
539 |
|
wenzelm@17291
|
540 |
lemma sfilter_scons [simp]:
|
wenzelm@17291
|
541 |
"x ~= \<bottom> ==> sfilter\<cdot>f\<cdot>(x && xs) =
|
wenzelm@17291
|
542 |
If f\<cdot>x then x && sfilter\<cdot>f\<cdot>xs else sfilter\<cdot>f\<cdot>xs fi"
|
oheimb@15188
|
543 |
by (subst sfilter_unfold, force)
|
oheimb@15188
|
544 |
|
oheimb@15188
|
545 |
|
oheimb@15188
|
546 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
547 |
section "i_rt"
|
oheimb@15188
|
548 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
549 |
|
oheimb@15188
|
550 |
lemma i_rt_UU [simp]: "i_rt n UU = UU"
|
haftmann@34928
|
551 |
by (induct n) (simp_all add: i_rt_def)
|
oheimb@15188
|
552 |
|
oheimb@15188
|
553 |
lemma i_rt_0 [simp]: "i_rt 0 s = s"
|
oheimb@15188
|
554 |
by (simp add: i_rt_def)
|
oheimb@15188
|
555 |
|
oheimb@15188
|
556 |
lemma i_rt_Suc [simp]: "a ~= UU ==> i_rt (Suc n) (a&&s) = i_rt n s"
|
oheimb@15188
|
557 |
by (simp add: i_rt_def iterate_Suc2 del: iterate_Suc)
|
oheimb@15188
|
558 |
|
oheimb@15188
|
559 |
lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt$s)"
|
oheimb@15188
|
560 |
by (simp only: i_rt_def iterate_Suc2)
|
oheimb@15188
|
561 |
|
oheimb@15188
|
562 |
lemma i_rt_Suc_back:"i_rt (Suc n) s = rt$(i_rt n s)"
|
oheimb@15188
|
563 |
by (simp only: i_rt_def,auto)
|
oheimb@15188
|
564 |
|
oheimb@15188
|
565 |
lemma i_rt_mono: "x << s ==> i_rt n x << i_rt n s"
|
oheimb@15188
|
566 |
by (simp add: i_rt_def monofun_rt_mult)
|
oheimb@15188
|
567 |
|
oheimb@15188
|
568 |
lemma i_rt_ij_lemma: "Fin (i + j) <= #x ==> Fin j <= #(i_rt i x)"
|
oheimb@15188
|
569 |
by (simp add: i_rt_def slen_rt_mult)
|
oheimb@15188
|
570 |
|
oheimb@15188
|
571 |
lemma slen_i_rt_mono: "#s2 <= #s1 ==> #(i_rt n s2) <= #(i_rt n s1)"
|
oheimb@15188
|
572 |
apply (induct_tac n,auto)
|
oheimb@15188
|
573 |
apply (simp add: i_rt_Suc_back)
|
oheimb@15188
|
574 |
by (drule slen_rt_mono,simp)
|
oheimb@15188
|
575 |
|
oheimb@15188
|
576 |
lemma i_rt_take_lemma1 [rule_format]: "ALL s. i_rt n (stream_take n$s) = UU"
|
wenzelm@17291
|
577 |
apply (induct_tac n)
|
oheimb@15188
|
578 |
apply (simp add: i_rt_Suc_back,auto)
|
oheimb@15188
|
579 |
apply (case_tac "s=UU",auto)
|
oheimb@15188
|
580 |
by (drule stream_exhaust_eq [THEN iffD1],auto)
|
oheimb@15188
|
581 |
|
oheimb@15188
|
582 |
lemma i_rt_slen: "(i_rt n s = UU) = (stream_take n$s = s)"
|
oheimb@15188
|
583 |
apply auto
|
wenzelm@17291
|
584 |
apply (insert i_rt_ij_lemma [of n "Suc 0" s])
|
oheimb@15188
|
585 |
apply (subgoal_tac "#(i_rt n s)=0")
|
oheimb@15188
|
586 |
apply (case_tac "stream_take n$s = s",simp+)
|
oheimb@15188
|
587 |
apply (insert slen_take_eq [rule_format,of n s],simp)
|
haftmann@27111
|
588 |
apply (cases "#s") apply (simp_all add: zero_inat_def)
|
haftmann@27111
|
589 |
apply (simp add: slen_take_eq)
|
haftmann@27111
|
590 |
apply (cases "#s")
|
haftmann@27111
|
591 |
using i_rt_take_lemma1 [of n s]
|
haftmann@27111
|
592 |
apply (simp_all add: zero_inat_def)
|
haftmann@27111
|
593 |
done
|
oheimb@15188
|
594 |
|
oheimb@15188
|
595 |
lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU"
|
oheimb@15188
|
596 |
by (simp add: i_rt_slen slen_take_lemma1)
|
oheimb@15188
|
597 |
|
oheimb@15188
|
598 |
lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s"
|
oheimb@15188
|
599 |
apply (induct_tac n, auto)
|
oheimb@15188
|
600 |
apply (rule stream.casedist [of "s"], auto simp del: i_rt_Suc)
|
oheimb@15188
|
601 |
by (simp add: i_rt_Suc_back stream_finite_rt_eq)+
|
oheimb@15188
|
602 |
|
oheimb@15188
|
603 |
lemma take_i_rt_len_lemma: "ALL sl x j t. Fin sl = #x & n <= sl &
|
wenzelm@17291
|
604 |
#(stream_take n$x) = Fin t & #(i_rt n x)= Fin j
|
oheimb@15188
|
605 |
--> Fin (j + t) = #x"
|
haftmann@27111
|
606 |
apply (induct n, auto)
|
haftmann@27111
|
607 |
apply (simp add: zero_inat_def)
|
oheimb@15188
|
608 |
apply (case_tac "x=UU",auto)
|
haftmann@27111
|
609 |
apply (simp add: zero_inat_def)
|
oheimb@15188
|
610 |
apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
|
oheimb@15188
|
611 |
apply (subgoal_tac "EX k. Fin k = #y",clarify)
|
oheimb@15188
|
612 |
apply (erule_tac x="k" in allE)
|
oheimb@15188
|
613 |
apply (erule_tac x="y" in allE,auto)
|
oheimb@15188
|
614 |
apply (erule_tac x="THE p. Suc p = t" in allE,auto)
|
haftmann@27111
|
615 |
apply (simp add: iSuc_def split: inat.splits)
|
haftmann@27111
|
616 |
apply (simp add: iSuc_def split: inat.splits)
|
oheimb@15188
|
617 |
apply (simp only: the_equality)
|
haftmann@27111
|
618 |
apply (simp add: iSuc_def split: inat.splits)
|
oheimb@15188
|
619 |
apply force
|
haftmann@27111
|
620 |
apply (simp add: iSuc_def split: inat.splits)
|
haftmann@27111
|
621 |
done
|
oheimb@15188
|
622 |
|
wenzelm@17291
|
623 |
lemma take_i_rt_len:
|
oheimb@15188
|
624 |
"[| Fin sl = #x; n <= sl; #(stream_take n$x) = Fin t; #(i_rt n x) = Fin j |] ==>
|
oheimb@15188
|
625 |
Fin (j + t) = #x"
|
oheimb@15188
|
626 |
by (blast intro: take_i_rt_len_lemma [rule_format])
|
oheimb@15188
|
627 |
|
oheimb@15188
|
628 |
|
oheimb@15188
|
629 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
630 |
section "i_th"
|
oheimb@15188
|
631 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
632 |
|
oheimb@15188
|
633 |
lemma i_th_i_rt_step:
|
wenzelm@17291
|
634 |
"[| i_th n s1 << i_th n s2; i_rt (Suc n) s1 << i_rt (Suc n) s2 |] ==>
|
oheimb@15188
|
635 |
i_rt n s1 << i_rt n s2"
|
oheimb@15188
|
636 |
apply (simp add: i_th_def i_rt_Suc_back)
|
oheimb@15188
|
637 |
apply (rule stream.casedist [of "i_rt n s1"],simp)
|
oheimb@15188
|
638 |
apply (rule stream.casedist [of "i_rt n s2"],auto)
|
huffman@30803
|
639 |
done
|
oheimb@15188
|
640 |
|
wenzelm@17291
|
641 |
lemma i_th_stream_take_Suc [rule_format]:
|
oheimb@15188
|
642 |
"ALL s. i_th n (stream_take (Suc n)$s) = i_th n s"
|
oheimb@15188
|
643 |
apply (induct_tac n,auto)
|
oheimb@15188
|
644 |
apply (simp add: i_th_def)
|
oheimb@15188
|
645 |
apply (case_tac "s=UU",auto)
|
oheimb@15188
|
646 |
apply (drule stream_exhaust_eq [THEN iffD1],auto)
|
oheimb@15188
|
647 |
apply (case_tac "s=UU",simp add: i_th_def)
|
oheimb@15188
|
648 |
apply (drule stream_exhaust_eq [THEN iffD1],auto)
|
oheimb@15188
|
649 |
by (simp add: i_th_def i_rt_Suc_forw)
|
oheimb@15188
|
650 |
|
oheimb@15188
|
651 |
lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)$s)"
|
oheimb@15188
|
652 |
apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)$s)"])
|
oheimb@15188
|
653 |
apply (rule i_th_stream_take_Suc [THEN subst])
|
oheimb@15188
|
654 |
apply (simp add: i_th_def i_rt_Suc_back [symmetric])
|
oheimb@15188
|
655 |
by (simp add: i_rt_take_lemma1)
|
oheimb@15188
|
656 |
|
wenzelm@17291
|
657 |
lemma i_th_last_eq:
|
oheimb@15188
|
658 |
"i_th n s1 = i_th n s2 ==> i_rt n (stream_take (Suc n)$s1) = i_rt n (stream_take (Suc n)$s2)"
|
oheimb@15188
|
659 |
apply (insert i_th_last [of n s1])
|
oheimb@15188
|
660 |
apply (insert i_th_last [of n s2])
|
oheimb@15188
|
661 |
by auto
|
oheimb@15188
|
662 |
|
oheimb@15188
|
663 |
lemma i_th_prefix_lemma:
|
wenzelm@17291
|
664 |
"[| k <= n; stream_take (Suc n)$s1 << stream_take (Suc n)$s2 |] ==>
|
oheimb@15188
|
665 |
i_th k s1 << i_th k s2"
|
oheimb@15188
|
666 |
apply (insert i_th_stream_take_Suc [of k s1, THEN sym])
|
oheimb@15188
|
667 |
apply (insert i_th_stream_take_Suc [of k s2, THEN sym],auto)
|
oheimb@15188
|
668 |
apply (simp add: i_th_def)
|
oheimb@15188
|
669 |
apply (rule monofun_cfun, auto)
|
oheimb@15188
|
670 |
apply (rule i_rt_mono)
|
oheimb@15188
|
671 |
by (blast intro: stream_take_lemma10)
|
oheimb@15188
|
672 |
|
wenzelm@17291
|
673 |
lemma take_i_rt_prefix_lemma1:
|
oheimb@15188
|
674 |
"stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
|
wenzelm@17291
|
675 |
i_rt (Suc n) s1 << i_rt (Suc n) s2 ==>
|
oheimb@15188
|
676 |
i_rt n s1 << i_rt n s2 & stream_take n$s1 << stream_take n$s2"
|
oheimb@15188
|
677 |
apply auto
|
oheimb@15188
|
678 |
apply (insert i_th_prefix_lemma [of n n s1 s2])
|
oheimb@15188
|
679 |
apply (rule i_th_i_rt_step,auto)
|
oheimb@15188
|
680 |
by (drule mono_stream_take_pred,simp)
|
oheimb@15188
|
681 |
|
wenzelm@17291
|
682 |
lemma take_i_rt_prefix_lemma:
|
oheimb@15188
|
683 |
"[| stream_take n$s1 << stream_take n$s2; i_rt n s1 << i_rt n s2 |] ==> s1 << s2"
|
oheimb@15188
|
684 |
apply (case_tac "n=0",simp)
|
nipkow@25161
|
685 |
apply (auto)
|
wenzelm@17291
|
686 |
apply (subgoal_tac "stream_take 0$s1 << stream_take 0$s2 &
|
oheimb@15188
|
687 |
i_rt 0 s1 << i_rt 0 s2")
|
oheimb@15188
|
688 |
defer 1
|
oheimb@15188
|
689 |
apply (rule zero_induct,blast)
|
oheimb@15188
|
690 |
apply (blast dest: take_i_rt_prefix_lemma1)
|
oheimb@15188
|
691 |
by simp
|
oheimb@15188
|
692 |
|
wenzelm@17291
|
693 |
lemma streams_prefix_lemma: "(s1 << s2) =
|
wenzelm@17291
|
694 |
(stream_take n$s1 << stream_take n$s2 & i_rt n s1 << i_rt n s2)"
|
oheimb@15188
|
695 |
apply auto
|
oheimb@15188
|
696 |
apply (simp add: monofun_cfun_arg)
|
oheimb@15188
|
697 |
apply (simp add: i_rt_mono)
|
oheimb@15188
|
698 |
by (erule take_i_rt_prefix_lemma,simp)
|
oheimb@15188
|
699 |
|
oheimb@15188
|
700 |
lemma streams_prefix_lemma1:
|
oheimb@15188
|
701 |
"[| stream_take n$s1 = stream_take n$s2; i_rt n s1 = i_rt n s2 |] ==> s1 = s2"
|
oheimb@15188
|
702 |
apply (simp add: po_eq_conv,auto)
|
oheimb@15188
|
703 |
apply (insert streams_prefix_lemma)
|
oheimb@15188
|
704 |
by blast+
|
oheimb@15188
|
705 |
|
oheimb@15188
|
706 |
|
oheimb@15188
|
707 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
708 |
section "sconc"
|
oheimb@15188
|
709 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
710 |
|
oheimb@15188
|
711 |
lemma UU_sconc [simp]: " UU ooo s = s "
|
haftmann@27111
|
712 |
by (simp add: sconc_def zero_inat_def)
|
oheimb@15188
|
713 |
|
oheimb@15188
|
714 |
lemma scons_neq_UU: "a~=UU ==> a && s ~=UU"
|
oheimb@15188
|
715 |
by auto
|
oheimb@15188
|
716 |
|
oheimb@15188
|
717 |
lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y"
|
haftmann@27111
|
718 |
apply (simp add: sconc_def zero_inat_def iSuc_def split: inat.splits, auto)
|
oheimb@15188
|
719 |
apply (rule someI2_ex,auto)
|
oheimb@15188
|
720 |
apply (rule_tac x="x && y" in exI,auto)
|
oheimb@15188
|
721 |
apply (simp add: i_rt_Suc_forw)
|
oheimb@15188
|
722 |
apply (case_tac "xa=UU",simp)
|
oheimb@15188
|
723 |
by (drule stream_exhaust_eq [THEN iffD1],auto)
|
oheimb@15188
|
724 |
|
wenzelm@17291
|
725 |
lemma ex_sconc [rule_format]:
|
oheimb@15188
|
726 |
"ALL k y. #x = Fin k --> (EX w. stream_take k$w = x & i_rt k w = y)"
|
oheimb@15188
|
727 |
apply (case_tac "#x")
|
oheimb@15188
|
728 |
apply (rule stream_finite_ind [of x],auto)
|
oheimb@15188
|
729 |
apply (simp add: stream.finite_def)
|
oheimb@15188
|
730 |
apply (drule slen_take_lemma1,blast)
|
haftmann@27111
|
731 |
apply (simp_all add: zero_inat_def iSuc_def split: inat.splits)
|
oheimb@15188
|
732 |
apply (erule_tac x="y" in allE,auto)
|
oheimb@15188
|
733 |
by (rule_tac x="a && w" in exI,auto)
|
oheimb@15188
|
734 |
|
wenzelm@17291
|
735 |
lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y"
|
haftmann@27111
|
736 |
apply (simp add: sconc_def split: inat.splits, arith?,auto)
|
oheimb@15188
|
737 |
apply (rule someI2_ex,auto)
|
oheimb@15188
|
738 |
by (drule ex_sconc,simp)
|
oheimb@15188
|
739 |
|
oheimb@15188
|
740 |
lemma sconc_inj2: "\<lbrakk>Fin n = #x; x ooo y = x ooo z\<rbrakk> \<Longrightarrow> y = z"
|
oheimb@15188
|
741 |
apply (frule_tac y=y in rt_sconc1)
|
oheimb@15188
|
742 |
by (auto elim: rt_sconc1)
|
oheimb@15188
|
743 |
|
oheimb@15188
|
744 |
lemma sconc_UU [simp]:"s ooo UU = s"
|
oheimb@15188
|
745 |
apply (case_tac "#s")
|
haftmann@27111
|
746 |
apply (simp add: sconc_def)
|
oheimb@15188
|
747 |
apply (rule someI2_ex)
|
oheimb@15188
|
748 |
apply (rule_tac x="s" in exI)
|
oheimb@15188
|
749 |
apply auto
|
oheimb@15188
|
750 |
apply (drule slen_take_lemma1,auto)
|
oheimb@15188
|
751 |
apply (simp add: i_rt_lemma_slen)
|
oheimb@15188
|
752 |
apply (drule slen_take_lemma1,auto)
|
oheimb@15188
|
753 |
apply (simp add: i_rt_slen)
|
haftmann@27111
|
754 |
by (simp add: sconc_def)
|
oheimb@15188
|
755 |
|
oheimb@15188
|
756 |
lemma stream_take_sconc [simp]: "Fin n = #x ==> stream_take n$(x ooo y) = x"
|
oheimb@15188
|
757 |
apply (simp add: sconc_def)
|
haftmann@27111
|
758 |
apply (cases "#x")
|
haftmann@27111
|
759 |
apply auto
|
haftmann@27111
|
760 |
apply (rule someI2_ex, auto)
|
oheimb@15188
|
761 |
by (drule ex_sconc,simp)
|
oheimb@15188
|
762 |
|
oheimb@15188
|
763 |
lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y"
|
haftmann@27111
|
764 |
apply (cases "#x",auto)
|
haftmann@27111
|
765 |
apply (simp add: sconc_def iSuc_Fin)
|
oheimb@15188
|
766 |
apply (rule someI2_ex)
|
haftmann@27111
|
767 |
apply (drule ex_sconc, simp)
|
haftmann@27111
|
768 |
apply (rule someI2_ex, auto)
|
oheimb@15188
|
769 |
apply (simp add: i_rt_Suc_forw)
|
haftmann@27111
|
770 |
apply (rule_tac x="a && x" in exI, auto)
|
oheimb@15188
|
771 |
apply (case_tac "xa=UU",auto)
|
oheimb@15188
|
772 |
apply (drule stream_exhaust_eq [THEN iffD1],auto)
|
oheimb@15188
|
773 |
apply (drule streams_prefix_lemma1,simp+)
|
oheimb@15188
|
774 |
by (simp add: sconc_def)
|
oheimb@15188
|
775 |
|
oheimb@15188
|
776 |
lemma ft_sconc: "x ~= UU ==> ft$(x ooo y) = ft$x"
|
oheimb@15188
|
777 |
by (rule stream.casedist [of x],auto)
|
oheimb@15188
|
778 |
|
oheimb@15188
|
779 |
lemma sconc_assoc: "(x ooo y) ooo z = x ooo y ooo z"
|
oheimb@15188
|
780 |
apply (case_tac "#x")
|
oheimb@15188
|
781 |
apply (rule stream_finite_ind [of x],auto simp del: scons_sconc)
|
oheimb@15188
|
782 |
apply (simp add: stream.finite_def del: scons_sconc)
|
oheimb@15188
|
783 |
apply (drule slen_take_lemma1,auto simp del: scons_sconc)
|
oheimb@15188
|
784 |
apply (case_tac "a = UU", auto)
|
oheimb@15188
|
785 |
by (simp add: sconc_def)
|
oheimb@15188
|
786 |
|
oheimb@15188
|
787 |
|
oheimb@15188
|
788 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
789 |
|
huffman@25833
|
790 |
lemma cont_sconc_lemma1: "stream_finite x \<Longrightarrow> cont (\<lambda>y. x ooo y)"
|
huffman@25833
|
791 |
by (erule stream_finite_ind, simp_all)
|
huffman@25833
|
792 |
|
huffman@25833
|
793 |
lemma cont_sconc_lemma2: "\<not> stream_finite x \<Longrightarrow> cont (\<lambda>y. x ooo y)"
|
huffman@25833
|
794 |
by (simp add: sconc_def slen_def)
|
huffman@25833
|
795 |
|
huffman@25833
|
796 |
lemma cont_sconc: "cont (\<lambda>y. x ooo y)"
|
huffman@25833
|
797 |
apply (cases "stream_finite x")
|
huffman@25833
|
798 |
apply (erule cont_sconc_lemma1)
|
huffman@25833
|
799 |
apply (erule cont_sconc_lemma2)
|
huffman@25833
|
800 |
done
|
huffman@25833
|
801 |
|
oheimb@15188
|
802 |
lemma sconc_mono: "y << y' ==> x ooo y << x ooo y'"
|
huffman@25833
|
803 |
by (rule cont_sconc [THEN cont2mono, THEN monofunE])
|
oheimb@15188
|
804 |
|
oheimb@15188
|
805 |
lemma sconc_mono1 [simp]: "x << x ooo y"
|
oheimb@15188
|
806 |
by (rule sconc_mono [of UU, simplified])
|
oheimb@15188
|
807 |
|
oheimb@15188
|
808 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
809 |
|
oheimb@15188
|
810 |
lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)"
|
oheimb@15188
|
811 |
apply (case_tac "#x",auto)
|
wenzelm@17291
|
812 |
apply (insert sconc_mono1 [of x y])
|
huffman@19440
|
813 |
by auto
|
oheimb@15188
|
814 |
|
oheimb@15188
|
815 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
816 |
|
oheimb@15188
|
817 |
lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x"
|
oheimb@15188
|
818 |
by (rule stream.casedist,auto)
|
oheimb@15188
|
819 |
|
wenzelm@17291
|
820 |
lemma i_th_sconc_lemma [rule_format]:
|
oheimb@15188
|
821 |
"ALL x y. Fin n < #x --> i_th n (x ooo y) = i_th n x"
|
oheimb@15188
|
822 |
apply (induct_tac n, auto)
|
oheimb@15188
|
823 |
apply (simp add: Fin_0 i_th_def)
|
oheimb@15188
|
824 |
apply (simp add: slen_empty_eq ft_sconc)
|
oheimb@15188
|
825 |
apply (simp add: i_th_def)
|
oheimb@15188
|
826 |
apply (case_tac "x=UU",auto)
|
oheimb@15188
|
827 |
apply (drule stream_exhaust_eq [THEN iffD1], auto)
|
oheimb@15188
|
828 |
apply (erule_tac x="ya" in allE)
|
haftmann@27111
|
829 |
apply (case_tac "#ya") by simp_all
|
oheimb@15188
|
830 |
|
oheimb@15188
|
831 |
|
oheimb@15188
|
832 |
|
oheimb@15188
|
833 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
834 |
|
oheimb@15188
|
835 |
lemma sconc_lemma [rule_format, simp]: "ALL s. stream_take n$s ooo i_rt n s = s"
|
oheimb@15188
|
836 |
apply (induct_tac n,auto)
|
oheimb@15188
|
837 |
apply (case_tac "s=UU",auto)
|
oheimb@15188
|
838 |
by (drule stream_exhaust_eq [THEN iffD1],auto)
|
oheimb@15188
|
839 |
|
oheimb@15188
|
840 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
841 |
subsection "pointwise equality"
|
oheimb@15188
|
842 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
843 |
|
wenzelm@17291
|
844 |
lemma ex_last_stream_take_scons: "stream_take (Suc n)$s =
|
oheimb@15188
|
845 |
stream_take n$s ooo i_rt n (stream_take (Suc n)$s)"
|
oheimb@15188
|
846 |
by (insert sconc_lemma [of n "stream_take (Suc n)$s"],simp)
|
oheimb@15188
|
847 |
|
wenzelm@17291
|
848 |
lemma i_th_stream_take_eq:
|
oheimb@15188
|
849 |
"!!n. ALL n. i_th n s1 = i_th n s2 ==> stream_take n$s1 = stream_take n$s2"
|
oheimb@15188
|
850 |
apply (induct_tac n,auto)
|
oheimb@15188
|
851 |
apply (subgoal_tac "stream_take (Suc na)$s1 =
|
oheimb@15188
|
852 |
stream_take na$s1 ooo i_rt na (stream_take (Suc na)$s1)")
|
wenzelm@17291
|
853 |
apply (subgoal_tac "i_rt na (stream_take (Suc na)$s1) =
|
oheimb@15188
|
854 |
i_rt na (stream_take (Suc na)$s2)")
|
wenzelm@17291
|
855 |
apply (subgoal_tac "stream_take (Suc na)$s2 =
|
oheimb@15188
|
856 |
stream_take na$s2 ooo i_rt na (stream_take (Suc na)$s2)")
|
oheimb@15188
|
857 |
apply (insert ex_last_stream_take_scons,simp)
|
oheimb@15188
|
858 |
apply blast
|
oheimb@15188
|
859 |
apply (erule_tac x="na" in allE)
|
oheimb@15188
|
860 |
apply (insert i_th_last_eq [of _ s1 s2])
|
oheimb@15188
|
861 |
by blast+
|
oheimb@15188
|
862 |
|
oheimb@15188
|
863 |
lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2"
|
oheimb@15188
|
864 |
by (insert i_th_stream_take_eq [THEN stream.take_lemmas],blast)
|
oheimb@15188
|
865 |
|
oheimb@15188
|
866 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
867 |
subsection "finiteness"
|
oheimb@15188
|
868 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
869 |
|
oheimb@15188
|
870 |
lemma slen_sconc_finite1:
|
oheimb@15188
|
871 |
"[| #(x ooo y) = Infty; Fin n = #x |] ==> #y = Infty"
|
oheimb@15188
|
872 |
apply (case_tac "#y ~= Infty",auto)
|
oheimb@15188
|
873 |
apply (drule_tac y=y in rt_sconc1)
|
oheimb@15188
|
874 |
apply (insert stream_finite_i_rt [of n "x ooo y"])
|
oheimb@15188
|
875 |
by (simp add: slen_infinite)
|
oheimb@15188
|
876 |
|
oheimb@15188
|
877 |
lemma slen_sconc_infinite1: "#x=Infty ==> #(x ooo y) = Infty"
|
oheimb@15188
|
878 |
by (simp add: sconc_def)
|
oheimb@15188
|
879 |
|
oheimb@15188
|
880 |
lemma slen_sconc_infinite2: "#y=Infty ==> #(x ooo y) = Infty"
|
oheimb@15188
|
881 |
apply (case_tac "#x")
|
oheimb@15188
|
882 |
apply (simp add: sconc_def)
|
oheimb@15188
|
883 |
apply (rule someI2_ex)
|
oheimb@15188
|
884 |
apply (drule ex_sconc,auto)
|
oheimb@15188
|
885 |
apply (erule contrapos_pp)
|
oheimb@15188
|
886 |
apply (insert stream_finite_i_rt)
|
nipkow@31084
|
887 |
apply (fastsimp simp add: slen_infinite,auto)
|
oheimb@15188
|
888 |
by (simp add: sconc_def)
|
oheimb@15188
|
889 |
|
oheimb@15188
|
890 |
lemma sconc_finite: "(#x~=Infty & #y~=Infty) = (#(x ooo y)~=Infty)"
|
oheimb@15188
|
891 |
apply auto
|
nipkow@31084
|
892 |
apply (metis not_Infty_eq slen_sconc_finite1)
|
nipkow@31084
|
893 |
apply (metis not_Infty_eq slen_sconc_infinite1)
|
nipkow@31084
|
894 |
apply (metis not_Infty_eq slen_sconc_infinite2)
|
nipkow@31084
|
895 |
done
|
oheimb@15188
|
896 |
|
oheimb@15188
|
897 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
898 |
|
oheimb@15188
|
899 |
lemma slen_sconc_mono3: "[| Fin n = #x; Fin k = #(x ooo y) |] ==> n <= k"
|
oheimb@15188
|
900 |
apply (insert slen_mono [of "x" "x ooo y"])
|
haftmann@27111
|
901 |
apply (cases "#x") apply simp_all
|
haftmann@27111
|
902 |
apply (cases "#(x ooo y)") apply simp_all
|
haftmann@27111
|
903 |
done
|
oheimb@15188
|
904 |
|
oheimb@15188
|
905 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
906 |
subsection "finite slen"
|
oheimb@15188
|
907 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
908 |
|
oheimb@15188
|
909 |
lemma slen_sconc: "[| Fin n = #x; Fin m = #y |] ==> #(x ooo y) = Fin (n + m)"
|
oheimb@15188
|
910 |
apply (case_tac "#(x ooo y)")
|
oheimb@15188
|
911 |
apply (frule_tac y=y in rt_sconc1)
|
oheimb@15188
|
912 |
apply (insert take_i_rt_len [of "THE j. Fin j = #(x ooo y)" "x ooo y" n n m],simp)
|
oheimb@15188
|
913 |
apply (insert slen_sconc_mono3 [of n x _ y],simp)
|
oheimb@15188
|
914 |
by (insert sconc_finite [of x y],auto)
|
oheimb@15188
|
915 |
|
oheimb@15188
|
916 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
917 |
subsection "flat prefix"
|
oheimb@15188
|
918 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
919 |
|
oheimb@15188
|
920 |
lemma sconc_prefix: "(s1::'a::flat stream) << s2 ==> EX t. s1 ooo t = s2"
|
oheimb@15188
|
921 |
apply (case_tac "#s1")
|
wenzelm@17291
|
922 |
apply (subgoal_tac "stream_take nat$s1 = stream_take nat$s2")
|
oheimb@15188
|
923 |
apply (rule_tac x="i_rt nat s2" in exI)
|
oheimb@15188
|
924 |
apply (simp add: sconc_def)
|
oheimb@15188
|
925 |
apply (rule someI2_ex)
|
oheimb@15188
|
926 |
apply (drule ex_sconc)
|
oheimb@15188
|
927 |
apply (simp,clarsimp,drule streams_prefix_lemma1)
|
wenzelm@17291
|
928 |
apply (simp+,rule slen_take_lemma3 [of _ s1 s2])
|
oheimb@15188
|
929 |
apply (simp+,rule_tac x="UU" in exI)
|
wenzelm@17291
|
930 |
apply (insert slen_take_lemma3 [of _ s1 s2])
|
oheimb@15188
|
931 |
by (rule stream.take_lemmas,simp)
|
oheimb@15188
|
932 |
|
oheimb@15188
|
933 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
934 |
subsection "continuity"
|
oheimb@15188
|
935 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
936 |
|
oheimb@15188
|
937 |
lemma chain_sconc: "chain S ==> chain (%i. (x ooo S i))"
|
oheimb@15188
|
938 |
by (simp add: chain_def,auto simp add: sconc_mono)
|
oheimb@15188
|
939 |
|
oheimb@15188
|
940 |
lemma chain_scons: "chain S ==> chain (%i. a && S i)"
|
oheimb@15188
|
941 |
apply (simp add: chain_def,auto)
|
oheimb@15188
|
942 |
by (rule monofun_cfun_arg,simp)
|
oheimb@15188
|
943 |
|
oheimb@15188
|
944 |
lemma contlub_scons: "contlub (%x. a && x)"
|
oheimb@15188
|
945 |
by (simp add: contlub_Rep_CFun2)
|
oheimb@15188
|
946 |
|
oheimb@15188
|
947 |
lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
|
huffman@25833
|
948 |
by (rule contlubE [OF contlub_Rep_CFun2, symmetric])
|
oheimb@15188
|
949 |
|
wenzelm@17291
|
950 |
lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==>
|
oheimb@15188
|
951 |
(LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
|
oheimb@15188
|
952 |
apply (rule stream_finite_ind [of x])
|
oheimb@15188
|
953 |
apply (auto)
|
oheimb@15188
|
954 |
apply (subgoal_tac "(LUB i. a && (s ooo Y i)) = a && (LUB i. s ooo Y i)")
|
oheimb@15188
|
955 |
by (force,blast dest: contlub_scons_lemma chain_sconc)
|
oheimb@15188
|
956 |
|
wenzelm@17291
|
957 |
lemma contlub_sconc_lemma:
|
oheimb@15188
|
958 |
"chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
|
oheimb@15188
|
959 |
apply (case_tac "#x=Infty")
|
oheimb@15188
|
960 |
apply (simp add: sconc_def)
|
huffman@18075
|
961 |
apply (drule finite_lub_sconc,auto simp add: slen_infinite)
|
huffman@18075
|
962 |
done
|
oheimb@15188
|
963 |
|
wenzelm@17291
|
964 |
lemma contlub_sconc: "contlub (%y. x ooo y)"
|
huffman@25833
|
965 |
by (rule cont_sconc [THEN cont2contlub])
|
oheimb@15188
|
966 |
|
oheimb@15188
|
967 |
lemma monofun_sconc: "monofun (%y. x ooo y)"
|
huffman@16218
|
968 |
by (simp add: monofun_def sconc_mono)
|
oheimb@15188
|
969 |
|
oheimb@15188
|
970 |
|
oheimb@15188
|
971 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
972 |
section "constr_sconc"
|
oheimb@15188
|
973 |
(* ----------------------------------------------------------------------- *)
|
oheimb@15188
|
974 |
|
oheimb@15188
|
975 |
lemma constr_sconc_UUs [simp]: "constr_sconc UU s = s"
|
haftmann@27111
|
976 |
by (simp add: constr_sconc_def zero_inat_def)
|
oheimb@15188
|
977 |
|
oheimb@15188
|
978 |
lemma "x ooo y = constr_sconc x y"
|
oheimb@15188
|
979 |
apply (case_tac "#x")
|
oheimb@15188
|
980 |
apply (rule stream_finite_ind [of x],auto simp del: scons_sconc)
|
oheimb@15188
|
981 |
defer 1
|
oheimb@15188
|
982 |
apply (simp add: constr_sconc_def del: scons_sconc)
|
oheimb@15188
|
983 |
apply (case_tac "#s")
|
haftmann@27111
|
984 |
apply (simp add: iSuc_Fin)
|
oheimb@15188
|
985 |
apply (case_tac "a=UU",auto simp del: scons_sconc)
|
oheimb@15188
|
986 |
apply (simp)
|
oheimb@15188
|
987 |
apply (simp add: sconc_def)
|
oheimb@15188
|
988 |
apply (simp add: constr_sconc_def)
|
oheimb@15188
|
989 |
apply (simp add: stream.finite_def)
|
oheimb@15188
|
990 |
by (drule slen_take_lemma1,auto)
|
oheimb@15188
|
991 |
|
oheimb@2570
|
992 |
end
|