]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/Ztest.ma
restructuring
[helm.git] / matita / matita / tests / Ztest.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "arithmetics/nat.ma".
16
17 ninductive Z : Type ≝
18   OZ : Z
19 | pos : nat → Z
20 | neg : nat → Z.
21
22 interpretation "Integers" 'Z = Z.
23
24 (* TODO: move the following two to datatypes/compare.ma *)
25 ninductive compare : Type[0] ≝
26 | LT : compare
27 | EQ : compare
28 | GT : compare.
29
30 nlet rec nat_compare n m: compare ≝
31 match n with
32 [ O ⇒ match m with 
33       [ O ⇒ EQ
34       | (S q) ⇒ LT ]
35 | S p ⇒ match m with 
36       [ O ⇒ GT
37       | S q ⇒ nat_compare p q]].
38
39 ndefinition Zplus : Z → Z → Z ≝
40   λx,y. match x with
41     [ OZ ⇒ y
42     | pos m ⇒
43         match y with
44          [ OZ ⇒ x
45          | pos n ⇒ (pos (pred ((S m)+(S n))))
46          | neg n ⇒ 
47               match nat_compare m n with
48                 [ LT ⇒ (neg (pred (n-m)))
49                 | EQ ⇒ OZ
50                 | GT ⇒ (pos (pred (m-n)))] ]
51     | neg m ⇒
52         match y with
53          [ OZ ⇒ x
54          | pos n ⇒
55               match nat_compare m n with
56                 [ LT ⇒ (pos (pred (n-m)))
57                 | EQ ⇒ OZ
58                 | GT ⇒ (neg (pred (m-n)))]     
59          | neg n ⇒ (neg (pred ((S m)+(S n))))] ].
60
61 interpretation "integer plus" 'plus x y = (Zplus x y).
62
63 ndefinition Z_of_nat ≝
64 λn. match n with
65 [ O ⇒ OZ 
66 | S n ⇒ pos n].
67
68 nlemma fails : ∀p. p + Z_of_nat 1 = Z_of_nat 1 + p.
69 #p;nnormalize;