real.why 7.48 KB
Newer Older
1
2

theory Real 
MARCHE Claude's avatar
MARCHE Claude committed
3

4
5
6
7
8
9
  logic zero : real = 0.0
  logic one  : real = 1.0
  
  clone export algebra.Field with 
     type t = real, logic zero = zero, logic one = one

MARCHE Claude's avatar
MARCHE Claude committed
10
  logic (< )(real, real)
11
12
13
  logic (<=)(x:real, y:real) = x < y or x = y
  logic (> )(x:real, y:real) = y < x
  logic (>=)(x:real, y:real) = y <= x
14
  
15
16
  clone export relations.TotalOrder with
    type t = real, logic rel = (<=)
17
18
19
20
21
22
23

end 

theory Abs

  use import Real

24
  logic abs(x : real) : real = if x >= 0.0 then x else -x
25

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

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

30
31
32
33
34
35
36
37
38
end

theory MinMax

  use import Real

  logic min(real,real) : real
  logic max(real,real) : real

39
40
41
42
  axiom Max_is_ge   : forall x y:real. max x y >= x and max x y >= y
  axiom Max_is_some : forall x y:real. max x y = x or max x y = y
  axiom Min_is_le   : forall x y:real. min x y <= x and min x y <= y
  axiom Min_is_some : forall x y:real. min x y = x or min x y = y
43
44
45
46
47
48
49
50
51
52

end

theory FromInt

  use int.Int
  use import Real

  logic from_int(int) : real

53
54
  axiom Zero: from_int 0 = 0.0
  axiom One: from_int 1 = 1.0
55
56

  axiom Add: 
57
    forall x y:int. from_int (Int.(+) x y) = from_int x + from_int y
58
  axiom Sub: 
59
    forall x y:int. from_int (Int.(-) x y) = from_int x - from_int y
60
  axiom Mul: 
61
    forall x y:int. from_int (Int.(*) x y) = from_int x * from_int y
62
  axiom Neg: 
63
    forall x y:int. from_int (Int.(-_) (x)) = - from_int x
64

MARCHE Claude's avatar
MARCHE Claude committed
65
66
67
68
69
70
end

theory FromIntTest

  use import FromInt

71
  lemma Test1: from_int 2 = 2.0
MARCHE Claude's avatar
MARCHE Claude committed
72

73
74
75
76
end

theory Truncate

MARCHE Claude's avatar
MARCHE Claude committed
77
78
79
80
81
82
83
84
  use import Real
  use import FromInt

  (* truncate: rounds towards zero *)

  logic truncate(real) : int

  axiom Truncate_int :
