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