X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fbyte8.ma;h=fd412e59e70d5e5347de8f1c9e7e5b35fc718e74;hb=9e291b4d0a99118cd0a1c5540ef00c25ca37a56d;hp=fedc5a65a017b2ea54da0dcc61beaaf8bcfcc760;hpb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;p=helm.git

diff --git a/helm/software/matita/library/freescale/byte8.ma b/helm/software/matita/library/freescale/byte8.ma
index fedc5a65a..fd412e59e 100644
--- a/helm/software/matita/library/freescale/byte8.ma
+++ b/helm/software/matita/library/freescale/byte8.ma
@@ -24,9 +24,6 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-set "baseuri" "cic:/matita/freescale/byte8".
-
-(*include "/media/VIRTUOSO/freescale/exadecim.ma".*)
 include "freescale/exadecim.ma".
 
 (* ******************** *)
@@ -80,20 +77,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 +103,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 +134,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 +276,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 +287,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 +371,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;