1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/Z/z".
18 include "higher_order_defs/functions.ma".
20 inductive Z : Set \def
25 definition Z_of_nat \def
26 \lambda n. match n with
28 | (S n)\Rightarrow pos n].
32 definition neg_Z_of_nat \def
33 \lambda n. match n with
35 | (S n)\Rightarrow neg n].
41 | (pos n) \Rightarrow n
42 | (neg n) \Rightarrow n].
44 definition OZ_test \def
48 | (pos n) \Rightarrow false
49 | (neg n) \Rightarrow false].
51 theorem OZ_test_to_Prop :\forall z:Z.
53 [true \Rightarrow z=OZ
54 |false \Rightarrow \lnot (z=OZ)].
60 | (pos n) \Rightarrow False
61 | (neg n) \Rightarrow False].
62 apply Hcut.rewrite > H.simplify.exact I.
66 | (pos n) \Rightarrow False
67 | (neg n) \Rightarrow False].
68 apply Hcut. rewrite > H.simplify.exact I.
72 theorem injective_pos: injective nat Z pos.
75 change with abs (pos x) = abs (pos y).
76 apply eq_f.assumption.
79 variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
82 theorem injective_neg: injective nat Z neg.
85 change with abs (neg x) = abs (neg y).
86 apply eq_f.assumption.
89 variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
92 theorem not_eq_OZ_pos: \forall n:nat. \lnot (OZ = (pos n)).
97 | (pos n) \Rightarrow False
98 | (neg n) \Rightarrow False].
103 theorem not_eq_OZ_neg :\forall n:nat. \lnot (OZ = (neg n)).
107 [ OZ \Rightarrow True
108 | (pos n) \Rightarrow False
109 | (neg n) \Rightarrow False].
114 theorem not_eq_pos_neg :\forall n,m:nat. \lnot ((pos n) = (neg m)).
118 [ OZ \Rightarrow False
119 | (pos n) \Rightarrow True
120 | (neg n) \Rightarrow False].
125 theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
129 right.apply not_eq_OZ_neg.
130 right.apply not_eq_OZ_pos.
132 apply not_eq_OZ_neg n ?.apply sym_eq.assumption.
133 elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))).
134 left.apply eq_f.assumption.
135 right.intro.apply H.apply injective_neg.assumption.
136 right.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption.
138 apply not_eq_OZ_pos n ?.apply sym_eq.assumption.
139 right.apply not_eq_pos_neg.
140 elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))).
141 left.apply eq_f.assumption.
142 right.intro.apply H.apply injective_pos.assumption.
145 (* end discrimination *)
147 definition Zsucc \def
148 \lambda z. match z with
149 [ OZ \Rightarrow pos O
150 | (pos n) \Rightarrow pos (S n)
151 | (neg n) \Rightarrow
154 | (S p) \Rightarrow neg p]].
156 definition Zpred \def
157 \lambda z. match z with
158 [ OZ \Rightarrow neg O
159 | (pos n) \Rightarrow
162 | (S p) \Rightarrow pos p]
163 | (neg n) \Rightarrow neg (S n)].
165 theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z.
166 intros.elim z.reflexivity.
172 theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z.
173 intros.elim z.reflexivity.