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;
     1 (*  Title:      HOL/ex/ApproximationEx.thy
     2     Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009
     3 *)
     4 
     5 theory ApproximationEx
     6 imports "~~/src/HOL/Reflection/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 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"
    43   by (approximation 10)
    44 
    45 
    46 end
    47