src/HOL/Quickcheck.thy
changeset 36049 0ce5b7a5c2fd
parent 35880 2623b23e41fc
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/Quickcheck.thy	Wed Mar 31 16:44:41 2010 +0200
     1.2 +++ b/src/HOL/Quickcheck.thy	Wed Mar 31 16:44:41 2010 +0200
     1.3 @@ -187,6 +187,10 @@
     1.4  where
     1.5    "if_randompred b = (if b then single () else empty)"
     1.6  
     1.7 +definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
     1.8 +where
     1.9 +  "iterate_upto f n m = Pair (Code_Numeral.iterate_upto f n m)"
    1.10 +
    1.11  definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
    1.12  where
    1.13    "not_randompred P = (\<lambda>s. let
    1.14 @@ -199,9 +203,9 @@
    1.15  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
    1.16    where "map f P = bind P (single o f)"
    1.17  
    1.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
    1.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
    1.20  hide (open) type randompred
    1.21  hide (open) const random collapse beyond random_fun_aux random_fun_lift
    1.22 -  iter' iter empty single bind union if_randompred not_randompred Random map
    1.23 +  iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
    1.24  
    1.25  end