1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "num/bool.ma".
29 inductive nat : Type ≝
33 interpretation "Natural numbers" 'N = nat.
35 default "natural numbers" cic:/matita/common/nat/nat.ind.
37 alias num (instance 0) = "natural number".
39 nlet rec eq_nat (n1,n2:nat) on n1 ≝
41 [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
42 | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
48 | (S p) ⇒ match m with
49 [ O ⇒ false | (S q) ⇒ le_nat p q ]
52 interpretation "natural 'less or equal to'" 'leq x y = (le_nat x y).
54 ndefinition lt_nat ≝ λn1,n2:nat.(le_nat n1 n2) ⊗ (⊖ (eq_nat n1 n2)).
56 interpretation "natural 'less than'" 'lt x y = (lt_nat x y).
58 ndefinition ge_nat ≝ λn1,n2:nat.(⊖ (le_nat n1 n2)) ⊕ (eq_nat n1 n2).
60 interpretation "natural 'greater or equal to'" 'geq x y = (ge_nat x y).
62 ndefinition gt_nat ≝ λn1,n2:nat.⊖ (le_nat n1 n2).
64 interpretation "natural 'greater than'" 'gt x y = (gt_nat x y).
66 nlet rec plus (n1,n2:nat) on n1 ≝
69 | (S n1') ⇒ S (plus n1' n2) ].
71 interpretation "natural plus" 'plus x y = (plus x y).
73 nlet rec times (n1,n2:nat) on n1 ≝
76 | (S n1') ⇒ n2 + (times n1' n2) ].
78 interpretation "natural times" 'times x y = (times x y).
86 | (S q) ⇒ minus p q ]].
88 interpretation "natural minus" 'minus x y = (minus x y).
90 nlet rec div_aux p m n : nat ≝
91 match (le_nat m n) with
96 | (S q) ⇒ S (div_aux q (m-(S n)) n)]].
98 ndefinition div : nat → nat → nat ≝
101 | (S p) ⇒ div_aux n n p].
103 interpretation "natural divide" 'divide x y = (div x y).