prodT merged with prod

[helm.git] / helm / software / matita / library / freescale / word16.ma

diff --git a/helm/software/matita/library/freescale/word16.ma b/helm/software/matita/library/freescale/word16.ma
index 9a260b10e8840087af12a1246614367aace639a6..b1448b98521ca421affc912fce4620aed224b1d1 100644 (file)
--- a/helm/software/matita/library/freescale/word16.ma
+++ b/helm/software/matita/library/freescale/word16.ma
@@ -80,20 +80,20 @@ definition xor_w16 ≝
 (* 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' ]]].
 
@@ -106,20 +106,20 @@ let rec ror_w16_n (w:word16) (n:nat) on n ≝
 (* 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' ]]].
 
@@ -137,16 +137,16 @@ definition not_w16 ≝
 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))).
@@ -252,14 +252,14 @@ axiom eq_nat_of_word16_n_nat_of_word16_mod_n_65536:
 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.