real.why 7.92 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2
theory Real
MARCHE Claude's avatar
MARCHE Claude committed
3

Andrei Paskevich's avatar
Andrei Paskevich committed
4
5
  function zero : real = 0.0
  function one  : real = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
6

Andrei Paskevich's avatar
Andrei Paskevich committed
7
8
9
  predicate (< ) real real
  predicate (> ) (x y : real) = y < x
  predicate (<=) (x y : real) = x < y \/ x = y
MARCHE Claude's avatar
MARCHE Claude committed
10

Andrei Paskevich's avatar
Andrei Paskevich committed
11
12
  clone export algebra.OrderedField with type t = real,
    function zero = zero, function one = one, predicate (<=) = (<=)
13

MARCHE Claude's avatar
MARCHE Claude committed
14
15
16
17
18
19
end

theory RealInfix

  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
20
21
22
23
24
  function (+.) (x:real) (y:real) : real = x + y
  function (-.) (x:real) (y:real) : real = x - y
  function ( *.) (x:real) (y:real) : real = x * y
  function (/.) (x:real) (y:real) : real = x / y
  function (-._) (x:real) : real = - x
MARCHE Claude's avatar
MARCHE Claude committed
25

Andrei Paskevich's avatar
Andrei Paskevich committed
26
27
28
29
  predicate (<=.) (x:real) (y:real) = x <= y
  predicate (>=.) (x:real) (y:real) = x >= y
  predicate ( <.) (x:real) (y:real) = x < y
  predicate ( >.) (x:real) (y:real) = x > y
MARCHE Claude's avatar
MARCHE Claude committed
30
31

end
32
33
34
35
36

theory Abs

  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
37
  function abs(x : real) : real = if x >= 0.0 then x else -x
38

39
  lemma Abs_le: forall x y:real. abs x <= y <-> -y <= x <= y
MARCHE Claude's avatar
MARCHE Claude committed
40

41
  lemma Abs_pos: forall x:real. abs x >= 0.0
MARCHE Claude's avatar
MARCHE Claude committed
42

43
44
45
46
47
48
end

theory MinMax

  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
49
50
  function min real real : real
  function max real real : real
51

Andrei Paskevich's avatar
Andrei Paskevich committed
52
53
54
55
  axiom Max_is_ge   : forall x y:real. max x y >= x /\ max x y >= y
  axiom Max_is_some : forall x y:real. max x y = x \/ max x y = y
  axiom Min_is_le   : forall x y:real. min x y <= x /\ min x y <= y
  axiom Min_is_some : forall x y:real. min x y = x \/ min x y = y
56
57
58
59
60
61
62
63

end

theory FromInt

  use int.Int
  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
64
  function from_int int : real
65

66
67
  axiom Zero: from_int 0 = 0.0
  axiom One: from_int 1 = 1.0
68

MARCHE Claude's avatar
MARCHE Claude committed
69
  axiom Add:
70
    forall x y:int. from_int (Int.(+) x y) = from_int x + from_int y
MARCHE Claude's avatar
MARCHE Claude committed
71
  axiom Sub:
72
    forall x y:int. from_int (Int.(-) x y) = from_int x - from_int y
MARCHE Claude's avatar
MARCHE Claude committed
73
  axiom Mul:
74
    forall x y:int. from_int (Int.(*) x y) = from_int x * from_int y
MARCHE Claude's avatar
MARCHE Claude committed
75
  axiom Neg:
76
    forall x y:int. from_int (Int.(-_) (x)) = - from_int x
77

MARCHE Claude's avatar
MARCHE Claude committed
78
79
80
81
82
83
end

theory FromIntTest

  use import FromInt

84
  lemma Test1: from_int 2 = 2.0
MARCHE Claude's avatar
MARCHE Claude committed
85

86
87
88
89
end

theory Truncate

MARCHE Claude's avatar
MARCHE Claude committed
90
91
92
93
94
  use import Real
  use import FromInt

  (* truncate: rounds towards zero *)

Andrei Paskevich's avatar
Andrei Paskevich committed
95
  function truncate real : int
MARCHE Claude's avatar
MARCHE Claude committed
96
97

  axiom Truncate_int :
