author | immler |
Wed, 21 Sep 2016 17:56:25 +0200 | |
changeset 63931 | f17a1c60ac39 |
parent 63263 | c6c95d64607a |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
30443
873fa77be5f0
Extended approximation boundaries by fractions and base-2 floating point numbers
hoelzl
parents:
30429
diff
changeset
|
1 |
(* Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009 *) |
30122 | 2 |
|
30429
39acdf031548
moved Decision_Procs examples to Decision_Procs/ex
haftmann
parents:
30413
diff
changeset
|
3 |
theory Approximation_Ex |
48480 | 4 |
imports Complex_Main "../Approximation" |
29805 | 5 |
begin |
6 |
||
60533 | 7 |
text \<open> |
29805 | 8 |
|
9 |
Here are some examples how to use the approximation method. |
|
10 |
||
31863
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
11 |
The approximation method has the following syntax: |
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
12 |
|
31864
90ec13cf7ab0
removed latex markup - there is no document generated from Decision_Procs/ex
hoelzl
parents:
31863
diff
changeset
|
13 |
approximate "prec" (splitting: "x" = "depth" and "y" = "depth" ...)? (taylor: "z" = "derivates")? |
31863
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
14 |
|
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
15 |
Here "prec" specifies the precision used in all computations, it is specified as |
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
16 |
number of bits to calculate. In the proposition to prove an arbitrary amount of |
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
17 |
variables can be used, but each one need to be bounded by an upper and lower |
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
18 |
bound. |
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
19 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48480
diff
changeset
|
20 |
To specify the bounds either @{term "l\<^sub>1 \<le> x \<and> x \<le> u\<^sub>1"}, |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
48480
diff
changeset
|
21 |
@{term "x \<in> { l\<^sub>1 .. u\<^sub>1 }"} or @{term "x = bnd"} can be used. Where the |
31863
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
22 |
bound specification are again arithmetic formulas containing variables. They can |
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
23 |
be connected using either meta level or HOL equivalence. |
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
24 |
|
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
25 |
To use interval splitting add for each variable whos interval should be splitted |
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
26 |
to the "splitting:" parameter. The parameter specifies how often each interval |
31864
90ec13cf7ab0
removed latex markup - there is no document generated from Decision_Procs/ex
hoelzl
parents:
31863
diff
changeset
|
27 |
should be divided, e.g. when x = 16 is specified, there will be @{term "65536 = 2^16"} |
90ec13cf7ab0
removed latex markup - there is no document generated from Decision_Procs/ex
hoelzl
parents:
31863
diff
changeset
|
28 |
intervals to be calculated. |
31863
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
29 |
|
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
30 |
To use taylor series expansion specify the variable to derive. You need to |
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
31 |
specify the amount of derivations to compute. When using taylor series expansion |
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
32 |
only one variable can be used. |
29805 | 33 |
|
60533 | 34 |
\<close> |
29805 | 35 |
|
36 |
section "Compute some transcendental values" |
|
37 |
||
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:
59658
diff
changeset
|
38 |
lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < (inverse (2^51) :: real)" |
47600 | 39 |
by (approximation 60) |
29805 | 40 |
|
41 |
lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 :: real)" |
|
47600 | 42 |
by (approximation 40) |
29805 | 43 |
|
44 |
lemma "\<bar> sqrt 2 - 1.4142135623730951 \<bar> < inverse 10 ^ 16" |
|
47600 | 45 |
by (approximation 60) |
31387 | 46 |
|
29805 | 47 |
lemma "\<bar> pi - 3.1415926535897932385 \<bar> < inverse 10 ^ 18" |
47600 | 48 |
by (approximation 70) |
29805 | 49 |
|
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58985
diff
changeset
|
50 |
lemma "\<bar> sin 100 + 0.50636564110975879 \<bar> < (inverse 10 ^ 17 :: real)" |
47600 | 51 |
by (approximation 70) |
31467
f7d2aa438bee
Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents:
31387
diff
changeset
|
52 |
|
29805 | 53 |
section "Use variable ranges" |
54 |
||
55 |
lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455" |
|
56 |
by (approximation 10) |
|
57 |
||
31811
64dea9a15031
Improved computation of bounds and implemented interval splitting for 'approximation'.
hoelzl
parents:
31467
diff
changeset
|
58 |
lemma "x \<in> {0.5 .. 4.5} \<longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455" |
64dea9a15031
Improved computation of bounds and implemented interval splitting for 'approximation'.
hoelzl
parents:
31467
diff
changeset
|
59 |
by (approximation 10) |
64dea9a15031
Improved computation of bounds and implemented interval splitting for 'approximation'.
hoelzl
parents:
31467
diff
changeset
|
60 |
|
30413
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset
|
61 |
lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455" |
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset
|
62 |
by (approximation 20) |
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset
|
63 |
|
30443
873fa77be5f0
Extended approximation boundaries by fractions and base-2 floating point numbers
hoelzl
parents:
30429
diff
changeset
|
64 |
lemma "1 / 2^1 \<le> x \<and> x \<le> 9 / 2^1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455" |
30413
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset
|
65 |
by (approximation 10) |
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset
|
66 |
|
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58985
diff
changeset
|
67 |
lemma "3.2 \<le> (x::real) \<and> x \<le> 6.2 \<Longrightarrow> sin x \<le> 0" |
58985
bf498e0af9e3
truncate intermediate results in horner to improve performance of approximate;
immler
parents:
56923
diff
changeset
|
68 |
by (approximation 10) |
29805 | 69 |
|
63263
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
60533
diff
changeset
|
70 |
lemma "3.2 \<le> (x::real) \<and> x \<le> 3.9 \<Longrightarrow> real_of_int (ceiling x) \<in> {4 .. 4}" |
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
60533
diff
changeset
|
71 |
by (approximation 10) |
c6c95d64607a
approximation, derivative, and continuity of floor and ceiling
immler
parents:
60533
diff
changeset
|
72 |
|
31811
64dea9a15031
Improved computation of bounds and implemented interval splitting for 'approximation'.
hoelzl
parents:
31467
diff
changeset
|
73 |
lemma |
64dea9a15031
Improved computation of bounds and implemented interval splitting for 'approximation'.
hoelzl
parents:
31467
diff
changeset
|
74 |
defines "g \<equiv> 9.80665" and "v \<equiv> 128.61" and "d \<equiv> pi / 180" |
64dea9a15031
Improved computation of bounds and implemented interval splitting for 'approximation'.
hoelzl
parents:
31467
diff
changeset
|
75 |
shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }" |
47600 | 76 |
using assms by (approximation 20) |
31811
64dea9a15031
Improved computation of bounds and implemented interval splitting for 'approximation'.
hoelzl
parents:
31467
diff
changeset
|
77 |
|
53077 | 78 |
lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x" |
32650 | 79 |
by (approximation 30 splitting: x=1 taylor: x = 3) |
80 |
||
63931
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63263
diff
changeset
|
81 |
lemma "(n::real) \<in> {32 .. 62} \<Longrightarrow> \<lceil>log 2 (2 * (\<lfloor>n\<rfloor> div 2) + 1)\<rceil> = \<lceil>log 2 (\<lfloor>n\<rfloor> + 1)\<rceil>" |
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63263
diff
changeset
|
82 |
unfolding eq_iff |
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63263
diff
changeset
|
83 |
by (approximation 20) |
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63263
diff
changeset
|
84 |
|
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63263
diff
changeset
|
85 |
approximate 10 |
31863
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31811
diff
changeset
|
86 |
|
29805 | 87 |
end |