dk_binary_nat.dk

#NAME dk_binary_nat.

def UNat : Type := dk_nat.Nat.
def Bool : Type := dk_bool.Bool.

bNat : cc.uT.
def BNat : Type := cc.eT bNat.

O : BNat.
def S0 : BNat -> BNat.
S1 : BNat -> BNat.
(; twice zero is zero ;)
[] S0 O --> O.

def nat_of_bnat : BNat -> UNat.
[] nat_of_bnat O --> dk_nat.O
[bn]
    nat_of_bnat (S0 bn)
      -->
    dk_nat.mult dk_nat.2 (nat_of_bnat bn)
[bn]
    nat_of_bnat (S1 bn)
      -->
    dk_nat.S (dk_nat.mult dk_nat.2 (nat_of_bnat bn)).

def succ : BNat -> BNat.
(; 0 + 1 = 2 * 0 + 1 ;)
[] succ O --> S1 O.
(; 2n + 1 = 2n + 1 ;)
[n] succ (S0 n) --> S1 n
(; 2n + 1 + 1 = 2 (n+1) ;)
[n] succ (S1 n) --> S0 (succ n).

def bnat_of_nat : UNat -> BNat.
[] bnat_of_nat dk_nat.O --> O
[n] bnat_of_nat (dk_nat.S n) --> succ (bnat_of_nat n).

(; Order ;)
def lt : BNat -> BNat -> Bool.
def gt : BNat -> BNat -> Bool.
def leq : BNat -> BNat -> Bool.
def geq : BNat -> BNat -> Bool.

[] lt _ O --> dk_bool.false
[] lt O _ --> dk_bool.true
[n,m] lt (S0 n) (S0 m) --> lt n m
[n,m] lt (S0 n) (S1 m) --> leq n m
[n,m] lt (S1 n) (S0 m) --> lt n m
[n,m] lt (S1 n) (S1 m) --> lt n m.

[n,m] gt n m --> lt m n.

[] leq O _ --> dk_bool.true
[] leq _ O --> dk_bool.false
[n,m] leq (S0 n) (S0 m) --> leq n m
[n,m] leq (S0 n) (S1 m) --> leq n m
[n,m] leq (S1 n) (S0 m) --> lt n m
[n,m] leq (S1 n) (S1 m) --> leq n m.

[n,m] geq n m --> leq m n.

(; Equality ;)
def eq : BNat -> BNat -> Bool.
[n,m] eq n m
      --> dk_bool.and (leq n m) (geq n m).

(; Operations ;)

(; Addition ;)
def plus : BNat -> BNat -> BNat.
[m] plus O m --> m
[n] plus n O --> n
[n,m] plus (S0 n) (S0 m) --> S0 (plus n m)
[n,m] plus (S0 n) (S1 m) --> S1 (plus n m)
[n,m] plus (S1 n) (S0 m) --> S1 (plus n m)
[n,m] plus (S1 n) (S1 m) --> S0 (succ (plus n m)).

(; Product ;)
def mult : BNat -> BNat -> BNat.
[] mult O _ --> O
[] mult _ O --> O
[n,m] mult (S0 n) (S0 m) --> S0 (S0 (mult n m))
[n,m] mult (S0 n) (S1 m) --> S0 (plus m (S0 (mult n m)))
[n,m] mult (S1 n) (S0 m) --> S0 (plus n (S0 (mult n m)))
[n,m] mult (S1 n) (S1 m) --> S1 (plus (S0 (mult m n)) (plus n m)).

(; Min and Max ;)
def max : BNat -> BNat -> BNat.
[m,n] max m n --> dk_bool.ite bNat (leq m n) n m.

def min : BNat -> BNat -> BNat.
[m,n] min m n --> dk_bool.ite bNat (leq m n) m n.

(; Euclidian division ;)
(; by a power of 2 ;)
def div2 : BNat -> BNat.
[] div2 O --> O
[n] div2 (S0 n) --> n
[n] div2 (S1 n) --> n.

def length : BNat -> UNat.
[] length O --> dk_nat.O
[n] length (S0 n) --> dk_nat.S (length n)
[n] length (S1 n) --> dk_nat.S (length n).

(; quo2 n k = n / 2^k ;)
def quo2 : BNat -> UNat -> BNat.
[n] quo2 n dk_nat.O --> n
[] quo2 O _ --> O
[n,k] quo2 (S0 n) (dk_nat.S k) --> quo2 n k
[n,k] quo2 (S1 n) (dk_nat.S k) --> quo2 n k.

(; mod2 n k = n % 2^k ;)
def mod2 : BNat -> UNat -> BNat.
[] mod2 _ dk_nat.O --> O
[] mod2 O _ --> O
[n,k] mod2 (S0 n) (dk_nat.S k) --> S0 (mod2 n k)
[n,k] mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).


(; Casting to machine numbers ;)

def mnat_of_bnat : N : UNat -> bn : BNat -> dk_machine_int.MInt N.
[N] mnat_of_bnat N O --> dk_machine_int.zero N
[ ] mnat_of_bnat dk_nat.O _ --> dk_machine_int.O.
[N,bn]
    mnat_of_bnat (dk_nat.S N) (dk_binary_natS0 bn)
      -->
    dk_machine_int.S0 N (mnat_of_bnat N bn)
[N,bn]
    mnat_of_bnat (dk_nat.S N) (dk_binary_natS1 bn)
      -->
    dk_machine_int.S1 N (mnat_of_bnat N bn).