# 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 \<Rightarrow> ('a Predicate.pred \<times> 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 \<Rightarrow> ('a \<Rightarrow> 'b rpred) \<Rightarrow> 'b rpred"
-(* (infixl "\<guillemotright>=" 60) *)
-  where "bind RP f =
-  (\<lambda>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 \<Rightarrow> 'a rpred \<Rightarrow> 'a rpred"
-(* (infixl "\<squnion>" 80) *)
-where
-  "supp RP1 RP2 = (\<lambda>s. let (P1, s') = RP1 s; (P2, s'') = RP2 s'
-  in (sup_class.sup P1 P2, s''))"
-
-definition if_rpred :: "bool \<Rightarrow> 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 \<Rightarrow> unit rpred"
-where
-  "not_rpred P = (\<lambda>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 \<Rightarrow> 'a rpred"
-  where
-  "lift_pred = Pair"
-
-definition lift_random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a rpred"
-  where "lift_random g = scomp g (Pair o (Predicate.single o fst))"
-
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> '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