X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Ftheory.ma;h=228692451a5d3637bd8a1a95d17edc3c7bfd3849;hb=c39f5efd7ee59d07dd62ddef25d7cd09a1a3a704;hp=dcf3789fda825512c7a055221e8186059070bf44;hpb=c3fc204cc02f1031b5d17fb0f2be1fc01e5c452f;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
index dcf3789fd..228692451 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.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/pts.ma".
@@ -35,31 +31,31 @@ include "freescale/pts.ma".
 ninductive True: Prop ≝
  I : True.
 
-ndefinition True_ind : ΠP:Prop.P → True → P ≝
+(*ndefinition True_ind_xx : ΠP:Prop.P → True → P ≝
 λP:Prop.λp:P.λH:True.
  match H with [ I ⇒ p ].
 
-ndefinition True_rec : ΠP:Set.P → True → P ≝
+ndefinition True_rec_xx : ΠP:Set.P → True → P ≝
 λP:Set.λp:P.λH:True.
  match H with [ I ⇒ p ].
 
-ndefinition True_rect : ΠP:Type.P → True → P ≝
+ndefinition True_rect_xx : ΠP:Type.P → True → P ≝
 λP:Type.λp:P.λH:True.
- match H with [ I ⇒ p ].
+ match H with [ I ⇒ p ].*)
 
 ninductive False: Prop ≝.
 
-ndefinition False_ind : ΠP:Prop.False → P ≝
+(*ndefinition False_ind_xx : ΠP:Prop.False → P ≝
 λP:Prop.λH:False.
  match H in False return λH1:False.P with [].
 
-ndefinition False_rec : ΠP:Set.False → P ≝
+ndefinition False_rec_xx : ΠP:Set.False → P ≝
 λP:Set.λH:False.
  match H in False return λH1:False.P with [].
 
-ndefinition False_rect : ΠP:Type.False → P ≝
+ndefinition False_rect_xx : ΠP:Type.False → P ≝
 λP:Type.λH:False.
- match H in False return λH1:False.P with [].
+ match H in False return λH1:False.P with [].*)
 
 ndefinition Not: Prop → Prop ≝
 λA.(A → False).
@@ -70,7 +66,8 @@ nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  #A; #C; #H;
  nnormalize;
  #H1;
