author | hoelzl |
Wed, 11 Mar 2009 13:53:51 +0100 | |
changeset 30443 | 873fa77be5f0 |
parent 30429 | 39acdf031548 |
child 31387 | c4a3c3e9dc8e |
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 |
39acdf031548
moved Decision_Procs examples to Decision_Procs/ex
haftmann
parents:
30413
diff
changeset
|
4 |
imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation" |
29805 | 5 |
begin |
6 |
||
7 |
text {* |
|
8 |
||
9 |
Here are some examples how to use the approximation method. |
|
10 |
||
11 |
The parameter passed to the method specifies the precision used by the computations, it is specified |
|
12 |
as number of bits to calculate. When a variable is used it needs to be bounded by an interval. This |
|
13 |
interval is specified as a conjunction of the lower and upper bound. It must have the form |
|
14 |
@{text "\<lbrakk> l\<^isub>1 \<le> x\<^isub>1 \<and> x\<^isub>1 \<le> u\<^isub>1 ; \<dots> ; l\<^isub>n \<le> x\<^isub>n \<and> x\<^isub>n \<le> u\<^isub>n \<rbrakk> \<Longrightarrow> F"} where @{term F} is the formula, and |
|
15 |
@{text "x\<^isub>1, \<dots>, x\<^isub>n"} are the variables. The lower bounds @{text "l\<^isub>1, \<dots>, l\<^isub>n"} and the upper bounds |
|
16 |
@{text "u\<^isub>1, \<dots>, u\<^isub>n"} must either be integer numerals, floating point numbers or of the form |
|
17 |
@{term "m * pow2 e"} to specify a exact floating point value. |
|
18 |
||
19 |
*} |
|
20 |
||
21 |
section "Compute some transcendental values" |
|
22 |
||
23 |
lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < inverse (2^51) " |
|
24 |
by (approximation 80) |
|
25 |
||
26 |
lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 :: real)" |
|
27 |
by (approximation 80) |
|
28 |
||
29 |
lemma "\<bar> sqrt 2 - 1.4142135623730951 \<bar> < inverse 10 ^ 16" |
|
30 |
by (approximation 80) |
|
31 |
||
32 |
lemma "\<bar> pi - 3.1415926535897932385 \<bar> < inverse 10 ^ 18" |
|
33 |
by (approximation 80) |
|
34 |
||
35 |
section "Use variable ranges" |
|
36 |
||
37 |
lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455" |
|
38 |
by (approximation 10) |
|
39 |
||
30413
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset
|
40 |
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
|
41 |
by (approximation 20) |
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset
|
42 |
|
30443
873fa77be5f0
Extended approximation boundaries by fractions and base-2 floating point numbers
hoelzl
parents:
30429
diff
changeset
|
43 |
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
|
44 |
by (approximation 10) |
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset
|
45 |
|
29805 | 46 |
lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x" |
47 |
by (approximation 10) |
|
48 |
||
49 |
end |
|
50 |