source: Deliverables/D4.1/Matita/BitVector.ma @ 234

Last change on this file since 234 was 234, checked in by mulligan, 9 years ago

Division and modulus implemented. All necessary orders on naturals
completed. More operations on bitvectors (and general operations that
apply to all vectors) implemented.

File size: 1.3 KB
Line 
1include "List.ma".
2include "Vector.ma".
3include "Nat.ma".
4include "Bool.ma".
5
6ndefinition BitVector ≝ λn: Nat. Vector Bool n.
7ndefinition Bit ≝ BitVector (S Z).
8ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
9ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
10ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
11ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
12
13ndefinition zero ≝
14  λn: Nat.
15    replicate Bool n False.
16   
17ndefinition conjunction ≝
18  λn: Nat.
19  λb: BitVector n.
20  λc: BitVector n.
21    zip Bool Bool Bool n conjunction b c.
22   
23ndefinition inclusive_disjunction ≝
24  λn: Nat.
25  λb: BitVector n.
26  λc: BitVector n.
27    zip Bool Bool Bool n inclusive_disjunction b c.
28   
29ndefinition exclusive_disjunction ≝
30  λn: Nat.
31  λb: BitVector n.
32  λc: BitVector n.
33    zip Bool Bool Bool n exclusive_disjunction b c.
34   
35ndefinition complement ≝
36  λn: Nat.
37  λb: BitVector n.
38    map Bool Bool n (negation) b.
39
40ndefinition divide_with_remainder ≝
41  λm, n: Nat.
42    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
43
44nlet rec bitvector_of_nat_aux (n: Nat): List Nat ≝
45  let div_rem ≝ divide_with_remainder n (S (S Z)) in
46  let div ≝ first Nat Nat div_rem in
47  let rem ≝ second Nat Nat div_rem in
48    Empty Nat.
Note: See TracBrowser for help on using the repository browser.