src/HOL/Random_Pred.thy
changeset 51126 df86080de4cb
child 51143 0a2371e7ced3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Random_Pred.thy	Thu Feb 14 15:27:10 2013 +0100
     1.3 @@ -0,0 +1,76 @@
     1.4 +
     1.5 +(* Author: Lukas Bulwahn, TU Muenchen *)
     1.6 +
     1.7 +header {* The Random-Predicate Monad *}
     1.8 +
     1.9 +theory Random_Pred
    1.10 +imports Quickcheck_Random
    1.11 +begin
    1.12 +
    1.13 +fun iter' :: "'a itself \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
    1.14 +where
    1.15 +  "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
    1.16 +     let ((x, _), seed') = Quickcheck_Random.random sz seed
    1.17 +   in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
    1.18 +
    1.19 +definition iter :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
    1.20 +where
    1.21 +  "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
    1.22 +
    1.23 +lemma [code]:
    1.24 +  "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
    1.25 +     let ((x, _), seed') = Quickcheck_Random.random sz seed
    1.26 +   in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
    1.27 +   unfolding iter_def iter'.simps [of _ nrandom] ..
    1.28 +
    1.29 +type_synonym 'a random_pred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
    1.30 +
    1.31 +definition empty :: "'a random_pred"
    1.32 +  where "empty = Pair bot"
    1.33 +
    1.34 +definition single :: "'a => 'a random_pred"
    1.35 +  where "single x = Pair (Predicate.single x)"
    1.36 +
    1.37 +definition bind :: "'a random_pred \<Rightarrow> ('a \<Rightarrow> 'b random_pred) \<Rightarrow> 'b random_pred"
    1.38 +  where
    1.39 +    "bind R f = (\<lambda>s. let
    1.40 +       (P, s') = R s;
    1.41 +       (s1, s2) = Random.split_seed s'
    1.42 +     in (Predicate.bind P (%a. fst (f a s1)), s2))"
    1.43 +
    1.44 +definition union :: "'a random_pred \<Rightarrow> 'a random_pred \<Rightarrow> 'a random_pred"
    1.45 +where
    1.46 +  "union R1 R2 = (\<lambda>s. let
    1.47 +     (P1, s') = R1 s; (P2, s'') = R2 s'
    1.48 +   in (sup_class.sup P1 P2, s''))"
    1.49 +
    1.50 +definition if_randompred :: "bool \<Rightarrow> unit random_pred"
    1.51 +where
    1.52 +  "if_randompred b = (if b then single () else empty)"
    1.53 +
    1.54 +definition iterate_upto :: "(code_numeral \<Rightarrow> 'a) => code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a random_pred"
    1.55 +where
    1.56 +  "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
    1.57 +
    1.58 +definition not_randompred :: "unit random_pred \<Rightarrow> unit random_pred"
    1.59 +where
    1.60 +  "not_randompred P = (\<lambda>s. let
    1.61 +     (P', s') = P s
    1.62 +   in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
    1.63 +
    1.64 +definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a random_pred"
    1.65 +  where "Random g = scomp g (Pair o (Predicate.single o fst))"
    1.66 +
    1.67 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a random_pred \<Rightarrow> 'b random_pred"
    1.68 +  where "map f P = bind P (single o f)"
    1.69 +
    1.70 +hide_const (open) iter' iter empty single bind union if_randompred
    1.71 +  iterate_upto not_randompred Random map
    1.72 +
    1.73 +hide_fact iter'.simps
    1.74 +  
    1.75 +hide_fact (open) iter_def empty_def single_def bind_def union_def
    1.76 +  if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 
    1.77 +
    1.78 +end
    1.79 +