src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy
author wenzelm
Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337 d3996d5873dd
parent 61586 5197a2ecb658
child 67443 3abf6a722518
permissions -rw-r--r--
proper syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58988
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
     1
theory Approximation_Quickcheck_Ex
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
     2
imports "../Approximation"
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
     3
begin
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
     4
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
     5
lemma
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
     6
  fixes x::real and y::real
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
     7
  shows "sin x \<le> tan x"
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
     8
  using [[quickcheck_approximation_custom_seed = 1]]
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
     9
  quickcheck[approximation, expect=counterexample]
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    10
  oops
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    11
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    12
lemma "x \<le> y \<Longrightarrow> arctan y / y \<le> arctan x / x"
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    13
  using [[quickcheck_approximation_custom_seed = 1]]
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    14
  quickcheck[approximation, expect=counterexample]
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    15
  oops
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    16
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    17
lemma "0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> arctan y / y \<le> arctan x / x"
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    18
  using [[quickcheck_approximation_custom_seed = 1]]
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    19
  quickcheck[approximation, expect=no_counterexample]
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    20
  by (rule arctan_divide_mono)
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    21
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    22
lemma
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    23
  fixes x::real
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    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"
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    25
  using [[quickcheck_approximation_custom_seed = 1]]
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    26
  quickcheck[approximation, expect=counterexample, size=10, iterations=1000, verbose]
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    27
  oops
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    28
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    29
lemma
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    30
  fixes x::real
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 58988
diff changeset
    31
  shows "x > 1 \<Longrightarrow> x \<le> 2 ^ 20 * log 2 x + 1 \<and> (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
58988
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    32
  using [[quickcheck_approximation_custom_seed = 1]]
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    33
  using [[quickcheck_approximation_epsilon = 0.00000001]]
61586
5197a2ecb658 isabelle update_cartouches -c -t;
wenzelm
parents: 60017
diff changeset
    34
    \<comment>\<open>avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"}
58988
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    35
      and therefore avoids expensive failing attempts for certification\<close>
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    36
  quickcheck[approximation, expect=counterexample, size=20]
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    37
  oops
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    38
6ebf918128b9 added quickcheck[approximation]
immler
parents:
diff changeset
    39
end