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