src/HOL/Decision_Procs/ex/Approximation_Ex.thy
author paulson <lp15@cam.ac.uk>
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