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 ninductive nat : Type ≝
34 interpretation "Natural numbers" 'N = nat.
36 default "natural numbers" cic:/matita/common/nat/nat.ind.
38 alias num (instance 0) = "natural number".
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.
142 nlet rec eq_nat (n1,n2:nat) on n1 ≝
144 [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
145 | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
148 nlet rec le_nat n m ≝
151 | (S p) ⇒ match m with
152 [ O ⇒ false | (S q) ⇒ le_nat p q ]
155 interpretation "natural 'less or equal to'" 'leq x y = (le_nat x y).
157 ndefinition lt_nat ≝ λn1,n2:nat.(le_nat n1 n2) ⊗ (⊖ (eq_nat n1 n2)).
159 interpretation "natural 'less than'" 'lt x y = (lt_nat x y).
161 ndefinition ge_nat ≝ λn1,n2:nat.(⊖ (le_nat n1 n2)) ⊕ (eq_nat n1 n2).
163 interpretation "natural 'greater or equal to'" 'geq x y = (ge_nat x y).
165 ndefinition gt_nat ≝ λn1,n2:nat.⊖ (le_nat n1 n2).
167 interpretation "natural 'greater than'" 'gt x y = (gt_nat x y).
169 nlet rec plus (n1,n2:nat) on n1 ≝
172 | (S n1') ⇒ S (plus n1' n2) ].
174 interpretation "natural plus" 'plus x y = (plus x y).
176 nlet rec times (n1,n2:nat) on n1 ≝
179 | (S n1') ⇒ n2 + (times n1' n2) ].
181 interpretation "natural times" 'times x y = (times x y).
189 | (S q) ⇒ minus p q ]].
191 interpretation "natural minus" 'minus x y = (minus x y).
193 nlet rec div_aux p m n : nat ≝
194 match (le_nat m n) with
199 | (S q) ⇒ S (div_aux q (m-(S n)) n)]].
201 ndefinition div : nat → nat → nat ≝
204 | (S p) ⇒ div_aux n n p].
206 interpretation "natural divide" 'divide x y = (div x y).
208 ndefinition pred ≝ λn.match n with [ O ⇒ O | S n ⇒ n ].
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.