From b3f8b89278d193ed0aa0f39e7f8d74cf1de81d8d Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 29 Nov 2013 16:33:57 +0000
Subject: [PATCH] addition for natural numbers with infinity

---
 .../lambdadelta/ground_2/lib/arith.ma         |  4 ++
 .../lambdadelta/ground_2/web/ground_2_src.tbl |  2 +-
 .../lambdadelta/ground_2/ynat/ynat_plus.ma    | 57 +++++++++++++++++++
 .../lambdadelta/ground_2/ynat/ynat_succ.ma    |  5 ++
 4 files changed, 67 insertions(+), 1 deletion(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 732c1b64c..0cbcff85e 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -134,6 +134,10 @@ lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b).
 #B #f #b #l elim l -l normalize //
 qed.
 
+lemma iter_plus: ∀B:Type[0]. ∀f:B→B. ∀b,l1,l2. f^(l1+l2) b = f^l1 (f^l2 b).
+#B #f #b #l1 elim l1 -l1 normalize //
+qed.
+
 (* Trichotomy operator ******************************************************)
 
 (* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index 8bc1e8538..827a8fcf8 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -8,7 +8,7 @@ table {
    ]
    class "yellow"
    [ { "natural numbers with infinity" * } {
-        [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?&lt;? )" * ]
+        [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?&lt;? )" "ynat_plus ( ? + ? )" * ]
      }
    ]
    class "orange"
diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
new file mode 100644
index 000000000..8f348733e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground_2/ynat/ynat_lt.ma".
+
+(* NATURAL NUMBERS WITH INFINITY ********************************************)
+
+(* addition *)
+definition yplus: ynat → ynat → ynat ≝ λx,y. match x with
+[ yinj m ⇒ ysucc^m y
+| Y      ⇒ Y
+].
+
+interpretation "ynat plus" 'plus x y = (yplus x y).
+
+(* Properties on successor **************************************************)
+
+lemma yplus_succ1: ∀m,n. (⫯m) + n = ⫯(m + n).
+* //
+qed.
+
+lemma yplus_SO1: ∀m. 1 + m = ⫯m.
+* //
+qed. 
+
+(* Basic properties *********************************************************)
+
+lemma yplus_inj: ∀m,n. yinj m + yinj n = yinj (m + n).
+#m elim m -m //
+#m #IHm #n >(yplus_succ1 m) >IHm -IHm //
+qed.
+
+lemma yplus_Y2: ∀m. (m + ∞) = ∞.
+* normalize //
+qed.
+
+lemma yplus_comm: commutative … yplus.
+* [ #m ] * [1,3: #n ] //
+normalize >ysucc_iter_Y //
+qed.
+
+lemma yplus_assoc: associative … yplus.
+* // #x * //
+#y #z >yplus_inj whd in ⊢ (??%%); >iter_plus //
+qed.
+
diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
index c244b9cae..a8d1946be 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
@@ -38,6 +38,11 @@ lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m. n = ⫯m.
 ]
 qed-.
 
+lemma ysucc_iter_Y: ∀m. ysucc^m (∞) = ∞.
+#m elim m -m //
+#m #IHm whd in ⊢ (??%?); >IHm //
+qed.
+
 (* Inversion lemmas *********************************************************)
 
 lemma ysucc_inj: ∀m,n. ⫯m = ⫯n → m = n.
-- 
2.39.2