src/HOL/Random_Pred.thy
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Random_Pred.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Random_Pred.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -7,13 +7,13 @@
     1.4  imports Quickcheck_Random
     1.5  begin
     1.6  
     1.7 -fun iter' :: "'a itself \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
     1.8 +fun iter' :: "'a itself \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
     1.9  where
    1.10    "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
    1.11       let ((x, _), seed') = Quickcheck_Random.random sz seed
    1.12     in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
    1.13  
    1.14 -definition iter :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
    1.15 +definition iter :: "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
    1.16  where
    1.17    "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
    1.18  
    1.19 @@ -48,7 +48,7 @@
    1.20  where
    1.21    "if_randompred b = (if b then single () else empty)"
    1.22  
    1.23 -definition iterate_upto :: "(code_numeral \<Rightarrow> 'a) => code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a random_pred"
    1.24 +definition iterate_upto :: "(natural \<Rightarrow> 'a) => natural \<Rightarrow> natural \<Rightarrow> 'a random_pred"
    1.25  where
    1.26    "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
    1.27