1(* Title: HOL/HOLCF/FOCUS/Fstreams.thy 2 Author: Borislav Gajanovic 3 4FOCUS flat streams (with lifted elements). 5 6TODO: integrate this with Fstream. 7*) 8 9theory Fstreams 10imports "HOLCF-Library.Stream" 11begin 12 13default_sort type 14 15type_synonym 'a fstream = "('a lift) stream" 16 17definition 18 fsingleton :: "'a => 'a fstream" ("<_>" [1000] 999) where 19 fsingleton_def2: "fsingleton = (%a. Def a && UU)" 20 21definition 22 fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where 23 "fsfilter A = sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))" 24 25definition 26 fsmap :: "('a => 'b) => 'a fstream -> 'b fstream" where 27 "fsmap f = smap\<cdot>(flift2 f)" 28 29definition 30 jth :: "nat => 'a fstream => 'a" where 31 "jth = (%n s. if enat n < #s then THE a. i_th n s = Def a else undefined)" 32 33definition 34 first :: "'a fstream => 'a" where 35 "first = (%s. jth 0 s)" 36 37definition 38 last :: "'a fstream => 'a" where 39 "last = (%s. case #s of enat n => (if n~=0 then jth (THE k. Suc k = n) s else undefined))" 40 41 42abbreviation 43 emptystream :: "'a fstream" ("<>") where 44 "<> == \<bottom>" 45 46abbreviation 47 fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)" [64,63] 63) where 48 "A\<copyright>s == fsfilter A\<cdot>s" 49 50notation (ASCII) 51 fsfilter' ("(_'(C')_)" [64,63] 63) 52 53 54lemma ft_fsingleton[simp]: "ft\<cdot>(<a>) = Def a" 55by (simp add: fsingleton_def2) 56 57lemma slen_fsingleton[simp]: "#(<a>) = enat 1" 58by (simp add: fsingleton_def2 enat_defs) 59 60lemma slen_fstreams[simp]: "#(<a> ooo s) = eSuc (#s)" 61by (simp add: fsingleton_def2) 62 63lemma slen_fstreams2[simp]: "#(s ooo <a>) = eSuc (#s)" 64apply (cases "#s") 65apply (auto simp add: eSuc_enat) 66apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto) 67apply (simp add: sconc_def) 68done 69 70lemma j_th_0_fsingleton[simp]:"jth 0 (<a>) = a" 71apply (simp add: fsingleton_def2 jth_def) 72apply (simp add: i_th_def enat_0) 73done 74 75lemma jth_0[simp]: "jth 0 (<a> ooo s) = a" 76apply (simp add: fsingleton_def2 jth_def) 77apply (simp add: i_th_def enat_0) 78done 79 80lemma first_sconc[simp]: "first (<a> ooo s) = a" 81by (simp add: first_def) 82 83lemma first_fsingleton[simp]: "first (<a>) = a" 84by (simp add: first_def) 85 86lemma jth_n[simp]: "enat n = #s ==> jth n (s ooo <a>) = a" 87apply (simp add: jth_def, auto) 88apply (simp add: i_th_def rt_sconc1) 89apply (simp add: enat_defs split: enat.splits) 90done 91 92lemma last_sconc[simp]: "enat n = #s ==> last (s ooo <a>) = a" 93apply (simp add: last_def) 94apply (simp add: enat_defs split:enat.splits) 95apply (drule sym, auto) 96done 97 98lemma last_fsingleton[simp]: "last (<a>) = a" 99by (simp add: last_def) 100 101lemma first_UU[simp]: "first UU = undefined" 102by (simp add: first_def jth_def) 103 104lemma last_UU[simp]:"last UU = undefined" 105by (simp add: last_def jth_def enat_defs) 106 107lemma last_infinite[simp]:"#s = \<infinity> \<Longrightarrow> last s = undefined" 108by (simp add: last_def) 109 110lemma jth_slen_lemma1:"n \<le> k \<and> enat n = #s \<Longrightarrow> jth k s = undefined" 111by (simp add: jth_def enat_defs split:enat.splits, auto) 112 113lemma jth_UU[simp]:"jth n UU = undefined" 114by (simp add: jth_def) 115 116lemma ext_last:"\<lbrakk>s \<noteq> UU; enat (Suc n) = #s\<rbrakk> \<Longrightarrow> (stream_take n\<cdot>s) ooo <(last s)> = s" 117apply (simp add: last_def) 118apply (case_tac "#s", auto) 119apply (simp add: fsingleton_def2) 120apply (subgoal_tac "Def (jth n s) = i_th n s") 121apply (auto simp add: i_th_last) 122apply (drule slen_take_lemma1, auto) 123apply (simp add: jth_def) 124apply (case_tac "i_th n s = UU") 125apply auto 126apply (simp add: i_th_def) 127apply (case_tac "i_rt n s = UU", auto) 128apply (drule i_rt_slen [THEN iffD1]) 129apply (drule slen_take_eq_rev [rule_format, THEN iffD2],auto) 130apply (drule not_Undef_is_Def [THEN iffD1], auto) 131done 132 133 134lemma fsingleton_lemma1[simp]: "(<a> = <b>) = (a=b)" 135by (simp add: fsingleton_def2) 136 137lemma fsingleton_lemma2[simp]: "<a> ~= <>" 138by (simp add: fsingleton_def2) 139 140lemma fsingleton_sconc:"<a> ooo s = Def a && s" 141by (simp add: fsingleton_def2) 142 143lemma fstreams_ind: 144 "[| adm P; P <>; !!a s. P s ==> P (<a> ooo s) |] ==> P x" 145apply (simp add: fsingleton_def2) 146apply (rule stream.induct, auto) 147apply (drule not_Undef_is_Def [THEN iffD1], auto) 148done 149 150lemma fstreams_ind2: 151 "[| adm P; P <>; !!a. P (<a>); !!a b s. P s ==> P (<a> ooo <b> ooo s) |] ==> P x" 152apply (simp add: fsingleton_def2) 153apply (rule stream_ind2, auto) 154apply (drule not_Undef_is_Def [THEN iffD1], auto)+ 155done 156 157lemma fstreams_take_Suc[simp]: "stream_take (Suc n)\<cdot>(<a> ooo s) = <a> ooo stream_take n\<cdot>s" 158by (simp add: fsingleton_def2) 159 160lemma fstreams_not_empty[simp]: "<a> ooo s \<noteq> <>" 161by (simp add: fsingleton_def2) 162 163lemma fstreams_not_empty2[simp]: "s ooo <a> \<noteq> <>" 164by (case_tac "s=UU", auto) 165 166lemma fstreams_exhaust: "x = UU \<or> (\<exists>a s. x = <a> ooo s)" 167apply (simp add: fsingleton_def2, auto) 168apply (erule contrapos_pp, auto) 169apply (drule stream_exhaust_eq [THEN iffD1], auto) 170apply (drule not_Undef_is_Def [THEN iffD1], auto) 171done 172 173lemma fstreams_cases: "\<lbrakk>x = UU \<Longrightarrow> P; \<And>a y. x = <a> ooo y \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 174by (insert fstreams_exhaust [of x], auto) 175 176lemma fstreams_exhaust_eq: "x \<noteq> UU \<longleftrightarrow> (\<exists>a y. x = <a> ooo y)" 177apply (simp add: fsingleton_def2, auto) 178apply (drule stream_exhaust_eq [THEN iffD1], auto) 179apply (drule not_Undef_is_Def [THEN iffD1], auto) 180done 181 182lemma fstreams_inject: "<a> ooo s = <b> ooo t \<longleftrightarrow> a = b \<and> s = t" 183by (simp add: fsingleton_def2) 184 185lemma fstreams_prefix: "<a> ooo s << t \<Longrightarrow> \<exists>tt. t = <a> ooo tt \<and> s << tt" 186apply (simp add: fsingleton_def2) 187apply (insert stream_prefix [of "Def a" s t], auto) 188done 189 190lemma fstreams_prefix': "x << <a> ooo z \<longleftrightarrow> x = <> \<or> (\<exists>y. x = <a> ooo y \<and> y << z)" 191apply (auto, case_tac "x=UU", auto) 192apply (drule stream_exhaust_eq [THEN iffD1], auto) 193apply (simp add: fsingleton_def2, auto) 194apply (drule ax_flat, simp) 195apply (erule sconc_mono) 196done 197 198lemma ft_fstreams[simp]: "ft\<cdot>(<a> ooo s) = Def a" 199by (simp add: fsingleton_def2) 200 201lemma rt_fstreams[simp]: "rt\<cdot>(<a> ooo s) = s" 202by (simp add: fsingleton_def2) 203 204lemma ft_eq[simp]: "ft\<cdot>s = Def a \<longleftrightarrow> (\<exists>t. s = <a> ooo t)" 205apply (cases s, auto) 206apply (auto simp add: fsingleton_def2) 207done 208 209lemma surjective_fstreams: "<d> ooo y = x \<longleftrightarrow> (ft\<cdot>x = Def d \<and> rt\<cdot>x = y)" 210by auto 211 212lemma fstreams_mono: "<a> ooo b << <a> ooo c \<Longrightarrow> b << c" 213by (simp add: fsingleton_def2) 214 215lemma fsmap_UU[simp]: "fsmap f\<cdot>UU = UU" 216by (simp add: fsmap_def) 217 218lemma fsmap_fsingleton_sconc: "fsmap f\<cdot>(<x> ooo xs) = <(f x)> ooo (fsmap f\<cdot>xs)" 219by (simp add: fsmap_def fsingleton_def2 flift2_def) 220 221lemma fsmap_fsingleton[simp]: "fsmap f\<cdot>(<x>) = <(f x)>" 222by (simp add: fsmap_def fsingleton_def2 flift2_def) 223 224 225lemma fstreams_chain_lemma[rule_format]: 226 "\<forall>s x y. stream_take n\<cdot>(s::'a fstream) << x \<and> x << y \<and> y << s \<and> x \<noteq> y \<longrightarrow> stream_take (Suc n)\<cdot>s << y" 227apply (induct_tac n, auto) 228apply (case_tac "s=UU", auto) 229apply (drule stream_exhaust_eq [THEN iffD1], auto) 230apply (case_tac "y=UU", auto) 231apply (drule stream_exhaust_eq [THEN iffD1], auto) 232apply (simp add: flat_below_iff) 233apply (case_tac "s=UU", auto) 234apply (drule stream_exhaust_eq [THEN iffD1], auto) 235apply (erule_tac x="ya" in allE) 236apply (drule stream_prefix, auto) 237apply (case_tac "y=UU",auto) 238apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) 239apply auto 240apply (simp add: flat_below_iff) 241apply (erule_tac x="tt" in allE) 242apply (erule_tac x="yb" in allE, auto) 243apply (simp add: flat_below_iff) 244apply (simp add: flat_below_iff) 245done 246 247lemma fstreams_lub_lemma1: "\<lbrakk>chain Y; (LUB i. Y i) = <a> ooo s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = <a> ooo t" 248apply (subgoal_tac "(LUB i. Y i) ~= UU") 249apply (frule lub_eq_bottom_iff, auto) 250apply (drule_tac x="i" in is_ub_thelub, auto) 251apply (drule fstreams_prefix' [THEN iffD1], auto) 252done 253 254lemma fstreams_lub1: 255 "\<lbrakk>chain Y; (LUB i. Y i) = <a> ooo s\<rbrakk> 256 \<Longrightarrow> (\<exists>j t. Y j = <a> ooo t) \<and> (\<exists>X. chain X \<and> (\<forall>i. \<exists>j. <a> ooo X i << Y j) \<and> (LUB i. X i) = s)" 257apply (auto simp add: fstreams_lub_lemma1) 258apply (rule_tac x="\<lambda>n. stream_take n\<cdot>s" in exI, auto) 259apply (induct_tac i, auto) 260apply (drule fstreams_lub_lemma1, auto) 261apply (rule_tac x="j" in exI, auto) 262apply (case_tac "max_in_chain j Y") 263apply (frule lub_finch1 [THEN lub_eqI], auto) 264apply (rule_tac x="j" in exI) 265apply (erule subst) back back 266apply (simp add: below_prod_def sconc_mono) 267apply (simp add: max_in_chain_def, auto) 268apply (rule_tac x="ja" in exI) 269apply (subgoal_tac "Y j << Y ja") 270apply (drule fstreams_prefix, auto)+ 271apply (rule sconc_mono) 272apply (rule fstreams_chain_lemma, auto) 273apply (subgoal_tac "Y ja << (LUB i. (Y i))", clarsimp) 274apply (drule fstreams_mono, simp) 275apply (rule is_ub_thelub, simp) 276apply (blast intro: chain_mono) 277by (rule stream_reach2) 278 279 280lemma lub_Pair_not_UU_lemma: 281 "\<lbrakk>chain Y; (LUB i. Y i) = ((a::'a::flat), b); a \<noteq> UU; b \<noteq> UU\<rbrakk> 282 \<Longrightarrow> \<exists>j c d. Y j = (c, d) \<and> c \<noteq> UU \<and> d \<noteq> UU" 283apply (frule lub_prod, clarsimp) 284apply (clarsimp simp add: lub_eq_bottom_iff [where Y="\<lambda>i. fst (Y i)"]) 285apply (case_tac "Y i", clarsimp) 286apply (case_tac "max_in_chain i Y") 287apply (drule maxinch_is_thelub, auto) 288apply (rule_tac x="i" in exI, auto) 289apply (simp add: max_in_chain_def, auto) 290apply (subgoal_tac "Y i << Y j",auto) 291apply (simp add: below_prod_def, clarsimp) 292apply (drule ax_flat, auto) 293apply (case_tac "snd (Y j) = UU",auto) 294apply (case_tac "Y j", auto) 295apply (rule_tac x="j" in exI) 296apply (case_tac "Y j",auto) 297apply (drule chain_mono, auto) 298done 299 300lemma fstreams_lub_lemma2: 301 "\<lbrakk>chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) \<noteq> UU\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = (a, <m> ooo t)" 302apply (frule lub_Pair_not_UU_lemma, auto) 303apply (drule_tac x="j" in is_ub_thelub, auto) 304apply (drule ax_flat, clarsimp) 305apply (drule fstreams_prefix' [THEN iffD1], auto) 306done 307 308lemma fstreams_lub2: 309 "\<lbrakk>chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) \<noteq> UU\<rbrakk> 310 \<Longrightarrow> (\<exists>j t. Y j = (a, <m> ooo t)) \<and> (\<exists>X. chain X \<and> (\<forall>i. \<exists>j. (a, <m> ooo X i) << Y j) \<and> (LUB i. X i) = ms)" 311apply (auto simp add: fstreams_lub_lemma2) 312apply (rule_tac x="\<lambda>n. stream_take n\<cdot>ms" in exI, auto) 313apply (induct_tac i, auto) 314apply (drule fstreams_lub_lemma2, auto) 315apply (rule_tac x="j" in exI, auto) 316apply (case_tac "max_in_chain j Y") 317apply (frule lub_finch1 [THEN lub_eqI], auto) 318apply (rule_tac x="j" in exI) 319apply (erule subst) back back 320apply (simp add: sconc_mono) 321apply (simp add: max_in_chain_def, auto) 322apply (rule_tac x="ja" in exI) 323apply (subgoal_tac "Y j << Y ja") 324apply (simp add: below_prod_def, auto) 325apply (drule below_trans) 326apply (simp add: ax_flat, auto) 327apply (drule fstreams_prefix, auto)+ 328apply (rule sconc_mono) 329apply (subgoal_tac "tt \<noteq> tta" "tta << ms") 330apply (blast intro: fstreams_chain_lemma) 331apply (frule lub_prod, auto) 332apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp) 333apply (drule fstreams_mono, simp) 334apply (rule is_ub_thelub chainI) 335apply (simp add: chain_def below_prod_def) 336apply (subgoal_tac "fst (Y j) \<noteq> fst (Y ja) \<or> snd (Y j) \<noteq> snd (Y ja)", simp) 337apply (drule ax_flat, simp)+ 338apply (drule prod_eqI, auto) 339apply (simp add: chain_mono) 340apply (rule stream_reach2) 341done 342 343 344lemma cpo_cont_lemma: 345 "\<lbrakk>monofun (f::'a::cpo \<Rightarrow> 'b::cpo); (\<forall>Y. chain Y \<longrightarrow> f (lub(range Y)) << (LUB i. f (Y i)))\<rbrakk> \<Longrightarrow> cont f" 346apply (erule contI2) 347apply simp 348done 349 350end 351