src/HOL/Decision_Procs/ex/Approximation_Ex.thy
 author paulson Sat Apr 11 11:56:40 2015 +0100 (2015-04-11) changeset 60017 b785d6d06430 parent 59658 0cc388370041 child 60533 1e7ccd864b62 permissions -rw-r--r--
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
```     1 (* Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009 *)
```
```     2
```
```     3 theory Approximation_Ex
```
```     4 imports Complex_Main "../Approximation"
```
```     5 begin
```
```     6
```
```     7 text {*
```
```     8
```
```     9 Here are some examples how to use the approximation method.
```
```    10
```
```    11 The approximation method has the following syntax:
```
```    12
```
```    13 approximate "prec" (splitting: "x" = "depth" and "y" = "depth" ...)? (taylor: "z" = "derivates")?
```
```    14
```
```    15 Here "prec" specifies the precision used in all computations, it is specified as
```
```    16 number of bits to calculate. In the proposition to prove an arbitrary amount of
```
```    17 variables can be used, but each one need to be bounded by an upper and lower
```
```    18 bound.
```
```    19
```
```    20 To specify the bounds either @{term "l\<^sub>1 \<le> x \<and> x \<le> u\<^sub>1"},
```
```    21 @{term "x \<in> { l\<^sub>1 .. u\<^sub>1 }"} or @{term "x = bnd"} can be used. Where the
```
```    22 bound specification are again arithmetic formulas containing variables. They can
```
```    23 be connected using either meta level or HOL equivalence.
```
```    24
```
```    25 To use interval splitting add for each variable whos interval should be splitted
```
```    26 to the "splitting:" parameter. The parameter specifies how often each interval
```
```    27 should be divided, e.g. when x = 16 is specified, there will be @{term "65536 = 2^16"}
```
```    28 intervals to be calculated.
```
```    29
```
```    30 To use taylor series expansion specify the variable to derive. You need to
```
```    31 specify the amount of derivations to compute. When using taylor series expansion
```
```    32 only one variable can be used.
```
```    33
```
```    34 *}
```
```    35
```
```    36 section "Compute some transcendental values"
```
```    37
```
```    38 lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < (inverse (2^51) :: real)"
```
```    39   by (approximation 60)
```
```    40
```
```    41 lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 :: real)"
```
```    42   by (approximation 40)
```
```    43
```
```    44 lemma "\<bar> sqrt 2 - 1.4142135623730951 \<bar> < inverse 10 ^ 16"
```
```    45   by (approximation 60)
```
```    46
```
```    47 lemma "\<bar> pi - 3.1415926535897932385 \<bar> < inverse 10 ^ 18"
```
```    48   by (approximation 70)
```
```    49
```
```    50 lemma "\<bar> sin 100 + 0.50636564110975879 \<bar> < (inverse 10 ^ 17 :: real)"
```
```    51   by (approximation 70)
```
```    52
```
```    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
```
```    58 lemma "x \<in> {0.5 .. 4.5} \<longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
```
```    59   by (approximation 10)
```
```    60
```
```    61 lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
```
```    62   by (approximation 20)
```
```    63
```
```    64 lemma "1 / 2^1 \<le> x \<and> x \<le> 9 / 2^1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
```
```    65   by (approximation 10)
```
```    66
```
```    67 lemma "3.2 \<le> (x::real) \<and> x \<le> 6.2 \<Longrightarrow> sin x \<le> 0"
```
```    68   by (approximation 10)
```
```    69
```
```    70 lemma
```
```    71   defines "g \<equiv> 9.80665" and "v \<equiv> 128.61" and "d \<equiv> pi / 180"
```
```    72   shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
```
```    73   using assms by (approximation 20)
```
```    74
```
```    75 lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x"
```
```    76   by (approximation 30 splitting: x=1 taylor: x = 3)
```
```    77
```
```    78 approximate "10"
```
```    79
```
```    80 end
```