src/HOL/Lazy_Sequence.thy

--- a/src/HOL/Lazy_Sequence.thy	Thu Oct 21 19:13:08 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Thu Oct 21 19:13:09 2010 +0200
@@ -140,6 +140,71 @@
   datatypes lazy_sequence = Lazy_Sequence
   functions map yield yieldn
 
+subsection {* Generator Sequences *}
+
+
+subsubsection {* General lazy sequence operation *}
+
+definition product :: "'a Lazy_Sequence.lazy_sequence \<Rightarrow> 'b Lazy_Sequence.lazy_sequence \<Rightarrow> ('a * 'b) Lazy_Sequence.lazy_sequence"
+where
+  "product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))"
+
+
+subsubsection {* small_lazy typeclasses *}
+
+class small_lazy =
+  fixes small_lazy :: "int \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
+
+instantiation unit :: small_lazy
+begin
+
+definition "small_lazy d = Lazy_Sequence.single ()"
+
+instance ..
+
+end
+
+instantiation int :: small_lazy
+begin
+
+text {* maybe optimise this expression -> append (single x) xs == cons x xs 
+Performance difference? *}
+
+function small_lazy' :: "int => int => int Lazy_Sequence.lazy_sequence"
+where "small_lazy' d i = (if d < i then Lazy_Sequence.empty else
+  Lazy_Sequence.append (Lazy_Sequence.single i) (small_lazy' d (i + 1)))"
+by pat_completeness auto
+
+termination 
+  by (relation "measure (%(d, i). nat (d + 1 - i))") auto
+
+definition "small_lazy d = small_lazy' d (- d)"
+
+instance ..
+
+end
+
+instantiation prod :: (small_lazy, small_lazy) small_lazy
+begin
+
+definition
+  "small_lazy d = product (small_lazy d) (small_lazy d)"
+
+instance ..
+
+end
+
+instantiation list :: (small_lazy) small_lazy
+begin
+
+fun small_lazy_list :: "int => 'a list Lazy_Sequence.lazy_sequence"
+where
+  "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)"
+
+instance ..
+
+end
+
 subsection {* With Hit Bound Value *}
 text {* assuming in negative context *}
 
@@ -149,7 +214,6 @@
 where
   [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
 
-
 definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
 where
   [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
@@ -194,7 +258,10 @@
   "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
 
 hide_type (open) lazy_sequence
-hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
-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
+hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq
+  iterate_upto not_seq product
+  
+hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def
+  iterate_upto.simps product_def if_seq_def not_seq_def
 
 end