include "Vector.ma". include "List.ma". include "Nat.ma". include "Bool.ma". ndefinition BitVector ≝ λn: Nat. Vector Bool n. ndefinition Bit ≝ BitVector (S Z). ndefinition Nibble ≝ BitVector (S (S (S (S Z)))). ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))). ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))). ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). ndefinition zero ≝ λn: Nat. replicate Bool n False. ndefinition conjunction ≝ λn: Nat. λb: BitVector n. λc: BitVector n. zip Bool Bool Bool n conjunction b c. ndefinition inclusive_disjunction ≝ λn: Nat. λb: BitVector n. λc: BitVector n. zip Bool Bool Bool n inclusive_disjunction b c. ndefinition exclusive_disjunction ≝ λn: Nat. λb: BitVector n. λc: BitVector n. zip Bool Bool Bool n exclusive_disjunction b c. ndefinition complement ≝ λn: Nat. λb: BitVector n. map Bool Bool n (negation) b. ndefinition divide_with_remainder ≝ λm, n: Nat. mk_Cartesian Nat Nat (m ÷ n) (modulus m n). nlet rec bitvector_of_nat_aux (n: Nat) on n ≝ let div_rem ≝ divide_with_remainder n (S (S Z)) in let div ≝ first Nat Nat div_rem in let rem ≝ second Nat Nat div_rem in match div with [ Z ⇒ match rem with [ Z ⇒ Empty Bool | S r ⇒ True :: (bitvector_of_nat_aux Z) ] | S d ⇒ match rem with [ Z ⇒ False :: (bitvector_of_nat_aux (S d)) | S r ⇒ True :: (bitvector_of_nat_aux (S d)) ] ].