src/HOLCF/FOCUS/Fstream.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,263 +0,0 @@
     1.4 -(*  Title:      HOLCF/FOCUS/Fstream.thy
     1.5 -    Author:     David von Oheimb, TU Muenchen
     1.6 -
     1.7 -FOCUS streams (with lifted elements).
     1.8 -
     1.9 -TODO: integrate Fstreams.thy
    1.10 -*)
    1.11 -
    1.12 -header {* FOCUS flat streams *}
    1.13 -
    1.14 -theory Fstream
    1.15 -imports Stream
    1.16 -begin
    1.17 -
    1.18 -default_sort type
    1.19 -
    1.20 -types 'a fstream = "'a lift stream"
    1.21 -
    1.22 -definition
    1.23 -  fscons        :: "'a     \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
    1.24 -  "fscons a = (\<Lambda> s. Def a && s)"
    1.25 -
    1.26 -definition
    1.27 -  fsfilter      :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
    1.28 -  "fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))"
    1.29 -
    1.30 -abbreviation
    1.31 -  emptystream   :: "'a fstream"                          ("<>") where
    1.32 -  "<> == \<bottom>"
    1.33 -
    1.34 -abbreviation
    1.35 -  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_~>_)"    [66,65] 65) where
    1.36 -  "a~>s == fscons a\<cdot>s"
    1.37 -
    1.38 -abbreviation
    1.39 -  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   ("(_'(C')_)" [64,63] 63) where
    1.40 -  "A(C)s == fsfilter A\<cdot>s"
    1.41 -
    1.42 -notation (xsymbols)
    1.43 -  fscons'  ("(_\<leadsto>_)"                                                 [66,65] 65) and
    1.44 -  fsfilter'  ("(_\<copyright>_)"                                               [64,63] 63)
    1.45 -
    1.46 -
    1.47 -lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
    1.48 -by simp
    1.49 -
    1.50 -
    1.51 -section "fscons"
    1.52 -
    1.53 -lemma fscons_def2: "a~>s = Def a && s"
    1.54 -apply (unfold fscons_def)
    1.55 -apply (simp)
    1.56 -done
    1.57 -
    1.58 -lemma fstream_exhaust: "x = UU |  (? a y. x = a~> y)"
    1.59 -apply (simp add: fscons_def2)
    1.60 -apply (cut_tac stream.nchotomy)
    1.61 -apply (fast dest: not_Undef_is_Def [THEN iffD1])
    1.62 -done
    1.63 -
    1.64 -lemma fstream_cases: "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P"
    1.65 -apply (cut_tac fstream_exhaust)
    1.66 -apply (erule disjE)
    1.67 -apply fast
    1.68 -apply fast
    1.69 -done
    1.70 -
    1.71 -lemma fstream_exhaust_eq: "(x ~= UU) = (? a y. x = a~> y)"
    1.72 -apply (simp add: fscons_def2 stream_exhaust_eq)
    1.73 -apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
    1.74 -done
    1.75 -
    1.76 -
    1.77 -lemma fscons_not_empty [simp]: "a~> s ~= <>"
    1.78 -by (simp add: fscons_def2)
    1.79 -
    1.80 -
    1.81 -lemma fscons_inject [simp]: "(a~> s = b~> t) = (a = b &  s = t)"
    1.82 -by (simp add: fscons_def2)
    1.83 -
    1.84 -lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt &  s << tt"
    1.85 -apply (cases t)
    1.86 -apply (cut_tac fscons_not_empty)
    1.87 -apply (fast dest: eq_UU_iff [THEN iffD2])
    1.88 -apply (simp add: fscons_def2)
    1.89 -done
    1.90 -
    1.91 -lemma fstream_prefix' [simp]:
    1.92 -        "x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))"
    1.93 -apply (simp add: fscons_def2 Def_not_UU [THEN stream_prefix'])
    1.94 -apply (safe)
    1.95 -apply (erule_tac [!] contrapos_np)
    1.96 -prefer 2 apply (fast elim: DefE)
    1.97 -apply (rule lift.exhaust)
    1.98 -apply (erule (1) notE)
    1.99 -apply (safe)
   1.100 -apply (drule Def_below_Def [THEN iffD1])
   1.101 -apply fast
   1.102 -done
   1.103 -
   1.104 -(* ------------------------------------------------------------------------- *)
   1.105 -
   1.106 -section "ft & rt"
   1.107 -
   1.108 -lemmas ft_empty = stream.sel_rews (1)
   1.109 -lemma ft_fscons [simp]: "ft\<cdot>(m~> s) = Def m"
   1.110 -by (simp add: fscons_def)
   1.111 -
   1.112 -lemmas rt_empty = stream.sel_rews (2)
   1.113 -lemma rt_fscons [simp]: "rt\<cdot>(m~> s) = s"
   1.114 -by (simp add: fscons_def)
   1.115 -
   1.116 -lemma ft_eq [simp]: "(ft\<cdot>s = Def a) = (? t. s = a~> t)"
   1.117 -apply (unfold fscons_def)
   1.118 -apply (simp)
   1.119 -apply (safe)
   1.120 -apply (erule subst)
   1.121 -apply (rule exI)
   1.122 -apply (rule surjectiv_scons [symmetric])
   1.123 -apply (simp)
   1.124 -done
   1.125 -
   1.126 -lemma surjective_fscons_lemma: "(d\<leadsto>y = x) = (ft\<cdot>x = Def d & rt\<cdot>x = y)"
   1.127 -by auto
   1.128 -
   1.129 -lemma surjective_fscons: "ft\<cdot>x = Def d \<Longrightarrow> d\<leadsto>rt\<cdot>x = x"
   1.130 -by (simp add: surjective_fscons_lemma)
   1.131 -
   1.132 -
   1.133 -(* ------------------------------------------------------------------------- *)
   1.134 -
   1.135 -section "take"
   1.136 -
   1.137 -lemma fstream_take_Suc [simp]:
   1.138 -        "stream_take (Suc n)\<cdot>(a~> s) = a~> stream_take n\<cdot>s"
   1.139 -by (simp add: fscons_def)
   1.140 -
   1.141 -
   1.142 -(* ------------------------------------------------------------------------- *)
   1.143 -
   1.144 -section "slen"
   1.145 -
   1.146 -lemma slen_fscons: "#(m~> s) = iSuc (#s)"
   1.147 -by (simp add: fscons_def)
   1.148 -
   1.149 -lemma slen_fscons_eq:
   1.150 -        "(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)"
   1.151 -apply (simp add: fscons_def2 slen_scons_eq)
   1.152 -apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
   1.153 -done
   1.154 -
   1.155 -lemma slen_fscons_eq_rev:
   1.156 -        "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))"
   1.157 -apply (simp add: fscons_def2 slen_scons_eq_rev)
   1.158 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   1.159 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   1.160 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   1.161 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   1.162 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   1.163 -apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   1.164 -apply (erule contrapos_np)
   1.165 -apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
   1.166 -done
   1.167 -
   1.168 -lemma slen_fscons_less_eq:
   1.169 -        "(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))"
   1.170 -apply (subst slen_fscons_eq_rev)
   1.171 -apply (fast dest!: fscons_inject [THEN iffD1])
   1.172 -done
   1.173 -
   1.174 -
   1.175 -(* ------------------------------------------------------------------------- *)
   1.176 -
   1.177 -section "induction"
   1.178 -
   1.179 -lemma fstream_ind:
   1.180 -        "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x"
   1.181 -apply (erule stream.induct)
   1.182 -apply (assumption)
   1.183 -apply (unfold fscons_def2)
   1.184 -apply (fast dest: not_Undef_is_Def [THEN iffD1])
   1.185 -done
   1.186 -
   1.187 -lemma fstream_ind2:
   1.188 -  "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x"
   1.189 -apply (erule stream_ind2)
   1.190 -apply (assumption)
   1.191 -apply (unfold fscons_def2)
   1.192 -apply (fast dest: not_Undef_is_Def [THEN iffD1])
   1.193 -apply (fast dest: not_Undef_is_Def [THEN iffD1])
   1.194 -done
   1.195 -
   1.196 -
   1.197 -(* ------------------------------------------------------------------------- *)
   1.198 -
   1.199 -section "fsfilter"
   1.200 -
   1.201 -lemma fsfilter_empty: "A(C)UU = UU"
   1.202 -apply (unfold fsfilter_def)
   1.203 -apply (rule sfilter_empty)
   1.204 -done
   1.205 -
   1.206 -lemma fsfilter_fscons:
   1.207 -        "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)"
   1.208 -apply (unfold fsfilter_def)
   1.209 -apply (simp add: fscons_def2 If_and_if)
   1.210 -done
   1.211 -
   1.212 -lemma fsfilter_emptys: "{}(C)x = UU"
   1.213 -apply (rule_tac x="x" in fstream_ind)
   1.214 -apply (simp)
   1.215 -apply (rule fsfilter_empty)
   1.216 -apply (simp add: fsfilter_fscons)
   1.217 -done
   1.218 -
   1.219 -lemma fsfilter_insert: "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)"
   1.220 -by (simp add: fsfilter_fscons)
   1.221 -
   1.222 -lemma fsfilter_single_in: "{a}(C)a~> x = a~> ({a}(C)x)"
   1.223 -by (rule fsfilter_insert)
   1.224 -
   1.225 -lemma fsfilter_single_out: "b ~= a ==> {a}(C)b~> x = ({a}(C)x)"
   1.226 -by (simp add: fsfilter_fscons)
   1.227 -
   1.228 -lemma fstream_lub_lemma1:
   1.229 -    "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
   1.230 -apply (case_tac "max_in_chain i Y")
   1.231 -apply  (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
   1.232 -apply  (force)
   1.233 -apply (unfold max_in_chain_def)
   1.234 -apply auto
   1.235 -apply (frule (1) chain_mono)
   1.236 -apply (rule_tac x="Y j" in fstream_cases)
   1.237 -apply  (force)
   1.238 -apply (drule_tac x="j" in is_ub_thelub)
   1.239 -apply (force)
   1.240 -done
   1.241 -
   1.242 -lemma fstream_lub_lemma:
   1.243 -      "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> (\<exists>j t. Y j = a\<leadsto>t) & (\<exists>X. chain X & (!i. ? j. Y j = a\<leadsto>X i) & (\<Squnion>i. X i) = s)"
   1.244 -apply (frule (1) fstream_lub_lemma1)
   1.245 -apply (clarsimp)
   1.246 -apply (rule_tac x="%i. rt\<cdot>(Y(i+j))" in exI)
   1.247 -apply (rule conjI)
   1.248 -apply  (erule chain_shift [THEN chain_monofun])
   1.249 -apply safe
   1.250 -apply  (drule_tac i="j" and j="i+j" in chain_mono)
   1.251 -apply   (simp)
   1.252 -apply  (simp)
   1.253 -apply  (rule_tac x="i+j" in exI)
   1.254 -apply  (drule fstream_prefix)
   1.255 -apply  (clarsimp)
   1.256 -apply  (subst contlub_cfun [symmetric])
   1.257 -apply   (rule chainI)
   1.258 -apply   (fast)
   1.259 -apply  (erule chain_shift)
   1.260 -apply (subst lub_const)
   1.261 -apply (subst lub_range_shift)
   1.262 -apply  (assumption)
   1.263 -apply (simp)
   1.264 -done
   1.265 -
   1.266 -end