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

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

More work on bitvectors.

File size: 1.6 KB
Line 
1include "Vector.ma".
2include "List.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) on n ≝
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    match div with
49      [ Z ⇒
50        match rem with
51          [ Z ⇒ Empty Bool
52          | S r ⇒ True :: (bitvector_of_nat_aux Z)
53          ]
54      | S d ⇒
55        match rem with
56          [ Z ⇒ False :: (bitvector_of_nat_aux (S d))
57          | S r ⇒ True :: (bitvector_of_nat_aux (S d))
58          ]
59      ].
Note: See TracBrowser for help on using the repository browser.