helm/software/matita/contribs/ng_assembly/freescale/exadecim_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:                                                         *)
  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/bool_lemmas.ma".
  28 include "freescale/exadecim.ma".
  29
  30 (* *********** *)
  31 (* ESADECIMALI *)
  32 (* *********** *)
  33
  34 ndefinition exadecim_destruct :
  35  Πe1,e2:exadecim.ΠP:Prop.e1 = e2 →
  36  match e1 with
  37   [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ]
  38   | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
  39   | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ]
  40   | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
  41   | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ]
  42   | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
  43   | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ]
  44   | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
  45   | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ]
  46   | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
  47   | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ]
  48   | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
  49   | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ]
  50   | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
  51   | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ]
  52   | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
  53   ].
  54  #e1; #e2; #P;
  55  nelim e1;
  56  ##[ ##1: nelim e2; nnormalize; #H;
  57           ##[ ##1: napply (λx:P.x)
  58           ##| ##*: napply (False_ind ??);
  59                    nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
  60                    nrewrite > H; nnormalize; napply I
  61           ##]
  62  ##| ##2: nelim e2; nnormalize; #H;
  63           ##[ ##2: napply (λx:P.x)
  64           ##| ##*: napply (False_ind ??);
  65                    nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
  66                    nrewrite > H; nnormalize; napply I
  67           ##]
  68  ##| ##3: nelim e2; nnormalize; #H;
  69           ##[ ##3: napply (λx:P.x)
  70           ##| ##*: napply (False_ind ??);
  71                    nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
  72                    nrewrite > H; nnormalize; napply I
  73           ##]
  74  ##| ##4: nelim e2; nnormalize; #H;
  75           ##[ ##4: napply (λx:P.x)
  76           ##| ##*: napply (False_ind ??);
  77                    nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
  78                    nrewrite > H; nnormalize; napply I
  79           ##]
  80  ##| ##5: nelim e2; nnormalize; #H;
  81           ##[ ##5: napply (λx:P.x)
  82           ##| ##*: napply (False_ind ??);
  83                    nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
  84                    nrewrite > H; nnormalize; napply I
  85           ##]
  86  ##| ##6: nelim e2; nnormalize; #H;
  87           ##[ ##6: napply (λx:P.x)
  88           ##| ##*: napply (False_ind ??);
  89                    nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
  90                    nrewrite > H; nnormalize; napply I
  91           ##]
  92  ##| ##7: nelim e2; nnormalize; #H;
  93           ##[ ##7: napply (λx:P.x)
  94           ##| ##*: napply (False_ind ??);
  95                    nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
  96                    nrewrite > H; nnormalize; napply I
  97           ##]
  98  ##| ##8: nelim e2; nnormalize; #H;
  99           ##[ ##8: napply (λx:P.x)
 100           ##| ##*: napply (False_ind ??);
 101                    nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
 102                    nrewrite > H; nnormalize; napply I
 103           ##]
 104  ##| ##9: nelim e2; nnormalize; #H;
 105           ##[ ##9: napply (λx:P.x)
 106           ##| ##*: napply (False_ind ??);
 107                    nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
 108                    nrewrite > H; nnormalize; napply I
 109           ##]
 110  ##| ##10: nelim e2; nnormalize; #H;
 111           ##[ ##10: napply (λx:P.x)
 112           ##| ##*: napply (False_ind ??);
 113                    nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
 114                    nrewrite > H; nnormalize; napply I
 115           ##]
 116  ##| ##11: nelim e2; nnormalize; #H;
 117           ##[ ##11: napply (λx:P.x)
 118           ##| ##*: napply (False_ind ??);
 119                    nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
 120                    nrewrite > H; nnormalize; napply I
 121           ##]
 122  ##| ##12: nelim e2; nnormalize; #H;
 123           ##[ ##12: napply (λx:P.x)
 124           ##| ##*: napply (False_ind ??);
 125                    nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
 126                    nrewrite > H; nnormalize; napply I
 127           ##]
 128  ##| ##13: nelim e2; nnormalize; #H;
 129           ##[ ##13: napply (λx:P.x)
 130           ##| ##*: napply (False_ind ??);
 131                    nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
 132                    nrewrite > H; nnormalize; napply I
 133           ##]
 134  ##| ##14: nelim e2; nnormalize; #H;
 135           ##[ ##14: napply (λx:P.x)
 136           ##| ##*: napply (False_ind ??);
 137                    nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
 138                    nrewrite > H; nnormalize; napply I
 139           ##]
 140  ##| ##15: nelim e2; nnormalize; #H;
 141           ##[ ##15: napply (λx:P.x)
 142           ##| ##*: napply (False_ind ??);
 143                    nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
 144                    nrewrite > H; nnormalize; napply I
 145           ##]
 146  ##| ##16: nelim e2; nnormalize; #H;
 147           ##[ ##16: napply (λx:P.x)
 148           ##| ##*: napply (False_ind ??);
 149                    nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
 150                    nrewrite > H; nnormalize; napply I
 151           ##]
 152  ##]
 153 nqed.
 154
 155 nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
 156  #e1; #e2;
 157  nelim e1;
 158  nelim e2;
 159  nnormalize;
 160  napply (refl_eq ??).
 161 nqed.
 162
 163 nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
 164  #e1; #e2;
 165  nelim e1;
 166  nelim e2;
 167  nnormalize;
 168  napply (refl_eq ??).
 169 nqed.
 170
 171 nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
 172  #e1; #e2; #e3;
 173  nelim e1;
 174  ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 175  ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 176  ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 177  ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 178  ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 179  ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 180  ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 181  ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 182  ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 183  ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 184  ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 185  ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 186  ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 187  ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 188  ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 189  ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 190  ##]
 191 nqed.
 192
 193 nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
 194  #e1; #e2;
 195  nelim e1;
 196  nelim e2;
 197  nnormalize;
 198  napply (refl_eq ??).
 199 nqed.
 200
 201 nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
 202  #e1; #e2; #e3;
 203  nelim e1;
 204  ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 205  ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 206  ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 207  ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 208  ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 209  ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 210  ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 211  ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 212  ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 213  ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 214  ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 215  ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 216  ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 217  ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 218  ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 219  ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 220  ##]
 221 nqed.
 222
 223 nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
 224  #e1; #e2;
 225  nelim e1;
 226  nelim e2;
 227  nnormalize;
 228  napply (refl_eq ??).
 229 nqed.
 230
 231 nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
 232  #e1; #e2; #e3;
 233  nelim e1;
 234  ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 235  ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 236  ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 237  ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 238  ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 239  ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 240  ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 241  ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 242  ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 243  ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 244  ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 245  ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 246  ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 247  ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 248  ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 249  ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 250  ##]
 251 nqed.
 252
 253 nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc e2 e1 c.
 254  #e1; #e2; #c;
 255  nelim e1;
 256  nelim e2;
 257  nelim c;
 258  nnormalize;
 259  napply (refl_eq ??).
 260 nqed.
 261
 262 nlemma plusex_dc_dc_to_dc_d : ∀e1,e2,c.fst ?? (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_d e1 e2 c.
 263  #e1; #e2; #c;
 264  nelim e1;
 265  nelim e2;
 266  nelim c;
 267  nnormalize;
 268  napply (refl_eq ??).
 269 nqed.
 270
 271 nlemma plusex_dc_dc_to_dc_c : ∀e1,e2,c.snd ?? (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_c e1 e2 c.
 272  #e1; #e2; #c;
 273  nelim e1;
 274  nelim e2;
 275  nelim c;
 276  nnormalize;
 277  napply (refl_eq ??).
 278 nqed.
 279
 280 nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2.
 281  #e1; #e2;
 282  nelim e1;
 283  nelim e2;
 284  nnormalize;
 285  napply (refl_eq ??).
 286 nqed.
 287
 288 nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst ?? (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
 289  #e1; #e2;
 290  nelim e1;
 291  nelim e2;
 292  nnormalize;
 293  napply (refl_eq ??).
 294 nqed.
 295
 296 nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd ?? (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
 297  #e1; #e2;
 298  nelim e1;
 299  nelim e2;
 300  nnormalize;
 301  napply (refl_eq ??).
 302 nqed.
 303
 304 nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c.
 305  #e1; #e2; #c;
 306  nelim e1;
 307  nelim e2;
 308  nelim c;
 309  nnormalize;
 310  napply (refl_eq ??).
 311 nqed.
 312
 313 nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c.
 314  #e1; #e2; #c;
 315  nelim e1;
 316  nelim e2;
 317  nelim c;
 318  nnormalize;
 319  napply (refl_eq ??).
 320 nqed.
 321
 322 nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
 323  #e1; #e2;
 324  nelim e1;
 325  nelim e2;
 326  nnormalize;
 327  napply (refl_eq ??).
 328 nqed.
 329
 330 nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst ?? (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
 331  #e1; #e2;
 332  nelim e1;
 333  nelim e2;
 334  nnormalize;
 335  napply (refl_eq ??).
 336 nqed.
 337
 338 nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd ?? (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
 339  #e1; #e2;
 340  nelim e1;
 341  nelim e2;
 342  nnormalize;
 343  napply (refl_eq ??).
 344 nqed.
 345
 346 nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
 347  #e1; #e2;
 348  nelim e1;
 349  nelim e2;
 350  nnormalize;
 351  napply (refl_eq ??).
 352 nqed.
 353
 354 nlemma associative_plusex_d_d : ∀e1,e2,e3.(plus_ex_d_d (plus_ex_d_d e1 e2) e3) = (plus_ex_d_d e1 (plus_ex_d_d e2 e3)).
 355  #e1; #e2; #e3;
 356  nelim e1;
 357  ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 358  ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 359  ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 360  ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 361  ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 362  ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 363  ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 364  ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 365  ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 366  ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 367  ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 368  ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 369  ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 370  ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 371  ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 372  ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 373  ##]
 374 nqed.
 375
 376 nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
 377  #e1; #e2;
 378  nelim e1;
 379  nelim e2;
 380  nnormalize;
 381  napply (refl_eq ??).
 382 nqed.
 383
 384 nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
 385  #e1; #e2; #H;
 386  nletin K ≝ (bool_destruct ?? (e1 = e2) H);
 387  nelim e1 in K:(%) ⊢ %;
 388  nelim e2;
 389  nnormalize;
 390  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (refl_eq ??)
 391  ##| ##*: #H; napply H
 392  ##]
 393 nqed.
 394
 395 nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
 396  #e1; #e2; #H;
 397  nletin K ≝ (exadecim_destruct ?? (eq_ex e1 e2 = true) H);
 398  nelim e1 in K:(%) ⊢ %;
 399  nelim e2;
 400  nnormalize;
 401  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (refl_eq ??)
 402  ##| ##*: #H; napply H
 403  ##]
 404 nqed.