extracted/z.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Relations
   6
   7 open Nat
   8
   9 open Hints_declaration
  10
  11 open Core_notation
  12
  13 open Pts
  14
  15 open Logic
  16
  17 open Positive
  18
  19 type 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 **)
  26 let rec z_rect_Type4 h_OZ h_pos h_neg = function
  27 | OZ -> h_OZ
  28 | Pos x_4786 -> h_pos x_4786
  29 | Neg x_4787 -> h_neg x_4787
  30
  31 (** val z_rect_Type5 :
  32     'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
  33 let rec z_rect_Type5 h_OZ h_pos h_neg = function
  34 | OZ -> h_OZ
  35 | Pos x_4792 -> h_pos x_4792
  36 | Neg x_4793 -> h_neg x_4793
  37
  38 (** val z_rect_Type3 :
  39     'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
  40 let rec z_rect_Type3 h_OZ h_pos h_neg = function
  41 | OZ -> h_OZ
  42 | Pos x_4798 -> h_pos x_4798
  43 | Neg x_4799 -> h_neg x_4799
  44
  45 (** val z_rect_Type2 :
  46     'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
  47 let rec z_rect_Type2 h_OZ h_pos h_neg = function
  48 | OZ -> h_OZ
  49 | Pos x_4804 -> h_pos x_4804
  50 | Neg x_4805 -> h_neg x_4805
  51
  52 (** val z_rect_Type1 :
  53     'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
  54 let rec z_rect_Type1 h_OZ h_pos h_neg = function
  55 | OZ -> h_OZ
  56 | Pos x_4810 -> h_pos x_4810
  57 | Neg x_4811 -> h_neg x_4811
  58
  59 (** val z_rect_Type0 :
  60     'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
  61 let rec z_rect_Type0 h_OZ h_pos h_neg = function
  62 | OZ -> h_OZ
  63 | Pos x_4816 -> h_pos x_4816
  64 | Neg x_4817 -> h_neg x_4817
  65
  66 (** val z_inv_rect_Type4 :
  67     z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
  68     'a1) -> 'a1 **)
  69 let 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 **)
  75 let 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 **)
  81 let 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 **)
  87 let 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 **)
  93 let 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 -> __ **)
  97 let 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 **)
 105 let 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 **)
 110 let 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 **)
 115 let 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 **)
 121 let oZ_test = function
 122 | OZ -> Bool.True
 123 | Pos x -> Bool.False
 124 | Neg x -> Bool.False
 125
 126 (** val zsucc : z -> z **)
 127 let 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 **)
 137 let 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 **)
 147 let 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 **)
 166 let 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 **)
 185 let 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 **)
 208 let zopp = function
 209 | OZ -> OZ
 210 | Pos n -> Neg n
 211 | Neg n -> Pos n
 212
 213 (** val zminus : z -> z -> z **)
 214 let zminus x y =
 215   zplus x (zopp y)
 216
 217 (** val z_two_power_nat : Nat.nat -> z **)
 218 let z_two_power_nat n =
 219   Pos (Positive.two_power_nat n)
 220
 221 (** val z_two_power_pos : Positive.pos -> z **)
 222 let z_two_power_pos n =
 223   Pos (Positive.two_power_pos n)
 224
 225 (** val two_p : z -> z **)
 226 let two_p = function
 227 | OZ -> Pos Positive.One
 228 | Pos p -> Pos (Positive.two_power_pos p)
 229 | Neg x -> OZ
 230
 231 open Types
 232
 233 (** val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum **)
 234 let 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 **)
 240 let 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 **)
 259 let 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 **)
 278 let 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 **)
 282 let 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 **)
 286 let 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 **)
 301 let zmax x y =
 302   match z_compare x y with
 303   | Positive.LT -> y
 304   | Positive.EQ -> x
 305   | Positive.GT -> x
 306