X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword16.ma;h=e0c59bab3869df2166db9a80123aaf63353ebf57;hb=38fccc2b774e493a94eedef76342b56079c0e694;hp=b078169d7d9c730155cbbc78c48cf711b362630d;hpb=b1c174cffd3c1d10383a52d63a6e662156fb0bb7;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
index b078169d7..e0c59bab3 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -90,10 +90,10 @@ ndefinition ror_w16 ≝
    | false ⇒ mk_word16 wh' wl' ]]].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_w16_n (w:word16) (n:exadecim) (r:rec_exadecim n) on r ≝
- match r with
-  [ ex_O ⇒ w
-  | ex_S t n' ⇒ ror_w16_n (ror_w16 w) t n' ].
+nlet rec ror_w16_n (w:word16) (n:nat) on n ≝
+ match n with
+  [ O ⇒ w
+  | S n' ⇒ ror_w16_n (ror_w16 w) n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_w16 ≝
@@ -116,10 +116,10 @@ ndefinition rol_w16 ≝
    | false ⇒ mk_word16 wh' wl' ]]].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_w16_n (w:word16) (n:exadecim) (r:rec_exadecim n) on r ≝
- match r with
-  [ ex_O ⇒ w
-  | ex_S t n' ⇒ rol_w16_n (rol_w16 w) t n' ].
+nlet rec rol_w16_n (w:word16) (n:nat) on n ≝
+ match n with
+  [ O ⇒ w
+  | S n' ⇒ rol_w16_n (rol_w16 w) n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_w16 ≝
@@ -200,15 +200,15 @@ ndefinition mul_b8 ≝
 ]]]]]].
 
 (* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
-nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:oct) (rc:rec_oct c) on rc ≝
+nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:nat) on c ≝
  let w' ≝ plus_w16_d_d divd (compl_w16 divs) in
-  match rc with
-  [ oc_O ⇒ match le_w16 divs divd with
+  match c with
+  [ O ⇒ match le_w16 divs divd with
    [ true ⇒ triple … (or_b8 molt q) (w16l w') (⊖ (eq_b8 (w16h w') 〈x0,x0〉))
    | false ⇒ triple … q (w16l divd) (⊖ (eq_b8 (w16h divd) 〈x0,x0〉)) ]
-  | oc_S t c' ⇒ match le_w16 divs divd with
-   [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) t c'
-   | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q t c' ]].
+  | S c' ⇒ match le_w16 divs divd with
+   [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) c'
+   | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q c' ]].
 
 ndefinition div_b8 ≝
 λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with
@@ -224,7 +224,7 @@ ndefinition div_b8 ≝
 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
 (*    puo' essere sottratto al dividendo *) 
-  | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 ? (ex_to_recex x7)) 〈x8,x0〉 〈x0,x0〉 ? (oct_to_recoct o7) ]].
+  | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 7) 〈x8,x0〉 〈x0,x0〉 7 ]].
 
 (* operatore x in [inf,sup] *)
 ndefinition inrange_w16 ≝
@@ -482,14 +482,12 @@ ndefinition w16_to_recw16_aux4 ≝
  | xF ⇒ w16_to_recw16_aux4_15 … recw
  ].
 
-nlemma w16_to_recw16_aux5 : ∀b.rec_byte8 (〈b8h b,b8l b〉) → rec_byte8 b.
- #b; nelim b; #e1; #e2; nnormalize; #input; napply input. nqed.
-
-ndefinition w16_to_recw16 ≝
-λn.w16_to_recw16_aux4 (w16h n) (b8h (w16l n)) (b8l (w16l n))
-    (w16_to_recw16_aux3 (w16h n) (b8h (w16l n)) (w16_to_recw16_aux2 (w16h n) ?)).
- nelim n; #b1; #b2;
- nchange with (rec_byte8 b1);
- napply (w16_to_recw16_aux5 b1);
- napply (b8_to_recb8 b1).
+ndefinition w16_to_recw16 : Πw.rec_word16 w.
+ #w;
+ nletin K ≝ (w16_to_recw16_aux4 (w16h w) (b8h (w16l w)) (b8l (w16l w))
+              (w16_to_recw16_aux3 (w16h w) (b8h (w16l w)) (w16_to_recw16_aux2 (w16h w) (b8_to_recb8 (w16h w)))));
+ nelim w in K:(%) ⊢ %;
+ #b1; #b2;
+ nelim b2;
+ #e1; #e2; nnormalize; #H; napply H.
 nqed.