1.1 --- a/src/HOL/Code_Numeral.thy	Wed Mar 31 16:44:41 2010 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Mar 31 16:44:41 2010 +0200
     1.3 @@ -280,6 +280,16 @@
     1.4  
     1.5  hide (open) const of_nat nat_of int_of
     1.6  
     1.7 +subsubsection {* Lazy Evaluation of an indexed function *}
     1.8 +
     1.9 +function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Predicate.pred"
    1.10 +where
    1.11 +  "iterate_upto f n m = Predicate.Seq (%u. if n > m then Predicate.Empty else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
    1.12 +by pat_completeness auto
    1.13 +
    1.14 +termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
    1.15 +
    1.16 +hide (open) const iterate_upto
    1.17  
    1.18  subsection {* Code generator setup *}
    1.19