1 2(* Author: Lukas Bulwahn, TU Muenchen *) 3 4section \<open>The Random-Predicate Monad\<close> 5 6theory Random_Pred 7imports Quickcheck_Random 8begin 9 10fun iter' :: "'a itself \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred" 11where 12 "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else 13 let ((x, _), seed') = Quickcheck_Random.random sz seed 14 in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))" 15 16definition iter :: "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred" 17where 18 "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed" 19 20lemma [code]: 21 "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else 22 let ((x, _), seed') = Quickcheck_Random.random sz seed 23 in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))" 24 unfolding iter_def iter'.simps [of _ nrandom] .. 25 26type_synonym 'a random_pred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)" 27 28definition empty :: "'a random_pred" 29 where "empty = Pair bot" 30 31definition single :: "'a => 'a random_pred" 32 where "single x = Pair (Predicate.single x)" 33 34definition bind :: "'a random_pred \<Rightarrow> ('a \<Rightarrow> 'b random_pred) \<Rightarrow> 'b random_pred" 35 where 36 "bind R f = (\<lambda>s. let 37 (P, s') = R s; 38 (s1, s2) = Random.split_seed s' 39 in (Predicate.bind P (%a. fst (f a s1)), s2))" 40 41definition union :: "'a random_pred \<Rightarrow> 'a random_pred \<Rightarrow> 'a random_pred" 42where 43 "union R1 R2 = (\<lambda>s. let 44 (P1, s') = R1 s; (P2, s'') = R2 s' 45 in (sup_class.sup P1 P2, s''))" 46 47definition if_randompred :: "bool \<Rightarrow> unit random_pred" 48where 49 "if_randompred b = (if b then single () else empty)" 50 51definition iterate_upto :: "(natural \<Rightarrow> 'a) => natural \<Rightarrow> natural \<Rightarrow> 'a random_pred" 52where 53 "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)" 54 55definition not_randompred :: "unit random_pred \<Rightarrow> unit random_pred" 56where 57 "not_randompred P = (\<lambda>s. let 58 (P', s') = P s 59 in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))" 60 61definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a random_pred" 62 where "Random g = scomp g (Pair \<circ> (Predicate.single \<circ> fst))" 63 64definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a random_pred \<Rightarrow> 'b random_pred" 65 where "map f P = bind P (single \<circ> f)" 66 67hide_const (open) iter' iter empty single bind union if_randompred 68 iterate_upto not_randompred Random map 69 70hide_fact iter'.simps 71 72hide_fact (open) iter_def empty_def single_def bind_def union_def 73 if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 74 75end 76 77