src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy
author paulson <lp15@cam.ac.uk>
Sat Apr 11 11:56:40 2015 +0100 (2015-04-11)
changeset 60017 b785d6d06430
parent 58988 6ebf918128b9
child 61586 5197a2ecb658
permissions -rw-r--r--
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
immler@58988
     1
theory Approximation_Quickcheck_Ex
immler@58988
     2
imports "../Approximation"
immler@58988
     3
begin
immler@58988
     4
immler@58988
     5
lemma
immler@58988
     6
  fixes x::real and y::real
immler@58988
     7
  shows "sin x \<le> tan x"
immler@58988
     8
  using [[quickcheck_approximation_custom_seed = 1]]
immler@58988
     9
  quickcheck[approximation, expect=counterexample]
immler@58988
    10
  oops
immler@58988
    11
immler@58988
    12
lemma "x \<le> y \<Longrightarrow> arctan y / y \<le> arctan x / x"
immler@58988
    13
  using [[quickcheck_approximation_custom_seed = 1]]
immler@58988
    14
  quickcheck[approximation, expect=counterexample]
immler@58988
    15
  oops
immler@58988
    16
immler@58988
    17
lemma "0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> arctan y / y \<le> arctan x / x"
immler@58988
    18
  using [[quickcheck_approximation_custom_seed = 1]]
immler@58988
    19
  quickcheck[approximation, expect=no_counterexample]
immler@58988
    20
  by (rule arctan_divide_mono)
immler@58988
    21
immler@58988
    22
lemma
immler@58988
    23
  fixes x::real
immler@58988
    24
  shows "exp (exp x + exp y + sin x * sin y) - 0.4 > 0 \<or> 0.98 - sin x / (sin x * sin y + 2)^2 > 0"
immler@58988
    25
  using [[quickcheck_approximation_custom_seed = 1]]
immler@58988
    26
  quickcheck[approximation, expect=counterexample, size=10, iterations=1000, verbose]
immler@58988
    27
  oops
immler@58988
    28
immler@58988
    29
lemma
immler@58988
    30
  fixes x::real
lp15@60017
    31
  shows "x > 1 \<Longrightarrow> x \<le> 2 ^ 20 * log 2 x + 1 \<and> (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
immler@58988
    32
  using [[quickcheck_approximation_custom_seed = 1]]
immler@58988
    33
  using [[quickcheck_approximation_epsilon = 0.00000001]]
immler@58988
    34
    --\<open>avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"}
immler@58988
    35
      and therefore avoids expensive failing attempts for certification\<close>
immler@58988
    36
  quickcheck[approximation, expect=counterexample, size=20]
immler@58988
    37
  oops
immler@58988
    38
immler@58988
    39
end