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