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