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

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