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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/pts.ma".
24 include "freescale/bool.ma".
30 inductive nat : Type ≝
34 interpretation "Natural numbers" 'N = nat.
36 default "natural numbers" cic:/matita/freescale/nat/nat.ind.
38 alias num (instance 0) = "natural number".
40 nlet rec nat_ind (P:nat → Prop) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
41 match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_ind P p f n1) ].
43 nlet rec nat_rec (P:nat → Set) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
44 match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rec P p f n1) ].
46 nlet rec nat_rect (P:nat → Type) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
47 match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rect P p f n1) ].
49 nlet rec eq_nat (n1,n2:nat) on n1 ≝
51 [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
52 | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
58 | (S p) ⇒ match m with
59 [ O ⇒ false | (S q) ⇒ le_nat p q ]
62 nlet rec plus (n1,n2:nat) on n1 ≝
65 | (S n1') ⇒ S (plus n1' n2) ].
67 interpretation "natural plus" 'plus x y = (plus x y).
69 nlet rec times (n1,n2:nat) on n1 ≝
72 | (S n1') ⇒ n2 + (times n1' n2) ].
74 interpretation "natural times" 'times x y = (times x y).
82 | (S q) ⇒ minus p q ]].
84 interpretation "natural minus" 'minus x y = (minus x y).
86 nlet rec div_aux p m n : nat ≝
87 match (le_nat m n) with
92 | (S q) ⇒ S (div_aux q (m-(S n)) n)]].
94 ndefinition div : nat → nat → nat ≝
97 | (S p) ⇒ div_aux n n p].
99 interpretation "natural divide" 'divide x y = (div x y).