Why3_Real.thy 6.3 KB
Newer Older
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
theory Why3_Real
imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation" Why3_Setup
begin

section {* Real numbers and the basic unary and binary operators *}

why3_open "real/Real.xml"

why3_vc infix_lseq_def by auto

why3_vc Assoc by auto

why3_vc Unit_def_l by auto

why3_vc Unit_def_r by auto

why3_vc Inv_def_l by auto

why3_vc Inv_def_r by auto

why3_vc Comm by simp

why3_vc Assoc1 by simp

why3_vc Mul_distr_l by (simp add: Fields.linordered_field_class.sign_simps)

why3_vc Mul_distr_r by (simp add: Rings.comm_semiring_class.distrib)

why3_vc infix_mn_def by auto

why3_vc Comm1 by auto

why3_vc Unitary by auto

why3_vc NonTrivialRing by auto

why3_vc Inverse by (simp add: assms)

why3_vc add_div by (simp add: Fields.division_ring_class.add_divide_distrib)

why3_vc sub_div by (simp add: Fields.division_ring_class.diff_divide_distrib)

why3_vc neg_div by auto

why3_vc assoc_mul_div by auto

why3_vc assoc_div_mul by auto

why3_vc assoc_div_div by auto

why3_vc Refl by auto

why3_vc Trans
  using assms
  by auto

why3_vc Antisymm
  using assms
  by auto

why3_vc Total by auto

why3_vc ZeroLessOne by auto

why3_vc CompatOrderAdd
  using assms
  by auto

why3_vc CompatOrderMult
  using assms
  by (simp add: Rings.ordered_semiring_class.mult_right_mono)

why3_vc infix_sl_def by (simp add: Real.divide_real_def)

why3_end

section {* Alternative Infix Operators *}

why3_open "real/RealInfix.xml"

why3_end

section {* Absolute Value *}

why3_open "real/Abs.xml"

why3_vc Abs_le by auto

why3_vc Abs_pos by auto

why3_vc Abs_sum by auto

why3_vc abs_def by (simp add: Real.abs_real_def)

why3_vc Abs_prod by (simp add: Rings.linordered_idom_class.abs_mult)

why3_vc triangular_inequality by (simp add: Real.abs_real_def)

why3_end

section {* Minimum and Maximum *}

why3_open "real/MinMax.xml"

why3_vc Max_l
  using assms
  by auto

why3_vc Min_r
  using assms
  by auto

why3_vc max_def by auto

why3_vc min_def by auto

why3_vc Max_comm by auto

why3_vc Min_comm by auto

why3_vc Max_assoc by auto

why3_vc Min_assoc by auto

why3_end

section {* Injection of integers into reals *}

why3_open "real/FromInt.xml"
  constants
    from_int = of_int

why3_vc Add by auto

why3_vc Mul by auto

why3_vc Neg by auto

why3_vc One by auto

why3_vc Sub by auto

why3_vc Zero by auto

why3_end

section {* Various truncation functions *}

(* truncate: rounds towards zero *)

definition truncate :: "real \<Rightarrow> int" where
  "truncate x = (if x \<ge> 0 then floor x else ceiling x)"

why3_open "real/Truncate.xml"
  constants
  truncate = truncate
  floor = floor
  ceil = ceiling

subsection {* Roundings up and down *}

why3_vc Ceil_up
163
  by (simp_all add: ceiling_correct)
164
165
166
167
168
169

why3_vc Ceil_int by auto

why3_vc Floor_int by auto

why3_vc Floor_down
170
  by (simp_all add: floor_correct [simplified])
171
172
173
174
175
176
177
178
179
180
181
182

why3_vc Ceil_monotonic
  using assms
  by (simp add:ceiling_mono)

why3_vc Floor_monotonic
  using assms
  by (simp add:floor_mono)

subsection {* Rounding towards zero *}

why3_vc Real_of_truncate
183
184
  using floor_correct [of x] ceiling_correct [of x]
  by (simp_all add: truncate_def)
185
186
187
188

why3_vc Truncate_int by (simp add:truncate_def)

why3_vc Truncate_up_neg
189
190
  using assms ceiling_correct [of x]
  by (simp_all add: truncate_def)
191
192

why3_vc Truncate_down_pos
193
194
  using assms floor_correct [of x]
  by (simp_all add: truncate_def)
