author  eberlm <eberlm@in.tum.de> 
Wed, 26 Apr 2017 17:01:10 +0200  
changeset 65582  a1bc1b020cf2 
child 66280  0c5eb47e2696 
permissions  rwrr 
65582
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1 
(* 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

2 
Author: Johannes Hoelzl, TU Muenchen 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

3 
Coercions removed by Dmitriy Traytel 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

4 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

5 
This file contains only general material about computing lower/upper bounds 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

6 
on real functions. Approximation.thy contains the actual approximation algorithm 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

7 
and the approximation oracle. This is in order to make a clear separation between 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

8 
"morally immaculate" material about upper/lower bounds and the trusted oracle/reflection. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

9 
*) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

10 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

11 
theory Approximation_Bounds 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

12 
imports 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

13 
Complex_Main 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

14 
"~~/src/HOL/Library/Float" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

15 
Dense_Linear_Order 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

16 
begin 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

17 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

18 
declare powr_neg_one [simp] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

19 
declare powr_neg_numeral [simp] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

20 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

21 
section "Horner Scheme" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

22 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

23 
subsection \<open>Define auxiliary helper \<open>horner\<close> function\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

24 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

25 
primrec horner :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> real" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

26 
"horner F G 0 i k x = 0"  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

27 
"horner F G (Suc n) i k x = 1 / k  x * horner F G n (F i) (G i k) x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

28 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

29 
lemma horner_schema': 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

30 
fixes x :: real and a :: "nat \<Rightarrow> real" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

31 
shows "a 0  x * (\<Sum> i=0..<n. (1)^i * a (Suc i) * x^i) = (\<Sum> i=0..<Suc n. (1)^i * a i * x^i)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

32 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

33 
have shift_pow: "\<And>i.  (x * ((1)^i * a (Suc i) * x ^ i)) = (1)^(Suc i) * a (Suc i) * x ^ (Suc i)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

34 
by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

35 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

36 
unfolding sum_distrib_left shift_pow uminus_add_conv_diff [symmetric] sum_negf[symmetric] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

37 
sum_head_upt_Suc[OF zero_less_Suc] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

38 
sum.reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (1)^n *a n * x^n"] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

39 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

40 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

41 
lemma horner_schema: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

42 
fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

43 
assumes f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

