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

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

More work on bitvectors.

File size: 1.6 KB
RevLine 
[235]1include "Vector.ma".
[234]2include "List.ma".
[228]3include "Nat.ma".
4include "Bool.ma".
[224]5
[228]6ndefinition BitVector ≝ λn: Nat. Vector Bool n.
[230]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)))))))))))))))).
[224]12
[228]13ndefinition zero ≝
14  λn: Nat.
15    replicate Bool n False.
16   
[224]17ndefinition conjunction ≝
[228]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.
[231]33    zip Bool Bool Bool n exclusive_disjunction b c.
[232]34   
[234]35ndefinition complement ≝
36  λn: Nat.
37  λb: BitVector n.
38    map Bool Bool n (negation) b.
[232]39
[234]40ndefinition divide_with_remainder ≝
41  λm, n: Nat.
42    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
43
[235]44nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
[234]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
[235]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.