--- a/src/HOL/Code_Numeral.thy Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Code_Numeral.thy Wed Mar 31 16:44:41 2010 +0200
@@ -280,6 +280,16 @@
hide (open) const of_nat nat_of int_of
+subsubsection {* Lazy Evaluation of an indexed function *}
+
+function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Predicate.pred"
+where
+ "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))"
+by pat_completeness auto
+
+termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
+
+hide (open) const iterate_upto
subsection {* Code generator setup *}