author | nipkow |
Mon, 30 May 2022 20:58:45 +0200 | |
changeset 75496 | 99b37c391433 |
parent 67091 | 1393c2340eec |
permissions | -rw-r--r-- |
51126 | 1 |
|
2 |
(* Author: Lukas Bulwahn, TU Muenchen *) |
|
3 |
||
60758 | 4 |
section \<open>The Random-Predicate Monad\<close> |
51126 | 5 |
|
6 |
theory Random_Pred |
|
7 |
imports Quickcheck_Random |
|
8 |
begin |
|
9 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
10 |
fun iter' :: "'a itself \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred" |
51126 | 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 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
16 |
definition iter :: "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred" |
51126 | 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 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
51 |
definition iterate_upto :: "(natural \<Rightarrow> 'a) => natural \<Rightarrow> natural \<Rightarrow> 'a random_pred" |
51126 | 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" |
|
67091 | 62 |
where "Random g = scomp g (Pair \<circ> (Predicate.single \<circ> fst))" |
51126 | 63 |
|
64 |
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a random_pred \<Rightarrow> 'b random_pred" |
|
67091 | 65 |
where "map f P = bind P (single \<circ> f)" |
51126 | 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 |