# HG changeset patch # User noschinl # Date 1397474772 -7200 # Node ID 5b171d4e1d6e895e00fc8cc0bdd6cc7cbff4596b # Parent f4635657d66fac591c9df7c086f6d075b49f42e3 Removed old experiment (broken since b458b4ac570f resp 4159caa18f85) diff -r f4635657d66f -r 5b171d4e1d6e src/HOL/ex/RPred.thy --- a/src/HOL/ex/RPred.thy Mon Apr 14 13:08:17 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,52 +0,0 @@ -theory RPred -imports Quickcheck Random Predicate -begin - -type_synonym 'a "rpred" = "Random.seed \ ('a Predicate.pred \ Random.seed)" - -section {* The RandomPred Monad *} - -text {* A monad to combine the random state monad and the predicate monad *} - -definition bot :: "'a rpred" - where "bot = Pair (bot_class.bot)" - -definition return :: "'a => 'a rpred" - where "return x = Pair (Predicate.single x)" - -definition bind :: "'a rpred \ ('a \ 'b rpred) \ 'b rpred" -(* (infixl "\=" 60) *) - where "bind RP f = - (\s. let (P, s') = RP s; - (s1, s2) = Random.split_seed s' - in (Predicate.bind P (%a. fst (f a s1)), s2))" - -definition supp :: "'a rpred \ 'a rpred \ 'a rpred" -(* (infixl "\" 80) *) -where - "supp RP1 RP2 = (\s. let (P1, s') = RP1 s; (P2, s'') = RP2 s' - in (sup_class.sup P1 P2, s''))" - -definition if_rpred :: "bool \ unit rpred" -where - "if_rpred b = (if b then return () else bot)" - -(* Missing a good definition for negation: not_rpred *) - -definition not_rpred :: "unit rpred \ unit rpred" -where - "not_rpred P = (\s. let (P', s') = P s in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))" - -definition lift_pred :: "'a Predicate.pred \ 'a rpred" - where - "lift_pred = Pair" - -definition lift_random :: "(Random.seed \ ('a \ (unit \ term)) \ Random.seed) \ 'a rpred" - where "lift_random g = scomp g (Pair o (Predicate.single o fst))" - -definition map :: "('a \ 'b) \ ('a rpred \ 'b rpred)" - where "map f P = bind P (return o f)" - -hide_const (open) return bind supp map - -end \ No newline at end of file