src/HOL/Lazy_Sequence.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45214 66ba67adafab
child 50055 94041d602ecb
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 
     2 (* Author: Lukas Bulwahn, TU Muenchen *)
     3 
     4 header {* Lazy sequences *}
     5 
     6 theory Lazy_Sequence
     7 imports List Code_Numeral
     8 begin
     9 
    10 datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence"
    11 
    12 definition Lazy_Sequence :: "(unit => ('a * 'a lazy_sequence) option) => 'a lazy_sequence"
    13 where
    14   "Lazy_Sequence f = (case f () of None => Empty | Some (x, xq) => Insert x xq)"
    15 
    16 code_datatype Lazy_Sequence 
    17 
    18 primrec yield :: "'a lazy_sequence => ('a * 'a lazy_sequence) option"
    19 where
    20   "yield Empty = None"
    21 | "yield (Insert x xq) = Some (x, xq)"
    22 
    23 lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
    24 by (cases xq) auto
    25 
    26 lemma yield_Seq [code]:
    27   "yield (Lazy_Sequence f) = f ()"
    28 unfolding Lazy_Sequence_def by (cases "f ()") auto
    29 
    30 lemma Seq_yield:
    31   "Lazy_Sequence (%u. yield f) = f"
    32 unfolding Lazy_Sequence_def by (cases f) auto
    33 
    34 lemma lazy_sequence_size_code [code]:
    35   "lazy_sequence_size s xq = (case yield xq of None => 0 | Some (x, xq') => s x + lazy_sequence_size s xq' + 1)"
    36 by (cases xq) auto
    37 
    38 lemma size_code [code]:
    39   "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
    40 by (cases xq) auto
    41 
    42 lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
    43   (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
    44 apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq) 
    45 apply (cases yq) apply (auto simp add: equal_eq) done
    46 
    47 lemma [code nbe]:
    48   "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
    49   by (fact equal_refl)
    50 
    51 lemma seq_case [code]:
    52   "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
    53 by (cases xq) auto
    54 
    55 lemma [code]: "lazy_sequence_rec f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq' (lazy_sequence_rec f g xq'))"
    56 by (cases xq) auto
    57 
    58 definition empty :: "'a lazy_sequence"
    59 where
    60   [code]: "empty = Lazy_Sequence (%u. None)"
    61 
    62 definition single :: "'a => 'a lazy_sequence"
    63 where
    64   [code]: "single x = Lazy_Sequence (%u. Some (x, empty))"
    65 
    66 primrec append :: "'a lazy_sequence => 'a lazy_sequence => 'a lazy_sequence"
    67 where
    68   "append Empty yq = yq"
    69 | "append (Insert x xq) yq = Insert x (append xq yq)"
    70 
    71 lemma [code]:
    72   "append xq yq = Lazy_Sequence (%u. case yield xq of
    73      None => yield yq
    74   | Some (x, xq') => Some (x, append xq' yq))"
    75 unfolding Lazy_Sequence_def
    76 apply (cases "xq")
    77 apply auto
    78 apply (cases "yq")
    79 apply auto
    80 done
    81 
    82 primrec flat :: "'a lazy_sequence lazy_sequence => 'a lazy_sequence"
    83 where
    84   "flat Empty = Empty"
    85 | "flat (Insert xq xqq) = append xq (flat xqq)"
    86  
    87 lemma [code]:
    88   "flat xqq = Lazy_Sequence (%u. case yield xqq of
    89     None => None
    90   | Some (xq, xqq') => yield (append xq (flat xqq')))"
    91 apply (cases "xqq")
    92 apply (auto simp add: Seq_yield)
    93 unfolding Lazy_Sequence_def
    94 by auto
    95 
    96 primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence"
    97 where
    98   "map f Empty = Empty"
    99 | "map f (Insert x xq) = Insert (f x) (map f xq)"
   100 
   101 lemma [code]:
   102   "map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))"
   103 apply (cases xq)
   104 apply (auto simp add: Seq_yield)
   105 unfolding Lazy_Sequence_def
   106 apply auto
   107 done
   108 
   109 definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence"
   110 where
   111   [code]: "bind xq f = flat (map f xq)"
   112 
   113 definition if_seq :: "bool => unit lazy_sequence"
   114 where
   115   "if_seq b = (if b then single () else empty)"
   116 
   117 function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence"
   118 where
   119   "iterate_upto f n m = Lazy_Sequence.Lazy_Sequence (%u. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
   120 by pat_completeness auto
   121 
   122 termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
   123 
   124 definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
   125 where
   126   "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
   127 
   128 subsection {* Code setup *}
   129 
   130 fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" where
   131   "anamorph f k x = (if k = 0 then ([], x)
   132     else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow>
   133       let (vs, z) = anamorph f (k - 1) y
   134     in (v # vs, z))"
   135 
   136 definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where
   137   "yieldn = anamorph yield"
   138 
   139 code_reflect Lazy_Sequence
   140   datatypes lazy_sequence = Lazy_Sequence
   141   functions map yield yieldn
   142 
   143 subsection {* Generator Sequences *}
   144 
   145 
   146 subsubsection {* General lazy sequence operation *}
   147 
   148 definition product :: "'a Lazy_Sequence.lazy_sequence \<Rightarrow> 'b Lazy_Sequence.lazy_sequence \<Rightarrow> ('a * 'b) Lazy_Sequence.lazy_sequence"
   149 where
   150   "product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))"
   151 
   152 
   153 subsubsection {* Small lazy typeclasses *}
   154 
   155 class small_lazy =
   156   fixes small_lazy :: "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
   157 
   158 instantiation unit :: small_lazy
   159 begin
   160 
   161 definition "small_lazy d = Lazy_Sequence.single ()"
   162 
   163 instance ..
   164 
   165 end
   166 
   167 instantiation int :: small_lazy
   168 begin
   169 
   170 text {* maybe optimise this expression -> append (single x) xs == cons x xs 
   171 Performance difference? *}
   172 
   173 function small_lazy' :: "int => int => int Lazy_Sequence.lazy_sequence"
   174 where "small_lazy' d i = (if d < i then Lazy_Sequence.empty else
   175   Lazy_Sequence.append (Lazy_Sequence.single i) (small_lazy' d (i + 1)))"
   176 by pat_completeness auto
   177 
   178 termination 
   179   by (relation "measure (%(d, i). nat (d + 1 - i))") auto
   180 
   181 definition "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
   182 
   183 instance ..
   184 
   185 end
   186 
   187 instantiation prod :: (small_lazy, small_lazy) small_lazy
   188 begin
   189 
   190 definition
   191   "small_lazy d = product (small_lazy d) (small_lazy d)"
   192 
   193 instance ..
   194 
   195 end
   196 
   197 instantiation list :: (small_lazy) small_lazy
   198 begin
   199 
   200 fun small_lazy_list :: "code_numeral => 'a list Lazy_Sequence.lazy_sequence"
   201 where
   202   "small_lazy_list d = Lazy_Sequence.append (Lazy_Sequence.single []) (if d > 0 then Lazy_Sequence.bind (product (small_lazy (d - 1)) (small_lazy (d - 1))) (%(x, xs). Lazy_Sequence.single (x # xs)) else Lazy_Sequence.empty)"
   203 
   204 instance ..
   205 
   206 end
   207 
   208 subsection {* With Hit Bound Value *}
   209 text {* assuming in negative context *}
   210 
   211 type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
   212 
   213 definition hit_bound :: "'a hit_bound_lazy_sequence"
   214 where
   215   [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
   216 
   217 definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
   218 where
   219   [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
   220 
   221 primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
   222 where
   223   "hb_flat Empty = Empty"
   224 | "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq)"
   225 
   226 lemma [code]:
   227   "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
   228     None => None
   229   | Some (xq, xqq') => yield (append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq')))"
   230 apply (cases "xqq")
   231 apply (auto simp add: Seq_yield)
   232 unfolding Lazy_Sequence_def
   233 by auto
   234 
   235 primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence"
   236 where
   237   "hb_map f Empty = Empty"
   238 | "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)"
   239 
   240 lemma [code]:
   241   "hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
   242 apply (cases xq)
   243 apply (auto simp add: Seq_yield)
   244 unfolding Lazy_Sequence_def
   245 apply auto
   246 done
   247 
   248 definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
   249 where
   250   [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
   251 
   252 definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
   253 where
   254   "hb_if_seq b = (if b then hb_single () else empty)"
   255 
   256 definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence"
   257 where
   258   "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
   259 
   260 hide_type (open) lazy_sequence
   261 hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq
   262   iterate_upto not_seq product
   263   
   264 hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def
   265   iterate_upto.simps product_def if_seq_def not_seq_def
   266 
   267 end