src/HOL/Code_Numeral.thy
changeset 36049 0ce5b7a5c2fd
parent 35687 564a49e8be44
child 36176 3fe7e97ccca8
--- 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 *}