Why3_Real.thy.2016-1 6.41 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
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)

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

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

145 146
why3_vc Monotonic using assms by auto

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

why3_vc Ceil_int by auto

why3_vc Floor_int by auto

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

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

Stefan Berghofer's avatar
Stefan Berghofer committed
188
why3_vc Truncate_int by (simp add: truncate_def)
189 190

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

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

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

why3_vc Truncate_monotonic_int1
204 205
  using assms
  by (simp add: truncate_def floor_le_iff ceiling_le_iff)
206 207

why3_vc Truncate_monotonic_int2
208 209
  using assms
  by (simp add: truncate_def le_floor_iff le_ceiling_iff)
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 273 274

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
275 276
  using assms
  by (simp add: nat_add_distrib)
277 278

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

why3_vc Pow_ge_one using assms by auto

why3_vc Power_mult
285 286
  using assms
  by (simp add: nat_mult_distrib power_mult)
287

288 289 290
why3_vc Power_comm1 by simp

why3_vc Power_comm2 by (simp add: semiring_normalization_rules(30))
291 292 293

why3_vc Power_s_alt
proof -
294 295
  have "nat n = Suc (nat (n - 1))" using assms by auto
  then show ?thesis by simp
296 297 298 299 300 301 302 303 304 305
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
306 307 308
abbreviation (input)
  "why3_divide \<equiv> divide"

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

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