adding Lazy_Sequences with explicit depth-bound

--- a/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:48 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:49 2010 +0200
@@ -152,6 +152,59 @@
 
 code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
 
+section {* With Hit Bound Value *}
+text {* assuming in negative context *}
+
+types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
+
+definition hit_bound :: "'a hit_bound_lazy_sequence"
+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))"
+
+primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
+where
+  "hb_flat Empty = Empty"
+| "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq)"
+
+lemma [code]:
+  "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
+    None => None
+  | Some (xq, xqq') => yield (append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq')))"
+apply (cases "xqq")
+apply (auto simp add: Seq_yield)
+unfolding Lazy_Sequence_def
+by auto
+
+primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence"
+where
+  "hb_map f Empty = Empty"
+| "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)"
+
+lemma [code]:
+  "hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
+apply (cases xq)
+apply (auto simp add: Seq_yield)
+unfolding Lazy_Sequence_def
+apply auto
+done
+
+definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
+where
+  [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
+
+definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
+where
+  "hb_if_seq b = (if b then hb_single () else empty)"
+
+definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence"
+where
+  "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
+
 hide (open) type lazy_sequence
 hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
 hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:48 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:49 2010 +0200
@@ -916,10 +916,9 @@
 fun mk_not t =
   let
     val pT = mk_pos_random_dseqT HOLogic.unitT
-    val nT =
-  @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
-    @{typ code_numeral} --> Type (@{type_name Option.option},
-      [Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])])
+    val nT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+      @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
+        [Type (@{type_name Option.option}, [@{typ unit}])])
 
   in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
 
@@ -938,12 +937,12 @@
 fun mk_neg_random_dseqT T =
    @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
     @{typ code_numeral} --> 
-    Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])
+    Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
 
 fun dest_neg_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
     Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
-    Type (@{type_name Option.option},
-      [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])])) = T
+      Type (@{type_name Lazy_Sequence.lazy_sequence},
+        [Type (@{type_name Option.option}, [T])])])])])])) = T
   | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
 
 fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);