matita/matita/contribs/ng_assembly/common/nat.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/bool.ma".
  24
  25 (* ******** *)
  26 (* NATURALI *)
  27 (* ******** *)
  28
  29 ninductive nat : Type ≝
  30   O : nat
  31 | S : nat → nat.
  32
  33 (*
  34 interpretation "Natural numbers" 'N = nat.
  35
  36 default "natural numbers" cic:/matita/common/nat/nat.ind.
  37
  38 alias num (instance 0) = "natural number".
  39 *)
  40
  41 nlet rec nat_it (T:Type) (f:T → T) (arg:T) (n:nat) on n ≝
  42  match n with
  43   [ O ⇒ arg
  44   | S n' ⇒ nat_it T f (f arg) n'
  45   ].
  46
  47 ndefinition nat1 ≝ S O.
  48 ndefinition nat2 ≝ S nat1.
  49 ndefinition nat3 ≝ S nat2.
  50 ndefinition nat4 ≝ S nat3.
  51 ndefinition nat5 ≝ S nat4.
  52 ndefinition nat6 ≝ S nat5.
  53 ndefinition nat7 ≝ S nat6.
  54 ndefinition nat8 ≝ S nat7.
  55 ndefinition nat9 ≝ S nat8.
  56 ndefinition nat10 ≝ S nat9.
  57 ndefinition nat11 ≝ S nat10.
  58 ndefinition nat12 ≝ S nat11.
  59 ndefinition nat13 ≝ S nat12.
  60 ndefinition nat14 ≝ S nat13.
  61 ndefinition nat15 ≝ S nat14.
  62 ndefinition nat16 ≝ S nat15.
  63 ndefinition nat17 ≝ S nat16.
  64 ndefinition nat18 ≝ S nat17.
  65 ndefinition nat19 ≝ S nat18.
  66 ndefinition nat20 ≝ S nat19.
  67 ndefinition nat21 ≝ S nat20.
  68 ndefinition nat22 ≝ S nat21.
  69 ndefinition nat23 ≝ S nat22.
  70 ndefinition nat24 ≝ S nat23.
  71 ndefinition nat25 ≝ S nat24.
  72 ndefinition nat26 ≝ S nat25.
  73 ndefinition nat27 ≝ S nat26.
  74 ndefinition nat28 ≝ S nat27.
  75 ndefinition nat29 ≝ S nat28.
  76 ndefinition nat30 ≝ S nat29.
  77 ndefinition nat31 ≝ S nat30.
  78 ndefinition nat32 ≝ S nat31.
  79 ndefinition nat33 ≝ S nat32.
  80 ndefinition nat34 ≝ S nat33.
  81 ndefinition nat35 ≝ S nat34.
  82 ndefinition nat36 ≝ S nat35.
  83 ndefinition nat37 ≝ S nat36.
  84 ndefinition nat38 ≝ S nat37.
  85 ndefinition nat39 ≝ S nat38.
  86 ndefinition nat40 ≝ S nat39.
  87 ndefinition nat41 ≝ S nat40.
  88 ndefinition nat42 ≝ S nat41.
  89 ndefinition nat43 ≝ S nat42.
  90 ndefinition nat44 ≝ S nat43.
  91 ndefinition nat45 ≝ S nat44.
  92 ndefinition nat46 ≝ S nat45.
  93 ndefinition nat47 ≝ S nat46.
  94 ndefinition nat48 ≝ S nat47.
  95 ndefinition nat49 ≝ S nat48.
  96 ndefinition nat50 ≝ S nat49.
  97 ndefinition nat51 ≝ S nat50.
  98 ndefinition nat52 ≝ S nat51.
  99 ndefinition nat53 ≝ S nat52.
 100 ndefinition nat54 ≝ S nat53.
 101 ndefinition nat55 ≝ S nat54.
 102 ndefinition nat56 ≝ S nat55.
 103 ndefinition nat57 ≝ S nat56.
 104 ndefinition nat58 ≝ S nat57.
 105 ndefinition nat59 ≝ S nat58.
 106 ndefinition nat60 ≝ S nat59.
 107 ndefinition nat61 ≝ S nat60.
 108 ndefinition nat62 ≝ S nat61.
 109 ndefinition nat63 ≝ S nat62.
 110 ndefinition nat64 ≝ S nat63.
 111 ndefinition nat65 ≝ S nat64.
 112 ndefinition nat66 ≝ S nat65.
 113 ndefinition nat67 ≝ S nat66.
 114 ndefinition nat68 ≝ S nat67.
 115 ndefinition nat69 ≝ S nat68.
 116 ndefinition nat70 ≝ S nat69.
 117 ndefinition nat71 ≝ S nat70.
 118 ndefinition nat72 ≝ S nat71.
 119 ndefinition nat73 ≝ S nat72.
 120 ndefinition nat74 ≝ S nat73.
 121 ndefinition nat75 ≝ S nat74.
 122 ndefinition nat76 ≝ S nat75.
 123 ndefinition nat77 ≝ S nat76.
 124 ndefinition nat78 ≝ S nat77.
 125 ndefinition nat79 ≝ S nat78.
 126 ndefinition nat80 ≝ S nat79.
 127 ndefinition nat81 ≝ S nat80.
 128 ndefinition nat82 ≝ S nat81.
 129 ndefinition nat83 ≝ S nat82.
 130 ndefinition nat84 ≝ S nat83.
 131 ndefinition nat85 ≝ S nat84.
 132 ndefinition nat86 ≝ S nat85.
 133 ndefinition nat87 ≝ S nat86.
 134 ndefinition nat88 ≝ S nat87.
 135 ndefinition nat89 ≝ S nat88.
 136 ndefinition nat90 ≝ S nat89.
 137 ndefinition nat91 ≝ S nat90.
 138 ndefinition nat92 ≝ S nat91.
 139 ndefinition nat93 ≝ S nat92.
 140 ndefinition nat94 ≝ S nat93.
 141 ndefinition nat95 ≝ S nat94.
 142 ndefinition nat96 ≝ S nat95.
 143 ndefinition nat97 ≝ S nat96.
 144 ndefinition nat98 ≝ S nat97.
 145 ndefinition nat99 ≝ S nat98.
 146 ndefinition nat100 ≝ S nat99.
 147
 148 nlet rec eq_nat (n1,n2:nat) on n1 ≝
 149  match n1 with
 150   [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
 151   | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
 152   ].
 153
 154 nlet rec le_nat n m ≝
 155  match n with
 156   [ O ⇒ true
 157   | (S p) ⇒ match m with
 158    [ O ⇒ false | (S q) ⇒ le_nat p q ]
 159   ].
 160
 161 interpretation "natural 'less or equal to'" 'leq x y = (le_nat x y).
 162
 163 ndefinition lt_nat ≝ λn1,n2:nat.(le_nat n1 n2) ⊗ (⊖ (eq_nat n1 n2)).
 164
 165 interpretation "natural 'less than'" 'lt x y = (lt_nat x y).
 166
 167 ndefinition ge_nat ≝ λn1,n2:nat.(⊖ (le_nat n1 n2)) ⊕ (eq_nat n1 n2).
 168
 169 interpretation "natural 'greater or equal to'" 'geq x y = (ge_nat x y).
 170
 171 ndefinition gt_nat ≝ λn1,n2:nat.⊖ (le_nat n1 n2).
 172
 173 interpretation "natural 'greater than'" 'gt x y = (gt_nat x y).
 174
 175 nlet rec plus (n1,n2:nat) on n1 ≝
 176  match n1 with
 177   [ O ⇒ n2
 178   | (S n1') ⇒ S (plus n1' n2) ].
 179
 180 interpretation "natural plus" 'plus x y = (plus x y).
 181
 182 nlet rec times (n1,n2:nat) on n1 ≝
 183  match n1 with
 184   [ O ⇒ O
 185   | (S n1') ⇒ n2 + (times n1' n2) ].
 186
 187 interpretation "natural times" 'times x y = (times x y).
 188
 189 nlet rec minus n m ≝
 190  match n with
 191  [ O ⇒ O
 192  | (S p) ⇒
 193         match m with
 194         [O ⇒ (S p)
 195   | (S q) ⇒ minus p q ]].
 196
 197 interpretation "natural minus" 'minus x y = (minus x y).
 198
 199 nlet rec div_aux p m n : nat ≝
 200 match (le_nat m n) with
 201 [ true ⇒ O
 202 | false ⇒
 203   match p with
 204   [ O ⇒ O
 205   | (S q) ⇒ S (div_aux q (m-(S n)) n)]].
 206
 207 ndefinition div : nat → nat → nat ≝
 208 λn,m.match m with
 209  [ O ⇒ S n
 210  | (S p) ⇒ div_aux n n p].
 211
 212 interpretation "natural divide" 'divide x y = (div x y).
 213
 214 ndefinition pred ≝ λn.match n with [ O ⇒ O | S n ⇒ n ].
 215
 216 ndefinition nat128 ≝ nat64 + nat64.
 217 ndefinition nat256 ≝ nat128 + nat128.
 218 ndefinition nat512 ≝ nat256 + nat256.
 219 ndefinition nat1024 ≝ nat512 + nat512.
 220 ndefinition nat2048 ≝ nat1024 + nat1024.
 221 ndefinition nat4096 ≝ nat2048 + nat2048.
 222 ndefinition nat8192 ≝ nat4096 + nat4096.
 223 ndefinition nat16384 ≝ nat8192 + nat8192.
 224 ndefinition nat32768 ≝ nat16384 + nat16384.
 225 ndefinition nat65536 ≝ nat32768 + nat32768.