1(* Title: HOL/HOLCF/FOCUS/Fstream.thy 2 Author: David von Oheimb, TU Muenchen 3 4FOCUS streams (with lifted elements). 5 6TODO: integrate Fstreams.thy 7*) 8 9section \<open>FOCUS flat streams\<close> 10 11theory Fstream 12imports "HOLCF-Library.Stream" 13begin 14 15default_sort type 16 17type_synonym 'a fstream = "'a lift stream" 18 19definition 20 fscons :: "'a \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where 21 "fscons a = (\<Lambda> s. Def a && s)" 22 23definition 24 fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where 25 "fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))" 26 27abbreviation 28 emptystream :: "'a fstream" ("<>") where 29 "<> == \<bottom>" 30 31abbreviation 32 fscons' :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<leadsto>_)" [66,65] 65) where 33 "a\<leadsto>s == fscons a\<cdot>s" 34 35abbreviation 36 fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)" [64,63] 63) where 37 "A\<copyright>s == fsfilter A\<cdot>s" 38 39notation (ASCII) 40 fscons' ("(_~>_)" [66,65] 65) and 41 fsfilter' ("(_'(C')_)" [64,63] 63) 42 43 44lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d" 45by simp 46 47 48section "fscons" 49 50lemma fscons_def2: "a~>s = Def a && s" 51apply (unfold fscons_def) 52apply (simp) 53done 54 55lemma fstream_exhaust: "x = UU \<or> (\<exists>a y. x = a~> y)" 56apply (simp add: fscons_def2) 57apply (cut_tac stream.nchotomy) 58apply (fast dest: not_Undef_is_Def [THEN iffD1]) 59done 60 61lemma fstream_cases: "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P" 62apply (cut_tac fstream_exhaust) 63apply (erule disjE) 64apply fast 65apply fast 66done 67 68lemma fstream_exhaust_eq: "(x \<noteq> UU) = (\<exists>a y. x = a~> y)" 69apply (simp add: fscons_def2 stream_exhaust_eq) 70apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) 71done 72 73 74lemma fscons_not_empty [simp]: "a~> s \<noteq> <>" 75by (simp add: fscons_def2) 76 77 78lemma fscons_inject [simp]: "(a~> s = b~> t) = (a = b \<and> s = t)" 79by (simp add: fscons_def2) 80 81lemma fstream_prefix: "a~> s << t ==> \<exists>tt. t = a~> tt \<and> s << tt" 82apply (cases t) 83apply (cut_tac fscons_not_empty) 84apply (fast dest: bottomI) 85apply (simp add: fscons_def2) 86done 87 88lemma fstream_prefix' [simp]: 89 "x << a~> z = (x = <> \<or> (\<exists>y. x = a~> y \<and> y << z))" 90apply (simp add: fscons_def2 lift.distinct(2) [THEN stream_prefix']) 91apply (safe) 92apply (erule_tac [!] contrapos_np) 93prefer 2 apply (fast elim: DefE) 94apply (rule lift.exhaust) 95apply (erule (1) notE) 96apply (safe) 97apply (drule Def_below_Def [THEN iffD1]) 98apply fast 99done 100 101(* ------------------------------------------------------------------------- *) 102 103section "ft & rt" 104 105lemmas ft_empty = stream.sel_rews (1) 106lemma ft_fscons [simp]: "ft\<cdot>(m~> s) = Def m" 107by (simp add: fscons_def) 108 109lemmas rt_empty = stream.sel_rews (2) 110lemma rt_fscons [simp]: "rt\<cdot>(m~> s) = s" 111by (simp add: fscons_def) 112 113lemma ft_eq [simp]: "(ft\<cdot>s = Def a) = (\<exists>t. s = a~> t)" 114apply (unfold fscons_def) 115apply (simp) 116apply (safe) 117apply (erule subst) 118apply (rule exI) 119apply (rule surjectiv_scons [symmetric]) 120apply (simp) 121done 122 123lemma surjective_fscons_lemma: "(d\<leadsto>y = x) = (ft\<cdot>x = Def d & rt\<cdot>x = y)" 124by auto 125 126lemma surjective_fscons: "ft\<cdot>x = Def d \<Longrightarrow> d\<leadsto>rt\<cdot>x = x" 127by (simp add: surjective_fscons_lemma) 128 129 130(* ------------------------------------------------------------------------- *) 131 132section "take" 133 134lemma fstream_take_Suc [simp]: 135 "stream_take (Suc n)\<cdot>(a~> s) = a~> stream_take n\<cdot>s" 136by (simp add: fscons_def) 137 138 139(* ------------------------------------------------------------------------- *) 140 141section "slen" 142 143lemma slen_fscons: "#(m~> s) = eSuc (#s)" 144by (simp add: fscons_def) 145 146lemma slen_fscons_eq: 147 "(enat (Suc n) < #x) = (\<exists>a y. x = a~> y \<and> enat n < #y)" 148apply (simp add: fscons_def2 slen_scons_eq) 149apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) 150done 151 152lemma slen_fscons_eq_rev: 153 "(#x < enat (Suc (Suc n))) = (\<forall>a y. x \<noteq> a~> y \<or> #y < enat (Suc n))" 154apply (simp add: fscons_def2 slen_scons_eq_rev) 155apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>) 156apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>) 157apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>) 158apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>) 159apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>) 160apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>) 161apply (erule contrapos_np) 162apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) 163done 164 165lemma slen_fscons_less_eq: 166 "(#(a~> y) < enat (Suc (Suc n))) = (#y < enat (Suc n))" 167apply (subst slen_fscons_eq_rev) 168apply (fast dest!: fscons_inject [THEN iffD1]) 169done 170 171 172(* ------------------------------------------------------------------------- *) 173 174section "induction" 175 176lemma fstream_ind: 177 "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" 178apply (erule stream.induct) 179apply (assumption) 180apply (unfold fscons_def2) 181apply (fast dest: not_Undef_is_Def [THEN iffD1]) 182done 183 184lemma fstream_ind2: 185 "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x" 186apply (erule stream_ind2) 187apply (assumption) 188apply (unfold fscons_def2) 189apply (fast dest: not_Undef_is_Def [THEN iffD1]) 190apply (fast dest: not_Undef_is_Def [THEN iffD1]) 191done 192 193 194(* ------------------------------------------------------------------------- *) 195 196section "fsfilter" 197 198lemma fsfilter_empty: "A(C)UU = UU" 199apply (unfold fsfilter_def) 200apply (rule sfilter_empty) 201done 202 203lemma fsfilter_fscons: 204 "A(C)x~> xs = (if x\<in>A then x~> (A(C)xs) else A(C)xs)" 205apply (unfold fsfilter_def) 206apply (simp add: fscons_def2 If_and_if) 207done 208 209lemma fsfilter_emptys: "{}(C)x = UU" 210apply (rule_tac x="x" in fstream_ind) 211apply (simp) 212apply (rule fsfilter_empty) 213apply (simp add: fsfilter_fscons) 214done 215 216lemma fsfilter_insert: "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" 217by (simp add: fsfilter_fscons) 218 219lemma fsfilter_single_in: "{a}(C)a~> x = a~> ({a}(C)x)" 220by (rule fsfilter_insert) 221 222lemma fsfilter_single_out: "b ~= a ==> {a}(C)b~> x = ({a}(C)x)" 223by (simp add: fsfilter_fscons) 224 225lemma fstream_lub_lemma1: 226 "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t" 227apply (case_tac "max_in_chain i Y") 228apply (drule (1) lub_finch1 [THEN lub_eqI, THEN sym]) 229apply (force) 230apply (unfold max_in_chain_def) 231apply auto 232apply (frule (1) chain_mono) 233apply (rule_tac x="Y j" in fstream_cases) 234apply (force) 235apply (drule_tac x="j" in is_ub_thelub) 236apply (force) 237done 238 239lemma fstream_lub_lemma: 240 "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> (\<exists>j t. Y j = a\<leadsto>t) \<and> (\<exists>X. chain X \<and> (\<forall>i. \<exists>j. Y j = a\<leadsto>X i) \<and> (\<Squnion>i. X i) = s)" 241apply (frule (1) fstream_lub_lemma1) 242apply (clarsimp) 243apply (rule_tac x="\<lambda>i. rt\<cdot>(Y(i+j))" in exI) 244apply (rule conjI) 245apply (erule chain_shift [THEN chain_monofun]) 246apply safe 247apply (drule_tac i="j" and j="i+j" in chain_mono) 248apply (simp) 249apply (simp) 250apply (rule_tac x="i+j" in exI) 251apply (drule fstream_prefix) 252apply (clarsimp) 253apply (subst lub_APP) 254apply (rule chainI) 255apply (fast) 256apply (erule chain_shift) 257apply (subst lub_const) 258apply (subst lub_range_shift) 259apply (assumption) 260apply (simp) 261done 262 263end 264