src/HOL/Random_Pred.thy
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 58889 5b7a9633cfa8
equal deleted inserted replaced
51142:ac9e909fe55d 51143:0a2371e7ced3
     5 
     5 
     6 theory Random_Pred
     6 theory Random_Pred
     7 imports Quickcheck_Random
     7 imports Quickcheck_Random
     8 begin
     8 begin
     9 
     9 
    10 fun iter' :: "'a itself \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
    10 fun iter' :: "'a itself \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
    11 where
    11 where
    12   "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
    12   "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
    13      let ((x, _), seed') = Quickcheck_Random.random sz seed
    13      let ((x, _), seed') = Quickcheck_Random.random sz seed
    14    in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
    14    in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
    15 
    15 
    16 definition iter :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
    16 definition iter :: "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
    17 where
    17 where
    18   "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
    18   "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
    19 
    19 
    20 lemma [code]:
    20 lemma [code]:
    21   "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
    21   "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
    46 
    46 
    47 definition if_randompred :: "bool \<Rightarrow> unit random_pred"
    47 definition if_randompred :: "bool \<Rightarrow> unit random_pred"
    48 where
    48 where
    49   "if_randompred b = (if b then single () else empty)"
    49   "if_randompred b = (if b then single () else empty)"
    50 
    50 
    51 definition iterate_upto :: "(code_numeral \<Rightarrow> 'a) => code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a random_pred"
    51 definition iterate_upto :: "(natural \<Rightarrow> 'a) => natural \<Rightarrow> natural \<Rightarrow> 'a random_pred"
    52 where
    52 where
    53   "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
    53   "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
    54 
    54 
    55 definition not_randompred :: "unit random_pred \<Rightarrow> unit random_pred"
    55 definition not_randompred :: "unit random_pred \<Rightarrow> unit random_pred"
    56 where
    56 where