freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
deleted file mode 100755 (executable)
index ebaf9ae..0000000
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
+++ /dev/null
@@ -1,101 +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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
-(*                                                                        *)
-(* ********************************************************************** *)
-
-include "num/bool_lemmas.ma".
-include "freescale/opcode_base.ma".
-
-(* ********************************************** *)
-(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
-(* ********************************************** *)
-
-ndefinition mcu_type_destruct_aux ≝
-Πm1,m2:mcu_type.ΠP:Prop.m1 = m2 →
- match eq_mcutype m1 m2 with [ true ⇒ P → P | false ⇒ P ].
-
-ndefinition mcutype_destruct : mcu_type_destruct_aux.
- #m1; #m2; #P; #H;
- nrewrite < H;
- nelim m1;
- nnormalize;
- napply (λx.x).
-nqed.
-
-nlemma symmetric_eqmcutype : symmetricT mcu_type bool eq_mcutype.
- #m1; #m2;
- nelim m1;
- nelim m2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m2).
- #m1; #m2;
- ncases m1;
- ncases m2;
- nnormalize;
- ##[ ##1,6,11,16: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eq_to_eqmcutype : ∀m1,m2.m1 = m2 → eq_mcutype m1 m2 = true.
- #m1; #m2;
- ncases m1;
- ncases m2;
- nnormalize;
- ##[ ##1,6,11,16: #H; napply refl_eq
- ##| ##*: #H; napply (mcutype_destruct … H)
- ##]
-nqed.
-
-nlemma decidable_mcutype : ∀x,y:mcu_type.decidable (x = y).
- #x; #y;
- nnormalize;
- nelim x;
- nelim y;
- ##[ ##1,6,11,16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
-          nnormalize; #H;
-          napply False_ind;
-          napply (mcutype_destruct … H)
- ##]
-nqed.
-
-nlemma neqmcutype_to_neq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = false) → (m1 ≠ m2).
- #m1; #m2;
- ncases m1;
- ncases m2;
- nnormalize;
- ##[ ##1,6,11,16: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (mcutype_destruct … H1)
- ##]
-nqed.
-
-nlemma neq_to_neqmcutype : ∀m1,m2.m1 ≠ m2 → eq_mcutype m1 m2 = false.
- #m1; #m2;
- ncases m1;
- ncases m2;
- nnormalize;
- ##[ ##1,6,11,16: #H; nelim (H (refl_eq …))
- ##| ##*: #H; napply refl_eq
- ##]
-nqed.