freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation_lemmas.ma
index a289826a0aff49affa1bd096a98271f22593f54e..18db2df62117f964a9a9fe1c9c04ffe45f8133df 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/translation_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/translation_lemmas.ma
@@ -21,6 +21,7 @@
 (* ********************************************************************** *)
 
 include "freescale/translation.ma".
+include "num/byte8_lemmas.ma".
 
 (* ******************************************************* *)
 (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
@@ -33,3 +34,55 @@ nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
  nnormalize;
  napply refl_eq.
 nqed.
+
+nlemma symmetric_eqtbyte8 : ∀m.∀tb1,tb2:t_byte8 m.eq_tbyte8 m tb1 tb2 = eq_tbyte8 m tb2 tb1.
+ #m; #tb1; nelim tb1; #b1; #tb2; nelim tb2; #b2;
+ nchange with ((eq_b8 b1 b2) = (eq_b8 b2 b1));
+ napply (symmetric_eqb8 b1 b2).
+nqed.
+
+nlemma eqtbyte8_to_eq : ∀m.∀tb1,tb2:t_byte8 m.eq_tbyte8 m tb1 tb2 = true → tb1 = tb2.
+ #m; #tb1; nelim tb1; #b1; #tb2; nelim tb2; #b2;
+ nchange with ((eq_b8 b1 b2 = true) → ?);
+ #H;
+ nrewrite > (eqb8_to_eq b1 b2 H);
+ napply refl_eq.
+nqed.
+
+nlemma eq_to_eqtbyte8 : ∀m.∀tb1,tb2:t_byte8 m.tb1 = tb2 → eq_tbyte8 m tb1 tb2 = true.
+ #m; #tb1; nelim tb1; #b1; #tb2; nelim tb2; #b2;
+ nchange with (? → (eq_b8 b1 b2 = true));
+ #H;
+ nrewrite > (tbyte8_destruct m … H);
+ nrewrite > (eq_to_eqb8 b2 b2 (refl_eq …));
+ napply refl_eq.
+nqed.
+
+nlemma decidable_tbyte8 : ∀m.∀x,y:t_byte8 m.decidable (x = y).
+ #m; #x; nelim x; #e1; #y; nelim y; #e2;
+ nnormalize;
+ napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 e1 e2) …);
+ ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (tbyte8_destruct m … H1))
+ ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+ ##]
+nqed.
+
+nlemma neqtbyte8_to_neq : ∀m.∀tb1,tb2:t_byte8 m.(eq_tbyte8 m tb1 tb2 = false) → (tb1 ≠ tb2).
+ #m; #tb1; nelim tb1; #b1; #tb2; nelim tb2; #b2;
+ nchange with (((eq_b8 b1 b2) = false) → ?);
+ #H;
+ nnormalize;
+ #H1;
+ napply (neqb8_to_neq … H);
+ napply (tbyte8_destruct m … H1).
+nqed.
+
+nlemma neq_to_neqtbyte8 : ∀m.∀tb1,tb2:t_byte8 m.tb1 ≠ tb2 → eq_tbyte8 m tb1 tb2 = false.
+ #m; #tb1; nelim tb1; #b1; #tb2; nelim tb2; #b2;
+ #H; nchange with ((eq_b8 b1 b2) = false);
+ napply (neq_to_neqb8 b1 b2 ?);
+ nnormalize;
+ #H1;
+ nrewrite > H1 in H:(%); #H;
+ napply (H (refl_eq …)).
+nqed.