author | boehmes |
Mon, 17 Aug 2009 10:59:12 +0200 | |
changeset 32381 | 11542bebe4d4 |
parent 32311 | 50f953140636 |
child 32662 | 2faf1148c062 |
permissions | -rw-r--r-- |
32308
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
1 |
theory RPred |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
2 |
imports Quickcheck Random Predicate |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
3 |
begin |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
4 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
5 |
types 'a rpred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
6 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
7 |
section {* The RandomPred Monad *} |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
8 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
9 |
text {* A monad to combine the random state monad and the predicate monad *} |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
10 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
11 |
definition bot :: "'a rpred" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
12 |
where "bot = Pair (bot_class.bot)" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
13 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
14 |
definition return :: "'a => 'a rpred" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
15 |
where "return x = Pair (Predicate.single x)" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
16 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
17 |
definition bind :: "'a rpred \<Rightarrow> ('a \<Rightarrow> 'b rpred) \<Rightarrow> 'b rpred" (infixl "\<guillemotright>=" 60) |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
18 |
where "bind RP f = |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
19 |
(\<lambda>s. let (P, s') = RP s; |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
20 |
(s1, s2) = Random.split_seed s' |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
21 |
in (Predicate.bind P (%a. fst (f a s1)), s2))" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
22 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
23 |
definition supp :: "'a rpred \<Rightarrow> 'a rpred \<Rightarrow> 'a rpred" (infixl "\<squnion>" 80) |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
24 |
where |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
25 |
"supp RP1 RP2 = (\<lambda>s. let (P1, s') = RP1 s; (P2, s'') = RP2 s' |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
26 |
in (upper_semilattice_class.sup P1 P2, s''))" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
27 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
28 |
definition if_rpred :: "bool \<Rightarrow> unit rpred" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
29 |
where |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
30 |
"if_rpred b = (if b then return () else bot)" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
31 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
32 |
(* Missing a good definition for negation: not_rpred *) |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
33 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
34 |
definition not_rpred :: "unit Predicate.pred \<Rightarrow> unit rpred" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
35 |
where |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
36 |
"not_rpred = Pair o Predicate.not_pred" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
37 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
38 |
definition lift_pred :: "'a Predicate.pred \<Rightarrow> 'a rpred" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
39 |
where |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
40 |
"lift_pred = Pair" |
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
41 |
|
32311
50f953140636
adapted predicate compiler for quickcheck generators; added compilation of depth-limited search functions for predicates
bulwahn
parents:
32308
diff
changeset
|
42 |
definition lift_random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a rpred" |
50f953140636
adapted predicate compiler for quickcheck generators; added compilation of depth-limited search functions for predicates
bulwahn
parents:
32308
diff
changeset
|
43 |
where "lift_random g = scomp g (Pair o (Predicate.single o fst))" |
32308
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
44 |
|
32311
50f953140636
adapted predicate compiler for quickcheck generators; added compilation of depth-limited search functions for predicates
bulwahn
parents:
32308
diff
changeset
|
45 |
definition map_rpred :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)" |
50f953140636
adapted predicate compiler for quickcheck generators; added compilation of depth-limited search functions for predicates
bulwahn
parents:
32308
diff
changeset
|
46 |
where "map_rpred f P = P \<guillemotright>= (return o f)" |
32308
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
47 |
|
c2b74affab85
imported patch generic compilation of predicate compiler with different monads
bulwahn
parents:
diff
changeset
|
48 |
end |