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 set "baseuri" "cic:/matita/freescale/memory_struct/".
29 (*include "/media/VIRTUOSO/freescale/translation.ma".*)
30 include "freescale/translation.ma".
32 (* **************************** *)
33 (* TIPI PER I MODULI DI MEMORIA *)
34 (* **************************** *)
36 (* tipi di memoria:RAM/ROM/non installata *)
37 inductive memory_type : Type ≝
38 MEM_READ_ONLY: memory_type
39 | MEM_READ_WRITE: memory_type
40 | MEM_OUT_OF_BOUND: memory_type.
42 (* **************** *)
43 (* TIPO ARRAY DA 16 *)
44 (* **************** *)
46 (* definizione di un array omogeneo di dimensione 16 *)
47 inductive Prod16T (T:Type) : Type ≝
48 array_16T : T → T → T → T → T → T → T → T →
49 T → T → T → T → T → T → T → T →
52 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
53 (* posso definire un getter a matrice sull'array *)
54 definition getn_array16T ≝
55 λn:exadecim.λT:Type.λp:Prod16T T.
57 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
59 [ x0 ⇒ e00 | x1 ⇒ e01 | x2 ⇒ e02 | x3 ⇒ e03 | x4 ⇒ e04 | x5 ⇒ e05 | x6 ⇒ e06 | x7 ⇒ e07
60 | x8 ⇒ e08 | x9 ⇒ e09 | xA ⇒ e10 | xB ⇒ e11 | xC ⇒ e12 | xD ⇒ e13 | xE ⇒ e14 | xF ⇒ e15
63 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
64 (* posso definire un setter a matrice sull'array *)
65 definition setn_array16T ≝
66 λn:exadecim.λT:Type.λp:Prod16T T.λv:T.
68 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
70 [ x0 ⇒ array_16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
71 | x1 ⇒ array_16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
72 | x2 ⇒ array_16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
73 | x3 ⇒ array_16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
74 | x4 ⇒ array_16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
75 | x5 ⇒ array_16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
76 | x6 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15
77 | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15
78 | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15
79 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15
80 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15
81 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15
82 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15
83 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15
84 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15
85 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v
88 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
89 (* posso definire un setter multiplo [m,n] a matrice sull'array *)
90 definition setmn_array16T ≝
91 λm,n:exadecim.λT:Type.λp:Prod16T T.λv:T.
93 [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒
96 [ x0 ⇒ array_16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
97 | x1 ⇒ array_16T T v v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
98 | x2 ⇒ array_16T T v v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
99 | x3 ⇒ array_16T T v v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
100 | x4 ⇒ array_16T T v v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
101 | x5 ⇒ array_16T T v v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
102 | x6 ⇒ array_16T T v v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
103 | x7 ⇒ array_16T T v v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15
104 | x8 ⇒ array_16T T v v v v v v v v v e09 e10 e11 e12 e13 e14 e15
105 | x9 ⇒ array_16T T v v v v v v v v v v e10 e11 e12 e13 e14 e15
106 | xA ⇒ array_16T T v v v v v v v v v v v e11 e12 e13 e14 e15
107 | xB ⇒ array_16T T v v v v v v v v v v v v e12 e13 e14 e15
108 | xC ⇒ array_16T T v v v v v v v v v v v v v e13 e14 e15
109 | xD ⇒ array_16T T v v v v v v v v v v v v v v e14 e15
110 | xE ⇒ array_16T T v v v v v v v v v v v v v v v e15
111 | xF ⇒ array_16T T v v v v v v v v v v v v v v v v ]
114 | x1 ⇒ array_16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
115 | x2 ⇒ array_16T T e00 v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
116 | x3 ⇒ array_16T T e00 v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
117 | x4 ⇒ array_16T T e00 v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
118 | x5 ⇒ array_16T T e00 v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
119 | x6 ⇒ array_16T T e00 v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
120 | x7 ⇒ array_16T T e00 v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15
121 | x8 ⇒ array_16T T e00 v v v v v v v v e09 e10 e11 e12 e13 e14 e15
122 | x9 ⇒ array_16T T e00 v v v v v v v v v e10 e11 e12 e13 e14 e15
123 | xA ⇒ array_16T T e00 v v v v v v v v v v e11 e12 e13 e14 e15
124 | xB ⇒ array_16T T e00 v v v v v v v v v v v e12 e13 e14 e15
125 | xC ⇒ array_16T T e00 v v v v v v v v v v v v e13 e14 e15
126 | xD ⇒ array_16T T e00 v v v v v v v v v v v v v e14 e15
127 | xE ⇒ array_16T T e00 v v v v v v v v v v v v v v e15
128 | xF ⇒ array_16T T e00 v v v v v v v v v v v v v v v ]
131 | x2 ⇒ array_16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
132 | x3 ⇒ array_16T T e00 e01 v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
133 | x4 ⇒ array_16T T e00 e01 v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
134 | x5 ⇒ array_16T T e00 e01 v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
135 | x6 ⇒ array_16T T e00 e01 v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
136 | x7 ⇒ array_16T T e00 e01 v v v v v v e08 e09 e10 e11 e12 e13 e14 e15
137 | x8 ⇒ array_16T T e00 e01 v v v v v v v e09 e10 e11 e12 e13 e14 e15
138 | x9 ⇒ array_16T T e00 e01 v v v v v v v v e10 e11 e12 e13 e14 e15
139 | xA ⇒ array_16T T e00 e01 v v v v v v v v v e11 e12 e13 e14 e15
140 | xB ⇒ array_16T T e00 e01 v v v v v v v v v v e12 e13 e14 e15
141 | xC ⇒ array_16T T e00 e01 v v v v v v v v v v v e13 e14 e15
142 | xD ⇒ array_16T T e00 e01 v v v v v v v v v v v v e14 e15
143 | xE ⇒ array_16T T e00 e01 v v v v v v v v v v v v v e15
144 | xF ⇒ array_16T T e00 e01 v v v v v v v v v v v v v v ]
146 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p
147 | x3 ⇒ array_16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
148 | x4 ⇒ array_16T T e00 e01 e02 v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
149 | x5 ⇒ array_16T T e00 e01 e02 v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
150 | x6 ⇒ array_16T T e00 e01 e02 v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
151 | x7 ⇒ array_16T T e00 e01 e02 v v v v v e08 e09 e10 e11 e12 e13 e14 e15
152 | x8 ⇒ array_16T T e00 e01 e02 v v v v v v e09 e10 e11 e12 e13 e14 e15
153 | x9 ⇒ array_16T T e00 e01 e02 v v v v v v v e10 e11 e12 e13 e14 e15
154 | xA ⇒ array_16T T e00 e01 e02 v v v v v v v v e11 e12 e13 e14 e15
155 | xB ⇒ array_16T T e00 e01 e02 v v v v v v v v v e12 e13 e14 e15
156 | xC ⇒ array_16T T e00 e01 e02 v v v v v v v v v v e13 e14 e15
157 | xD ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v e14 e15
158 | xE ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v v e15
159 | xF ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v v v ]
161 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p
162 | x4 ⇒ array_16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
163 | x5 ⇒ array_16T T e00 e01 e02 e03 v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
164 | x6 ⇒ array_16T T e00 e01 e02 e03 v v v e07 e08 e09 e10 e11 e12 e13 e14 e15
165 | x7 ⇒ array_16T T e00 e01 e02 e03 v v v v e08 e09 e10 e11 e12 e13 e14 e15
166 | x8 ⇒ array_16T T e00 e01 e02 e03 v v v v v e09 e10 e11 e12 e13 e14 e15
167 | x9 ⇒ array_16T T e00 e01 e02 e03 v v v v v v e10 e11 e12 e13 e14 e15
168 | xA ⇒ array_16T T e00 e01 e02 e03 v v v v v v v e11 e12 e13 e14 e15
169 | xB ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v e12 e13 e14 e15
170 | xC ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v e13 e14 e15
171 | xD ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v e14 e15
172 | xE ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v v e15
173 | xF ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v v v ]
175 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p
176 | x5 ⇒ array_16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
177 | x6 ⇒ array_16T T e00 e01 e02 e03 e04 v v e07 e08 e09 e10 e11 e12 e13 e14 e15
178 | x7 ⇒ array_16T T e00 e01 e02 e03 e04 v v v e08 e09 e10 e11 e12 e13 e14 e15
179 | x8 ⇒ array_16T T e00 e01 e02 e03 e04 v v v v e09 e10 e11 e12 e13 e14 e15
180 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v e10 e11 e12 e13 e14 e15
181 | xA ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v e11 e12 e13 e14 e15
182 | xB ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v e12 e13 e14 e15
183 | xC ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v e13 e14 e15
184 | xD ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v e14 e15
185 | xE ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v v e15
186 | xF ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v v v ]
188 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p
189 | x6 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15
190 | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v e08 e09 e10 e11 e12 e13 e14 e15
191 | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v e09 e10 e11 e12 e13 e14 e15
192 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v e10 e11 e12 e13 e14 e15
193 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v e11 e12 e13 e14 e15
194 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v e12 e13 e14 e15
195 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v e13 e14 e15
196 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v e14 e15
197 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v e15
198 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v v ]
200 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p
201 | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15
202 | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v e09 e10 e11 e12 e13 e14 e15
203 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v e10 e11 e12 e13 e14 e15
204 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v e11 e12 e13 e14 e15
205 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v e12 e13 e14 e15
206 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v e13 e14 e15
207 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v e14 e15
208 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v e15
209 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v v ]
211 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
212 | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15
213 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v e10 e11 e12 e13 e14 e15
214 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v e11 e12 e13 e14 e15
215 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v e12 e13 e14 e15
216 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v e13 e14 e15
217 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v e14 e15
218 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v e15
219 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v v ]
221 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
223 | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15
224 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v e11 e12 e13 e14 e15
225 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v e12 e13 e14 e15
226 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v e13 e14 e15
227 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v e14 e15
228 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v e15
229 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v v ]
231 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
233 | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15
234 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v e12 e13 e14 e15
235 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v e13 e14 e15
236 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v e14 e15
237 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v e15
238 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v v ]
240 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
241 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p
242 | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15
243 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v e13 e14 e15
244 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v e14 e15
245 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v e15
246 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v v ]
248 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
249 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p
250 | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15
251 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v e14 e15
252 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v e15
253 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v v ]
255 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
256 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p
257 | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15
258 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v e15
259 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v v ]
261 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
262 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p
263 | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15
264 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v v ]
266 [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
267 | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p | xE ⇒ p
268 | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v ]
271 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
272 (* posso definire un setter composto [m+1,n-1] a matrice sull'array *)
273 (* NB: obbiettivo evitare l'overflow *)
274 definition setmn_array16T_succ_pred ≝
275 λm,n:exadecim.λT:Type.λp:Prod16T T.λv:T.
276 match lt_ex m xF with
277 [ true ⇒ match gt_ex n x0 with
278 [ true ⇒ setmn_array16T (succ_ex m) (pred_ex n) T p v
284 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
285 (* posso definire un setter composto [m+1,F] a matrice sull'array *)
286 (* NB: obbiettivo evitare l'overflow *)
287 definition setmn_array16T_succ ≝
288 λm:exadecim.λT:Type.λp:Prod16T T.λv:T.
289 match lt_ex m xF with
290 [ true ⇒ setmn_array16T (succ_ex m) xF T p v
294 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
295 (* posso definire un setter composto [0,n-1] a matrice sull'array *)
296 (* NB: obbiettivo evitare l'overflow *)
297 definition setmn_array16T_pred ≝
298 λn:exadecim.λT:Type.λp:Prod16T T.λv:T.
299 match gt_ex n x0 with
300 [ true ⇒ setmn_array16T x0 (pred_ex n) T p v
304 (* ************************** *)
305 (* TIPO BYTE COME INSIEME BIT *)
306 (* ************************** *)
308 (* definizione di un byte come 8 bit *)
309 inductive Prod8T (T:Type) : Type ≝
310 array_8T : T → T → T → T → T → T → T → T →
313 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
314 (* posso definire un getter a matrice sull'array *)
315 definition getn_array8T ≝
316 λn:oct.λT:Type.λp:Prod8T T.
318 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
320 [ o0 ⇒ e00 | o1 ⇒ e01 | o2 ⇒ e02 | o3 ⇒ e03 | o4 ⇒ e04 | o5 ⇒ e05 | o6 ⇒ e06 | o7 ⇒ e07 ]].
322 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
323 (* posso definire un setter a matrice sull'array *)
324 definition setn_array8T ≝
325 λn:oct.λT:Type.λp:Prod8T T.λv:T.
327 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
329 [ o0 ⇒ array_8T T e07 e06 e05 e04 e03 e02 e01 v
330 | o1 ⇒ array_8T T e07 e06 e05 e04 e03 e02 v e00
331 | o2 ⇒ array_8T T e07 e06 e05 e04 e03 v e01 e00
332 | o3 ⇒ array_8T T e07 e06 e05 e04 v e02 e01 e00
333 | o4 ⇒ array_8T T e07 e06 e05 v e03 e02 e01 e00
334 | o5 ⇒ array_8T T e07 e06 v e04 e03 e02 e01 e00
335 | o6 ⇒ array_8T T e07 v e05 e04 e03 e02 e01 e00
336 | o7 ⇒ array_8T T v e06 e05 e04 e03 e02 e01 e00
340 definition byte8_of_bits ≝
343 [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒
345 (or_ex (match e07 with [ true ⇒ x8 | false ⇒ x0 ])
346 (or_ex (match e06 with [ true ⇒ x4 | false ⇒ x0 ])
347 (or_ex (match e05 with [ true ⇒ x2 | false ⇒ x0 ])
348 (match e04 with [ true ⇒ x1 | false ⇒ x0 ]))))
349 (or_ex (match e03 with [ true ⇒ x8 | false ⇒ x0 ])
350 (or_ex (match e02 with [ true ⇒ x4 | false ⇒ x0 ])
351 (or_ex (match e01 with [ true ⇒ x2 | false ⇒ x0 ])
352 (match e00 with [ true ⇒ x1 | false ⇒ x0 ])))) ].
355 definition bits_of_byte8 ≝
358 [ x0 ⇒ match b8l p with
359 [ x0 ⇒ array_8T bool false false false false false false false false
360 | x1 ⇒ array_8T bool false false false false false false false true
361 | x2 ⇒ array_8T bool false false false false false false true false
362 | x3 ⇒ array_8T bool false false false false false false true true
363 | x4 ⇒ array_8T bool false false false false false true false false
364 | x5 ⇒ array_8T bool false false false false false true false true
365 | x6 ⇒ array_8T bool false false false false false true true false
366 | x7 ⇒ array_8T bool false false false false false true true true
367 | x8 ⇒ array_8T bool false false false false true false false false
368 | x9 ⇒ array_8T bool false false false false true false false true
369 | xA ⇒ array_8T bool false false false false true false true false
370 | xB ⇒ array_8T bool false false false false true false true true
371 | xC ⇒ array_8T bool false false false false true true false false
372 | xD ⇒ array_8T bool false false false false true true false true
373 | xE ⇒ array_8T bool false false false false true true true false
374 | xF ⇒ array_8T bool false false false false true true true true ]
375 | x1 ⇒ match b8l p with
376 [ x0 ⇒ array_8T bool false false false true false false false false
377 | x1 ⇒ array_8T bool false false false true false false false true
378 | x2 ⇒ array_8T bool false false false true false false true false
379 | x3 ⇒ array_8T bool false false false true false false true true
380 | x4 ⇒ array_8T bool false false false true false true false false
381 | x5 ⇒ array_8T bool false false false true false true false true
382 | x6 ⇒ array_8T bool false false false true false true true false
383 | x7 ⇒ array_8T bool false false false true false true true true
384 | x8 ⇒ array_8T bool false false false true true false false false
385 | x9 ⇒ array_8T bool false false false true true false false true
386 | xA ⇒ array_8T bool false false false true true false true false
387 | xB ⇒ array_8T bool false false false true true false true true
388 | xC ⇒ array_8T bool false false false true true true false false
389 | xD ⇒ array_8T bool false false false true true true false true
390 | xE ⇒ array_8T bool false false false true true true true false
391 | xF ⇒ array_8T bool false false false true true true true true ]
392 | x2 ⇒ match b8l p with
393 [ x0 ⇒ array_8T bool false false true false false false false false
394 | x1 ⇒ array_8T bool false false true false false false false true
395 | x2 ⇒ array_8T bool false false true false false false true false
396 | x3 ⇒ array_8T bool false false true false false false true true
397 | x4 ⇒ array_8T bool false false true false false true false false
398 | x5 ⇒ array_8T bool false false true false false true false true
399 | x6 ⇒ array_8T bool false false true false false true true false
400 | x7 ⇒ array_8T bool false false true false false true true true
401 | x8 ⇒ array_8T bool false false true false true false false false
402 | x9 ⇒ array_8T bool false false true false true false false true
403 | xA ⇒ array_8T bool false false true false true false true false
404 | xB ⇒ array_8T bool false false true false true false true true
405 | xC ⇒ array_8T bool false false true false true true false false
406 | xD ⇒ array_8T bool false false true false true true false true
407 | xE ⇒ array_8T bool false false true false true true true false
408 | xF ⇒ array_8T bool false false true false true true true true ]
409 | x3 ⇒ match b8l p with
410 [ x0 ⇒ array_8T bool false false true true false false false false
411 | x1 ⇒ array_8T bool false false true true false false false true
412 | x2 ⇒ array_8T bool false false true true false false true false
413 | x3 ⇒ array_8T bool false false true true false false true true
414 | x4 ⇒ array_8T bool false false true true false true false false
415 | x5 ⇒ array_8T bool false false true true false true false true
416 | x6 ⇒ array_8T bool false false true true false true true false
417 | x7 ⇒ array_8T bool false false true true false true true true
418 | x8 ⇒ array_8T bool false false true true true false false false
419 | x9 ⇒ array_8T bool false false true true true false false true
420 | xA ⇒ array_8T bool false false true true true false true false
421 | xB ⇒ array_8T bool false false true true true false true true
422 | xC ⇒ array_8T bool false false true true true true false false
423 | xD ⇒ array_8T bool false false true true true true false true
424 | xE ⇒ array_8T bool false false true true true true true false
425 | xF ⇒ array_8T bool false false true true true true true true ]
426 | x4 ⇒ match b8l p with
427 [ x0 ⇒ array_8T bool false true false false false false false false
428 | x1 ⇒ array_8T bool false true false false false false false true
429 | x2 ⇒ array_8T bool false true false false false false true false
430 | x3 ⇒ array_8T bool false true false false false false true true
431 | x4 ⇒ array_8T bool false true false false false true false false
432 | x5 ⇒ array_8T bool false true false false false true false true
433 | x6 ⇒ array_8T bool false true false false false true true false
434 | x7 ⇒ array_8T bool false true false false false true true true
435 | x8 ⇒ array_8T bool false true false false true false false false
436 | x9 ⇒ array_8T bool false true false false true false false true
437 | xA ⇒ array_8T bool false true false false true false true false
438 | xB ⇒ array_8T bool false true false false true false true true
439 | xC ⇒ array_8T bool false true false false true true false false
440 | xD ⇒ array_8T bool false true false false true true false true
441 | xE ⇒ array_8T bool false true false false true true true false
442 | xF ⇒ array_8T bool false true false false true true true true ]
443 | x5 ⇒ match b8l p with
444 [ x0 ⇒ array_8T bool false true false true false false false false
445 | x1 ⇒ array_8T bool false true false true false false false true
446 | x2 ⇒ array_8T bool false true false true false false true false
447 | x3 ⇒ array_8T bool false true false true false false true true
448 | x4 ⇒ array_8T bool false true false true false true false false
449 | x5 ⇒ array_8T bool false true false true false true false true
450 | x6 ⇒ array_8T bool false true false true false true true false
451 | x7 ⇒ array_8T bool false true false true false true true true
452 | x8 ⇒ array_8T bool false true false true true false false false
453 | x9 ⇒ array_8T bool false true false true true false false true
454 | xA ⇒ array_8T bool false true false true true false true false
455 | xB ⇒ array_8T bool false true false true true false true true
456 | xC ⇒ array_8T bool false true false true true true false false
457 | xD ⇒ array_8T bool false true false true true true false true
458 | xE ⇒ array_8T bool false true false true true true true false
459 | xF ⇒ array_8T bool false true false true true true true true ]
460 | x6 ⇒ match b8l p with
461 [ x0 ⇒ array_8T bool false true true false false false false false
462 | x1 ⇒ array_8T bool false true true false false false false true
463 | x2 ⇒ array_8T bool false true true false false false true false
464 | x3 ⇒ array_8T bool false true true false false false true true
465 | x4 ⇒ array_8T bool false true true false false true false false
466 | x5 ⇒ array_8T bool false true true false false true false true
467 | x6 ⇒ array_8T bool false true true false false true true false
468 | x7 ⇒ array_8T bool false true true false false true true true
469 | x8 ⇒ array_8T bool false true true false true false false false
470 | x9 ⇒ array_8T bool false true true false true false false true
471 | xA ⇒ array_8T bool false true true false true false true false
472 | xB ⇒ array_8T bool false true true false true false true true
473 | xC ⇒ array_8T bool false true true false true true false false
474 | xD ⇒ array_8T bool false true true false true true false true
475 | xE ⇒ array_8T bool false true true false true true true false
476 | xF ⇒ array_8T bool false true true false true true true true ]
477 | x7 ⇒ match b8l p with
478 [ x0 ⇒ array_8T bool false true true true false false false false
479 | x1 ⇒ array_8T bool false true true true false false false true
480 | x2 ⇒ array_8T bool false true true true false false true false
481 | x3 ⇒ array_8T bool false true true true false false true true
482 | x4 ⇒ array_8T bool false true true true false true false false
483 | x5 ⇒ array_8T bool false true true true false true false true
484 | x6 ⇒ array_8T bool false true true true false true true false
485 | x7 ⇒ array_8T bool false true true true false true true true
486 | x8 ⇒ array_8T bool false true true true true false false false
487 | x9 ⇒ array_8T bool false true true true true false false true
488 | xA ⇒ array_8T bool false true true true true false true false
489 | xB ⇒ array_8T bool false true true true true false true true
490 | xC ⇒ array_8T bool false true true true true true false false
491 | xD ⇒ array_8T bool false true true true true true false true
492 | xE ⇒ array_8T bool false true true true true true true false
493 | xF ⇒ array_8T bool false true true true true true true true ]
494 | x8 ⇒ match b8l p with
495 [ x0 ⇒ array_8T bool true false false false false false false false
496 | x1 ⇒ array_8T bool true false false false false false false true
497 | x2 ⇒ array_8T bool true false false false false false true false
498 | x3 ⇒ array_8T bool true false false false false false true true
499 | x4 ⇒ array_8T bool true false false false false true false false
500 | x5 ⇒ array_8T bool true false false false false true false true
501 | x6 ⇒ array_8T bool true false false false false true true false
502 | x7 ⇒ array_8T bool true false false false false true true true
503 | x8 ⇒ array_8T bool true false false false true false false false
504 | x9 ⇒ array_8T bool true false false false true false false true
505 | xA ⇒ array_8T bool true false false false true false true false
506 | xB ⇒ array_8T bool true false false false true false true true
507 | xC ⇒ array_8T bool true false false false true true false false
508 | xD ⇒ array_8T bool true false false false true true false true
509 | xE ⇒ array_8T bool true false false false true true true false
510 | xF ⇒ array_8T bool true false false false true true true true ]
511 | x9 ⇒ match b8l p with
512 [ x0 ⇒ array_8T bool true false false true false false false false
513 | x1 ⇒ array_8T bool true false false true false false false true
514 | x2 ⇒ array_8T bool true false false true false false true false
515 | x3 ⇒ array_8T bool true false false true false false true true
516 | x4 ⇒ array_8T bool true false false true false true false false
517 | x5 ⇒ array_8T bool true false false true false true false true
518 | x6 ⇒ array_8T bool true false false true false true true false
519 | x7 ⇒ array_8T bool true false false true false true true true
520 | x8 ⇒ array_8T bool true false false true true false false false
521 | x9 ⇒ array_8T bool true false false true true false false true
522 | xA ⇒ array_8T bool true false false true true false true false
523 | xB ⇒ array_8T bool true false false true true false true true
524 | xC ⇒ array_8T bool true false false true true true false false
525 | xD ⇒ array_8T bool true false false true true true false true
526 | xE ⇒ array_8T bool true false false true true true true false
527 | xF ⇒ array_8T bool true false false true true true true true ]
528 | xA ⇒ match b8l p with
529 [ x0 ⇒ array_8T bool true false true false false false false false
530 | x1 ⇒ array_8T bool true false true false false false false true
531 | x2 ⇒ array_8T bool true false true false false false true false
532 | x3 ⇒ array_8T bool true false true false false false true true
533 | x4 ⇒ array_8T bool true false true false false true false false
534 | x5 ⇒ array_8T bool true false true false false true false true
535 | x6 ⇒ array_8T bool true false true false false true true false
536 | x7 ⇒ array_8T bool true false true false false true true true
537 | x8 ⇒ array_8T bool true false true false true false false false
538 | x9 ⇒ array_8T bool true false true false true false false true
539 | xA ⇒ array_8T bool true false true false true false true false
540 | xB ⇒ array_8T bool true false true false true false true true
541 | xC ⇒ array_8T bool true false true false true true false false
542 | xD ⇒ array_8T bool true false true false true true false true
543 | xE ⇒ array_8T bool true false true false true true true false
544 | xF ⇒ array_8T bool true false true false true true true true ]
545 | xB ⇒ match b8l p with
546 [ x0 ⇒ array_8T bool true false true true false false false false
547 | x1 ⇒ array_8T bool true false true true false false false true
548 | x2 ⇒ array_8T bool true false true true false false true false
549 | x3 ⇒ array_8T bool true false true true false false true true
550 | x4 ⇒ array_8T bool true false true true false true false false
551 | x5 ⇒ array_8T bool true false true true false true false true
552 | x6 ⇒ array_8T bool true false true true false true true false
553 | x7 ⇒ array_8T bool true false true true false true true true
554 | x8 ⇒ array_8T bool true false true true true false false false
555 | x9 ⇒ array_8T bool true false true true true false false true
556 | xA ⇒ array_8T bool true false true true true false true false
557 | xB ⇒ array_8T bool true false true true true false true true
558 | xC ⇒ array_8T bool true false true true true true false false
559 | xD ⇒ array_8T bool true false true true true true false true
560 | xE ⇒ array_8T bool true false true true true true true false
561 | xF ⇒ array_8T bool true false true true true true true true ]
562 | xC ⇒ match b8l p with
563 [ x0 ⇒ array_8T bool true true false false false false false false
564 | x1 ⇒ array_8T bool true true false false false false false true
565 | x2 ⇒ array_8T bool true true false false false false true false
566 | x3 ⇒ array_8T bool true true false false false false true true
567 | x4 ⇒ array_8T bool true true false false false true false false
568 | x5 ⇒ array_8T bool true true false false false true false true
569 | x6 ⇒ array_8T bool true true false false false true true false
570 | x7 ⇒ array_8T bool true true false false false true true true
571 | x8 ⇒ array_8T bool true true false false true false false false
572 | x9 ⇒ array_8T bool true true false false true false false true
573 | xA ⇒ array_8T bool true true false false true false true false
574 | xB ⇒ array_8T bool true true false false true false true true
575 | xC ⇒ array_8T bool true true false false true true false false
576 | xD ⇒ array_8T bool true true false false true true false true
577 | xE ⇒ array_8T bool true true false false true true true false
578 | xF ⇒ array_8T bool true true false false true true true true ]
579 | xD ⇒ match b8l p with
580 [ x0 ⇒ array_8T bool true true false true false false false false
581 | x1 ⇒ array_8T bool true true false true false false false true
582 | x2 ⇒ array_8T bool true true false true false false true false
583 | x3 ⇒ array_8T bool true true false true false false true true
584 | x4 ⇒ array_8T bool true true false true false true false false
585 | x5 ⇒ array_8T bool true true false true false true false true
586 | x6 ⇒ array_8T bool true true false true false true true false
587 | x7 ⇒ array_8T bool true true false true false true true true
588 | x8 ⇒ array_8T bool true true false true true false false false
589 | x9 ⇒ array_8T bool true true false true true false false true
590 | xA ⇒ array_8T bool true true false true true false true false
591 | xB ⇒ array_8T bool true true false true true false true true
592 | xC ⇒ array_8T bool true true false true true true false false
593 | xD ⇒ array_8T bool true true false true true true false true
594 | xE ⇒ array_8T bool true true false true true true true false
595 | xF ⇒ array_8T bool true true false true true true true true ]
596 | xE ⇒ match b8l p with
597 [ x0 ⇒ array_8T bool true true true false false false false false
598 | x1 ⇒ array_8T bool true true true false false false false true
599 | x2 ⇒ array_8T bool true true true false false false true false
600 | x3 ⇒ array_8T bool true true true false false false true true
601 | x4 ⇒ array_8T bool true true true false false true false false
602 | x5 ⇒ array_8T bool true true true false false true false true
603 | x6 ⇒ array_8T bool true true true false false true true false
604 | x7 ⇒ array_8T bool true true true false false true true true
605 | x8 ⇒ array_8T bool true true true false true false false false
606 | x9 ⇒ array_8T bool true true true false true false false true
607 | xA ⇒ array_8T bool true true true false true false true false
608 | xB ⇒ array_8T bool true true true false true false true true
609 | xC ⇒ array_8T bool true true true false true true false false
610 | xD ⇒ array_8T bool true true true false true true false true
611 | xE ⇒ array_8T bool true true true false true true true false
612 | xF ⇒ array_8T bool true true true false true true true true ]
613 | xF ⇒ match b8l p with
614 [ x0 ⇒ array_8T bool true true true true false false false false
615 | x1 ⇒ array_8T bool true true true true false false false true
616 | x2 ⇒ array_8T bool true true true true false false true false
617 | x3 ⇒ array_8T bool true true true true false false true true
618 | x4 ⇒ array_8T bool true true true true false true false false
619 | x5 ⇒ array_8T bool true true true true false true false true
620 | x6 ⇒ array_8T bool true true true true false true true false
621 | x7 ⇒ array_8T bool true true true true false true true true
622 | x8 ⇒ array_8T bool true true true true true false false false
623 | x9 ⇒ array_8T bool true true true true true false false true
624 | xA ⇒ array_8T bool true true true true true false true false
625 | xB ⇒ array_8T bool true true true true true false true true
626 | xC ⇒ array_8T bool true true true true true true false false
627 | xD ⇒ array_8T bool true true true true true true false true
628 | xE ⇒ array_8T bool true true true true true true true false
629 | xF ⇒ array_8T bool true true true true true true true true ]
632 (* ********************** *)
633 (* TEOREMI/LEMMMI/ASSIOMI *)
634 (* ********************** *)
637 lemma ok_byte8_of_bits_bits_of_byte8 :
639 byte8_of_bits (bits_of_byte8 b) = b.
641 elim b; elim e; elim e1;
646 lemma ok_bits_of_byte8_byte8_of_bits :
647 ∀b7,b6,b5,b4,b3,b2,b1,b0.
648 bits_of_byte8 (byte8_of_bits (array_8T bool b7 b6 b5 b4 b3 b2 b1 b0))
649 = array_8T bool b7 b6 b5 b4 b3 b2 b1 b0.
651 elim b0; elim b1; elim b2; elim b3; elim b4; elim b5; elim b6; elim b7;