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/byte8".
29 (*include "/media/VIRTUOSO/freescale/exadecim.ma".*)
30 include "freescale/exadecim.ma".
32 (* ******************** *)
33 (* DEFINIZIONE DEI BYTE *)
34 (* ******************** *)
43 notation "〈x,y〉" non associative with precedence 80
44 for @{ 'mk_byte8 $x $y }.
45 interpretation "mk_byte8" 'mk_byte8 x y =
46 (cic:/matita/freescale/byte8/byte8.ind#xpointer(1/1/1) x y).
49 definition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
53 λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
55 | false ⇒ match gt_ex (b8h b1) (b8h b2) with
57 | false ⇒ lt_ex (b8l b1) (b8l b2) ]].
60 definition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2).
63 definition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).
66 definition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).
70 λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)).
74 λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)).
78 λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)).
80 (* operatore rotazione destra con carry *)
82 λb:byte8.λc:bool.match rcr_ex (b8h b) c with
83 [ pairT bh' c' ⇒ match rcr_ex (b8l b) c' with
84 [ pairT bl' c'' ⇒ pairT ?? (mk_byte8 bh' bl') c'' ]].
86 (* operatore shift destro *)
88 λb:byte8.match rcr_ex (b8h b) false with
89 [ pairT bh' c' ⇒ match rcr_ex (b8l b) c' with
90 [ pairT bl' c'' ⇒ pairT ?? (mk_byte8 bh' bl') c'' ]].
92 (* operatore rotazione destra *)
94 λb:byte8.match rcr_ex (b8h b) false with
95 [ pairT bh' c' ⇒ match rcr_ex (b8l b) c' with
96 [ pairT bl' c'' ⇒ match c'' with
97 [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
98 | false ⇒ mk_byte8 bh' bl' ]]].
100 (* operatore rotazione destra n-volte *)
101 let rec ror_b8_n (b:byte8) (n:nat) on n ≝
104 | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
106 (* operatore rotazione sinistra con carry *)
108 λb:byte8.λc:bool.match rcl_ex (b8l b) c with
109 [ pairT bl' c' ⇒ match rcl_ex (b8h b) c' with
110 [ pairT bh' c'' ⇒ pairT ?? (mk_byte8 bh' bl') c'' ]].
112 (* operatore shift sinistro *)
114 λb:byte8.match rcl_ex (b8l b) false with
115 [ pairT bl' c' ⇒ match rcl_ex (b8h b) c' with
116 [ pairT bh' c'' ⇒ pairT ?? (mk_byte8 bh' bl') c'' ]].
118 (* operatore rotazione sinistra *)
120 λb:byte8.match rcl_ex (b8l b) false with
121 [ pairT bl' c' ⇒ match rcl_ex (b8h b) c' with
122 [ pairT bh' c'' ⇒ match c'' with
123 [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
124 | false ⇒ mk_byte8 bh' bl' ]]].
126 (* operatore rotazione sinistra n-volte *)
127 let rec rol_b8_n (b:byte8) (n:nat) on n ≝
130 | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
132 (* operatore not/complemento a 1 *)
134 λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)).
136 (* operatore somma con carry *)
138 λb1,b2:byte8.λc:bool.
139 match plus_ex (b8l b1) (b8l b2) c with
140 [ pairT l c' ⇒ match plus_ex (b8h b1) (b8h b2) c' with
141 [ pairT h c'' ⇒ pairT ?? (mk_byte8 h l) c'' ]].
143 (* operatore somma senza carry *)
144 definition plus_b8nc ≝
145 λb1,b2:byte8.fstT ?? (plus_b8 b1 b2 false).
147 (* operatore carry della somma *)
148 definition plus_b8c ≝
149 λb1,b2:byte8.sndT ?? (plus_b8 b1 b2 false).
151 (* operatore Most Significant Bit *)
152 definition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
154 (* byte → naturali *)
155 definition nat_of_byte8 ≝ λb:byte8.16*(b8h b) + (b8l b).
157 coercion cic:/matita/freescale/byte8/nat_of_byte8.con.
159 (* naturali → byte *)
160 definition byte8_of_nat ≝ λn.mk_byte8 (exadecim_of_nat (n/16)) (exadecim_of_nat n).
162 (* operatore predecessore *)
164 λb:byte8.match eq_ex (b8l b) x0 with
165 [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b))
166 | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ].
168 (* operatore successore *)
170 λb:byte8.match eq_ex (b8l b) xF with
171 [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
172 | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ].
174 (* operatore neg/complemento a 2 *)
175 definition compl_b8 ≝
176 λb:byte8.match MSB_b8 b with
177 [ true ⇒ succ_b8 (not_b8 b)
178 | false ⇒ not_b8 (pred_b8 b) ].
180 (* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
182 λe1,e2:exadecim.match e1 with
184 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x0〉 | x2 ⇒ 〈x0,x0〉 | x3 ⇒ 〈x0,x0〉
185 | x4 ⇒ 〈x0,x0〉 | x5 ⇒ 〈x0,x0〉 | x6 ⇒ 〈x0,x0〉 | x7 ⇒ 〈x0,x0〉
186 | x8 ⇒ 〈x0,x0〉 | x9 ⇒ 〈x0,x0〉 | xA ⇒ 〈x0,x0〉 | xB ⇒ 〈x0,x0〉
187 | xC ⇒ 〈x0,x0〉 | xD ⇒ 〈x0,x0〉 | xE ⇒ 〈x0,x0〉 | xF ⇒ 〈x0,x0〉 ]
189 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x1〉 | x2 ⇒ 〈x0,x2〉 | x3 ⇒ 〈x0,x3〉
190 | x4 ⇒ 〈x0,x4〉 | x5 ⇒ 〈x0,x5〉 | x6 ⇒ 〈x0,x6〉 | x7 ⇒ 〈x0,x7〉
191 | x8 ⇒ 〈x0,x8〉 | x9 ⇒ 〈x0,x9〉 | xA ⇒ 〈x0,xA〉 | xB ⇒ 〈x0,xB〉
192 | xC ⇒ 〈x0,xC〉 | xD ⇒ 〈x0,xD〉 | xE ⇒ 〈x0,xE〉 | xF ⇒ 〈x0,xF〉 ]
194 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x2〉 | x2 ⇒ 〈x0,x4〉 | x3 ⇒ 〈x0,x6〉
195 | x4 ⇒ 〈x0,x8〉 | x5 ⇒ 〈x0,xA〉 | x6 ⇒ 〈x0,xC〉 | x7 ⇒ 〈x0,xE〉
196 | x8 ⇒ 〈x1,x0〉 | x9 ⇒ 〈x1,x2〉 | xA ⇒ 〈x1,x4〉 | xB ⇒ 〈x1,x6〉
197 | xC ⇒ 〈x1,x8〉 | xD ⇒ 〈x1,xA〉 | xE ⇒ 〈x1,xC〉 | xF ⇒ 〈x1,xE〉 ]
199 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x3〉 | x2 ⇒ 〈x0,x6〉 | x3 ⇒ 〈x0,x9〉
200 | x4 ⇒ 〈x0,xC〉 | x5 ⇒ 〈x0,xF〉 | x6 ⇒ 〈x1,x2〉 | x7 ⇒ 〈x1,x5〉
201 | x8 ⇒ 〈x1,x8〉 | x9 ⇒ 〈x1,xB〉 | xA ⇒ 〈x1,xE〉 | xB ⇒ 〈x2,x1〉
202 | xC ⇒ 〈x2,x4〉 | xD ⇒ 〈x2,x7〉 | xE ⇒ 〈x2,xA〉 | xF ⇒ 〈x2,xD〉 ]
204 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x4〉 | x2 ⇒ 〈x0,x8〉 | x3 ⇒ 〈x0,xC〉
205 | x4 ⇒ 〈x1,x0〉 | x5 ⇒ 〈x1,x4〉 | x6 ⇒ 〈x1,x8〉 | x7 ⇒ 〈x1,xC〉
206 | x8 ⇒ 〈x2,x0〉 | x9 ⇒ 〈x2,x4〉 | xA ⇒ 〈x2,x8〉 | xB ⇒ 〈x2,xC〉
207 | xC ⇒ 〈x3,x0〉 | xD ⇒ 〈x3,x4〉 | xE ⇒ 〈x3,x8〉 | xF ⇒ 〈x3,xC〉 ]
209 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x5〉 | x2 ⇒ 〈x0,xA〉 | x3 ⇒ 〈x0,xF〉
210 | x4 ⇒ 〈x1,x4〉 | x5 ⇒ 〈x1,x9〉 | x6 ⇒ 〈x1,xE〉 | x7 ⇒ 〈x2,x3〉
211 | x8 ⇒ 〈x2,x8〉 | x9 ⇒ 〈x2,xD〉 | xA ⇒ 〈x3,x2〉 | xB ⇒ 〈x3,x7〉
212 | xC ⇒ 〈x3,xC〉 | xD ⇒ 〈x4,x1〉 | xE ⇒ 〈x4,x6〉 | xF ⇒ 〈x4,xB〉 ]
214 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x6〉 | x2 ⇒ 〈x0,xC〉 | x3 ⇒ 〈x1,x2〉
215 | x4 ⇒ 〈x1,x8〉 | x5 ⇒ 〈x1,xE〉 | x6 ⇒ 〈x2,x4〉 | x7 ⇒ 〈x2,xA〉
216 | x8 ⇒ 〈x3,x0〉 | x9 ⇒ 〈x3,x6〉 | xA ⇒ 〈x3,xC〉 | xB ⇒ 〈x4,x2〉
217 | xC ⇒ 〈x4,x8〉 | xD ⇒ 〈x4,xE〉 | xE ⇒ 〈x5,x4〉 | xF ⇒ 〈x5,xA〉 ]
219 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x7〉 | x2 ⇒ 〈x0,xE〉 | x3 ⇒ 〈x1,x5〉
220 | x4 ⇒ 〈x1,xC〉 | x5 ⇒ 〈x2,x3〉 | x6 ⇒ 〈x2,xA〉 | x7 ⇒ 〈x3,x1〉
221 | x8 ⇒ 〈x3,x8〉 | x9 ⇒ 〈x3,xF〉 | xA ⇒ 〈x4,x6〉 | xB ⇒ 〈x4,xD〉
222 | xC ⇒ 〈x5,x4〉 | xD ⇒ 〈x5,xB〉 | xE ⇒ 〈x6,x2〉 | xF ⇒ 〈x6,x9〉 ]
224 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x8〉 | x2 ⇒ 〈x1,x0〉 | x3 ⇒ 〈x1,x8〉
225 | x4 ⇒ 〈x2,x0〉 | x5 ⇒ 〈x2,x8〉 | x6 ⇒ 〈x3,x0〉 | x7 ⇒ 〈x3,x8〉
226 | x8 ⇒ 〈x4,x0〉 | x9 ⇒ 〈x4,x8〉 | xA ⇒ 〈x5,x0〉 | xB ⇒ 〈x5,x8〉
227 | xC ⇒ 〈x6,x0〉 | xD ⇒ 〈x6,x8〉 | xE ⇒ 〈x7,x0〉 | xF ⇒ 〈x7,x8〉 ]
229 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x9〉 | x2 ⇒ 〈x1,x2〉 | x3 ⇒ 〈x1,xB〉
230 | x4 ⇒ 〈x2,x4〉 | x5 ⇒ 〈x2,xD〉 | x6 ⇒ 〈x3,x6〉 | x7 ⇒ 〈x3,xF〉
231 | x8 ⇒ 〈x4,x8〉 | x9 ⇒ 〈x5,x1〉 | xA ⇒ 〈x5,xA〉 | xB ⇒ 〈x6,x3〉
232 | xC ⇒ 〈x6,xC〉 | xD ⇒ 〈x7,x5〉 | xE ⇒ 〈x7,xE〉 | xF ⇒ 〈x8,x7〉 ]
234 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xA〉 | x2 ⇒ 〈x1,x4〉 | x3 ⇒ 〈x1,xE〉
235 | x4 ⇒ 〈x2,x8〉 | x5 ⇒ 〈x3,x2〉 | x6 ⇒ 〈x3,xC〉 | x7 ⇒ 〈x4,x6〉
236 | x8 ⇒ 〈x5,x0〉 | x9 ⇒ 〈x5,xA〉 | xA ⇒ 〈x6,x4〉 | xB ⇒ 〈x6,xE〉
237 | xC ⇒ 〈x7,x8〉 | xD ⇒ 〈x8,x2〉 | xE ⇒ 〈x8,xC〉 | xF ⇒ 〈x9,x6〉 ]
239 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xB〉 | x2 ⇒ 〈x1,x6〉 | x3 ⇒ 〈x2,x1〉
240 | x4 ⇒ 〈x2,xC〉 | x5 ⇒ 〈x3,x7〉 | x6 ⇒ 〈x4,x2〉 | x7 ⇒ 〈x4,xD〉
241 | x8 ⇒ 〈x5,x8〉 | x9 ⇒ 〈x6,x3〉 | xA ⇒ 〈x6,xE〉 | xB ⇒ 〈x7,x9〉
242 | xC ⇒ 〈x8,x4〉 | xD ⇒ 〈x8,xF〉 | xE ⇒ 〈x9,xA〉 | xF ⇒ 〈xA,x5〉 ]
244 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xC〉 | x2 ⇒ 〈x1,x8〉 | x3 ⇒ 〈x2,x4〉
245 | x4 ⇒ 〈x3,x0〉 | x5 ⇒ 〈x3,xC〉 | x6 ⇒ 〈x4,x8〉 | x7 ⇒ 〈x5,x4〉
246 | x8 ⇒ 〈x6,x0〉 | x9 ⇒ 〈x6,xC〉 | xA ⇒ 〈x7,x8〉 | xB ⇒ 〈x8,x4〉
247 | xC ⇒ 〈x9,x0〉 | xD ⇒ 〈x9,xC〉 | xE ⇒ 〈xA,x8〉 | xF ⇒ 〈xB,x4〉 ]
249 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xD〉 | x2 ⇒ 〈x1,xA〉 | x3 ⇒ 〈x2,x7〉
250 | x4 ⇒ 〈x3,x4〉 | x5 ⇒ 〈x4,x1〉 | x6 ⇒ 〈x4,xE〉 | x7 ⇒ 〈x5,xB〉
251 | x8 ⇒ 〈x6,x8〉 | x9 ⇒ 〈x7,x5〉 | xA ⇒ 〈x8,x2〉 | xB ⇒ 〈x8,xF〉
252 | xC ⇒ 〈x9,xC〉 | xD ⇒ 〈xA,x9〉 | xE ⇒ 〈xB,x6〉 | xF ⇒ 〈xC,x3〉 ]
254 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xE〉 | x2 ⇒ 〈x1,xC〉 | x3 ⇒ 〈x2,xA〉
255 | x4 ⇒ 〈x3,x8〉 | x5 ⇒ 〈x4,x6〉 | x6 ⇒ 〈x5,x4〉 | x7 ⇒ 〈x6,x2〉
256 | x8 ⇒ 〈x7,x0〉 | x9 ⇒ 〈x7,xE〉 | xA ⇒ 〈x8,xC〉 | xB ⇒ 〈x9,xA〉
257 | xC ⇒ 〈xA,x8〉 | xD ⇒ 〈xB,x6〉 | xE ⇒ 〈xC,x4〉 | xF ⇒ 〈xD,x2〉 ]
259 [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xF〉 | x2 ⇒ 〈x1,xE〉 | x3 ⇒ 〈x2,xD〉
260 | x4 ⇒ 〈x3,xC〉 | x5 ⇒ 〈x4,xB〉 | x6 ⇒ 〈x5,xA〉 | x7 ⇒ 〈x6,x9〉
261 | x8 ⇒ 〈x7,x8〉 | x9 ⇒ 〈x8,x7〉 | xA ⇒ 〈x9,x6〉 | xB ⇒ 〈xA,x5〉
262 | xC ⇒ 〈xB,x4〉 | xD ⇒ 〈xC,x3〉 | xE ⇒ 〈xD,x2〉 | xF ⇒ 〈xE,x1〉 ]
265 (* correzione per somma su BCD *)
266 (* input: halfcarry,carry,X(BCD+BCD) *)
267 (* output: X',carry' *)
270 match lt_b8 X 〈x9,xA〉 with
273 (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
274 [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
276 let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
278 | false ⇒ plus_b8nc X 〈x0,x6〉 ] in
279 let X'' ≝ match c with
280 [ true ⇒ plus_b8nc X' 〈x6,x0〉
285 (* X' = [X:0x9A-0xFF]
286 [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
287 [(b16l X):0xA-0xF] X + 0x6 + 0x60 *)
289 let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
291 | false ⇒ plus_b8nc X 〈x0,x6〉 ] in
292 let X'' ≝ plus_b8nc X' 〈x6,x0〉 in
296 (* iteratore sui byte *)
297 definition forall_byte8 ≝
299 forall_exadecim (λbh.
300 forall_exadecim (λbl.
301 P (mk_byte8 bh bl))).
303 (* ********************** *)
304 (* TEOREMI/LEMMMI/ASSIOMI *)
305 (* ********************** *)
307 lemma byte8_of_nat_nat_of_byte8: ∀b. byte8_of_nat (nat_of_byte8 b) = b.
315 lemma lt_nat_of_byte8_256: ∀b. nat_of_byte8 b < 256.
318 letin H ≝ (lt_nat_of_exadecim_16 (b8h b)); clearbody H;
319 letin K ≝ (lt_nat_of_exadecim_16 (b8l b)); clearbody K;
320 unfold lt in H K ⊢ %;
321 letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
322 letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
324 cut (16*b8h b ≤ 16*15);
325 [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
326 simplify in Hf:(? ? %);
328 | apply le_times_r. apply H'.
332 lemma nat_of_byte8_byte8_of_nat: ∀n. nat_of_byte8 (byte8_of_nat n) = n \mod 256.
334 letin H ≝ (lt_nat_of_byte8_256 (byte8_of_nat n)); clearbody H;
335 rewrite < (lt_to_eq_mod ? ? H); clear H;
338 change with ((16*(exadecim_of_nat (n/16)) + exadecim_of_nat n) \mod 256 = n \mod 256);
339 letin H ≝ (div_mod n 16 ?); clearbody H; [ autobatch | ];
340 rewrite > symmetric_times in H;
341 rewrite > nat_of_exadecim_exadecim_of_nat in ⊢ (? ? (? (? % ?) ?) ?);
342 rewrite > nat_of_exadecim_exadecim_of_nat in ⊢ (? ? (? (? ? %) ?) ?);
343 rewrite > H in ⊢ (? ? ? (? % ?)); clear H;
344 rewrite > mod_plus in ⊢ (? ? % ?);
345 rewrite > mod_plus in ⊢ (? ? ? %);
346 apply eq_mod_to_eq_plus_mod;
347 rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch];
348 rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch];
349 rewrite < (eq_mod_times_times_mod ? ? 16 256) in ⊢ (? ? (? % ?) ?); [2: reflexivity | ];
350 rewrite < mod_mod in ⊢ (? ? % ?);
356 lemma eq_nat_of_byte8_n_nat_of_byte8_mod_n_256:
357 ∀n. byte8_of_nat n = byte8_of_nat (n \mod 256).
361 [ rewrite > exadecim_of_nat_mod in ⊢ (? ? % ?);
362 rewrite > exadecim_of_nat_mod in ⊢ (? ? ? %);
365 | rewrite > exadecim_of_nat_mod;
366 rewrite > exadecim_of_nat_mod in ⊢ (? ? ? %);
367 rewrite > divides_to_eq_mod_mod_mod;
369 | apply (witness ? ? 16). reflexivity.
376 match plus_b8 b1 b2 c with
377 [ pairT r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte8 r + nat_of_bool c' * 256
383 ∀b. plus_b8 (mk_byte8 x0 x0) b false = pairT ?? b false.
392 ∀x. plus_b8nc (mk_byte8 x0 x0) x = x.
395 rewrite > plusb8_O_x;
399 lemma eq_nat_of_byte8_mod: ∀b. nat_of_byte8 b = nat_of_byte8 b \mod 256.
401 lapply (lt_nat_of_byte8_256 b);
402 rewrite > (lt_to_eq_mod ? ? Hletin) in ⊢ (? ? ? %);
407 ∀b1,b2:byte8.nat_of_byte8 (plus_b8nc b1 b2) = (b1 + b2) \mod 256.
410 generalize in match (plusb8_ok b1 b2 false);
411 elim (plus_b8 b1 b2 false);
413 change with (nat_of_byte8 t = (b1 + b2) \mod 256);
414 rewrite < plus_n_O in H;
415 rewrite > H; clear H;
417 letin K ≝ (eq_nat_of_byte8_mod t); clearbody K;
418 letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
420 autobatch paramodulation.
423 lemma eq_eqb8_x0_x0_byte8_of_nat_S_false:
424 ∀b. b < 255 → eq_b8 (mk_byte8 x0 x0) (byte8_of_nat (S b)) = false.
427 cut (b < 15 ∨ b ≥ 15);
430 change in ⊢ (? ? (? ? %) ?) with (eq_ex x0 (exadecim_of_nat (S b)));
431 rewrite > eq_eqex_S_x0_false;
432 [ elim (eq_ex (b8h (mk_byte8 x0 x0))
433 (b8h (mk_byte8 (exadecim_of_nat (S b/16)) (exadecim_of_nat (S b)))));
439 change in ⊢ (? ? (? % ?) ?) with (eq_ex x0 (exadecim_of_nat (S b/16)));
440 letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
448 rewrite > eq_eqex_S_x0_false;
453 clear H2; clear a; clear H1; clear Hcut;
454 apply (le_times_to_le 16) [ autobatch | ] ;
455 rewrite > (div_mod (S b) 16) in H;[2:autobatch|]
456 rewrite > (div_mod 255 16) in H:(? ? %);[2:autobatch|]
457 lapply (le_to_le_plus_to_le ? ? ? ? ? H);
459 apply lt_mod_m_m;autobatch
460 |rewrite > sym_times;
461 rewrite > sym_times in ⊢ (? ? %);
462 normalize in ⊢ (? ? %);apply Hletin;
467 | elim (or_lt_le b 15);unfold ge;autobatch
471 axiom eq_mod_O_to_exists: ∀n,m. n \mod m = 0 → ∃z. n = z*m.
473 lemma eq_b8pred_S_a_a:
474 ∀a. a < 255 → pred_b8 (byte8_of_nat (S a)) = byte8_of_nat a.
477 apply (bool_elim ? (eq_ex (b8l (byte8_of_nat (S a))) x0)); intros;
478 [ change with (mk_byte8 (pred_ex (b8h (byte8_of_nat (S a)))) (pred_ex (b8l (byte8_of_nat (S a))))
480 rewrite > (eqex_true_to_eq ? ? H1);
481 normalize in ⊢ (? ? (? ? %) ?);
483 change with (mk_byte8 (pred_ex (exadecim_of_nat (S a/16))) xF =
484 mk_byte8 (exadecim_of_nat (a/16)) (exadecim_of_nat a));
485 lapply (eqex_true_to_eq ? ? H1); clear H1;
486 unfold byte8_of_nat in Hletin;
487 change in Hletin with (exadecim_of_nat (S a) = x0);
488 lapply (eq_f ? ? nat_of_exadecim ? ? Hletin); clear Hletin;
489 normalize in Hletin1:(? ? ? %);
490 rewrite > nat_of_exadecim_exadecim_of_nat in Hletin1;
491 elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
493 rewrite > lt_O_to_div_times; [2: autobatch | ]
494 lapply (eq_f ? ? (λx.x/16) ? ? H1);
495 rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ]
496 lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
497 rewrite > eq_mod_times_n_m_m_O in Hletin1;
499 | change with (mk_byte8 (b8h (byte8_of_nat (S a))) (pred_ex (b8l (byte8_of_nat (S a))))
502 change with (mk_byte8 (exadecim_of_nat (S a/16)) (pred_ex (exadecim_of_nat (S a)))
503 = mk_byte8 (exadecim_of_nat (a/16)) (exadecim_of_nat a));
504 lapply (eqex_false_to_not_eq ? ? H1);
505 unfold byte8_of_nat in Hletin;
506 change in Hletin with (exadecim_of_nat (S a) ≠ x0);
507 cut (nat_of_exadecim (exadecim_of_nat (S a)) ≠ 0);
510 lapply (eq_f ? ? exadecim_of_nat ? ? H2);
511 rewrite > exadecim_of_nat_nat_of_exadecim in Hletin1;
519 ∀x:byte8.∀n.plus_b8nc (byte8_of_nat (x*n)) x = byte8_of_nat (x * S n).
521 rewrite < byte8_of_nat_nat_of_byte8;
522 rewrite > (plusb8nc_ok (byte8_of_nat (x*n)) x);
523 rewrite < times_n_Sm;
524 rewrite > nat_of_byte8_byte8_of_nat in ⊢ (? ? (? (? (? % ?) ?)) ?);
525 rewrite > eq_nat_of_byte8_n_nat_of_byte8_mod_n_256 in ⊢ (? ? ? %);
526 rewrite > mod_plus in ⊢ (? ? (? %) ?);
527 rewrite > mod_plus in ⊢ (? ? ? (? %));
528 rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: autobatch | ];
529 rewrite > sym_plus in ⊢ (? ? (? (? % ?)) ?);
533 lemma eq_plusb8c_x0_x0_x_false:
534 ∀x.plus_b8c (mk_byte8 x0 x0) x = false.
542 axiom eqb8_true_to_eq: ∀b,b'. eq_b8 b b' = true → b=b'.
544 axiom eqb8_false_to_not_eq: ∀b,b'. eq_b8 b b' = false → b ≠ b'.
546 axiom byte8_of_nat_mod: ∀n.byte8_of_nat n = byte8_of_nat (n \mod 256).
551 ∀e1,e2.nat_of_byte8 (mul_ex e1 e2) = (nat_of_exadecim e1) * (nat_of_exadecim e2).