matitaB/matita/contribs/ng_assembly2/emulator/status/RS08_status.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 "emulator/status/RS08_status_base.ma".
  24
  25 (* *********************************** *)
  26 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  27 (* *********************************** *)
  28
  29 nlemma aluRS08_destruct_1 :
  30 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  31  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  32  x1 = y1.
  33  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  34  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
  35  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
  36                 with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
  37  nrewrite < H;
  38  nnormalize;
  39  napply refl_eq.
  40 nqed.
  41
  42 nlemma aluRS08_destruct_2 :
  43 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  44  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  45  x2 = y2.
  46  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  47  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
  48  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
  49                 with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
  50  nrewrite < H;
  51  nnormalize;
  52  napply refl_eq.
  53 nqed.
  54
  55 nlemma aluRS08_destruct_3 :
  56 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  57  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  58  x3 = y3.
  59  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  60  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
  61  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
  62                 with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
  63  nrewrite < H;
  64  nnormalize;
  65  napply refl_eq.
  66 nqed.
  67
  68 nlemma aluRS08_destruct_4 :
  69 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  70  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  71  x4 = y4.
  72  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  73  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
  74  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
  75                 with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
  76  nrewrite < H;
  77  nnormalize;
  78  napply refl_eq.
  79 nqed.
  80
  81 nlemma aluRS08_destruct_5 :
  82 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  83  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  84  x5 = y5.
  85  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  86  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
  87  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
  88                 with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
  89  nrewrite < H;
  90  nnormalize;
  91  napply refl_eq.
  92 nqed.
  93
  94 nlemma aluRS08_destruct_6 :
  95 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
  96  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
  97  x6 = y6.
  98  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  99  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 100  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 101                 with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
 102  nrewrite < H;
 103  nnormalize;
 104  napply refl_eq.
 105 nqed.
 106
 107 nlemma aluRS08_destruct_7 :
 108 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 109  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 110  x7 = y7.
 111  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 112  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 113  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 114                 with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
 115  nrewrite < H;
 116  nnormalize;
 117  napply refl_eq.
 118 nqed.
 119
 120 nlemma aluRS08_destruct_8 :
 121 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 122  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 123  x8 = y8.
 124  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 125  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 126  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 127                 with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
 128  nrewrite < H;
 129  nnormalize;
 130  napply refl_eq.
 131 nqed.
 132
 133 nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_RS08_alu alu1 alu2 = true.
 134  #alu1; #alu2;
 135  ncases alu1;
 136  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 137  ncases alu2;
 138  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 139  nrewrite > (aluRS08_destruct_1 … H);
 140  nrewrite > (aluRS08_destruct_2 … H);
 141  nrewrite > (aluRS08_destruct_3 … H);
 142  nrewrite > (aluRS08_destruct_4 … H);
 143  nrewrite > (aluRS08_destruct_5 … H);
 144  nrewrite > (aluRS08_destruct_6 … H);
 145  nrewrite > (aluRS08_destruct_7 … H);
 146  nrewrite > (aluRS08_destruct_8 … H);
 147  nchange with (
 148   ((eqc ? y1 y1) ⊗ (eqc ? y2 y2) ⊗
 149    (eqc ? y3 y3) ⊗ (eqc ? y4 y4) ⊗
 150    (eqc ? y5 y5) ⊗ (eqc ? y6 y6) ⊗
 151    (eqc ? y7 y7) ⊗ (eqc ? y8 y8)) = true);
 152  nrewrite > (eq_to_eqc ? y1 y1 (refl_eq …));
 153  nrewrite > (eq_to_eqc ? y2 y2 (refl_eq …));
 154  nrewrite > (eq_to_eqc ? y3 y3 (refl_eq …));
 155  nrewrite > (eq_to_eqc ? y4 y4 (refl_eq …));
 156  nrewrite > (eq_to_eqc ? y5 y5 (refl_eq …));
 157  nrewrite > (eq_to_eqc ? y6 y6 (refl_eq …));
 158  nrewrite > (eq_to_eqc ? y7 y7 (refl_eq …));
 159  nrewrite > (eq_to_eqc ? y8 y8 (refl_eq …));
 160  napply refl_eq.
 161 nqed.
 162
 163 nlemma neqaluRS08_to_neq : ∀alu1,alu2.eq_RS08_alu alu1 alu2 = false → alu1 ≠ alu2.
 164  #s1; #s2; #H;
 165  napply (not_to_not (s1 = s2) (eq_RS08_alu s1 s2 = true) …);
 166  ##[ ##1: napply (eq_to_eqaluRS08 s1 s2)
 167  ##| ##2: napply (eqfalse_to_neqtrue … H)
 168  ##]
 169 nqed.
 170
 171 nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_RS08_alu alu1 alu2 = true → alu1 = alu2.
 172  #alu1; #alu2;
 173  ncases alu1;
 174  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 175  ncases alu2;
 176  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 177  nchange in H:(%) with (
 178   ((eqc ? x1 y1) ⊗ (eqc ? x2 y2) ⊗
 179    (eqc ? x3 y3) ⊗ (eqc ? x4 y4) ⊗
 180    (eqc ? x5 y5) ⊗ (eqc ? x6 y6) ⊗
 181    (eqc ? x7 y7) ⊗ (eqc ? x8 y8)) = true);
 182  nrewrite > (eqc_to_eq … (andb_true_true_r … H));
 183  nletin H1 ≝ (andb_true_true_l … H);
 184  nrewrite > (eqc_to_eq … (andb_true_true_r … H1));
 185  nletin H2 ≝ (andb_true_true_l … H1);
 186  nrewrite > (eqc_to_eq … (andb_true_true_r … H2));
 187  nletin H3 ≝ (andb_true_true_l … H2);
 188  nrewrite > (eqc_to_eq … (andb_true_true_r … H3));
 189  nletin H4 ≝ (andb_true_true_l … H3);
 190  nrewrite > (eqc_to_eq … (andb_true_true_r … H4));
 191  nletin H5 ≝ (andb_true_true_l … H4);
 192  nrewrite > (eqc_to_eq … (andb_true_true_r … H5));
 193  nletin H6 ≝ (andb_true_true_l … H5);
 194  nrewrite > (eqc_to_eq … (andb_true_true_r … H6));
 195  nrewrite > (eqc_to_eq … (andb_true_true_l … H6));
 196  napply refl_eq.
 197 nqed.
 198
 199 nlemma neq_to_neqaluRS08 : ∀alu1,alu2.alu1 ≠ alu2 → eq_RS08_alu alu1 alu2 = false.
 200  #s1; #s2; #H;
 201  napply (neqtrue_to_eqfalse (eq_RS08_alu s1 s2));
 202  napply (not_to_not (eq_RS08_alu s1 s2 = true) (s1 = s2) ? H);
 203  napply (eqaluRS08_to_eq s1 s2).
 204 nqed.
 205
 206 nlemma decidable_aluRS08 : ∀x,y:alu_RS08.decidable (x = y).
 207  #x; #y; nnormalize;
 208  napply (or2_elim (eq_RS08_alu x y = true) (eq_RS08_alu x y = false) ? (decidable_bexpr ?));
 209  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqaluRS08_to_eq … H))
 210  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqaluRS08_to_neq … H))
 211  ##]
 212 nqed.
 213
 214
 215 nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_RS08_alu.
 216  #alu1; #alu2;
 217  ncases alu1;
 218  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 219  ncases alu2;
 220  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 221  nchange with (
 222   ((eqc ? x1 y1) ⊗ (eqc ? x2 y2) ⊗
 223    (eqc ? x3 y3) ⊗ (eqc ? x4 y4) ⊗
 224    (eqc ? x5 y5) ⊗ (eqc ? x6 y6) ⊗
 225    (eqc ? x7 y7) ⊗ (eqc ? x8 y8)) =
 226   ((eqc ? y1 x1) ⊗ (eqc ? y2 x2) ⊗
 227    (eqc ? y3 x3) ⊗ (eqc ? y4 x4) ⊗
 228    (eqc ? y5 x5) ⊗ (eqc ? y6 x6) ⊗
 229    (eqc ? y7 x7) ⊗ (eqc ? y8 x8)));
 230  nrewrite > (symmetric_eqc ? x1 y1);
 231  nrewrite > (symmetric_eqc ? x2 y2);
 232  nrewrite > (symmetric_eqc ? x3 y3);
 233  nrewrite > (symmetric_eqc ? x4 y4);
 234  nrewrite > (symmetric_eqc ? x5 y5);
 235  nrewrite > (symmetric_eqc ? x6 y6);
 236  nrewrite > (symmetric_eqc ? x7 y7);
 237  nrewrite > (symmetric_eqc ? x8 y8);
 238  napply refl_eq.
 239 nqed.
 240
 241 nlemma aluRS08_is_comparable : comparable.
 242  @ alu_RS08
 243   ##[ napply (mk_alu_RS08 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
 244                           (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?))
 245   ##| napply forall_RS08_alu
 246   ##| napply eq_RS08_alu
 247   ##| napply eqaluRS08_to_eq
 248   ##| napply eq_to_eqaluRS08
 249   ##| napply neqaluRS08_to_neq
 250   ##| napply neq_to_neqaluRS08
 251   ##| napply decidable_aluRS08
 252   ##| napply symmetric_eqaluRS08
 253   ##]
 254 nqed.
 255
 256 unification hint 0 ≔ ⊢ carr aluRS08_is_comparable ≡ alu_RS08.