X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Ftheory.ma;h=a9e6287a8a074741fd7a3f140f01b3b7120cb004;hb=dcde2b362a4106e36623d25e6a2d26dffac61848;hp=ceda6dccac7680d1b491918fa64f8b1e28df4da9;hpb=55274856efac172aba293d4216fdc659d07a89d7;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 ceda6dcca..a9e6287a8 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".
@@ -30,48 +26,26 @@ include "freescale/pts.ma".
 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
 (* ********************************** *)
 
+(* logic/connectives.ma *)
+
 ninductive True: Prop ≝
  I : True.
 
-ndefinition True_ind : ΠP:Prop.P → True → P ≝
-λP:Prop.λp:P.λH:True.
- match H with [ I ⇒ p ].
-
-ndefinition True_rec : ΠP:Set.P → True → P ≝
-λP:Set.λp:P.λH:True.
- match H with [ I ⇒ p ].
-
-ndefinition True_rect : ΠP:Type.P → True → P ≝
-λP:Type.λp:P.λH:True.
- match H with [ I ⇒ p ].
-
 ninductive False: Prop ≝.
 
-ndefinition False_ind : ΠP:Prop.False → P ≝
-λP:Prop.λH:False.
- match H in False return λH1:False.P with [].
-
-ndefinition False_rec : ΠP:Set.False → P ≝
-λP:Set.λH:False.
- match H in False return λH1:False.P with [].
-
-ndefinition False_rect : ΠP:Type.False → P ≝
-λP:Type.λH:False.
- match H in False return λH1:False.P with [].
-
 ndefinition Not: Prop → Prop ≝
 λA.(A → False).
 
 interpretation "logical not" 'not x = (Not x).
 
-ntheorem absurd : ∀A,C:Prop.A → ¬A → C.
+nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  #A; #C; #H;
  nnormalize;
  #H1;
- nelim (H1 H).
+ nelim (H1 H);
 nqed.
 
-ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
+nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
  #A; #B; #H;
  nnormalize;
  #H1; #H2;
@@ -81,30 +55,19 @@ 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 ≝
-λ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 ≝
-λ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 ≝
-λA,B:Prop.λP:Type.λf:A → B → P.λH:And A B.
- match H with [conj H1 H2 ⇒ f H1 H2 ].
-
 interpretation "logical and" 'and x y = (And x y).
 
-ntheorem proj1: ∀A,B:Prop.A ∧ B → A.
+nlemma proj1: ∀A,B:Prop.A ∧ B → A.
  #A; #B; #H;
- napply (And_ind A B ?? H);
+ (* \ldots al posto di ??? *)
+ napply (And_ind A B … H);
  #H1; #H2;
  napply H1.
 nqed.
 
-ntheorem proj2: ∀A,B:Prop.A ∧ B → B.
+nlemma proj2: ∀A,B:Prop.A ∧ B → B.
  #A; #B; #H;
- napply (And_ind A B ?? H);
+ napply (And_ind A B … H);
  #H1; #H2;
  napply H2.
 nqed.
@@ -113,10 +76,6 @@ 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 ≝
-λ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 ].
-
 interpretation "logical or" 'or x y = (Or x y).
 
 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
@@ -124,21 +83,15 @@ 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 ≝
-λ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 ].
-
 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 ≝
-λ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 ].
-
 ndefinition iff ≝
-λA,B.(A -> B) ∧ (B -> A).
+λA,B.(A → B) ∧ (B → A).
+
+(* higher_order_defs/relations *)
 
 ndefinition relation : Type → Type ≝
 λA:Type.A → A → Prop. 
@@ -164,36 +117,128 @@ ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x,y:A.R x y → ¬ (R y x).
 
+(* logic/equality.ma *)
+
 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 ≝
-λ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 ≝
-λ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 ≝
-λA:Type.λx:A.λP:A → Type.λp:P x.λa:A.λH:eq A x a.
- match H with [refl_eq ⇒ p ].
-
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 
-ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
+nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  #A;
  nnormalize;
  #x; #y; #H;
  nrewrite < H;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
-ntheorem eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  #A; #x; #P; #H; #y; #H1;
- napply (eq_ind ? x ? H y ?);
- nrewrite < H1;
- napply (refl_eq ??).
+ nrewrite < (symmetric_eq … H1);
+ napply H.
+nqed.
+
+ndefinition relationT : Type → Type → Type ≝
+λA,T:Type.A → A → T.
+
+ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
+λA,T.λR.∀x,y:A.R x y = R y x.
+
+ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
+λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
+
+(* list/list.ma *)
+
+ninductive list (A:Type) : Type ≝
+  nil: list A
+| cons: A → list A → list A.
+
+nlet rec append A (l1: list A) l2 on l1 ≝
+ match l1 with
+  [ nil ⇒ l2
+  | (cons hd tl) ⇒ cons A hd (append A tl l2) ].
+
+notation "hvbox(hd break :: tl)"
+  right associative with precedence 47
+  for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+  non associative with precedence 90
+  for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+  right associative with precedence 47
+  for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2.
+ #T; #x1; #x2; #y1; #y2; #H;
+ nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
+ #T; #x1; #x2; #y1; #y2; #H;
+ nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
+ #T; #x; #y; #H;
+ nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
+ nrewrite > H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
+ #T; #x; #y; #H;
+ nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
+ #T; #l;
+ nelim l;
+ nnormalize;
+ ##[ ##1: napply refl_eq
+ ##| ##2: #x; #y; #H;
+          nrewrite > H;
+          napply refl_eq
+ ##]
+nqed.
+
+nlemma associative_list : ∀T.associative (list T) (append T).
+ #T; #x; #y; #z;
+ nelim x;
+ nnormalize;
+ ##[ ##1: napply refl_eq
+ ##| ##2: #a; #b; #H;
+          nrewrite > H;
+          napply refl_eq
+ ##]
+nqed.
+
+nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
+ #T; #l1; #l2; #a;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
+ #T; #a; #l; #l1;
+ nrewrite > (associative_list T l [a] l1);
+ nnormalize;
+ napply refl_eq.
 nqed.