equal
deleted
inserted
replaced
25 "pos_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))" |
25 "pos_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))" |
26 |
26 |
27 definition pos_if_random_dseq :: "bool => unit pos_random_dseq" |
27 definition pos_if_random_dseq :: "bool => unit pos_random_dseq" |
28 where |
28 where |
29 "pos_if_random_dseq b = (if b then pos_single () else pos_empty)" |
29 "pos_if_random_dseq b = (if b then pos_single () else pos_empty)" |
|
30 |
|
31 definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_random_dseq" |
|
32 where |
|
33 "pos_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.pos_iterate_upto f n m)" |
30 |
34 |
31 definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq" |
35 definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq" |
32 where |
36 where |
33 "pos_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.pos_not_seq (R nrandom size seed))" |
37 "pos_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.pos_not_seq (R nrandom size seed))" |
34 |
38 |
64 |
68 |
65 definition neg_if_random_dseq :: "bool => unit neg_random_dseq" |
69 definition neg_if_random_dseq :: "bool => unit neg_random_dseq" |
66 where |
70 where |
67 "neg_if_random_dseq b = (if b then neg_single () else neg_empty)" |
71 "neg_if_random_dseq b = (if b then neg_single () else neg_empty)" |
68 |
72 |
|
73 definition neg_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a neg_random_dseq" |
|
74 where |
|
75 "neg_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.neg_iterate_upto f n m)" |
|
76 |
69 definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq" |
77 definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq" |
70 where |
78 where |
71 "neg_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.neg_not_seq (R nrandom size seed))" |
79 "neg_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.neg_not_seq (R nrandom size seed))" |
72 (* |
80 (* |
73 fun iter :: "(code_numeral * code_numeral => ('a * (unit => term)) * code_numeral * code_numeral) => code_numeral => code_numeral * code_numeral => 'a Lazy_Sequence.lazy_sequence" |
81 fun iter :: "(code_numeral * code_numeral => ('a * (unit => term)) * code_numeral * code_numeral) => code_numeral => code_numeral * code_numeral => 'a Lazy_Sequence.lazy_sequence" |
86 hide const DSequence.empty DSequence.single DSequence.eval |
94 hide const DSequence.empty DSequence.single DSequence.eval |
87 DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq |
95 DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq |
88 DSequence.map |
96 DSequence.map |
89 *) |
97 *) |
90 |
98 |
91 hide (open) const pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_not_random_dseq iter Random pos_map |
99 hide (open) const |
92 neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_not_random_dseq neg_map |
100 pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map |
|
101 neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map |
93 hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq |
102 hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq |
94 (* FIXME: hide facts *) |
103 (* FIXME: hide facts *) |
95 (*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*) |
104 (*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*) |
96 |
105 |
97 end |
106 end |