author | wenzelm |
Mon, 15 Feb 2016 14:55:44 +0100 | |
changeset 62337 | d3996d5873dd |
parent 61586 | 5197a2ecb658 |
child 67443 | 3abf6a722518 |
permissions | -rw-r--r-- |
58988 | 1 |
theory Approximation_Quickcheck_Ex |
2 |
imports "../Approximation" |
|
3 |
begin |
|
4 |
||
5 |
lemma |
|
6 |
fixes x::real and y::real |
|
7 |
shows "sin x \<le> tan x" |
|
8 |
using [[quickcheck_approximation_custom_seed = 1]] |
|
9 |
quickcheck[approximation, expect=counterexample] |
|
10 |
oops |
|
11 |
||
12 |
lemma "x \<le> y \<Longrightarrow> arctan y / y \<le> arctan x / x" |
|
13 |
using [[quickcheck_approximation_custom_seed = 1]] |
|
14 |
quickcheck[approximation, expect=counterexample] |
|
15 |
oops |
|
16 |
||
17 |
lemma "0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> arctan y / y \<le> arctan x / x" |
|
18 |
using [[quickcheck_approximation_custom_seed = 1]] |
|
19 |
quickcheck[approximation, expect=no_counterexample] |
|
20 |
by (rule arctan_divide_mono) |
|
21 |
||
22 |
lemma |
|
23 |
fixes x::real |
|
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" |
|
25 |
using [[quickcheck_approximation_custom_seed = 1]] |
|
26 |
quickcheck[approximation, expect=counterexample, size=10, iterations=1000, verbose] |
|
27 |
oops |
|
28 |
||
29 |
lemma |
|
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 | 32 |
using [[quickcheck_approximation_custom_seed = 1]] |
33 |
using [[quickcheck_approximation_epsilon = 0.00000001]] |
|
61586 | 34 |
\<comment>\<open>avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"} |
58988 | 35 |
and therefore avoids expensive failing attempts for certification\<close> |
36 |
quickcheck[approximation, expect=counterexample, size=20] |
|
37 |
oops |
|
38 |
||
39 |
end |