adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
authorbulwahn
Wed Mar 31 16:44:41 2010 +0200 (2010-03-31)
changeset 360490ce5b7a5c2fd
parent 36048 1d2faa488166
child 36050 88203782cf12
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
src/HOL/Code_Numeral.thy
src/HOL/Lazy_Sequence.thy
src/HOL/New_DSequence.thy
src/HOL/New_Random_Sequence.thy
src/HOL/Quickcheck.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
     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  
     2.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Mar 31 16:44:41 2010 +0200
     2.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Mar 31 16:44:41 2010 +0200
     2.3 @@ -110,6 +110,13 @@
     2.4  where
     2.5    "if_seq b = (if b then single () else empty)"
     2.6  
     2.7 +function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence"
     2.8 +where
     2.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))"
    2.10 +by pat_completeness auto
    2.11 +
    2.12 +termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
    2.13 +
    2.14  definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
    2.15  where
    2.16    "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
    2.17 @@ -206,7 +213,7 @@
    2.18    "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
    2.19  
    2.20  hide (open) type lazy_sequence
    2.21 -hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
    2.22 -hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
    2.23 +hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
    2.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
    2.25  
    2.26  end
     3.1 --- a/src/HOL/New_DSequence.thy	Wed Mar 31 16:44:41 2010 +0200
     3.2 +++ b/src/HOL/New_DSequence.thy	Wed Mar 31 16:44:41 2010 +0200
     3.3 @@ -35,6 +35,10 @@
     3.4  where
     3.5    "pos_if_seq b = (if b then pos_single () else pos_empty)"
     3.6  
     3.7 +definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_dseq"
     3.8 +where
     3.9 +  "pos_iterate_upto f n m = (%i. Lazy_Sequence.iterate_upto f n m)"
    3.10 + 
    3.11  definition pos_map :: "('a => 'b) => 'a pos_dseq => 'b pos_dseq"
    3.12  where
    3.13    "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
    3.14 @@ -67,6 +71,10 @@
    3.15  where
    3.16    "neg_if_seq b = (if b then neg_single () else neg_empty)"
    3.17  
    3.18 +definition neg_iterate_upto 
    3.19 +where
    3.20 +  "neg_iterate_upto f n m = (%i. Lazy_Sequence.iterate_upto (%i. Some (f i)) n m)"
    3.21 +
    3.22  definition neg_map :: "('a => 'b) => 'a neg_dseq => 'b neg_dseq"
    3.23  where
    3.24    "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
    3.25 @@ -86,10 +94,10 @@
    3.26  hide (open) type pos_dseq neg_dseq
    3.27  
    3.28  hide (open) const 
    3.29 -  pos_empty pos_single pos_bind pos_union pos_if_seq pos_not_seq
    3.30 -  neg_empty neg_single neg_bind neg_union neg_if_seq neg_not_seq
    3.31 +  pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
    3.32 +  neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
    3.33  hide (open) fact
    3.34 -  pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_not_seq_def pos_map_def
    3.35 -  neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_not_seq_def neg_map_def
    3.36 +  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
    3.37 +  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
    3.38  
    3.39  end
     4.1 --- a/src/HOL/New_Random_Sequence.thy	Wed Mar 31 16:44:41 2010 +0200
     4.2 +++ b/src/HOL/New_Random_Sequence.thy	Wed Mar 31 16:44:41 2010 +0200
     4.3 @@ -28,6 +28,10 @@
     4.4  where
     4.5    "pos_if_random_dseq b = (if b then pos_single () else pos_empty)"
     4.6  
     4.7 +definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_random_dseq"
     4.8 +where
     4.9 +  "pos_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.pos_iterate_upto f n m)"
    4.10 +
    4.11  definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq"
    4.12  where
    4.13    "pos_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.pos_not_seq (R nrandom size seed))"
    4.14 @@ -66,6 +70,10 @@
    4.15  where
    4.16    "neg_if_random_dseq b = (if b then neg_single () else neg_empty)"
    4.17  
    4.18 +definition neg_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a neg_random_dseq"
    4.19 +where
    4.20 +  "neg_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.neg_iterate_upto f n m)"
    4.21 +
    4.22  definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq"
    4.23  where
    4.24    "neg_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.neg_not_seq (R nrandom size seed))"
    4.25 @@ -88,8 +96,9 @@
    4.26    DSequence.map
    4.27  *)
    4.28  
    4.29 -hide (open) const pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_not_random_dseq iter Random pos_map
    4.30 -  neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_not_random_dseq neg_map
    4.31 +hide (open) const
    4.32 +  pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
    4.33 +  neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
    4.34  hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
    4.35  (* FIXME: hide facts *)
    4.36  (*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
     5.1 --- a/src/HOL/Quickcheck.thy	Wed Mar 31 16:44:41 2010 +0200
     5.2 +++ b/src/HOL/Quickcheck.thy	Wed Mar 31 16:44:41 2010 +0200
     5.3 @@ -187,6 +187,10 @@
     5.4  where
     5.5    "if_randompred b = (if b then single () else empty)"
     5.6  
     5.7 +definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
     5.8 +where
     5.9 +  "iterate_upto f n m = Pair (Code_Numeral.iterate_upto f n m)"
    5.10 +
    5.11  definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
    5.12  where
    5.13    "not_randompred P = (\<lambda>s. let
    5.14 @@ -199,9 +203,9 @@
    5.15  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
    5.16    where "map f P = bind P (single o f)"
    5.17  
    5.18 -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
    5.19 +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
    5.20  hide (open) type randompred
    5.21  hide (open) const random collapse beyond random_fun_aux random_fun_lift
    5.22 -  iter' iter empty single bind union if_randompred not_randompred Random map
    5.23 +  iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
    5.24  
    5.25  end
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 31 16:44:41 2010 +0200
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 31 16:44:41 2010 +0200
     6.3 @@ -67,6 +67,7 @@
     6.4      mk_bind : term * term -> term,
     6.5      mk_sup : term * term -> term,
     6.6      mk_if : term -> term,
     6.7 +    mk_iterate_upto : typ -> term * term * term -> term,
     6.8      mk_not : term -> term,
     6.9      mk_map : typ -> typ -> term -> term -> term
    6.10    };
    6.11 @@ -77,6 +78,7 @@
    6.12    val mk_bind : compilation_funs -> term * term -> term
    6.13    val mk_sup : compilation_funs -> term * term -> term
    6.14    val mk_if : compilation_funs -> term -> term
    6.15 +  val mk_iterate_upto : compilation_funs -> typ -> term * term * term -> term
    6.16    val mk_not : compilation_funs -> term -> term
    6.17    val mk_map : compilation_funs -> typ -> typ -> term -> term -> term
    6.18    val funT_of : compilation_funs -> mode -> typ -> typ
    6.19 @@ -605,6 +607,7 @@
    6.20    mk_bind : term * term -> term,
    6.21    mk_sup : term * term -> term,
    6.22    mk_if : term -> term,
    6.23 +  mk_iterate_upto : typ -> term * term * term -> term,
    6.24    mk_not : term -> term,
    6.25    mk_map : typ -> typ -> term -> term -> term
    6.26  };
    6.27 @@ -616,6 +619,7 @@
    6.28  fun mk_bind (CompilationFuns funs) = #mk_bind funs
    6.29  fun mk_sup (CompilationFuns funs) = #mk_sup funs
    6.30  fun mk_if (CompilationFuns funs) = #mk_if funs
    6.31 +fun mk_iterate_upto (CompilationFuns funs) = #mk_iterate_upto funs
    6.32  fun mk_not (CompilationFuns funs) = #mk_not funs
    6.33  fun mk_map (CompilationFuns funs) = #mk_map funs
    6.34  
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Wed Mar 31 16:44:41 2010 +0200
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Wed Mar 31 16:44:41 2010 +0200
     7.3 @@ -29,6 +29,11 @@
     7.4  fun mk_if cond = Const (@{const_name Predicate.if_pred},
     7.5    HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
     7.6  
     7.7 +fun mk_iterate_upto T (f, from, to) =
     7.8 +  list_comb (Const (@{const_name Code_Numeral.iterate_upto},
     7.9 +      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_predT T),
    7.10 +    [f, from, to])
    7.11 +
    7.12  fun mk_not t =
    7.13    let
    7.14      val T = mk_predT HOLogic.unitT
    7.15 @@ -54,8 +59,8 @@
    7.16  
    7.17  val compfuns = Predicate_Compile_Aux.CompilationFuns
    7.18      {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
    7.19 -    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
    7.20 -    mk_map = mk_map};
    7.21 +    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
    7.22 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
    7.23  
    7.24  end;
    7.25  
    7.26 @@ -90,6 +95,11 @@
    7.27  fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
    7.28    HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
    7.29  
    7.30 +fun mk_iterate_upto T (f, from, to) =
    7.31 +  list_comb (Const (@{const_name Quickcheck.iterate_upto},
    7.32 +      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_randompredT T),
    7.33 +    [f, from, to])
    7.34 +
    7.35  fun mk_not t =
    7.36    let
    7.37      val T = mk_randompredT HOLogic.unitT
    7.38 @@ -101,7 +111,7 @@
    7.39  val compfuns = Predicate_Compile_Aux.CompilationFuns
    7.40      {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
    7.41      mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
    7.42 -    mk_not = mk_not, mk_map = mk_map};
    7.43 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
    7.44  
    7.45  end;
    7.46  
    7.47 @@ -132,6 +142,8 @@
    7.48  fun mk_if cond = Const (@{const_name DSequence.if_seq},
    7.49    HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
    7.50  
    7.51 +fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
    7.52 +
    7.53  fun mk_not t = let val T = mk_dseqT HOLogic.unitT
    7.54    in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
    7.55  
    7.56 @@ -141,7 +153,7 @@
    7.57  val compfuns = Predicate_Compile_Aux.CompilationFuns
    7.58      {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
    7.59      mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
    7.60 -    mk_not = mk_not, mk_map = mk_map}
    7.61 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
    7.62  
    7.63  end;
    7.64  
    7.65 @@ -176,6 +188,12 @@
    7.66  fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
    7.67    HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
    7.68  
    7.69 +fun mk_iterate_upto T (f, from, to) =
    7.70 +  list_comb (Const (@{const_name New_Random_Sequence.pos_iterate_upto},
    7.71 +      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
    7.72 +        ---> mk_pos_random_dseqT T),
    7.73 +    [f, from, to])
    7.74 +
    7.75  fun mk_not t =
    7.76    let
    7.77      val pT = mk_pos_random_dseqT HOLogic.unitT
    7.78 @@ -191,7 +209,7 @@
    7.79  val compfuns = Predicate_Compile_Aux.CompilationFuns
    7.80      {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
    7.81      mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
    7.82 -    mk_not = mk_not, mk_map = mk_map}
    7.83 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
    7.84  
    7.85  end;
    7.86  
    7.87 @@ -228,6 +246,12 @@
    7.88  fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
    7.89    HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
    7.90  
    7.91 +fun mk_iterate_upto T (f, from, to) =
    7.92 +  list_comb (Const (@{const_name New_Random_Sequence.neg_iterate_upto},
    7.93 +      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
    7.94 +        ---> mk_neg_random_dseqT T),
    7.95 +    [f, from, to])
    7.96 +
    7.97  fun mk_not t =
    7.98    let
    7.99      val nT = mk_neg_random_dseqT HOLogic.unitT
   7.100 @@ -241,7 +265,7 @@
   7.101  val compfuns = Predicate_Compile_Aux.CompilationFuns
   7.102      {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
   7.103      mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   7.104 -    mk_not = mk_not, mk_map = mk_map}
   7.105 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   7.106  
   7.107  end;
   7.108  
   7.109 @@ -276,6 +300,8 @@
   7.110  fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
   7.111    HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
   7.112  
   7.113 +fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
   7.114 +
   7.115  fun mk_not t =
   7.116    let
   7.117      val T = mk_random_dseqT HOLogic.unitT
   7.118 @@ -287,7 +313,7 @@
   7.119  val compfuns = Predicate_Compile_Aux.CompilationFuns
   7.120      {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
   7.121      mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   7.122 -    mk_not = mk_not, mk_map = mk_map}
   7.123 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   7.124  
   7.125  end;
   7.126