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