matita/contribs/assembly/freescale/aux_bases.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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/word16.ma".
  28
  29 (* ************************ *)
  30 (* DEFINIZIONE DEGLI OTTALI *)
  31 (* ************************ *)
  32
  33 inductive oct : Type ≝
  34   o0: oct
  35 | o1: oct
  36 | o2: oct
  37 | o3: oct
  38 | o4: oct
  39 | o5: oct
  40 | o6: oct
  41 | o7: oct.
  42
  43 (* ottali → esadecimali *)
  44 definition exadecim_of_oct ≝
  45 λo:oct.
  46  match o with
  47   [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3
  48   | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].
  49
  50 coercion cic:/matita/freescale/aux_bases/exadecim_of_oct.con.
  51
  52 (* iteratore sugli ottali *)
  53 definition forall_oct ≝ λP.
  54  P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
  55
  56 (* ***************************** *)
  57 (* DEFINIZIONE DEI BITRIGESIMALI *)
  58 (* ***************************** *)
  59
  60 inductive bitrigesim : Type ≝
  61   t00: bitrigesim
  62 | t01: bitrigesim
  63 | t02: bitrigesim
  64 | t03: bitrigesim
  65 | t04: bitrigesim
  66 | t05: bitrigesim
  67 | t06: bitrigesim
  68 | t07: bitrigesim
  69 | t08: bitrigesim
  70 | t09: bitrigesim
  71 | t0A: bitrigesim
  72 | t0B: bitrigesim
  73 | t0C: bitrigesim
  74 | t0D: bitrigesim
  75 | t0E: bitrigesim
  76 | t0F: bitrigesim
  77 | t10: bitrigesim
  78 | t11: bitrigesim
  79 | t12: bitrigesim
  80 | t13: bitrigesim
  81 | t14: bitrigesim
  82 | t15: bitrigesim
  83 | t16: bitrigesim
  84 | t17: bitrigesim
  85 | t18: bitrigesim
  86 | t19: bitrigesim
  87 | t1A: bitrigesim
  88 | t1B: bitrigesim
  89 | t1C: bitrigesim
  90 | t1D: bitrigesim
  91 | t1E: bitrigesim
  92 | t1F: bitrigesim.
  93
  94 (* bitrigesimali → byte *)
  95 definition byte8_of_bitrigesim ≝
  96 λt:bitrigesim.
  97  match t with
  98   [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
  99   | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
 100   | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
 101   | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
 102   | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
 103   | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
 104   | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
 105   | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉 ].
 106
 107 coercion cic:/matita/freescale/aux_bases/byte8_of_bitrigesim.con.
 108
 109 (* iteratore sui bitrigesimali *)
 110 definition forall_bitrigesim ≝ λP.
 111  P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗
 112  P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗
 113  P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗
 114  P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F.