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