prodT merged with prod

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

diff --git a/helm/software/matita/library/freescale/byte8.ma b/helm/software/matita/library/freescale/byte8.ma
index fedc5a65a017b2ea54da0dcc61beaaf8bcfcc760..9c39bdb142054b5f40c12d72a9a9a5fb8de7c808 100644 (file)
--- a/helm/software/matita/library/freescale/byte8.ma
+++ b/helm/software/matita/library/freescale/byte8.ma
@@ -80,20 +80,20 @@ definition xor_b8 ≝
 (* 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' ]]].
 
@@ -106,20 +106,20 @@ let rec ror_b8_n (b:byte8) (n:nat) on n ≝
 (* 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' ]]].
 
@@ -137,16 +137,16 @@ definition not_b8 ≝
 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)).
@@ -279,7 +279,7 @@ definition daa_b8 ≝
    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]
@@ -290,7 +290,7 @@ definition daa_b8 ≝
     [ 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 *)
@@ -374,13 +374,13 @@ qed.
 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;