src/HOL/Lazy_Sequence.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 58152 6fe60a9a5bad
child 58310 91ea607a34d8
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     1 
     2 (* Author: Lukas Bulwahn, TU Muenchen *)
     3 
     4 header {* Lazy sequences *}
     5 
     6 theory Lazy_Sequence
     7 imports Predicate
     8 begin
     9 
    10 subsection {* Type of lazy sequences *}
    11 
    12 datatype_new (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
    13 
    14 primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
    15 where
    16   "list_of_lazy_sequence (lazy_sequence_of_list xs) = xs"
    17 
    18 lemma lazy_sequence_of_list_of_lazy_sequence [simp]:
    19   "lazy_sequence_of_list (list_of_lazy_sequence xq) = xq"
    20   by (cases xq) simp_all
    21 
    22 lemma lazy_sequence_eqI:
    23   "list_of_lazy_sequence xq = list_of_lazy_sequence yq \<Longrightarrow> xq = yq"
    24   by (cases xq, cases yq) simp
    25 
    26 lemma lazy_sequence_eq_iff:
    27   "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
    28   by (auto intro: lazy_sequence_eqI)
    29 
    30 lemma size_lazy_sequence_eq [code]:
    31   "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
    32   "size xq = Suc (length (list_of_lazy_sequence xq))"
    33   by (cases xq, simp)+
    34 
    35 lemma case_lazy_sequence [simp]:
    36   "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
    37   by (cases xq) auto
    38 
    39 lemma rec_lazy_sequence [simp]:
    40   "rec_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
    41   by (cases xq) auto
    42 
    43 definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence"
    44 where
    45   "Lazy_Sequence f = lazy_sequence_of_list (case f () of
    46     None \<Rightarrow> []
    47   | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
    48 
    49 code_datatype Lazy_Sequence
    50 
    51 declare list_of_lazy_sequence.simps [code del]
    52 declare lazy_sequence.case [code del]
    53 declare lazy_sequence.rec [code del]
    54 
    55 lemma list_of_Lazy_Sequence [simp]:
    56   "list_of_lazy_sequence (Lazy_Sequence f) = (case f () of
    57     None \<Rightarrow> []
    58   | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
    59   by (simp add: Lazy_Sequence_def)
    60 
    61 definition yield :: "'a lazy_sequence \<Rightarrow> ('a \<times> 'a lazy_sequence) option"
    62 where
    63   "yield xq = (case list_of_lazy_sequence xq of
    64     [] \<Rightarrow> None
    65   | x # xs \<Rightarrow> Some (x, lazy_sequence_of_list xs))" 
    66 
    67 lemma yield_Seq [simp, code]:
    68   "yield (Lazy_Sequence f) = f ()"
    69   by (cases "f ()") (simp_all add: yield_def split_def)
    70 
    71 lemma case_yield_eq [simp]: "case_option g h (yield xq) =
    72   case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
    73   by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
    74 
    75 lemma size_lazy_sequence_code [code]:
    76   "size_lazy_sequence s xq = (case yield xq of
    77     None \<Rightarrow> 1
    78   | Some (x, xq') \<Rightarrow> Suc (s x + size_lazy_sequence s xq'))"
    79   by (cases "list_of_lazy_sequence xq") (simp_all add: size_lazy_sequence_eq)
    80 
    81 lemma equal_lazy_sequence_code [code]:
    82   "HOL.equal xq yq = (case (yield xq, yield yq) of
    83     (None, None) \<Rightarrow> True
    84   | (Some (x, xq'), Some (y, yq')) \<Rightarrow> HOL.equal x y \<and> HOL.equal xq yq
    85   | _ \<Rightarrow> False)"
    86   by (simp_all add: lazy_sequence_eq_iff equal_eq split: list.splits)
    87 
    88 lemma [code nbe]:
    89   "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
    90   by (fact equal_refl)
    91 
    92 definition empty :: "'a lazy_sequence"
    93 where
    94   "empty = lazy_sequence_of_list []"
    95 
    96 lemma list_of_lazy_sequence_empty [simp]:
    97   "list_of_lazy_sequence empty = []"
    98   by (simp add: empty_def)
    99 
   100 lemma empty_code [code]:
   101   "empty = Lazy_Sequence (\<lambda>_. None)"
   102   by (simp add: lazy_sequence_eq_iff)
   103 
   104 definition single :: "'a \<Rightarrow> 'a lazy_sequence"
   105 where
   106   "single x = lazy_sequence_of_list [x]"
   107 
   108 lemma list_of_lazy_sequence_single [simp]:
   109   "list_of_lazy_sequence (single x) = [x]"
   110   by (simp add: single_def)
   111 
   112 lemma single_code [code]:
   113   "single x = Lazy_Sequence (\<lambda>_. Some (x, empty))"
   114   by (simp add: lazy_sequence_eq_iff)
   115 
   116 definition append :: "'a lazy_sequence \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a lazy_sequence"
   117 where
   118   "append xq yq = lazy_sequence_of_list (list_of_lazy_sequence xq @ list_of_lazy_sequence yq)"
   119 
   120 lemma list_of_lazy_sequence_append [simp]:
   121   "list_of_lazy_sequence (append xq yq) = list_of_lazy_sequence xq @ list_of_lazy_sequence yq"
   122   by (simp add: append_def)
   123 
   124 lemma append_code [code]:
   125   "append xq yq = Lazy_Sequence (\<lambda>_. case yield xq of
   126     None \<Rightarrow> yield yq
   127   | Some (x, xq') \<Rightarrow> Some (x, append xq' yq))"
   128   by (simp_all add: lazy_sequence_eq_iff split: list.splits)
   129 
   130 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b lazy_sequence"
   131 where
   132   "map f xq = lazy_sequence_of_list (List.map f (list_of_lazy_sequence xq))"
   133 
   134 lemma list_of_lazy_sequence_map [simp]:
   135   "list_of_lazy_sequence (map f xq) = List.map f (list_of_lazy_sequence xq)"
   136   by (simp add: map_def)
   137 
   138 lemma map_code [code]:
   139   "map f xq =
   140     Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
   141   by (simp_all add: lazy_sequence_eq_iff split: list.splits)
   142 
   143 definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence"
   144 where
   145   "flat xqq = lazy_sequence_of_list (concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq)))"
   146 
   147 lemma list_of_lazy_sequence_flat [simp]:
   148   "list_of_lazy_sequence (flat xqq) = concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq))"
   149   by (simp add: flat_def)
   150 
   151 lemma flat_code [code]:
   152   "flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
   153     None \<Rightarrow> None
   154   | Some (xq, xqq') \<Rightarrow> yield (append xq (flat xqq')))"
   155   by (simp add: lazy_sequence_eq_iff split: list.splits)
   156 
   157 definition bind :: "'a lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b lazy_sequence) \<Rightarrow> 'b lazy_sequence"
   158 where
   159   "bind xq f = flat (map f xq)"
   160 
   161 definition if_seq :: "bool \<Rightarrow> unit lazy_sequence"
   162 where
   163   "if_seq b = (if b then single () else empty)"
   164 
   165 definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option"
   166 where
   167   "those xq = map_option lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
   168   
   169 function iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a lazy_sequence"
   170 where
   171   "iterate_upto f n m =
   172     Lazy_Sequence (\<lambda>_. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
   173   by pat_completeness auto
   174 
   175 termination by (relation "measure (\<lambda>(f, n, m). nat_of_natural (m + 1 - n))")
   176   (auto simp add: less_natural_def)
   177 
   178 definition not_seq :: "unit lazy_sequence \<Rightarrow> unit lazy_sequence"
   179 where
   180   "not_seq xq = (case yield xq of
   181     None \<Rightarrow> single ()
   182   | Some ((), xq) \<Rightarrow> empty)"
   183 
   184   
   185 subsection {* Code setup *}
   186 
   187 code_reflect Lazy_Sequence
   188   datatypes lazy_sequence = Lazy_Sequence
   189 
   190 ML {*
   191 signature LAZY_SEQUENCE =
   192 sig
   193   datatype 'a lazy_sequence = Lazy_Sequence of (unit -> ('a * 'a Lazy_Sequence.lazy_sequence) option)
   194   val map: ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
   195   val yield: 'a lazy_sequence -> ('a * 'a lazy_sequence) option
   196   val yieldn: int -> 'a lazy_sequence -> 'a list * 'a lazy_sequence
   197 end;
   198 
   199 structure Lazy_Sequence : LAZY_SEQUENCE =
   200 struct
   201 
   202 datatype lazy_sequence = datatype Lazy_Sequence.lazy_sequence;
   203 
   204 fun map f = @{code Lazy_Sequence.map} f;
   205 
   206 fun yield P = @{code Lazy_Sequence.yield} P;
   207 
   208 fun yieldn k = Predicate.anamorph yield k;
   209 
   210 end;
   211 *}
   212 
   213 
   214 subsection {* Generator Sequences *}
   215 
   216 subsubsection {* General lazy sequence operation *}
   217 
   218 definition product :: "'a lazy_sequence \<Rightarrow> 'b lazy_sequence \<Rightarrow> ('a \<times> 'b) lazy_sequence"
   219 where
   220   "product s1 s2 = bind s1 (\<lambda>a. bind s2 (\<lambda>b. single (a, b)))"
   221 
   222 
   223 subsubsection {* Small lazy typeclasses *}
   224 
   225 class small_lazy =
   226   fixes small_lazy :: "natural \<Rightarrow> 'a lazy_sequence"
   227 
   228 instantiation unit :: small_lazy
   229 begin
   230 
   231 definition "small_lazy d = single ()"
   232 
   233 instance ..
   234 
   235 end
   236 
   237 instantiation int :: small_lazy
   238 begin
   239 
   240 text {* maybe optimise this expression -> append (single x) xs == cons x xs 
   241 Performance difference? *}
   242 
   243 function small_lazy' :: "int \<Rightarrow> int \<Rightarrow> int lazy_sequence"
   244 where
   245   "small_lazy' d i = (if d < i then empty
   246     else append (single i) (small_lazy' d (i + 1)))"
   247     by pat_completeness auto
   248 
   249 termination 
   250   by (relation "measure (%(d, i). nat (d + 1 - i))") auto
   251 
   252 definition
   253   "small_lazy d = small_lazy' (int (nat_of_natural d)) (- (int (nat_of_natural d)))"
   254 
   255 instance ..
   256 
   257 end
   258 
   259 instantiation prod :: (small_lazy, small_lazy) small_lazy
   260 begin
   261 
   262 definition
   263   "small_lazy d = product (small_lazy d) (small_lazy d)"
   264 
   265 instance ..
   266 
   267 end
   268 
   269 instantiation list :: (small_lazy) small_lazy
   270 begin
   271 
   272 fun small_lazy_list :: "natural \<Rightarrow> 'a list lazy_sequence"
   273 where
   274   "small_lazy_list d = append (single [])
   275     (if d > 0 then bind (product (small_lazy (d - 1))
   276       (small_lazy (d - 1))) (\<lambda>(x, xs). single (x # xs)) else empty)"
   277 
   278 instance ..
   279 
   280 end
   281 
   282 subsection {* With Hit Bound Value *}
   283 text {* assuming in negative context *}
   284 
   285 type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
   286 
   287 definition hit_bound :: "'a hit_bound_lazy_sequence"
   288 where
   289   "hit_bound = Lazy_Sequence (\<lambda>_. Some (None, empty))"
   290 
   291 lemma list_of_lazy_sequence_hit_bound [simp]:
   292   "list_of_lazy_sequence hit_bound = [None]"
   293   by (simp add: hit_bound_def)
   294   
   295 definition hb_single :: "'a \<Rightarrow> 'a hit_bound_lazy_sequence"
   296 where
   297   "hb_single x = Lazy_Sequence (\<lambda>_. Some (Some x, empty))"
   298 
   299 definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence"
   300 where
   301   "hb_map f xq = map (map_option f) xq"
   302 
   303 lemma hb_map_code [code]:
   304   "hb_map f xq =
   305     Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (map_option f x, hb_map f xq')) (yield xq))"
   306   using map_code [of "map_option f" xq] by (simp add: hb_map_def)
   307 
   308 definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence"
   309 where
   310   "hb_flat xqq = lazy_sequence_of_list (concat
   311     (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> map_option list_of_lazy_sequence) (list_of_lazy_sequence xqq)))"
   312 
   313 lemma list_of_lazy_sequence_hb_flat [simp]:
   314   "list_of_lazy_sequence (hb_flat xqq) =
   315     concat (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> map_option list_of_lazy_sequence) (list_of_lazy_sequence xqq))"
   316   by (simp add: hb_flat_def)
   317 
   318 lemma hb_flat_code [code]:
   319   "hb_flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
   320     None \<Rightarrow> None
   321   | Some (xq, xqq') \<Rightarrow> yield
   322      (append (case xq of None \<Rightarrow> hit_bound | Some xq \<Rightarrow> xq) (hb_flat xqq')))"
   323   by (simp add: lazy_sequence_eq_iff split: list.splits option.splits)
   324 
   325 definition hb_bind :: "'a hit_bound_lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b hit_bound_lazy_sequence) \<Rightarrow> 'b hit_bound_lazy_sequence"
   326 where
   327   "hb_bind xq f = hb_flat (hb_map f xq)"
   328 
   329 definition hb_if_seq :: "bool \<Rightarrow> unit hit_bound_lazy_sequence"
   330 where
   331   "hb_if_seq b = (if b then hb_single () else empty)"
   332 
   333 definition hb_not_seq :: "unit hit_bound_lazy_sequence \<Rightarrow> unit lazy_sequence"
   334 where
   335   "hb_not_seq xq = (case yield xq of
   336     None \<Rightarrow> single ()
   337   | Some (x, xq) \<Rightarrow> empty)"
   338 
   339 hide_const (open) yield empty single append flat map bind
   340   if_seq those iterate_upto not_seq product
   341 
   342 hide_fact (open) yield_def empty_def single_def append_def flat_def map_def bind_def
   343   if_seq_def those_def not_seq_def product_def 
   344 
   345 end