X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Fz.ma;fp=helm%2Fmatita%2Flibrary%2FZ%2Fz.ma;h=ea50a2cd9c3b70729df6c8c6bb4b16d661d80d41;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hp=0000000000000000000000000000000000000000;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953;p=helm.git

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
new file mode 100644
index 000000000..ea50a2cd9
--- /dev/null
+++ b/helm/matita/library/Z/z.ma
@@ -0,0 +1,173 @@
+(**************************************************************************)
+(*       ___	                                                            *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/Z/z".
+
+include "datatypes/bool.ma".
+include "nat/nat.ma".
+
+inductive Z : Set \def
+  OZ : Z
+| pos : nat \to Z
+| neg : nat \to Z.
+
+definition Z_of_nat \def
+\lambda n. match n with
+[ O \Rightarrow  OZ 
+| (S n)\Rightarrow  pos n].
+
+coercion cic:/matita/Z/z/Z_of_nat.con.
+
+definition neg_Z_of_nat \def
+\lambda n. match n with
+[ O \Rightarrow  OZ 
+| (S n)\Rightarrow  neg n].
+
+definition abs \def
+\lambda z.
+ match z with 
+[ OZ \Rightarrow O
+| (pos n) \Rightarrow n
+| (neg n) \Rightarrow n].
+
+definition OZ_test \def
+\lambda z.
+match z with 
+[ OZ \Rightarrow true
+| (pos n) \Rightarrow false
+| (neg n) \Rightarrow false].
+
+theorem OZ_test_to_Prop :\forall z:Z.
+match OZ_test z with
+[true \Rightarrow z=OZ 
+|false \Rightarrow z \neq OZ].
+intros.elim z.
+simplify.reflexivity.
+simplify. unfold Not. intros (H).
+discriminate H.
+simplify. unfold Not. intros (H).
+discriminate H.
+qed.
+
+(* discrimination *)
+theorem injective_pos: injective nat Z pos.
+unfold injective.
+intros.
+change with (abs (pos x) = abs (pos y)).
+apply eq_f.assumption.
+qed.
+
+variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
+\def injective_pos.
+
+theorem injective_neg: injective nat Z neg.
+unfold injective.
+intros.
+change with (abs (neg x) = abs (neg y)).
+apply eq_f.assumption.
+qed.
+
+variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
+\def injective_neg.
+
+theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
+unfold Not.intros (n H).
+discriminate H.
+qed.
+
+theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
+unfold Not.intros (n H).
+discriminate H.
+qed.
+
+theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
+unfold Not.intros (n m H).
+discriminate H.
+qed.
+
+theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
+intros.unfold decidable.
+elim x.
+(* goal: x=OZ *)
+  elim y.
+  (* goal: x=OZ y=OZ *)
+    left.reflexivity.
+  (* goal: x=OZ 2=2 *)
+    right.apply not_eq_OZ_pos.
+  (* goal: x=OZ 2=3 *)
+    right.apply not_eq_OZ_neg.
+(* goal: x=pos *)
+  elim y.
+  (* goal: x=pos y=OZ *)
+    right.unfold Not.intro.
+    apply (not_eq_OZ_pos n). symmetry. assumption.
+  (* goal: x=pos y=pos *)
+    elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
+    left.apply eq_f.assumption.
+    right.unfold Not.intros (H_inj).apply H. injection H_inj. assumption.
+  (* goal: x=pos y=neg *)
+    right.unfold Not.intro.apply (not_eq_pos_neg n n1). assumption.
+(* goal: x=neg *)
+  elim y.
+  (* goal: x=neg y=OZ *)
+    right.unfold Not.intro.
+    apply (not_eq_OZ_neg n). symmetry. assumption.
+  (* goal: x=neg y=pos *)
+    right. unfold Not.intro. apply (not_eq_pos_neg n1 n). symmetry. assumption.
+  (* goal: x=neg y=neg *)
+    elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
+    left.apply eq_f.assumption.
+    right.unfold Not.intro.apply H.apply injective_neg.assumption.
+qed.
+
+(* end discrimination *)
+
+definition Zsucc \def
+\lambda z. match z with
+[ OZ \Rightarrow pos O
+| (pos n) \Rightarrow pos (S n)
+| (neg n) \Rightarrow 
+	  match n with
+	  [ O \Rightarrow OZ
+	  | (S p) \Rightarrow neg p]].
+
+definition Zpred \def
+\lambda z. match z with
+[ OZ \Rightarrow neg O
+| (pos n) \Rightarrow 
+	  match n with
+	  [ O \Rightarrow OZ
+	  | (S p) \Rightarrow pos p]
+| (neg n) \Rightarrow neg (S n)].
+
+theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z.
+intros.
+elim z.
+  reflexivity.
+  reflexivity.
+  elim n.
+    reflexivity.
+    reflexivity.
+qed.
+
+theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z.
+intros.
+elim z.
+  reflexivity.
+  elim n.
+    reflexivity.
+    reflexivity.
+  reflexivity.
+qed.
+