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