[2717] | 1 | open Preamble |
---|
| 2 | |
---|
| 3 | open Hints_declaration |
---|
| 4 | |
---|
| 5 | open Core_notation |
---|
| 6 | |
---|
| 7 | open Pts |
---|
| 8 | |
---|
| 9 | open Logic |
---|
| 10 | |
---|
| 11 | open Types |
---|
| 12 | |
---|
| 13 | open Bool |
---|
| 14 | |
---|
| 15 | open Relations |
---|
| 16 | |
---|
| 17 | open Nat |
---|
| 18 | |
---|
| 19 | open List |
---|
| 20 | |
---|
| 21 | open Div_and_mod |
---|
| 22 | |
---|
| 23 | open Jmeq |
---|
| 24 | |
---|
| 25 | open Russell |
---|
| 26 | |
---|
| 27 | open Util |
---|
| 28 | |
---|
| 29 | type 'x set (* AXIOM TO BE REALIZED *) |
---|
| 30 | |
---|
| 31 | type 'elt_type set0 = |
---|
| 32 | | Empty |
---|
| 33 | | Node of Nat.nat * 'elt_type set0 * 'elt_type * 'elt_type set0 |
---|
| 34 | |
---|
| 35 | (** val set_rect_Type4 : |
---|
| 36 | 'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) -> |
---|
| 37 | 'a1 set0 -> 'a2 **) |
---|
| 38 | let rec set_rect_Type4 h_empty h_node = function |
---|
| 39 | | Empty -> h_empty |
---|
| 40 | | Node (x_18359, x_18358, x_18357, x_18356) -> |
---|
| 41 | h_node x_18359 x_18358 x_18357 x_18356 |
---|
| 42 | (set_rect_Type4 h_empty h_node x_18358) |
---|
| 43 | (set_rect_Type4 h_empty h_node x_18356) |
---|
| 44 | |
---|
| 45 | (** val set_rect_Type3 : |
---|
| 46 | 'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) -> |
---|
| 47 | 'a1 set0 -> 'a2 **) |
---|
| 48 | let rec set_rect_Type3 h_empty h_node = function |
---|
| 49 | | Empty -> h_empty |
---|
| 50 | | Node (x_18373, x_18372, x_18371, x_18370) -> |
---|
| 51 | h_node x_18373 x_18372 x_18371 x_18370 |
---|
| 52 | (set_rect_Type3 h_empty h_node x_18372) |
---|
| 53 | (set_rect_Type3 h_empty h_node x_18370) |
---|
| 54 | |
---|
| 55 | (** val set_rect_Type2 : |
---|
| 56 | 'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) -> |
---|
| 57 | 'a1 set0 -> 'a2 **) |
---|
| 58 | let rec set_rect_Type2 h_empty h_node = function |
---|
| 59 | | Empty -> h_empty |
---|
| 60 | | Node (x_18380, x_18379, x_18378, x_18377) -> |
---|
| 61 | h_node x_18380 x_18379 x_18378 x_18377 |
---|
| 62 | (set_rect_Type2 h_empty h_node x_18379) |
---|
| 63 | (set_rect_Type2 h_empty h_node x_18377) |
---|
| 64 | |
---|
| 65 | (** val set_rect_Type1 : |
---|
| 66 | 'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) -> |
---|
| 67 | 'a1 set0 -> 'a2 **) |
---|
| 68 | let rec set_rect_Type1 h_empty h_node = function |
---|
| 69 | | Empty -> h_empty |
---|
| 70 | | Node (x_18387, x_18386, x_18385, x_18384) -> |
---|
| 71 | h_node x_18387 x_18386 x_18385 x_18384 |
---|
| 72 | (set_rect_Type1 h_empty h_node x_18386) |
---|
| 73 | (set_rect_Type1 h_empty h_node x_18384) |
---|
| 74 | |
---|
| 75 | (** val set_rect_Type0 : |
---|
| 76 | 'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) -> |
---|
| 77 | 'a1 set0 -> 'a2 **) |
---|
| 78 | let rec set_rect_Type0 h_empty h_node = function |
---|
| 79 | | Empty -> h_empty |
---|
| 80 | | Node (x_18394, x_18393, x_18392, x_18391) -> |
---|
| 81 | h_node x_18394 x_18393 x_18392 x_18391 |
---|
| 82 | (set_rect_Type0 h_empty h_node x_18393) |
---|
| 83 | (set_rect_Type0 h_empty h_node x_18391) |
---|
| 84 | |
---|
| 85 | (** val set_inv_rect_Type4 : |
---|
| 86 | 'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__ |
---|
| 87 | -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **) |
---|
| 88 | let set_inv_rect_Type4 hterm h1 h2 = |
---|
| 89 | let hcut = set_rect_Type4 h1 h2 hterm in hcut __ |
---|
| 90 | |
---|
| 91 | (** val set_inv_rect_Type3 : |
---|
| 92 | 'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__ |
---|
| 93 | -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **) |
---|
| 94 | let set_inv_rect_Type3 hterm h1 h2 = |
---|
| 95 | let hcut = set_rect_Type3 h1 h2 hterm in hcut __ |
---|
| 96 | |
---|
| 97 | (** val set_inv_rect_Type2 : |
---|
| 98 | 'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__ |
---|
| 99 | -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **) |
---|
| 100 | let set_inv_rect_Type2 hterm h1 h2 = |
---|
| 101 | let hcut = set_rect_Type2 h1 h2 hterm in hcut __ |
---|
| 102 | |
---|
| 103 | (** val set_inv_rect_Type1 : |
---|
| 104 | 'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__ |
---|
| 105 | -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **) |
---|
| 106 | let set_inv_rect_Type1 hterm h1 h2 = |
---|
| 107 | let hcut = set_rect_Type1 h1 h2 hterm in hcut __ |
---|
| 108 | |
---|
| 109 | (** val set_inv_rect_Type0 : |
---|
| 110 | 'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__ |
---|
| 111 | -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **) |
---|
| 112 | let set_inv_rect_Type0 hterm h1 h2 = |
---|
| 113 | let hcut = set_rect_Type0 h1 h2 hterm in hcut __ |
---|
| 114 | |
---|
| 115 | (** val set_discr : 'a1 set0 -> 'a1 set0 -> __ **) |
---|
| 116 | let set_discr x y = |
---|
| 117 | Logic.eq_rect_Type2 x |
---|
| 118 | (match x with |
---|
| 119 | | Empty -> Obj.magic (fun _ dH -> dH) |
---|
| 120 | | Node (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y |
---|
| 121 | |
---|
| 122 | (** val set_jmdiscr : 'a1 set0 -> 'a1 set0 -> __ **) |
---|
| 123 | let set_jmdiscr x y = |
---|
| 124 | Logic.eq_rect_Type2 x |
---|
| 125 | (match x with |
---|
| 126 | | Empty -> Obj.magic (fun _ dH -> dH) |
---|
| 127 | | Node (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y |
---|
| 128 | |
---|
| 129 | (** val set_empty : 'a1 set0 **) |
---|
[2718] | 130 | let set_empty _ = |
---|
[2717] | 131 | failwith "AXIOM TO BE REALIZED" |
---|
| 132 | |
---|
| 133 | (** val set_size : 'a1 set0 -> Nat.nat **) |
---|
| 134 | let set_size _ = |
---|
| 135 | failwith "AXIOM TO BE REALIZED" |
---|
| 136 | |
---|
| 137 | (** val set_to_list : 'a1 set0 -> 'a1 List.list **) |
---|
| 138 | let set_to_list _ = |
---|
| 139 | failwith "AXIOM TO BE REALIZED" |
---|
| 140 | |
---|
| 141 | (** val set_insert : 'a1 -> 'a1 set0 -> 'a1 set0 **) |
---|
| 142 | let set_insert _ = |
---|
| 143 | failwith "AXIOM TO BE REALIZED" |
---|
| 144 | |
---|
| 145 | (** val set_remove : 'a1 -> 'a1 set0 -> 'a1 set0 **) |
---|
| 146 | let set_remove _ = |
---|
| 147 | failwith "AXIOM TO BE REALIZED" |
---|
| 148 | |
---|
| 149 | (** val set_member : |
---|
| 150 | ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set0 -> Bool.bool **) |
---|
| 151 | let set_member _ = |
---|
| 152 | failwith "AXIOM TO BE REALIZED" |
---|
| 153 | |
---|
| 154 | (** val set_forall : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **) |
---|
| 155 | let set_forall _ = |
---|
| 156 | failwith "AXIOM TO BE REALIZED" |
---|
| 157 | |
---|
| 158 | (** val set_exists : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **) |
---|
| 159 | let set_exists _ = |
---|
| 160 | failwith "AXIOM TO BE REALIZED" |
---|
| 161 | |
---|
| 162 | (** val set_filter : ('a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 **) |
---|
| 163 | let set_filter _ = |
---|
| 164 | failwith "AXIOM TO BE REALIZED" |
---|
| 165 | |
---|
| 166 | (** val set_map : ('a1 -> 'a2) -> 'a1 set0 -> 'a2 set0 **) |
---|
| 167 | let set_map _ = |
---|
| 168 | failwith "AXIOM TO BE REALIZED" |
---|
| 169 | |
---|
| 170 | (** val set_fold : ('a1 -> 'a2 -> 'a2) -> 'a1 set0 -> 'a2 -> 'a2 **) |
---|
| 171 | let set_fold _ = |
---|
| 172 | failwith "AXIOM TO BE REALIZED" |
---|
| 173 | |
---|
| 174 | (** val set_equal : |
---|
| 175 | ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **) |
---|
| 176 | let set_equal _ = |
---|
| 177 | failwith "AXIOM TO BE REALIZED" |
---|
| 178 | |
---|
| 179 | (** val set_diff : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **) |
---|
| 180 | let set_diff _ = |
---|
| 181 | failwith "AXIOM TO BE REALIZED" |
---|
| 182 | |
---|
| 183 | (** val set_is_empty : 'a1 set0 -> Bool.bool **) |
---|
| 184 | let set_is_empty set1 = |
---|
| 185 | Util.eq_nat (set_size set1) Nat.O |
---|
| 186 | |
---|
| 187 | (** val set_singleton : 'a1 -> 'a1 set0 **) |
---|
| 188 | let set_singleton elt = |
---|
[2718] | 189 | set_insert elt (set_empty ()) |
---|
[2717] | 190 | |
---|
| 191 | (** val set_from_list : 'a1 List.list -> 'a1 set0 **) |
---|
| 192 | let set_from_list the_list = |
---|
[2718] | 193 | List.foldr set_insert (set_empty ()) the_list |
---|
[2717] | 194 | |
---|
| 195 | (** val set_split : |
---|
| 196 | ('a1 -> Bool.bool) -> 'a1 set0 -> ('a1 set0, 'a1 set0) Types.prod **) |
---|
| 197 | let set_split pred0 the_set = |
---|
| 198 | let left = set_filter pred0 the_set in |
---|
| 199 | let npred = fun x -> Bool.notb (pred0 x) in |
---|
| 200 | let right = set_filter npred the_set in |
---|
| 201 | { Types.fst = left; Types.snd = right } |
---|
| 202 | |
---|
| 203 | (** val set_subset : |
---|
| 204 | ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **) |
---|
| 205 | let set_subset eq left right = |
---|
| 206 | set_forall (fun elt -> set_member eq elt right) left |
---|
| 207 | |
---|
| 208 | (** val set_subseteq : |
---|
| 209 | ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **) |
---|
| 210 | let set_subseteq eq left right = |
---|
| 211 | Bool.andb (set_equal eq left right) (set_subset eq left right) |
---|
| 212 | |
---|
| 213 | (** val set_union : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **) |
---|
| 214 | let set_union left right = |
---|
| 215 | set_fold set_insert left right |
---|
| 216 | |
---|
| 217 | (** val set_intersection : |
---|
| 218 | ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> 'a1 set0 **) |
---|
| 219 | let set_intersection eq left right = |
---|
| 220 | set_filter (fun elt -> set_member eq elt right) left |
---|
| 221 | |
---|