equal
deleted
inserted
replaced
19 where |
19 where |
20 "pos_single x = (%i. Lazy_Sequence.single x)" |
20 "pos_single x = (%i. Lazy_Sequence.single x)" |
21 |
21 |
22 definition pos_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq" |
22 definition pos_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq" |
23 where |
23 where |
24 "pos_bind x f = (%i. |
24 "pos_bind x f = (%i. Lazy_Sequence.bind (x i) (%a. f a i))" |
|
25 |
|
26 definition pos_decr_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq" |
|
27 where |
|
28 "pos_decr_bind x f = (%i. |
25 if i = 0 then |
29 if i = 0 then |
26 Lazy_Sequence.empty |
30 Lazy_Sequence.empty |
27 else |
31 else |
28 Lazy_Sequence.bind (x (i - 1)) (%a. f a i))" |
32 Lazy_Sequence.bind (x (i - 1)) (%a. f a i))" |
29 |
33 |
55 where |
59 where |
56 "neg_single x = (%i. Lazy_Sequence.hb_single x)" |
60 "neg_single x = (%i. Lazy_Sequence.hb_single x)" |
57 |
61 |
58 definition neg_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq" |
62 definition neg_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq" |
59 where |
63 where |
60 "neg_bind x f = (%i. |
64 "neg_bind x f = (%i. hb_bind (x i) (%a. f a i))" |
|
65 |
|
66 definition neg_decr_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq" |
|
67 where |
|
68 "neg_decr_bind x f = (%i. |
61 if i = 0 then |
69 if i = 0 then |
62 Lazy_Sequence.hit_bound |
70 Lazy_Sequence.hit_bound |
63 else |
71 else |
64 hb_bind (x (i - 1)) (%a. f a i))" |
72 hb_bind (x (i - 1)) (%a. f a i))" |
65 |
73 |
92 | Some ((), xq) => Lazy_Sequence.empty)" |
100 | Some ((), xq) => Lazy_Sequence.empty)" |
93 |
101 |
94 hide_type (open) pos_dseq neg_dseq |
102 hide_type (open) pos_dseq neg_dseq |
95 |
103 |
96 hide_const (open) |
104 hide_const (open) |
97 pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map |
105 pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map |
98 neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map |
106 neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map |
99 hide_fact (open) |
107 hide_fact (open) |
100 pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def |
108 pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def |
101 neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def |
109 neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def |
102 |
110 |
103 end |
111 end |