98
    forall i:int. truncate (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
99
100

  axiom Truncate_down_pos:
MARCHE Claude's avatar
MARCHE Claude committed
101
    forall x:real. x >= 0.0 ->
102
      from_int (truncate x) <= x < from_int (Int.(+) (truncate x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
103
104

  axiom Truncate_up_neg:
MARCHE Claude's avatar
MARCHE Claude committed
105
    forall x:real. x <= 0.0 ->
106
      from_int (Int.(-) (truncate x) 1) < x <= from_int (truncate x)
MARCHE Claude's avatar
MARCHE Claude committed
107
108

  axiom Real_of_truncate:
109
    forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0
MARCHE Claude's avatar
MARCHE Claude committed
110
111

  axiom Truncate_monotonic:
112
    forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y)
MARCHE Claude's avatar
MARCHE Claude committed
113
114

  axiom Truncate_monotonic_int1:
115
    forall x:real, i:int. x <= from_int i -> Int.(<=) (truncate x) i
MARCHE Claude's avatar
MARCHE Claude committed
116
117

  axiom Truncate_monotonic_int2:
118
    forall x:real, i:int. from_int i <= x -> Int.(<=) i (truncate x)
MARCHE Claude's avatar
MARCHE Claude committed
119
120
121

  (* roundings up and down *)

Andrei Paskevich's avatar
Andrei Paskevich committed
122
123
  function floor real : int
  function ceil real : int
MARCHE Claude's avatar
MARCHE Claude committed
124
125

  axiom Floor_int :
126
    forall i:int. floor (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
127
128

  axiom Ceil_int :
129
    forall i:int. floor (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
130
131

  axiom Floor_down:
132
    forall x:real. from_int (floor x) <= x < from_int (Int.(+) (floor x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
133
134

  axiom Ceil_up:
135
    forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x)
MARCHE Claude's avatar
MARCHE Claude committed
136
137

  axiom Floor_monotonic:
138
    forall x y:real. x <= y -> Int.(<=) (floor x) (floor y)
MARCHE Claude's avatar
MARCHE Claude committed
139
140

  axiom Ceil_monotonic:
141
    forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y)
142
143
144

end

MARCHE Claude's avatar
MARCHE Claude committed
145

MARCHE Claude's avatar
MARCHE Claude committed
146
147
148
149
theory Square

  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
150
  function sqr (x : real) : real = x * x
MARCHE Claude's avatar
MARCHE Claude committed
151

Andrei Paskevich's avatar
Andrei Paskevich committed
152
  function sqrt real : real
MARCHE Claude's avatar
MARCHE Claude committed
153

MARCHE Claude's avatar
MARCHE Claude committed
154
  axiom Sqrt_positive:
155
    forall x:real. x >= 0.0 -> sqrt x >= 0.0
MARCHE Claude's avatar
MARCHE Claude committed
156

MARCHE Claude's avatar
MARCHE Claude committed
157
  axiom Sqrt_square:
158
    forall x:real. x >= 0.0 -> sqr (sqrt x) = x
MARCHE Claude's avatar
MARCHE Claude committed
159

MARCHE Claude's avatar
MARCHE Claude committed
160
  axiom Square_sqrt:
161
    forall x:real. x >= 0.0 -> sqrt (x*x) = x
162
163
164

end

MARCHE Claude's avatar
MARCHE Claude committed
165
166
167
168
theory SquareTest

  use import Square

169
170
171
  lemma Sqrt_zero: sqrt 0.0 = 0.0
  lemma Sqrt_one: sqrt 1.0 = 1.0
  lemma Sqrt_four: sqrt 4.0 = 2.0
MARCHE Claude's avatar
MARCHE Claude committed
172
173
174

end

175
176
theory ExpLog

MARCHE Claude's avatar
MARCHE Claude committed
177
178
  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
179
  function exp real : real
MARCHE Claude's avatar
MARCHE Claude committed
180
  axiom Exp_zero : exp(0.0) = 1.0
181
  axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
MARCHE Claude's avatar
MARCHE Claude committed
182

Andrei Paskevich's avatar
Andrei Paskevich committed
183
  function e : real = exp 1.0
MARCHE Claude's avatar
MARCHE Claude committed
184

Andrei Paskevich's avatar
Andrei Paskevich committed
185
  function log real : real
186
  axiom Log_one : log 1.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
187
  axiom Log_mul :
Andrei Paskevich's avatar
Andrei Paskevich committed
188
    forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y
MARCHE Claude's avatar
MARCHE Claude committed
189

190
  axiom Log_exp: forall x:real. log (exp x) = x
MARCHE Claude's avatar
MARCHE Claude committed
191

192
  axiom Exp_log: forall x:real. x > 0.0 -> exp (log x) = x
MARCHE Claude's avatar
MARCHE Claude committed
193

Andrei Paskevich's avatar
Andrei Paskevich committed
194
195
  function log2 (x : real) : real = log x / log 2.0
  function log10 (x : real) : real = log x / log 10.0
196
197
198

end

MARCHE Claude's avatar
MARCHE Claude committed
199
200
201
202
theory ExpLogTest

  use import ExpLog

203
  lemma Log_e : log e = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
204
205
206
207

end


MARCHE Claude's avatar
MARCHE Claude committed
208
theory Power
209

MARCHE Claude's avatar
MARCHE Claude committed
210
211
212
213
  use import Real
  use import Square
  use import ExpLog

Andrei Paskevich's avatar
Andrei Paskevich committed
214
  function pow real real : real
MARCHE Claude's avatar
MARCHE Claude committed
215
216

  axiom Pow_zero_y:
217
    forall y:real. y <> 0.0 -> pow 0.0 y = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
218
219

  axiom Pow_x_zero:
220
    forall x:real. x <> 0.0 -> pow x 0.0 = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
221
222

  axiom Pow_x_one:
223
    forall x:real. pow x 1.0 = x
MARCHE Claude's avatar
MARCHE Claude committed
224
225

  axiom Pow_one_y:
226
    forall y:real. pow 1.0 y = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
227
228

  axiom Pow_x_two:
229
    forall x:real. pow x 2.0 = sqr x
MARCHE Claude's avatar
MARCHE Claude committed
230
231

  axiom Pow_half:
MARCHE Claude's avatar
MARCHE Claude committed
232
    forall x:real. x >= 0.0 -> pow x 0.5 = sqrt x
MARCHE Claude's avatar
MARCHE Claude committed
233
234

  axiom Pow_exp_log:
235
    forall x y:real. x > 0.0 -> pow x y = exp (y * log x)
MARCHE Claude's avatar
MARCHE Claude committed
236

237
238
end

MARCHE Claude's avatar
MARCHE Claude committed
239
240
241
242
theory PowerTest

  use import Power

243
  lemma Pow_2_2 : pow 2.0 2.0 = 4.0
MARCHE Claude's avatar
MARCHE Claude committed
244
245
246
247
248

end



MARCHE Claude's avatar
MARCHE Claude committed
249
(** Trigonometric functions
MARCHE Claude's avatar
MARCHE Claude committed
250
251
    [http://en.wikipedia.org/wiki/Trigonometric_function]
*)
MARCHE Claude's avatar
MARCHE Claude committed
252
theory Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
253
254
255
256
257

  use import Real
  use import Square
  use import Abs

Andrei Paskevich's avatar
Andrei Paskevich committed
258
259
  function cos real : real
  function sin real : real
MARCHE Claude's avatar
MARCHE Claude committed
260
261

  axiom Pythagorean_identity:
262
    forall x:real. sqr (cos x) + sqr (sin x) = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
263

264
265
  lemma Cos_le_one: forall x:real. abs (cos x) <= 1.0
  lemma Sin_le_one: forall x:real. abs (sin x) <= 1.0
MARCHE Claude's avatar
MARCHE Claude committed
266

267
268
  axiom Cos_0: cos 0.0 = 1.0
  axiom Sin_0: sin 0.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
269

Andrei Paskevich's avatar
Andrei Paskevich committed
270
  function pi : real
MARCHE Claude's avatar
MARCHE Claude committed
271

MARCHE Claude's avatar
more db    
MARCHE Claude committed
272
273
274
275
276
  axiom Pi_interval:
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
   < pi <
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197

277
278
  axiom Cos_pi: cos pi = -1.0
  axiom Sin_pi: sin pi = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
279

280
281
  axiom Cos_pi2: cos (0.5 * pi) = 0.0
  axiom Sin_pi2: sin (0.5 * pi) = 1.0
282

283
284
  axiom Cos_plus_pi: forall x:real. cos (x + pi) = - cos x
  axiom Sin_plus_pi: forall x:real. sin (x + pi) = - sin x
MARCHE Claude's avatar
MARCHE Claude committed
285

286
287
  axiom Cos_plus_pi2: forall x:real. cos (x + 0.5*pi) = - sin x
  axiom Sin_plus_pi2: forall x:real. sin (x + 0.5*pi) = cos x
MARCHE Claude's avatar
MARCHE Claude committed
288
289

  axiom Cos_neg:
290
    forall x:real. cos (-x) = cos x
MARCHE Claude's avatar
MARCHE Claude committed
291
  axiom Sin_neg:
292
    forall x:real. sin (-x) = - sin x
MARCHE Claude's avatar
MARCHE Claude committed
293

MARCHE Claude's avatar
MARCHE Claude committed
294
  axiom Cos_sum:
295
    forall x y:real. cos (x+y) = cos x * cos y - sin x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
296
  axiom Sin_sum:
297
    forall x y:real. sin (x+y) = sin x * cos y + cos x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
298

Andrei Paskevich's avatar
Andrei Paskevich committed
299
300
  function tan (x : real) : real = sin x / cos x
  function atan real : real
MARCHE Claude's avatar
MARCHE Claude committed
301
  axiom Tan_atan:
302
    forall x:real. tan (atan x) = x
303
304
305

end

MARCHE Claude's avatar
MARCHE Claude committed
306
307
308
309
310
311
theory TrigonometryTest

  use import Real
  use import Trigonometry
  use import Square

312
  lemma Cos_2_pi : cos (2.0 * pi) = 1.0
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
313
  lemma Sin_2_pi : sin (2.0 * pi) = 0.
314
315
  lemma Tan_pi_3 : tan (pi / 2.0) = sqrt 3.0
  lemma Atan_1   : atan 1.0 = pi / 4.0
MARCHE Claude's avatar
MARCHE Claude committed
316
317
318

end

MARCHE Claude's avatar
MARCHE Claude committed
319
(** hyperbolic functions
MARCHE Claude's avatar
MARCHE Claude committed
320
321
    [http://en.wikipedia.org/wiki/Hyperbolic_function]
*)
322
323
theory Hyperbolic

MARCHE Claude's avatar
MARCHE Claude committed
324
325
326
327
  use import Real
  use import Square
  use import ExpLog

Andrei Paskevich's avatar
Andrei Paskevich committed
328
329
330
  function sinh (x : real) : real = 0.5 * (exp x - exp (-x))
  function cosh (x : real) : real = 0.5 * (exp x + exp (-x))
  function tanh (x : real) : real = sinh x / cosh x
MARCHE Claude's avatar
MARCHE Claude committed
331

Andrei Paskevich's avatar
Andrei Paskevich committed
332
333
  function asinh (x : real) : real = log (x + sqrt (sqr x + 1.0))
  function acosh (x : real) : real
MARCHE Claude's avatar
MARCHE Claude committed
334
335
  axiom Acosh_def:
    forall x:real. x >= 1.0 -> acosh x = log (x + sqrt (sqr x - 1.0))
Andrei Paskevich's avatar
Andrei Paskevich committed
336
  function atanh (x : real) : real
MARCHE Claude's avatar
MARCHE Claude committed
337
338
  axiom Atanh_def:
    forall x:real. -1.0 < x < 1.0 -> atanh x = 0.5 * log ((1.0+x)/(1.0-x))
339
340
341

end

MARCHE Claude's avatar
MARCHE Claude committed
342
(** polar coordinates: atan2, hypot
MARCHE Claude's avatar
MARCHE Claude committed
343
344
    [http://en.wikipedia.org/wiki/Atan2]
*)
345
346
theory Polar

MARCHE Claude's avatar
MARCHE Claude committed
347
348
  use import Real
  use import Square
MARCHE Claude's avatar
MARCHE Claude committed
349
  use import Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
350

Andrei Paskevich's avatar
Andrei Paskevich committed
351
352
  function hypot (x y : real) : real = sqrt (sqr x + sqr y)
  function atan2 real real : real
MARCHE Claude's avatar
MARCHE Claude committed
353

MARCHE Claude's avatar
MARCHE Claude committed
354
  axiom X_from_polar:
355
    forall x y:real. x = hypot x y * cos (atan2 y x)
MARCHE Claude's avatar
MARCHE Claude committed
356
357

  axiom Y_from_polar:
358
    forall x y:real. y = hypot x y * sin (atan2 y x)
359
360
end