1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
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
|
module Univ
type iType
end
module Ghost
type gh 'a
constant gh : gh 'a
end
module Int
use export int.Int
end
module IntTrunc
function floor (x : int) : int = x
function ceiling (x : int) : int = x
function truncate (x : int) : int = x
function round (x : int) : int = x
function to_int (x : int) : int = x
predicate is_int int = true
predicate is_rat int = true
end
module IntDivE
use export int.EuclideanDivision
end
module IntDivT
(* TODO: divide and truncate *)
function div_t (x y : int) : int
function mod_t (x y : int) : int
end
module IntDivF
(* TODO: divide and floor *)
function div_f (x y : int) : int
function mod_f (x y : int) : int
end
module Rat
use int.Int as Int
type rat
predicate (< ) (x y : rat)
predicate (> ) (x y : rat) = y < x
predicate (<=) (x y : rat) = x < y \/ x = y
predicate (>=) (x y : rat) = y <= x
clone export algebra.OrderedField
with type t = rat, predicate (<=) = (<=)
function frac (n d : int) : rat
function numerator rat : int
function denominator rat : int
axiom inversion : forall r : rat. r = frac (numerator r) (denominator r)
axiom dpositive : forall r : rat. Int.(>) (denominator r) 0
axiom frac_zero : forall d : int. d <> 0 -> frac 0 d = zero
axiom frac_unit : forall d : int. d <> 0 -> frac d d = one
axiom nume_zero : numerator zero = 0
axiom deno_zero : denominator zero = 1
axiom nume_unit : numerator one = 1
axiom deno_unit : denominator one = 1
axiom proportion : forall n1 n2 d1 d2 : int. d1 <> 0 -> d2 <> 0 ->
(frac n1 d1 = frac n2 d2 <-> Int.(*) n1 d2 = Int.(*) n2 d1)
function to_rat (x : rat) : rat = x
predicate is_int (r : rat) = denominator r = 1
predicate is_rat rat = true
end
module RatTrunc
use Rat
(* TODO: axiomatize *)
function floor (x : rat) : rat
function ceiling (x : rat) : rat
function truncate (x : rat) : rat
function round (x : rat) : rat
function to_int (x : rat) : int = numerator (floor x)
end
module RatDivE
use Rat
(* TODO: euclidean division *)
function div (x y : rat) : rat
function mod (x y : rat) : rat
end
module RatDivT
use Rat
(* TODO: divide and truncate *)
function div_t (x y : rat) : rat
function mod_t (x y : rat) : rat
end
module RatDivF
use Rat
(* TODO: divide and floor *)
function div_f (x y : rat) : rat
function mod_f (x y : rat) : rat
end
module Real
use export real.Real
function to_real (x : real) : real = x
end
module RealTrunc
use Real
use real.FromInt as FromInt
use real.Truncate as Truncate
function floor (x : real) : real = FromInt.from_int (Truncate.floor x)
function ceiling (x : real) : real = FromInt.from_int (Truncate.ceil x)
function truncate (x : real) : real = FromInt.from_int (Truncate.truncate x)
(* TODO : axiomatize *)
function round (x : real) : real
function to_int (x : real) : int = Truncate.floor x
predicate is_int (r : real) = r = FromInt.from_int (Truncate.truncate r)
predicate is_rat (r : real) =
exists n d : int. d <> 0 /\ r * FromInt.from_int d = FromInt.from_int n
end
module RealDivE
(* TODO: euclidean division *)
function div (x y : real) : real
function mod (x y : real) : real
end
module RealDivT
(* TODO: divide and truncate *)
function div_t (x y : real) : real
function mod_t (x y : real) : real
end
module RealDivF
(* TODO: divide and floor *)
function div_f (x y : real) : real
function mod_f (x y : real) : real
end
module IntToRat
use Rat
function to_rat (x : int) : rat = frac x 1
end
module IntToReal
use real.FromInt as FromInt
function to_real (x : int) : real = FromInt.from_int x
end
module RealToRat
use Rat
(* TODO: axiomatize *)
function to_rat (x : real) : rat
end
module RatToReal
use Rat
use real.Real
use real.FromInt as FromInt
function to_real (x : rat) : real =
FromInt.from_int (numerator x) / FromInt.from_int (denominator x)
end
|
