helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.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/opcode_base_lemmas_opcode2.ma".
  28 include "freescale/opcode_base_lemmas_instrmode2.ma".
  29 include "freescale/word16_lemmas.ma".
  30
  31 (* ********************************************** *)
  32 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  33 (* ********************************************** *)
  34
  35 nlemma anyop_destruct : ∀m.∀x1,x2:opcode.anyOP m x1 = anyOP m x2 → x1 = x2.
  36  #m; #x1; #x2; #H;
  37  nchange with (match anyOP m x2 with [ anyOP a ⇒ x1 = a ]);
  38  nrewrite < H;
  39  nnormalize;
  40  napply (refl_eq ??).
  41 nqed.
  42
  43 nlemma symmetric_eqanyop : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = eq_anyop m op2 op1.
  44  #m;
  45  ncases m;
  46  #op1; #op2;
  47  ncases op1;
  48  #x1;
  49  ncases op2;
  50  #x2;
  51  nchange with (eq_op x1 x2 = eq_op x2 x1);
  52  nrewrite > (symmetric_eqop x1 x2);
  53  napply (refl_eq ??).
  54 nqed.
  55
  56 nlemma eqanyop_to_eq : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = true → op1 = op2.
  57  #m;
  58  ncases m;
  59  #op1; #op2;
  60  ncases op1;
  61  #x1;
  62  ncases op2;
  63  #x2;
  64  nchange with ((eq_op x1 x2 = true) → ?);
  65  #H;
  66  nrewrite > (eqop_to_eq ?? H);
  67  napply (refl_eq ??).
  68 nqed.
  69
  70 nlemma eq_to_eqanyop : ∀m.∀op1,op2:any_opcode m.op1 = op2 → eq_anyop m op1 op2 = true.
  71  #m;
  72  ncases m;
  73  #op1; #op2;
  74  ncases op1;
  75  #p1;
  76  ncases op2;
  77  #p2; #H;
  78  nrewrite > (anyop_destruct ??? H);
  79  nchange with (eq_op p2 p2 = true);
  80  nrewrite > (eq_to_eqop p2 p2 (refl_eq opcode p2));
  81  napply (refl_eq ??).
  82 nqed.
  83
  84 nlemma b8w16_destruct_b8_b8 : ∀x1,x2.Byte x1 = Byte x2 → x1 = x2.
  85  #x1; #x2; #H;
  86  nchange with (match Byte x2 with [ Byte a ⇒ x1 = a | Word _ ⇒ False ]);
  87  nrewrite < H;
  88  nnormalize;
  89  napply (refl_eq ??).
  90 nqed.
  91
  92 nlemma b8w16_destruct_w16_w16 : ∀x1,x2.Word x1 = Word x2 → x1 = x2.
  93  #x1; #x2; #H;
  94  nchange with (match Word x2 with [ Word a ⇒ x1 = a | Byte _ ⇒ False ]);
  95  nrewrite < H;
  96  nnormalize;
  97  napply (refl_eq ??).
  98 nqed.
  99
 100 nlemma b8w16_destruct_b8_w16 : ∀x1,x2.Byte x1 = Word x2 → False.
 101  #x1; #x2; #H;
 102  nchange with (match Byte x1 with [ Word _ ⇒ True | Byte a ⇒ False ]);
 103  nrewrite > H;
 104  nnormalize;
 105  napply I.
 106 nqed.
 107
 108 nlemma b8w16_destruct_w16_b8 : ∀x1,x2.Word x1 = Byte x2 → False.
 109  #x1; #x2; #H;
 110  nchange with (match Word x1 with [ Word a ⇒ False | Byte _ ⇒ True ]);
 111  nrewrite > H;
 112  nnormalize;
 113  napply I.
 114 nqed.
 115
 116 nlemma symmetric_eqb8w16 : ∀bw1,bw2.eq_b8w16 bw1 bw2 = eq_b8w16 bw2 bw1.
 117  #bw1; #bw2;
 118  ncases bw1;
 119  #x1;
 120  ncases bw2;
 121  #x2;
 122  ##[ ##1: nchange with (eq_b8 x1 x2 = eq_b8 x2 x1);
 123           nrewrite > (symmetric_eqb8 x1 x2);
 124           napply (refl_eq ??)
 125  ##| ##2,3: nnormalize; napply (refl_eq ??)
 126  ##| ##4: nchange with (eq_w16 x1 x2 = eq_w16 x2 x1);
 127           nrewrite > (symmetric_eqw16 x1 x2);
 128           napply (refl_eq ??)
 129  ##]
 130 nqed.