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

Last change on this file since 246 was 246, checked in by mulligan, 9 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.