author | wenzelm |
Fri, 05 Apr 2019 17:05:32 +0200 | |
changeset 70067 | 9b34dbeb1103 |
parent 67091 | 1393c2340eec |
permissions | -rw-r--r-- |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
1 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
2 |
(* Author: Lukas Bulwahn, TU Muenchen *) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
3 |
|
60758 | 4 |
section \<open>Various kind of sequences inside the random monad\<close> |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
5 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
6 |
theory Random_Sequence |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
7 |
imports Random_Pred |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
8 |
begin |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
9 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
10 |
type_synonym 'a random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a Limited_Sequence.dseq \<times> Random.seed)" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
11 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
12 |
definition empty :: "'a random_dseq" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
13 |
where |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
14 |
"empty = (%nrandom size. Pair (Limited_Sequence.empty))" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
15 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
16 |
definition single :: "'a => 'a random_dseq" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
17 |
where |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
18 |
"single x = (%nrandom size. Pair (Limited_Sequence.single x))" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
19 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
20 |
definition bind :: "'a random_dseq => ('a \<Rightarrow> 'b random_dseq) \<Rightarrow> 'b random_dseq" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
21 |
where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
22 |
"bind R f = (\<lambda>nrandom size s. let |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
23 |
(P, s') = R nrandom size s; |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
24 |
(s1, s2) = Random.split_seed s' |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
25 |
in (Limited_Sequence.bind P (%a. fst (f a nrandom size s1)), s2))" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
26 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
27 |
definition union :: "'a random_dseq => 'a random_dseq => 'a random_dseq" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
28 |
where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
29 |
"union R1 R2 = (\<lambda>nrandom size s. let |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
30 |
(S1, s') = R1 nrandom size s; (S2, s'') = R2 nrandom size s' |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
31 |
in (Limited_Sequence.union S1 S2, s''))" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
32 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
33 |
definition if_random_dseq :: "bool => unit random_dseq" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
34 |
where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
35 |
"if_random_dseq b = (if b then single () else empty)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
36 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
37 |
definition not_random_dseq :: "unit random_dseq => unit random_dseq" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
38 |
where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
39 |
"not_random_dseq R = (\<lambda>nrandom size s. let |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
40 |
(S, s') = R nrandom size s |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
41 |
in (Limited_Sequence.not_seq S, s'))" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
42 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
43 |
definition map :: "('a => 'b) => 'a random_dseq => 'b random_dseq" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
44 |
where |
67091 | 45 |
"map f P = bind P (single \<circ> f)" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
46 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
47 |
fun Random :: "(natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq" |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
48 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
49 |
"Random g nrandom = (%size. if nrandom <= 0 then (Pair Limited_Sequence.empty) else |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
50 |
(scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (Limited_Sequence.union (Limited_Sequence.single (fst r)) rs)))))" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
51 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
52 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
53 |
type_synonym 'a pos_random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.pos_dseq" |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
54 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
55 |
definition pos_empty :: "'a pos_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
56 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
57 |
"pos_empty = (%nrandom size seed. Limited_Sequence.pos_empty)" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
58 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
59 |
definition pos_single :: "'a => 'a pos_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
60 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
61 |
"pos_single x = (%nrandom size seed. Limited_Sequence.pos_single x)" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
62 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
63 |
definition pos_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
64 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
65 |
"pos_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
66 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
67 |
definition pos_decr_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
68 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
69 |
"pos_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
70 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
71 |
definition pos_union :: "'a pos_random_dseq => 'a pos_random_dseq => 'a pos_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
72 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
73 |
"pos_union R1 R2 = (\<lambda>nrandom size seed. Limited_Sequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
74 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
75 |
definition pos_if_random_dseq :: "bool => unit pos_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
76 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
77 |
"pos_if_random_dseq b = (if b then pos_single () else pos_empty)" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
78 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
79 |
definition pos_iterate_upto :: "(natural => 'a) => natural => natural => 'a pos_random_dseq" |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
80 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
81 |
"pos_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.pos_iterate_upto f n m)" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
82 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
83 |
definition pos_map :: "('a => 'b) => 'a pos_random_dseq => 'b pos_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
84 |
where |
67091 | 85 |
"pos_map f P = pos_bind P (pos_single \<circ> f)" |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
86 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
87 |
fun iter :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
88 |
\<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Lazy_Sequence.lazy_sequence" |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
89 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
90 |
"iter random nrandom seed = |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
91 |
(if nrandom = 0 then Lazy_Sequence.empty else Lazy_Sequence.Lazy_Sequence (%u. let ((x, _), seed') = random seed in Some (x, iter random (nrandom - 1) seed')))" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
92 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
93 |
definition pos_Random :: "(natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
94 |
\<Rightarrow> 'a pos_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
95 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
96 |
"pos_Random g = (%nrandom size seed depth. iter (g size) nrandom seed)" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
97 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
98 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
99 |
type_synonym 'a neg_random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.neg_dseq" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
100 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
101 |
definition neg_empty :: "'a neg_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
102 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
103 |
"neg_empty = (%nrandom size seed. Limited_Sequence.neg_empty)" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
104 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
105 |
definition neg_single :: "'a => 'a neg_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
106 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
107 |
"neg_single x = (%nrandom size seed. Limited_Sequence.neg_single x)" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
108 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
109 |
definition neg_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
110 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
111 |
"neg_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
112 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
113 |
definition neg_decr_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
114 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
115 |
"neg_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
116 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
117 |
definition neg_union :: "'a neg_random_dseq => 'a neg_random_dseq => 'a neg_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
118 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
119 |
"neg_union R1 R2 = (\<lambda>nrandom size seed. Limited_Sequence.neg_union (R1 nrandom size seed) (R2 nrandom size seed))" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
120 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
121 |
definition neg_if_random_dseq :: "bool => unit neg_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
122 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
123 |
"neg_if_random_dseq b = (if b then neg_single () else neg_empty)" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
124 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
125 |
definition neg_iterate_upto :: "(natural => 'a) => natural => natural => 'a neg_random_dseq" |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
126 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
127 |
"neg_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.neg_iterate_upto f n m)" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
128 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
129 |
definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
130 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
131 |
"neg_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.neg_not_seq (R nrandom size seed))" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
132 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
133 |
definition neg_map :: "('a => 'b) => 'a neg_random_dseq => 'b neg_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
134 |
where |
67091 | 135 |
"neg_map f P = neg_bind P (neg_single \<circ> f)" |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
136 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
137 |
definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
138 |
where |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
139 |
"pos_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.pos_not_seq (R nrandom size seed))" |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
140 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset
|
141 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
142 |
hide_const (open) |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
143 |
empty single bind union if_random_dseq not_random_dseq map Random |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
144 |
pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_random_dseq pos_iterate_upto |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
145 |
pos_not_random_dseq pos_map iter pos_Random |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
146 |
neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_random_dseq neg_iterate_upto |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
147 |
neg_not_random_dseq neg_map |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
148 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
149 |
hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
150 |
map_def Random.simps |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
151 |
pos_empty_def pos_single_def pos_bind_def pos_decr_bind_def pos_union_def pos_if_random_dseq_def |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
152 |
pos_iterate_upto_def pos_not_random_dseq_def pos_map_def iter.simps pos_Random_def |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
153 |
neg_empty_def neg_single_def neg_bind_def neg_decr_bind_def neg_union_def neg_if_random_dseq_def |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
154 |
neg_iterate_upto_def neg_not_random_dseq_def neg_map_def |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
155 |
|
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
156 |
end |
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
157 |