1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/bool.ma".
33 ninductive ProdT (T1:Type) (T2:Type) : Type ≝
34 pair : T1 → T2 → ProdT T1 T2.
37 : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Prop.
38 (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
40 λT1,T2:Type.λP:ProdT T1 T2 → Prop.
41 λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
43 match p with [ pair t t1 ⇒ f t t1 ].
46 : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Set.
47 (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
49 λT1,T2:Type.λP:ProdT T1 T2 → Set.
50 λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
52 match p with [ pair t t1 ⇒ f t t1 ].
54 ndefinition ProdT_rect
55 : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Type.
56 (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
58 λT1,T2:Type.λP:ProdT T1 T2 → Type.
59 λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
61 match p with [ pair t t1 ⇒ f t t1 ].
64 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair x _ ⇒ x ].
67 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair _ x ⇒ x ].
70 λT1,T2:Type.λp1,p2:ProdT T1 T2.
71 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.
72 match p1 with [ pair x1 y1 ⇒
73 match p2 with [ pair x2 y2 ⇒
74 (f1 x1 x2) ⊗ (f2 y1 y2) ]].
76 ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
77 triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
79 ndefinition Prod3T_ind
80 : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Prop.
81 (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
82 Πp:Prod3T T1 T2 T3.P p ≝
83 λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Prop.
84 λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
86 match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
88 ndefinition Prod3T_rec
89 : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Set.
90 (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
91 Πp:Prod3T T1 T2 T3.P p ≝
92 λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Set.
93 λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
95 match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
97 ndefinition Prod3T_rect
98 : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Type.
99 (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
100 Πp:Prod3T T1 T2 T3.P p ≝
101 λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Type.
102 λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
104 match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
107 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple x _ _ ⇒ x ].
110 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ x _ ⇒ x ].
113 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ].
115 ndefinition eq_triple ≝
116 λT1,T2,T3:Type.λp1,p2:Prod3T T1 T2 T3.
117 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.
118 match p1 with [ triple x1 y1 z1 ⇒
119 match p2 with [ triple x2 y2 z2 ⇒
120 (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ]].
122 ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
123 quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
125 ndefinition Prod4T_ind
126 : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Prop.
127 (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
128 Πp:Prod4T T1 T2 T3 T4.P p ≝
129 λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Prop.
130 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
131 λp:Prod4T T1 T2 T3 T4.
132 match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
134 ndefinition Prod4T_rec
135 : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Set.
136 (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
137 Πp:Prod4T T1 T2 T3 T4.P p ≝
138 λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Set.
139 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
140 λp:Prod4T T1 T2 T3 T4.
141 match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
143 ndefinition Prod4T_rect
144 : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Type.
145 (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
146 Πp:Prod4T T1 T2 T3 T4.P p ≝
147 λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Type.
148 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
149 λp:Prod4T T1 T2 T3 T4.
150 match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
153 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple x _ _ _ ⇒ x ].
156 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ x _ _ ⇒ x ].
159 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ x _ ⇒ x ].
162 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ].
164 ndefinition eq_quadruple ≝
165 λT1,T2,T3,T4:Type.λp1,p2:Prod4T T1 T2 T3 T4.
166 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.
167 match p1 with [ quadruple x1 y1 z1 w1 ⇒
168 match p2 with [ quadruple x2 y2 z2 w2 ⇒
169 (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ]].
171 ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
172 quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
174 ndefinition Prod5T_ind
175 : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Prop.
176 (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
177 Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
178 λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Prop.
179 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
180 λp:Prod5T T1 T2 T3 T4 T5.
181 match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
183 ndefinition Prod5T_rec
184 : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Set.
185 (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
186 Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
187 λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Set.
188 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
189 λp:Prod5T T1 T2 T3 T4 T5.
190 match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
192 ndefinition Prod5T_rect
193 : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Type.
194 (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
195 Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
196 λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Type.
197 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
198 λp:Prod5T T1 T2 T3 T4 T5.
199 match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
202 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple x _ _ _ _ ⇒ x ].
205 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ x _ _ _ ⇒ x ].
208 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ x _ _ ⇒ x ].
211 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ x _ ⇒ x ].
214 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
216 ndefinition eq_quintuple ≝
217 λT1,T2,T3,T4,T5:Type.λp1,p2:Prod5T T1 T2 T3 T4 T5.
218 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool.
219 match p1 with [ quintuple x1 y1 z1 w1 v1 ⇒
220 match p2 with [ quintuple x2 y2 z2 w2 v2 ⇒
221 (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ⊗ (f5 v1 v2) ]].