(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
-set "baseuri" "cic:/matita/freescale/byte8".
-
-(*include "/media/VIRTUOSO/freescale/exadecim.ma".*)
include "freescale/exadecim.ma".
(* ******************** *)
(* operatore rotazione destra con carry *)
definition rcr_b8 ≝
λb:byte8.λc:bool.match rcr_ex (b8h b) c with
- [ pairT bh' c' ⇒ match rcr_ex (b8l b) c' with
- [ pairT bl' c'' ⇒ pairT ?? (mk_byte8 bh' bl') c'' ]].
+ [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
+ [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
(* operatore shift destro *)
definition shr_b8 ≝
λb:byte8.match rcr_ex (b8h b) false with
- [ pairT bh' c' ⇒ match rcr_ex (b8l b) c' with
- [ pairT bl' c'' ⇒ pairT ?? (mk_byte8 bh' bl') c'' ]].
+ [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
+ [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
(* operatore rotazione destra *)
definition ror_b8 ≝
λb:byte8.match rcr_ex (b8h b) false with
- [ pairT bh' c' ⇒ match rcr_ex (b8l b) c' with
- [ pairT bl' c'' ⇒ match c'' with
+ [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
+ [ pair bl' c'' ⇒ match c'' with
[ true ⇒ mk_byte8 (or_ex x8 bh') bl'
| false ⇒ mk_byte8 bh' bl' ]]].
(* operatore rotazione sinistra con carry *)
definition rcl_b8 ≝
λb:byte8.λc:bool.match rcl_ex (b8l b) c with
- [ pairT bl' c' ⇒ match rcl_ex (b8h b) c' with
- [ pairT bh' c'' ⇒ pairT ?? (mk_byte8 bh' bl') c'' ]].
+ [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
+ [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
(* operatore shift sinistro *)
definition shl_b8 ≝
λb:byte8.match rcl_ex (b8l b) false with
- [ pairT bl' c' ⇒ match rcl_ex (b8h b) c' with
- [ pairT bh' c'' ⇒ pairT ?? (mk_byte8 bh' bl') c'' ]].
+ [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
+ [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
(* operatore rotazione sinistra *)
definition rol_b8 ≝
λb:byte8.match rcl_ex (b8l b) false with
- [ pairT bl' c' ⇒ match rcl_ex (b8h b) c' with
- [ pairT bh' c'' ⇒ match c'' with
+ [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
+ [ pair bh' c'' ⇒ match c'' with
[ true ⇒ mk_byte8 bh' (or_ex x1 bl')
| false ⇒ mk_byte8 bh' bl' ]]].
definition plus_b8 ≝
λb1,b2:byte8.λc:bool.
match plus_ex (b8l b1) (b8l b2) c with
- [ pairT l c' ⇒ match plus_ex (b8h b1) (b8h b2) c' with
- [ pairT h c'' ⇒ pairT ?? (mk_byte8 h l) c'' ]].
+ [ pair l c' ⇒ match plus_ex (b8h b1) (b8h b2) c' with
+ [ pair h c'' ⇒ pair ?? (mk_byte8 h l) c'' ]].
(* operatore somma senza carry *)
definition plus_b8nc ≝
-λb1,b2:byte8.fstT ?? (plus_b8 b1 b2 false).
+λb1,b2:byte8.fst ?? (plus_b8 b1 b2 false).
(* operatore carry della somma *)
definition plus_b8c ≝
-λb1,b2:byte8.sndT ?? (plus_b8 b1 b2 false).
+λb1,b2:byte8.snd ?? (plus_b8 b1 b2 false).
(* operatore Most Significant Bit *)
definition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
let X'' ≝ match c with
[ true ⇒ plus_b8nc X' 〈x6,x0〉
| false ⇒ X' ] in
- pairT ?? X'' c
+ pair ?? X'' c
(* [X:0x9A-0xFF] *)
(* c' = 1 *)
(* X' = [X:0x9A-0xFF]
[ true ⇒ X
| false ⇒ plus_b8nc X 〈x0,x6〉 ] in
let X'' ≝ plus_b8nc X' 〈x6,x0〉 in
- pairT ?? X'' true
+ pair ?? X'' true
].
(* iteratore sui byte *)
lemma plusb8_ok:
∀b1,b2,c.
match plus_b8 b1 b2 c with
- [ pairT r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte8 r + nat_of_bool c' * 256
+ [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte8 r + nat_of_bool c' * 256
].
intros; elim daemon.
qed.
lemma plusb8_O_x:
- ∀b. plus_b8 (mk_byte8 x0 x0) b false = pairT ?? b false.
+ ∀b. plus_b8 (mk_byte8 x0 x0) b false = pair ?? b false.
intros;
elim b;
elim e;