src/HOL/Lazy_Sequence.thy
changeset 40051 b6acda4d1c29
parent 38857 97775f3e8722
child 40056 0bee30e3a4ad
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Thu Oct 21 19:13:08 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Thu Oct 21 19:13:09 2010 +0200
     1.3 @@ -140,6 +140,71 @@
     1.4    datatypes lazy_sequence = Lazy_Sequence
     1.5    functions map yield yieldn
     1.6  
     1.7 +subsection {* Generator Sequences *}
     1.8 +
     1.9 +
    1.10 +subsubsection {* General lazy sequence operation *}
    1.11 +
    1.12 +definition product :: "'a Lazy_Sequence.lazy_sequence \<Rightarrow> 'b Lazy_Sequence.lazy_sequence \<Rightarrow> ('a * 'b) Lazy_Sequence.lazy_sequence"
    1.13 +where
    1.14 +  "product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))"
    1.15 +
    1.16 +
    1.17 +subsubsection {* small_lazy typeclasses *}
    1.18 +
    1.19 +class small_lazy =
    1.20 +  fixes small_lazy :: "int \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
    1.21 +
    1.22 +instantiation unit :: small_lazy
    1.23 +begin
    1.24 +
    1.25 +definition "small_lazy d = Lazy_Sequence.single ()"
    1.26 +
    1.27 +instance ..
    1.28 +
    1.29 +end
    1.30 +
    1.31 +instantiation int :: small_lazy
    1.32 +begin
    1.33 +
    1.34 +text {* maybe optimise this expression -> append (single x) xs == cons x xs 
    1.35 +Performance difference? *}
    1.36 +
    1.37 +function small_lazy' :: "int => int => int Lazy_Sequence.lazy_sequence"
    1.38 +where "small_lazy' d i = (if d < i then Lazy_Sequence.empty else
    1.39 +  Lazy_Sequence.append (Lazy_Sequence.single i) (small_lazy' d (i + 1)))"
    1.40 +by pat_completeness auto
    1.41 +
    1.42 +termination 
    1.43 +  by (relation "measure (%(d, i). nat (d + 1 - i))") auto
    1.44 +
    1.45 +definition "small_lazy d = small_lazy' d (- d)"
    1.46 +
    1.47 +instance ..
    1.48 +
    1.49 +end
    1.50 +
    1.51 +instantiation prod :: (small_lazy, small_lazy) small_lazy
    1.52 +begin
    1.53 +
    1.54 +definition
    1.55 +  "small_lazy d = product (small_lazy d) (small_lazy d)"
    1.56 +
    1.57 +instance ..
    1.58 +
    1.59 +end
    1.60 +
    1.61 +instantiation list :: (small_lazy) small_lazy
    1.62 +begin
    1.63 +
    1.64 +fun small_lazy_list :: "int => 'a list Lazy_Sequence.lazy_sequence"
    1.65 +where
    1.66 +  "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)"
    1.67 +
    1.68 +instance ..
    1.69 +
    1.70 +end
    1.71 +
    1.72  subsection {* With Hit Bound Value *}
    1.73  text {* assuming in negative context *}
    1.74  
    1.75 @@ -149,7 +214,6 @@
    1.76  where
    1.77    [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
    1.78  
    1.79 -
    1.80  definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
    1.81  where
    1.82    [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
    1.83 @@ -194,7 +258,10 @@
    1.84    "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
    1.85  
    1.86  hide_type (open) lazy_sequence
    1.87 -hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
    1.88 -hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
    1.89 +hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq
    1.90 +  iterate_upto not_seq product
    1.91 +  
    1.92 +hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def
    1.93 +  iterate_upto.simps product_def if_seq_def not_seq_def
    1.94  
    1.95  end