adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler

--- 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 *}
 

--- a/src/HOL/Lazy_Sequence.thy	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Wed Mar 31 16:44:41 2010 +0200
@@ -110,6 +110,13 @@
 where
   "if_seq b = (if b then single () else empty)"
 
+function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence"
+where
+  "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))"
+by pat_completeness auto
+
+termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
+
 definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
 where
   "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
@@ -206,7 +213,7 @@
   "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
 
 hide (open) type lazy_sequence
-hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
-hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
+hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
+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
 
 end

--- a/src/HOL/New_DSequence.thy	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/New_DSequence.thy	Wed Mar 31 16:44:41 2010 +0200
@@ -35,6 +35,10 @@
 where
   "pos_if_seq b = (if b then pos_single () else pos_empty)"
 
+definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_dseq"
+where
+  "pos_iterate_upto f n m = (%i. Lazy_Sequence.iterate_upto f n m)"
+ 
 definition pos_map :: "('a => 'b) => 'a pos_dseq => 'b pos_dseq"
 where
   "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
@@ -67,6 +71,10 @@
 where
   "neg_if_seq b = (if b then neg_single () else neg_empty)"
 
+definition neg_iterate_upto 
+where
+  "neg_iterate_upto f n m = (%i. Lazy_Sequence.iterate_upto (%i. Some (f i)) n m)"
+
 definition neg_map :: "('a => 'b) => 'a neg_dseq => 'b neg_dseq"
 where
   "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
@@ -86,10 +94,10 @@
 hide (open) type pos_dseq neg_dseq
 
 hide (open) const 
-  pos_empty pos_single pos_bind pos_union pos_if_seq pos_not_seq
-  neg_empty neg_single neg_bind neg_union neg_if_seq neg_not_seq
+  pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
+  neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
 hide (open) fact
-  pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_not_seq_def pos_map_def
-  neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_not_seq_def neg_map_def
+  pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def
+  neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def
 
 end

--- a/src/HOL/New_Random_Sequence.thy	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/New_Random_Sequence.thy	Wed Mar 31 16:44:41 2010 +0200
@@ -28,6 +28,10 @@
 where
   "pos_if_random_dseq b = (if b then pos_single () else pos_empty)"
 
+definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_random_dseq"
+where
+  "pos_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.pos_iterate_upto f n m)"
+
 definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq"
 where
   "pos_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.pos_not_seq (R nrandom size seed))"
@@ -66,6 +70,10 @@
 where
   "neg_if_random_dseq b = (if b then neg_single () else neg_empty)"
 
+definition neg_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a neg_random_dseq"
+where
+  "neg_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.neg_iterate_upto f n m)"
+
 definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq"
 where
   "neg_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.neg_not_seq (R nrandom size seed))"
@@ -88,8 +96,9 @@
   DSequence.map
 *)
 
-hide (open) const pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_not_random_dseq iter Random pos_map
-  neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_not_random_dseq neg_map
+hide (open) const
+  pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
+  neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
 hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
 (* FIXME: hide facts *)
 (*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)

--- a/src/HOL/Quickcheck.thy	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Quickcheck.thy	Wed Mar 31 16:44:41 2010 +0200
@@ -187,6 +187,10 @@
 where
   "if_randompred b = (if b then single () else empty)"
 
+definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
+where
+  "iterate_upto f n m = Pair (Code_Numeral.iterate_upto f n m)"
+
 definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
 where
   "not_randompred P = (\<lambda>s. let
@@ -199,9 +203,9 @@
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
   where "map f P = bind P (single o f)"
 
-hide (open) fact iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def
+hide (open) fact iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
 hide (open) type randompred
 hide (open) const random collapse beyond random_fun_aux random_fun_lift
-  iter' iter empty single bind union if_randompred not_randompred Random map
+  iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
 
 end

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 31 16:44:41 2010 +0200
@@ -67,6 +67,7 @@
     mk_bind : term * term -> term,
     mk_sup : term * term -> term,
     mk_if : term -> term,
+    mk_iterate_upto : typ -> term * term * term -> term,
     mk_not : term -> term,
     mk_map : typ -> typ -> term -> term -> term
   };
