]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/common/prod.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / ng_assembly / common / prod.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "num/bool.ma".
24
25 (* ***** *)
26 (* TUPLE *)
27 (* ***** *)
28
29 ninductive ProdT (T1:Type) (T2:Type) : Type ≝
30  pair : T1 → T2 → ProdT T1 T2.
31
32 ndefinition fst ≝
33 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  x _ ⇒ x ].
34
35 ndefinition snd ≝
36 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  _ x ⇒ x ].
37
38 ndefinition eq_pair ≝
39 λT1,T2:Type.
40 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.
41 λp1,p2:ProdT T1 T2.
42  (f1 (fst … p1) (fst … p2)) ⊗
43  (f2 (snd … p1) (snd … p2)).
44
45 ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
46 triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
47
48 ndefinition fst3T ≝
49 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple x _ _ ⇒ x ].
50
51 ndefinition snd3T ≝
52 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ x _ ⇒ x ].
53
54 ndefinition thd3T ≝
55 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ].
56
57 ndefinition eq_triple ≝
58 λT1,T2,T3:Type.
59 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.
60 λp1,p2:Prod3T T1 T2 T3.
61  (f1 (fst3T … p1) (fst3T … p2)) ⊗
62  (f2 (snd3T … p1) (snd3T … p2)) ⊗
63  (f3 (thd3T … p1) (thd3T … p2)).
64
65 ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
66 quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
67
68 ndefinition fst4T ≝
69 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple x _ _ _ ⇒ x ].
70
71 ndefinition snd4T ≝
72 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ x _ _ ⇒ x ].
73
74 ndefinition thd4T ≝
75 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ x _ ⇒ x ].
76
77 ndefinition fth4T ≝
78 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ].
79
80 ndefinition eq_quadruple ≝
81 λT1,T2,T3,T4:Type.
82 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.
83 λp1,p2:Prod4T T1 T2 T3 T4.
84  (f1 (fst4T … p1) (fst4T … p2)) ⊗
85  (f2 (snd4T … p1) (snd4T … p2)) ⊗
86  (f3 (thd4T … p1) (thd4T … p2)) ⊗
87  (f4 (fth4T … p1) (fth4T … p2)).
88
89 ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
90 quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
91
92 ndefinition fst5T ≝
93 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple x _ _ _ _ ⇒ x ].
94
95 ndefinition snd5T ≝
96 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ x _ _ _ ⇒ x ].
97
98 ndefinition thd5T ≝
99 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ x _ _ ⇒ x ].
100
101 ndefinition fth5T ≝
102 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ x _ ⇒ x ].
103
104 ndefinition fft5T ≝
105 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
106
107 ndefinition eq_quintuple ≝
108 λT1,T2,T3,T4,T5:Type.
109 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool.
110 λp1,p2:Prod5T T1 T2 T3 T4 T5.
111  (f1 (fst5T … p1) (fst5T … p2)) ⊗
112  (f2 (snd5T … p1) (snd5T … p2)) ⊗
113  (f3 (thd5T … p1) (thd5T … p2)) ⊗
114  (f4 (fth5T … p1) (fth5T … p2)) ⊗
115  (f5 (fft5T … p1) (fft5T … p2)).