author  hoelzl 
Tue, 10 Mar 2009 16:36:22 +0100  
changeset 30413  c41afa5607be 
parent 30122  1c912a9d8200 
permissions  rwrr 
30122  1 
(* Title: HOL/ex/ApproximationEx.thy 
2 
Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009 

29805  3 
*) 
30122  4 

29805  5 
theory ApproximationEx 
30413
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset

6 
imports "~~/src/HOL/Decision_Procs/Approximation" 
29805  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 

30413
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset

42 
lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x  0.91 \<bar> < 0.455" 
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset

43 
by (approximation 20) 
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset

44 

c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset

45 
lemma "1 * pow2 1 \<le> x \<and> x \<le> 9 * pow2 1 \<Longrightarrow> \<bar> arctan x  0.91 \<bar> < 0.455" 
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset

46 
by (approximation 10) 
c41afa5607be
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
hoelzl
parents:
30122
diff
changeset

47 

29805  48 
lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x" 
49 
by (approximation 10) 

50 

51 
end 

52 