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 *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "universe/exadecim.ma".
25 (* operazioni su EX_UN *)
27 (* scheletro di funzione a 1 argomento *)
28 ndefinition farg1_unex ≝
29 λT:Type.λf1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:T.λe2:S_UN EX_UN.
30 match getelem ? e2 return λx.member_list ? x eq_UN EX_UN = true → T with
31 [ ux0 ⇒ λq:(true = true).f1 | ux1 ⇒ λq:(true = true).f2
32 | ux2 ⇒ λq:(true = true).f3 | ux3 ⇒ λq:(true = true).f4
33 | ux4 ⇒ λq:(true = true).f5 | ux5 ⇒ λq:(true = true).f6
34 | ux6 ⇒ λq:(true = true).f7 | ux7 ⇒ λq:(true = true).f8
35 | ux8 ⇒ λq:(true = true).f9 | ux9 ⇒ λq:(true = true).f10
36 | uxA ⇒ λq:(true = true).f11 | uxB ⇒ λq:(true = true).f12
37 | uxC ⇒ λq:(true = true).f13 | uxD ⇒ λq:(true = true).f14
38 | uxE ⇒ λq:(true = true).f15 | uxF ⇒ λq:(true = true).f16
39 | _ ⇒ λq:(false = true).False_rect_Type0 ? (bool_destruct … q)
42 (* scheletro di funzione a 2 argomenti *)
43 ndefinition farg2_unex ≝
44 λT:Type.λf1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:S_UN EX_UN → T.λe1:S_UN EX_UN.
45 match getelem ? e1 return λx.member_list ? x eq_UN EX_UN = true → S_UN EX_UN → T with
46 [ ux0 ⇒ λp:(true = true).f1
47 | ux1 ⇒ λp:(true = true).f2
48 | ux2 ⇒ λp:(true = true).f3
49 | ux3 ⇒ λp:(true = true).f4
50 | ux4 ⇒ λp:(true = true).f5
51 | ux5 ⇒ λp:(true = true).f6
52 | ux6 ⇒ λp:(true = true).f7
53 | ux7 ⇒ λp:(true = true).f8
54 | ux8 ⇒ λp:(true = true).f9
55 | ux9 ⇒ λp:(true = true).f10
56 | uxA ⇒ λp:(true = true).f11
57 | uxB ⇒ λp:(true = true).f12
58 | uxC ⇒ λp:(true = true).f13
59 | uxD ⇒ λp:(true = true).f14
60 | uxE ⇒ λp:(true = true).f15
61 | uxF ⇒ λp:(true = true).f16
62 | _ ⇒ λp:(false = true).False_rect_Type0 ? (bool_destruct … p)
65 (* scheletro di funzione a 2 argomenti simmetrica *)
66 ndefinition farg2sym_unex ≝
68 λf00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
69 λf11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
70 λf22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
71 λf33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
72 λf44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
73 λf55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
74 λf66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
75 λf77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
76 λf88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
77 λf99,f9A,f9B,f9C,f9D,f9E,f9F:T.
78 λfAA,fAB,fAC,fAD,fAE,fAF:T.
79 λfBB,fBC,fBD,fBE,fBF:T.
85 (farg1_unex ? f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F)
86 (farg1_unex ? f01 f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F)
87 (farg1_unex ? f02 f12 f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F)
88 (farg1_unex ? f03 f13 f23 f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F)
89 (farg1_unex ? f04 f14 f24 f34 f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F)
90 (farg1_unex ? f05 f15 f25 f35 f45 f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F)
91 (farg1_unex ? f06 f16 f26 f36 f46 f56 f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F)
92 (farg1_unex ? f07 f17 f27 f37 f47 f57 f67 f77 f78 f79 f7A f7B f7C f7D f7E f7F)
93 (farg1_unex ? f08 f18 f28 f38 f48 f58 f68 f78 f88 f89 f8A f8B f8C f8D f8E f8F)
94 (farg1_unex ? f09 f19 f29 f39 f49 f59 f69 f79 f89 f99 f9A f9B f9C f9D f9E f9F)
95 (farg1_unex ? f0A f1A f2A f3A f4A f5A f6A f7A f8A f9A fAA fAB fAC fAD fAE fAF)
96 (farg1_unex ? f0B f1B f2B f3B f4B f5B f6B f7B f8B f9B fAB fBB fBC fBD fBE fBF)
97 (farg1_unex ? f0C f1C f2C f3C f4C f5C f6C f7C f8C f9C fAC fBC fCC fCD fCE fCF)
98 (farg1_unex ? f0D f1D f2D f3D f4D f5D f6D f7D f8D f9D fAD fBD fCD fDD fDE fDF)
99 (farg1_unex ? f0E f1E f2E f3E f4E f5E f6E f7E f8E f9E fAE fBE fCE fDE fEE fEF)
100 (farg1_unex ? f0F f1F f2F f3F f4F f5F f6F f7F f8F f9F fAF fBF fCF fDF fEF fFF).
103 ndefinition eq_unex ≝ λe1,e2:S_UN EX_UN.eq_SUN ? e1 e2.
106 ndefinition lt_unex ≝
108 (farg1_unex ? false true true true true true true true true true true true true true true true)
109 (farg1_unex ? false false true true true true true true true true true true true true true true)
110 (farg1_unex ? false false false true true true true true true true true true true true true true)
111 (farg1_unex ? false false false false true true true true true true true true true true true true)
112 (farg1_unex ? false false false false false true true true true true true true true true true true)
113 (farg1_unex ? false false false false false false true true true true true true true true true true)
114 (farg1_unex ? false false false false false false false true true true true true true true true true)
115 (farg1_unex ? false false false false false false false false true true true true true true true true)
116 (farg1_unex ? false false false false false false false false false true true true true true true true)
117 (farg1_unex ? false false false false false false false false false false true true true true true true)
118 (farg1_unex ? false false false false false false false false false false false true true true true true)
119 (farg1_unex ? false false false false false false false false false false false false true true true true)
120 (farg1_unex ? false false false false false false false false false false false false false true true true)
121 (farg1_unex ? false false false false false false false false false false false false false false true true)
122 (farg1_unex ? false false false false false false false false false false false false false false false true)
123 (farg1_unex ? false false false false false false false false false false false false false false false false).
126 ndefinition le_unex ≝
128 (farg1_unex ? true true true true true true true true true true true true true true true true)
129 (farg1_unex ? false true true true true true true true true true true true true true true true)
130 (farg1_unex ? false false true true true true true true true true true true true true true true)
131 (farg1_unex ? false false false true true true true true true true true true true true true true)
132 (farg1_unex ? false false false false true true true true true true true true true true true true)
133 (farg1_unex ? false false false false false true true true true true true true true true true true)
134 (farg1_unex ? false false false false false false true true true true true true true true true true)
135 (farg1_unex ? false false false false false false false true true true true true true true true true)
136 (farg1_unex ? false false false false false false false false true true true true true true true true)
137 (farg1_unex ? false false false false false false false false false true true true true true true true)
138 (farg1_unex ? false false false false false false false false false false true true true true true true)
139 (farg1_unex ? false false false false false false false false false false false true true true true true)
140 (farg1_unex ? false false false false false false false false false false false false true true true true)
141 (farg1_unex ? false false false false false false false false false false false false false true true true)
142 (farg1_unex ? false false false false false false false false false false false false false false true true)
143 (farg1_unex ? false false false false false false false false false false false false false false false true).
146 ndefinition gt_unex ≝ λe1,e2:S_UN EX_UN.⊖(le_unex e1 e2).
149 ndefinition ge_unex ≝ λe1,e2:S_UN EX_UN.⊖(lt_unex e1 e2).
151 (* opeartore and : simmetrico per costruzione *)
152 ndefinition and_unex ≝
154 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0
155 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1
156 un_x2 un_x2 un_x0 un_x0 un_x2 un_x2 un_x0 un_x0 un_x2 un_x2 un_x0 un_x0 un_x2 un_x2
157 un_x3 un_x0 un_x1 un_x2 un_x3 un_x0 un_x1 un_x2 un_x3 un_x0 un_x1 un_x2 un_x3
158 un_x4 un_x4 un_x4 un_x4 un_x0 un_x0 un_x0 un_x0 un_x4 un_x4 un_x4 un_x4
159 un_x5 un_x4 un_x5 un_x0 un_x1 un_x0 un_x1 un_x4 un_x5 un_x4 un_x5
160 un_x6 un_x6 un_x0 un_x0 un_x2 un_x2 un_x4 un_x4 un_x6 un_x6
161 un_x7 un_x0 un_x1 un_x2 un_x3 un_x4 un_x5 un_x6 un_x7
162 un_x8 un_x8 un_x8 un_x8 un_x8 un_x8 un_x8 un_x8
163 un_x9 un_x8 un_x9 un_x8 un_x9 un_x8 un_x9
164 un_xA un_xA un_x8 un_x8 un_xA un_xA
165 un_xB un_x8 un_x9 un_xA un_xB
166 un_xC un_xC un_xC un_xC
172 esiste una regola semplice per ottenere associativo per costruzione?
173 ragionando in matrice simmetrico e' : a(i,j) = a(j,i) → A = trasposta(A)
174 ragionando in matrice associativo e' : a(a(i,j),k) = a(i,a(j,k)) → come espresso?
176 nlemma pippo : un_x3 = (and_unex un_x3 un_xF).
180 nlemma symmetric_farg2unex1 :
182 ∀f00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
183 ∀f11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
184 ∀f22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
185 ∀f33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
186 ∀f44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
187 ∀f55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
188 ∀f66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
189 ∀f77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
190 ∀f88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
191 ∀f99,f9A,f9B,f9C,f9D,f9E,f9F:T.
192 ∀fAA,fAB,fAC,fAD,fAE,fAF:T.
193 ∀fBB,fBC,fBD,fBE,fBF:T.
198 ∀dim1.∀dim2.∀y:S_UN EX_UN.
199 (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
200 f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
201 f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
202 f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
203 f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
204 f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
205 f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
206 f77 f78 f79 f7A f7B f7C f7D f7E f7F
207 f88 f89 f8A f8B f8C f8D f8E f8F
208 f99 f9A f9B f9C f9D f9E f9F
209 fAA fAB fAC fAD fAE fAF
215 (S_EL EX_UN ux0 dim1 dim2) y) =
216 (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
217 f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
218 f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
219 f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
220 f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
221 f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
222 f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
223 f77 f78 f79 f7A f7B f7C f7D f7E f7F
224 f88 f89 f8A f8B f8C f8D f8E f8F
225 f99 f9A f9B f9C f9D f9E f9F
226 fAA fAB fAC fAD fAE fAF
232 y (S_EL EX_UN ux0 dim1 dim2)).
234 #f00; #f01; #f02; #f03; #f04; #f05; #f06; #f07; #f08; #f09; #f0A; #f0B; #f0C; #f0D; #f0E; #f0F;
235 #f11; #f12; #f13; #f14; #f15; #f16; #f17; #f18; #f19; #f1A; #f1B; #f1C; #f1D; #f1E; #f1F;
236 #f22; #f23; #f24; #f25; #f26; #f27; #f28; #f29; #f2A; #f2B; #f2C; #f2D; #f2E; #f2F;
237 #f33; #f34; #f35; #f36; #f37; #f38; #f39; #f3A; #f3B; #f3C; #f3D; #f3E; #f3F;
238 #f44; #f45; #f46; #f47; #f48; #f49; #f4A; #f4B; #f4C; #f4D; #f4E; #f4F;
239 #f55; #f56; #f57; #f58; #f59; #f5A; #f5B; #f5C; #f5D; #f5E; #f5F;
240 #f66; #f67; #f68; #f69; #f6A; #f6B; #f6C; #f6D; #f6E; #f6F;
241 #f77; #f78; #f79; #f7A; #f7B; #f7C; #f7D; #f7E; #f7F;
242 #f88; #f89; #f8A; #f8B; #f8C; #f8D; #f8E; #f8F;
243 #f99; #f9A; #f9B; #f9C; #f9D; #f9E; #f9F;
244 #fAA; #fAB; #fAC; #fAD; #fAE; #fAF;
245 #fBB; #fBC; #fBD; #fBE; #fBF;
246 #fCC; #fCD; #fCE; #fCF;
250 #dim11; #dim12; #y; nelim y;
252 ##| ##1: #u; ncases u;
253 ##[ ##13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: #dim21; #dim22; nnormalize; napply refl_eq
254 ##| ##*: #dim21; nnormalize in dim21:(%); napply (bool_destruct … dim21)
259 ... e cosi via fino a
261 nlemma symmetric_farg2unex :
263 ∀f00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
264 ∀f11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
265 ∀f22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
266 ∀f33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
267 ∀f44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
268 ∀f55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
269 ∀f66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
270 ∀f77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
271 ∀f88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
272 ∀f99,f9A,f9B,f9C,f9D,f9E,f9F:T.
273 ∀fAA,fAB,fAC,fAD,fAE,fAF:T.
274 ∀fBB,fBC,fBD,fBE,fBF:T.
280 (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
281 f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
282 f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
283 f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
284 f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
285 f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
286 f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
287 f77 f78 f79 f7A f7B f7C f7D f7E f7F
288 f88 f89 f8A f8B f8C f8D f8E f8F
289 f99 f9A f9B f9C f9D f9E f9F
290 fAA fAB fAC fAD fAE fAF
297 (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
298 f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
299 f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
300 f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
301 f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
302 f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
303 f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
304 f77 f78 f79 f7A f7B f7C f7D f7E f7F
305 f88 f89 f8A f8B f8C f8D f8E f8F
306 f99 f9A f9B f9C f9D f9E f9F
307 fAA fAB fAC fAD fAE fAF
315 #f00; #f01; #f02; #f03; #f04; #f05; #f06; #f07; #f08; #f09; #f0A; #f0B; #f0C; #f0D; #f0E; #f0F;
316 #f11; #f12; #f13; #f14; #f15; #f16; #f17; #f18; #f19; #f1A; #f1B; #f1C; #f1D; #f1E; #f1F;
317 #f22; #f23; #f24; #f25; #f26; #f27; #f28; #f29; #f2A; #f2B; #f2C; #f2D; #f2E; #f2F;
318 #f33; #f34; #f35; #f36; #f37; #f38; #f39; #f3A; #f3B; #f3C; #f3D; #f3E; #f3F;
319 #f44; #f45; #f46; #f47; #f48; #f49; #f4A; #f4B; #f4C; #f4D; #f4E; #f4F;
320 #f55; #f56; #f57; #f58; #f59; #f5A; #f5B; #f5C; #f5D; #f5E; #f5F;
321 #f66; #f67; #f68; #f69; #f6A; #f6B; #f6C; #f6D; #f6E; #f6F;
322 #f77; #f78; #f79; #f7A; #f7B; #f7C; #f7D; #f7E; #f7F;
323 #f88; #f89; #f8A; #f8B; #f8C; #f8D; #f8E; #f8F;
324 #f99; #f9A; #f9B; #f9C; #f9D; #f9E; #f9F;
325 #fAA; #fAB; #fAC; #fAD; #fAE; #fAF;
326 #fBB; #fBC; #fBD; #fBE; #fBF;
327 #fCC; #fCD; #fCE; #fCF;
333 ##| ##1: #u; ncases u;
334 ##[ ##13: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
335 ##| ##14: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
336 ##| ##15: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
337 ##| ##16: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
338 ##| ##17: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
339 ##| ##18: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
340 ##| ##19: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
341 ##| ##20: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
342 ##| ##21: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
343 ##| ##22: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
344 ##| ##23: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
345 ##| ##24: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
346 ##| ##25: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
347 ##| ##26: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
348 ##| ##27: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
349 ##| ##28: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
350 ##| ##*: #dim1; nnormalize in dim1:(%) napply (bool_destruct … dim1)