src/HOL/ex/ApproximationEx.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 30122 1c912a9d8200
child 30413 c41afa5607be
permissions -rw-r--r--
added lemmas
     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