helm/software/matita/contribs/ng_assembly/num/comp_num.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/exadecim.ma".
  24
  25 (* *********** *)
  26 (* ESADECIMALI *)
  27 (* *********** *)
  28
  29 nrecord comp_num (T:Type) : Type ≝
  30  {
  31  cnH: T;
  32  cnL: T
  33  }.
  34
  35 ndefinition forall_cn ≝
  36 λT.λf:(T → bool) → bool.λP.
  37  f (λh.
  38  f (λl.
  39   P (mk_comp_num T h l))).
  40
  41 (* operatore = *)
  42 ndefinition eq2_cn ≝
  43 λT.λfeq:T → T → bool.
  44 λcn1,cn2:comp_num T.
  45  (feq (cnH ? cn1) (cnH ? cn2)) ⊗ (feq (cnL ? cn1) (cnL ? cn2)).
  46
  47 ndefinition eq_cn ≝
  48 λT.λfeq:T → bool.
  49 λcn:comp_num T.
  50  (feq (cnH ? cn)) ⊗ (feq (cnL ? cn)).
  51
  52 (* operatore < > *)
  53 ndefinition ltgt_cn ≝
  54 λT.λfeq:T → T → bool.λfltgt:T → T → bool.
  55 λcn1,cn2:comp_num T.
  56  (fltgt (cnH ? cn1) (cnH ? cn2)) ⊕
  57  ((feq (cnH ? cn1) (cnH ? cn2)) ⊗ (fltgt (cnL ? cn1) (cnL ? cn2))).
  58
  59 (* operatore ≤ ≥ *)
  60 ndefinition lege_cn ≝
  61 λT.λfeq:T → T → bool.λfltgt:T → T → bool.λflege:T → T → bool.
  62 λcn1,cn2:comp_num T.
  63  (fltgt (cnH ? cn1) (cnH ? cn2)) ⊕
  64  ((feq (cnH ? cn1) (cnH ? cn2)) ⊗ (flege (cnL ? cn1) (cnL ? cn2))).
  65
  66 (* operatore cn1 op cn2 *)
  67 ndefinition fop2_cn ≝
  68 λT.λfop:T → T → T.
  69 λcn1,cn2:comp_num T.
  70  mk_comp_num ? (fop (cnH ? cn1) (cnH ? cn2)) (fop (cnL ? cn1) (cnL ? cn2)).
  71
  72 ndefinition fop_cn ≝
  73 λT.λfop:T → T.
  74 λcn:comp_num T.
  75  mk_comp_num ? (fop (cnH ? cn)) (fop (cnL ? cn)).
  76
  77 (* operatore su parte high *)
  78 ndefinition getOPH_cn ≝
  79 λT.λf:T → bool.
  80 λcn:comp_num T.
  81  f (cnH ? cn).
  82
  83 ndefinition setOPH_cn ≝
  84 λT.λf:T → T.
  85 λcn:comp_num T.
  86  mk_comp_num ? (f (cnH ? cn)) (cnL ? cn).
  87
  88 (* operatore su parte low *)
  89 ndefinition getOPL_cn ≝
  90 λT.λf:T → bool.
  91 λcn:comp_num T.
  92  f (cnL ? cn).
  93
  94 ndefinition setOPL_cn ≝
  95 λT.λf:T → T.
  96 λcn:comp_num T.
  97  mk_comp_num ? (cnH ? cn) (f (cnL ? cn)).
  98
  99 (* operatore pred/succ *)
 100 ndefinition predsucc_cn ≝
 101 λT.λfz:T → bool.λfps:T → T.
 102 λcn:comp_num T.
 103  match fz (cnL ? cn) with
 104   [ true ⇒ mk_comp_num ? (fps (cnH ? cn)) (fps (cnL ? cn))
 105   | false ⇒ mk_comp_num ? (cnH ? cn) (fps (cnL ? cn)) ].
 106
 107 (* operatore con carry applicato DX → SX *)
 108 ndefinition opcr2_cn ≝
 109 λT.λfopcr:bool → T → T → (ProdT bool T).
 110 λc:bool.λcn1,cn2:comp_num T.
 111  match fopcr c (cnH ? cn1) (cnH ? cn2) with
 112   [ pair c' cnh' ⇒ match fopcr c' (cnL ? cn1) (cnL ? cn2) with
 113    [ pair c'' cnl' ⇒ pair … c'' (mk_comp_num ? cnh' cnl') ]].
 114
 115 ndefinition opcr_cn ≝
 116 λT.λfopcr:bool → T → (ProdT bool T).
 117 λc:bool.λcn:comp_num T.
 118  match fopcr c (cnH ? cn) with
 119   [ pair c' cnh' ⇒ match fopcr c' (cnL ? cn) with
 120    [ pair c'' cnl' ⇒ pair … c'' (mk_comp_num ? cnh' cnl') ]].
 121
 122 (* operatore con carry applicato SX → DX *)
 123 ndefinition opcl2_cn ≝
 124 λT.λfopcl:bool → T → T → (ProdT bool T).
 125 λc:bool.λcn1,cn2:comp_num T.
 126  match fopcl c (cnL ? cn1) (cnL ? cn2) with
 127   [ pair c' cnl' ⇒ match fopcl c' (cnH ? cn1) (cnH ? cn2) with
 128    [ pair c'' cnh' ⇒ pair … c'' (mk_comp_num ? cnh' cnl') ]].
 129
 130 ndefinition opcl_cn ≝
 131 λT.λfopcl:bool → T → (ProdT bool T).
 132 λc:bool.λcn:comp_num T.
 133  match fopcl c (cnL ? cn) with
 134   [ pair c' cnl' ⇒ match fopcl c' (cnH ? cn) with
 135    [ pair c'' cnh' ⇒ pair … c'' (mk_comp_num ? cnh' cnl') ]].