freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly / num / word16.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
index 1abaf059971ea2ca5c3486a62a5d26d8f353fcd5..e89e64f3d81babb84715b4de1a9623f685c579c8 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -42,20 +42,27 @@ ndefinition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1)
 
 (* operatore < *)
 ndefinition lt_w16 ≝
-λw1,w2:word16.match lt_b8 (w16h w1) (w16h w2) with
- [ true ⇒ true
- | false ⇒ match gt_b8 (w16h w1) (w16h w2) with
-  [ true ⇒ false
-  | false ⇒ lt_b8 (w16l w1) (w16l w2) ]].
+λw1,w2:word16.
+ (lt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (lt_b8 (w16l w1) (w16l w2))).
 
 (* operatore ≤ *)
-ndefinition le_w16 ≝ λw1,w2:word16.(eq_w16 w1 w2) ⊕ (lt_w16 w1 w2).
+ndefinition le_w16 ≝
+λw1,w2:word16.
+ (lt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (le_b8 (w16l w1) (w16l w2))).
 
 (* operatore > *)
-ndefinition gt_w16 ≝ λw1,w2:word16.⊖ (le_w16 w1 w2).
+ndefinition gt_w16 ≝
+λw1,w2:word16.
+ (gt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (gt_b8 (w16l w1) (w16l w2))).
 
 (* operatore ≥ *)
-ndefinition ge_w16 ≝ λw1,w2:word16.⊖ (lt_w16 w1 w2).
+ndefinition ge_w16 ≝
+λw1,w2:word16.
+ (gt_b8 (w16h w1) (w16h w2)) ⊕
+ ((eq_b8 (w16h w1) (w16h w2)) ⊗ (ge_b8 (w16l w1) (w16l w2))).
 
 (* operatore and *)
 ndefinition and_w16 ≝
@@ -224,11 +231,14 @@ 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〉 7) 〈x8,x0〉 〈x0,x0〉 7 ]].
+  | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 nat7) 〈x8,x0〉 〈x0,x0〉 nat7 ]].
 
-(* operatore x in [inf,sup] *)
+(* operatore x in [inf,sup] o in sup],[inf *)
 ndefinition inrange_w16 ≝
-λx,inf,sup:word16.(le_w16 inf sup) ⊗ (ge_w16 x inf) ⊗ (le_w16 x sup).
+λx,inf,sup:word16.
+ match le_w16 inf sup with
+  [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_w16 inf x) (le_w16 x sup).
 
 (* iteratore sulle word *)
 ndefinition forall_w16 ≝