Why3_Real.thy.2017 6.41 KB
Newer Older
1
theory Why3_Real
Stefan Berghofer's avatar
Stefan Berghofer committed
2 3 4 5
imports
  Why3_Setup
  Complex_Main
  "HOL-Decision_Procs.Approximation"
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
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)

98
why3_vc Abs_prod by (simp add: abs_mult)
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

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

148 149
why3_vc Monotonic using assms by auto

150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
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
168
  by (simp_all add: ceiling_correct)
169 170 171 172 173 174

why3_vc Ceil_int by auto

why3_vc Floor_int by auto

why3_vc Floor_down
175
  by (simp_all add: floor_correct [simplified])
176 177 178 179 180 181 182 183 184 185 186 187

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
188
  using floor_correct [of x] ceiling_correct [of x]
Stefan Berghofer's avatar
Stefan Berghofer committed
189
  by (simp_all add: truncate_def del: of_int_floor_le le_of_int_ceiling)
190

Stefan Berghofer's avatar
Stefan Berghofer committed
191
why3_vc Truncate_int by (simp add: truncate_def)
192 193

why3_vc Truncate_up_neg
194 195
  using assms ceiling_correct [of x]
  by (simp_all add: truncate_def)
196 197

why3_vc Truncate_down_pos
198 199
  using assms floor_correct [of x]
  by (simp_all add: truncate_def)
200 201

why3_vc Truncate_monotonic
202
  using assms
203
  unfolding truncate_def
204
  by (simp add: floor_mono ceiling_mono order_trans [of "\<lceil>x\<rceil>" 0 "\<lfloor>y\<rfloor>"])
205 206

why3_vc Truncate_monotonic_int1
207 208
  using assms
  by (simp add: truncate_def floor_le_iff ceiling_le_iff)
209 210

why3_vc Truncate_monotonic_int2
211 212
  using assms
  by (simp add: truncate_def le_floor_iff le_ceiling_iff)
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 273 274 275 276 277

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
278 279
  using assms
  by (simp add: nat_add_distrib)
280 281

why3_vc Power_sum
282 283
  using assms
  by (simp add: nat_add_distrib power_add)
284 285 286 287

why3_vc Pow_ge_one using assms by auto

why3_vc Power_mult
288 289
  using assms
  by (simp add: nat_mult_distrib power_mult)
290

291 292 293
why3_vc Power_comm1 by simp

why3_vc Power_comm2 by (simp add: semiring_normalization_rules(30))
294 295 296

why3_vc Power_s_alt
proof -
297 298
  have "nat n = Suc (nat (n - 1))" using assms by auto
  then show ?thesis by simp
299 300 301 302 303 304 305 306 307 308
qed

why3_end

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

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

section {* Trigonometric Functions *}

Stefan Berghofer's avatar
Stefan Berghofer committed
309 310 311
abbreviation (input)
  "why3_divide \<equiv> divide"

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 339 340 341 342 343 344 345 346 347 348
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

349
why3_vc Pi_double_precision_bounds
350
proof -
351 352
  have "7074237752028440 / 2251799813685248 < pi"
    by (approximation 57)
353
  then show ?C1 by simp
354 355
  have "pi < 7074237752028441 / 2251799813685248"
    by (approximation 55)
356
  then show ?C2 by simp
357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378
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