src/HOL/ex/RPred.thy
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 42463 f270e3e18be5
child 44845 5e51075cbd97
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
bulwahn@32308
     1
theory RPred
bulwahn@32308
     2
imports Quickcheck Random Predicate
bulwahn@32308
     3
begin
bulwahn@32308
     4
wenzelm@42463
     5
type_synonym 'a "rpred" = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
bulwahn@32308
     6
bulwahn@32308
     7
section {* The RandomPred Monad *}
bulwahn@32308
     8
bulwahn@32308
     9
text {* A monad to combine the random state monad and the predicate monad *}
bulwahn@32308
    10
bulwahn@32308
    11
definition bot :: "'a rpred"
bulwahn@32308
    12
  where "bot = Pair (bot_class.bot)"
bulwahn@32308
    13
bulwahn@32308
    14
definition return :: "'a => 'a rpred"
bulwahn@32308
    15
  where "return x = Pair (Predicate.single x)"
bulwahn@32308
    16
bulwahn@32662
    17
definition bind :: "'a rpred \<Rightarrow> ('a \<Rightarrow> 'b rpred) \<Rightarrow> 'b rpred"
bulwahn@32662
    18
(* (infixl "\<guillemotright>=" 60) *)
bulwahn@32308
    19
  where "bind RP f =
bulwahn@32308
    20
  (\<lambda>s. let (P, s') = RP s;
bulwahn@32308
    21
        (s1, s2) = Random.split_seed s'
bulwahn@32308
    22
    in (Predicate.bind P (%a. fst (f a s1)), s2))"
bulwahn@32308
    23
bulwahn@32662
    24
definition supp :: "'a rpred \<Rightarrow> 'a rpred \<Rightarrow> 'a rpred"
bulwahn@32662
    25
(* (infixl "\<squnion>" 80) *)
bulwahn@32308
    26
where
bulwahn@32308
    27
  "supp RP1 RP2 = (\<lambda>s. let (P1, s') = RP1 s; (P2, s'') = RP2 s'
haftmann@35028
    28
  in (semilattice_sup_class.sup P1 P2, s''))"
bulwahn@32308
    29
bulwahn@32308
    30
definition if_rpred :: "bool \<Rightarrow> unit rpred"
bulwahn@32308
    31
where
bulwahn@32308
    32
  "if_rpred b = (if b then return () else bot)"
bulwahn@32308
    33
bulwahn@32308
    34
(* Missing a good definition for negation: not_rpred *)
bulwahn@32308
    35
bulwahn@33138
    36
definition not_rpred :: "unit rpred \<Rightarrow> unit rpred"
bulwahn@32308
    37
where
bulwahn@33138
    38
  "not_rpred P = (\<lambda>s. let (P', s') = P s in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
bulwahn@32308
    39
bulwahn@32308
    40
definition lift_pred :: "'a Predicate.pred \<Rightarrow> 'a rpred"
bulwahn@32308
    41
  where
bulwahn@32308
    42
  "lift_pred = Pair"
bulwahn@32308
    43
bulwahn@32311
    44
definition lift_random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a rpred"
bulwahn@32311
    45
  where "lift_random g = scomp g (Pair o (Predicate.single o fst))"
bulwahn@32308
    46
bulwahn@33137
    47
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
bulwahn@33142
    48
  where "map f P = bind P (return o f)"
bulwahn@32662
    49
wenzelm@36176
    50
hide_const (open) return bind supp map
bulwahn@32308
    51
  
bulwahn@32308
    52
end