matita/matita/contribs/lambdadelta/ground_2/etc/ynat_old/ynat.etc

   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 "arithmetics/nat.ma".
  16
  17 (* INFINITARY NATURAL NUMBERS ***********************************************)
  18
  19 (* the type of infinitary natural numbers *)
  20 coinductive ynat: Type[0] ≝
  21 | YO: ynat
  22 | YS: ynat → ynat
  23 .
  24
  25 interpretation "ynat successor" 'Successor m = (YS m).
  26
  27 (* the coercion of nat to ynat *)
  28 let rec ynat_of_nat n ≝ match n with
  29 [ O   ⇒ YO
  30 | S m ⇒ YS (ynat_of_nat m)
  31 ].
  32
  33 coercion ynat_of_nat.
  34
  35 (* the infinity *)
  36 let corec Y : ynat ≝ ⫯Y.
  37
  38 interpretation "ynat infinity" 'Infinity = Y.
  39
  40 (* destructing identity on ynat *)
  41 definition yid: ynat → ynat ≝ λm. match m with
  42 [ YO   ⇒ 0
  43 | YS n ⇒ ⫯n
  44 ].
  45
  46 (* Properties ***************************************************************)
  47
  48 fact yid_rew: ∀n. yid n = n.
  49 * // qed-.
  50
  51 lemma Y_rew: ⫯∞ = ∞.
  52 <(yid_rew ∞) in ⊢ (???%); //
  53 qed.