Smaller formulae.

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma b/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma
index 4dd950268c39a3a62875eacb1423cd172d25db20..f15537cc75f6a1c5dd6eb5905c94d7c7eaad0be7 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma
@@ -13,18 +13,15 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/exadecim.ma".
+include "freescale/bitrigesim.ma".
 
 (* **** *)
 (* BYTE *)
@@ -36,21 +33,6 @@ nrecord byte8 : Type ≝
  b8l: exadecim
  }.
 
-ndefinition byte8_ind : ΠP:byte8 → Prop.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
-λP:byte8 → Prop.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
- match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
-
-ndefinition byte8_rec : ΠP:byte8 → Set.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
-λP:byte8 → Set.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
- match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
-
-ndefinition byte8_rect : ΠP:byte8 → Type.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
-λP:byte8 → Type.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
- match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
-
-ndefinition b8h ≝ λb:byte8.match b with [ mk_byte8 x _ ⇒ x ].
-ndefinition b8l ≝ λb:byte8.match b with [ mk_byte8 _ x ⇒ x ].
-
 (* \langle \rangle *)
 notation "〈x,y〉" non associative with precedence 80
  for @{ 'mk_byte8 $x $y }.
@@ -92,13 +74,13 @@ ndefinition xor_b8 ≝
 ndefinition rcr_b8 ≝
 λb:byte8.λc:bool.match rcr_ex (b8h b) c with
  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
-  [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]]. 
+  [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]]. 
 
 (* operatore shift destro *)
 ndefinition shr_b8 ≝
 λb:byte8.match rcr_ex (b8h b) false with
  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
-  [ pair bl' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
+  [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
 
 (* operatore rotazione destra *)
 ndefinition ror_b8 ≝
@@ -109,22 +91,22 @@ ndefinition ror_b8 ≝
    | false ⇒ mk_byte8 bh' bl' ]]].
 
 (* operatore rotazione destra n-volte *)
-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' ].
+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' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_b8 ≝
 λb:byte8.λc:bool.match rcl_ex (b8l b) c with
  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
-  [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]]. 
+  [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]]. 
 
 (* operatore shift sinistro *)
 ndefinition shl_b8 ≝
 λb:byte8.match rcl_ex (b8l b) false with
  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
-  [ pair bh' c'' ⇒ pair ?? (mk_byte8 bh' bl') c'' ]].
+  [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
 
 (* operatore rotazione sinistra *)
 ndefinition rol_b8 ≝
@@ -135,10 +117,10 @@ ndefinition rol_b8 ≝
    | false ⇒ mk_byte8 bh' bl' ]]].
 
 (* operatore rotazione sinistra n-volte *)
-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' ].
+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' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_b8 ≝
@@ -149,7 +131,7 @@ ndefinition plus_b8_dc_dc ≝
 λb1,b2:byte8.λc:bool.
  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
   [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
-   [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]].
+   [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
 
 (* operatore somma con data+carry → data *)
 ndefinition plus_b8_dc_d ≝
@@ -167,7 +149,7 @@ ndefinition plus_b8_d_dc ≝
 λb1,b2:byte8.
  match plus_ex_d_dc (b8l b1) (b8l b2) with
   [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
-   [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]].
+   [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
 
 (* operatore somma con data → data *)
 ndefinition plus_b8_d_d ≝
@@ -183,9 +165,6 @@ ndefinition plus_b8_d_c ≝
 (* operatore Most Significant Bit *)
 ndefinition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
 
-(* byte → naturali *)
-ndefinition nat_of_byte8 ≝ λb:byte8.(16*(nat_of_exadecim (b8h b))) + (nat_of_exadecim (b8l b)).
-
 (* operatore predecessore *)
 ndefinition pred_b8 ≝
 λb:byte8.match eq_ex (b8l b) x0 with
@@ -306,7 +285,7 @@ ndefinition daa_b8 ≝
    let X'' ≝ match c with
     [ true ⇒ plus_b8_d_d X' 〈x6,x0〉
     | false ⇒ X' ] in
-   pair ?? X'' c
+   pair … X'' c
   (* [X:0x9A-0xFF] *)
   (* c' = 1 *)
   (* X' = [X:0x9A-0xFF]
@@ -317,12 +296,68 @@ ndefinition daa_b8 ≝
     [ true ⇒ X
     | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
    let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in
-   pair ?? X'' true
+   pair … X'' true
   ].
 
 (* iteratore sui byte *)
-ndefinition forall_byte8 ≝
+ndefinition forall_b8 ≝
  λP.
-  forall_exadecim (λbh.
-  forall_exadecim (λbl.
+  forall_ex (λbh.
+  forall_ex (λbl.
    P (mk_byte8 bh bl))).
+
+(* byte ricorsivi *)
+ninductive rec_byte8 : byte8 → Type ≝
+  b8_O : rec_byte8 〈x0,x0〉
+| b8_S : ∀n.rec_byte8 n → rec_byte8 (succ_b8 n).
+
+(* 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))))))))))))))).
+
+(* ... cifra esadecimale superiore *)
+nlet rec b8_to_recb8_aux2 (n:exadecim) (r:rec_exadecim n) on r ≝
+ match r return λx.λy:rec_exadecim x.rec_byte8 〈x,x0〉 with
+  [ ex_O ⇒ b8_O
+  | ex_S t n' ⇒ b8_to_recb8_aux1 ? (b8_to_recb8_aux2 t n')
+  ].
+
+(* ... cifra esadecimale inferiore *)
+ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1,n2〉 ≝
+λ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))))))))))))))
+  ].
+
+ndefinition b8_to_recb8 ≝
+λn.b8_to_recb8_aux3 (b8h n) (b8l n) (b8_to_recb8_aux2 (b8h n) (ex_to_recex (b8h n))).
+
+(* ottali → esadecimali *)
+ndefinition b8_of_bit ≝
+λn.match n with
+ [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
+ | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
+ | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
+ | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
+ | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
+ | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
+ | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
+ | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉
+ ].