dk_binary_nat.dk 3.24 KB
Newer Older
1
#NAME dk_binary_nat.
2

3
4
def UNat : Type := dk_nat.Nat.
def Bool : Type := dk_bool.Bool.
5

6
bNat : cc.uT.
7
def BNat : Type := cc.eT bNat.
8

9
O : BNat.
10
def S0 : BNat -> BNat.
11
S1 : BNat -> BNat.
12
13
14
(; twice zero is zero ;)
[] S0 O --> O.

15
def nat_of_bnat : BNat -> UNat.
16
[] nat_of_bnat O --> dk_nat.O
17
[bn]
18
19
20
    nat_of_bnat (S0 bn)
      -->
    dk_nat.mult dk_nat.2 (nat_of_bnat bn)
21
[bn]
22
23
24
25
    nat_of_bnat (S1 bn)
      -->
    dk_nat.S (dk_nat.mult dk_nat.2 (nat_of_bnat bn)).

26
def succ : BNat -> BNat.
27
28
29
(; 0 + 1 = 2 * 0 + 1 ;)
[] succ O --> S1 O.
(; 2n + 1 = 2n + 1 ;)
30
[n] succ (S0 n) --> S1 n
31
(; 2n + 1 + 1 = 2 (n+1) ;)
32
[n] succ (S1 n) --> S0 (succ n).
33

34
def bnat_of_nat : UNat -> BNat.
35
[] bnat_of_nat dk_nat.O --> O
36
[n] bnat_of_nat (dk_nat.S n) --> succ (bnat_of_nat n).
37
38

(; Order ;)
39
40
41
42
def lt : BNat -> BNat -> Bool.
def gt : BNat -> BNat -> Bool.
def leq : BNat -> BNat -> Bool.
def geq : BNat -> BNat -> Bool.
43

44
45
46
47
48
49
[] 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.
50

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

53
54
55
56
57
58
[] 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.
59

60
[n,m] geq n m --> leq m n.
61
62

(; Equality ;)
63
64
def eq : BNat -> BNat -> Bool.
[n,m] eq n m
65
      --> dk_bool.and (leq n m) (geq n m).
66
67
68
69

(; Operations ;)

(; Addition ;)
70
71
72
73
74
75
76
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)).
77
78

(; Product ;)
79
80
81
82
83
84
85
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)).
86
87

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

91
92
def min : BNat -> BNat -> BNat.
[m,n] min m n --> dk_bool.ite bNat (leq m n) m n.
93
94
95

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

101
def length : BNat -> UNat.
102
[] length O --> dk_nat.O
103
104
[n] length (S0 n) --> dk_nat.S (length n)
[n] length (S1 n) --> dk_nat.S (length n).
105
106

(; quo2 n k = n / 2^k ;)
107
108
109
110
111
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.
112
113

(; mod2 n k = n % 2^k ;)
114
115
116
117
118
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).
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133


(; 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).