]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/num/comp_num.ma
wip ....
[helm.git] / matita / 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') ]].