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