@@ -77,6 +78,7 @@
   val mk_bind : compilation_funs -> term * term -> term
   val mk_sup : compilation_funs -> term * term -> term
   val mk_if : compilation_funs -> term -> term
+  val mk_iterate_upto : compilation_funs -> typ -> term * term * term -> term
   val mk_not : compilation_funs -> term -> term
   val mk_map : compilation_funs -> typ -> typ -> term -> term -> term
   val funT_of : compilation_funs -> mode -> typ -> typ
@@ -605,6 +607,7 @@
   mk_bind : term * term -> term,
   mk_sup : term * term -> term,
   mk_if : term -> term,
+  mk_iterate_upto : typ -> term * term * term -> term,
   mk_not : term -> term,
   mk_map : typ -> typ -> term -> term -> term
 };
@@ -616,6 +619,7 @@
 fun mk_bind (CompilationFuns funs) = #mk_bind funs
 fun mk_sup (CompilationFuns funs) = #mk_sup funs
 fun mk_if (CompilationFuns funs) = #mk_if funs
+fun mk_iterate_upto (CompilationFuns funs) = #mk_iterate_upto funs
 fun mk_not (CompilationFuns funs) = #mk_not funs
 fun mk_map (CompilationFuns funs) = #mk_map funs
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Wed Mar 31 16:44:41 2010 +0200
@@ -29,6 +29,11 @@
 fun mk_if cond = Const (@{const_name Predicate.if_pred},
   HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
 
+fun mk_iterate_upto T (f, from, to) =
+  list_comb (Const (@{const_name Code_Numeral.iterate_upto},
+      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_predT T),
+    [f, from, to])
+
 fun mk_not t =
   let
     val T = mk_predT HOLogic.unitT
@@ -54,8 +59,8 @@
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
-    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
-    mk_map = mk_map};
+    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
 
 end;
 
@@ -90,6 +95,11 @@
 fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
   HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
 
+fun mk_iterate_upto T (f, from, to) =
+  list_comb (Const (@{const_name Quickcheck.iterate_upto},
+      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_randompredT T),
+    [f, from, to])
+
 fun mk_not t =
   let
     val T = mk_randompredT HOLogic.unitT
@@ -101,7 +111,7 @@
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
     mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
-    mk_not = mk_not, mk_map = mk_map};
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
 
 end;
 
@@ -132,6 +142,8 @@
 fun mk_if cond = Const (@{const_name DSequence.if_seq},
   HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
 
+fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+
 fun mk_not t = let val T = mk_dseqT HOLogic.unitT
   in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
 
@@ -141,7 +153,7 @@
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
     mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
-    mk_not = mk_not, mk_map = mk_map}
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 end;
 
@@ -176,6 +188,12 @@
 fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
   HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
 
+fun mk_iterate_upto T (f, from, to) =
+  list_comb (Const (@{const_name New_Random_Sequence.pos_iterate_upto},
+      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
+        ---> mk_pos_random_dseqT T),
+    [f, from, to])
+
 fun mk_not t =
   let
     val pT = mk_pos_random_dseqT HOLogic.unitT
@@ -191,7 +209,7 @@
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
     mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
-    mk_not = mk_not, mk_map = mk_map}
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 end;
 
@@ -228,6 +246,12 @@
 fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
   HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
 
+fun mk_iterate_upto T (f, from, to) =
+  list_comb (Const (@{const_name New_Random_Sequence.neg_iterate_upto},
+      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
+        ---> mk_neg_random_dseqT T),
+    [f, from, to])
+
 fun mk_not t =
   let
     val nT = mk_neg_random_dseqT HOLogic.unitT
@@ -241,7 +265,7 @@
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
     mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
-    mk_not = mk_not, mk_map = mk_map}
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 end;
 
@@ -276,6 +300,8 @@
 fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
   HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
 
+fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+
 fun mk_not t =
   let
     val T = mk_random_dseqT HOLogic.unitT
@@ -287,7 +313,7 @@
 val compfuns = Predicate_Compile_Aux.CompilationFuns
     {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
     mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
-    mk_not = mk_not, mk_map = mk_map}
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 end;