helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status_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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/word16_lemmas.ma".
  24 include "emulator/status/RS08_status.ma".
  25
  26 (* *********************************** *)
  27 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  28 (* *********************************** *)
  29
  30 nlemma aluRS08_destruct_1 :
  31 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  32  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  33  x1 = y1.
  34  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  35  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
  36  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
  37                 with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
  38  nrewrite < H;
  39  nnormalize;
  40  napply refl_eq.
  41 nqed.
  42
  43 nlemma aluRS08_destruct_2 :
  44 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  45  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  46  x2 = y2.
  47  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  48  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
  49  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
  50                 with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
  51  nrewrite < H;
  52  nnormalize;
  53  napply refl_eq.
  54 nqed.
  55
  56 nlemma aluRS08_destruct_3 :
  57 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  58  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  59  x3 = y3.
  60  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  61  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
  62  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
  63                 with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
  64  nrewrite < H;
  65  nnormalize;
  66  napply refl_eq.
  67 nqed.
  68
  69 nlemma aluRS08_destruct_4 :
  70 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  71  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  72  x4 = y4.
  73  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  74  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
  75  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
  76                 with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
  77  nrewrite < H;
  78  nnormalize;
  79  napply refl_eq.
  80 nqed.
  81
  82 nlemma aluRS08_destruct_5 :
  83 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  84  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  85  x5 = y5.
  86  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  87  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
  88  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
  89                 with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
  90  nrewrite < H;
  91  nnormalize;
  92  napply refl_eq.
  93 nqed.
  94
  95 nlemma aluRS08_destruct_6 :
  96 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  97  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  98  x6 = y6.
  99  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 100  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 101  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 102                 with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
 103  nrewrite < H;
 104  nnormalize;
 105  napply refl_eq.
 106 nqed.
 107
 108 nlemma aluRS08_destruct_7 :
 109 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 110  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 111  x7 = y7.
 112  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 113  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 114  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 115                 with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
 116  nrewrite < H;
 117  nnormalize;
 118  napply refl_eq.
 119 nqed.
 120
 121 nlemma aluRS08_destruct_8 :
 122 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 123  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 124  x8 = y8.
 125  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 126  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 127  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 128                 with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
 129  nrewrite < H;
 130  nnormalize;
 131  napply refl_eq.
 132 nqed.
 133
 134 nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_RS08_alu.
 135  #alu1; #alu2;
 136  ncases alu1;
 137  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 138  ncases alu2;
 139  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 140  nchange with (
 141   ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
 142    (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 143    (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
 144    (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) =
 145   ((eq_b8 y1 x1) ⊗ (eq_w16 y2 x2) ⊗
 146    (eq_w16 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
 147    (eq_b8 y5 x5) ⊗ (eq_b8 y6 x6) ⊗
 148    (eq_bool y7 x7) ⊗ (eq_bool y8 x8)));
 149  nrewrite > (symmetric_eqb8 x1 y1);
 150  nrewrite > (symmetric_eqw16 x2 y2);
 151  nrewrite > (symmetric_eqw16 x3 y3);
 152  nrewrite > (symmetric_eqw16 x4 y4);
 153  nrewrite > (symmetric_eqb8 x5 y5);
 154  nrewrite > (symmetric_eqb8 x6 y6);
 155  nrewrite > (symmetric_eqbool x7 y7);
 156  nrewrite > (symmetric_eqbool x8 y8);
 157  napply refl_eq.
 158 nqed.
 159
 160 nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_RS08_alu alu1 alu2 = true → alu1 = alu2.
 161  #alu1; #alu2;
 162  ncases alu1;
 163  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 164  ncases alu2;
 165  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 166  nchange in H:(%) with (
 167   ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
 168    (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 169    (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
 170    (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) = true);
 171  nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
 172  nletin H1 ≝ (andb_true_true_l … H);
 173  nrewrite > (eqbool_to_eq … (andb_true_true_r … H1));
 174  nletin H2 ≝ (andb_true_true_l … H1);
 175  nrewrite > (eqb8_to_eq … (andb_true_true_r … H2));
 176  nletin H3 ≝ (andb_true_true_l … H2);
 177  nrewrite > (eqb8_to_eq … (andb_true_true_r … H3));
 178  nletin H4 ≝ (andb_true_true_l … H3);
 179  nrewrite > (eqw16_to_eq … (andb_true_true_r … H4));
 180  nletin H5 ≝ (andb_true_true_l … H4);
 181  nrewrite > (eqw16_to_eq … (andb_true_true_r … H5));
 182  nletin H6 ≝ (andb_true_true_l … H5);
 183  nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
 184  nrewrite > (eqb8_to_eq … (andb_true_true_l … H6));
 185  napply refl_eq.
 186 nqed.
 187
 188 nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_RS08_alu alu1 alu2 = true.
 189  #alu1; #alu2;
 190  ncases alu1;
 191  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 192  ncases alu2;
 193  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 194  nrewrite > (aluRS08_destruct_1 … H);
 195  nrewrite > (aluRS08_destruct_2 … H);
 196  nrewrite > (aluRS08_destruct_3 … H);
 197  nrewrite > (aluRS08_destruct_4 … H);
 198  nrewrite > (aluRS08_destruct_5 … H);
 199  nrewrite > (aluRS08_destruct_6 … H);
 200  nrewrite > (aluRS08_destruct_7 … H);
 201  nrewrite > (aluRS08_destruct_8 … H);
 202  nchange with (
 203   ((eq_b8 y1 y1) ⊗ (eq_w16 y2 y2) ⊗
 204    (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
 205    (eq_b8 y5 y5) ⊗ (eq_b8 y6 y6) ⊗
 206    (eq_bool y7 y7) ⊗ (eq_bool y8 y8)) = true);
 207  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
 208  nrewrite > (eq_to_eqw16 y2 y2 (refl_eq …));
 209  nrewrite > (eq_to_eqw16 y3 y3 (refl_eq …));
 210  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
 211  nrewrite > (eq_to_eqb8 y5 y5 (refl_eq …));
 212  nrewrite > (eq_to_eqb8 y6 y6 (refl_eq …));
 213  nrewrite > (eq_to_eqbool y7 y7 (refl_eq …));
 214  nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
 215  napply refl_eq.
 216 nqed.
 217
 218 nlemma decidable_aluRS08_aux1
 219  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 220  (x1 ≠ y1) →
 221  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
 222  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
 223  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 224  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 225  nnormalize; #H; #H1;
 226  napply (H (aluRS08_destruct_1 … H1)).
 227 nqed.
 228
 229 nlemma decidable_aluRS08_aux2
 230  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 231  (x2 ≠ y2) →
 232  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
 233  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
 234  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 235  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 236  nnormalize; #H; #H1;
 237  napply (H (aluRS08_destruct_2 … H1)).
 238 nqed.
 239
 240 nlemma decidable_aluRS08_aux3
 241  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 242  (x3 ≠ y3) →
 243  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
 244  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
 245  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 246  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 247  nnormalize; #H; #H1;
 248  napply (H (aluRS08_destruct_3 … H1)).
 249 nqed.
 250
 251 nlemma decidable_aluRS08_aux4
 252  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 253  (x4 ≠ y4) →
 254  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
 255  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
 256  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 257  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 258  nnormalize; #H; #H1;
 259  napply (H (aluRS08_destruct_4 … H1)).
 260 nqed.
 261
 262 nlemma decidable_aluRS08_aux5
 263  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 264  (x5 ≠ y5) →
 265  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
 266  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
 267  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 268  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 269  nnormalize; #H; #H1;
 270  napply (H (aluRS08_destruct_5 … H1)).
 271 nqed.
 272
 273 nlemma decidable_aluRS08_aux6
 274  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 275  (x6 ≠ y6) →
 276  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
 277  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
 278  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 279  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 280  nnormalize; #H; #H1;
 281  napply (H (aluRS08_destruct_6 … H1)).
 282 nqed.
 283
 284 nlemma decidable_aluRS08_aux7
 285  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 286  (x7 ≠ y7) →
 287  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
 288  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
 289  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 290  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 291  nnormalize; #H; #H1;
 292  napply (H (aluRS08_destruct_7 … H1)).
 293 nqed.
 294
 295 nlemma decidable_aluRS08_aux8
 296  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 297  (x8 ≠ y8) →
 298  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
 299  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
 300  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 301  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 302  nnormalize; #H; #H1;
 303  napply (H (aluRS08_destruct_8 … H1)).
 304 nqed.
 305
 306 nlemma decidable_aluRS08 : ∀x,y:alu_RS08.decidable (x = y).
 307  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 308  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 309  nnormalize;
 310  napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
 311  ##[ ##2: #H; napply (or2_intro2 … (decidable_aluRS08_aux1 … H))
 312  ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x2 y2) …);
 313   ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluRS08_aux2 … H1))
 314   ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …);
 315    ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluRS08_aux3 … H2))
 316    ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
 317     ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluRS08_aux4 … H3))
 318     ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x5 y5) …);
 319      ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluRS08_aux5 … H4))
 320      ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x6 y6) …);
 321       ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluRS08_aux6 … H5))
 322       ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …);
 323        ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluRS08_aux7 … H6))
 324        ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
 325         ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluRS08_aux8 … H7))
 326         ##| ##1: #H7; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
 327                       nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
 328                       napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 329         ##]
 330        ##]
 331       ##]
 332      ##]
 333     ##]
 334    ##]
 335   ##]
 336  ##]
 337 nqed.