helm/software/matita/contribs/ng_assembly/freescale/translation_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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/translation.ma".
  24 include "num/byte8_lemmas.ma".
  25
  26 (* ******************************************************* *)
  27 (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
  28 (* ******************************************************* *)
  29
  30 nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
  31  #m; #b1; #b2; #H;
  32  nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
  33  nrewrite < H;
  34  nnormalize;
  35  napply refl_eq.
  36 nqed.
  37
  38 nlemma symmetric_eqtbyte8 : ∀m.∀tb1,tb2:t_byte8 m.eq_tbyte8 m tb1 tb2 = eq_tbyte8 m tb2 tb1.
  39  #m; #tb1; nelim tb1; #b1; #tb2; nelim tb2; #b2;
  40  nchange with ((eq_b8 b1 b2) = (eq_b8 b2 b1));
  41  napply (symmetric_eqb8 b1 b2).
  42 nqed.
  43
  44 nlemma eqtbyte8_to_eq : ∀m.∀tb1,tb2:t_byte8 m.eq_tbyte8 m tb1 tb2 = true → tb1 = tb2.
  45  #m; #tb1; nelim tb1; #b1; #tb2; nelim tb2; #b2;
  46  nchange with ((eq_b8 b1 b2 = true) → ?);
  47  #H;
  48  nrewrite > (eqb8_to_eq b1 b2 H);
  49  napply refl_eq.
  50 nqed.
  51
  52 nlemma eq_to_eqtbyte8 : ∀m.∀tb1,tb2:t_byte8 m.tb1 = tb2 → eq_tbyte8 m tb1 tb2 = true.
  53  #m; #tb1; nelim tb1; #b1; #tb2; nelim tb2; #b2;
  54  nchange with (? → (eq_b8 b1 b2 = true));
  55  #H;
  56  nrewrite > (tbyte8_destruct m … H);
  57  nrewrite > (eq_to_eqb8 b2 b2 (refl_eq …));
  58  napply refl_eq.
  59 nqed.
  60
  61 nlemma decidable_tbyte8 : ∀m.∀x,y:t_byte8 m.decidable (x = y).
  62  #m; #x; nelim x; #e1; #y; nelim y; #e2;
  63  nnormalize;
  64  napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 e1 e2) …);
  65  ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (tbyte8_destruct m … H1))
  66  ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
  67  ##]
  68 nqed.
  69
  70 nlemma neqtbyte8_to_neq : ∀m.∀tb1,tb2:t_byte8 m.(eq_tbyte8 m tb1 tb2 = false) → (tb1 ≠ tb2).
  71  #m; #tb1; nelim tb1; #b1; #tb2; nelim tb2; #b2;
  72  nchange with (((eq_b8 b1 b2) = false) → ?);
  73  #H;
  74  nnormalize;
  75  #H1;
  76  napply (neqb8_to_neq … H);
  77  napply (tbyte8_destruct m … H1).
  78 nqed.
  79
  80 nlemma neq_to_neqtbyte8 : ∀m.∀tb1,tb2:t_byte8 m.tb1 ≠ tb2 → eq_tbyte8 m tb1 tb2 = false.
  81  #m; #tb1; nelim tb1; #b1; #tb2; nelim tb2; #b2;
  82  #H; nchange with ((eq_b8 b1 b2) = false);
  83  napply (neq_to_neqb8 b1 b2 ?);
  84  nnormalize;
  85  #H1;
  86  nrewrite > H1 in H:(%); #H;
  87  napply (H (refl_eq …)).
  88 nqed.