|
(* Author: Lukas Bulwahn, TU Muenchen *)
section \<open>The Random-Predicate Monad\<close>
theory Random_Pred
imports Quickcheck_Random
begin
fun iter' :: "'a itself \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
where
"iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
let ((x, _), seed') = Quickcheck_Random.random sz seed
in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
definition iter :: "natural \ natural \ Random.seed \ ('a::random) Predicate.pred"
where
"iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
lemma [code]:
"iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
let ((x, _), seed') = Quickcheck_Random.random sz seed
in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
unfolding iter_def iter'.simps [of _ nrandom] ..
type_synonym 'a random_pred = "Random.seed \ ('a Predicate.pred \ Random.seed)"
definition empty :: "'a random_pred"
where "empty = Pair bot"
definition single :: "'a => 'a random_pred"
where "single x = Pair (Predicate.single x)"
definition bind :: "'a random_pred \ ('a \ 'b random_pred) \ 'b random_pred"
where
"bind R f = (\s. let
(P, s') = R s;
(s1, s2) = Random.split_seed s'
in (Predicate.bind P (%a. fst (f a s1)), s2))"
definition union :: "'a random_pred \ 'a random_pred \ 'a random_pred"
where
"union R1 R2 = (\s. let
(P1, s') = R1 s; (P2, s'') = R2 s'
in (sup_class.sup P1 P2, s''))"
definition if_randompred :: "bool \ unit random_pred"
where
"if_randompred b = (if b then single () else empty)"
definition iterate_upto :: "(natural \ 'a) => natural \ natural \ 'a random_pred"
where
"iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
definition not_randompred :: "unit random_pred \ unit random_pred"
where
"not_randompred P = (\s. let
(P', s') = P s
in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
definition Random :: "(Random.seed \ ('a \ (unit \ term)) \ Random.seed) \ 'a random_pred"
where "Random g = scomp g (Pair \ (Predicate.single \ fst))"
definition map :: "('a \ 'b) \ 'a random_pred \ 'b random_pred"
where "map f P = bind P (single \ f)"
hide_const (open) iter' iter empty single bind union if_randompred
iterate_upto not_randompred Random map
hide_fact iter'.simps
hide_fact (open) iter_def empty_def single_def bind_def union_def
if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
end
¤ Dauer der Verarbeitung: 0.28 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
