helm/software/matita/contribs/ng_assembly/num/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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/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 (* iteratore sugli ottali *)
  40 ndefinition forall_oct ≝ λP.
  41  P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
  42
  43 (* operatore = *)
  44 ndefinition eq_oct ≝
  45 λn1,n2:oct.
  46  match n1 with
  47   [ o0 ⇒ match n2 with [ o0 ⇒ true  | _ ⇒ false ]
  48   | o1 ⇒ match n2 with [ o1 ⇒ true  | _ ⇒ false ]
  49   | o2 ⇒ match n2 with [ o2 ⇒ true  | _ ⇒ false ]
  50   | o3 ⇒ match n2 with [ o3 ⇒ true  | _ ⇒ false ]
  51   | o4 ⇒ match n2 with [ o4 ⇒ true  | _ ⇒ false ]
  52   | o5 ⇒ match n2 with [ o5 ⇒ true  | _ ⇒ false ]
  53   | o6 ⇒ match n2 with [ o6 ⇒ true  | _ ⇒ false ]
  54   | o7 ⇒ match n2 with [ o7 ⇒ true  | _ ⇒ false ]
  55   ].
  56
  57 (* operatore and *)
  58 ndefinition and_oct ≝
  59 λe1,e2:oct.match e1 with
  60  [ o0 ⇒ match e2 with
  61   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0
  62   | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o0 | o7 ⇒ o0 ]
  63  | o1 ⇒ match e2 with
  64   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1
  65   | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o0 | o7 ⇒ o1 ]
  66  | o2 ⇒ match e2 with
  67   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2
  68   | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o2 | o7 ⇒ o2 ]
  69  | o3 ⇒ match e2 with
  70   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
  71   | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ]
  72  | o4 ⇒ match e2 with
  73   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0
  74   | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o4 | o7 ⇒ o4 ]
  75  | o5 ⇒ match e2 with
  76   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1
  77   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o4 | o7 ⇒ o5 ]
  78  | o6 ⇒ match e2 with
  79   [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2
  80   | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o6 | o7 ⇒ o6 ]
  81  | o7 ⇒ match e2 with
  82   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
  83   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
  84  ].
  85
  86 (* operatore or *)
  87 ndefinition or_oct ≝
  88 λe1,e2:oct.match e1 with
  89  [ o0 ⇒ match e2 with
  90   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
  91   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
  92  | o1 ⇒ match e2 with
  93   [ o0 ⇒ o1 | o1 ⇒ o1 | o2 ⇒ o3 | o3 ⇒ o3
  94   | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
  95  | o2 ⇒ match e2 with
  96   [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o2 | o3 ⇒ o3
  97   | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
  98  | o3 ⇒ match e2 with
  99   [ o0 ⇒ o3 | o1 ⇒ o3 | o2 ⇒ o3 | o3 ⇒ o3
 100   | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
 101  | o4 ⇒ match e2 with
 102   [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7
 103   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
 104  | o5 ⇒ match e2 with
 105   [ o0 ⇒ o5 | o1 ⇒ o5 | o2 ⇒ o7 | o3 ⇒ o7
 106   | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
 107  | o6 ⇒ match e2 with
 108   [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o6 | o3 ⇒ o7
 109   | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
 110  | o7 ⇒ match e2 with
 111   [ o0 ⇒ o7 | o1 ⇒ o7 | o2 ⇒ o7 | o3 ⇒ o7
 112   | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
 113  ].
 114
 115 (* operatore xor *)
 116 ndefinition xor_oct ≝
 117 λe1,e2:oct.match e1 with
 118  [ o0 ⇒ match e2 with
 119   [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
 120   | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
 121  | o1 ⇒ match e2 with
 122   [ o0 ⇒ o1 | o1 ⇒ o0 | o2 ⇒ o3 | o3 ⇒ o2
 123   | o4 ⇒ o5 | o5 ⇒ o4 | o6 ⇒ o7 | o7 ⇒ o6 ]
 124  | o2 ⇒ match e2 with
 125   [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o0 | o3 ⇒ o1
 126   | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o4 | o7 ⇒ o5 ]
 127  | o3 ⇒ match e2 with
 128   [ o0 ⇒ o3 | o1 ⇒ o2 | o2 ⇒ o1 | o3 ⇒ o0
 129   | o4 ⇒ o7 | o5 ⇒ o6 | o6 ⇒ o5 | o7 ⇒ o4 ]
 130  | o4 ⇒ match e2 with
 131   [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7
 132   | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ]
 133  | o5 ⇒ match e2 with
 134   [ o0 ⇒ o5 | o1 ⇒ o4 | o2 ⇒ o7 | o3 ⇒ o6
 135   | o4 ⇒ o1 | o5 ⇒ o0 | o6 ⇒ o3 | o7 ⇒ o2 ]
 136  | o6 ⇒ match e2 with
 137   [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o4 | o3 ⇒ o5
 138   | o4 ⇒ o2 | o5 ⇒ o3 | o6 ⇒ o0 | o7 ⇒ o1 ]
 139  | o7 ⇒ match e2 with
 140   [ o0 ⇒ o7 | o1 ⇒ o6 | o2 ⇒ o5 | o3 ⇒ o4
 141   | o4 ⇒ o3 | o5 ⇒ o2 | o6 ⇒ o1 | o7 ⇒ o0 ]
 142  ].
 143
 144 (* operatore successore *)
 145 ndefinition succ_oct ≝
 146 λn.match n with
 147  [ o0 ⇒ o1 | o1 ⇒ o2 | o2 ⇒ o3 | o3 ⇒ o4 | o4 ⇒ o5 | o5 ⇒ o6 | o6 ⇒ o7 | o7 ⇒ o0 ].
 148
 149 (* ottali ricorsivi *)
 150 ninductive rec_oct : oct → Type ≝
 151   oc_O : rec_oct o0
 152 | oc_S : ∀n.rec_oct n → rec_oct (succ_oct n).
 153
 154 (* ottali → ottali ricorsivi *)
 155 ndefinition oct_to_recoct ≝
 156 λn.match n return λx.rec_oct x with
 157  [ o0 ⇒ oc_O
 158  | o1 ⇒ oc_S ? oc_O
 159  | o2 ⇒ oc_S ? (oc_S ? oc_O)
 160  | o3 ⇒ oc_S ? (oc_S ? (oc_S ? oc_O))
 161  | o4 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))
 162  | o5 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))
 163  | o6 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))))
 164  | o7 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))))
 165  ].