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/nat/nat".
17 include "logic/equality.ma".
18 include "logic/connectives.ma".
19 include "higher_order_defs/functions.ma".
21 inductive nat : Set \def
25 definition pred: nat \to nat \def
26 \lambda n:nat. match n with
28 | (S p) \Rightarrow p ].
30 theorem pred_Sn : \forall n:nat.n=(pred (S n)).
34 theorem injective_S : injective nat nat S.
39 apply eq_f. assumption.
42 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m
45 theorem not_eq_S : \forall n,m:nat.
46 \lnot n=m \to \lnot (S n = S m).
47 intros. simplify. intros.
48 apply H. apply injective_S. assumption.
51 definition not_zero : nat \to Prop \def
55 | (S p) \Rightarrow True ].
57 theorem not_eq_O_S : \forall n:nat. \lnot O=S n.
58 intros. simplify. intros.
64 theorem not_eq_n_Sn : \forall n:nat. \lnot n=S n.
67 apply not_eq_S.assumption.
71 \forall n:nat.\forall P:nat \to Prop.
72 P O \to (\forall m:nat. P (S m)) \to P n.
73 intros.elim n.assumption.apply H1.
77 \forall R:nat \to nat \to Prop.
78 (\forall n:nat. R O n) \to
79 (\forall n:nat. R (S n) O) \to
80 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
83 apply nat_case m.apply H1.
84 intros.apply H2. apply H3.