195
196

why3_vc Truncate_monotonic
197
  using assms
198
  unfolding truncate_def
199
  by (simp add: floor_mono ceiling_mono order_trans [of "\<lceil>x\<rceil>" 0 "\<lfloor>y\<rfloor>"])
200
201

why3_vc Truncate_monotonic_int1
202
203
  using assms
  by (simp add: truncate_def floor_le_iff ceiling_le_iff)
204
205

why3_vc Truncate_monotonic_int2
206
207
  using assms
  by (simp add: truncate_def le_floor_iff le_ceiling_iff)
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272

why3_end

section {* Square and Square Root *}

why3_open "real/Square.xml"
  constants
    sqrt = sqrt

why3_vc Sqrt_le
  using assms
  by auto

why3_vc Sqrt_mul by (simp add: NthRoot.real_sqrt_mult)

why3_vc Sqrt_square
  using assms
  by (simp add: sqr_def)

why3_vc Square_sqrt
  using assms
  by auto

why3_vc Sqrt_positive
  using assms
  by auto

why3_end

section {* Exponential and Logarithm *}

why3_open "real/ExpLog.xml"
  constants
    exp = exp
    log = ln

why3_vc Exp_log
  using assms
  by auto

why3_vc Exp_sum by (simp add: Transcendental.exp_add)

why3_vc Log_exp by auto

why3_vc Log_mul
  using assms
  by (simp add: Transcendental.ln_mult)

why3_vc Log_one by auto

why3_vc Exp_zero by auto

why3_end

section {* Power of a real to an integer *}

(* TODO: clones int.Exponentiation which is not yet realized *)

why3_open "real/PowerInt.xml"

why3_vc Power_0 by auto

why3_vc Power_1 by auto

why3_vc Power_s
273
274
  using assms
  by (simp add: nat_add_distrib)
275
276

why3_vc Power_sum
277
278
  using assms
  by (simp add: nat_add_distrib power_add)
279
280
281
282

why3_vc Pow_ge_one using assms by auto

why3_vc Power_mult
283
284
  using assms
  by (simp add: nat_mult_distrib power_mult)
285
286
287
288
289

why3_vc Power_mult2 by (simp only:Power.comm_monoid_mult_class.power_mult_distrib)

why3_vc Power_s_alt
proof -
290
291
  have "nat n = Suc (nat (n - 1))" using assms by auto
  then show ?thesis by simp
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
qed

why3_end

section {* Power of a real to a real exponent *}

(* TODO: no power to a real exponent in Isabelle? *)

section {* Trigonometric Functions *}

why3_open "real/Trigonometry.xml"
  constants
    cos = cos
    sin = sin
    pi = pi
    atan = arctan

why3_vc Cos_0 by auto

why3_vc Sin_0 by auto

why3_vc Cos_pi by auto

why3_vc Sin_pi by auto

why3_vc Cos_neg by auto

why3_vc Cos_pi2 by auto

why3_vc Cos_sum by (simp add: Transcendental.cos_add)

why3_vc Sin_neg by auto

why3_vc Sin_pi2 by auto

why3_vc Sin_sum by (simp add: Transcendental.sin_add)

why3_vc tan_def by (simp add: Transcendental.tan_def)

why3_vc Tan_atan by (simp add: Transcendental.tan_arctan)

why3_vc Cos_le_one by auto

why3_vc Sin_le_one by auto

why3_vc Cos_plus_pi by auto

339
why3_vc Pi_double_precision_bounds
340
proof -
341
342
  have "7074237752028440 / 2251799813685248 < pi"
    by (approximation 57)
343
  then show ?C1 by simp
344
345
  have "pi < 7074237752028441 / 2251799813685248"
    by (approximation 55)
346
  then show ?C2 by simp
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
qed

why3_vc Sin_plus_pi by auto

why3_vc Cos_plus_pi2 by (simp add: Transcendental.minus_sin_cos_eq)

why3_vc Sin_plus_pi2 by (simp add: sin_add)

why3_vc Pythagorean_identity
  by (simp add: sqr_def)

why3_end

section {* Hyperbolic Functions *}

(* TODO: missing acosh *)

section {* Polar Coordinates *}

(* TODO: missing atan2 *)

end