85
    forall i:int. truncate (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
86
87
88

  axiom Truncate_down_pos:
    forall x:real. x >= 0.0 -> 
89
      from_int (truncate x) <= x < from_int (Int.(+) (truncate x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
90
91
92

  axiom Truncate_up_neg:
    forall x:real. x <= 0.0 -> 
93
      from_int (Int.(-) (truncate x) 1) < x <= from_int (truncate x)
MARCHE Claude's avatar
MARCHE Claude committed
94
95

  axiom Real_of_truncate:
96
    forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0
MARCHE Claude's avatar
MARCHE Claude committed
97
98

  axiom Truncate_monotonic:
99
    forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y)
MARCHE Claude's avatar
MARCHE Claude committed
100
101

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

  axiom Truncate_monotonic_int2:
105
    forall x:real, i:int. from_int i <= x -> Int.(<=) i (truncate x)
MARCHE Claude's avatar
MARCHE Claude committed
106
107
108
109
110
111
112

  (* roundings up and down *)

  logic floor(real) : int
  logic ceil(real) : int

  axiom Floor_int :
113
    forall i:int. floor (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
114
115

  axiom Ceil_int :
116
    forall i:int. floor (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
117
118

  axiom Floor_down:
119
    forall x:real. from_int (floor x) <= x < from_int (Int.(+) (floor x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
120
121

  axiom Ceil_up:
122
    forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x)
MARCHE Claude's avatar
MARCHE Claude committed
123
124

  axiom Floor_monotonic:
125
    forall x y:real. x <= y -> Int.(<=) (floor x) (floor y)
MARCHE Claude's avatar
MARCHE Claude committed
126
127

  axiom Ceil_monotonic:
128
    forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y)
129
130
131

end

MARCHE Claude's avatar
MARCHE Claude committed
132

MARCHE Claude's avatar
MARCHE Claude committed
133
134
135
136
137
138
139
140
141
theory Square

  use import Real

  logic sqr(x:real):real = x * x

  logic sqrt(real):real

  axiom Sqrt_positive: 
142
    forall x:real. x >= 0.0 -> sqrt x >= 0.0
MARCHE Claude's avatar
MARCHE Claude committed
143
144

  axiom Sqrt_square:  
145
    forall x:real. x >= 0.0 -> sqr (sqrt x) = x
MARCHE Claude's avatar
MARCHE Claude committed
146
147

  axiom Square_sqrt: 
148
    forall x:real. x >= 0.0 -> sqrt (x*x) = x
149
150
151

end

MARCHE Claude's avatar
MARCHE Claude committed
152
153
154
155
theory SquareTest

  use import Square

156
157
158
  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
159
160
161

end

162
163
theory ExpLog

MARCHE Claude's avatar
MARCHE Claude committed
164
165
166
167
  use import Real

  logic exp(real) : real
  axiom Exp_zero : exp(0.0) = 1.0
168
  axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
MARCHE Claude's avatar
MARCHE Claude committed
169

170
  logic e : real = exp 1.0
MARCHE Claude's avatar
MARCHE Claude committed
171

MARCHE Claude's avatar
MARCHE Claude committed
172
  logic log(real) : real
173
  axiom Log_one : log 1.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
174
  axiom Log_mul : 
175
    forall x y:real. x > 0.0 and y > 0.0 -> log (x*y) = log x + log y
MARCHE Claude's avatar
MARCHE Claude committed
176

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

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

181
182
  logic log2(x:real) : real = log x / log 2.0
  logic log10(x:real) : real = log x / log 10.0
183
184
185

end

MARCHE Claude's avatar
MARCHE Claude committed
186
187
188
189
theory ExpLogTest

  use import ExpLog

190
  lemma Log_e : log e = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
191
192
193
194

end


195
196
theory Power 

MARCHE Claude's avatar
MARCHE Claude committed
197
198
199
200
201
202
203
  use import Real
  use import Square
  use import ExpLog

  logic pow(real,real) : real

  axiom Pow_zero_y:
204
    forall y:real. y <> 0.0 -> pow 0.0 y = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
205
206

  axiom Pow_x_zero:
207
    forall x:real. x <> 0.0 -> pow x 0.0 = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
208
209

  axiom Pow_x_one:
210
    forall x:real. pow x 1.0 = x
MARCHE Claude's avatar
MARCHE Claude committed
211
212

  axiom Pow_one_y:
213
    forall y:real. pow 1.0 y = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
214
215

  axiom Pow_x_two:
216
    forall x:real. pow x 2.0 = sqr x
MARCHE Claude's avatar
MARCHE Claude committed
217
218

  axiom Pow_half:
219
    forall x:real. x >= 0.0 -> pow x 0.5 = sqrt x  
MARCHE Claude's avatar
MARCHE Claude committed
220
221

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

224
225
end

MARCHE Claude's avatar
MARCHE Claude committed
226
227
228
229
theory PowerTest

  use import Power

230
  lemma Pow_2_2 : pow 2.0 2.0 = 4.0
MARCHE Claude's avatar
MARCHE Claude committed
231
232
233
234
235

end



MARCHE Claude's avatar
MARCHE Claude committed
236
237
238
(** Trigonometric functions 
    [http://en.wikipedia.org/wiki/Trigonometric_function]
*)
MARCHE Claude's avatar
MARCHE Claude committed
239
theory Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
240
241
242
243
244
245
246
247
248

  use import Real
  use import Square
  use import Abs

  logic cos(real) : real
  logic sin(real) : real

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

251
252
  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
253

254
255
  axiom Cos_0: cos 0.0 = 1.0
  axiom Sin_0: sin 0.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
256
257
258

  logic pi : real

MARCHE Claude's avatar
more db    
MARCHE Claude committed
259
260
261
262
263
  axiom Pi_interval:
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
   < pi <
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197

264
265
  axiom Cos_pi: cos pi = -1.0
  axiom Sin_pi: sin pi = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
266

267
268
  axiom Cos_pi2: cos (0.5 * pi) = 0.0
  axiom Sin_pi2: sin (0.5 * pi) = 1.0
269

270
271
  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
272

273
274
  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
275
276

  axiom Cos_neg:
277
    forall x:real. cos (-x) = cos x
MARCHE Claude's avatar
MARCHE Claude committed
278
  axiom Sin_neg:
279
    forall x:real. sin (-x) = - sin x
MARCHE Claude's avatar
MARCHE Claude committed
280
281
 
  axiom Cos_sum:
282
    forall x y:real. cos (x+y) = cos x * cos y - sin x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
283
  axiom Sin_sum:
284
    forall x y:real. sin (x+y) = sin x * cos y + cos x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
285

286
  logic tan(x:real) : real = sin x / cos x
MARCHE Claude's avatar
MARCHE Claude committed
287
288
  logic atan(real) : real
  axiom Tan_atan:
289
    forall x:real. tan (atan x) = x
290
291
292

end

MARCHE Claude's avatar
MARCHE Claude committed
293
294
295
296
297
298
theory TrigonometryTest

  use import Real
  use import Trigonometry
  use import Square

299
300
301
302
  lemma Cos_2_pi : cos (2.0 * pi) = 1.0
  lemma Sin_2_pi : cos (2.0 * pi) = 0.
  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
303
304
305

end

MARCHE Claude's avatar
MARCHE Claude committed
306
307
308
(** hyperbolic functions 
    [http://en.wikipedia.org/wiki/Hyperbolic_function]
*)
309
310
theory Hyperbolic

MARCHE Claude's avatar
MARCHE Claude committed
311
312
313
314
  use import Real
  use import Square
  use import ExpLog

315
316
317
  logic sinh(x:real) : real = 0.5 * (exp x - exp (-x))
  logic cosh(x:real) : real = 0.5 * (exp x + exp (-x))
  logic tanh(x:real) : real = sinh x / cosh x
MARCHE Claude's avatar
MARCHE Claude committed
318

319
  logic arsinh(x:real) : real = log (x + sqrt (sqr x + 1.0))
MARCHE Claude's avatar
MARCHE Claude committed
320
321
  logic arcosh(x:real) : real
  axiom Arcosh_def:
322
    forall x:real. x >= 1.0 -> arcosh x = log (x + sqrt (sqr x - 1.0))
MARCHE Claude's avatar
MARCHE Claude committed
323
324
  logic artanh(x:real) : real
  axiom Artanh_def:
325
    forall x:real. -1.0 < x < 1.0 -> artanh x = 0.5 * log ((1.0+x)/(1.0-x))
326
327
328

end

MARCHE Claude's avatar
MARCHE Claude committed
329
330
331
(** polar coordinates: atan2, hypot 
    [http://en.wikipedia.org/wiki/Atan2]
*)
332
333
theory Polar

MARCHE Claude's avatar
MARCHE Claude committed
334
335
  use import Real
  use import Square
MARCHE Claude's avatar
MARCHE Claude committed
336
  use import Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
337

338
  logic hypot(x:real,y:real) : real = sqrt (sqr x + sqr y)
MARCHE Claude's avatar
MARCHE Claude committed
339
  logic atan2(real,real) : real
340
 
MARCHE Claude's avatar
MARCHE Claude committed
341
  axiom X_from_polar:
342
    forall x y:real. x = hypot x y * cos (atan2 y x)
MARCHE Claude's avatar
MARCHE Claude committed
343
344

  axiom Y_from_polar:
345
    forall x y:real. y = hypot x y * sin (atan2 y x)
346
347
end