(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
-set "baseuri" "cic:/matita/freescale/word16".
-
-(*include "/media/VIRTUOSO/freescale/byte8.ma".*)
include "freescale/byte8.ma".
(* ********************** *)
(* operatore rotazione destra con carry *)
definition rcr_w16 ≝
λw:word16.λc:bool.match rcr_b8 (w16h w) c with
- [ pairT wh' c' ⇒ match rcr_b8 (w16l w) c' with
- [ pairT wl' c'' ⇒ pairT ?? (mk_word16 wh' wl') c'' ]].
+ [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
+ [ pair wl' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]].
(* operatore shift destro *)
definition shr_w16 ≝
λw:word16.match rcr_b8 (w16h w) false with
- [ pairT wh' c' ⇒ match rcr_b8 (w16l w) c' with
- [ pairT wl' c'' ⇒ pairT ?? (mk_word16 wh' wl') c'' ]].
+ [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
+ [ pair wl' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]].
(* operatore rotazione destra *)
definition ror_w16 ≝
λw:word16.match rcr_b8 (w16h w) false with
- [ pairT wh' c' ⇒ match rcr_b8 (w16l w) c' with
- [ pairT wl' c'' ⇒ match c'' with
+ [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
+ [ pair wl' c'' ⇒ match c'' with
[ true ⇒ mk_word16 (or_b8 (mk_byte8 x8 x0) wh') wl'
| false ⇒ mk_word16 wh' wl' ]]].
(* operatore rotazione sinistra con carry *)
definition rcl_w16 ≝
λw:word16.λc:bool.match rcl_b8 (w16l w) c with
- [ pairT wl' c' ⇒ match rcl_b8 (w16h w) c' with
- [ pairT wh' c'' ⇒ pairT ?? (mk_word16 wh' wl') c'' ]].
+ [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
+ [ pair wh' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]].
(* operatore shift sinistro *)
definition shl_w16 ≝
λw:word16.match rcl_b8 (w16l w) false with
- [ pairT wl' c' ⇒ match rcl_b8 (w16h w) c' with
- [ pairT wh' c'' ⇒ pairT ?? (mk_word16 wh' wl') c'' ]].
+ [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
+ [ pair wh' c'' ⇒ pair ?? (mk_word16 wh' wl') c'' ]].
(* operatore rotazione sinistra *)
definition rol_w16 ≝
λw:word16.match rcl_b8 (w16l w) false with
- [ pairT wl' c' ⇒ match rcl_b8 (w16h w) c' with
- [ pairT wh' c'' ⇒ match c'' with
+ [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
+ [ pair wh' c'' ⇒ match c'' with
[ true ⇒ mk_word16 wh' (or_b8 (mk_byte8 x0 x1) wl')
| false ⇒ mk_word16 wh' wl' ]]].
definition plus_w16 ≝
λw1,w2:word16.λc:bool.
match plus_b8 (w16l w1) (w16l w2) c with
- [ pairT l c' ⇒ match plus_b8 (w16h w1) (w16h w2) c' with
- [ pairT h c'' ⇒ pairT ?? (mk_word16 h l) c'' ]].
+ [ pair l c' ⇒ match plus_b8 (w16h w1) (w16h w2) c' with
+ [ pair h c'' ⇒ pair ?? (mk_word16 h l) c'' ]].
(* operatore somma senza carry *)
definition plus_w16nc ≝
-λw1,w2:word16.fstT ?? (plus_w16 w1 w2 false).
+λw1,w2:word16.fst ?? (plus_w16 w1 w2 false).
(* operatore carry della somma *)
definition plus_w16c ≝
-λw1,w2:word16.sndT ?? (plus_w16 w1 w2 false).
+λw1,w2:word16.snd ?? (plus_w16 w1 w2 false).
(* operatore Most Significant Bit *)
definition MSB_w16 ≝ λw:word16.eq_ex x8 (and_ex x8 (b8h (w16h w))).
lemma plusw16_ok:
∀b1,b2,c.
match plus_w16 b1 b2 c with
- [ pairT r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_word16 r + nat_of_bool c' * (256 * 256)
+ [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_word16 r + nat_of_bool c' * (256 * 256)
].
intros; elim daemon.
qed.
(* TODO: dimostrare diversamente *)
axiom plusw16_O_x:
- ∀b. plus_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) b false = pairT ?? b false.
+ ∀b. plus_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) b false = pair ?? b false.
lemma plusw16nc_O_x:
∀x. plus_w16nc (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) x = x.