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))
          ]
      ].