freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma
deleted file mode 100755 (executable)
index 116774e..0000000
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma
+++ /dev/null
@@ -1,126 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(*                          Progetto FreeScale                            *)
-(*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
-(*                                                                        *)
-(* ********************************************************************** *)
-
-include "freescale/opcode_base_lemmas_opcode2.ma".
-include "freescale/opcode_base_lemmas_instrmode2.ma".
-include "freescale/word16_lemmas.ma".
-
-(* ********************************************** *)
-(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
-(* ********************************************** *)
-
-nlemma anyop_destruct : ∀m.∀x1,x2:opcode.anyOP m x1 = anyOP m x2 → x1 = x2.
- #m; #x1; #x2; #H;
- nchange with (match anyOP m x2 with [ anyOP a ⇒ x1 = a ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_eqanyop : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = eq_anyop m op2 op1.
- #m;
- ncases m;
- #op1; #op2;
- ncases op1;
- #x1;
- ncases op2;
- #x2;
- nchange with (eq_op x1 x2 = eq_op x2 x1);
- nrewrite > (symmetric_eqop x1 x2);
- napply refl_eq.
-nqed.
-
-nlemma eqanyop_to_eq : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = true → op1 = op2.
- #m;
- ncases m;
- #op1; #op2;
- ncases op1;
- #x1;
- ncases op2;
- #x2;
- nchange with ((eq_op x1 x2 = true) → ?);
- #H;
- nrewrite > (eqop_to_eq … H);
- napply refl_eq.
-nqed.
-
-nlemma eq_to_eqanyop : ∀m.∀op1,op2:any_opcode m.op1 = op2 → eq_anyop m op1 op2 = true.
- #m;
- ncases m;
- #op1; #op2;
- ncases op1;
- #p1;
- ncases op2;
- #p2; #H;
- nrewrite > (anyop_destruct … H);
- nchange with (eq_op p2 p2 = true);
- nrewrite > (eq_to_eqop p2 p2 (refl_eq opcode p2));
- napply refl_eq.
-nqed.
-
-nlemma b8w16_destruct_b8_b8 : ∀x1,x2.Byte x1 = Byte x2 → x1 = x2.
- #x1; #x2; #H;
- nchange with (match Byte x2 with [ Byte a ⇒ x1 = a | Word _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma b8w16_destruct_w16_w16 : ∀x1,x2.Word x1 = Word x2 → x1 = x2.
- #x1; #x2; #H;
- nchange with (match Word x2 with [ Word a ⇒ x1 = a | Byte _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma b8w16_destruct_b8_w16 : ∀x1,x2.Byte x1 = Word x2 → False.
- #x1; #x2; #H;
- nchange with (match Byte x1 with [ Word _ ⇒ True | Byte a ⇒ False ]);
- nrewrite > H;
- nnormalize;
- napply I.
-nqed.
-
-nlemma b8w16_destruct_w16_b8 : ∀x1,x2.Word x1 = Byte x2 → False.
- #x1; #x2; #H;
- nchange with (match Word x1 with [ Word a ⇒ False | Byte _ ⇒ True ]);
- nrewrite > H;
- nnormalize;
- napply I.
-nqed.
-
-nlemma symmetric_eqb8w16 : ∀bw1,bw2.eq_b8w16 bw1 bw2 = eq_b8w16 bw2 bw1.
- #bw1; #bw2;
- ncases bw1;
- #x1;
- ncases bw2;
- #x2;
- ##[ ##1: nchange with (eq_b8 x1 x2 = eq_b8 x2 x1);
-          nrewrite > (symmetric_eqb8 x1 x2);
-          napply refl_eq
- ##| ##2,3: nnormalize; napply refl_eq
- ##| ##4: nchange with (eq_w16 x1 x2 = eq_w16 x2 x1);
-          nrewrite > (symmetric_eqw16 x1 x2);
-          napply refl_eq
- ##]
-nqed.