freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / common / theory.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index bb1358926ccde64c1ba6b7eb65896b99b1c3c365..c4bd19f167a1974ff29e08707c916e27da28a92b 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -57,37 +57,171 @@ nlemma prop_to_nnprop : ∀P.P → ¬¬P.
  napply (H1 H).
 nqed.
 
-ninductive And (A,B:Prop) : Prop ≝
- conj : A → B → (And A B).
+ninductive And2 (A,B:Prop) : Prop ≝
+ conj2 : A → B → (And2 A B).
 
-interpretation "logical and" 'and x y = (And x y).
+interpretation "logical and" 'and x y = (And2 x y).
 
-nlemma proj1: ∀A,B:Prop.A ∧ B → A.
+nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
  #A; #B; #H;
- (* \ldots al posto di ??? *)
- napply (And_ind A B … H);
+ napply (And2_ind A B … H);
  #H1; #H2;
  napply H1.
 nqed.
 
-nlemma proj2: ∀A,B:Prop.A ∧ B → B.
+nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
  #A; #B; #H;
- napply (And_ind A B … H);
+ napply (And2_ind A B … H);
  #H1; #H2;
  napply H2.
 nqed.
 
-ninductive Or (A,B:Prop) : Prop ≝
-  or_introl : A → (Or A B)
-| or_intror : B → (Or A B).
+ninductive And3 (A,B,C:Prop) : Prop ≝
+ conj3 : A → B → C → (And3 A B C).
 
-interpretation "logical or" 'or x y = (Or x y).
+nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
+ #A; #B; #C; #H;
+ napply (And3_ind A B C … H);
+ #H1; #H2; #H3;
+ napply H1.
+nqed.
+
+nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
+ #A; #B; #C; #H;
+ napply (And3_ind A B C … H);
+ #H1; #H2; #H3;
+ napply H2.
+nqed.
+
+nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
+ #A; #B; #C; #H;
+ napply (And3_ind A B C … H);
+ #H1; #H2; #H3;
+ napply H3.
+nqed.
+
+ninductive And4 (A,B,C,D:Prop) : Prop ≝
+ conj4 : A → B → C → D → (And4 A B C D).
+
+nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H1.
+nqed.
+
+nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H2.
+nqed.
+
+nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H3.
+nqed.
+
+nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H4.
+nqed.
+
+ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
+ conj5 : A → B → C → D → E → (And5 A B C D E).
+
+nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H1.
+nqed.
+
+nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H2.
+nqed.
+
+nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H3.
+nqed.
+
+nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H4.
+nqed.
+
+nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H5.
+nqed.
+
+ninductive Or2 (A,B:Prop) : Prop ≝
+  or2_intro1 : A → (Or2 A B)
+| or2_intro2 : B → (Or2 A B).
+
+interpretation "logical or" 'or x y = (Or2 x y).
 
 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
 
-nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G.
- #P; #Q; #G; #H; #H1; #H2;
- napply (Or_ind P Q ? H1 H2 ?);
+nlemma or2_elim
+ : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
+ #P1; #P2; #Q; #H; #f1; #f2;
+ napply (Or2_ind P1 P2 ? f1 f2 ?);
+ napply H.
+nqed.
+
+ninductive Or3 (A,B,C:Prop) : Prop ≝
+  or3_intro1 : A → (Or3 A B C)
+| or3_intro2 : B → (Or3 A B C)
+| or3_intro3 : C → (Or3 A B C).
+
+nlemma or3_elim
+ : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
+ #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
+ napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
+ napply H.
+nqed.
+
+ninductive Or4 (A,B,C,D:Prop) : Prop ≝
+  or4_intro1 : A → (Or4 A B C D)
+| or4_intro2 : B → (Or4 A B C D)
+| or4_intro3 : C → (Or4 A B C D)
+| or4_intro4 : D → (Or4 A B C D).
+
+nlemma or4_elim
+ : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
+   ∀f3:P3 → Q.∀f4:P4 → Q.Q.
+ #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
+ napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
+ napply H.
+nqed.
+
+ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
+  or5_intro1 : A → (Or5 A B C D E)
+| or5_intro2 : B → (Or5 A B C D E)
+| or5_intro3 : C → (Or5 A B C D E)
+| or5_intro4 : D → (Or5 A B C D E)
+| or5_intro5 : E → (Or5 A B C D E).
+
+nlemma or5_elim
+ : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
+   ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
+ #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
+ napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
  napply H.
 nqed.