source: Deliverables/D4.1/Matita/Arithmetic.ma @ 246

Last change on this file since 246 was 246, checked in by mulligan, 11 years ago

Added physical file (Arithmetic) for arithmetic on bit vectors, and
added sparse bitvector trie for modelling 8051 memory.

File size: 3.1 KB
Line 
1include "Infrastructure/Universes.ma".
2include "Infrastructure/Equality.ma".
3include "Infrastructure/Connectives.ma".
4
5include "Common/Nat/Nat.ma".
6include "Common/Nat/Addition.ma".
7include "Common/Nat/Multiplication.ma".
8include "Common/Nat/Division_Modulus.ma".
9include "Common/Nat/Order.ma".
10
11include "Programming/Datatypes/Bool.ma".
12
13include "Programming/Datatypes/Listlike/Vector/BitVector.ma".
14include "Programming/Datatypes/Listlike/List/List.ma".
15   
16ndefinition eight ≝ exponential (S(S(Z))) (S(S(S(Z)))).
17ndefinition sixteen ≝ eight + eight.
18ndefinition one_hundred_and_twenty_eight ≝ sixteen × eight.
19ndefinition two_hundred_and_fifty_six ≝
20  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                         
21   
22ndefinition add_n_with_carry:
23      ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (List Bool) ≝
24  λn: Nat.
25  λb: BitVector n.
26  λc: BitVector n.
27  λcarry: Bool.
28    let b_as_nat ≝ nat_of_bitvector n b in
29    let c_as_nat ≝ nat_of_bitvector n c in
30    let carry_as_nat ≝ nat_of_bool carry in
31    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
32    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) × n)) +
33                  (modulus c_as_nat ((S (S Z)) × n)) +
34                  c_as_nat) ≥ ((S (S Z)) × n) in
35    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
36                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
37                  c_as_nat) ≥ ((S (S Z))^(n - (S Z)))) in
38    let result ≝ modulus result_old ((S (S Z))^n) in
39    let cy_flag ≝ (result_old ≥ ((S (S Z))^n)) in
40    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
41      ? (mk_Cartesian (BitVector n) ? (bitvector_of_nat n result)
42                          (cy_flag :: ac_flag :: ov_flag :: Empty Bool)).
43    //.
44nqed.
45
46(*
47ndefinition sub_8_with_carry ≝
48  λb: BitVector eight.
49  λc: BitVector eight.
50  λcarry: Bool.
51    let b_as_nat ≝ nat_of_bitvector eight b in
52    let c_as_nat ≝ nat_of_bitvector eight c in
53    let carry_as_nat ≝ nat_of_bool carry in
54    let result_old_1 ≝ subtraction_underflow b_as_nat c_as_nat in
55      match result_old_1 with
56        [ Nothing ⇒
57          let ac_flag ≝ True in
58         
59        | Just result_old_1' ⇒
60        ]
61*)
62   
63ndefinition add_8_with_carry ≝ add_n_with_carry eight.
64ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
65
66ndefinition increment ≝
67  λn: Nat.
68  λb: BitVector n.
69    let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in
70    let overflow ≝ b_as_nat ≥ (S (S Z))^n in
71      match overflow with
72        [ True ⇒ bitvector_of_nat n Z
73        | False ⇒ bitvector_of_nat n b_as_nat
74        ].
75       
76ndefinition decrement ≝
77  λn: Nat.
78  λb: BitVector n.
79    let b_as_nat ≝ nat_of_bitvector n b in
80      match b_as_nat with
81        [ Z ⇒ max n
82        | S o ⇒ bitvector_of_nat n o
83        ].
84       
85alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop".
86
87ndefinition bitvector_of_bool:
88      ∀n: Nat. ∀b: Bool. BitVector n ≝
89  λn: Nat.
90  λb: Bool.
91    ? (pad (n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
92  //.
93nqed.
Note: See TracBrowser for help on using the repository browser.