src/HOL/Random_Pred.thy
 changeset 51143 0a2371e7ced3 parent 51126 df86080de4cb child 58889 5b7a9633cfa8
equal 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`