helm/software/matita/contribs/ng_assembly/freescale/word16_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/byte8_lemmas.ma".
  28 include "freescale/word16.ma".
  29
  30 (* **** *)
  31 (* WORD *)
  32 (* **** *)
  33
  34 nlemma word16_destruct_1 :
  35 ∀x1,x2,y1,y2.
  36  mk_word16 x1 y1 = mk_word16 x2 y2 → x1 = x2.
  37  #x1; #x2; #y1; #y2; #H;
  38  nchange with (match mk_word16 x2 y2 with [ mk_word16 a _ ⇒ x1 = a ]);
  39  nrewrite < H;
  40  nnormalize;
  41  napply (refl_eq ??).
  42 nqed.
  43
  44 nlemma word16_destruct_2 :
  45 ∀x1,x2,y1,y2.
  46  mk_word16 x1 y1 = mk_word16 x2 y2 → y1 = y2.
  47  #x1; #x2; #y1; #y2; #H;
  48  nchange with (match mk_word16 x2 y2 with [ mk_word16 _ b ⇒ y1 = b ]);
  49  nrewrite < H;
  50  nnormalize;
  51  napply (refl_eq ??).
  52 nqed.
  53
  54 nlemma symmetric_eqw16 : symmetricT word16 bool eq_w16.
  55  #w1; #w2;
  56  nelim w1;
  57  nelim w2;
  58  #b1; #b2; #b3; #b4;
  59  nchange with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = ((eq_b8 b1 b3)⊗(eq_b8 b2 b4)));
  60  nrewrite > (symmetric_eqb8 b1 b3);
  61  nrewrite > (symmetric_eqb8 b2 b4);
  62  napply (refl_eq ??).
  63 nqed.
  64
  65 nlemma symmetric_andw16 : symmetricT word16 word16 and_w16.
  66  #w1; #w2;
  67  nelim w1;
  68  nelim w2;
  69  #b1; #b2; #b3; #b4;
  70  nchange with ((mk_word16 (and_b8 b3 b1) (and_b8 b4 b2)) = (mk_word16 (and_b8 b1 b3) (and_b8 b2 b4)));
  71  nrewrite > (symmetric_andb8 b1 b3);
  72  nrewrite > (symmetric_andb8 b2 b4);
  73  napply (refl_eq ??).
  74 nqed.
  75
  76 nlemma associative_andw16 : ∀w1,w2,w3.(and_w16 (and_w16 w1 w2) w3) = (and_w16 w1 (and_w16 w2 w3)).
  77  #w1; #w2; #w3;
  78  nelim w1;
  79  #b1; #b2;
  80  nelim w2;
  81  #b3; #b4;
  82  nelim w3;
  83  #b5; #b6;
  84  nchange with (mk_word16 (and_b8 (and_b8 b1 b3) b5) (and_b8 (and_b8 b2 b4) b6) =
  85   mk_word16 (and_b8 b1 (and_b8 b3 b5)) (and_b8 b2 (and_b8 b4 b6)));
  86  nrewrite < (associative_andb8 b1 b3 b5);
  87  nrewrite < (associative_andb8 b2 b4 b6);
  88  napply (refl_eq ??).
  89 nqed.
  90
  91 nlemma symmetric_orw16 : symmetricT word16 word16 or_w16.
  92  #w1; #w2;
  93  nelim w1;
  94  nelim w2;
  95  #b1; #b2; #b3; #b4;
  96  nchange with ((mk_word16 (or_b8 b3 b1) (or_b8 b4 b2)) = (mk_word16 (or_b8 b1 b3) (or_b8 b2 b4)));
  97  nrewrite > (symmetric_orb8 b1 b3);
  98  nrewrite > (symmetric_orb8 b2 b4);
  99  napply (refl_eq ??).
 100 nqed.
 101
 102 nlemma associative_orw16 : ∀w1,w2,w3.(or_w16 (or_w16 w1 w2) w3) = (or_w16 w1 (or_w16 w2 w3)).
 103  #w1; #w2; #w3;
 104  nelim w1;
 105  #b1; #b2;
 106  nelim w2;
 107  #b3; #b4;
 108  nelim w3;
 109  #b5; #b6;
 110  nchange with (mk_word16 (or_b8 (or_b8 b1 b3) b5) (or_b8 (or_b8 b2 b4) b6) =
 111   mk_word16 (or_b8 b1 (or_b8 b3 b5)) (or_b8 b2 (or_b8 b4 b6)));
 112  nrewrite < (associative_orb8 b1 b3 b5);
 113  nrewrite < (associative_orb8 b2 b4 b6);
 114  napply (refl_eq ??).
 115 nqed.
 116
 117 nlemma symmetric_xorw16 : symmetricT word16 word16 xor_w16.
 118  #w1; #w2;
 119  nelim w1;
 120  nelim w2;
 121  #b1; #b2; #b3; #b4;
 122  nchange with ((mk_word16 (xor_b8 b3 b1) (xor_b8 b4 b2)) = (mk_word16 (xor_b8 b1 b3) (xor_b8 b2 b4)));
 123  nrewrite > (symmetric_xorb8 b1 b3);
 124  nrewrite > (symmetric_xorb8 b2 b4);
 125  napply (refl_eq ??).
 126 nqed.
 127
 128 nlemma associative_xorw16 : ∀w1,w2,w3.(xor_w16 (xor_w16 w1 w2) w3) = (xor_w16 w1 (xor_w16 w2 w3)).
 129  #w1; #w2; #w3;
 130  nelim w1;
 131  #b1; #b2;
 132  nelim w2;
 133  #b3; #b4;
 134  nelim w3;
 135  #b5; #b6;
 136  nchange with (mk_word16 (xor_b8 (xor_b8 b1 b3) b5) (xor_b8 (xor_b8 b2 b4) b6) =
 137   mk_word16 (xor_b8 b1 (xor_b8 b3 b5)) (xor_b8 b2 (xor_b8 b4 b6)));
 138  nrewrite < (associative_xorb8 b1 b3 b5);
 139  nrewrite < (associative_xorb8 b2 b4 b6);
 140  napply (refl_eq ??).
 141 nqed.
 142
 143 nlemma symmetric_plusw16_dc_dc : ∀w1,w2,c.plus_w16_dc_dc w1 w2 c = plus_w16_dc_dc w2 w1 c.
 144  #w1; #w2; #c;
 145  nelim w1;
 146  #b1; #b2;
 147  nelim w2;
 148  #b3; #b4;
 149  nchange with (
 150   match plus_b8_dc_dc b2 b4 c with
 151    [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
 152     [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]] =
 153   match plus_b8_dc_dc b4 b2 c with
 154    [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
 155     [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]]);
 156  nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
 157  ncases (plus_b8_dc_dc b2 b4 c);
 158  #b5; #c1;
 159  nchange with (
 160   match plus_b8_dc_dc b1 b3 c1 with
 161    [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ] =
 162   match plus_b8_dc_dc b3 b1 c1 with
 163    [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ]);
 164  nrewrite > (symmetric_plusb8_dc_dc b1 b3 c1);
 165  napply (refl_eq ??).
 166 nqed.
 167
 168 nlemma symmetric_plusw16_dc_d : ∀w1,w2,c.plus_w16_dc_d w1 w2 c = plus_w16_dc_d w2 w1 c.
 169  #w1; #w2; #c;
 170  nelim w1;
 171  #b1; #b2;
 172  nelim w2;
 173  #b3; #b4;
 174  nchange with (
 175   match plus_b8_dc_dc b2 b4 c with
 176    [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
 177   match plus_b8_dc_dc b4 b2 c with
 178    [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
 179  nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
 180  ncases (plus_b8_dc_dc b2 b4 c);
 181  #b5; #c1;
 182  nchange with (〈plus_b8_dc_d b1 b3 c1:b5〉 = 〈plus_b8_dc_d b3 b1 c1:b5〉);
 183  nrewrite > (symmetric_plusb8_dc_d b1 b3 c1);
 184  napply (refl_eq ??).
 185 nqed.
 186
 187 nlemma symmetric_plusw16_dc_c : ∀w1,w2,c.plus_w16_dc_c w1 w2 c = plus_w16_dc_c w2 w1 c.
 188  #w1; #w2; #c;
 189  nelim w1;
 190  #b1; #b2;
 191  nelim w2;
 192  #b3; #b4;
 193  nchange with (
 194   plus_b8_dc_c b1 b3 (plus_b8_dc_c b2 b4 c) =
 195   plus_b8_dc_c b3 b1 (plus_b8_dc_c b4 b2 c));
 196  nrewrite > (symmetric_plusb8_dc_c b4 b2 c);
 197  nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_dc_c b2 b4 c));
 198  napply (refl_eq ??).
 199 nqed.
 200
 201 nlemma symmetric_plusw16_d_dc : ∀w1,w2.plus_w16_d_dc w1 w2 = plus_w16_d_dc w2 w1.
 202  #w1; #w2;
 203  nelim w1;
 204  #b1; #b2;
 205  nelim w2;
 206  #b3; #b4;
 207  nchange with (
 208   match plus_b8_d_dc b2 b4 with
 209    [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
 210     [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]] =
 211   match plus_b8_d_dc b4 b2 with
 212    [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
 213     [ pair h c' ⇒ pair ?? 〈h:l〉 c' ]]);
 214  nrewrite > (symmetric_plusb8_d_dc b4 b2);
 215  ncases (plus_b8_d_dc b2 b4);
 216  #b5; #c;
 217  nchange with (
 218   match plus_b8_dc_dc b1 b3 c with
 219    [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ] =
 220   match plus_b8_dc_dc b3 b1 c with
 221    [ pair h c' ⇒ pair ?? 〈h:b5〉 c' ]);
 222  nrewrite > (symmetric_plusb8_dc_dc b1 b3 c);
 223  napply (refl_eq ??).
 224 nqed.
 225
 226 nlemma symmetric_plusw16_d_d : ∀w1,w2.plus_w16_d_d w1 w2 = plus_w16_d_d w2 w1.
 227  #w1; #w2;
 228  nelim w1;
 229  #b1; #b2;
 230  nelim w2;
 231  #b3; #b4;
 232  nchange with (
 233   match plus_b8_d_dc b2 b4 with
 234    [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
 235   match plus_b8_d_dc b4 b2 with
 236    [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
 237  nrewrite > (symmetric_plusb8_d_dc b4 b2);
 238  ncases (plus_b8_d_dc b2 b4);
 239  #b5; #c;
 240  nchange with (〈plus_b8_dc_d b1 b3 c:b5〉 = 〈plus_b8_dc_d b3 b1 c:b5〉);
 241  nrewrite > (symmetric_plusb8_dc_d b1 b3 c);
 242  napply (refl_eq ??).
 243 nqed.
 244
 245 nlemma symmetric_plusw16_d_c : ∀w1,w2.plus_w16_d_c w1 w2 = plus_w16_d_c w2 w1.
 246  #w1; #w2;
 247  nelim w1;
 248  #b1; #b2;
 249  nelim w2;
 250  #b3; #b4;
 251  nchange with (
 252   plus_b8_dc_c b1 b3 (plus_b8_d_c b2 b4) =
 253   plus_b8_dc_c b3 b1 (plus_b8_d_c b4 b2));
 254  nrewrite > (symmetric_plusb8_d_c b4 b2);
 255  nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_d_c b2 b4));
 256  napply (refl_eq ??).
 257 nqed.
 258
 259 nlemma symmetric_mulb8 : symmetricT byte8 word16 mul_b8.
 260  #b1; #b2;
 261  nelim b1;
 262  #e1; #e2;
 263  nelim b2;
 264  #e3; #e4;
 265  nchange with (match mul_ex e2 e4 with
 266  [ mk_byte8 t1_h t1_l ⇒ match mul_ex e1 e4 with
 267  [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with
 268  [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with
 269  [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
 270  ]]]] = match mul_ex e4 e2 with
 271  [ mk_byte8 t1_h t1_l ⇒ match mul_ex e3 e2 with
 272  [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with
 273  [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with
 274  [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
 275  ]]]]);
 276  nrewrite < (symmetric_mulex e2 e4);
 277  ncases (mul_ex e2 e4);
 278  #e5; #e6;
 279  nchange with (match mul_ex e1 e4 with
 280  [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with
 281  [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with
 282  [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
 283  ]]] = match mul_ex e3 e2 with
 284  [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with
 285  [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with
 286  [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
 287  ]]]);
 288  ncases (mul_ex e3 e2);
 289  #e7; #e8;
 290  ncases (mul_ex e1 e4);
 291  #e9; #e10;
 292  nchange with (match mul_ex e1 e3 with
 293  [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
 294  ] = match mul_ex e3 e1 with
 295  [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
 296  ]);
 297  nrewrite < (symmetric_mulex e1 e3);
 298  ncases (mul_ex e1 e3);
 299  #e11; #e12;
 300  nchange with ((plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉) =
 301   (plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉));
 302  nrewrite > (symmetric_plusw16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉);
 303  napply (refl_eq ??).
 304 nqed.
 305
 306 nlemma eqw16_to_eq : ∀w1,w2:word16.(eq_w16 w1 w2 = true) → (w1 = w2).
 307  #w1; #w2;
 308  nelim w1;
 309  nelim w2;
 310  #b1; #b2; #b3; #b4;
 311  nchange in ⊢ (% → ?) with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = true);
 312  #H;
 313  nrewrite < (eqb8_to_eq ?? (andb_true_true_l ?? H));
 314  nrewrite < (eqb8_to_eq ?? (andb_true_true_r ?? H));
 315  napply (refl_eq ??).
 316 nqed.
 317
 318 nlemma eq_to_eqw16 : ∀w1,w2.w1 = w2 → eq_w16 w1 w2 = true.
 319  #w1; #w2;
 320  nelim w1;
 321  nelim w2;
 322  #b1; #b2; #b3; #b4;
 323  #H;
 324  nrewrite < (word16_destruct_1 ???? H);
 325  nrewrite < (word16_destruct_2 ???? H);
 326  nchange with (((eq_b8 b3 b3)⊗(eq_b8 b4 b4)) = true);
 327  nrewrite > (eq_to_eqb8 b3 b3 (refl_eq ??));
 328  nrewrite > (eq_to_eqb8 b4 b4 (refl_eq ??));
 329  nnormalize;
 330  napply (refl_eq ??).
 331 nqed.