X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Foption_lemmas.ma;h=82a33c9f8d4bbcb2a00aa2148ebf843266af7af1;hb=11a6c88f3e717b019be2eae71711c70473b5467a;hp=30df5ac07ce6f277a3ed92ca745647b2f56bf4c3;hpb=64bdbee95e40a5be3bb6c5c2866869103730a4d0;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
index 30df5ac07..82a33c9f8 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.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/bool_lemmas.ma".
@@ -31,7 +27,7 @@ include "freescale/option.ma".
 (* OPTION *)
 (* ****** *)
 
-nlemma option_destruct : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
+nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
  #T; #x1; #x2; #H;
  nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
  nrewrite < H;
@@ -55,49 +51,51 @@ nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
  napply I.
 nqed.
 
-nlemma bsymmetric_eqoption :
-∀T:Type.∀o1,o2:option T.∀f:T → T → bool.
+nlemma symmetric_eqoption :
+∀T:Type.∀op1,op2:option T.∀f:T → T → bool.
  (symmetricT T bool f) →
- (eq_option T o1 o2 f = eq_option T o2 o1 f).
- #T; #o1; #o2; #f; #H;
- ncases o1;
- ncases o2;
+ (eq_option T op1 op2 f = eq_option T op2 op1 f).
+ #T; #op1; #op2; #f; #H;
+ napply (option_ind T ??? op1);
+ napply (option_ind T ??? op2);
  nnormalize;
  ##[ ##1: napply (refl_eq ??)
- ##| ##2,3: #x; napply (refl_eq ??)
- ##| ##4: #x1; #x2; nrewrite > (H x1 x2); napply (refl_eq ??)
+ ##| ##2,3: #H; napply (refl_eq ??)
+ ##| ##4: #a; #a0;
+          nrewrite > (H a0 a);
+          napply (refl_eq ??)
  ##]
 nqed.
 
 nlemma eq_to_eqoption :
-∀T.∀o1,o2:option T.∀f:T → T → bool.
+∀T.∀op1,op2:option T.∀f:T → T → bool.
  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
- (o1 = o2 → eq_option T o1 o2 f = true).
- #T; #o1; #o2; #f; #H;
- ncases o1;
- ncases o2;
- ##[ ##1: nnormalize; #H1; napply (refl_eq ??)
- ##| ##2: #H1; #H2; nelim (option_destruct_none_some ?? H2)
- ##| ##3: #H1; #H2; nelim (option_destruct_some_none ?? H2)
- ##| ##4: #x1; #x2; #H1;
-          nrewrite > (option_destruct ??? H1);
-          nnormalize;
-          nrewrite > (H x1 x1 (refl_eq ??));
+ (op1 = op2 → eq_option T op1 op2 f = true).
+ #T; #op1; #op2; #f; #H;
+ napply (option_ind T ??? op1);
+ napply (option_ind T ??? op2);
+ nnormalize;
+ ##[ ##1: #H1; napply (refl_eq ??)
+ ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
+ ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
+ ##| ##4: #a; #a0; #H1;
+          nrewrite > (option_destruct_some_some ??? H1);
+          nrewrite > (H a a (refl_eq ??));
           napply (refl_eq ??)
  ##]
 nqed.
 
 nlemma eqoption_to_eq :
-∀T.∀o1,o2:option T.∀f:T → T → bool.
+∀T.∀op1,op2:option T.∀f:T → T → bool.
  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
- (eq_option T o1 o2 f = true → o1 = o2).
- #T; #o1; #o2; #f; #H;
- ncases o1;
- ncases o2;
- ##[ ##1: nnormalize; #H1; napply (refl_eq ??)
- ##| ##2,3: #H1; #H2; nnormalize in H2:(%); napply (bool_destruct ??? H2)
- ##| ##4: #x1; #x2; #H1;
-          nnormalize in H1:(%);
+ (eq_option T op1 op2 f = true → op1 = op2).
+ #T; #op1; #op2; #f; #H;
+ napply (option_ind T ??? op1);
+ napply (option_ind T ??? op2);
+ nnormalize;
+ ##[ ##1: #H1; napply (refl_eq ??)
+ ##| ##2,3: #a; #H1; napply (bool_destruct ??? H1)
+ ##| ##4: #a; #a0; #H1;
           nrewrite > (H ?? H1);
           napply (refl_eq ??)
  ##]