44 
shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. ( 1) ^ j * (1 / (f (j' + j))) * x ^ j)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

45 
proof (induct n arbitrary: j') 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

46 
case 0 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

47 
then show ?case by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

48 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

49 
case (Suc n) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

50 
show ?case unfolding horner.simps Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

51 
using horner_schema'[of "\<lambda> j. 1 / (f (j' + j))"] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

52 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

53 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

54 
lemma horner_bounds': 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

55 
fixes lb :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" and ub :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

56 
assumes "0 \<le> real_of_float x" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

57 
and lb_0: "\<And> i k x. lb 0 i k x = 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

58 
and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = float_plus_down prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

59 
(lapprox_rat prec 1 k) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

60 
( float_round_up prec (x * (ub n (F i) (G i k) x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

61 
and ub_0: "\<And> i k x. ub 0 i k x = 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

62 
and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = float_plus_up prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

63 
(rapprox_rat prec 1 k) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

64 
( float_round_down prec (x * (lb n (F i) (G i k) x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

65 
shows "(lb n ((F ^^ j') s) (f j') x) \<le> horner F G n ((F ^^ j') s) (f j') x \<and> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

66 
horner F G n ((F ^^ j') s) (f j') x \<le> (ub n ((F ^^ j') s) (f j') x)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

67 
(is "?lb n j' \<le> ?horner n j' \<and> ?horner n j' \<le> ?ub n j'") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

68 
proof (induct n arbitrary: j') 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

69 
case 0 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

70 
thus ?case unfolding lb_0 ub_0 horner.simps by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

71 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

72 
case (Suc n) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

73 
thus ?case using lapprox_rat[of prec 1 "f j'"] using rapprox_rat[of 1 "f j'" prec] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

74 
Suc[where j'="Suc j'"] \<open>0 \<le> real_of_float x\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

75 
by (auto intro!: add_mono mult_left_mono float_round_down_le float_round_up_le 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

76 
order_trans[OF add_mono[OF _ float_plus_down_le]] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

77 
order_trans[OF _ add_mono[OF _ float_plus_up_le]] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

78 
simp add: lb_Suc ub_Suc field_simps f_Suc) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

79 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

80 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

81 
subsection "Theorems for floating point functions implementing the horner scheme" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

82 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

83 
text \<open> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

84 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

85 
Here @{term_type "f :: nat \<Rightarrow> nat"} is the sequence defining the Taylor series, the coefficients are 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

86 
all alternating and reciprocs. We use @{term G} and @{term F} to describe the computation of @{term f}. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

87 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

88 
\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

89 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

90 
lemma horner_bounds: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

91 
fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

92 
assumes "0 \<le> real_of_float x" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

93 
and lb_0: "\<And> i k x. lb 0 i k x = 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

94 
and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = float_plus_down prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

95 
(lapprox_rat prec 1 k) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

96 
( float_round_up prec (x * (ub n (F i) (G i k) x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

97 
and ub_0: "\<And> i k x. ub 0 i k x = 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

98 
and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = float_plus_up prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

99 
(rapprox_rat prec 1 k) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

100 
( float_round_down prec (x * (lb n (F i) (G i k) x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

101 
shows "(lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. ( 1) ^ j * (1 / (f (j' + j))) * (x ^ j))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

102 
(is "?lb") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

103 
and "(\<Sum>j=0..<n. ( 1) ^ j * (1 / (f (j' + j))) * (x ^ j)) \<le> (ub n ((F ^^ j') s) (f j') x)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

104 
(is "?ub") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

105 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

106 
have "?lb \<and> ?ub" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

107 
using horner_bounds'[where lb=lb, OF \<open>0 \<le> real_of_float x\<close> f_Suc lb_0 lb_Suc ub_0 ub_Suc] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

108 
unfolding horner_schema[where f=f, OF f_Suc] by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

109 
thus "?lb" and "?ub" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

110 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

111 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

112 
lemma horner_bounds_nonpos: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

113 
fixes F :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

114 
assumes "real_of_float x \<le> 0" and f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

115 
and lb_0: "\<And> i k x. lb 0 i k x = 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

116 
and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = float_plus_down prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

117 
(lapprox_rat prec 1 k) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

118 
(float_round_down prec (x * (ub n (F i) (G i k) x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

119 
and ub_0: "\<And> i k x. ub 0 i k x = 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

120 
and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = float_plus_up prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

121 
(rapprox_rat prec 1 k) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

122 
(float_round_up prec (x * (lb n (F i) (G i k) x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

123 
shows "(lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (1 / (f (j' + j))) * real_of_float x ^ j)" (is "?lb") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

124 
and "(\<Sum>j=0..<n. (1 / (f (j' + j))) * real_of_float x ^ j) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

125 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

126 
have diff_mult_minus: "x  y * z = x +  y * z" for x y z :: float by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

127 
have sum_eq: "(\<Sum>j=0..<n. (1 / (f (j' + j))) * real_of_float x ^ j) = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

128 
(\<Sum>j = 0..<n. ( 1) ^ j * (1 / (f (j' + j))) * real_of_float ( x) ^ j)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

129 
by (auto simp add: field_simps power_mult_distrib[symmetric]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

130 
have "0 \<le> real_of_float (x)" using assms by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

131 
from horner_bounds[where G=G and F=F and f=f and s=s and prec=prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

132 
and lb="\<lambda> n i k x. lb n i k (x)" and ub="\<lambda> n i k x. ub n i k (x)", 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

133 
unfolded lb_Suc ub_Suc diff_mult_minus, 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

134 
OF this f_Suc lb_0 _ ub_0 _] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

135 
show "?lb" and "?ub" unfolding minus_minus sum_eq 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

136 
by (auto simp: minus_float_round_up_eq minus_float_round_down_eq) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

137 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

138 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

139 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

140 
subsection \<open>Selectors for next even or odd number\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

141 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

142 
text \<open> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

143 
The horner scheme computes alternating series. To get the upper and lower bounds we need to 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

144 
guarantee to access a even or odd member. To do this we use @{term get_odd} and @{term get_even}. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

145 
\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

146 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

147 
definition get_odd :: "nat \<Rightarrow> nat" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

148 
"get_odd n = (if odd n then n else (Suc n))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

149 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

150 
definition get_even :: "nat \<Rightarrow> nat" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

151 
"get_even n = (if even n then n else (Suc n))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

152 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

153 
lemma get_odd[simp]: "odd (get_odd n)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

154 
unfolding get_odd_def by (cases "odd n") auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

155 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

156 
lemma get_even[simp]: "even (get_even n)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

157 
unfolding get_even_def by (cases "even n") auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

158 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

159 
lemma get_odd_ex: "\<exists> k. Suc k = get_odd n \<and> odd (Suc k)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

160 
by (auto simp: get_odd_def odd_pos intro!: exI[of _ "n  1"]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

161 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

162 
lemma get_even_double: "\<exists>i. get_even n = 2 * i" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

163 
using get_even by (blast elim: evenE) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

164 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

165 
lemma get_odd_double: "\<exists>i. get_odd n = 2 * i + 1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

166 
using get_odd by (blast elim: oddE) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

167 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

168 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

169 
section "Power function" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

170 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

171 
definition float_power_bnds :: "nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float * float" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

172 
"float_power_bnds prec n l u = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

173 
(if 0 < l then (power_down_fl prec l n, power_up_fl prec u n) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

174 
else if odd n then 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

175 
( power_up_fl prec \<bar>l\<bar> n, 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

176 
if u < 0 then  power_down_fl prec \<bar>u\<bar> n else power_up_fl prec u n) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

177 
else if u < 0 then (power_down_fl prec \<bar>u\<bar> n, power_up_fl prec \<bar>l\<bar> n) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

178 
else (0, power_up_fl prec (max \<bar>l\<bar> \<bar>u\<bar>) n))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

179 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

180 
lemma le_minus_power_downI: "0 \<le> x \<Longrightarrow> x ^ n \<le>  a \<Longrightarrow> a \<le>  power_down prec x n" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

181 
by (subst le_minus_iff) (auto intro: power_down_le power_mono_odd) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

182 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

183 
lemma float_power_bnds: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

184 
"(l1, u1) = float_power_bnds prec n l u \<Longrightarrow> x \<in> {l .. u} \<Longrightarrow> (x::real) ^ n \<in> {l1..u1}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

185 
by (auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

186 
simp: float_power_bnds_def max_def real_power_up_fl real_power_down_fl minus_le_iff 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

187 
split: if_split_asm 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

188 
intro!: power_up_le power_down_le le_minus_power_downI 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

189 
intro: power_mono_odd power_mono power_mono_even zero_le_even_power) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

190 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

191 
lemma bnds_power: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

192 
"\<forall>(x::real) l u. (l1, u1) = float_power_bnds prec n l u \<and> x \<in> {l .. u} \<longrightarrow> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

193 
l1 \<le> x ^ n \<and> x ^ n \<le> u1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

194 
using float_power_bnds by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

195 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

196 
section \<open>Approximation utility functions\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

197 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

198 
definition bnds_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<times> float" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

199 
"bnds_mult prec a1 a2 b1 b2 = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

200 
(float_plus_down prec (nprt a1 * pprt b2) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

201 
(float_plus_down prec (nprt a2 * nprt b2) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

202 
(float_plus_down prec (pprt a1 * pprt b1) (pprt a2 * nprt b1))), 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

203 
float_plus_up prec (pprt a2 * pprt b2) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

204 
(float_plus_up prec (pprt a1 * nprt b2) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

205 
(float_plus_up prec (nprt a2 * pprt b1) (nprt a1 * nprt b1))))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

206 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

207 
lemma bnds_mult: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

208 
fixes prec :: nat and a1 aa2 b1 b2 :: float 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

209 
assumes "(l, u) = bnds_mult prec a1 a2 b1 b2" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

210 
assumes "a \<in> {real_of_float a1..real_of_float a2}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

211 
assumes "b \<in> {real_of_float b1..real_of_float b2}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

212 
shows "a * b \<in> {real_of_float l..real_of_float u}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

213 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

214 
from assms have "real_of_float l \<le> a * b" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

215 
by (intro order.trans[OF _ mult_ge_prts[of a1 a a2 b1 b b2]]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

216 
(auto simp: bnds_mult_def intro!: float_plus_down_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

217 
moreover from assms have "real_of_float u \<ge> a * b" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

218 
by (intro order.trans[OF mult_le_prts[of a1 a a2 b1 b b2]]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

219 
(auto simp: bnds_mult_def intro!: float_plus_up_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

220 
ultimately show ?thesis by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

221 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

222 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

223 
definition map_bnds :: "(nat \<Rightarrow> float \<Rightarrow> float) \<Rightarrow> (nat \<Rightarrow> float \<Rightarrow> float) \<Rightarrow> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

224 
nat \<Rightarrow> (float \<times> float) \<Rightarrow> (float \<times> float)" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

225 
"map_bnds lb ub prec = (\<lambda>(l,u). (lb prec l, ub prec u))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

226 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

227 
lemma map_bnds: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

228 
assumes "(lf, uf) = map_bnds lb ub prec (l, u)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

229 
assumes "mono f" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

230 
assumes "x \<in> {real_of_float l..real_of_float u}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

231 
assumes "real_of_float (lb prec l) \<le> f (real_of_float l)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

232 
assumes "real_of_float (ub prec u) \<ge> f (real_of_float u)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

233 
shows "f x \<in> {real_of_float lf..real_of_float uf}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

234 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

235 
from assms have "real_of_float lf = real_of_float (lb prec l)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

236 
by (simp add: map_bnds_def) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

237 
also have "real_of_float (lb prec l) \<le> f (real_of_float l)" by fact 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

238 
also from assms have "\<dots> \<le> f x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

239 
by (intro monoD[OF \<open>mono f\<close>]) auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

240 
finally have lf: "real_of_float lf \<le> f x" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

241 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

242 
from assms have "f x \<le> f (real_of_float u)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

243 
by (intro monoD[OF \<open>mono f\<close>]) auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

244 
also have "\<dots> \<le> real_of_float (ub prec u)" by fact 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

245 
also from assms have "\<dots> = real_of_float uf" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

246 
by (simp add: map_bnds_def) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

247 
finally have uf: "f x \<le> real_of_float uf" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

248 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

249 
from lf uf show ?thesis by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

250 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

251 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

252 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

253 
section "Square root" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

254 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

255 
text \<open> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

256 
The square root computation is implemented as newton iteration. As first first step we use the 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

257 
nearest power of two greater than the square root. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

258 
\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

259 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

260 
fun sqrt_iteration :: "nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

261 
"sqrt_iteration prec 0 x = Float 1 ((bitlen \<bar>mantissa x\<bar> + exponent x) div 2 + 1)"  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

262 
"sqrt_iteration prec (Suc m) x = (let y = sqrt_iteration prec m x 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

263 
in Float 1 ( 1) * float_plus_up prec y (float_divr prec x y))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

264 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

265 
lemma compute_sqrt_iteration_base[code]: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

266 
shows "sqrt_iteration prec n (Float m e) = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

267 
(if n = 0 then Float 1 ((if m = 0 then 0 else bitlen \<bar>m\<bar> + e) div 2 + 1) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

268 
else (let y = sqrt_iteration prec (n  1) (Float m e) in 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

269 
Float 1 ( 1) * float_plus_up prec y (float_divr prec (Float m e) y)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

270 
using bitlen_Float by (cases n) simp_all 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

271 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

272 
function ub_sqrt lb_sqrt :: "nat \<Rightarrow> float \<Rightarrow> float" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

273 
"ub_sqrt prec x = (if 0 < x then (sqrt_iteration prec prec x) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

274 
else if x < 0 then  lb_sqrt prec ( x) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

275 
else 0)"  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

276 
"lb_sqrt prec x = (if 0 < x then (float_divl prec x (sqrt_iteration prec prec x)) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

277 
else if x < 0 then  ub_sqrt prec ( x) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

278 
else 0)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

279 
by pat_completeness auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

280 
termination by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 0 then 1 else 0))", auto) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

281 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

282 
declare lb_sqrt.simps[simp del] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

283 
declare ub_sqrt.simps[simp del] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

284 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

285 
lemma sqrt_ub_pos_pos_1: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

286 
assumes "sqrt x < b" and "0 < b" and "0 < x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

287 
shows "sqrt x < (b + x / b)/2" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

288 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

289 
from assms have "0 < (b  sqrt x)\<^sup>2 " by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

290 
also have "\<dots> = b\<^sup>2  2 * b * sqrt x + (sqrt x)\<^sup>2" by algebra 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

291 
also have "\<dots> = b\<^sup>2  2 * b * sqrt x + x" using assms by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

292 
finally have "0 < b\<^sup>2  2 * b * sqrt x + x" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

293 
hence "0 < b / 2  sqrt x + x / (2 * b)" using assms 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

294 
by (simp add: field_simps power2_eq_square) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

295 
thus ?thesis by (simp add: field_simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

296 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

297 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

298 
lemma sqrt_iteration_bound: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

299 
assumes "0 < real_of_float x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

300 
shows "sqrt x < sqrt_iteration prec n x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

301 
proof (induct n) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

302 
case 0 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

303 
show ?case 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

304 
proof (cases x) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

305 
case (Float m e) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

306 
hence "0 < m" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

307 
using assms 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

308 
apply (auto simp: sign_simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

309 
by (meson not_less powr_ge_pzero) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

310 
hence "0 < sqrt m" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

311 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

312 
have int_nat_bl: "(nat (bitlen m)) = bitlen m" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

313 
using bitlen_nonneg by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

314 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

315 
have "x = (m / 2^nat (bitlen m)) * 2 powr (e + (nat (bitlen m)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

316 
unfolding Float by (auto simp: powr_realpow[symmetric] field_simps powr_add) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

317 
also have "\<dots> < 1 * 2 powr (e + nat (bitlen m))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

318 
proof (rule mult_strict_right_mono, auto) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

319 
show "m < 2^nat (bitlen m)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

320 
using bitlen_bounds[OF \<open>0 < m\<close>, THEN conjunct2] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

321 
unfolding of_int_less_iff[of m, symmetric] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

322 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

323 
finally have "sqrt x < sqrt (2 powr (e + bitlen m))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

324 
unfolding int_nat_bl by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

325 
also have "\<dots> \<le> 2 powr ((e + bitlen m) div 2 + 1)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

326 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

327 
let ?E = "e + bitlen m" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

328 
have E_mod_pow: "2 powr (?E mod 2) < 4" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

329 
proof (cases "?E mod 2 = 1") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

330 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

331 
thus ?thesis by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

332 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

333 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

334 
have "0 \<le> ?E mod 2" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

335 
have "?E mod 2 < 2" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

336 
from this[THEN zless_imp_add1_zle] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

337 
have "?E mod 2 \<le> 0" using False by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

338 
from xt1(5)[OF \<open>0 \<le> ?E mod 2\<close> this] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

339 
show ?thesis by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

340 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

341 
hence "sqrt (2 powr (?E mod 2)) < sqrt (2 * 2)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

342 
by (auto simp del: real_sqrt_four) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

343 
hence E_mod_pow: "sqrt (2 powr (?E mod 2)) < 2" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

344 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

345 
have E_eq: "2 powr ?E = 2 powr (?E div 2 + ?E div 2 + ?E mod 2)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

346 
by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

347 
have "sqrt (2 powr ?E) = sqrt (2 powr (?E div 2) * 2 powr (?E div 2) * 2 powr (?E mod 2))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

348 
unfolding E_eq unfolding powr_add[symmetric] by (metis of_int_add) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

349 
also have "\<dots> = 2 powr (?E div 2) * sqrt (2 powr (?E mod 2))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

350 
unfolding real_sqrt_mult[of _ "2 powr (?E mod 2)"] real_sqrt_abs2 by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

351 
also have "\<dots> < 2 powr (?E div 2) * 2 powr 1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

352 
by (rule mult_strict_left_mono) (auto intro: E_mod_pow) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

353 
also have "\<dots> = 2 powr (?E div 2 + 1)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

354 
unfolding add.commute[of _ 1] powr_add[symmetric] by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

355 
finally show ?thesis by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

356 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

357 
finally show ?thesis using \<open>0 < m\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

358 
unfolding Float 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

359 
by (subst compute_sqrt_iteration_base) (simp add: ac_simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

360 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

361 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

362 
case (Suc n) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

363 
let ?b = "sqrt_iteration prec n x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

364 
have "0 < sqrt x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

365 
using \<open>0 < real_of_float x\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

366 
also have "\<dots> < real_of_float ?b" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

367 
using Suc . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

368 
finally have "sqrt x < (?b + x / ?b)/2" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

369 
using sqrt_ub_pos_pos_1[OF Suc _ \<open>0 < real_of_float x\<close>] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

370 
also have "\<dots> \<le> (?b + (float_divr prec x ?b))/2" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

371 
by (rule divide_right_mono, auto simp add: float_divr) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

372 
also have "\<dots> = (Float 1 ( 1)) * (?b + (float_divr prec x ?b))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

373 
by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

374 
also have "\<dots> \<le> (Float 1 ( 1)) * (float_plus_up prec ?b (float_divr prec x ?b))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

375 
by (auto simp add: algebra_simps float_plus_up_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

376 
finally show ?case 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

377 
unfolding sqrt_iteration.simps Let_def distrib_left . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

378 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

379 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

380 
lemma sqrt_iteration_lower_bound: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

381 
assumes "0 < real_of_float x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

382 
shows "0 < real_of_float (sqrt_iteration prec n x)" (is "0 < ?sqrt") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

383 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

384 
have "0 < sqrt x" using assms by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

385 
also have "\<dots> < ?sqrt" using sqrt_iteration_bound[OF assms] . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

386 
finally show ?thesis . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

387 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

388 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

389 
lemma lb_sqrt_lower_bound: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

390 
assumes "0 \<le> real_of_float x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

391 
shows "0 \<le> real_of_float (lb_sqrt prec x)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

392 
proof (cases "0 < x") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

393 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

394 
hence "0 < real_of_float x" and "0 \<le> x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

395 
using \<open>0 \<le> real_of_float x\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

396 
hence "0 < sqrt_iteration prec prec x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

397 
using sqrt_iteration_lower_bound by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

398 
hence "0 \<le> real_of_float (float_divl prec x (sqrt_iteration prec prec x))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

399 
using float_divl_lower_bound[OF \<open>0 \<le> x\<close>] unfolding less_eq_float_def by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

400 
thus ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

401 
unfolding lb_sqrt.simps using True by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

402 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

403 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

404 
with \<open>0 \<le> real_of_float x\<close> have "real_of_float x = 0" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

405 
thus ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

406 
unfolding lb_sqrt.simps by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

407 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

408 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

409 
lemma bnds_sqrt': "sqrt x \<in> {(lb_sqrt prec x) .. (ub_sqrt prec x)}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

410 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

411 
have lb: "lb_sqrt prec x \<le> sqrt x" if "0 < x" for x :: float 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

412 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

413 
from that have "0 < real_of_float x" and "0 \<le> real_of_float x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

414 
hence sqrt_gt0: "0 < sqrt x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

415 
hence sqrt_ub: "sqrt x < sqrt_iteration prec prec x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

416 
using sqrt_iteration_bound by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

417 
have "(float_divl prec x (sqrt_iteration prec prec x)) \<le> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

418 
x / (sqrt_iteration prec prec x)" by (rule float_divl) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

419 
also have "\<dots> < x / sqrt x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

420 
by (rule divide_strict_left_mono[OF sqrt_ub \<open>0 < real_of_float x\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

421 
mult_pos_pos[OF order_less_trans[OF sqrt_gt0 sqrt_ub] sqrt_gt0]]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

422 
also have "\<dots> = sqrt x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

423 
unfolding inverse_eq_iff_eq[of _ "sqrt x", symmetric] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

424 
sqrt_divide_self_eq[OF \<open>0 \<le> real_of_float x\<close>, symmetric] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

425 
finally show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

426 
unfolding lb_sqrt.simps if_P[OF \<open>0 < x\<close>] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

427 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

428 
have ub: "sqrt x \<le> ub_sqrt prec x" if "0 < x" for x :: float 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

429 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

430 
from that have "0 < real_of_float x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

431 
hence "0 < sqrt x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

432 
hence "sqrt x < sqrt_iteration prec prec x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

433 
using sqrt_iteration_bound by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

434 
then show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

435 
unfolding ub_sqrt.simps if_P[OF \<open>0 < x\<close>] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

436 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

437 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

438 
using lb[of "x"] ub[of "x"] lb[of x] ub[of x] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

439 
by (auto simp add: lb_sqrt.simps ub_sqrt.simps real_sqrt_minus) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

440 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

441 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

442 
lemma bnds_sqrt: "\<forall>(x::real) lx ux. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

443 
(l, u) = (lb_sqrt prec lx, ub_sqrt prec ux) \<and> x \<in> {lx .. ux} \<longrightarrow> l \<le> sqrt x \<and> sqrt x \<le> u" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

444 
proof ((rule allI) +, rule impI, erule conjE, rule conjI) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

445 
fix x :: real 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

446 
fix lx ux 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

447 
assume "(l, u) = (lb_sqrt prec lx, ub_sqrt prec ux)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

448 
and x: "x \<in> {lx .. ux}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

449 
hence l: "l = lb_sqrt prec lx " and u: "u = ub_sqrt prec ux" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

450 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

451 
have "sqrt lx \<le> sqrt x" using x by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

452 
from order_trans[OF _ this] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

453 
show "l \<le> sqrt x" unfolding l using bnds_sqrt'[of lx prec] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

454 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

455 
have "sqrt x \<le> sqrt ux" using x by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

456 
from order_trans[OF this] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

457 
show "sqrt x \<le> u" unfolding u using bnds_sqrt'[of ux prec] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

458 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

459 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

460 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

461 
section "Arcus tangens and \<pi>" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

462 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

463 
subsection "Compute arcus tangens series" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

464 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

465 
text \<open> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

466 
As first step we implement the computation of the arcus tangens series. This is only valid in the range 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

467 
@{term "{1 :: real .. 1}"}. This is used to compute \<pi> and then the entire arcus tangens. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

468 
\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

469 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

470 
fun ub_arctan_horner :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

471 
and lb_arctan_horner :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

472 
"ub_arctan_horner prec 0 k x = 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

473 
 "ub_arctan_horner prec (Suc n) k x = float_plus_up prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

474 
(rapprox_rat prec 1 k) ( float_round_down prec (x * (lb_arctan_horner prec n (k + 2) x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

475 
 "lb_arctan_horner prec 0 k x = 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

476 
 "lb_arctan_horner prec (Suc n) k x = float_plus_down prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

477 
(lapprox_rat prec 1 k) ( float_round_up prec (x * (ub_arctan_horner prec n (k + 2) x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

478 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

479 
lemma arctan_0_1_bounds': 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

480 
assumes "0 \<le> real_of_float y" "real_of_float y \<le> 1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

481 
and "even n" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

482 
shows "arctan (sqrt y) \<in> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

483 
{(sqrt y * lb_arctan_horner prec n 1 y) .. (sqrt y * ub_arctan_horner prec (Suc n) 1 y)}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

484 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

485 
let ?c = "\<lambda>i. ( 1) ^ i * (1 / (i * 2 + (1::nat)) * sqrt y ^ (i * 2 + 1))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

486 
let ?S = "\<lambda>n. \<Sum> i=0..<n. ?c i" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

487 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

488 
have "0 \<le> sqrt y" using assms by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

489 
have "sqrt y \<le> 1" using assms by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

490 
from \<open>even n\<close> obtain m where "2 * m = n" by (blast elim: evenE) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

491 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

492 
have "arctan (sqrt y) \<in> { ?S n .. ?S (Suc n) }" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

493 
proof (cases "sqrt y = 0") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

494 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

495 
then show ?thesis by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

496 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

497 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

498 
hence "0 < sqrt y" using \<open>0 \<le> sqrt y\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

499 
hence prem: "0 < 1 / (0 * 2 + (1::nat)) * sqrt y ^ (0 * 2 + 1)" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

500 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

501 
have "\<bar> sqrt y \<bar> \<le> 1" using \<open>0 \<le> sqrt y\<close> \<open>sqrt y \<le> 1\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

502 
from mp[OF summable_Leibniz(2)[OF zeroseq_arctan_series[OF this] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

503 
monoseq_arctan_series[OF this]] prem, THEN spec, of m, unfolded \<open>2 * m = n\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

504 
show ?thesis unfolding arctan_series[OF \<open>\<bar> sqrt y \<bar> \<le> 1\<close>] Suc_eq_plus1 atLeast0LessThan . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

505 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

506 
note arctan_bounds = this[unfolded atLeastAtMost_iff] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

507 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

508 
have F: "\<And>n. 2 * Suc n + 1 = 2 * n + 1 + 2" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

509 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

510 
note bounds = horner_bounds[where s=1 and f="\<lambda>i. 2 * i + 1" and j'=0 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

511 
and lb="\<lambda>n i k x. lb_arctan_horner prec n k x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

512 
and ub="\<lambda>n i k x. ub_arctan_horner prec n k x", 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

513 
OF \<open>0 \<le> real_of_float y\<close> F lb_arctan_horner.simps ub_arctan_horner.simps] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

514 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

515 
have "(sqrt y * lb_arctan_horner prec n 1 y) \<le> arctan (sqrt y)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

516 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

517 
have "(sqrt y * lb_arctan_horner prec n 1 y) \<le> ?S n" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

518 
using bounds(1) \<open>0 \<le> sqrt y\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

519 
apply (simp only: power_add power_one_right mult.assoc[symmetric] sum_distrib_right[symmetric]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

520 
apply (simp only: mult.commute[where 'a=real] mult.commute[of _ "2::nat"] power_mult) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

521 
apply (auto intro!: mult_left_mono) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

522 
done 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

523 
also have "\<dots> \<le> arctan (sqrt y)" using arctan_bounds .. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

524 
finally show ?thesis . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

525 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

526 
moreover 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

527 
have "arctan (sqrt y) \<le> (sqrt y * ub_arctan_horner prec (Suc n) 1 y)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

528 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

529 
have "arctan (sqrt y) \<le> ?S (Suc n)" using arctan_bounds .. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

530 
also have "\<dots> \<le> (sqrt y * ub_arctan_horner prec (Suc n) 1 y)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

531 
using bounds(2)[of "Suc n"] \<open>0 \<le> sqrt y\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

532 
apply (simp only: power_add power_one_right mult.assoc[symmetric] sum_distrib_right[symmetric]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

533 
apply (simp only: mult.commute[where 'a=real] mult.commute[of _ "2::nat"] power_mult) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

534 
apply (auto intro!: mult_left_mono) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

535 
done 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

536 
finally show ?thesis . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

537 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

538 
ultimately show ?thesis by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

539 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

540 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

541 
lemma arctan_0_1_bounds: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

542 
assumes "0 \<le> real_of_float y" "real_of_float y \<le> 1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

543 
shows "arctan (sqrt y) \<in> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

544 
{(sqrt y * lb_arctan_horner prec (get_even n) 1 y) .. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

545 
(sqrt y * ub_arctan_horner prec (get_odd n) 1 y)}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

546 
using 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

547 
arctan_0_1_bounds'[OF assms, of n prec] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

548 
arctan_0_1_bounds'[OF assms, of "n + 1" prec] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

549 
arctan_0_1_bounds'[OF assms, of "n  1" prec] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

550 
by (auto simp: get_even_def get_odd_def odd_pos 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

551 
simp del: ub_arctan_horner.simps lb_arctan_horner.simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

552 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

553 
lemma arctan_lower_bound: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

554 
assumes "0 \<le> x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

555 
shows "x / (1 + x\<^sup>2) \<le> arctan x" (is "?l x \<le> _") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

556 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

557 
have "?l x  arctan x \<le> ?l 0  arctan 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

558 
using assms 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

559 
by (intro DERIV_nonpos_imp_nonincreasing[where f="\<lambda>x. ?l x  arctan x"]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

560 
(auto intro!: derivative_eq_intros simp: add_nonneg_eq_0_iff field_simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

561 
thus ?thesis by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

562 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

563 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

564 
lemma arctan_divide_mono: "0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> arctan y / y \<le> arctan x / x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

565 
by (rule DERIV_nonpos_imp_nonincreasing[where f="\<lambda>x. arctan x / x"]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

566 
(auto intro!: derivative_eq_intros divide_nonpos_nonneg 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

567 
simp: inverse_eq_divide arctan_lower_bound) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

568 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

569 
lemma arctan_mult_mono: "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> x * arctan y \<le> y * arctan x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

570 
using arctan_divide_mono[of x y] by (cases "x = 0") (simp_all add: field_simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

571 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

572 
lemma arctan_mult_le: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

573 
assumes "0 \<le> x" "x \<le> y" "y * z \<le> arctan y" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

574 
shows "x * z \<le> arctan x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

575 
proof (cases "x = 0") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

576 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

577 
then show ?thesis by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

578 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

579 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

580 
with assms have "z \<le> arctan y / y" by (simp add: field_simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

581 
also have "\<dots> \<le> arctan x / x" using assms \<open>x \<noteq> 0\<close> by (auto intro!: arctan_divide_mono) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

582 
finally show ?thesis using assms \<open>x \<noteq> 0\<close> by (simp add: field_simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

583 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

584 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

585 
lemma arctan_le_mult: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

586 
assumes "0 < x" "x \<le> y" "arctan x \<le> x * z" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

587 
shows "arctan y \<le> y * z" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

588 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

589 
from assms have "arctan y / y \<le> arctan x / x" by (auto intro!: arctan_divide_mono) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

590 
also have "\<dots> \<le> z" using assms by (auto simp: field_simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

591 
finally show ?thesis using assms by (simp add: field_simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

592 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

593 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

594 
lemma arctan_0_1_bounds_le: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

595 
assumes "0 \<le> x" "x \<le> 1" "0 < real_of_float xl" "real_of_float xl \<le> x * x" "x * x \<le> real_of_float xu" "real_of_float xu \<le> 1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

596 
shows "arctan x \<in> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

597 
{x * lb_arctan_horner p1 (get_even n) 1 xu .. x * ub_arctan_horner p2 (get_odd n) 1 xl}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

598 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

599 
from assms have "real_of_float xl \<le> 1" "sqrt (real_of_float xl) \<le> x" "x \<le> sqrt (real_of_float xu)" "0 \<le> real_of_float xu" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

600 
"0 \<le> real_of_float xl" "0 < sqrt (real_of_float xl)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

601 
by (auto intro!: real_le_rsqrt real_le_lsqrt simp: power2_eq_square) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

602 
from arctan_0_1_bounds[OF \<open>0 \<le> real_of_float xu\<close> \<open>real_of_float xu \<le> 1\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

603 
have "sqrt (real_of_float xu) * real_of_float (lb_arctan_horner p1 (get_even n) 1 xu) \<le> arctan (sqrt (real_of_float xu))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

604 
by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

605 
from arctan_mult_le[OF \<open>0 \<le> x\<close> \<open>x \<le> sqrt _\<close> this] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

606 
have "x * real_of_float (lb_arctan_horner p1 (get_even n) 1 xu) \<le> arctan x" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

607 
moreover 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

608 
from arctan_0_1_bounds[OF \<open>0 \<le> real_of_float xl\<close> \<open>real_of_float xl \<le> 1\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

609 
have "arctan (sqrt (real_of_float xl)) \<le> sqrt (real_of_float xl) * real_of_float (ub_arctan_horner p2 (get_odd n) 1 xl)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

610 
by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

611 
from arctan_le_mult[OF \<open>0 < sqrt xl\<close> \<open>sqrt xl \<le> x\<close> this] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

612 
have "arctan x \<le> x * real_of_float (ub_arctan_horner p2 (get_odd n) 1 xl)" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

613 
ultimately show ?thesis by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

614 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

615 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

616 
lemma arctan_0_1_bounds_round: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

617 
assumes "0 \<le> real_of_float x" "real_of_float x \<le> 1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

618 
shows "arctan x \<in> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

619 
{real_of_float x * lb_arctan_horner p1 (get_even n) 1 (float_round_up (Suc p2) (x * x)) .. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

620 
real_of_float x * ub_arctan_horner p3 (get_odd n) 1 (float_round_down (Suc p4) (x * x))}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

621 
using assms 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

622 
apply (cases "x > 0") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

623 
apply (intro arctan_0_1_bounds_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

624 
apply (auto simp: float_round_down.rep_eq float_round_up.rep_eq 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

625 
intro!: truncate_up_le1 mult_le_one truncate_down_le truncate_up_le truncate_down_pos 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

626 
mult_pos_pos) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

627 
done 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

628 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

629 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

630 
subsection "Compute \<pi>" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

631 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

632 
definition ub_pi :: "nat \<Rightarrow> float" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

633 
"ub_pi prec = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

634 
(let 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

635 
A = rapprox_rat prec 1 5 ; 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

636 
B = lapprox_rat prec 1 239 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

637 
in ((Float 1 2) * float_plus_up prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

638 
((Float 1 2) * float_round_up prec (A * (ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

639 
(float_round_down (Suc prec) (A * A))))) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

640 
( float_round_down prec (B * (lb_arctan_horner prec (get_even (prec div 14 + 1)) 1 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

641 
(float_round_up (Suc prec) (B * B)))))))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

642 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

643 
definition lb_pi :: "nat \<Rightarrow> float" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

644 
"lb_pi prec = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

645 
(let 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

646 
A = lapprox_rat prec 1 5 ; 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

647 
B = rapprox_rat prec 1 239 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

648 
in ((Float 1 2) * float_plus_down prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

649 
((Float 1 2) * float_round_down prec (A * (lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

650 
(float_round_up (Suc prec) (A * A))))) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

651 
( float_round_up prec (B * (ub_arctan_horner prec (get_odd (prec div 14 + 1)) 1 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

652 
(float_round_down (Suc prec) (B * B)))))))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

653 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

654 
lemma pi_boundaries: "pi \<in> {(lb_pi n) .. (ub_pi n)}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

655 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

656 
have machin_pi: "pi = 4 * (4 * arctan (1 / 5)  arctan (1 / 239))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

657 
unfolding machin[symmetric] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

658 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

659 
{ 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

660 
fix prec n :: nat 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

661 
fix k :: int 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

662 
assume "1 < k" hence "0 \<le> k" and "0 < k" and "1 \<le> k" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

663 
let ?k = "rapprox_rat prec 1 k" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

664 
let ?kl = "float_round_down (Suc prec) (?k * ?k)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

665 
have "1 div k = 0" using div_pos_pos_trivial[OF _ \<open>1 < k\<close>] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

666 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

667 
have "0 \<le> real_of_float ?k" by (rule order_trans[OF _ rapprox_rat]) (auto simp add: \<open>0 \<le> k\<close>) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

668 
have "real_of_float ?k \<le> 1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

669 
by (auto simp add: \<open>0 < k\<close> \<open>1 \<le> k\<close> less_imp_le 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

670 
intro!: mult_le_one order_trans[OF _ rapprox_rat] rapprox_rat_le1) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

671 
have "1 / k \<le> ?k" using rapprox_rat[where x=1 and y=k] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

672 
hence "arctan (1 / k) \<le> arctan ?k" by (rule arctan_monotone') 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

673 
also have "\<dots> \<le> (?k * ub_arctan_horner prec (get_odd n) 1 ?kl)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

674 
using arctan_0_1_bounds_round[OF \<open>0 \<le> real_of_float ?k\<close> \<open>real_of_float ?k \<le> 1\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

675 
by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

676 
finally have "arctan (1 / k) \<le> ?k * ub_arctan_horner prec (get_odd n) 1 ?kl" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

677 
} note ub_arctan = this 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

678 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

679 
{ 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

680 
fix prec n :: nat 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

681 
fix k :: int 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

682 
assume "1 < k" hence "0 \<le> k" and "0 < k" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

683 
let ?k = "lapprox_rat prec 1 k" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

684 
let ?ku = "float_round_up (Suc prec) (?k * ?k)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

685 
have "1 div k = 0" using div_pos_pos_trivial[OF _ \<open>1 < k\<close>] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

686 
have "1 / k \<le> 1" using \<open>1 < k\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

687 
have "0 \<le> real_of_float ?k" using lapprox_rat_nonneg[where x=1 and y=k, OF zero_le_one \<open>0 \<le> k\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

688 
by (auto simp add: \<open>1 div k = 0\<close>) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

689 
have "0 \<le> real_of_float (?k * ?k)" by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

690 
have "real_of_float ?k \<le> 1" using lapprox_rat by (rule order_trans, auto simp add: \<open>1 / k \<le> 1\<close>) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

691 
hence "real_of_float (?k * ?k) \<le> 1" using \<open>0 \<le> real_of_float ?k\<close> by (auto intro!: mult_le_one) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

692 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

693 
have "?k \<le> 1 / k" using lapprox_rat[where x=1 and y=k] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

694 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

695 
have "?k * lb_arctan_horner prec (get_even n) 1 ?ku \<le> arctan ?k" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

696 
using arctan_0_1_bounds_round[OF \<open>0 \<le> real_of_float ?k\<close> \<open>real_of_float ?k \<le> 1\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

697 
by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

698 
also have "\<dots> \<le> arctan (1 / k)" using \<open>?k \<le> 1 / k\<close> by (rule arctan_monotone') 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

699 
finally have "?k * lb_arctan_horner prec (get_even n) 1 ?ku \<le> arctan (1 / k)" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

700 
} note lb_arctan = this 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

701 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

702 
have "pi \<le> ub_pi n " 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

703 
unfolding ub_pi_def machin_pi Let_def times_float.rep_eq Float_num 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

704 
using lb_arctan[of 239] ub_arctan[of 5] powr_realpow[of 2 2] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

705 
by (intro mult_left_mono float_plus_up_le float_plus_down_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

706 
(auto intro!: mult_left_mono float_round_down_le float_round_up_le diff_mono) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

707 
moreover have "lb_pi n \<le> pi" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

708 
unfolding lb_pi_def machin_pi Let_def times_float.rep_eq Float_num 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

709 
using lb_arctan[of 5] ub_arctan[of 239] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

710 
by (intro mult_left_mono float_plus_up_le float_plus_down_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

711 
(auto intro!: mult_left_mono float_round_down_le float_round_up_le diff_mono) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

712 
ultimately show ?thesis by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

713 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

714 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

715 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

716 
subsection "Compute arcus tangens in the entire domain" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

717 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

718 
function lb_arctan :: "nat \<Rightarrow> float \<Rightarrow> float" and ub_arctan :: "nat \<Rightarrow> float \<Rightarrow> float" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

719 
"lb_arctan prec x = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

720 
(let 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

721 
ub_horner = \<lambda> x. float_round_up prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

722 
(x * 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

723 
ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (float_round_down (Suc prec) (x * x))); 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

724 
lb_horner = \<lambda> x. float_round_down prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

725 
(x * 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

726 
lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (float_round_up (Suc prec) (x * x))) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

727 
in 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

728 
if x < 0 then  ub_arctan prec (x) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

729 
else if x \<le> Float 1 ( 1) then lb_horner x 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

730 
else if x \<le> Float 1 1 then 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

731 
Float 1 1 * 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

732 
lb_horner 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

733 
(float_divl prec x 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

734 
(float_plus_up prec 1 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

735 
(ub_sqrt prec (float_plus_up prec 1 (float_round_up prec (x * x)))))) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

736 
else let inv = float_divr prec 1 x in 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

737 
if inv > 1 then 0 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

738 
else float_plus_down prec (lb_pi prec * Float 1 ( 1)) (  ub_horner inv))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

739 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

740 
 "ub_arctan prec x = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

741 
(let 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

742 
lb_horner = \<lambda> x. float_round_down prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

743 
(x * 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

744 
lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (float_round_up (Suc prec) (x * x))) ; 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

745 
ub_horner = \<lambda> x. float_round_up prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

746 
(x * 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

747 
ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (float_round_down (Suc prec) (x * x))) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

748 
in if x < 0 then  lb_arctan prec (x) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

749 
else if x \<le> Float 1 ( 1) then ub_horner x 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

750 
else if x \<le> Float 1 1 then 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

751 
let y = float_divr prec x 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

752 
(float_plus_down 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

753 
(Suc prec) 1 (lb_sqrt prec (float_plus_down prec 1 (float_round_down prec (x * x))))) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

754 
in if y > 1 then ub_pi prec * Float 1 ( 1) else Float 1 1 * ub_horner y 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

755 
else float_plus_up prec (ub_pi prec * Float 1 ( 1)) (  lb_horner (float_divl prec 1 x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

756 
by pat_completeness auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

757 
termination 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

758 
by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 0 then 1 else 0))", auto) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

759 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

760 
declare ub_arctan_horner.simps[simp del] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

761 
declare lb_arctan_horner.simps[simp del] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

762 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

763 
lemma lb_arctan_bound': 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

764 
assumes "0 \<le> real_of_float x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

765 
shows "lb_arctan prec x \<le> arctan x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

766 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

767 
have "\<not> x < 0" and "0 \<le> x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

768 
using \<open>0 \<le> real_of_float x\<close> by (auto intro!: truncate_up_le ) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

769 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

770 
let "?ub_horner x" = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

771 
"x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (float_round_down (Suc prec) (x * x))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

772 
and "?lb_horner x" = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

773 
"x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (float_round_up (Suc prec) (x * x))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

774 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

775 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

776 
proof (cases "x \<le> Float 1 ( 1)") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

777 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

778 
hence "real_of_float x \<le> 1" by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

779 
from arctan_0_1_bounds_round[OF \<open>0 \<le> real_of_float x\<close> \<open>real_of_float x \<le> 1\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

780 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

781 
unfolding lb_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] if_P[OF True] using \<open>0 \<le> x\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

782 
by (auto intro!: float_round_down_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

783 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

784 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

785 
hence "0 < real_of_float x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

786 
let ?R = "1 + sqrt (1 + real_of_float x * real_of_float x)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

787 
let ?sxx = "float_plus_up prec 1 (float_round_up prec (x * x))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

788 
let ?fR = "float_plus_up prec 1 (ub_sqrt prec ?sxx)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

789 
let ?DIV = "float_divl prec x ?fR" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

790 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

791 
have divisor_gt0: "0 < ?R" by (auto intro: add_pos_nonneg) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

792 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

793 
have "sqrt (1 + x*x) \<le> sqrt ?sxx" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

794 
by (auto simp: float_plus_up.rep_eq plus_up_def float_round_up.rep_eq intro!: truncate_up_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

795 
also have "\<dots> \<le> ub_sqrt prec ?sxx" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

796 
using bnds_sqrt'[of ?sxx prec] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

797 
finally 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

798 
have "sqrt (1 + x*x) \<le> ub_sqrt prec ?sxx" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

799 
hence "?R \<le> ?fR" by (auto simp: float_plus_up.rep_eq plus_up_def intro!: truncate_up_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

800 
hence "0 < ?fR" and "0 < real_of_float ?fR" using \<open>0 < ?R\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

801 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

802 
have monotone: "?DIV \<le> x / ?R" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

803 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

804 
have "?DIV \<le> real_of_float x / ?fR" by (rule float_divl) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

805 
also have "\<dots> \<le> x / ?R" by (rule divide_left_mono[OF \<open>?R \<le> ?fR\<close> \<open>0 \<le> real_of_float x\<close> mult_pos_pos[OF order_less_le_trans[OF divisor_gt0 \<open>?R \<le> real_of_float ?fR\<close>] divisor_gt0]]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

806 
finally show ?thesis . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

807 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

808 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

809 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

810 
proof (cases "x \<le> Float 1 1") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

811 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

812 
have "x \<le> sqrt (1 + x * x)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

813 
using real_sqrt_sum_squares_ge2[where x=1, unfolded numeral_2_eq_2] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

814 
also note \<open>\<dots> \<le> (ub_sqrt prec ?sxx)\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

815 
finally have "real_of_float x \<le> ?fR" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

816 
by (auto simp: float_plus_up.rep_eq plus_up_def intro!: truncate_up_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

817 
moreover have "?DIV \<le> real_of_float x / ?fR" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

818 
by (rule float_divl) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

819 
ultimately have "real_of_float ?DIV \<le> 1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

820 
unfolding divide_le_eq_1_pos[OF \<open>0 < real_of_float ?fR\<close>, symmetric] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

821 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

822 
have "0 \<le> real_of_float ?DIV" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

823 
using float_divl_lower_bound[OF \<open>0 \<le> x\<close>] \<open>0 < ?fR\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

824 
unfolding less_eq_float_def by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

825 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

826 
from arctan_0_1_bounds_round[OF \<open>0 \<le> real_of_float (?DIV)\<close> \<open>real_of_float (?DIV) \<le> 1\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

827 
have "Float 1 1 * ?lb_horner ?DIV \<le> 2 * arctan ?DIV" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

828 
by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

829 
also have "\<dots> \<le> 2 * arctan (x / ?R)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

830 
using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono arctan_monotone') 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

831 
also have "2 * arctan (x / ?R) = arctan x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

832 
using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

833 
finally show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

834 
unfolding lb_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

835 
if_not_P[OF \<open>\<not> x \<le> Float 1 ( 1)\<close>] if_P[OF True] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

836 
by (auto simp: float_round_down.rep_eq 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

837 
intro!: order_trans[OF mult_left_mono[OF truncate_down]]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

838 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

839 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

840 
hence "2 < real_of_float x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

841 
hence "1 \<le> real_of_float x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

842 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

843 
let "?invx" = "float_divr prec 1 x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

844 
have "0 \<le> arctan x" using arctan_monotone'[OF \<open>0 \<le> real_of_float x\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

845 
using arctan_tan[of 0, unfolded tan_zero] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

846 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

847 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

848 
proof (cases "1 < ?invx") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

849 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

850 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

851 
unfolding lb_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

852 
if_not_P[OF \<open>\<not> x \<le> Float 1 ( 1)\<close>] if_not_P[OF False] if_P[OF True] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

853 
using \<open>0 \<le> arctan x\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

854 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

855 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

856 
hence "real_of_float ?invx \<le> 1" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

857 
have "0 \<le> real_of_float ?invx" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

858 
by (rule order_trans[OF _ float_divr]) (auto simp add: \<open>0 \<le> real_of_float x\<close>) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

859 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

860 
have "1 / x \<noteq> 0" and "0 < 1 / x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

861 
using \<open>0 < real_of_float x\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

862 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

863 
have "arctan (1 / x) \<le> arctan ?invx" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

864 
unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone', rule float_divr) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

865 
also have "\<dots> \<le> ?ub_horner ?invx" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

866 
using arctan_0_1_bounds_round[OF \<open>0 \<le> real_of_float ?invx\<close> \<open>real_of_float ?invx \<le> 1\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

867 
by (auto intro!: float_round_up_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

868 
also note float_round_up 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

869 
finally have "pi / 2  float_round_up prec (?ub_horner ?invx) \<le> arctan x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

870 
using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

871 
unfolding sgn_pos[OF \<open>0 < 1 / real_of_float x\<close>] le_diff_eq by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

872 
moreover 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

873 
have "lb_pi prec * Float 1 ( 1) \<le> pi / 2" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

874 
unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

875 
ultimately 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

876 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

877 
unfolding lb_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

878 
if_not_P[OF \<open>\<not> x \<le> Float 1 ( 1)\<close>] if_not_P[OF \<open>\<not> x \<le> Float 1 1\<close>] if_not_P[OF False] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

879 
by (auto intro!: float_plus_down_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

880 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

881 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

882 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

883 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

884 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

885 
lemma ub_arctan_bound': 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

886 
assumes "0 \<le> real_of_float x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

887 
shows "arctan x \<le> ub_arctan prec x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

888 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

889 
have "\<not> x < 0" and "0 \<le> x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

890 
using \<open>0 \<le> real_of_float x\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

891 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

892 
let "?ub_horner x" = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

893 
"float_round_up prec (x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (float_round_down (Suc prec) (x * x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

894 
let "?lb_horner x" = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

895 
"float_round_down prec (x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (float_round_up (Suc prec) (x * x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

896 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

897 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

898 
proof (cases "x \<le> Float 1 ( 1)") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

899 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

900 
hence "real_of_float x \<le> 1" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

901 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

902 
unfolding ub_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] if_P[OF True] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

903 
using arctan_0_1_bounds_round[OF \<open>0 \<le> real_of_float x\<close> \<open>real_of_float x \<le> 1\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

904 
by (auto intro!: float_round_up_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

905 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

906 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

907 
hence "0 < real_of_float x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

908 
let ?R = "1 + sqrt (1 + real_of_float x * real_of_float x)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

909 
let ?sxx = "float_plus_down prec 1 (float_round_down prec (x * x))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

910 
let ?fR = "float_plus_down (Suc prec) 1 (lb_sqrt prec ?sxx)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

911 
let ?DIV = "float_divr prec x ?fR" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

912 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

913 
have sqr_ge0: "0 \<le> 1 + real_of_float x * real_of_float x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

914 
using sum_power2_ge_zero[of 1 "real_of_float x", unfolded numeral_2_eq_2] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

915 
hence "0 \<le> real_of_float (1 + x*x)" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

916 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

917 
hence divisor_gt0: "0 < ?R" by (auto intro: add_pos_nonneg) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

918 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

919 
have "lb_sqrt prec ?sxx \<le> sqrt ?sxx" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

920 
using bnds_sqrt'[of ?sxx] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

921 
also have "\<dots> \<le> sqrt (1 + x*x)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

922 
by (auto simp: float_plus_down.rep_eq plus_down_def float_round_down.rep_eq truncate_down_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

923 
finally have "lb_sqrt prec ?sxx \<le> sqrt (1 + x*x)" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

924 
hence "?fR \<le> ?R" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

925 
by (auto simp: float_plus_down.rep_eq plus_down_def truncate_down_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

926 
have "0 < real_of_float ?fR" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

927 
by (auto simp: float_plus_down.rep_eq plus_down_def float_round_down.rep_eq 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

928 
intro!: truncate_down_ge1 lb_sqrt_lower_bound order_less_le_trans[OF zero_less_one] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

929 
truncate_down_nonneg add_nonneg_nonneg) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

930 
have monotone: "x / ?R \<le> (float_divr prec x ?fR)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

931 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

932 
from divide_left_mono[OF \<open>?fR \<le> ?R\<close> \<open>0 \<le> real_of_float x\<close> mult_pos_pos[OF divisor_gt0 \<open>0 < real_of_float ?fR\<close>]] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

933 
have "x / ?R \<le> x / ?fR" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

934 
also have "\<dots> \<le> ?DIV" by (rule float_divr) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

935 
finally show ?thesis . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

936 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

937 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

938 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

939 
proof (cases "x \<le> Float 1 1") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

940 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

941 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

942 
proof (cases "?DIV > 1") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

943 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

944 
have "pi / 2 \<le> ub_pi prec * Float 1 ( 1)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

945 
unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

946 
from order_less_le_trans[OF arctan_ubound this, THEN less_imp_le] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

947 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

948 
unfolding ub_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

949 
if_not_P[OF \<open>\<not> x \<le> Float 1 ( 1)\<close>] if_P[OF \<open>x \<le> Float 1 1\<close>] if_P[OF True] . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

950 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

951 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

952 
hence "real_of_float ?DIV \<le> 1" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

953 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

954 
have "0 \<le> x / ?R" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

955 
using \<open>0 \<le> real_of_float x\<close> \<open>0 < ?R\<close> unfolding zero_le_divide_iff by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

956 
hence "0 \<le> real_of_float ?DIV" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

957 
using monotone by (rule order_trans) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

958 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

959 
have "arctan x = 2 * arctan (x / ?R)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

960 
using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

961 
also have "\<dots> \<le> 2 * arctan (?DIV)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

962 
using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

963 
also have "\<dots> \<le> (Float 1 1 * ?ub_horner ?DIV)" unfolding Float_num 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

964 
using arctan_0_1_bounds_round[OF \<open>0 \<le> real_of_float ?DIV\<close> \<open>real_of_float ?DIV \<le> 1\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

965 
by (auto intro!: float_round_up_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

966 
finally show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

967 
unfolding ub_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

968 
if_not_P[OF \<open>\<not> x \<le> Float 1 ( 1)\<close>] if_P[OF \<open>x \<le> Float 1 1\<close>] if_not_P[OF False] . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

969 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

970 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

971 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

972 
hence "2 < real_of_float x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

973 
hence "1 \<le> real_of_float x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

974 
hence "0 < real_of_float x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

975 
hence "0 < x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

976 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

977 
let "?invx" = "float_divl prec 1 x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

978 
have "0 \<le> arctan x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

979 
using arctan_monotone'[OF \<open>0 \<le> real_of_float x\<close>] and arctan_tan[of 0, unfolded tan_zero] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

980 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

981 
have "real_of_float ?invx \<le> 1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

982 
unfolding less_float_def 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

983 
by (rule order_trans[OF float_divl]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

984 
(auto simp add: \<open>1 \<le> real_of_float x\<close> divide_le_eq_1_pos[OF \<open>0 < real_of_float x\<close>]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

985 
have "0 \<le> real_of_float ?invx" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

986 
using \<open>0 < x\<close> by (intro float_divl_lower_bound) auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

987 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

988 
have "1 / x \<noteq> 0" and "0 < 1 / x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

989 
using \<open>0 < real_of_float x\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

990 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

991 
have "(?lb_horner ?invx) \<le> arctan (?invx)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

992 
using arctan_0_1_bounds_round[OF \<open>0 \<le> real_of_float ?invx\<close> \<open>real_of_float ?invx \<le> 1\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

993 
by (auto intro!: float_round_down_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

994 
also have "\<dots> \<le> arctan (1 / x)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

995 
unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone') (rule float_divl) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

996 
finally have "arctan x \<le> pi / 2  (?lb_horner ?invx)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

997 
using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

998 
unfolding sgn_pos[OF \<open>0 < 1 / x\<close>] le_diff_eq by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

999 
moreover 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1000 
have "pi / 2 \<le> ub_pi prec * Float 1 ( 1)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1001 
unfolding Float_num times_divide_eq_right mult_1_right 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1002 
using pi_boundaries by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1003 
ultimately 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1004 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1005 
unfolding ub_arctan.simps Let_def if_not_P[OF \<open>\<not> x < 0\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1006 
if_not_P[OF \<open>\<not> x \<le> Float 1 ( 1)\<close>] if_not_P[OF False] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1007 
by (auto intro!: float_round_up_le float_plus_up_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1008 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1009 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1010 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1011 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1012 
lemma arctan_boundaries: "arctan x \<in> {(lb_arctan prec x) .. (ub_arctan prec x)}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1013 
proof (cases "0 \<le> x") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1014 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1015 
hence "0 \<le> real_of_float x" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1016 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1017 
using ub_arctan_bound'[OF \<open>0 \<le> real_of_float x\<close>] lb_arctan_bound'[OF \<open>0 \<le> real_of_float x\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1018 
unfolding atLeastAtMost_iff by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1019 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1020 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1021 
let ?mx = "x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1022 
from False have "x < 0" and "0 \<le> real_of_float ?mx" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1023 
by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1024 
hence bounds: "lb_arctan prec ?mx \<le> arctan ?mx \<and> arctan ?mx \<le> ub_arctan prec ?mx" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1025 
using ub_arctan_bound'[OF \<open>0 \<le> real_of_float ?mx\<close>] lb_arctan_bound'[OF \<open>0 \<le> real_of_float ?mx\<close>] by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1026 
show ?thesis 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1027 
unfolding minus_float.rep_eq arctan_minus lb_arctan.simps[where x=x] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1028 
ub_arctan.simps[where x=x] Let_def if_P[OF \<open>x < 0\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1029 
unfolding atLeastAtMost_iff using bounds[unfolded minus_float.rep_eq arctan_minus] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1030 
by (simp add: arctan_minus) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1031 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1032 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1033 
lemma bnds_arctan: "\<forall> (x::real) lx ux. (l, u) = (lb_arctan prec lx, ub_arctan prec ux) \<and> x \<in> {lx .. ux} \<longrightarrow> l \<le> arctan x \<and> arctan x \<le> u" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1034 
proof (rule allI, rule allI, rule allI, rule impI) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1035 
fix x :: real 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1036 
fix lx ux 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1037 
assume "(l, u) = (lb_arctan prec lx, ub_arctan prec ux) \<and> x \<in> {lx .. ux}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1038 
hence l: "lb_arctan prec lx = l " 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1039 
and u: "ub_arctan prec ux = u" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1040 
and x: "x \<in> {lx .. ux}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1041 
by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1042 
show "l \<le> arctan x \<and> arctan x \<le> u" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1043 
proof 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1044 
show "l \<le> arctan x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1045 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1046 
from arctan_boundaries[of lx prec, unfolded l] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1047 
have "l \<le> arctan lx" by (auto simp del: lb_arctan.simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1048 
also have "\<dots> \<le> arctan x" using x by (auto intro: arctan_monotone') 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1049 
finally show ?thesis . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1050 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1051 
show "arctan x \<le> u" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1052 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1053 
have "arctan x \<le> arctan ux" using x by (auto intro: arctan_monotone') 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1054 
also have "\<dots> \<le> u" using arctan_boundaries[of ux prec, unfolded u] by (auto simp del: ub_arctan.simps) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1055 
finally show ?thesis . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1056 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1057 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1058 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1059 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1060 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1061 
section "Sinus and Cosinus" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1062 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1063 
subsection "Compute the cosinus and sinus series" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1064 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1065 
fun ub_sin_cos_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1066 
and lb_sin_cos_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1067 
"ub_sin_cos_aux prec 0 i k x = 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1068 
 "ub_sin_cos_aux prec (Suc n) i k x = float_plus_up prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1069 
(rapprox_rat prec 1 k) ( 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1070 
float_round_down prec (x * (lb_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1071 
 "lb_sin_cos_aux prec 0 i k x = 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1072 
 "lb_sin_cos_aux prec (Suc n) i k x = float_plus_down prec 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1073 
(lapprox_rat prec 1 k) ( 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1074 
float_round_up prec (x * (ub_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1075 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1076 
lemma cos_aux: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1077 
shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. ( 1) ^ i * (1/(fact (2 * i))) * x ^(2 * i))" (is "?lb") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1078 
and "(\<Sum> i=0..<n. ( 1) ^ i * (1/(fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1079 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1080 
have "0 \<le> real_of_float (x * x)" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1081 
let "?f n" = "fact (2 * n) :: nat" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1082 
have f_eq: "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 1 * (((\<lambda>i. i + 2) ^^ n) 1 + 1)" for n 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1083 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1084 
have "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1085 
then show ?thesis by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1086 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1087 
from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0, 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1088 
OF \<open>0 \<le> real_of_float (x * x)\<close> f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1089 
show ?lb and ?ub 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1090 
by (auto simp add: power_mult power2_eq_square[of "real_of_float x"]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1091 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1092 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1093 
lemma lb_sin_cos_aux_zero_le_one: "lb_sin_cos_aux prec n i j 0 \<le> 1" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1094 
by (cases j n rule: nat.exhaust[case_product nat.exhaust]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1095 
(auto intro!: float_plus_down_le order_trans[OF lapprox_rat]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1096 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1097 
lemma one_le_ub_sin_cos_aux: "odd n \<Longrightarrow> 1 \<le> ub_sin_cos_aux prec n i (Suc 0) 0" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1098 
by (cases n) (auto intro!: float_plus_up_le order_trans[OF _ rapprox_rat]) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1099 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1100 
lemma cos_boundaries: 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1101 
assumes "0 \<le> real_of_float x" and "x \<le> pi / 2" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1102 
shows "cos x \<in> {(lb_sin_cos_aux prec (get_even n) 1 1 (x * x)) .. (ub_sin_cos_aux prec (get_odd n) 1 1 (x * x))}" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1103 
proof (cases "real_of_float x = 0") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1104 
case False 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1105 
hence "real_of_float x \<noteq> 0" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1106 
hence "0 < x" and "0 < real_of_float x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1107 
using \<open>0 \<le> real_of_float x\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1108 
have "0 < x * x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1109 
using \<open>0 < x\<close> by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1110 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1111 
have morph_to_if_power: "(\<Sum> i=0..<n. (1::real) ^ i * (1/(fact (2 * i))) * x ^ (2 * i)) = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1112 
(\<Sum> i = 0 ..< 2 * n. (if even(i) then (( 1) ^ (i div 2))/((fact i)) else 0) * x ^ i)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1113 
(is "?sum = ?ifsum") for x n 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1114 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1115 
have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1116 
also have "\<dots> = 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1117 
(\<Sum> j = 0 ..< n. ( 1) ^ ((2 * j) div 2) / ((fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1118 
also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then ( 1) ^ (i div 2) / ((fact i)) * x ^ i else 0)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1119 
unfolding sum_split_even_odd atLeast0LessThan .. 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1120 
also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then ( 1) ^ (i div 2) / ((fact i)) else 0) * x ^ i)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1121 
by (rule sum.cong) auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1122 
finally show ?thesis . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1123 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1124 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1125 
{ fix n :: nat assume "0 < n" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1126 
hence "0 < 2 * n" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1127 
obtain t where "0 < t" and "t < real_of_float x" and 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1128 
cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (( 1) ^ (i div 2))/((fact i)) else 0) * (real_of_float x) ^ i) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1129 
+ (cos (t + 1/2 * (2 * n) * pi) / (fact (2*n))) * (real_of_float x)^(2*n)" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1130 
(is "_ = ?SUM + ?rest / ?fact * ?pow") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1131 
using Maclaurin_cos_expansion2[OF \<open>0 < real_of_float x\<close> \<open>0 < 2 * n\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1132 
unfolding cos_coeff_def atLeast0LessThan by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1133 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1134 
have "cos t * ( 1) ^ n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1135 
also have "\<dots> = cos (t + n * pi)" by (simp add: cos_add) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1136 
also have "\<dots> = ?rest" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1137 
finally have "cos t * ( 1) ^ n = ?rest" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1138 
moreover 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1139 
have "t \<le> pi / 2" using \<open>t < real_of_float x\<close> and \<open>x \<le> pi / 2\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1140 
hence "0 \<le> cos t" using \<open>0 < t\<close> and cos_ge_zero by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1141 
ultimately have even: "even n \<Longrightarrow> 0 \<le> ?rest" and odd: "odd n \<Longrightarrow> 0 \<le>  ?rest " by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1142 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1143 
have "0 < ?fact" by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1144 
have "0 < ?pow" using \<open>0 < real_of_float x\<close> by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1145 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1146 
{ 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1147 
assume "even n" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1148 
have "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> ?SUM" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1149 
unfolding morph_to_if_power[symmetric] using cos_aux by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1150 
also have "\<dots> \<le> cos x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1151 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1152 
from even[OF \<open>even n\<close>] \<open>0 < ?fact\<close> \<open>0 < ?pow\<close> 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1153 
have "0 \<le> (?rest / ?fact) * ?pow" by simp 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1154 
thus ?thesis unfolding cos_eq by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1155 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1156 
finally have "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> cos x" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1157 
} note lb = this 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1158 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1159 
{ 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1160 
assume "odd n" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1161 
have "cos x \<le> ?SUM" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1162 
proof  
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1163 
from \<open>0 < ?fact\<close> and \<open>0 < ?pow\<close> and odd[OF \<open>odd n\<close>] 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1164 
have "0 \<le> ( ?rest) / ?fact * ?pow" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1165 
by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1166 
thus ?thesis unfolding cos_eq by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1167 
qed 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1168 
also have "\<dots> \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1169 
unfolding morph_to_if_power[symmetric] using cos_aux by auto 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1170 
finally have "cos x \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1171 
} note ub = this and lb 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1172 
} note ub = this(1) and lb = this(2) 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1173 

a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1174 
have "cos x \<le> (ub_sin_cos_aux prec (get_odd n) 1 1 (x * x))" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1175 
using ub[OF odd_pos[OF get_odd] get_odd] . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1176 
moreover have "(lb_sin_cos_aux prec (get_even n) 1 1 (x * x)) \<le> cos x" 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1177 
proof (cases "0 < get_even n") 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1178 
case True 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1179 
show ?thesis using lb[OF True get_even] . 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1180 
next 
a1bc1b020cf2
tuned Approximation: separated general material from oracle
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

1181 
case False 
