source: extracted/z.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 7.6 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Positive
18
19type z =
20| OZ
21| Pos of Positive.pos
22| Neg of Positive.pos
23
24(** val z_rect_Type4 :
25    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
26let rec z_rect_Type4 h_OZ h_pos h_neg = function
27| OZ -> h_OZ
28| Pos x_1375 -> h_pos x_1375
29| Neg x_1376 -> h_neg x_1376
30
31(** val z_rect_Type5 :
32    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
33let rec z_rect_Type5 h_OZ h_pos h_neg = function
34| OZ -> h_OZ
35| Pos x_1381 -> h_pos x_1381
36| Neg x_1382 -> h_neg x_1382
37
38(** val z_rect_Type3 :
39    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
40let rec z_rect_Type3 h_OZ h_pos h_neg = function
41| OZ -> h_OZ
42| Pos x_1387 -> h_pos x_1387
43| Neg x_1388 -> h_neg x_1388
44
45(** val z_rect_Type2 :
46    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
47let rec z_rect_Type2 h_OZ h_pos h_neg = function
48| OZ -> h_OZ
49| Pos x_1393 -> h_pos x_1393
50| Neg x_1394 -> h_neg x_1394
51
52(** val z_rect_Type1 :
53    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
54let rec z_rect_Type1 h_OZ h_pos h_neg = function
55| OZ -> h_OZ
56| Pos x_1399 -> h_pos x_1399
57| Neg x_1400 -> h_neg x_1400
58
59(** val z_rect_Type0 :
60    'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
61let rec z_rect_Type0 h_OZ h_pos h_neg = function
62| OZ -> h_OZ
63| Pos x_1405 -> h_pos x_1405
64| Neg x_1406 -> h_neg x_1406
65
66(** val z_inv_rect_Type4 :
67    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
68    'a1) -> 'a1 **)
69let z_inv_rect_Type4 hterm h1 h2 h3 =
70  let hcut = z_rect_Type4 h1 h2 h3 hterm in hcut __
71
72(** val z_inv_rect_Type3 :
73    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
74    'a1) -> 'a1 **)
75let z_inv_rect_Type3 hterm h1 h2 h3 =
76  let hcut = z_rect_Type3 h1 h2 h3 hterm in hcut __
77
78(** val z_inv_rect_Type2 :
79    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
80    'a1) -> 'a1 **)
81let z_inv_rect_Type2 hterm h1 h2 h3 =
82  let hcut = z_rect_Type2 h1 h2 h3 hterm in hcut __
83
84(** val z_inv_rect_Type1 :
85    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
86    'a1) -> 'a1 **)
87let z_inv_rect_Type1 hterm h1 h2 h3 =
88  let hcut = z_rect_Type1 h1 h2 h3 hterm in hcut __
89
90(** val z_inv_rect_Type0 :
91    z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
92    'a1) -> 'a1 **)
93let z_inv_rect_Type0 hterm h1 h2 h3 =
94  let hcut = z_rect_Type0 h1 h2 h3 hterm in hcut __
95
96(** val z_discr : z -> z -> __ **)
97let z_discr x y =
98  Logic.eq_rect_Type2 x
99    (match x with
100     | OZ -> Obj.magic (fun _ dH -> dH)
101     | Pos a0 -> Obj.magic (fun _ dH -> dH __)
102     | Neg a0 -> Obj.magic (fun _ dH -> dH __)) y
103
104(** val z_of_nat : Nat.nat -> z **)
105let z_of_nat = function
106| Nat.O -> OZ
107| Nat.S n0 -> Pos (Positive.succ_pos_of_nat n0)
108
109(** val neg_Z_of_nat : Nat.nat -> z **)
110let neg_Z_of_nat = function
111| Nat.O -> OZ
112| Nat.S n0 -> Neg (Positive.succ_pos_of_nat n0)
113
114(** val abs : z -> Nat.nat **)
115let abs = function
116| OZ -> Nat.O
117| Pos n -> Positive.nat_of_pos n
118| Neg n -> Positive.nat_of_pos n
119
120(** val oZ_test : z -> Bool.bool **)
121let oZ_test = function
122| OZ -> Bool.True
123| Pos x -> Bool.False
124| Neg x -> Bool.False
125
126(** val zsucc : z -> z **)
127let zsucc = function
128| OZ -> Pos Positive.One
129| Pos n -> Pos (Positive.succ n)
130| Neg n ->
131  (match n with
132   | Positive.One -> OZ
133   | Positive.P1 x -> Neg (Positive.pred n)
134   | Positive.P0 x -> Neg (Positive.pred n))
135
136(** val zpred : z -> z **)
137let zpred = function
138| OZ -> Neg Positive.One
139| Pos n ->
140  (match n with
141   | Positive.One -> OZ
142   | Positive.P1 x -> Pos (Positive.pred n)
143   | Positive.P0 x -> Pos (Positive.pred n))
144| Neg n -> Neg (Positive.succ n)
145
146(** val eqZb : z -> z -> Bool.bool **)
147let rec eqZb x y =
148  match x with
149  | OZ ->
150    (match y with
151     | OZ -> Bool.True
152     | Pos q -> Bool.False
153     | Neg q -> Bool.False)
154  | Pos p ->
155    (match y with
156     | OZ -> Bool.False
157     | Pos q -> Positive.eqb p q
158     | Neg q -> Bool.False)
159  | Neg p ->
160    (match y with
161     | OZ -> Bool.False
162     | Pos q -> Bool.False
163     | Neg q -> Positive.eqb p q)
164
165(** val z_compare : z -> z -> Positive.compare **)
166let rec z_compare x y =
167  match x with
168  | OZ ->
169    (match y with
170     | OZ -> Positive.EQ
171     | Pos m -> Positive.LT
172     | Neg m -> Positive.GT)
173  | Pos n ->
174    (match y with
175     | OZ -> Positive.GT
176     | Pos m -> Positive.pos_compare n m
177     | Neg m -> Positive.GT)
178  | Neg n ->
179    (match y with
180     | OZ -> Positive.LT
181     | Pos m -> Positive.LT
182     | Neg m -> Positive.pos_compare m n)
183
184(** val zplus : z -> z -> z **)
185let rec zplus x y =
186  match x with
187  | OZ -> y
188  | Pos m ->
189    (match y with
190     | OZ -> x
191     | Pos n -> Pos (Positive.plus m n)
192     | Neg n ->
193       (match Positive.pos_compare m n with
194        | Positive.LT -> Neg (Positive.minus n m)
195        | Positive.EQ -> OZ
196        | Positive.GT -> Pos (Positive.minus m n)))
197  | Neg m ->
198    (match y with
199     | OZ -> x
200     | Pos n ->
201       (match Positive.pos_compare m n with
202        | Positive.LT -> Pos (Positive.minus n m)
203        | Positive.EQ -> OZ
204        | Positive.GT -> Neg (Positive.minus m n))
205     | Neg n -> Neg (Positive.plus m n))
206
207(** val zopp : z -> z **)
208let zopp = function
209| OZ -> OZ
210| Pos n -> Neg n
211| Neg n -> Pos n
212
213(** val zminus : z -> z -> z **)
214let zminus x y =
215  zplus x (zopp y)
216
217(** val z_two_power_nat : Nat.nat -> z **)
218let z_two_power_nat n =
219  Pos (Positive.two_power_nat n)
220
221(** val z_two_power_pos : Positive.pos -> z **)
222let z_two_power_pos n =
223  Pos (Positive.two_power_pos n)
224
225(** val two_p : z -> z **)
226let two_p = function
227| OZ -> Pos Positive.One
228| Pos p -> Pos (Positive.two_power_pos p)
229| Neg x -> OZ
230
231open Types
232
233(** val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum **)
234let decidable_eq_Z_Type z1 z2 =
235  (match eqZb z1 z2 with
236   | Bool.True -> (fun _ -> Types.Inl __)
237   | Bool.False -> (fun _ -> Types.Inr __)) __
238
239(** val zleb : z -> z -> Bool.bool **)
240let rec zleb x y =
241  match x with
242  | OZ ->
243    (match y with
244     | OZ -> Bool.True
245     | Pos m -> Bool.True
246     | Neg m -> Bool.False)
247  | Pos n ->
248    (match y with
249     | OZ -> Bool.False
250     | Pos m -> Positive.leb n m
251     | Neg m -> Bool.False)
252  | Neg n ->
253    (match y with
254     | OZ -> Bool.True
255     | Pos m -> Bool.True
256     | Neg m -> Positive.leb m n)
257
258(** val zltb : z -> z -> Bool.bool **)
259let rec zltb x y =
260  match x with
261  | OZ ->
262    (match y with
263     | OZ -> Bool.False
264     | Pos m -> Bool.True
265     | Neg m -> Bool.False)
266  | Pos n ->
267    (match y with
268     | OZ -> Bool.False
269     | Pos m -> Positive.leb (Positive.succ n) m
270     | Neg m -> Bool.False)
271  | Neg n ->
272    (match y with
273     | OZ -> Bool.True
274     | Pos m -> Bool.True
275     | Neg m -> Positive.leb (Positive.succ m) n)
276
277(** val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
278let zleb_elim_Type0 n m hle hnle =
279  Bool.bool_rect_Type0 (fun _ -> hle __) (fun _ -> hnle __) (zleb n m) __
280
281(** val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
282let zltb_elim_Type0 n m hlt hnlt =
283  Bool.bool_rect_Type0 (fun _ -> hlt __) (fun _ -> hnlt __) (zltb n m) __
284
285(** val z_times : z -> z -> z **)
286let rec z_times x y =
287  match x with
288  | OZ -> OZ
289  | Pos n ->
290    (match y with
291     | OZ -> OZ
292     | Pos m -> Pos (Positive.times n m)
293     | Neg m -> Neg (Positive.times n m))
294  | Neg n ->
295    (match y with
296     | OZ -> OZ
297     | Pos m -> Neg (Positive.times n m)
298     | Neg m -> Pos (Positive.times n m))
299
300(** val zmax : z -> z -> z **)
301let zmax x y =
302  match z_compare x y with
303  | Positive.LT -> y
304  | Positive.EQ -> x
305  | Positive.GT -> x
306
Note: See TracBrowser for help on using the repository browser.