src/HOL/Lazy_Sequence.thy
changeset 36049 0ce5b7a5c2fd
parent 36030 1cd962a0b1a6
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Mar 31 16:44:41 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Mar 31 16:44:41 2010 +0200
     1.3 @@ -110,6 +110,13 @@
     1.4  where
     1.5    "if_seq b = (if b then single () else empty)"
     1.6  
     1.7 +function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence"
     1.8 +where
     1.9 +  "iterate_upto f n m = Lazy_Sequence.Lazy_Sequence (%u. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
    1.10 +by pat_completeness auto
    1.11 +
    1.12 +termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
    1.13 +
    1.14  definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
    1.15  where
    1.16    "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
    1.17 @@ -206,7 +213,7 @@
    1.18    "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
    1.19  
    1.20  hide (open) type lazy_sequence
    1.21 -hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
    1.22 -hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
    1.23 +hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
    1.24 +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.25  
    1.26  end