dk_machine_int.dk 6.3 KB
Newer Older
1
#NAME dk_machine_int.
2
def Bool : Type := dk_bool.Bool.
3

4
5
6
def UNat : Type := dk_nat.Nat.
def UO : UNat := dk_nat.O.
def US : UNat -> UNat := dk_nat.S.
7

8
9
10
Mint : UNat -> cc.uT.
MInt : UNat -> Type.
[N] cc.eT (Mint N) --> MInt N.
11
12
13
14
15

O : MInt UO.
S0 : N : UNat -> MInt N -> MInt (US N).
S1 : N : UNat -> MInt N -> MInt (US N).

16
def zero : N : UNat -> MInt N.
17
[] zero dk_nat.O --> O
18
[N] zero (dk_nat.S N) --> S0 N (zero N).
19

20
def bound : N : UNat -> MInt N.
21
[] bound dk_nat.O --> O
22
[N] bound (dk_nat.S N) --> S1 N (bound N).
23
24

(; cast ;)
25
26
27
28
def downcast : N : UNat -> MInt (US N) -> MInt N.
[]    downcast dk_nat.O _ --> O
[N,n] downcast (dk_nat.S _) (S0 (dk_nat.S N) n) --> S0 N (downcast N n)
[N,n] downcast (dk_nat.S _) (S1 (dk_nat.S N) n) --> S1 N (downcast N n).
29

30
def double (N : UNat) (n : MInt N) : MInt N := downcast N (S0 N n).
31

32
def succ : N : UNat -> MInt N -> MInt N.
33
[] succ dk_nat.O O --> O
34
35
[N,n] succ (dk_nat.S _) (S0 N n) --> S1 N n
[N,n] succ (dk_nat.S _) (S1 N n) --> S0 N (succ N n).
36

37
def pred : N : UNat -> MInt N -> MInt N.
38
[] pred dk_nat.O O --> O
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
[N,n] pred (dk_nat.S _) (S1 N n) --> S0 N n
[N,n] pred (dk_nat.S _) (S0 N n) --> S1 N (pred N n).

def plus : N : UNat -> MInt N -> MInt N -> MInt N.
[]  plus dk_nat.O O O --> O
[N,n,m]
    plus (dk_nat.S N) (S0 _ n) (S0 _ m) --> S0 N (plus N n m)
[N,n,m]
    plus (dk_nat.S N) (S0 _ n) (S1 _ m) --> S1 N (plus N n m)
[N,n,m]
    plus (dk_nat.S N) (S1 _ n) (S0 _ m) --> S1 N (plus N n m)
[N,n,m]
    plus (dk_nat.S N) (S1 _ n) (S1 _ m) --> S0 N (succ N (plus N n m)).

def complement : N : UNat -> MInt N -> MInt N.
54
[] complement dk_nat.O O --> O
55
56
[N,n] complement (dk_nat.S N) (S0 _ n) --> S1 N (complement N n)
[N,n] complement (dk_nat.S N) (S1 _ n) --> S0 N (complement N n).
57

58
59
def opp : N : UNat -> MInt N -> MInt N.
[N,n] opp N n --> succ N (complement N n).
60

61
62
def sub : N : UNat -> MInt N -> MInt N -> MInt N.
[N,n,m] sub N n m --> plus N n (opp N m).
63
64

(; Product ;)
65
def mult : N : UNat -> MInt N -> MInt N -> MInt N.
66
[ ] mult dk_nat.O O O --> O
67
68
[N,n,m]
    mult (dk_nat.S N) (S0 _ n) (S0 _ m)
69
70
      -->
    double (US N) (S0 N (mult N n m))
71
72
[N,n,m]
    mult (dk_nat.S N) (S0 _ n) (S1 _ m)
73
74
      -->
    S0 N (plus N m (double N (mult N n m)))
75
76
[N,n,m]
    mult (dk_nat.S N) (S1 _ n) (S0 _ m)
77
78
      -->
    S0 N (plus N n (double N (mult N n m)))
79
80
[N,n,m]
    mult (dk_nat.S N) (S1 _ n) (S1 _ m)
81
82
      -->
    S1 N (plus N (double N (mult N m n)) (plus N n m)).
83
84

(; equality ;)
85
86
87
88
89
90
91
92
93
94
95
def equal : N : UNat -> MInt N -> MInt N -> Bool.
(; [n] equal _ n n --> dk_bool.true ;)
[] equal _ O O --> dk_bool.true
[N,n,m]
    equal (dk_nat.S N) (S0 _ n) (S0 _ m) --> equal N n m
[N,n,m]
    equal (dk_nat.S N) (S1 _ n) (S1 _ m) --> equal N n m
[]
    equal (dk_nat.S _) (S0 _ _) (S1 _ _) --> dk_bool.false
[]
    equal (dk_nat.S _) (S1 _ _) (S0 _ _) --> dk_bool.false.
