src/HOL/Random_Pred.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (19 months ago) changeset 67022 49309fe530fd parent 60758 d8d85a8172b5 child 67091 1393c2340eec permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
```     1
```
```     2 (* Author: Lukas Bulwahn, TU Muenchen *)
```
```     3
```
```     4 section \<open>The Random-Predicate Monad\<close>
```
```     5
```
```     6 theory Random_Pred
```
```     7 imports Quickcheck_Random
```
```     8 begin
```
```     9
```
```    10 fun iter' :: "'a itself \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
```
```    11 where
```
```    12   "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
```
```    13      let ((x, _), seed') = Quickcheck_Random.random sz seed
```
```    14    in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
```
```    15
```
```    16 definition iter :: "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
```
```    17 where
```
```    18   "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
```
```    19
```
```    20 lemma [code]:
```
```    21   "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
```
```    22      let ((x, _), seed') = Quickcheck_Random.random sz seed
```
```    23    in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
```
```    24    unfolding iter_def iter'.simps [of _ nrandom] ..
```
```    25
```
```    26 type_synonym 'a random_pred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
```
```    27
```
```    28 definition empty :: "'a random_pred"
```
```    29   where "empty = Pair bot"
```
```    30
```
```    31 definition single :: "'a => 'a random_pred"
```
```    32   where "single x = Pair (Predicate.single x)"
```
```    33
```
```    34 definition bind :: "'a random_pred \<Rightarrow> ('a \<Rightarrow> 'b random_pred) \<Rightarrow> 'b random_pred"
```
```    35   where
```
```    36     "bind R f = (\<lambda>s. let
```
```    37        (P, s') = R s;
```
```    38        (s1, s2) = Random.split_seed s'
```
```    39      in (Predicate.bind P (%a. fst (f a s1)), s2))"
```
```    40
```
```    41 definition union :: "'a random_pred \<Rightarrow> 'a random_pred \<Rightarrow> 'a random_pred"
```
```    42 where
```
```    43   "union R1 R2 = (\<lambda>s. let
```
```    44      (P1, s') = R1 s; (P2, s'') = R2 s'
```
```    45    in (sup_class.sup P1 P2, s''))"
```
```    46
```
```    47 definition if_randompred :: "bool \<Rightarrow> unit random_pred"
```
```    48 where
```
```    49   "if_randompred b = (if b then single () else empty)"
```
```    50
```
```    51 definition iterate_upto :: "(natural \<Rightarrow> 'a) => natural \<Rightarrow> natural \<Rightarrow> 'a random_pred"
```
```    52 where
```
```    53   "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
```
```    54
```
```    55 definition not_randompred :: "unit random_pred \<Rightarrow> unit random_pred"
```
```    56 where
```
```    57   "not_randompred P = (\<lambda>s. let
```
```    58      (P', s') = P s
```
```    59    in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
```
```    60
```
```    61 definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a random_pred"
```
```    62   where "Random g = scomp g (Pair o (Predicate.single o fst))"
```
```    63
```
```    64 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a random_pred \<Rightarrow> 'b random_pred"
```
```    65   where "map f P = bind P (single o f)"
```
```    66
```
```    67 hide_const (open) iter' iter empty single bind union if_randompred
```
```    68   iterate_upto not_randompred Random map
```
```    69
```
```    70 hide_fact iter'.simps
```
```    71
```
```    72 hide_fact (open) iter_def empty_def single_def bind_def union_def
```
```    73   if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
```
```    74
```
```    75 end
```
```    76
```