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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/opcode_base_lemmas_opcode.ma".
  24 include "freescale/opcode_base_lemmas_instrmode.ma".
  25 include "num/word16_lemmas.ma".
  26
  27 (* ********************************************** *)
  28 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  29 (* ********************************************** *)
  30
  31 nlemma anyop_destruct : ∀m.∀x1,x2:opcode.anyOP m x1 = anyOP m x2 → x1 = x2.
  32  #m; #x1; #x2; #H;
  33  nchange with (match anyOP m x2 with [ anyOP a ⇒ x1 = a ]);
  34  nrewrite < H;
  35  nnormalize;
  36  napply refl_eq.
  37 nqed.
  38
  39 nlemma symmetric_eqanyop : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = eq_anyop m op2 op1.
  40  #m;
  41  ncases m;
  42  #op1; #op2;
  43  ncases op1;
  44  #x1;
  45  ncases op2;
  46  #x2;
  47  nchange with (eq_op x1 x2 = eq_op x2 x1);
  48  nrewrite > (symmetric_eqop x1 x2);
  49  napply refl_eq.
  50 nqed.
  51
  52 nlemma eqanyop_to_eq : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = true → op1 = op2.
  53  #m;
  54  ncases m;
  55  #op1; #op2;
  56  ncases op1;
  57  #x1;
  58  ncases op2;
  59  #x2;
  60  nchange with ((eq_op x1 x2 = true) → ?);
  61  #H;
  62  nrewrite > (eqop_to_eq … H);
  63  napply refl_eq.
  64 nqed.
  65
  66 nlemma eq_to_eqanyop : ∀m.∀op1,op2:any_opcode m.op1 = op2 → eq_anyop m op1 op2 = true.
  67  #m;
  68  ncases m;
  69  #op1; #op2;
  70  ncases op1;
  71  #p1;
  72  ncases op2;
  73  #p2; #H;
  74  nrewrite > (anyop_destruct … H);
  75  nchange with (eq_op p2 p2 = true);
  76  nrewrite > (eq_to_eqop p2 p2 (refl_eq opcode p2));
  77  napply refl_eq.
  78 nqed.
  79
  80 nlemma decidable_anyop : ∀m.∀x,y:any_opcode m.decidable (x = y).
  81  #m; #x; nelim x; #e1; #y; nelim y; #e2;
  82  nnormalize;
  83  napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_op e1 e2) …);
  84  ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (anyop_destruct m … H1))
  85  ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
  86  ##]
  87 nqed.
  88
  89 nlemma neqanyop_to_neq : ∀m.∀op1,op2:any_opcode m.(eq_anyop m op1 op2 = false) → (op1 ≠ op2).
  90  #m; #op1; nelim op1; #e1; #op2; nelim op2; #e2;
  91  nchange with (((eq_op e1 e2) = false) → ?);
  92  #H;
  93  nnormalize;
  94  #H1;
  95  napply (neqop_to_neq … H);
  96  napply (anyop_destruct m … H1).
  97 nqed.
  98
  99 nlemma neq_to_neqanyop : ∀m.∀op1,op2:any_opcode m.op1 ≠ op2 → eq_anyop m op1 op2 = false.
 100  #m; #op1; nelim op1; #e1; #op2; nelim op2; #e2;
 101  #H; nchange with ((eq_op e1 e2) = false);
 102  napply (neq_to_neqop e1 e2 ?);
 103  nnormalize;
 104  #H1;
 105  nrewrite > H1 in H:(%); #H;
 106  napply (H (refl_eq …)).
 107 nqed.
 108
 109 nlemma b8w16_destruct_b8_b8 : ∀x1,x2.Byte x1 = Byte x2 → x1 = x2.
 110  #x1; #x2; #H;
 111  nchange with (match Byte x2 with [ Byte a ⇒ x1 = a | Word _ ⇒ False ]);
 112  nrewrite < H;
 113  nnormalize;
 114  napply refl_eq.
 115 nqed.
 116
 117 nlemma b8w16_destruct_w16_w16 : ∀x1,x2.Word x1 = Word x2 → x1 = x2.
 118  #x1; #x2; #H;
 119  nchange with (match Word x2 with [ Word a ⇒ x1 = a | Byte _ ⇒ False ]);
 120  nrewrite < H;
 121  nnormalize;
 122  napply refl_eq.
 123 nqed.
 124
 125 nlemma b8w16_destruct_b8_w16 : ∀x1,x2.Byte x1 = Word x2 → False.
 126  #x1; #x2; #H;
 127  nchange with (match Byte x1 with [ Word _ ⇒ True | Byte a ⇒ False ]);
 128  nrewrite > H;
 129  nnormalize;
 130  napply I.
 131 nqed.
 132
 133 nlemma b8w16_destruct_w16_b8 : ∀x1,x2.Word x1 = Byte x2 → False.
 134  #x1; #x2; #H;
 135  nchange with (match Word x1 with [ Word a ⇒ False | Byte _ ⇒ True ]);
 136  nrewrite > H;
 137  nnormalize;
 138  napply I.
 139 nqed.
 140
 141 nlemma symmetric_eqb8w16 : ∀bw1,bw2.eq_b8w16 bw1 bw2 = eq_b8w16 bw2 bw1.
 142  #bw1; #bw2;
 143  ncases bw1;
 144  #x1;
 145  ncases bw2;
 146  #x2;
 147  ##[ ##1: nchange with (eq_b8 x1 x2 = eq_b8 x2 x1);
 148           nrewrite > (symmetric_eqb8 x1 x2);
 149           napply refl_eq
 150  ##| ##2,3: nnormalize; napply refl_eq
 151  ##| ##4: nchange with (eq_w16 x1 x2 = eq_w16 x2 x1);
 152           nrewrite > (symmetric_eqw16 x1 x2);
 153           napply refl_eq
 154  ##]
 155 nqed.
 156
 157 nlemma eqb8w16_to_eq : ∀bw1,bw2.eq_b8w16 bw1 bw2 = true → bw1 = bw2.
 158  #bw1; #bw2;
 159  ncases bw1; #e1; ncases bw2; #e2;
 160  ##[ ##1: nchange with ((eq_b8 e1 e2 = true) → ?); #H; nrewrite > (eqb8_to_eq … H); napply refl_eq
 161  ##| ##2,3: nnormalize; #H; napply (bool_destruct … H)
 162  ##| ##4: nchange with ((eq_w16 e1 e2 = true) → ?); #H; nrewrite > (eqw16_to_eq … H); napply refl_eq
 163  ##]
 164 nqed.
 165
 166 nlemma eq_to_eqb8w16 : ∀bw1,bw2.bw1 = bw2 → eq_b8w16 bw1 bw2 = true.
 167  #bw1; #bw2;
 168  ncases bw1; #e1; ncases bw2; #e2;
 169  ##[ ##1: #H; nrewrite > (b8w16_destruct_b8_b8 … H);
 170           nchange with (eq_b8 e2 e2 = true);
 171           nrewrite > (eq_to_eqb8 e2 e2 (refl_eq …));
 172           napply refl_eq
 173  ##| ##2: #H; nelim (b8w16_destruct_b8_w16 … H)
 174  ##| ##3: #H; nelim (b8w16_destruct_w16_b8 … H);
 175  ##| ##4: #H; nrewrite > (b8w16_destruct_w16_w16 … H);
 176           nchange with (eq_w16 e2 e2 = true);
 177           nrewrite > (eq_to_eqw16 e2 e2 (refl_eq …));
 178           napply refl_eq
 179  ##]
 180 nqed.
 181
 182 nlemma decidable_b8w16 : ∀x,y:byte8_or_word16.decidable (x = y).
 183  #x; nelim x; #e1; #y; nelim y; #e2;
 184  nnormalize;
 185  ##[ ##1: napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 e1 e2) …);
 186           ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (b8w16_destruct_b8_b8 … H1))
 187           ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 188           ##]
 189  ##| ##2: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply (b8w16_destruct_b8_w16 … H)
 190  ##| ##3: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply (b8w16_destruct_w16_b8 … H)
 191  ##| ##4: napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 e1 e2) …);
 192           ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (b8w16_destruct_w16_w16 … H1))
 193           ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 194           ##]
 195  ##]
 196 nqed.
 197
 198 nlemma neqb8w16_to_neq : ∀bw1,bw2.eq_b8w16 bw1 bw2 = false → bw1 ≠ bw2.
 199  #bw1; #bw2;
 200  ncases bw1; #e1; ncases bw2; #e2;
 201  ##[ ##1: nchange with ((eq_b8 e1 e2 = false) → ?); #H;
 202           nnormalize; #H1; napply (neqb8_to_neq … H); napply (b8w16_destruct_b8_b8 … H1)
 203  ##| ##2: nnormalize; #H; #H1; napply (b8w16_destruct_b8_w16 … H1)
 204  ##| ##3: nnormalize; #H; #H1; napply (b8w16_destruct_w16_b8 … H1)
 205  ##| ##4: nchange with ((eq_w16 e1 e2 = false) → ?); #H;
 206           nnormalize; #H1; napply (neqw16_to_neq … H); napply (b8w16_destruct_w16_w16 … H1)
 207  ##]
 208 nqed.