freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
index f2cbdb7583e7959eae5ebbe0182387ca84302d0d..d759181cebea9ffeb1ee66b290d7bb5014966c98 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8.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              *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -43,20 +43,27 @@ ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1
 
 (* operatore < *)
 ndefinition lt_b8 ≝
-λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
- [ true ⇒ true
- | false ⇒ match gt_ex (b8h b1) (b8h b2) with
-  [ true ⇒ false
-  | false ⇒ lt_ex (b8l b1) (b8l b2) ]].
+λb1,b2:byte8.
+ (lt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (lt_ex (b8l b1) (b8l b2))).
 
 (* operatore ≤ *)
-ndefinition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2). 
+ndefinition le_b8 ≝
+λb1,b2:byte8.
+ (lt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (le_ex (b8l b1) (b8l b2))).
 
 (* operatore > *)
-ndefinition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).
+ndefinition gt_b8 ≝
+λb1,b2:byte8.
+ (gt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (gt_ex (b8l b1) (b8l b2))).
 
 (* operatore ≥ *)
-ndefinition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).
+ndefinition ge_b8 ≝
+λb1,b2:byte8.
+ (gt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (ge_ex (b8l b1) (b8l b2))).
 
 (* operatore and *)
 ndefinition and_b8 ≝
@@ -91,10 +98,10 @@ ndefinition ror_b8 ≝
    | false ⇒ mk_byte8 bh' bl' ]]].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝
- match r with
-  [ oc_O ⇒ b
-  | oc_S t n' ⇒ ror_b8_n (ror_b8 b) t n' ].
+nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
+ match n with
+  [ O ⇒ b
+  | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_b8 ≝
@@ -117,10 +124,10 @@ ndefinition rol_b8 ≝
    | false ⇒ mk_byte8 bh' bl' ]]].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝
- match r with
-  [ oc_O ⇒ b
-  | oc_S t n' ⇒ rol_b8_n (rol_b8 b) t n' ].
+nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
+ match n with
+  [ O ⇒ b
+  | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_b8 ≝
@@ -299,6 +306,13 @@ ndefinition daa_b8 ≝
    pair … X'' true
   ].
 
+(* operatore x in [inf,sup] o in sup],[inf *)
+ndefinition inrange_b8 ≝
+λx,inf,sup:byte8.
+ match le_b8 inf sup with
+  [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_b8 inf x) (le_b8 x sup).
+
 (* iteratore sui byte *)
 ndefinition forall_b8 ≝
  λP.
@@ -314,8 +328,10 @@ ninductive rec_byte8 : byte8 → Type ≝
 (* byte → byte ricorsivi *)
 ndefinition b8_to_recb8_aux1 : Πn.rec_byte8 〈n,x0〉 → rec_byte8 〈succ_ex n,x0〉 ≝
 λn.λrecb:rec_byte8 〈n,x0〉.
- b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (
- b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))).
+ b8_S 〈n,xF〉 (b8_S 〈n,xE〉 (b8_S 〈n,xD〉 (b8_S 〈n,xC〉 (
+ b8_S 〈n,xB〉 (b8_S 〈n,xA〉 (b8_S 〈n,x9〉 (b8_S 〈n,x8〉 (
+ b8_S 〈n,x7〉 (b8_S 〈n,x6〉 (b8_S 〈n,x5〉 (b8_S 〈n,x4〉 (
+ b8_S 〈n,x3〉 (b8_S 〈n,x2〉 (b8_S 〈n,x1〉 (b8_S 〈n,x0〉 recb))))))))))))))).
 
 (* ... cifra esadecimale superiore *)
 nlet rec b8_to_recb8_aux2 (n:exadecim) (r:rec_exadecim n) on r ≝
@@ -329,25 +345,54 @@ ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1
 λn1,n2.λrecb:rec_byte8 〈n1,x0〉.
  match n2 return λx.rec_byte8 〈n1,x〉 with
   [ x0 ⇒ recb
-  | x1 ⇒ b8_S ? recb
-  | x2 ⇒ b8_S ? (b8_S ? recb)
-  | x3 ⇒ b8_S ? (b8_S ? (b8_S ? recb))
-  | x4 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))
-  | x5 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))
-  | x6 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))
-  | x7 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))
-  | x8 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))
-  | x9 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))
-  | xA ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))
-  | xB ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))
-  | xC ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))))
-  | xD ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))
-  | xE ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))))))
-  | xF ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))
+  | x1 ⇒ b8_S 〈n1,x0〉 recb
+  | x2 ⇒ b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)
+  | x3 ⇒ b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))
+  | x4 ⇒ b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))
+  | x5 ⇒ b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
+         b8_S 〈n1,x0〉 recb))))
+  | x6 ⇒ b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
+         b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))
+  | x7 ⇒ b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
+         b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))
+  | x8 ⇒ b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
+         b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))
+  | x9 ⇒ b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
+         b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
+         b8_S 〈n1,x0〉 recb))))))))
+  | xA ⇒ b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
+         b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
+         b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))
+  | xB ⇒ b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
+         b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
+         b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))
+  | xC ⇒ b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (
+         b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
+         b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))
+  | xD ⇒ b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (
+         b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
+         b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
+         b8_S 〈n1,x0〉 recb))))))))))))
+  | xE ⇒ b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (
+         b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
+         b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
+         b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))))
+  | xF ⇒ b8_S 〈n1,xE〉 (b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (
+         b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
+         b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
+         b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))))))
   ].
 
-ndefinition b8_to_recb8 ≝
-λn.b8_to_recb8_aux3 (b8h n) (b8l n) (b8_to_recb8_aux2 (b8h n) (ex_to_recex (b8h n))).
+(*
+nlemma b8_to_recb8 : Πb.rec_byte8 b.
+ #b; nletin K ≝ (b8_to_recb8_aux3 
+     (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
+ ncases b in K; #e1; #e2; #K; napply K;
+nqed.
+*)
+
+ndefinition b8_to_recb8 : Πb.rec_byte8 b ≝
+λb.match b with [ mk_byte8 h l ⇒ b8_to_recb8_aux3 h l (b8_to_recb8_aux2 h (ex_to_recex h)) ].
 
 (* ottali → esadecimali *)
 ndefinition b8_of_bit ≝