lib/isabelle/Why3_Real.thy

   1 theory Why3_Real
   2 imports
   3   Why3_Setup
   4   Complex_Main
   5   "HOL-Decision_Procs.Approximation"
   6 begin
   7
   8 section \<open> Real numbers and the basic unary and binary operators \<close>
   9
  10 why3_open "real/Real.xml"
  11
  12 why3_vc infix_lseqqtdef by auto
  13
  14 why3_vc Assoc by auto
  15
  16 why3_vc Unit_def_l by auto
  17
  18 why3_vc Unit_def_r by auto
  19
  20 why3_vc Inv_def_l by auto
  21
  22 why3_vc Inv_def_r by auto
  23
  24 why3_vc Comm by simp
  25
  26 why3_vc Assoc1 by simp
  27
  28 why3_vc Mul_distr_l by (simp add: algebra_simps)
  29
  30 why3_vc Mul_distr_r by (simp add: Rings.comm_semiring_class.distrib)
  31
  32 why3_vc infix_mnqtdef by auto
  33
  34 why3_vc Comm1 by auto
  35
  36 why3_vc Unitary by auto
  37
  38 why3_vc NonTrivialRing by auto
  39
  40 why3_vc Inverse by (simp add: assms)
  41
  42 why3_vc add_div by (simp add: Fields.division_ring_class.add_divide_distrib)
  43
  44 why3_vc sub_div by (simp add: Fields.division_ring_class.diff_divide_distrib)
  45
  46 why3_vc neg_div by auto
  47
  48 why3_vc assoc_mul_div by auto
  49
  50 why3_vc assoc_div_mul by auto
  51
  52 why3_vc assoc_div_div by auto
  53
  54 why3_vc Refl by auto
  55
  56 why3_vc Trans
  57   using assms
  58   by auto
  59
  60 why3_vc Antisymm
  61   using assms
  62   by auto
  63
  64 why3_vc Total by auto
  65
  66 why3_vc ZeroLessOne by auto
  67
  68 why3_vc CompatOrderAdd
  69   using assms
  70   by auto
  71
  72 why3_vc CompatOrderMult
  73   using assms
  74   by (simp add: Rings.ordered_semiring_class.mult_right_mono)
  75
  76 why3_vc infix_slqtdef by (simp add: Real.divide_real_def)
  77
  78 why3_end
  79
  80 section \<open> Alternative Infix Operators \<close>
  81
  82 why3_open "real/RealInfix.xml"
  83
  84 why3_end
  85
  86 section \<open> Absolute Value \<close>
  87
  88 why3_open "real/Abs.xml"
  89
  90 why3_vc Abs_le by auto
  91
  92 why3_vc Abs_pos by auto
  93
  94 why3_vc Abs_sum by auto
  95
  96 why3_vc absqtdef by (simp add: Real.abs_real_def)
  97
  98 why3_vc Abs_prod by (simp add: abs_mult)
  99
 100 why3_vc triangular_inequality by (simp add: Real.abs_real_def)
 101
 102 why3_end
 103
 104 section \<open> Minimum and Maximum \<close>
 105
 106 why3_open "real/MinMax.xml"
 107
 108 why3_vc Max_l
 109   using assms
 110   by auto
 111
 112 why3_vc Min_r
 113   using assms
 114   by auto
 115
 116 why3_vc maxqtdef by auto
 117
 118 why3_vc minqtdef by auto
 119
 120 why3_vc Max_comm by auto
 121
 122 why3_vc Min_comm by auto
 123
 124 why3_vc Max_assoc by auto
 125
 126 why3_vc Min_assoc by auto
 127
 128 why3_end
 129
 130 section \<open> Injection of integers into reals \<close>
 131
 132 why3_open "real/FromInt.xml"
 133   constants
 134     from_int = of_int
 135
 136 why3_vc Add by auto
 137
 138 why3_vc Mul by auto
 139
 140 why3_vc Neg by auto
 141
 142 why3_vc One by auto
 143
 144 why3_vc Sub by auto
 145
 146 why3_vc Zero by auto
 147
 148 why3_vc Monotonic using assms by auto
 149
 150 why3_vc Injective using assms by auto
 151
 152 why3_end
 153
 154 section \<open> Various truncation functions \<close>
 155
 156 (* truncate: rounds towards zero *)
 157
 158 definition truncate :: "real \<Rightarrow> int" where
 159   "truncate x = (if x \<ge> 0 then floor x else ceiling x)"
 160
 161 why3_open "real/Truncate.xml"
 162   constants
 163   truncate = truncate
 164   floor = floor
 165   ceil = ceiling
 166
 167 subsection \<open> Roundings up and down \<close>
 168
 169 why3_vc Ceil_up
 170   by (simp_all add: ceiling_correct)
 171
 172 why3_vc Ceil_int by auto
 173
 174 why3_vc Floor_int by auto
 175
 176 why3_vc Floor_down
 177   by (simp_all add: floor_correct [simplified])
 178
 179 why3_vc Ceil_monotonic
 180   using assms
 181   by (simp add:ceiling_mono)
 182
 183 why3_vc Floor_monotonic
 184   using assms
 185   by (simp add:floor_mono)
 186
 187 subsection \<open> Rounding towards zero \<close>
 188
 189 why3_vc Real_of_truncate
 190   using floor_correct [of x] ceiling_correct [of x]
 191   by (simp_all add: truncate_def del: of_int_floor_le le_of_int_ceiling)
 192
 193 why3_vc Truncate_int by (simp add: truncate_def)
 194
 195 why3_vc Truncate_up_neg
 196   using assms ceiling_correct [of x]
 197   by (simp_all add: truncate_def)
 198
 199 why3_vc Truncate_down_pos
 200   using assms floor_correct [of x]
 201   by (simp_all add: truncate_def)
 202
 203 why3_vc Truncate_monotonic
 204   using assms
 205   unfolding truncate_def
 206   by (simp add: floor_mono ceiling_mono order_trans [of "\<lceil>x\<rceil>" 0 "\<lfloor>y\<rfloor>"])
 207
 208 why3_vc Truncate_monotonic_int1
 209   using assms
 210   by (simp add: truncate_def floor_le_iff ceiling_le_iff)
 211
 212 why3_vc Truncate_monotonic_int2
 213   using assms
 214   by (simp add: truncate_def le_floor_iff le_ceiling_iff)
 215
 216 why3_end
 217
 218 section \<open> Square and Square Root \<close>
 219
 220 why3_open "real/Square.xml"
 221   constants
 222     sqrt = sqrt
 223
 224 why3_vc Sqrt_le
 225   using assms
 226   by auto
 227
 228 why3_vc Sqrt_mul by (simp add: NthRoot.real_sqrt_mult)
 229
 230 why3_vc Sqrt_square
 231   using assms
 232   by (simp add: sqr_def)
 233
 234 why3_vc Square_sqrt
 235   using assms
 236   by auto
 237
 238 why3_vc Sqrt_positive
 239   using assms
 240   by auto
 241
 242 why3_end
 243
 244 section \<open> Exponential and Logarithm \<close>
 245
 246 why3_open "real/ExpLog.xml"
 247   constants
 248     exp = exp
 249     log = ln
 250
 251 why3_vc Exp_log
 252   using assms
 253   by auto
 254
 255 why3_vc Exp_sum by (simp add: Transcendental.exp_add)
 256
 257 why3_vc exp_increasing
 258   using assms by auto
 259
 260 why3_vc exp_positive
 261   by auto
 262
 263 why3_vc exp_inv
 264   by (simp add: exp_minus)
 265
 266 why3_vc exp_sum_opposite
 267   by (simp add: exp_minus exp_plus_inverse_exp)
 268
 269 why3_vc Log_exp by auto
 270
 271 why3_vc Log_mul
 272   using assms
 273   by (simp add: Transcendental.ln_mult)
 274
 275 why3_vc Log_one by auto
 276
 277 why3_vc Exp_zero by auto
 278
 279 why3_vc log_increasing
 280   using H1 H2 by auto
 281
 282 why3_vc log2_increasing
 283   using H1 H2 divide_real_def log2_def by auto
 284
 285 why3_vc log10_increasing
 286   using H1 H2 divide_real_def log10_def by force
 287
 288 why3_end
 289
 290 section \<open> Power of a real to an integer \<close>
 291
 292 (* TODO: clones int.Exponentiation which is not yet realized *)
 293
 294 why3_open "real/PowerInt.xml"
 295
 296 why3_vc Power_0 by auto
 297
 298 why3_vc Power_1 by auto
 299
 300 why3_vc Power_s
 301   using assms
 302   by (simp add: nat_add_distrib)
 303
 304 why3_vc Power_sum
 305   using assms
 306   by (simp add: nat_add_distrib power_add)
 307
 308 why3_vc Pow_ge_one using assms by auto
 309
 310 why3_vc Power_mult
 311   using assms
 312   by (simp add: nat_mult_distrib power_mult)
 313
 314 why3_vc Power_comm1 by simp
 315
 316 why3_vc Power_comm2 by (simp add: semiring_normalization_rules(30))
 317
 318 why3_vc Power_s_alt
 319 proof -
 320   have "nat n = Suc (nat (n - 1))" using assms by auto
 321   then show ?thesis by simp
 322 qed
 323
 324 why3_end
 325
 326 section \<open> Power of a real to a real exponent \<close>
 327
 328 (* TODO: no power to a real exponent in Isabelle? *)
 329
 330 section \<open> Trigonometric Functions \<close>
 331
 332 abbreviation (input)
 333   "why3_divide \<equiv> divide"
 334
 335 why3_open "real/Trigonometry.xml"
 336   constants
 337     cos = cos
 338     sin = sin
 339     pi = pi
 340     atan = arctan
 341
 342 why3_vc Cos_0 by auto
 343
 344 why3_vc Sin_0 by auto
 345
 346 why3_vc Cos_pi by auto
 347
 348 why3_vc Sin_pi by auto
 349
 350 why3_vc Cos_neg by auto
 351
 352 why3_vc Cos_pi2 by auto
 353
 354 why3_vc Cos_sum by (simp add: Transcendental.cos_add)
 355
 356 why3_vc Sin_neg by auto
 357
 358 why3_vc Sin_pi2 by auto
 359
 360 why3_vc Sin_sum by (simp add: Transcendental.sin_add)
 361
 362 why3_vc tanqtdef by (simp add: Transcendental.tan_def)
 363
 364 why3_vc Tan_atan by (simp add: Transcendental.tan_arctan)
 365
 366 why3_vc Cos_le_one by auto
 367
 368 why3_vc Sin_le_one by auto
 369
 370 why3_vc Cos_plus_pi by auto
 371
 372 why3_vc Pi_double_precision_bounds
 373 proof -
 374   have "884279719003555 / 281474976710656 < pi"
 375     by (approximation 57)
 376   then show ?C1 by simp
 377   have "pi < 7074237752028441 / 2251799813685248"
 378     by (approximation 55)
 379   then show ?C2 by simp
 380 qed
 381
 382 why3_vc Sin_plus_pi by auto
 383
 384 why3_vc Cos_plus_pi2 by (simp add: Transcendental.minus_sin_cos_eq)
 385
 386 why3_vc Sin_plus_pi2 by (simp add: sin_add)
 387
 388 why3_vc Pythagorean_identity
 389   by (simp add: sqr_def)
 390
 391 why3_end
 392
 393 section \<open> Hyperbolic Functions \<close>
 394
 395 (* TODO: missing acosh *)
 396
 397 section \<open> Polar Coordinates \<close>
 398
 399 (* TODO: missing atan2 *)
 400
 401 end