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 nlet rec eq_nat (n1,n2:nat) on n1 ≝
  42  match n1 with
  43   [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
  44   | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
  45   ].
  46
  47 nlet rec le_nat n m ≝
  48  match n with
  49   [ O ⇒ true
  50   | (S p) ⇒ match m with
  51    [ O ⇒ false | (S q) ⇒ le_nat p q ]
  52   ].
  53
  54 interpretation "natural 'less or equal to'" 'leq x y = (le_nat x y).
  55
  56 ndefinition lt_nat ≝ λn1,n2:nat.(le_nat n1 n2) ⊗ (⊖ (eq_nat n1 n2)).
  57
  58 interpretation "natural 'less than'" 'lt x y = (lt_nat x y).
  59
  60 ndefinition ge_nat ≝ λn1,n2:nat.(⊖ (le_nat n1 n2)) ⊕ (eq_nat n1 n2).
  61
  62 interpretation "natural 'greater or equal to'" 'geq x y = (ge_nat x y).
  63
  64 ndefinition gt_nat ≝ λn1,n2:nat.⊖ (le_nat n1 n2).
  65
  66 interpretation "natural 'greater than'" 'gt x y = (gt_nat x y).
  67
  68 nlet rec plus (n1,n2:nat) on n1 ≝
  69  match n1 with
  70   [ O ⇒ n2
  71   | (S n1') ⇒ S (plus n1' n2) ].
  72
  73 interpretation "natural plus" 'plus x y = (plus x y).
  74
  75 nlet rec times (n1,n2:nat) on n1 ≝
  76  match n1 with
  77   [ O ⇒ O
  78   | (S n1') ⇒ n2 + (times n1' n2) ].
  79
  80 interpretation "natural times" 'times x y = (times x y).
  81
  82 nlet rec minus n m ≝
  83  match n with
  84  [ O ⇒ O
  85  | (S p) ⇒
  86         match m with
  87         [O ⇒ (S p)
  88   | (S q) ⇒ minus p q ]].
  89
  90 interpretation "natural minus" 'minus x y = (minus x y).
  91
  92 nlet rec div_aux p m n : nat ≝
  93 match (le_nat m n) with
  94 [ true ⇒ O
  95 | false ⇒
  96   match p with
  97   [ O ⇒ O
  98   | (S q) ⇒ S (div_aux q (m-(S n)) n)]].
  99
 100 ndefinition div : nat → nat → nat ≝
 101 λn,m.match m with
 102  [ O ⇒ S n
 103  | (S p) ⇒ div_aux n n p].
 104
 105 interpretation "natural divide" 'divide x y = (div x y).