equal
deleted
inserted
replaced
1 (* Title: HOL/ex/ApproximationEx.thy |
1 (* Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009 *) |
2 Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009 |
|
3 *) |
|
4 |
2 |
5 theory Approximation_Ex |
3 theory Approximation_Ex |
6 imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation" |
4 imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation" |
7 begin |
5 begin |
8 |
6 |
40 by (approximation 10) |
38 by (approximation 10) |
41 |
39 |
42 lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455" |
40 lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455" |
43 by (approximation 20) |
41 by (approximation 20) |
44 |
42 |
45 lemma "1 * pow2 -1 \<le> x \<and> x \<le> 9 * pow2 -1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455" |
43 lemma "1 / 2^1 \<le> x \<and> x \<le> 9 / 2^1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455" |
46 by (approximation 10) |
44 by (approximation 10) |
47 |
45 |
48 lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x" |
46 lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x" |
49 by (approximation 10) |
47 by (approximation 10) |
50 |
48 |