- nelim (H1 H).
+ (* perche' non fa nelim (H1 H). ??? *)
+ napply (False_ind ? (H1 H)).
 nqed.
 
 nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
@@ -83,17 +80,17 @@ nqed.
 ninductive And (A,B:Prop) : Prop ≝
  conj : A → B → (And A B).
 
-ndefinition And_ind : ΠA,B:Prop.ΠP:Prop.(A → B → P) → And A B → P ≝
+(*ndefinition And_ind_xx : ΠA,B:Prop.ΠP:Prop.(A → B → P) → And A B → P ≝
 λA,B:Prop.λP:Prop.λf:A → B → P.λH:And A B.
  match H with [conj H1 H2 ⇒ f H1 H2 ].
 
-ndefinition And_rec : ΠA,B:Prop.ΠP:Set.(A → B → P) → And A B → P ≝
+ndefinition And_rec_xx : ΠA,B:Prop.ΠP:Set.(A → B → P) → And A B → P ≝
 λA,B:Prop.λP:Set.λf:A → B → P.λH:And A B.
  match H with [conj H1 H2 ⇒ f H1 H2 ].
 
-ndefinition And_rect : ΠA,B:Prop.ΠP:Type.(A → B → P) → And A B → P ≝
+ndefinition And_rect_xx : ΠA,B:Prop.ΠP:Type.(A → B → P) → And A B → P ≝
 λA,B:Prop.λP:Type.λf:A → B → P.λH:And A B.
- match H with [conj H1 H2 ⇒ f H1 H2 ].
+ match H with [conj H1 H2 ⇒ f H1 H2 ].*)
 
 interpretation "logical and" 'and x y = (And x y).
 
@@ -115,9 +112,9 @@ ninductive Or (A,B:Prop) : Prop ≝
   or_introl : A → (Or A B)
 | or_intror : B → (Or A B).
 
-ndefinition Or_ind : ΠA,B:Prop.ΠP:Prop.(A → P) → (B → P) → Or A B → P ≝
+(*ndefinition Or_ind_xx : ΠA,B:Prop.ΠP:Prop.(A → P) → (B → P) → Or A B → P ≝
 λA,B:Prop.λP:Prop.λf1:A → P.λf2:B → P.λH:Or A B.
- match H with [ or_introl H1 ⇒ f1 H1 | or_intror H1 ⇒ f2 H1 ].
+ match H with [ or_introl H1 ⇒ f1 H1 | or_intror H1 ⇒ f2 H1 ].*)
 
 interpretation "logical or" 'or x y = (Or x y).
 
@@ -126,18 +123,18 @@ ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
  ex_intro: ∀x:A.Q x → ex A Q.
 
-ndefinition ex_ind : ΠA:Type.ΠQ:A → Prop.ΠP:Prop.(Πa:A.Q a → P) → ex A Q → P ≝
+(*ndefinition ex_ind_xx : ΠA:Type.ΠQ:A → Prop.ΠP:Prop.(Πa:A.Q a → P) → ex A Q → P ≝
 λA:Type.λQ:A → Prop.λP:Prop.λf:(Πa:A.Q a → P).λH:ex A Q.
- match H with [ ex_intro H1 H2 ⇒ f H1 H2 ].
+ match H with [ ex_intro H1 H2 ⇒ f H1 H2 ].*)
 
 interpretation "exists" 'exists x = (ex ? x).
 
 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 
-ndefinition ex2_ind : ΠA:Type.ΠQ,R:A → Prop.ΠP:Prop.(Πa:A.Q a → R a → P) → ex2 A Q R → P ≝
+(*ndefinition ex2_ind_xx : ΠA:Type.ΠQ,R:A → Prop.ΠP:Prop.(Πa:A.Q a → R a → P) → ex2 A Q R → P ≝
 λA:Type.λQ,R:A → Prop.λP:Prop.λf:(Πa:A.Q a → R a → P).λH:ex2 A Q R.
- match H with [ ex_intro2 H1 H2 H3 ⇒ f H1 H2 H3 ].
+ match H with [ ex_intro2 H1 H2 H3 ⇒ f H1 H2 H3 ].*)
 
 ndefinition iff ≝
 λA,B.(A -> B) ∧ (B -> A).
@@ -173,17 +170,17 @@ ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 ninductive eq (A:Type) (x:A) : A → Prop ≝
  refl_eq : eq A x x.
 
-ndefinition eq_ind : ΠA:Type.Πx:A.ΠP:A → Prop.P x → Πa:A.eq A x a → P a ≝
+(*ndefinition eq_ind_xx : ΠA:Type.Πx:A.ΠP:A → Prop.P x → Πa:A.eq A x a → P a ≝
 λA:Type.λx:A.λP:A → Prop.λp:P x.λa:A.λH:eq A x a.
  match H with [refl_eq ⇒ p ].
 
-ndefinition eq_rec : ΠA:Type.Πx:A.ΠP:A → Set.P x → Πa:A.eq A x a → P a ≝
+ndefinition eq_rec_xx : ΠA:Type.Πx:A.ΠP:A → Set.P x → Πa:A.eq A x a → P a ≝
 λA:Type.λx:A.λP:A → Set.λp:P x.λa:A.λH:eq A x a.
  match H with [refl_eq ⇒ p ].
 
-ndefinition eq_rect : ΠA:Type.Πx:A.ΠP:A → Type.P x → Πa:A.eq A x a → P a ≝
+ndefinition eq_rect_xx : ΠA:Type.Πx:A.ΠP:A → Type.P x → Πa:A.eq A x a → P a ≝
 λA:Type.λx:A.λP:A → Type.λp:P x.λa:A.λH:eq A x a.
- match H with [refl_eq ⇒ p ].
+ match H with [refl_eq ⇒ p ].*)
 
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
@@ -193,6 +190,9 @@ nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  #A;
  nnormalize;
  #x; #y; #H;
+ (* rifiuta nrewrite >, nrewrite <
+    e la prima volta mi ha risposto con assert false,
+    poi con errori di tipo ??? *) 
  nrewrite < H;
  napply (refl_eq ??).
 nqed.