helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.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/bool_lemmas.ma".
  28 include "freescale/opcode_base.ma".
  29
  30 (* ********************************************** *)
  31 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  32 (* ********************************************** *)
  33
  34 ndefinition mcu_type_destruct_aux ≝
  35 Πm1,m2:mcu_type.ΠP:Prop.m1 = m2 →
  36  match m1 with
  37   [ HC05 ⇒ match m2 with [ HC05 ⇒ P → P | _ ⇒ P ]
  38   | HC08 ⇒ match m2 with [ HC08 ⇒ P → P | _ ⇒ P ]
  39   | HCS08 ⇒ match m2 with [ HCS08 ⇒ P → P | _ ⇒ P ]
  40   | RS08 ⇒ match m2 with [ RS08 ⇒ P → P | _ ⇒ P ]
  41   ].
  42
  43 ndefinition mcu_type_destruct : mcu_type_destruct_aux.
  44  #m1; #m2; #P;
  45  nelim m1;
  46  ##[ ##1: nelim m2; nnormalize; #H;
  47           ##[ ##1: napply (λx:P.x)
  48           ##| ##*: napply (False_ind ??);
  49                    nchange with (match HC05 with [ HC05 ⇒ False | _ ⇒ True ]);
  50                    nrewrite > H; nnormalize; napply I
  51           ##]
  52  ##| ##2: nelim m2; nnormalize; #H;
  53           ##[ ##2: napply (λx:P.x)
  54           ##| ##*: napply (False_ind ??);
  55                    nchange with (match HC08 with [ HC08 ⇒ False | _ ⇒ True ]);
  56                    nrewrite > H; nnormalize; napply I
  57           ##]
  58  ##| ##3: nelim m2; nnormalize; #H;
  59           ##[ ##3: napply (λx:P.x)
  60           ##| ##*: napply (False_ind ??);
  61                    nchange with (match HCS08 with [ HCS08 ⇒ False | _ ⇒ True ]);
  62                    nrewrite > H; nnormalize; napply I
  63           ##]
  64  ##| ##4: nelim m2; nnormalize; #H;
  65           ##[ ##4: napply (λx:P.x)
  66           ##| ##*: napply (False_ind ??);
  67                    nchange with (match RS08 with [ RS08 ⇒ False | _ ⇒ True ]);
  68                    nrewrite > H; nnormalize; napply I
  69           ##]
  70  ##]
  71 nqed.
  72
  73 nlemma symmetric_eqmcutype : symmetricT mcu_type bool eq_mcutype.
  74  #m1; #m2;
  75  nelim m1;
  76  nelim m2;
  77  nnormalize;
  78  napply (refl_eq ??).
  79 nqed.
  80
  81 nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m2).
  82  #m1; #m2;
  83  ncases m1;
  84  ncases m2;
  85  nnormalize;
  86  ##[ ##1,6,11,16: #H; napply (refl_eq ??)
  87  ##| ##*: #H; napply (bool_destruct ??? H)
  88  ##]
  89 nqed.
  90
  91 nlemma eq_to_eqmcutype : ∀m1,m2.m1 = m2 → eq_mcutype m1 m2 = true.
  92  #m1; #m2;
  93  ncases m1;
  94  ncases m2;
  95  nnormalize;
  96  ##[ ##1,6,11,16: #H; napply (refl_eq ??)
  97  ##| ##*: #H; napply (mcu_type_destruct ??? H)
  98  ##]
  99 nqed.
 100
 101 nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
 102  #n1; #n2; #H;
 103  nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
 104  nrewrite < H;
 105  nnormalize;
 106  napply (refl_eq ??).
 107 nqed.
 108
 109 nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
 110  #n1; #n2; #H;
 111  nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
 112  nrewrite < H;
 113  nnormalize;
 114  napply (refl_eq ??).
 115 nqed.
 116
 117 nlemma instr_mode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1 = e2.
 118  #e1; #e2; #H;
 119  nchange with (match MODE_TNY e2 with [ MODE_TNY a ⇒ e1 = a | _ ⇒ False ]);
 120  nrewrite < H;
 121  nnormalize;
 122  napply (refl_eq ??).
 123 nqed.
 124
 125 nlemma instr_mode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1 = t2.
 126  #t1; #t2; #H;
 127  nchange with (match MODE_SRT t2 with [ MODE_SRT a ⇒ t1 = a | _ ⇒ False ]);
 128  nrewrite < H;
 129  nnormalize;
 130  napply (refl_eq ??).
 131 nqed.