src/HOL/Lazy_Sequence.thy
changeset 36030 1cd962a0b1a6
parent 36024 c1ce2f60b0f2
child 36049 0ce5b7a5c2fd
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:48 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:49 2010 +0200
     1.3 @@ -152,6 +152,59 @@
     1.4  
     1.5  code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
     1.6  
     1.7 +section {* With Hit Bound Value *}
     1.8 +text {* assuming in negative context *}
     1.9 +
    1.10 +types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
    1.11 +
    1.12 +definition hit_bound :: "'a hit_bound_lazy_sequence"
    1.13 +where
    1.14 +  [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
    1.15 +
    1.16 +
    1.17 +definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
    1.18 +where
    1.19 +  [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
    1.20 +
    1.21 +primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
    1.22 +where
    1.23 +  "hb_flat Empty = Empty"
    1.24 +| "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq)"
    1.25 +
    1.26 +lemma [code]:
    1.27 +  "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
    1.28 +    None => None
    1.29 +  | Some (xq, xqq') => yield (append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq')))"
    1.30 +apply (cases "xqq")
    1.31 +apply (auto simp add: Seq_yield)
    1.32 +unfolding Lazy_Sequence_def
    1.33 +by auto
    1.34 +
    1.35 +primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence"
    1.36 +where
    1.37 +  "hb_map f Empty = Empty"
    1.38 +| "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)"
    1.39 +
    1.40 +lemma [code]:
    1.41 +  "hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
    1.42 +apply (cases xq)
    1.43 +apply (auto simp add: Seq_yield)
    1.44 +unfolding Lazy_Sequence_def
    1.45 +apply auto
    1.46 +done
    1.47 +
    1.48 +definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
    1.49 +where
    1.50 +  [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
    1.51 +
    1.52 +definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
    1.53 +where
    1.54 +  "hb_if_seq b = (if b then hb_single () else empty)"
    1.55 +
    1.56 +definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence"
    1.57 +where
    1.58 +  "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
    1.59 +
    1.60  hide (open) type lazy_sequence
    1.61  hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
    1.62  hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def