freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / status_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma
index 806e140ba86004dca5c312e77a80c1f22b751ed5..9edad75cc6c025d7315a6a4e06d5dcc2e7c35184 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma
@@ -15,16 +15,16 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
-include "freescale/word16_lemmas.ma".
+include "num/word16_lemmas.ma".
 include "freescale/opcode_base_lemmas1.ma".
 include "freescale/status.ma".
-include "freescale/option_lemmas.ma".
-include "freescale/prod_lemmas.ma".
+include "common/option_lemmas.ma".
+include "common/prod_lemmas.ma".
 
 (* *********************************** *)
 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
@@ -766,11 +766,11 @@ nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2
  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5;
           nchange with (
-           ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) =
-           ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_instrmode x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5)));
+           ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_im y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) =
+           ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_im x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5)));
           nrewrite > (symmetric_eqb8 x1 y1);
           nrewrite > (symmetric_eqanyop ? x2 y2);
-          nrewrite > (symmetric_eqinstrmode x3 y3);
+          nrewrite > (symmetric_eqim x3 y3);
           nrewrite > (symmetric_eqb8 x4 y4);
           nrewrite > (symmetric_eqw16 x5 y5);
           napply refl_eq
@@ -786,12 +786,12 @@ nlemma eqclk_to_eq : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = true → clk1 = clk
  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
           nchange in H:(%) with (
-           ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true);
+           ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_im y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true);
            nrewrite > (eqw16_to_eq … (andb_true_true_r … H));
            nletin H1 ≝ (andb_true_true_l … H);
            nrewrite > (eqb8_to_eq … (andb_true_true_r … H1));
            nletin H2 ≝ (andb_true_true_l … H1);
-           nrewrite > (eqinstrmode_to_eq … (andb_true_true_r … H2));
+           nrewrite > (eqim_to_eq … (andb_true_true_r … H2));
            nletin H3 ≝ (andb_true_true_l … H2);
            nrewrite > (eqanyop_to_eq … (andb_true_true_r … H3));
            nrewrite > (eqb8_to_eq … (andb_true_true_l … H3));
@@ -804,8 +804,8 @@ nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = tru
  ncases clk1;
  ncases clk2;
  ##[ ##1: nnormalize; #H; napply refl_eq
- ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some … H1)
- ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none … H1)
+ ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some ? p … H1)
+ ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none ? p … H1)
  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
           nrewrite > (quintuple_destruct_1 … (option_destruct_some_some … H));
@@ -814,10 +814,10 @@ nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = tru
           nrewrite > (quintuple_destruct_4 … (option_destruct_some_some … H));
           nrewrite > (quintuple_destruct_5 … (option_destruct_some_some … H));
           nchange with (
-           ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_instrmode x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true);
+           ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_im x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true);
           nrewrite > (eq_to_eqb8 x1 x1 (refl_eq …));
           nrewrite > (eq_to_eqanyop mcu x2 x2 (refl_eq ? x2));
-          nrewrite > (eq_to_eqinstrmode x3 x3 (refl_eq …));
+          nrewrite > (eq_to_eqim x3 x3 (refl_eq …));
           nrewrite > (eq_to_eqb8 x4 x4 (refl_eq …));
           nrewrite > (eq_to_eqw16 x5 x5 (refl_eq …));
           nnormalize;
@@ -959,7 +959,7 @@ nlemma eqstatus_to_eq :
  nchange with ((y1 = y1) ∧ (x4 = y4) ∧ (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
  nrewrite > (andb_true_true_r … (andb_true_true_l … H));
  nrewrite > (eqclk_to_eq … (andb_true_true_r … H));
- napply (conj … (conj … (refl_eq …) (refl_eq …)) (refl_eq …)).
+ napply (conj … (conj … (refl_eq ? y1) (refl_eq ? y4)) (refl_eq ? true)).
 nqed.
 
 nlemma eq_to_eqstatus_strong :
@@ -992,7 +992,7 @@ nlemma eq_to_eqstatus_strong :
  nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq …));
  nchange with ((forall_memory_ranged … ⊗ true) =true);
  nrewrite > (symmetric_andbool (forall_memory_ranged t y3 y3 y2 y2 addrl) true);
- nchange with (forall_memory_ranged … = true);
+ nchange with ((forall_memory_ranged t y3 y3 y2 y2 ?) = true);
  napply (list_ind word16 … addrl);
  ##[ ##1,3,5,7: nnormalize; napply refl_eq
  ##| ##2,4,6,8: #a; #l'; #H;