Smaller formulae.

[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
index c262ed8295c095e782ae78a06c37075f52de52cb..116774ed49547a2d7431d27ebe1a25952b1d9362 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma
@@ -13,15 +13,11 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/opcode_base_lemmas_opcode2.ma".
@@ -37,7 +33,7 @@ nlemma anyop_destruct : ∀m.∀x1,x2:opcode.anyOP m x1 = anyOP m x2 → x1 = x2
  nchange with (match anyOP m x2 with [ anyOP a ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqanyop : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = eq_anyop m op2 op1.
@@ -50,7 +46,7 @@ nlemma symmetric_eqanyop : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = eq_
  #x2;
  nchange with (eq_op x1 x2 = eq_op x2 x1);
  nrewrite > (symmetric_eqop x1 x2);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqanyop_to_eq : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = true → op1 = op2.
@@ -63,8 +59,8 @@ nlemma eqanyop_to_eq : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = true 
  #x2;
  nchange with ((eq_op x1 x2 = true) → ?);
  #H;
- nrewrite > (eqop_to_eq ?? H);
- napply (refl_eq ??).
+ 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.
@@ -75,10 +71,10 @@ nlemma eq_to_eqanyop : ∀m.∀op1,op2:any_opcode m.op1 = op2 → eq_anyop m op1
  #p1;
  ncases op2;
  #p2; #H;
- nrewrite > (anyop_destruct ??? 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 ??).
+ napply refl_eq.
 nqed.
 
 nlemma b8w16_destruct_b8_b8 : ∀x1,x2.Byte x1 = Byte x2 → x1 = x2.
@@ -86,7 +82,7 @@ nlemma b8w16_destruct_b8_b8 : ∀x1,x2.Byte x1 = Byte x2 → x1 = x2.
  nchange with (match Byte x2 with [ Byte a ⇒ x1 = a | Word _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma b8w16_destruct_w16_w16 : ∀x1,x2.Word x1 = Word x2 → x1 = x2.
@@ -94,7 +90,7 @@ nlemma b8w16_destruct_w16_w16 : ∀x1,x2.Word x1 = Word x2 → x1 = x2.
  nchange with (match Word x2 with [ Word a ⇒ x1 = a | Byte _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma b8w16_destruct_b8_w16 : ∀x1,x2.Byte x1 = Word x2 → False.
@@ -121,10 +117,10 @@ nlemma symmetric_eqb8w16 : ∀bw1,bw2.eq_b8w16 bw1 bw2 = eq_b8w16 bw2 bw1.
  #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 ??)
+          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 ??)
+          napply refl_eq
  ##]
 nqed.