src/HOL/Quickcheck.thy
changeset 33250 5c2af18a3237
parent 32657 5f13912245ff
child 33254 d0c00b81db1d
     1.1 --- a/src/HOL/Quickcheck.thy	Mon Oct 26 23:27:24 2009 +0100
     1.2 +++ b/src/HOL/Quickcheck.thy	Tue Oct 27 09:02:22 2009 +0100
     1.3 @@ -126,6 +126,47 @@
     1.4    shows "random_aux k = rhs k"
     1.5    using assms by (rule code_numeral.induct)
     1.6  
     1.7 +subsection {* the Random-Predicate Monad *} 
     1.8 +
     1.9 +types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
    1.10 +
    1.11 +definition empty :: "'a randompred"
    1.12 +  where "empty = Pair (bot_class.bot)"
    1.13 +
    1.14 +definition single :: "'a => 'a randompred"
    1.15 +  where "single x = Pair (Predicate.single x)"
    1.16 +
    1.17 +definition bind :: "'a randompred \<Rightarrow> ('a \<Rightarrow> 'b randompred) \<Rightarrow> 'b randompred"
    1.18 +  where
    1.19 +    "bind R f = (\<lambda>s. let
    1.20 +       (P, s') = R s;
    1.21 +       (s1, s2) = Random.split_seed s'
    1.22 +     in (Predicate.bind P (%a. fst (f a s1)), s2))"
    1.23 +
    1.24 +definition union :: "'a randompred \<Rightarrow> 'a randompred \<Rightarrow> 'a randompred"
    1.25 +where
    1.26 +  "union R1 R2 = (\<lambda>s. let
    1.27 +     (P1, s') = R1 s; (P2, s'') = R2 s'
    1.28 +   in (upper_semilattice_class.sup P1 P2, s''))"
    1.29 +
    1.30 +definition if_randompred :: "bool \<Rightarrow> unit randompred"
    1.31 +where
    1.32 +  "if_randompred b = (if b then single () else empty)"
    1.33 +
    1.34 +definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
    1.35 +where
    1.36 +  "not_randompred P = (\<lambda>s. let
    1.37 +     (P', s') = P s
    1.38 +   in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
    1.39 +
    1.40 +definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a randompred"
    1.41 +  where "Random g = scomp g (Pair o (Predicate.single o fst))"
    1.42 +
    1.43 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
    1.44 +  where "map f P = bind P (single o f)"
    1.45 +
    1.46 +subsection {* Code setup *}
    1.47 +
    1.48  use "Tools/quickcheck_generators.ML"
    1.49  setup {* Quickcheck_Generators.setup *}
    1.50  
    1.51 @@ -137,7 +178,9 @@
    1.52  code_reserved Quickcheck Quickcheck_Generators
    1.53  
    1.54  
    1.55 +hide (open) type randompred
    1.56  hide (open) const random collapse beyond random_fun_aux random_fun_lift
    1.57 +  empty single bind union if_randompred not_randompred Random map
    1.58  
    1.59  no_notation fcomp (infixl "o>" 60)
    1.60  no_notation scomp (infixl "o\<rightarrow>" 60)