helm/software/matita/contribs/ng_assembly/freescale/byte8_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/exadecim_lemmas.ma".
  28 include "freescale/byte8.ma".
  29
  30 (* **** *)
  31 (* BYTE *)
  32 (* **** *)
  33
  34 nlemma byte8_destruct_1 :
  35 ∀x1,x2,y1,y2.
  36  mk_byte8 x1 y1 = mk_byte8 x2 y2 → x1 = x2.
  37  #x1; #x2; #y1; #y2; #H;
  38  nchange with (match mk_byte8 x2 y2 with [ mk_byte8 a _ ⇒ x1 = a ]);
  39  nrewrite < H;
  40  nnormalize;
  41  napply (refl_eq ??).
  42 nqed.
  43
  44 nlemma byte8_destruct_2 :
  45 ∀x1,x2,y1,y2.
  46  mk_byte8 x1 y1 = mk_byte8 x2 y2 → y1 = y2.
  47  #x1; #x2; #y1; #y2; #H;
  48  nchange with (match mk_byte8 x2 y2 with [ mk_byte8 _ b ⇒ y1 = b ]);
  49  nrewrite < H;
  50  nnormalize;
  51  napply (refl_eq ??).
  52 nqed.
  53
  54 nlemma symmetric_eqb8 : symmetricT byte8 bool eq_b8.
  55  #b1; #b2;
  56  nelim b1;
  57  nelim b2;
  58  #e1; #e2; #e3; #e4;
  59  nchange with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = ((eq_ex e1 e3)⊗(eq_ex e2 e4)));
  60  nrewrite > (symmetric_eqex e1 e3);
  61  nrewrite > (symmetric_eqex e2 e4);
  62  napply (refl_eq ??).
  63 nqed.
  64
  65 nlemma symmetric_andb8 : symmetricT byte8 byte8 and_b8.
  66  #b1; #b2;
  67  nelim b1;
  68  nelim b2;
  69  #e1; #e2; #e3; #e4;
  70  nchange with ((mk_byte8 (and_ex e3 e1) (and_ex e4 e2)) = (mk_byte8 (and_ex e1 e3) (and_ex e2 e4)));
  71  nrewrite > (symmetric_andex e1 e3);
  72  nrewrite > (symmetric_andex e2 e4);
  73  napply (refl_eq ??).
  74 nqed.
  75
  76 nlemma associative_andb8 : ∀b1,b2,b3.(and_b8 (and_b8 b1 b2) b3) = (and_b8 b1 (and_b8 b2 b3)).
  77  #b1; #b2; #b3;
  78  nelim b1;
  79  #e1; #e2;
  80  nelim b2;
  81  #e3; #e4;
  82  nelim b3;
  83  #e5; #e6;
  84  nchange with (mk_byte8 (and_ex (and_ex e1 e3) e5) (and_ex (and_ex e2 e4) e6) =
  85   mk_byte8 (and_ex e1 (and_ex e3 e5)) (and_ex e2 (and_ex e4 e6)));
  86  nrewrite < (associative_andex e1 e3 e5);
  87  nrewrite < (associative_andex e2 e4 e6);
  88  napply (refl_eq ??).
  89 nqed.
  90
  91 nlemma symmetric_orb8 : symmetricT byte8 byte8 or_b8.
  92  #b1; #b2;
  93  nelim b1;
  94  nelim b2;
  95  #e1; #e2; #e3; #e4;
  96  nchange with ((mk_byte8 (or_ex e3 e1) (or_ex e4 e2)) = (mk_byte8 (or_ex e1 e3) (or_ex e2 e4)));
  97  nrewrite > (symmetric_orex e1 e3);
  98  nrewrite > (symmetric_orex e2 e4);
  99  napply (refl_eq ??).
 100 nqed.
 101
 102 nlemma associative_orb8 : ∀b1,b2,b3.(or_b8 (or_b8 b1 b2) b3) = (or_b8 b1 (or_b8 b2 b3)).
 103  #b1; #b2; #b3;
 104  nelim b1;
 105  #e1; #e2;
 106  nelim b2;
 107  #e3; #e4;
 108  nelim b3;
 109  #e5; #e6;
 110  nchange with (mk_byte8 (or_ex (or_ex e1 e3) e5) (or_ex (or_ex e2 e4) e6) =
 111   mk_byte8 (or_ex e1 (or_ex e3 e5)) (or_ex e2 (or_ex e4 e6)));
 112  nrewrite < (associative_orex e1 e3 e5);
 113  nrewrite < (associative_orex e2 e4 e6);
 114  napply (refl_eq ??).
 115 nqed.
 116
 117 nlemma symmetric_xorb8 : symmetricT byte8 byte8 xor_b8.
 118  #b1; #b2;
 119  nelim b1;
 120  nelim b2;
 121  #e1; #e2; #e3; #e4;
 122  nchange with ((mk_byte8 (xor_ex e3 e1) (xor_ex e4 e2)) = (mk_byte8 (xor_ex e1 e3) (xor_ex e2 e4)));
 123  nrewrite > (symmetric_xorex e1 e3);
 124  nrewrite > (symmetric_xorex e2 e4);
 125  napply (refl_eq ??).
 126 nqed.
 127
 128 nlemma associative_xorb8 : ∀b1,b2,b3.(xor_b8 (xor_b8 b1 b2) b3) = (xor_b8 b1 (xor_b8 b2 b3)).
 129  #b1; #b2; #b3;
 130  nelim b1;
 131  #e1; #e2;
 132  nelim b2;
 133  #e3; #e4;
 134  nelim b3;
 135  #e5; #e6;
 136  nchange with (mk_byte8 (xor_ex (xor_ex e1 e3) e5) (xor_ex (xor_ex e2 e4) e6) =
 137   mk_byte8 (xor_ex e1 (xor_ex e3 e5)) (xor_ex e2 (xor_ex e4 e6)));
 138  nrewrite < (associative_xorex e1 e3 e5);
 139  nrewrite < (associative_xorex e2 e4 e6);
 140  napply (refl_eq ??).
 141 nqed.
 142
 143 nlemma symmetric_plusb8_dc_dc : ∀b1,b2,c.plus_b8_dc_dc b1 b2 c = plus_b8_dc_dc b2 b1 c.
 144  #b1; #b2; #c;
 145  nelim b1;
 146  #e1; #e2;
 147  nelim b2;
 148  #e3; #e4;
 149  nchange with (
 150   match plus_ex_dc_dc e2 e4 c with
 151    [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
 152     [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]] =
 153   match plus_ex_dc_dc e4 e2 c with
 154    [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
 155     [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]]);
 156  nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
 157  ncases (plus_ex_dc_dc e2 e4 c);
 158  #e5; #c1;
 159  nchange with (
 160   match plus_ex_dc_dc e1 e3 c1 with
 161    [ pair h c' ⇒ pair ?? 〈h,e5〉 c' ] =
 162   match plus_ex_dc_dc e3 e1 c1 with
 163    [ pair h c' ⇒ pair ?? 〈h,e5〉 c' ]);
 164  nrewrite > (symmetric_plusex_dc_dc e1 e3 c1);
 165  napply (refl_eq ??).
 166 nqed.
 167
 168 nlemma symmetric_plusb8_dc_d : ∀b1,b2,c.plus_b8_dc_d b1 b2 c = plus_b8_dc_d b2 b1 c.
 169  #b1; #b2; #c;
 170  nelim b1;
 171  #e1; #e2;
 172  nelim b2;
 173  #e3; #e4;
 174  nchange with (
 175   match plus_ex_dc_dc e2 e4 c with
 176    [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
 177   match plus_ex_dc_dc e4 e2 c with
 178    [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
 179  nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
 180  ncases (plus_ex_dc_dc e2 e4 c);
 181  #e5; #c1;
 182  nchange with (〈plus_ex_dc_d e1 e3 c1,e5〉 = 〈plus_ex_dc_d e3 e1 c1,e5〉);
 183  nrewrite > (symmetric_plusex_dc_d e1 e3 c1);
 184  napply (refl_eq ??).
 185 nqed.
 186
 187 nlemma symmetric_plusb8_dc_c : ∀b1,b2,c.plus_b8_dc_c b1 b2 c = plus_b8_dc_c b2 b1 c.
 188  #b1; #b2; #c;
 189  nelim b1;
 190  #e1; #e2;
 191  nelim b2;
 192  #e3; #e4;
 193  nchange with (
 194   plus_ex_dc_c e1 e3 (plus_ex_dc_c e2 e4 c) =
 195   plus_ex_dc_c e3 e1 (plus_ex_dc_c e4 e2 c));
 196  nrewrite > (symmetric_plusex_dc_c e4 e2 c);
 197  nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_dc_c e2 e4 c));
 198  napply (refl_eq ??).
 199 nqed.
 200
 201 nlemma symmetric_plusb8_d_dc : ∀b1,b2.plus_b8_d_dc b1 b2 = plus_b8_d_dc b2 b1.
 202  #b1; #b2;
 203  nelim b1;
 204  #e1; #e2;
 205  nelim b2;
 206  #e3; #e4;
 207  nchange with (
 208   match plus_ex_d_dc e2 e4 with
 209    [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
 210     [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]] =
 211   match plus_ex_d_dc e4 e2 with
 212    [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
 213     [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]]);
 214  nrewrite > (symmetric_plusex_d_dc e4 e2);
 215  ncases (plus_ex_d_dc e2 e4);
 216  #e5; #c;
 217  nchange with (
 218   match plus_ex_dc_dc e1 e3 c with
 219    [ pair h c' ⇒ pair ?? 〈h,e5〉 c' ] =
 220   match plus_ex_dc_dc e3 e1 c with
 221    [ pair h c' ⇒ pair ?? 〈h,e5〉 c' ]);
 222  nrewrite > (symmetric_plusex_dc_dc e1 e3 c);
 223  napply (refl_eq ??).
 224 nqed.
 225
 226 nlemma symmetric_plusb8_d_d : ∀b1,b2.plus_b8_d_d b1 b2 = plus_b8_d_d b2 b1.
 227  #b1; #b2;
 228  nelim b1;
 229  #e1; #e2;
 230  nelim b2;
 231  #e3; #e4;
 232  nchange with (
 233   match plus_ex_d_dc e2 e4 with
 234    [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
 235   match plus_ex_d_dc e4 e2 with
 236    [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
 237  nrewrite > (symmetric_plusex_d_dc e4 e2);
 238  ncases (plus_ex_d_dc e2 e4);
 239  #e5; #c;
 240  nchange with (〈plus_ex_dc_d e1 e3 c,e5〉 = 〈plus_ex_dc_d e3 e1 c,e5〉);
 241  nrewrite > (symmetric_plusex_dc_d e1 e3 c);
 242  napply (refl_eq ??).
 243 nqed.
 244
 245 nlemma symmetric_plusb8_d_c : ∀b1,b2.plus_b8_d_c b1 b2 = plus_b8_d_c b2 b1.
 246  #b1; #b2;
 247  nelim b1;
 248  #e1; #e2;
 249  nelim b2;
 250  #e3; #e4;
 251  nchange with (
 252   plus_ex_dc_c e1 e3 (plus_ex_d_c e2 e4) =
 253   plus_ex_dc_c e3 e1 (plus_ex_d_c e4 e2));
 254  nrewrite > (symmetric_plusex_d_c e4 e2);
 255  nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_d_c e2 e4));
 256  napply (refl_eq ??).
 257 nqed.
 258
 259 nlemma symmetric_mulex : symmetricT exadecim byte8 mul_ex.
 260  #e1; #e2;
 261  nelim e1;
 262  nelim e2;
 263  nnormalize;
 264  napply (refl_eq ??).
 265 nqed.
 266
 267 nlemma eqb8_to_eq : ∀b1,b2:byte8.(eq_b8 b1 b2 = true) → (b1 = b2).
 268  #b1; #b2;
 269  nelim b1;
 270  nelim b2;
 271  #e1; #e2; #e3; #e4;
 272  nchange in ⊢ (% → ?) with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = true);
 273  #H;
 274  nrewrite < (eqex_to_eq ?? (andb_true_true_l ?? H));
 275  nrewrite < (eqex_to_eq ?? (andb_true_true_r ?? H));
 276  napply (refl_eq ??).
 277 nqed.
 278
 279 nlemma eq_to_eqb8 : ∀b1,b2.b1 = b2 → eq_b8 b1 b2 = true.
 280  #b1; #b2;
 281  nelim b1;
 282  nelim b2;
 283  #e1; #e2; #e3; #e4;
 284  #H;
 285  nrewrite < (byte8_destruct_1 ???? H);
 286  nrewrite < (byte8_destruct_2 ???? H);
 287  nchange with (((eq_ex e3 e3)⊗(eq_ex e4 e4)) = true);
 288  nrewrite > (eq_to_eqex e3 e3 (refl_eq ??));
 289  nrewrite > (eq_to_eqex e4 e4 (refl_eq ??));
 290  nnormalize;
 291  napply (refl_eq ??).
 292 nqed.