author  haftmann 
Fri, 15 Feb 2013 08:31:31 +0100  
changeset 51143  0a2371e7ced3 
parent 51126  df86080de4cb 
child 58889  5b7a9633cfa8 
permissions  rwrr 
51126  1 

2 
(* Author: Lukas Bulwahn, TU Muenchen *) 

3 

4 
header {* The RandomPredicate Monad *} 

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" 

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 