helm/software/matita/contribs/ng_assembly/freescale/oct.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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/bool.ma".
  24
  25 (* ****** *)
  26 (* OTTALI *)
  27 (* ****** *)
  28
  29 ninductive oct : Type ≝
  30   o0: oct
  31 | o1: oct
  32 | o2: oct
  33 | o3: oct
  34 | o4: oct
  35 | o5: oct
  36 | o6: oct
  37 | o7: oct.
  38
  39 (* operatore = *)
  40 ndefinition eq_oct ≝
  41 λn1,n2:oct.
  42  match n1 with
  43   [ o0 ⇒ match n2 with [ o0 ⇒ true  | _ ⇒ false ]
  44   | o1 ⇒ match n2 with [ o1 ⇒ true  | _ ⇒ false ]
  45   | o2 ⇒ match n2 with [ o2 ⇒ true  | _ ⇒ false ]
  46   | o3 ⇒ match n2 with [ o3 ⇒ true  | _ ⇒ false ]
  47   | o4 ⇒ match n2 with [ o4 ⇒ true  | _ ⇒ false ]
  48   | o5 ⇒ match n2 with [ o5 ⇒ true  | _ ⇒ false ]
  49   | o6 ⇒ match n2 with [ o6 ⇒ true  | _ ⇒ false ]
  50   | o7 ⇒ match n2 with [ o7 ⇒ true  | _ ⇒ false ]
  51   ].
  52
  53 (* iteratore sugli ottali *)
  54 ndefinition forall_oct ≝ λP.
  55  P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
  56
  57 (* operatore successore *)
  58 ndefinition succ_oct ≝
  59 λn.match n with
  60  [ o0 ⇒ o1 | o1 ⇒ o2 | o2 ⇒ o3 | o3 ⇒ o4 | o4 ⇒ o5 | o5 ⇒ o6 | o6 ⇒ o7 | o7 ⇒ o0 ].
  61
  62 (* ottali ricorsivi *)
  63 ninductive rec_oct : oct → Type ≝
  64   oc_O : rec_oct o0
  65 | oc_S : ∀n.rec_oct n → rec_oct (succ_oct n).
  66
  67 (* ottali → ottali ricorsivi *)
  68 ndefinition oct_to_recoct ≝
  69 λn.match n return λx.rec_oct x with
  70  [ o0 ⇒ oc_O
  71  | o1 ⇒ oc_S ? oc_O
  72  | o2 ⇒ oc_S ? (oc_S ? oc_O)
  73  | o3 ⇒ oc_S ? (oc_S ? (oc_S ? oc_O))
  74  | o4 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))
  75  | o5 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))
  76  | o6 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))))
  77  | o7 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))))
  78  ].