# source:Deliverables/D4.1/Matita/Arithmetic.ma@248

Last change on this file since 248 was 248, checked in by mulligan, 10 years ago

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