src/HOL/ex/ApproximationEx.thy
author hoelzl
Tue Mar 10 16:36:22 2009 +0100 (2009-03-10)
changeset 30413 c41afa5607be
parent 30122 1c912a9d8200
permissions -rw-r--r--
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
     1 (*  Title:      HOL/ex/ApproximationEx.thy
     2     Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009
     3 *)
     4 
     5 theory ApproximationEx
     6 imports "~~/src/HOL/Decision_Procs/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.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
    43   by (approximation 20)
    44 
    45 lemma "1 * pow2 -1 \<le> x \<and> x \<le> 9 * pow2 -1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
    46   by (approximation 10)
    47 
    48 lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"
    49   by (approximation 10)
    50 
    51 end
    52