(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
| false ⇒ mk_byte8 bh' bl' ]]].
(* operatore rotazione destra n-volte *)
-nlet rec ror_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝
- match r with
- [ oc_O ⇒ b
- | oc_S t n' ⇒ ror_b8_n (ror_b8 b) t n' ].
+nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
+ match n with
+ [ O ⇒ b
+ | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
(* operatore rotazione sinistra con carry *)
ndefinition rcl_b8 ≝
| false ⇒ mk_byte8 bh' bl' ]]].
(* operatore rotazione sinistra n-volte *)
-nlet rec rol_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝
- match r with
- [ oc_O ⇒ b
- | oc_S t n' ⇒ rol_b8_n (rol_b8 b) t n' ].
+nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
+ match n with
+ [ O ⇒ b
+ | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
(* operatore not/complemento a 1 *)
ndefinition not_b8 ≝
| xF ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))
].
-ndefinition b8_to_recb8 ≝
-λn.b8_to_recb8_aux3 (b8h n) (b8l n) (b8_to_recb8_aux2 (b8h n) (ex_to_recex (b8h n))).
+ndefinition b8_to_recb8 : Πb.rec_byte8 b.
+ #b;
+ nletin K ≝ (b8_to_recb8_aux3 (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
+ nelim b in K:(%) ⊢ %;
+ #e1; #e2; nnormalize; #H; napply H.
+nqed.
(* ottali → esadecimali *)
ndefinition b8_of_bit ≝