]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/ynat_pred.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / ynat_pred.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/arith/nat_pred.ma".
16 include "ground/arith/ynat_nat.ma".
17
18 (* PREDECESSOR FOR NON-NEGATIVE INTEGERS WITH INFINITY **********************)
19
20 definition ypred_aux (n): ynat ≝
21            yinj_nat (↓n).
22
23 (*** ypred *)
24 definition ypred: ynat → ynat ≝
25            ynat_bind_nat ypred_aux (∞).
26
27 interpretation
28   "successor (non-negative integers with infinity)"
29   'DownArrow x = (ypred x).
30
31 (* Constructions ************************************************************)
32
33 (*** ypred_O *)
34 lemma ypred_inj (n): yinj_nat (↓n) = ↓(yinj_nat n).
35 @(ynat_bind_nat_inj ypred_aux)
36 qed.
37
38 (*** ypred_Y *)
39 lemma ypred_inf: ∞ = ↓∞.
40 // qed.
41
42 (* Inversions ***************************************************************)
43
44 lemma eq_inv_ypred_inj (x) (n):
45       ↓x = yinj_nat n →
46       ∃∃m. x = yinj_nat m & n = ↓m.
47 #x #n @(ynat_split_nat_inf … x) -x
48 [ #m <ypred_inj #H <(eq_inv_yinj_nat_bi … H) -n
49   /2 width=3 by ex2_intro/
50 | #H elim (eq_inv_inf_yinj_nat … H)
51 ]
52 qed-.
53
54 (*** ypred_inv_refl *)
55 lemma ypred_inv_refl (x): x = ↓x → ∨∨ 𝟎 = x | ∞ = x.
56 #x @(ynat_split_nat_inf … x) -x //
57 #n <ypred_inj #H
58 lapply (eq_inv_yinj_nat_bi … H) -H #H
59 lapply (npred_inv_refl … H) -H #H
60 /2 width=1 by or_introl/
61 qed-.