helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode.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 "num/oct_lemmas.ma".
  24 include "num/bitrigesim_lemmas.ma".
  25 include "num/exadecim_lemmas.ma".
  26 include "freescale/opcode_base.ma".
  27
  28 (* ********************************************** *)
  29 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  30 (* ********************************************** *)
  31
  32 nlemma instrmode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
  33  #n1; #n2; #H;
  34  nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
  35  nrewrite < H;
  36  nnormalize;
  37  napply refl_eq.
  38 nqed.
  39
  40 nlemma instrmode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
  41  #n1; #n2; #H;
  42  nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
  43  nrewrite < H;
  44  nnormalize;
  45  napply refl_eq.
  46 nqed.
  47
  48 nlemma instrmode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1 = e2.
  49  #e1; #e2; #H;
  50  nchange with (match MODE_TNY e2 with [ MODE_TNY a ⇒ e1 = a | _ ⇒ False ]);
  51  nrewrite < H;
  52  nnormalize;
  53  napply refl_eq.
  54 nqed.
  55
  56 nlemma instrmode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1 = t2.
  57  #t1; #t2; #H;
  58  nchange with (match MODE_SRT t2 with [ MODE_SRT a ⇒ t1 = a | _ ⇒ False ]);
  59  nrewrite < H;
  60  nnormalize;
  61  napply refl_eq.
  62 nqed.
  63
  64 ndefinition instrmode_destruct_aux ≝
  65 Πi1,i2.ΠP:Prop.i1 = i2 →
  66  match eq_im i1 i2 with [ true ⇒ P → P | false ⇒ P ].
  67
  68 ndefinition instrmode_destruct : instrmode_destruct_aux.
  69  #t1; #t2; #P; #H;
  70  nrewrite < H;
  71  nelim t1;
  72  nnormalize;
  73  ##[ ##31,32,33,34: #sub; nelim sub; nnormalize ##]
  74  napply (λx.x).
  75 nqed.
  76
  77 nlemma eq_to_eqim : ∀n1,n2.n1 = n2 → eq_im n1 n2 = true.
  78  #n1; #n2; #H;
  79  nrewrite > H;
  80  nelim n2;
  81  ##[ ##31,32: #n; nchange with (eq_oct n n = true); napply (eq_to_eqoct n n (refl_eq …))
  82  ##| ##33: #n; nchange with (eq_ex n n = true); napply (eq_to_eqex n n (refl_eq …))
  83  ##| ##34: #n; nchange with (eq_bit n n = true); napply (eq_to_eqbit n n (refl_eq …))
  84  ##| ##*: nnormalize; napply refl_eq
  85  ##]
  86 nqed.
  87
  88 nlemma neqim_to_neq : ∀n1,n2.eq_im n1 n2 = false → n1 ≠ n2.
  89  #n1; #n2; #H;
  90  napply (not_to_not (n1 = n2) (eq_im n1 n2 = true) …);
  91  ##[ ##1: napply (eq_to_eqim n1 n2)
  92  ##| ##2: napply (eqfalse_to_neqtrue … H)
  93  ##]
  94 nqed.
  95
  96 nlemma eqim_to_eq1 : ∀i2.eq_im MODE_INH i2 = true → MODE_INH = i2.
  97  #i2; ncases i2; nnormalize;
  98  ##[ ##1: #H; napply refl_eq
  99  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 100  ##| ##*: #H; napply (bool_destruct … H)
 101  ##]
 102 nqed.
 103
 104 nlemma eqim_to_eq2 : ∀i2.eq_im MODE_INHA i2 = true → MODE_INHA = i2.
 105  #i2; ncases i2; nnormalize;
 106  ##[ ##2: #H; napply refl_eq
 107  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 108  ##| ##*: #H; napply (bool_destruct … H)
 109  ##]
 110 nqed.
 111
 112 nlemma eqim_to_eq3 : ∀i2.eq_im MODE_INHX i2 = true → MODE_INHX = i2.
 113  #i2; ncases i2; nnormalize;
 114  ##[ ##3: #H; napply refl_eq
 115  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 116  ##| ##*: #H; napply (bool_destruct … H)
 117  ##]
 118 nqed.
 119
 120 nlemma eqim_to_eq4 : ∀i2.eq_im MODE_INHH i2 = true → MODE_INHH = i2.
 121  #i2; ncases i2; nnormalize;
 122  ##[ ##4: #H; napply refl_eq
 123  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 124  ##| ##*: #H; napply (bool_destruct … H)
 125  ##]
 126 nqed.
 127
 128 nlemma eqim_to_eq5 : ∀i2.eq_im MODE_INHX0ADD i2 = true → MODE_INHX0ADD = i2.
 129  #i2; ncases i2; nnormalize;
 130  ##[ ##5: #H; napply refl_eq
 131  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 132  ##| ##*: #H; napply (bool_destruct … H)
 133  ##]
 134 nqed.
 135
 136 nlemma eqim_to_eq6 : ∀i2.eq_im MODE_INHX1ADD i2 = true → MODE_INHX1ADD = i2.
 137  #i2; ncases i2; nnormalize;
 138  ##[ ##6: #H; napply refl_eq
 139  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 140  ##| ##*: #H; napply (bool_destruct … H)
 141  ##]
 142 nqed.
 143
 144 nlemma eqim_to_eq7 : ∀i2.eq_im MODE_INHX2ADD i2 = true → MODE_INHX2ADD = i2.
 145  #i2; ncases i2; nnormalize;
 146  ##[ ##7: #H; napply refl_eq
 147  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 148  ##| ##*: #H; napply (bool_destruct … H)
 149  ##]
 150 nqed.
 151
 152 nlemma eqim_to_eq8 : ∀i2.eq_im MODE_IMM1 i2 = true → MODE_IMM1 = i2.
 153  #i2; ncases i2; nnormalize;
 154  ##[ ##8: #H; napply refl_eq
 155  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 156  ##| ##*: #H; napply (bool_destruct … H)
 157  ##]
 158 nqed.
 159
 160 nlemma eqim_to_eq9 : ∀i2.eq_im MODE_IMM1EXT i2 = true → MODE_IMM1EXT = i2.
 161  #i2; ncases i2; nnormalize;
 162  ##[ ##9: #H; napply refl_eq
 163  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 164  ##| ##*: #H; napply (bool_destruct … H)
 165  ##]
 166 nqed.
 167
 168 nlemma eqim_to_eq10 : ∀i2.eq_im MODE_IMM2 i2 = true → MODE_IMM2 = i2.
 169  #i2; ncases i2; nnormalize;
 170  ##[ ##10: #H; napply refl_eq
 171  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 172  ##| ##*: #H; napply (bool_destruct … H)
 173  ##]
 174 nqed.
 175
 176 nlemma eqim_to_eq11 : ∀i2.eq_im MODE_DIR1 i2 = true → MODE_DIR1 = i2.
 177  #i2; ncases i2; nnormalize;
 178  ##[ ##11: #H; napply refl_eq
 179  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 180  ##| ##*: #H; napply (bool_destruct … H)
 181  ##]
 182 nqed.
 183
 184 nlemma eqim_to_eq12 : ∀i2.eq_im MODE_DIR2 i2 = true → MODE_DIR2 = i2.
 185  #i2; ncases i2; nnormalize;
 186  ##[ ##12: #H; napply refl_eq
 187  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 188  ##| ##*: #H; napply (bool_destruct … H)
 189  ##]
 190 nqed.
 191
 192 nlemma eqim_to_eq13 : ∀i2.eq_im MODE_IX0 i2 = true → MODE_IX0 = i2.
 193  #i2; ncases i2; nnormalize;
 194  ##[ ##13: #H; napply refl_eq
 195  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 196  ##| ##*: #H; napply (bool_destruct … H)
 197  ##]
 198 nqed.
 199
 200 nlemma eqim_to_eq14 : ∀i2.eq_im MODE_IX1 i2 = true → MODE_IX1 = i2.
 201  #i2; ncases i2; nnormalize;
 202  ##[ ##14: #H; napply refl_eq
 203  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 204  ##| ##*: #H; napply (bool_destruct … H)
 205  ##]
 206 nqed.
 207
 208 nlemma eqim_to_eq15 : ∀i2.eq_im MODE_IX2 i2 = true → MODE_IX2 = i2.
 209  #i2; ncases i2; nnormalize;
 210  ##[ ##15: #H; napply refl_eq
 211  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 212  ##| ##*: #H; napply (bool_destruct … H)
 213  ##]
 214 nqed.
 215
 216 nlemma eqim_to_eq16 : ∀i2.eq_im MODE_SP1 i2 = true → MODE_SP1 = i2.
 217  #i2; ncases i2; nnormalize;
 218  ##[ ##16: #H; napply refl_eq
 219  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 220  ##| ##*: #H; napply (bool_destruct … H)
 221  ##]
 222 nqed.
 223
 224 nlemma eqim_to_eq17 : ∀i2.eq_im MODE_SP2 i2 = true → MODE_SP2 = i2.
 225  #i2; ncases i2; nnormalize;
 226  ##[ ##17: #H; napply refl_eq
 227  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 228  ##| ##*: #H; napply (bool_destruct … H)
 229  ##]
 230 nqed.
 231
 232 nlemma eqim_to_eq18 : ∀i2.eq_im MODE_DIR1_to_DIR1 i2 = true → MODE_DIR1_to_DIR1 = i2.
 233  #i2; ncases i2; nnormalize;
 234  ##[ ##18: #H; napply refl_eq
 235  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 236  ##| ##*: #H; napply (bool_destruct … H)
 237  ##]
 238 nqed.
 239
 240 nlemma eqim_to_eq19 : ∀i2.eq_im MODE_IMM1_to_DIR1 i2 = true → MODE_IMM1_to_DIR1 = i2.
 241  #i2; ncases i2; nnormalize;
 242  ##[ ##19: #H; napply refl_eq
 243  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 244  ##| ##*: #H; napply (bool_destruct … H)
 245  ##]
 246 nqed.
 247
 248 nlemma eqim_to_eq20 : ∀i2.eq_im MODE_IX0p_to_DIR1 i2 = true → MODE_IX0p_to_DIR1 = i2.
 249  #i2; ncases i2; nnormalize;
 250  ##[ ##20: #H; napply refl_eq
 251  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 252  ##| ##*: #H; napply (bool_destruct … H)
 253  ##]
 254 nqed.
 255
 256 nlemma eqim_to_eq21 : ∀i2.eq_im MODE_DIR1_to_IX0p i2 = true → MODE_DIR1_to_IX0p = i2.
 257  #i2; ncases i2; nnormalize;
 258  ##[ ##21: #H; napply refl_eq
 259  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 260  ##| ##*: #H; napply (bool_destruct … H)
 261  ##]
 262 nqed.
 263
 264 nlemma eqim_to_eq22 : ∀i2.eq_im MODE_INHA_and_IMM1 i2 = true → MODE_INHA_and_IMM1 = i2.
 265  #i2; ncases i2; nnormalize;
 266  ##[ ##22: #H; napply refl_eq
 267  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 268  ##| ##*: #H; napply (bool_destruct … H)
 269  ##]
 270 nqed.
 271
 272 nlemma eqim_to_eq23 : ∀i2.eq_im MODE_INHX_and_IMM1 i2 = true → MODE_INHX_and_IMM1 = i2.
 273  #i2; ncases i2; nnormalize;
 274  ##[ ##23: #H; napply refl_eq
 275  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 276  ##| ##*: #H; napply (bool_destruct … H)
 277  ##]
 278 nqed.
 279
 280 nlemma eqim_to_eq24 : ∀i2.eq_im MODE_IMM1_and_IMM1 i2 = true → MODE_IMM1_and_IMM1 = i2.
 281  #i2; ncases i2; nnormalize;
 282  ##[ ##24: #H; napply refl_eq
 283  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 284  ##| ##*: #H; napply (bool_destruct … H)
 285  ##]
 286 nqed.
 287
 288 nlemma eqim_to_eq25 : ∀i2.eq_im MODE_DIR1_and_IMM1 i2 = true → MODE_DIR1_and_IMM1 = i2.
 289  #i2; ncases i2; nnormalize;
 290  ##[ ##25: #H; napply refl_eq
 291  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 292  ##| ##*: #H; napply (bool_destruct … H)
 293  ##]
 294 nqed.
 295
 296 nlemma eqim_to_eq26 : ∀i2.eq_im MODE_IX0_and_IMM1 i2 = true → MODE_IX0_and_IMM1 = i2.
 297  #i2; ncases i2; nnormalize;
 298  ##[ ##26: #H; napply refl_eq
 299  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 300  ##| ##*: #H; napply (bool_destruct … H)
 301  ##]
 302 nqed.
 303
 304 nlemma eqim_to_eq27 : ∀i2.eq_im MODE_IX0p_and_IMM1 i2 = true → MODE_IX0p_and_IMM1 = i2.
 305  #i2; ncases i2; nnormalize;
 306  ##[ ##27: #H; napply refl_eq
 307  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 308  ##| ##*: #H; napply (bool_destruct … H)
 309  ##]
 310 nqed.
 311
 312 nlemma eqim_to_eq28 : ∀i2.eq_im MODE_IX1_and_IMM1 i2 = true → MODE_IX1_and_IMM1 = i2.
 313  #i2; ncases i2; nnormalize;
 314  ##[ ##28: #H; napply refl_eq
 315  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 316  ##| ##*: #H; napply (bool_destruct … H)
 317  ##]
 318 nqed.
 319
 320 nlemma eqim_to_eq29 : ∀i2.eq_im MODE_IX1p_and_IMM1 i2 = true → MODE_IX1p_and_IMM1 = i2.
 321  #i2; ncases i2; nnormalize;
 322  ##[ ##29: #H; napply refl_eq
 323  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 324  ##| ##*: #H; napply (bool_destruct … H)
 325  ##]
 326 nqed.
 327
 328 nlemma eqim_to_eq30 : ∀i2.eq_im MODE_SP1_and_IMM1 i2 = true → MODE_SP1_and_IMM1 = i2.
 329  #i2; ncases i2; nnormalize;
 330  ##[ ##30: #H; napply refl_eq
 331  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 332  ##| ##*: #H; napply (bool_destruct … H)
 333  ##]
 334 nqed.
 335
 336 nlemma eqim_to_eq31 : ∀n1,i2.eq_im (MODE_DIRn n1) i2 = true → MODE_DIRn n1 = i2.
 337  #n1; #i2; ncases i2;
 338  ##[ ##31: #n2; #H;
 339      nchange in H:(%) with (eq_oct n1 n2 = true);
 340      nrewrite > (eqoct_to_eq … H);
 341      napply refl_eq
 342  ##| ##32,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
 343  ##| ##*: nnormalize; #H; napply (bool_destruct … H)
 344  ##]
 345 nqed.
 346
 347 nlemma eqim_to_eq32 : ∀n1,i2.eq_im (MODE_DIRn_and_IMM1 n1) i2 = true → MODE_DIRn_and_IMM1 n1 = i2.
 348  #n1; #i2; ncases i2;
 349  ##[ ##32: #n2; #H;
 350      nchange in H:(%) with (eq_oct n1 n2 = true);
 351      nrewrite > (eqoct_to_eq … H);
 352      napply refl_eq
 353  ##| ##31,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
 354  ##| ##*: nnormalize; #H; napply (bool_destruct … H)
 355  ##]
 356 nqed.
 357
 358 nlemma eqim_to_eq33 : ∀n1,i2.eq_im (MODE_TNY n1) i2 = true → MODE_TNY n1 = i2.
 359  #n1; #i2; ncases i2;
 360  ##[ ##33: #n2; #H;
 361      nchange in H:(%) with (eq_ex n1 n2 = true);
 362      nrewrite > (eqex_to_eq … H);
 363      napply refl_eq
 364  ##| ##31,32,34: nnormalize; #n2; #H; napply (bool_destruct … H)
 365  ##| ##*: nnormalize; #H; napply (bool_destruct … H)
 366  ##]
 367 nqed.
 368
 369 nlemma eqim_to_eq34 : ∀n1,i2.eq_im (MODE_SRT n1) i2 = true → MODE_SRT n1 = i2.
 370  #n1; #i2; ncases i2;
 371  ##[ ##34: #n2; #H;
 372      nchange in H:(%) with (eq_bit n1 n2 = true);
 373      nrewrite > (eqbit_to_eq … H);
 374      napply refl_eq
 375  ##| ##31,32,33: nnormalize; #n2; #H; napply (bool_destruct … H)
 376  ##| ##*: nnormalize; #H; napply (bool_destruct … H)
 377  ##]
 378 nqed.
 379
 380 nlemma eqim_to_eq : ∀i1,i2.eq_im i1 i2 = true → i1 = i2.
 381  #i1; ncases i1;
 382  ##[ ##1: napply eqim_to_eq1 ##| ##2: napply eqim_to_eq2
 383  ##| ##3: napply eqim_to_eq3 ##| ##4: napply eqim_to_eq4
 384  ##| ##5: napply eqim_to_eq5 ##| ##6: napply eqim_to_eq6
 385  ##| ##7: napply eqim_to_eq7 ##| ##8: napply eqim_to_eq8
 386  ##| ##9: napply eqim_to_eq9 ##| ##10: napply eqim_to_eq10
 387  ##| ##11: napply eqim_to_eq11 ##| ##12: napply eqim_to_eq12
 388  ##| ##13: napply eqim_to_eq13 ##| ##14: napply eqim_to_eq14
 389  ##| ##15: napply eqim_to_eq15 ##| ##16: napply eqim_to_eq16
 390  ##| ##17: napply eqim_to_eq17 ##| ##18: napply eqim_to_eq18
 391  ##| ##19: napply eqim_to_eq19 ##| ##20: napply eqim_to_eq20
 392  ##| ##21: napply eqim_to_eq21 ##| ##22: napply eqim_to_eq22
 393  ##| ##23: napply eqim_to_eq23 ##| ##24: napply eqim_to_eq24
 394  ##| ##25: napply eqim_to_eq25 ##| ##26: napply eqim_to_eq26
 395  ##| ##27: napply eqim_to_eq27 ##| ##28: napply eqim_to_eq28
 396  ##| ##29: napply eqim_to_eq29 ##| ##30: napply eqim_to_eq30
 397  ##| ##31: napply eqim_to_eq31 ##| ##32: napply eqim_to_eq32
 398  ##| ##33: napply eqim_to_eq33 ##| ##34: napply eqim_to_eq34
 399  ##]
 400 nqed.
 401
 402 nlemma neq_to_neqim : ∀n1,n2.n1 ≠ n2 → eq_im n1 n2 = false.
 403  #n1; #n2; #H;
 404  napply (neqtrue_to_eqfalse (eq_im n1 n2));
 405  napply (not_to_not (eq_im n1 n2 = true) (n1 = n2) ? H);
 406  napply (eqim_to_eq n1 n2).
 407 nqed.
 408
 409 nlemma decidable_im : ∀x,y:instr_mode.decidable (x = y).
 410  #x; #y; nnormalize;
 411  napply (or2_elim (eq_im x y = true) (eq_im x y = false) ? (decidable_bexpr ?));
 412  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqim_to_eq … H))
 413  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqim_to_neq … H))
 414  ##]
 415 nqed.
 416
 417 nlemma symmetric_eqim : symmetricT instr_mode bool eq_im.
 418  #n1; #n2;
 419  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_im n1 n2));
 420  ##[ ##1: #H; nrewrite > H; napply refl_eq
 421  ##| ##2: #H; nrewrite > (neq_to_neqim n1 n2 H);
 422           napply (symmetric_eq ? (eq_im n2 n1) false);
 423           napply (neq_to_neqim n2 n1 (symmetric_neq ? n1 n2 H))
 424  ##]
 425 nqed.