helm/software/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 (*   Ultima modifica: 05/08/2009                                          *)
  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 ndefinition nat1 ≝ S O.
  42 ndefinition nat2 ≝ S nat1.
  43 ndefinition nat3 ≝ S nat2.
  44 ndefinition nat4 ≝ S nat3.
  45 ndefinition nat5 ≝ S nat4.
  46 ndefinition nat6 ≝ S nat5.
  47 ndefinition nat7 ≝ S nat6.
  48 ndefinition nat8 ≝ S nat7.
  49 ndefinition nat9 ≝ S nat8.
  50 ndefinition nat10 ≝ S nat9.
  51 ndefinition nat11 ≝ S nat10.
  52 ndefinition nat12 ≝ S nat11.
  53 ndefinition nat13 ≝ S nat12.
  54 ndefinition nat14 ≝ S nat13.
  55 ndefinition nat15 ≝ S nat14.
  56 ndefinition nat16 ≝ S nat15.
  57 ndefinition nat17 ≝ S nat16.
  58 ndefinition nat18 ≝ S nat17.
  59 ndefinition nat19 ≝ S nat18.
  60 ndefinition nat20 ≝ S nat19.
  61 ndefinition nat21 ≝ S nat20.
  62 ndefinition nat22 ≝ S nat21.
  63 ndefinition nat23 ≝ S nat22.
  64 ndefinition nat24 ≝ S nat23.
  65 ndefinition nat25 ≝ S nat24.
  66 ndefinition nat26 ≝ S nat25.
  67 ndefinition nat27 ≝ S nat26.
  68 ndefinition nat28 ≝ S nat27.
  69 ndefinition nat29 ≝ S nat28.
  70 ndefinition nat30 ≝ S nat29.
  71 ndefinition nat31 ≝ S nat30.
  72 ndefinition nat32 ≝ S nat31.
  73 ndefinition nat33 ≝ S nat32.
  74 ndefinition nat34 ≝ S nat33.
  75 ndefinition nat35 ≝ S nat34.
  76 ndefinition nat36 ≝ S nat35.
  77 ndefinition nat37 ≝ S nat36.
  78 ndefinition nat38 ≝ S nat37.
  79 ndefinition nat39 ≝ S nat38.
  80 ndefinition nat40 ≝ S nat39.
  81 ndefinition nat41 ≝ S nat40.
  82 ndefinition nat42 ≝ S nat41.
  83 ndefinition nat43 ≝ S nat42.
  84 ndefinition nat44 ≝ S nat43.
  85 ndefinition nat45 ≝ S nat44.
  86 ndefinition nat46 ≝ S nat45.
  87 ndefinition nat47 ≝ S nat46.
  88 ndefinition nat48 ≝ S nat47.
  89 ndefinition nat49 ≝ S nat48.
  90 ndefinition nat50 ≝ S nat49.
  91 ndefinition nat51 ≝ S nat50.
  92 ndefinition nat52 ≝ S nat51.
  93 ndefinition nat53 ≝ S nat52.
  94 ndefinition nat54 ≝ S nat53.
  95 ndefinition nat55 ≝ S nat54.
  96 ndefinition nat56 ≝ S nat55.
  97 ndefinition nat57 ≝ S nat56.
  98 ndefinition nat58 ≝ S nat57.
  99 ndefinition nat59 ≝ S nat58.
 100 ndefinition nat60 ≝ S nat59.
 101 ndefinition nat61 ≝ S nat60.
 102 ndefinition nat62 ≝ S nat61.
 103 ndefinition nat63 ≝ S nat62.
 104 ndefinition nat64 ≝ S nat63.
 105 ndefinition nat65 ≝ S nat64.
 106 ndefinition nat66 ≝ S nat65.
 107 ndefinition nat67 ≝ S nat66.
 108 ndefinition nat68 ≝ S nat67.
 109 ndefinition nat69 ≝ S nat68.
 110 ndefinition nat70 ≝ S nat69.
 111 ndefinition nat71 ≝ S nat70.
 112 ndefinition nat72 ≝ S nat71.
 113 ndefinition nat73 ≝ S nat72.
 114 ndefinition nat74 ≝ S nat73.
 115 ndefinition nat75 ≝ S nat74.
 116 ndefinition nat76 ≝ S nat75.
 117 ndefinition nat77 ≝ S nat76.
 118 ndefinition nat78 ≝ S nat77.
 119 ndefinition nat79 ≝ S nat78.
 120 ndefinition nat80 ≝ S nat79.
 121 ndefinition nat81 ≝ S nat80.
 122 ndefinition nat82 ≝ S nat81.
 123 ndefinition nat83 ≝ S nat82.
 124 ndefinition nat84 ≝ S nat83.
 125 ndefinition nat85 ≝ S nat84.
 126 ndefinition nat86 ≝ S nat85.
 127 ndefinition nat87 ≝ S nat86.
 128 ndefinition nat88 ≝ S nat87.
 129 ndefinition nat89 ≝ S nat88.
 130 ndefinition nat90 ≝ S nat89.
 131 ndefinition nat91 ≝ S nat90.
 132 ndefinition nat92 ≝ S nat91.
 133 ndefinition nat93 ≝ S nat92.
 134 ndefinition nat94 ≝ S nat93.
 135 ndefinition nat95 ≝ S nat94.
 136 ndefinition nat96 ≝ S nat95.
 137 ndefinition nat97 ≝ S nat96.
 138 ndefinition nat98 ≝ S nat97.
 139 ndefinition nat99 ≝ S nat98.
 140 ndefinition nat100 ≝ S nat99.
 141
 142 nlet rec eq_nat (n1,n2:nat) on n1 ≝
 143  match n1 with
 144   [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
 145   | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
 146   ].
 147
 148 nlet rec le_nat n m ≝
 149  match n with
 150   [ O ⇒ true
 151   | (S p) ⇒ match m with
 152    [ O ⇒ false | (S q) ⇒ le_nat p q ]
 153   ].
 154
 155 interpretation "natural 'less or equal to'" 'leq x y = (le_nat x y).
 156
 157 ndefinition lt_nat ≝ λn1,n2:nat.(le_nat n1 n2) ⊗ (⊖ (eq_nat n1 n2)).
 158
 159 interpretation "natural 'less than'" 'lt x y = (lt_nat x y).
 160
 161 ndefinition ge_nat ≝ λn1,n2:nat.(⊖ (le_nat n1 n2)) ⊕ (eq_nat n1 n2).
 162
 163 interpretation "natural 'greater or equal to'" 'geq x y = (ge_nat x y).
 164
 165 ndefinition gt_nat ≝ λn1,n2:nat.⊖ (le_nat n1 n2).
 166
 167 interpretation "natural 'greater than'" 'gt x y = (gt_nat x y).
 168
 169 nlet rec plus (n1,n2:nat) on n1 ≝
 170  match n1 with
 171   [ O ⇒ n2
 172   | (S n1') ⇒ S (plus n1' n2) ].
 173
 174 interpretation "natural plus" 'plus x y = (plus x y).
 175
 176 nlet rec times (n1,n2:nat) on n1 ≝
 177  match n1 with
 178   [ O ⇒ O
 179   | (S n1') ⇒ n2 + (times n1' n2) ].
 180
 181 interpretation "natural times" 'times x y = (times x y).
 182
 183 nlet rec minus n m ≝
 184  match n with
 185  [ O ⇒ O
 186  | (S p) ⇒
 187         match m with
 188         [O ⇒ (S p)
 189   | (S q) ⇒ minus p q ]].
 190
 191 interpretation "natural minus" 'minus x y = (minus x y).
 192
 193 nlet rec div_aux p m n : nat ≝
 194 match (le_nat m n) with
 195 [ true ⇒ O
 196 | false ⇒
 197   match p with
 198   [ O ⇒ O
 199   | (S q) ⇒ S (div_aux q (m-(S n)) n)]].
 200
 201 ndefinition div : nat → nat → nat ≝
 202 λn,m.match m with
 203  [ O ⇒ S n
 204  | (S p) ⇒ div_aux n n p].
 205
 206 interpretation "natural divide" 'divide x y = (div x y).
 207
 208 ndefinition pred ≝ λn.match n with [ O ⇒ O | S n ⇒ n ].
 209
 210 ndefinition nat128 ≝ nat64 * nat2.
 211 ndefinition nat256 ≝ nat128 * nat2.
 212 ndefinition nat512 ≝ nat256 * nat2.
 213 ndefinition nat1024 ≝ nat512 * nat2.
 214 ndefinition nat2048 ≝ nat1024 * nat2.
 215 ndefinition nat4096 ≝ nat2048 * nat2.
 216 ndefinition nat8192 ≝ nat4096 * nat2.
 217 ndefinition nat16384 ≝ nat8192 * nat2.
 218 ndefinition nat32768 ≝ nat16384 * nat2.
 219 ndefinition nat65536 ≝ nat32768 * nat2.