96
97

(; unsigned comparison ;)
98
99
def unsigned_lt : N : UNat -> MInt N -> MInt N -> Bool.
def unsigned_leq : N : UNat -> MInt N -> MInt N -> Bool.
100

101
[] unsigned_lt dk_nat.O O O --> dk_bool.false
102
103
[N,n,m]
    unsigned_lt (dk_nat.S N) (S0 _ n) (S0 _ m)
104
105
      -->
    unsigned_lt N n m
106
107
[N,n,m]
    unsigned_lt (dk_nat.S N) (S1 _ n) (S1 _ m)
108
109
      -->
    unsigned_lt N n m
110
111
[N,n,m]
    unsigned_lt (dk_nat.S N) (S0 _ n) (S1 _ m)
112
113
      -->
    unsigned_leq N n m
114
115
[N,n,m]
    unsigned_lt (dk_nat.S N) (S1 _ n) (S0 _ m)
116
117
      -->
    unsigned_lt N n m.
118

119
[] unsigned_leq dk_nat.O O O --> dk_bool.true
120
121
[N,n,m]
    unsigned_leq (dk_nat.S N) (S0 _ n) (S0 _ m)
122
123
      -->
    unsigned_leq N n m
124
125
[N,n,m]
    unsigned_leq (dk_nat.S N) (S1 _ n) (S1 _ m)
126
127
      -->
    unsigned_leq N n m
128
129
[N,n,m]
    unsigned_leq (dk_nat.S N) (S0 _ n) (S1 _ m)
130
131
      -->
    unsigned_leq N n m
132
133
[N,n,m]
    unsigned_leq (dk_nat.S N) (S1 _ n) (S0 _ m)
134
135
136
      -->
    unsigned_lt N n m.

137
138
def unsigned_gt : N : UNat -> MInt N -> MInt N -> Bool
                := N : UNat => n : MInt N => m : MInt N => unsigned_lt N m n.
139

140
141
def unsigned_geq : N : UNat -> MInt N -> MInt N -> Bool
                 := N : UNat => n : MInt N => m : MInt N => unsigned_leq N m n.
142
143

(; signed comparison ;)
144
def positive : N : UNat -> MInt N -> Bool.
145
146
147
[] positive dk_nat.O O --> dk_bool.true
[] positive (dk_nat.S dk_nat.O) (S0 dk_nat.O O) --> dk_bool.true
[] positive (dk_nat.S dk_nat.O) (S1 dk_nat.O O) --> dk_bool.false
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
[N,n] positive (dk_nat.S N) (S0 _ n) --> positive N n
[N,n] positive (dk_nat.S N) (S1 _ n) --> positive N n.

def signed_leq : N : UNat ->
                 n : MInt N ->
                 m : MInt N ->
                 Bool
               :=
                 N : UNat =>
                 n : MInt N =>
                 m : MInt N =>
                 dk_bool.iteb (dk_bool.and
                                (positive N m)
                                (dk_bool.not (positive N n)))
                              dk_bool.true
                                (dk_bool.iteb (dk_bool.and
                                                (positive N n)
                                                (dk_bool.not (positive N m)))
                                              dk_bool.false
                                                (positive N (sub N m n))).

def signed_geq : N : UNat ->
                 n : MInt N ->
                 m : MInt N ->
                 Bool
               :=
                 N : UNat =>
                 n : MInt N =>
                 m : MInt N =>
                 signed_leq N m n.

def signed_lt : N : UNat ->
                n : MInt N ->
                m : MInt N ->
                Bool
              :=
                N : UNat =>
                n : MInt N =>
                m : MInt N =>
                dk_bool.not (signed_geq N m n).

def signed_gt : N : UNat ->
                n : MInt N ->
                m : MInt N ->
                Bool
              :=
                N : UNat =>
                n : MInt N =>
                m : MInt N =>
                dk_bool.not (signed_leq N m n).
198

199
(; Casting Peano natural numbers ;)
200
201
202
def cast_peano : N : UNat -> n : UNat -> MInt N.
[N] cast_peano N dk_nat.O --> zero N
[N,n] cast_peano N (dk_nat.S n) --> succ N (cast_peano N n).
203
204

(; Casting binary natural numbers ;)
205

206
207
208
209
def cast_bnat : N : UNat -> bn : dk_binary_nat.BNat -> MInt N.
[N] cast_bnat N dk_binary_nat.O --> zero N
[ ] cast_bnat dk_nat.O _ --> O.
[N,bn]
210
211
212
    cast_bnat (dk_nat.S N) (dk_binary_nat.S0 bn)
      -->
    S0 N (cast_bnat N bn)
213
[N,bn]
214
215
216
    cast_bnat (dk_nat.S N) (dk_binary_nat.S1 bn)
      -->
    S1 N (cast_bnat N bn).