src/HOL/ex/ApproximationEx.thy
changeset 30413 c41afa5607be
parent 30122 1c912a9d8200
equal deleted inserted replaced
30407:81218f70997f 30413:c41afa5607be
     1 (*  Title:      HOL/ex/ApproximationEx.thy
     1 (*  Title:      HOL/ex/ApproximationEx.thy
     2     Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009
     2     Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009
     3 *)
     3 *)
     4 
     4 
     5 theory ApproximationEx
     5 theory ApproximationEx
     6 imports "~~/src/HOL/Reflection/Approximation"
     6 imports "~~/src/HOL/Decision_Procs/Approximation"
     7 begin
     7 begin
     8 
     8 
     9 text {*
     9 text {*
    10 
    10 
    11 Here are some examples how to use the approximation method.
    11 Here are some examples how to use the approximation method.
    37 section "Use variable ranges"
    37 section "Use variable ranges"
    38 
    38 
    39 lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
    39 lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
    40   by (approximation 10)
    40   by (approximation 10)
    41 
    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 
    42 lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"
    48 lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"
    43   by (approximation 10)
    49   by (approximation 10)
    44 
    50 
    45 
       
    46 end
    51 end
    47 
    52