matita/matita/contribs/ng_assembly/num/quatern.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 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/bool.ma".
  24
  25 (* ********** *)
  26 (* QUATERNARI *)
  27 (* ********** *)
  28
  29 ninductive quatern : Type ≝
  30   q0 : quatern
  31 | q1 : quatern
  32 | q2 : quatern
  33 | q3 : quatern.
  34
  35 (* operatore = *)
  36 ndefinition eq_qu ≝
  37 λn1,n2:quatern.
  38  match n1 with
  39   [ q0 ⇒ match n2 with [ q0 ⇒ true | _ ⇒ false ]
  40   | q1 ⇒ match n2 with [ q1 ⇒ true | _ ⇒ false ]
  41   | q2 ⇒ match n2 with [ q2 ⇒ true | _ ⇒ false ]
  42   | q3 ⇒ match n2 with [ q3 ⇒ true | _ ⇒ false ]
  43   ].
  44
  45 (* iteratore sui quaternari *)
  46 ndefinition forall_qu ≝ λP.
  47  P q0 ⊗ P q1 ⊗ P q2 ⊗ P q3.
  48
  49 (* operatore successorre *)
  50 ndefinition succ_qu ≝
  51 λn.match n with
  52  [ q0 ⇒ q1 | q1 ⇒ q2 | q2 ⇒ q3 | q3 ⇒ q0 ].
  53
  54 (* quaternari ricorsivi *)
  55 ninductive rec_quatern : quatern → Type ≝
  56   qu_O : rec_quatern q0
  57 | qu_S : ∀n.rec_quatern n → rec_quatern (succ_qu n).
  58
  59 (* quaternari → quaternari ricorsivi *)
  60 ndefinition qu_to_recqu ≝
  61 λn.match n return λx.rec_quatern x with
  62  [ q0 ⇒ qu_O
  63  | q1 ⇒ qu_S ? qu_O
  64  | q2 ⇒ qu_S ? (qu_S ? qu_O)
  65  | q3 ⇒ qu_S ? (qu_S ? (qu_S ? qu_O))
  66  ].