author  hoelzl 
Tue, 06 Dec 2011 14:29:37 +0100  
changeset 45772  8a8f78ce0dcf 
parent 45495  c55a07526dbe 
child 46028  9f113cdf3d66 
permissions  rwrr 
30122  1 
(* Title: HOL/Library/Float.thy 
2 
Author: Steven Obua 2008 

3 
Author: Johannes Hoelzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009 

4 
*) 

29988  5 

6 
header {* FloatingPoint Numbers *} 

7 

20485  8 
theory Float 
35032
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
33555
diff
changeset

9 
imports Complex_Main Lattice_Algebras 
20485  10 
begin 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

11 

19765  12 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21256
diff
changeset

13 
pow2 :: "int \<Rightarrow> real" where 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

14 
[simp]: "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (a)))))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

15 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

16 
datatype float = Float int int 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

17 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

18 
primrec of_float :: "float \<Rightarrow> real" where 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

19 
"of_float (Float a b) = real a * pow2 b" 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

20 

73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

21 
defs (overloaded) 
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31863
diff
changeset

22 
real_of_float_def [code_unfold]: "real == of_float" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

23 

41024  24 
declare [[coercion "% x . Float x 0"]] 
25 
declare [[coercion "real::float\<Rightarrow>real"]] 

26 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

27 
primrec mantissa :: "float \<Rightarrow> int" where 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

28 
"mantissa (Float a b) = a" 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

29 

73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

30 
primrec scale :: "float \<Rightarrow> int" where 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

31 
"scale (Float a b) = b" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21256
diff
changeset

32 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

33 
instantiation float :: zero begin 
31467
f7d2aa438bee
Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents:
31098
diff
changeset

34 
definition zero_float where "0 = Float 0 0" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

35 
instance .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

36 
end 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

37 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

38 
instantiation float :: one begin 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

39 
definition one_float where "1 = Float 1 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

40 
instance .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

41 
end 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

42 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

43 
instantiation float :: number begin 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

44 
definition number_of_float where "number_of n = Float n 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

45 
instance .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

46 
end 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

47 

32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

48 
lemma number_of_float_Float [code_unfold_post]: 
31467
f7d2aa438bee
Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents:
31098
diff
changeset

49 
"number_of k = Float (number_of k) 0" 
f7d2aa438bee
Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents:
31098
diff
changeset

50 
by (simp add: number_of_float_def number_of_is_id) 
f7d2aa438bee
Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents:
31098
diff
changeset

51 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

52 
lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b" 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

53 
unfolding real_of_float_def using of_float.simps . 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

54 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

55 
lemma real_of_float_neg_exp: "e < 0 \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (e))" by auto 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

56 
lemma real_of_float_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (e))" by auto 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

57 
lemma real_of_float_ge0_exp: "0 \<le> e \<Longrightarrow> real (Float m e) = real m * (2^nat e)" by auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

58 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

59 
lemma Float_num[simp]: shows 
31467
f7d2aa438bee
Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents:
31098
diff
changeset

60 
"real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

61 
"real (Float 1 1) = 1/2" and "real (Float 1 2) = 1/4" and "real (Float 1 3) = 1/8" and 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

62 
"real (Float 1 0) = 1" and "real (Float (number_of n) 0) = number_of n" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

63 
by auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

64 

31863
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31467
diff
changeset

65 
lemma float_number_of[simp]: "real (number_of x :: float) = number_of x" 
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31467
diff
changeset

66 
by (simp only:number_of_float_def Float_num[unfolded number_of_is_id]) 
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31467
diff
changeset

67 

e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31467
diff
changeset

68 
lemma float_number_of_int[simp]: "real (Float n 0) = real n" 
41528  69 
by simp 
31863
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31467
diff
changeset

70 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

71 
lemma pow2_0[simp]: "pow2 0 = 1" by simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

72 
lemma pow2_1[simp]: "pow2 1 = 2" by simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

73 
lemma pow2_neg: "pow2 x = inverse (pow2 (x))" by simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

74 

45495
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

75 
lemma pow2_powr: "pow2 a = 2 powr a" 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

76 
by (simp add: powr_realpow[symmetric] powr_minus) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

77 

45495
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

78 
declare pow2_def[simp del] 
19765  79 

16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

80 
lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)" 
45495
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

81 
by (simp add: pow2_powr powr_add) 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

82 

c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

83 
lemma pow2_diff: "pow2 (a  b) = pow2 a / pow2 b" 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

84 
by (simp add: pow2_powr powr_divide2) 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

85 

c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

86 
lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)" 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

87 
by (simp add: pow2_add) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

88 

41528  89 
lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f) auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

90 

41528  91 
lemma float_split: "\<exists> a b. x = Float a b" by (cases x) auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

92 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

93 
lemma float_split2: "(\<forall> a b. x \<noteq> Float a b) = False" by (auto simp add: float_split) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

94 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

95 
lemma float_zero[simp]: "real (Float 0 e) = 0" by simp 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

96 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

97 
lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> abs((a::int) div 2) < abs a" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

98 
by arith 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21256
diff
changeset

99 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

100 
function normfloat :: "float \<Rightarrow> float" where 
41528  101 
"normfloat (Float a b) = 
102 
(if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1)) 

103 
else if a=0 then Float 0 0 else Float a b)" 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

104 
by pat_completeness auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

105 
termination by (relation "measure (nat o abs o mantissa)") (auto intro: abs_div_2_less) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

106 
declare normfloat.simps[simp del] 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

107 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

108 
theorem normfloat[symmetric, simp]: "real f = real (normfloat f)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

109 
proof (induct f rule: normfloat.induct) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

110 
case (1 a b) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

111 
have real2: "2 = real (2::int)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

112 
by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

113 
show ?case 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

114 
apply (subst normfloat.simps) 
41528  115 
apply auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

116 
apply (subst 1[symmetric]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

117 
apply (auto simp add: pow2_add even_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

118 
done 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

119 
qed 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

120 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

121 
lemma pow2_neq_zero[simp]: "pow2 x \<noteq> 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

122 
by (auto simp add: pow2_def) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

123 

26313  124 
lemma pow2_int: "pow2 (int c) = 2^c" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

125 
by (simp add: pow2_def) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

126 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

127 
lemma zero_less_pow2[simp]: 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

128 
"0 < pow2 x" 
45495
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

129 
by (simp add: pow2_powr) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

130 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

131 
lemma normfloat_imp_odd_or_zero: "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

132 
proof (induct f rule: normfloat.induct) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

133 
case (1 u v) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

134 
from 1 have ab: "normfloat (Float u v) = Float a b" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

135 
{ 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

136 
assume eu: "even u" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

137 
assume z: "u \<noteq> 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

138 
have "normfloat (Float u v) = normfloat (Float (u div 2) (v + 1))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

139 
apply (subst normfloat.simps) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

140 
by (simp add: eu z) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

141 
with ab have "normfloat (Float (u div 2) (v + 1)) = Float a b" by simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

142 
with 1 eu z have ?case by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

143 
} 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

144 
note case1 = this 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

145 
{ 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

146 
assume "odd u \<or> u = 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

147 
then have ou: "\<not> (u \<noteq> 0 \<and> even u)" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

148 
have "normfloat (Float u v) = (if u = 0 then Float 0 0 else Float u v)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

149 
apply (subst normfloat.simps) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

150 
apply (simp add: ou) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

151 
done 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

152 
with ab have "Float a b = (if u = 0 then Float 0 0 else Float u v)" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

153 
then have ?case 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

154 
apply (case_tac "u=0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

155 
apply (auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

156 
by (insert ou, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

157 
} 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

158 
note case2 = this 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

159 
show ?case 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

160 
apply (case_tac "odd u \<or> u = 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

161 
apply (rule case2) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

162 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

163 
apply (rule case1) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

164 
apply auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

165 
done 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

166 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

167 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

168 
lemma float_eq_odd_helper: 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

169 
assumes odd: "odd a'" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

170 
and floateq: "real (Float a b) = real (Float a' b')" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

171 
shows "b \<le> b'" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

172 
proof  
45495
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

173 
from odd have "a' \<noteq> 0" by auto 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

174 
with floateq have a': "real a' = real a * pow2 (b  b')" 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

175 
by (simp add: pow2_diff field_simps) 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

176 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

177 
{ 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

178 
assume bcmp: "b > b'" 
45495
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

179 
then have "\<exists>c::nat. b  b' = int c + 1" 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

180 
by arith 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

181 
then guess c .. 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

182 
with a' have "real a' = real (a * 2^c * 2)" 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

183 
by (simp add: pow2_def nat_add_distrib) 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

184 
with odd have False 
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

185 
unfolding real_of_int_inject by simp 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

186 
} 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

187 
then show ?thesis by arith 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

188 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

189 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

190 
lemma float_eq_odd: 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

191 
assumes odd1: "odd a" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

192 
and odd2: "odd a'" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

193 
and floateq: "real (Float a b) = real (Float a' b')" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

194 
shows "a = a' \<and> b = b'" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

195 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

196 
from 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

197 
float_eq_odd_helper[OF odd2 floateq] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

198 
float_eq_odd_helper[OF odd1 floateq[symmetric]] 
41528  199 
have beq: "b = b'" by arith 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

200 
with floateq show ?thesis by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

201 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

202 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

203 
theorem normfloat_unique: 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

204 
assumes real_of_float_eq: "real f = real g" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

205 
shows "normfloat f = normfloat g" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

206 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

207 
from float_split[of "normfloat f"] obtain a b where normf:"normfloat f = Float a b" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

208 
from float_split[of "normfloat g"] obtain a' b' where normg:"normfloat g = Float a' b'" by auto 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

209 
have "real (normfloat f) = real (normfloat g)" 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

210 
by (simp add: real_of_float_eq) 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

211 
then have float_eq: "real (Float a b) = real (Float a' b')" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

212 
by (simp add: normf normg) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

213 
have ab: "odd a \<or> (a = 0 \<and> b = 0)" by (rule normfloat_imp_odd_or_zero[OF normf]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

214 
have ab': "odd a' \<or> (a' = 0 \<and> b' = 0)" by (rule normfloat_imp_odd_or_zero[OF normg]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

215 
{ 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

216 
assume odd: "odd a" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

217 
then have "a \<noteq> 0" by (simp add: even_def, arith) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

218 
with float_eq have "a' \<noteq> 0" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

219 
with ab' have "odd a'" by simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

220 
from odd this float_eq have "a = a' \<and> b = b'" by (rule float_eq_odd) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

221 
} 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

222 
note odd_case = this 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

223 
{ 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

224 
assume even: "even a" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

225 
with ab have a0: "a = 0" by simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

226 
with float_eq have a0': "a' = 0" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

227 
from a0 a0' ab ab' have "a = a' \<and> b = b'" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

228 
} 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

229 
note even_case = this 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

230 
from odd_case even_case show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

231 
apply (simp add: normf normg) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

232 
apply (case_tac "even a") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

233 
apply auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

234 
done 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

235 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

236 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

237 
instantiation float :: plus begin 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

238 
fun plus_float where 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

239 
[simp del]: "(Float a_m a_e) + (Float b_m b_e) = 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

240 
(if a_e \<le> b_e then Float (a_m + b_m * 2^(nat(b_e  a_e))) a_e 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

241 
else Float (a_m * 2^(nat (a_e  b_e)) + b_m) b_e)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

242 
instance .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

243 
end 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

244 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

245 
instantiation float :: uminus begin 
30960  246 
primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (m) e" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

247 
instance .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

248 
end 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

249 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

250 
instantiation float :: minus begin 
30960  251 
definition minus_float where [simp del]: "(z::float)  w = z + ( w)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

252 
instance .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

253 
end 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

254 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

255 
instantiation float :: times begin 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

256 
fun times_float where [simp del]: "(Float a_m a_e) * (Float b_m b_e) = Float (a_m * b_m) (a_e + b_e)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

257 
instance .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

258 
end 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

259 

30960  260 
primrec float_pprt :: "float \<Rightarrow> float" where 
261 
"float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)" 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

262 

30960  263 
primrec float_nprt :: "float \<Rightarrow> float" where 
264 
"float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))" 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

265 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

266 
instantiation float :: ord begin 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

267 
definition le_float_def: "z \<le> (w :: float) \<equiv> real z \<le> real w" 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

268 
definition less_float_def: "z < (w :: float) \<equiv> real z < real w" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

269 
instance .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

270 
end 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

271 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

272 
lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)" 
41528  273 
by (cases a, cases b) (simp add: algebra_simps plus_float.simps, 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

274 
auto simp add: pow2_int[symmetric] pow2_add[symmetric]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

275 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

276 
lemma real_of_float_minus[simp]: "real ( a) =  real (a :: float)" 
41528  277 
by (cases a) (simp add: uminus_float.simps) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

278 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

279 
lemma real_of_float_sub[simp]: "real (a  b) = real a  real (b :: float)" 
41528  280 
by (cases a, cases b) (simp add: minus_float_def) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

281 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

282 
lemma real_of_float_mult[simp]: "real (a*b) = real a * real (b :: float)" 
41528  283 
by (cases a, cases b) (simp add: times_float.simps pow2_add) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

284 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

285 
lemma real_of_float_0[simp]: "real (0 :: float) = 0" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

286 
by (auto simp add: zero_float_def float_zero) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

287 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

288 
lemma real_of_float_1[simp]: "real (1 :: float) = 1" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

289 
by (auto simp add: one_float_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

290 

16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

291 
lemma zero_le_float: 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

292 
"(0 <= real (Float a b)) = (0 <= a)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

293 
apply auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

294 
apply (auto simp add: zero_le_mult_iff) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

295 
apply (insert zero_less_pow2[of b]) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

296 
apply (simp_all) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

297 
done 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

298 

b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

299 
lemma float_le_zero: 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

300 
"(real (Float a b) <= 0) = (a <= 0)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

301 
apply auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

302 
apply (auto simp add: mult_le_0_iff) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

303 
apply (insert zero_less_pow2[of b]) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

304 
apply auto 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

305 
done 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

306 

39161
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

307 
lemma zero_less_float: 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

308 
"(0 < real (Float a b)) = (0 < a)" 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

309 
apply auto 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

310 
apply (auto simp add: zero_less_mult_iff) 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

311 
apply (insert zero_less_pow2[of b]) 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

312 
apply (simp_all) 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

313 
done 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

314 

75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

315 
lemma float_less_zero: 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

316 
"(real (Float a b) < 0) = (a < 0)" 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

317 
apply auto 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

318 
apply (auto simp add: mult_less_0_iff) 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

319 
apply (insert zero_less_pow2[of b]) 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

320 
apply (simp_all) 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

321 
done 
75849a560c09
When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents:
36778
diff
changeset

322 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

323 
declare real_of_float_simp[simp del] 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

324 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

325 
lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)" 
41528  326 
by (cases a) (auto simp add: zero_le_float float_le_zero) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

327 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

328 
lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)" 
41528  329 
by (cases a) (auto simp add: zero_le_float float_le_zero) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

330 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

331 
instance float :: ab_semigroup_add 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

332 
proof (intro_classes) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

333 
fix a b c :: float 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

334 
show "a + b + c = a + (b + c)" 
41528  335 
by (cases a, cases b, cases c) 
336 
(auto simp add: algebra_simps power_add[symmetric] plus_float.simps) 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

337 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

338 
fix a b :: float 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

339 
show "a + b = b + a" 
41528  340 
by (cases a, cases b) (simp add: plus_float.simps) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

341 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

342 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

343 
instance float :: comm_monoid_mult 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

344 
proof (intro_classes) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

345 
fix a b c :: float 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

346 
show "a * b * c = a * (b * c)" 
41528  347 
by (cases a, cases b, cases c) (simp add: times_float.simps) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

348 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

349 
fix a b :: float 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

350 
show "a * b = b * a" 
41528  351 
by (cases a, cases b) (simp add: times_float.simps) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

352 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

353 
fix a :: float 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

354 
show "1 * a = a" 
41528  355 
by (cases a) (simp add: times_float.simps one_float_def) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

356 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

357 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

358 
(* Floats do NOT form a cancel_semigroup_add: *) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

359 
lemma "0 + Float 0 1 = 0 + Float 0 2" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

360 
by (simp add: plus_float.simps zero_float_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

361 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

362 
instance float :: comm_semiring 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

363 
proof (intro_classes) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

364 
fix a b c :: float 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

365 
show "(a + b) * c = a * c + b * c" 
41528  366 
by (cases a, cases b, cases c) (simp add: plus_float.simps times_float.simps algebra_simps) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

367 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

368 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

369 
(* Floats do NOT form an order, because "(x < y) = (x <= y & x <> y)" does NOT hold *) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

370 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

371 
instance float :: zero_neq_one 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

372 
proof (intro_classes) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

373 
show "(0::float) \<noteq> 1" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

374 
by (simp add: zero_float_def one_float_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

375 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

376 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

377 
lemma float_le_simp: "((x::float) \<le> y) = (0 \<le> y  x)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

378 
by (auto simp add: le_float_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

379 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

380 
lemma float_less_simp: "((x::float) < y) = (0 < y  x)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

381 
by (auto simp add: less_float_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

382 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

383 
lemma real_of_float_min: "real (min x y :: float) = min (real x) (real y)" unfolding min_def le_float_def by auto 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

384 
lemma real_of_float_max: "real (max a b :: float) = max (real a) (real b)" unfolding max_def le_float_def by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

385 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

386 
lemma float_power: "real (x ^ n :: float) = real x ^ n" 
30960  387 
by (induct n) simp_all 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

388 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

389 
lemma zero_le_pow2[simp]: "0 \<le> pow2 s" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

390 
apply (subgoal_tac "0 < pow2 s") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

391 
apply (auto simp only:) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

392 
apply auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

393 
done 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

394 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

395 
lemma pow2_less_0_eq_False[simp]: "(pow2 s < 0) = False" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

396 
apply auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

397 
apply (subgoal_tac "0 \<le> pow2 s") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

398 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

399 
apply simp 
24301  400 
done 
401 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

402 
lemma pow2_le_0_eq_False[simp]: "(pow2 s \<le> 0) = False" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

403 
apply auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

404 
apply (subgoal_tac "0 < pow2 s") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

405 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

406 
apply simp 
24301  407 
done 
408 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

409 
lemma float_pos_m_pos: "0 < Float m e \<Longrightarrow> 0 < m" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

410 
unfolding less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

411 
by auto 
19765  412 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

413 
lemma float_pos_less1_e_neg: assumes "0 < Float m e" and "Float m e < 1" shows "e < 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

414 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

415 
have "0 < m" using float_pos_m_pos `0 < Float m e` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

416 
hence "0 \<le> real m" and "1 \<le> real m" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

417 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

418 
show "e < 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

419 
proof (rule ccontr) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

420 
assume "\<not> e < 0" hence "0 \<le> e" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

421 
hence "1 \<le> pow2 e" unfolding pow2_def by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

422 
from mult_mono[OF `1 \<le> real m` this `0 \<le> real m`] 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

423 
have "1 \<le> Float m e" by (simp add: le_float_def real_of_float_simp) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

424 
thus False using `Float m e < 1` unfolding less_float_def le_float_def by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

425 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

426 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

427 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

428 
lemma float_less1_mantissa_bound: assumes "0 < Float m e" "Float m e < 1" shows "m < 2^(nat (e))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

429 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

430 
have "e < 0" using float_pos_less1_e_neg assms by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

431 
have "\<And>x. (0::real) < 2^x" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

432 
have "real m < 2^(nat (e))" using `Float m e < 1` 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

433 
unfolding less_float_def real_of_float_neg_exp[OF `e < 0`] real_of_float_1 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

434 
real_mult_less_iff1[of _ _ 1, OF `0 < 2^(nat (e))`, symmetric] 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

435 
mult_assoc by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

436 
thus ?thesis unfolding real_of_int_less_iff[symmetric] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

437 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

438 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

439 
function bitlen :: "int \<Rightarrow> int" where 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

440 
"bitlen 0 = 0"  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

441 
"bitlen 1 = 1"  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

442 
"0 < x \<Longrightarrow> bitlen x = 1 + (bitlen (x div 2))"  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

443 
"x < 1 \<Longrightarrow> bitlen x = 1 + (bitlen (x div 2))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

444 
apply (case_tac "x = 0 \<or> x = 1 \<or> x < 1 \<or> x > 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

445 
apply auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

446 
done 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

447 
termination by (relation "measure (nat o abs)", auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

448 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

449 
lemma bitlen_ge0: "0 \<le> bitlen x" by (induct x rule: bitlen.induct, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

450 
lemma bitlen_ge1: "x \<noteq> 0 \<Longrightarrow> 1 \<le> bitlen x" by (induct x rule: bitlen.induct, auto simp add: bitlen_ge0) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

451 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

452 
lemma bitlen_bounds': assumes "0 < x" shows "2^nat (bitlen x  1) \<le> x \<and> x + 1 \<le> 2^nat (bitlen x)" (is "?P x") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

453 
using `0 < x` 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

454 
proof (induct x rule: bitlen.induct) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

455 
fix x 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

456 
assume "0 < x" and hyp: "0 < x div 2 \<Longrightarrow> ?P (x div 2)" hence "0 \<le> x" and "x \<noteq> 0" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

457 
{ fix x have "0 \<le> 1 + bitlen x" using bitlen_ge0[of x] by auto } note gt0_pls1 = this 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

458 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

459 
have "0 < (2::int)" by auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

460 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

461 
show "?P x" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

462 
proof (cases "x = 1") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

463 
case True show "?P x" unfolding True by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

464 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

465 
case False hence "2 \<le> x" using `0 < x` `x \<noteq> 1` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

466 
hence "2 div 2 \<le> x div 2" by (rule zdiv_mono1, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

467 
hence "0 < x div 2" and "x div 2 \<noteq> 0" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

468 
hence bitlen_s1_ge0: "0 \<le> bitlen (x div 2)  1" using bitlen_ge1[OF `x div 2 \<noteq> 0`] by auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

469 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

470 
{ from hyp[OF `0 < x div 2`] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

471 
have "2 ^ nat (bitlen (x div 2)  1) \<le> x div 2" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

472 
hence "2 ^ nat (bitlen (x div 2)  1) * 2 \<le> x div 2 * 2" by (rule mult_right_mono, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

473 
also have "\<dots> \<le> x" using `0 < x` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

474 
finally have "2^nat (1 + bitlen (x div 2)  1) \<le> x" unfolding power_Suc2[symmetric] Suc_nat_eq_nat_zadd1[OF bitlen_s1_ge0] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

475 
} moreover 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

476 
{ have "x + 1 \<le> x  x mod 2 + 2" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

477 
proof  
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

478 
have "x mod 2 < 2" using `0 < x` by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

479 
hence "x < x  x mod 2 + 2" unfolding algebra_simps by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

480 
thus ?thesis by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

481 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

482 
also have "x  x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` zdiv_zmod_equality2[of x 2 0] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

483 
also have "\<dots> \<le> 2^nat (bitlen (x div 2)) * 2" using hyp[OF `0 < x div 2`, THEN conjunct2] by (rule mult_right_mono, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

484 
also have "\<dots> = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

485 
finally have "x + 1 \<le> 2^(1 + nat (bitlen (x div 2)))" . 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

486 
} 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

487 
ultimately show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

488 
unfolding bitlen.simps(3)[OF `0 < x`] nat_add_distrib[OF zero_le_one bitlen_ge0] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

489 
unfolding add_commute nat_add_distrib[OF zero_le_one gt0_pls1] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

490 
by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

491 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

492 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

493 
fix x :: int assume "x < 1" and "0 < x" hence False by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

494 
thus "?P x" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

495 
qed auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

496 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

497 
lemma bitlen_bounds: assumes "0 < x" shows "2^nat (bitlen x  1) \<le> x \<and> x < 2^nat (bitlen x)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

498 
using bitlen_bounds'[OF `0<x`] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

499 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

500 
lemma bitlen_div: assumes "0 < m" shows "1 \<le> real m / 2^nat (bitlen m  1)" and "real m / 2^nat (bitlen m  1) < 2" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

501 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

502 
let ?B = "2^nat(bitlen m  1)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

503 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

504 
have "?B \<le> m" using bitlen_bounds[OF `0 <m`] .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

505 
hence "1 * ?B \<le> real m" unfolding real_of_int_le_iff[symmetric] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

506 
thus "1 \<le> real m / ?B" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

507 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

508 
have "m \<noteq> 0" using assms by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

509 
have "0 \<le> bitlen m  1" using bitlen_ge1[OF `m \<noteq> 0`] by auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

510 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

511 
have "m < 2^nat(bitlen m)" using bitlen_bounds[OF `0 <m`] .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

512 
also have "\<dots> = 2^nat(bitlen m  1 + 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

513 
also have "\<dots> = ?B * 2" unfolding nat_add_distrib[OF `0 \<le> bitlen m  1` zero_le_one] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

514 
finally have "real m < 2 * ?B" unfolding real_of_int_less_iff[symmetric] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

515 
hence "real m / ?B < 2 * ?B / ?B" by (rule divide_strict_right_mono, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

516 
thus "real m / ?B < 2" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

517 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

518 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

519 
lemma float_gt1_scale: assumes "1 \<le> Float m e" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

520 
shows "0 \<le> e + (bitlen m  1)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

521 
proof (cases "0 \<le> e") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

522 
have "0 < Float m e" using assms unfolding less_float_def le_float_def by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

523 
hence "0 < m" using float_pos_m_pos by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

524 
hence "m \<noteq> 0" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

525 
case True with bitlen_ge1[OF `m \<noteq> 0`] show ?thesis by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

526 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

527 
have "0 < Float m e" using assms unfolding less_float_def le_float_def by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

528 
hence "0 < m" using float_pos_m_pos by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

529 
hence "m \<noteq> 0" and "1 < (2::int)" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

530 
case False let ?S = "2^(nat (e))" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

531 
have "1 \<le> real m * inverse ?S" using assms unfolding le_float_def real_of_float_nge0_exp[OF False] by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

532 
hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

533 
hence "?S \<le> real m" unfolding mult_assoc by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

534 
hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

535 
from this bitlen_bounds[OF `0 < m`, THEN conjunct2] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

536 
have "nat (e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF `1 < 2`, symmetric] by (rule order_le_less_trans) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

537 
hence "e < bitlen m" using False bitlen_ge0 by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

538 
thus ?thesis by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

539 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

540 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

541 
lemma normalized_float: assumes "m \<noteq> 0" shows "real (Float m ( (bitlen m  1))) = real m / 2^nat (bitlen m  1)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

542 
proof (cases " (bitlen m  1) = 0") 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

543 
case True show ?thesis unfolding real_of_float_simp pow2_def using True by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

544 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

545 
case False hence P: "\<not> 0 \<le>  (bitlen m  1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

546 
show ?thesis unfolding real_of_float_nge0_exp[OF P] divide_inverse by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

547 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

548 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

549 
lemma bitlen_Pls: "bitlen (Int.Pls) = Int.Pls" by (subst Pls_def, subst Pls_def, simp) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

550 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

551 
lemma bitlen_Min: "bitlen (Int.Min) = Int.Bit1 Int.Pls" by (subst Min_def, simp add: Bit1_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

552 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

553 
lemma bitlen_B0: "bitlen (Int.Bit0 b) = (if iszero b then Int.Pls else Int.succ (bitlen b))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

554 
apply (auto simp add: iszero_def succ_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

555 
apply (simp add: Bit0_def Pls_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

556 
apply (subst Bit0_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

557 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

558 
apply (subgoal_tac "0 < 2 * b \<or> 2 * b < 1") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

559 
apply auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

560 
done 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

561 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

562 
lemma bitlen_B1: "bitlen (Int.Bit1 b) = (if iszero (Int.succ b) then Int.Bit1 Int.Pls else Int.succ (bitlen b))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

563 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

564 
have h: "! x. (2*x + 1) div 2 = (x::int)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

565 
by arith 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

566 
show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

567 
apply (auto simp add: iszero_def succ_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

568 
apply (subst Bit1_def)+ 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

569 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

570 
apply (subgoal_tac "2 * b + 1 = 1") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

571 
apply (simp only:) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

572 
apply simp_all 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

573 
apply (subst Bit1_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

574 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

575 
apply (subgoal_tac "0 < 2 * b + 1 \<or> 2 * b + 1 < 1") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

576 
apply (auto simp add: h) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

577 
done 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

578 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

579 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

580 
lemma bitlen_number_of: "bitlen (number_of w) = number_of (bitlen w)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

581 
by (simp add: number_of_is_id) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

582 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

583 
lemma [code]: "bitlen x = 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

584 
(if x = 0 then 0 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

585 
else if x = 1 then 1 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

586 
else (1 + (bitlen (x div 2))))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

587 
by (cases "x = 0 \<or> x = 1 \<or> 0 < x") auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

588 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

589 
definition lapprox_posrat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

590 
where 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

591 
"lapprox_posrat prec x y = 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

592 
(let 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

593 
l = nat (int prec + bitlen y  bitlen x) ; 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

594 
d = (x * 2^l) div y 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

595 
in normfloat (Float d ( (int l))))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

596 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

597 
lemma pow2_minus: "pow2 (x) = inverse (pow2 x)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

598 
unfolding pow2_neg[of "x"] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

599 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

600 
lemma lapprox_posrat: 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

601 
assumes x: "0 \<le> x" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

602 
and y: "0 < y" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

603 
shows "real (lapprox_posrat prec x y) \<le> real x / real y" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

604 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

605 
let ?l = "nat (int prec + bitlen y  bitlen x)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

606 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

607 
have "real (x * 2^?l div y) * inverse (2^?l) \<le> (real (x * 2^?l) / real y) * inverse (2^?l)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

608 
by (rule mult_right_mono, fact real_of_int_div4, simp) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

609 
also have "\<dots> \<le> (real x / real y) * 2^?l * inverse (2^?l)" by auto 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

610 
finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding mult_assoc by auto 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

611 
thus ?thesis unfolding lapprox_posrat_def Let_def normfloat real_of_float_simp 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

612 
unfolding pow2_minus pow2_int minus_minus . 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

613 
qed 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

614 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

615 
lemma real_of_int_div_mult: 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

616 
fixes x y c :: int assumes "0 < y" and "0 < c" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

617 
shows "real (x div y) \<le> real (x * c div y) * inverse (real c)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

618 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

619 
have "c * (x div y) + 0 \<le> c * x div y" unfolding zdiv_zmult1_eq[of c x y] 
44766  620 
by (rule add_left_mono, 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

621 
auto intro!: mult_nonneg_nonneg 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

622 
simp add: pos_imp_zdiv_nonneg_iff[OF `0 < y`] `0 < c`[THEN less_imp_le] pos_mod_sign[OF `0 < y`]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

623 
hence "real (x div y) * real c \<le> real (x * c div y)" 
44766  624 
unfolding real_of_int_mult[symmetric] real_of_int_le_iff mult_commute by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

625 
hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

626 
using `0 < c` by auto 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

627 
thus ?thesis unfolding mult_assoc using `0 < c` by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

628 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

629 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

630 
lemma lapprox_posrat_bottom: assumes "0 < y" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

631 
shows "real (x div y) \<le> real (lapprox_posrat n x y)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

632 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

633 
have pow: "\<And>x. (0::int) < 2^x" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

634 
show ?thesis 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

635 
unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

636 
using real_of_int_div_mult[OF `0 < y` pow] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

637 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

638 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

639 
lemma lapprox_posrat_nonneg: assumes "0 \<le> x" and "0 < y" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

640 
shows "0 \<le> real (lapprox_posrat n x y)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

641 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

642 
show ?thesis 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

643 
unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

644 
using pos_imp_zdiv_nonneg_iff[OF `0 < y`] assms by (auto intro!: mult_nonneg_nonneg) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

645 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

646 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

647 
definition rapprox_posrat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

648 
where 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

649 
"rapprox_posrat prec x y = (let 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

650 
l = nat (int prec + bitlen y  bitlen x) ; 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

651 
X = x * 2^l ; 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

652 
d = X div y ; 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

653 
m = X mod y 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

654 
in normfloat (Float (d + (if m = 0 then 0 else 1)) ( (int l))))" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

655 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

656 
lemma rapprox_posrat: 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

657 
assumes x: "0 \<le> x" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

658 
and y: "0 < y" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

659 
shows "real x / real y \<le> real (rapprox_posrat prec x y)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

660 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

661 
let ?l = "nat (int prec + bitlen y  bitlen x)" let ?X = "x * 2^?l" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

662 
show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

663 
proof (cases "?X mod y = 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

664 
case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

665 
from real_of_int_div[OF this] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

666 
have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

667 
also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

668 
finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

669 
thus ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True] 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

670 
unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

671 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

672 
case False 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

673 
have "0 \<le> real y" and "real y \<noteq> 0" using `0 < y` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

674 
have "0 \<le> real y * 2^?l" by (rule mult_nonneg_nonneg, rule `0 \<le> real y`, auto) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

675 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

676 
have "?X = y * (?X div y) + ?X mod y" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

677 
also have "\<dots> \<le> y * (?X div y) + y" by (rule add_mono, auto simp add: pos_mod_bound[OF `0 < y`, THEN less_imp_le]) 
44766  678 
also have "\<dots> = y * (?X div y + 1)" unfolding right_distrib by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

679 
finally have "real ?X \<le> real y * real (?X div y + 1)" unfolding real_of_int_le_iff real_of_int_mult[symmetric] . 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

680 
hence "real ?X / (real y * 2^?l) \<le> real y * real (?X div y + 1) / (real y * 2^?l)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

681 
by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

682 
also have "\<dots> = real y * real (?X div y + 1) / real y / 2^?l" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

683 
also have "\<dots> = real (?X div y + 1) * inverse (2^?l)" unfolding nonzero_mult_divide_cancel_left[OF `real y \<noteq> 0`] 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

684 
unfolding divide_inverse .. 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

685 
finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False] 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

686 
unfolding pow2_minus pow2_int minus_minus by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

687 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

688 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

689 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

690 
lemma rapprox_posrat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

691 
shows "real (rapprox_posrat n x y) \<le> 1" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

692 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

693 
let ?l = "nat (int n + bitlen y  bitlen x)" let ?X = "x * 2^?l" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

694 
show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

695 
proof (cases "?X mod y = 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

696 
case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

697 
from real_of_int_div[OF this] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

698 
have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

699 
also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

700 
finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

701 
also have "real x / real y \<le> 1" using `0 \<le> x` and `0 < y` and `x \<le> y` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

702 
finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True] 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

703 
unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

704 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

705 
case False 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

706 
have "x \<noteq> y" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

707 
proof (rule ccontr) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

708 
assume "\<not> x \<noteq> y" hence "x = y" by auto 
30034  709 
have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

710 
thus False using False by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

711 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

712 
hence "x < y" using `x \<le> y` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

713 
hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

714 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

715 
from real_of_int_div4[of "?X" y] 
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35032
diff
changeset

716 
have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of . 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

717 
also have "\<dots> < 1 * 2^?l" using `real x / real y < 1` by (rule mult_strict_right_mono, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

718 
finally have "?X div y < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

719 
hence "?X div y + 1 \<le> 2^?l" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

720 
hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)" 
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35032
diff
changeset

721 
unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

722 
by (rule mult_right_mono, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

723 
hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

724 
thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False] 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

725 
unfolding pow2_minus pow2_int minus_minus by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

726 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

727 
qed 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

728 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

729 
lemma zdiv_greater_zero: fixes a b :: int assumes "0 < a" and "a \<le> b" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

730 
shows "0 < b div a" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

731 
proof (rule ccontr) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

732 
have "0 \<le> b" using assms by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

733 
assume "\<not> 0 < b div a" hence "b div a = 0" using `0 \<le> b`[unfolded pos_imp_zdiv_nonneg_iff[OF `0<a`, of b, symmetric]] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

734 
have "b = a * (b div a) + b mod a" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

735 
hence "b = b mod a" unfolding `b div a = 0` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

736 
hence "b < a" using `0 < a`[THEN pos_mod_bound, of b] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

737 
thus False using `a \<le> b` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

738 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

739 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

740 
lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

741 
shows "real (rapprox_posrat n x y) < 1" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

742 
proof (cases "x = 0") 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

743 
case True thus ?thesis unfolding rapprox_posrat_def True Let_def normfloat real_of_float_simp by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

744 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

745 
case False hence "0 < x" using `0 \<le> x` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

746 
hence "x < y" using assms by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

747 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

748 
let ?l = "nat (int n + bitlen y  bitlen x)" let ?X = "x * 2^?l" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

749 
show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

750 
proof (cases "?X mod y = 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

751 
case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

752 
from real_of_int_div[OF this] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

753 
have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

754 
also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

755 
finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

756 
also have "real x / real y < 1" using `0 \<le> x` and `0 < y` and `x < y` by auto 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

757 
finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_P[OF True] 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

758 
unfolding pow2_minus pow2_int minus_minus by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

759 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

760 
case False 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

761 
hence "(real x / real y) < 1 / 2" using `0 < y` and `0 \<le> x` `2 * x < y` by auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

762 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

763 
have "0 < ?X div y" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

764 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

765 
have "2^nat (bitlen x  1) \<le> y" and "y < 2^nat (bitlen y)" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

766 
using bitlen_bounds[OF `0 < x`, THEN conjunct1] bitlen_bounds[OF `0 < y`, THEN conjunct2] `x < y` by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

767 
hence "(2::int)^nat (bitlen x  1) < 2^nat (bitlen y)" by (rule order_le_less_trans) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

768 
hence "bitlen x \<le> bitlen y" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

769 
hence len_less: "nat (bitlen x  1) \<le> nat (int (n  1) + bitlen y)" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

770 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

771 
have "x \<noteq> 0" and "y \<noteq> 0" using `0 < x` `0 < y` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

772 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

773 
have exp_eq: "nat (int (n  1) + bitlen y)  nat (bitlen x  1) = ?l" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

774 
using `bitlen x \<le> bitlen y` bitlen_ge1[OF `x \<noteq> 0`] bitlen_ge1[OF `y \<noteq> 0`] `0 < n` by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

775 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

776 
have "y * 2^nat (bitlen x  1) \<le> y * x" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

777 
using bitlen_bounds[OF `0 < x`, THEN conjunct1] `0 < y`[THEN less_imp_le] by (rule mult_left_mono) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

778 
also have "\<dots> \<le> 2^nat (bitlen y) * x" using bitlen_bounds[OF `0 < y`, THEN conjunct2, THEN less_imp_le] `0 \<le> x` by (rule mult_right_mono) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

779 
also have "\<dots> \<le> x * 2^nat (int (n  1) + bitlen y)" unfolding mult_commute[of x] by (rule mult_right_mono, auto simp add: `0 \<le> x`) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

780 
finally have "real y * 2^nat (bitlen x  1) * inverse (2^nat (bitlen x  1)) \<le> real x * 2^nat (int (n  1) + bitlen y) * inverse (2^nat (bitlen x  1))" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

781 
unfolding real_of_int_le_iff[symmetric] by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

782 
hence "real y \<le> real x * (2^nat (int (n  1) + bitlen y) / (2^nat (bitlen x  1)))" 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

783 
unfolding mult_assoc divide_inverse by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

784 
also have "\<dots> = real x * (2^(nat (int (n  1) + bitlen y)  nat (bitlen x  1)))" using power_diff[of "2::real", OF _ len_less] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

785 
finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

786 
thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

787 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

788 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

789 
from real_of_int_div4[of "?X" y] 
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35032
diff
changeset

790 
have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of . 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

791 
also have "\<dots> < 1/2 * 2^?l" using `real x / real y < 1/2` by (rule mult_strict_right_mono, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

792 
finally have "?X div y * 2 < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

793 
hence "?X div y + 1 < 2^?l" using `0 < ?X div y` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

794 
hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)" 
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35032
diff
changeset

795 
unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

796 
by (rule mult_strict_right_mono, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

797 
hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

798 
thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False] 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

799 
unfolding pow2_minus pow2_int minus_minus by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

800 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

801 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

802 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

803 
lemma approx_rat_pattern: fixes P and ps :: "nat * int * int" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

804 
assumes Y: "\<And>y prec x. \<lbrakk>y = 0; ps = (prec, x, 0)\<rbrakk> \<Longrightarrow> P" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

805 
and A: "\<And>x y prec. \<lbrakk>0 \<le> x; 0 < y; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

806 
and B: "\<And>x y prec. \<lbrakk>x < 0; 0 < y; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

807 
and C: "\<And>x y prec. \<lbrakk>x < 0; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

808 
and D: "\<And>x y prec. \<lbrakk>0 \<le> x; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

809 
shows P 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

810 
proof  
41528  811 
obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps) auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

812 
from Y have "y = 0 \<Longrightarrow> P" by auto 
41528  813 
moreover { 
814 
assume "0 < y" 

815 
have P 

816 
proof (cases "0 \<le> x") 

817 
case True 

818 
with A and `0 < y` show P by auto 

819 
next 

820 
case False 

821 
with B and `0 < y` show P by auto 

822 
qed 

823 
} 

824 
moreover { 

825 
assume "y < 0" 

826 
have P 

827 
proof (cases "0 \<le> x") 

828 
case True 

829 
with D and `y < 0` show P by auto 

830 
next 

831 
case False 

832 
with C and `y < 0` show P by auto 

833 
qed 

834 
} 

835 
ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0") auto 

16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

836 
qed 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

837 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

838 
function lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

839 
where 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

840 
"y = 0 \<Longrightarrow> lapprox_rat prec x y = 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

841 
 "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> lapprox_rat prec x y = lapprox_posrat prec x y" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

842 
 "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> lapprox_rat prec x y =  (rapprox_posrat prec (x) y)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

843 
 "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> lapprox_rat prec x y = lapprox_posrat prec (x) (y)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

844 
 "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> lapprox_rat prec x y =  (rapprox_posrat prec x (y))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

845 
apply simp_all by (rule approx_rat_pattern) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

846 
termination by lexicographic_order 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

847 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

848 
lemma compute_lapprox_rat[code]: 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

849 
"lapprox_rat prec x y = (if y = 0 then 0 else if 0 \<le> x then (if 0 < y then lapprox_posrat prec x y else  (rapprox_posrat prec x (y))) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

850 
else (if 0 < y then  (rapprox_posrat prec (x) y) else lapprox_posrat prec (x) (y)))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

851 
by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

852 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

853 
lemma lapprox_rat: "real (lapprox_rat prec x y) \<le> real x / real y" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

854 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

855 
have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

856 
show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

857 
apply (case_tac "y = 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

858 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

859 
apply (case_tac "0 \<le> x \<and> 0 < y") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

860 
apply (simp add: lapprox_posrat) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

861 
apply (case_tac "x < 0 \<and> 0 < y") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

862 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

863 
apply (subst minus_le_iff) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

864 
apply (rule h[OF rapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

865 
apply (simp_all) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

866 
apply (case_tac "x < 0 \<and> y < 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

867 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

868 
apply (rule h[OF _ lapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

869 
apply (simp_all) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

870 
apply (case_tac "0 \<le> x \<and> y < 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

871 
apply (simp) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

872 
apply (subst minus_le_iff) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

873 
apply (rule h[OF rapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

874 
apply simp_all 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

875 
apply arith 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

876 
done 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

877 
qed 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

878 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

879 
lemma lapprox_rat_bottom: assumes "0 \<le> x" and "0 < y" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

880 
shows "real (x div y) \<le> real (lapprox_rat n x y)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

881 
unfolding lapprox_rat.simps(2)[OF assms] using lapprox_posrat_bottom[OF `0<y`] . 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

882 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

883 
function rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

884 
where 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

885 
"y = 0 \<Longrightarrow> rapprox_rat prec x y = 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

886 
 "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> rapprox_rat prec x y = rapprox_posrat prec x y" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

887 
 "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> rapprox_rat prec x y =  (lapprox_posrat prec (x) y)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

888 
 "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> rapprox_rat prec x y = rapprox_posrat prec (x) (y)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

889 
 "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> rapprox_rat prec x y =  (lapprox_posrat prec x (y))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

890 
apply simp_all by (rule approx_rat_pattern) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

891 
termination by lexicographic_order 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

892 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

893 
lemma compute_rapprox_rat[code]: 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

894 
"rapprox_rat prec x y = (if y = 0 then 0 else if 0 \<le> x then (if 0 < y then rapprox_posrat prec x y else  (lapprox_posrat prec x (y))) else 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

895 
(if 0 < y then  (lapprox_posrat prec (x) y) else rapprox_posrat prec (x) (y)))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

896 
by auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

897 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

898 
lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

899 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

900 
have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

901 
show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

902 
apply (case_tac "y = 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

903 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

904 
apply (case_tac "0 \<le> x \<and> 0 < y") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

905 
apply (simp add: rapprox_posrat) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

906 
apply (case_tac "x < 0 \<and> 0 < y") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

907 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

908 
apply (subst le_minus_iff) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

909 
apply (rule h[OF _ lapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

910 
apply (simp_all) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

911 
apply (case_tac "x < 0 \<and> y < 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

912 
apply simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

913 
apply (rule h[OF rapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

914 
apply (simp_all) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

915 
apply (case_tac "0 \<le> x \<and> y < 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

916 
apply (simp) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

917 
apply (subst le_minus_iff) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

918 
apply (rule h[OF _ lapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

919 
apply simp_all 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

920 
apply arith 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

921 
done 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

922 
qed 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

923 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

924 
lemma rapprox_rat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

925 
shows "real (rapprox_rat n x y) \<le> 1" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

926 
unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`] using rapprox_posrat_le1[OF assms] . 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

927 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

928 
lemma rapprox_rat_neg: assumes "x < 0" and "0 < y" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

929 
shows "real (rapprox_rat n x y) \<le> 0" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

930 
unfolding rapprox_rat.simps(3)[OF assms] using lapprox_posrat_nonneg[of "x" y n] assms by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

931 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

932 
lemma rapprox_rat_nonneg_neg: assumes "0 \<le> x" and "y < 0" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

933 
shows "real (rapprox_rat n x y) \<le> 0" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

934 
unfolding rapprox_rat.simps(5)[OF assms] using lapprox_posrat_nonneg[of x "y" n] assms by auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

935 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

936 
lemma rapprox_rat_nonpos_pos: assumes "x \<le> 0" and "0 < y" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

937 
shows "real (rapprox_rat n x y) \<le> 0" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

938 
proof (cases "x = 0") 
41528  939 
case True 
940 
hence "0 \<le> x" by auto show ?thesis 

941 
unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`] 

942 
unfolding True rapprox_posrat_def Let_def 

943 
by auto 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

944 
next 
41528  945 
case False 
946 
hence "x < 0" using assms by auto 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

947 
show ?thesis using rapprox_rat_neg[OF `x < 0` `0 < y`] . 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

948 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

949 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

950 
fun float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

951 
where 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

952 
"float_divl prec (Float m1 s1) (Float m2 s2) = 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

953 
(let 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

954 
l = lapprox_rat prec m1 m2; 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

955 
f = Float 1 (s1  s2) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

956 
in 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

957 
f * l)" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

958 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

959 
lemma float_divl: "real (float_divl prec x y) \<le> real x / real y" 
45772  960 
using lapprox_rat[of prec "mantissa x" "mantissa y"] 
961 
by (cases x y rule: float.exhaust[case_product float.exhaust]) 

962 
(simp split: split_if_asm 

963 
add: real_of_float_simp pow2_diff field_simps le_divide_eq mult_less_0_iff zero_less_mult_iff) 

16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

964 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

965 
lemma float_divl_lower_bound: assumes "0 \<le> x" and "0 < y" shows "0 \<le> float_divl prec x y" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

966 
proof (cases x, cases y) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

967 
fix xm xe ym ye :: int 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

968 
assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye" 
41528  969 
have "0 \<le> xm" 
970 
using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] 

971 
by auto 

972 
have "0 < ym" 

973 
using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] 

974 
by auto 

16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

975 

41528  976 
have "\<And>n. 0 \<le> real (Float 1 n)" 
977 
unfolding real_of_float_simp using zero_le_pow2 by auto 

978 
moreover have "0 \<le> real (lapprox_rat prec xm ym)" 

979 
apply (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]]) 

980 
apply (auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`]) 

981 
done 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

982 
ultimately show "0 \<le> float_divl prec x y" 
41528  983 
unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0 
984 
by (auto intro!: mult_nonneg_nonneg) 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

985 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

986 

41528  987 
lemma float_divl_pos_less1_bound: 
988 
assumes "0 < x" and "x < 1" and "0 < prec" 

989 
shows "1 \<le> float_divl prec 1 x" 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

990 
proof (cases x) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

991 
case (Float m e) 
41528  992 
from `0 < x` `x < 1` have "0 < m" "e < 0" 
993 
using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

994 
let ?b = "nat (bitlen m)" and ?e = "nat (e)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

995 
have "1 \<le> m" and "m \<noteq> 0" using `0 < m` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

996 
with bitlen_bounds[OF `0 < m`] have "m < 2^?b" and "(2::int) \<le> 2^?b" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

997 
hence "1 \<le> bitlen m" using power_le_imp_le_exp[of "2::int" 1 ?b] by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

998 
hence pow_split: "nat (int prec + bitlen m  1) = (prec  1) + ?b" using `0 < prec` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

999 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1000 
have pow_not0: "\<And>x. (2::real)^x \<noteq> 0" by auto 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1001 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1002 
from float_less1_mantissa_bound `0 < x` `x < 1` Float 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1003 
have "m < 2^?e" by auto 
41528  1004 
with bitlen_bounds[OF `0 < m`, THEN conjunct1] have "(2::int)^nat (bitlen m  1) < 2^?e" 
1005 
by (rule order_le_less_trans) 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1006 
from power_less_imp_less_exp[OF _ this] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1007 
have "bitlen m \<le>  e" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1008 
hence "(2::real)^?b \<le> 2^?e" by auto 
41528  1009 
hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)" 
1010 
by (rule mult_right_mono) auto 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1011 
hence "(1::real) \<le> 2^?e * inverse (2^?b)" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1012 
also 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1013 
let ?d = "real (2 ^ nat (int prec + bitlen m  1) div m) * inverse (2 ^ nat (int prec + bitlen m  1))" 
41528  1014 
{ 
1015 
have "2^(prec  1) * m \<le> 2^(prec  1) * 2^?b" 

1016 
using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto 

1017 
also have "\<dots> = 2 ^ nat (int prec + bitlen m  1)" 

44766  1018 
unfolding pow_split power_add by auto 
41528  1019 
finally have "2^(prec  1) * m div m \<le> 2 ^ nat (int prec + bitlen m  1) div m" 
1020 
using `0 < m` by (rule zdiv_mono1) 

1021 
hence "2^(prec  1) \<le> 2 ^ nat (int prec + bitlen m  1) div m" 

1022 
unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] . 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1023 
hence "2^(prec  1) * inverse (2 ^ nat (int prec + bitlen m  1)) \<le> ?d" 
41528  1024 
unfolding real_of_int_le_iff[of "2^(prec  1)", symmetric] by auto 
1025 
} 

1026 
from mult_left_mono[OF this [unfolded pow_split power_add inverse_mult_distrib mult_assoc[symmetric] right_inverse[OF pow_not0] mult_1_left], of "2^?e"] 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1027 
have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1028 
finally have "1 \<le> 2^?e * ?d" . 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1029 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1030 
have e_nat: "0  e = int (nat (e))" using `e < 0` by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1031 
have "bitlen 1 = 1" using bitlen.simps by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1032 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1033 
show ?thesis 
41528  1034 
unfolding one_float_def Float float_divl.simps Let_def 
1035 
lapprox_rat.simps(2)[OF zero_le_one `0 < m`] 

1036 
lapprox_posrat_def `bitlen 1 = 1` 

1037 
unfolding le_float_def real_of_float_mult normfloat real_of_float_simp 

1038 
pow2_minus pow2_int e_nat 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1039 
using `1 \<le> 2^?e * ?d` by (auto simp add: pow2_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1040 
qed 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1041 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1042 
fun float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1043 
where 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1044 
"float_divr prec (Float m1 s1) (Float m2 s2) = 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1045 
(let 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1046 
r = rapprox_rat prec m1 m2; 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1047 
f = Float 1 (s1  s2) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1048 
in 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1049 
f * r)" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1050 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1051 
lemma float_divr: "real x / real y \<le> real (float_divr prec x y)" 
45772  1052 
using rapprox_rat[of "mantissa x" "mantissa y" prec] 
1053 
by (cases x y rule: float.exhaust[case_product float.exhaust]) 

1054 
(simp split: split_if_asm 

1055 
add: real_of_float_simp pow2_diff field_simps divide_le_eq mult_less_0_iff zero_less_mult_iff) 

16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1056 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1057 
lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1058 
proof  
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1059 
have "1 \<le> 1 / real x" using `0 < x` and `x < 1` unfolding less_float_def by auto 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1060 
also have "\<dots> \<le> real (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1061 
finally show ?thesis unfolding le_float_def by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1062 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1063 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1064 
lemma float_divr_nonpos_pos_upper_bound: assumes "x \<le> 0" and "0 < y" shows "float_divr prec x y \<le> 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1065 
proof (cases x, cases y) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1066 
fix xm xe ym ye :: int 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1067 
assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1068 
have "xm \<le> 0" using `x \<le> 0`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 mult_le_0_iff] by auto 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1069 
have "0 < ym" using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1070 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1071 
have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1072 
moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonpos_pos[OF `xm \<le> 0` `0 < ym`] . 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1073 
ultimately show "float_divr prec x y \<le> 0" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1074 
unfolding x_eq y_eq float_divr.simps Let_def le_float_def real_of_float_0 real_of_float_mult by (auto intro!: mult_nonneg_nonpos) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1075 
qed 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1076 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1077 
lemma float_divr_nonneg_neg_upper_bound: assumes "0 \<le> x" and "y < 0" shows "float_divr prec x y \<le> 0" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1078 
proof (cases x, cases y) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1079 
fix xm xe ym ye :: int 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1080 
assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1081 
have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] by auto 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1082 
have "ym < 0" using `y < 0`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 mult_less_0_iff] by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1083 
hence "0 <  ym" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1084 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1085 
have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1086 
moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonneg_neg[OF `0 \<le> xm` `ym < 0`] . 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1087 
ultimately show "float_divr prec x y \<le> 0" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1088 
unfolding x_eq y_eq float_divr.simps Let_def le_float_def real_of_float_0 real_of_float_mult by (auto intro!: mult_nonneg_nonpos) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1089 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1090 

30960  1091 
primrec round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1092 
"round_down prec (Float m e) = (let d = bitlen m  int prec in 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1093 
if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1094 
else Float m e)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1095 

30960  1096 
primrec round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1097 
"round_up prec (Float m e) = (let d = bitlen m  int prec in 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1098 
if 0 < d then let P = 2^nat d ; n = m div P ; r = m mod P in Float (n + (if r = 0 then 0 else 1)) (e + d) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1099 
else Float m e)" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1100 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1101 
lemma round_up: "real x \<le> real (round_up prec x)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1102 
proof (cases x) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1103 
case (Float m e) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1104 
let ?d = "bitlen m  int prec" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1105 
let ?p = "(2::int)^nat ?d" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1106 
have "0 < ?p" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1107 
show "?thesis" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1108 
proof (cases "0 < ?d") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1109 
case True 
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35032
diff
changeset

1110 
hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1111 
show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1112 
proof (cases "m mod ?p = 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1113 
case True 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1114 
have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right, symmetric] . 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1115 
have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

1116 
by (auto simp add: pow2_add `0 < ?d` pow_d) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1117 
thus ?thesis 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

1118 
unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

1119 
by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1120 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1121 
case False 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1122 
have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] .. 
44766  1123 
also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib mult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le]) 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1124 
finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

1125 
unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

1126 
by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1127 
thus ?thesis 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

1128 
unfolding Float round_up.simps Let_def if_not_P[OF `\<not> m mod ?p = 0`] if_P[OF `0 < ?d`] . 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1129 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1130 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1131 
case False 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1132 
show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1133 
unfolding Float round_up.simps Let_def if_not_P[OF False] .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1134 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1135 
qed 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1136 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1137 
lemma round_down: "real (round_down prec x) \<le> real x" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1138 
proof (cases x) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1139 
case (Float m e) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1140 
let ?d = "bitlen m  int prec" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1141 
let ?p = "(2::int)^nat ?d" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1142 
have "0 < ?p" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1143 
show "?thesis" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1144 
proof (cases "0 < ?d") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1145 
case True 
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35032
diff
changeset

1146 
hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1147 
have "m div ?p * ?p \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1148 
also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] .. 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1149 
finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e] 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1150 
unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1151 
by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1152 
thus ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1153 
unfolding Float round_down.simps Let_def if_P[OF `0 < ?d`] . 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1154 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1155 
case False 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1156 
show ?thesis 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1157 
unfolding Float round_down.simps Let_def if_not_P[OF False] .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1158 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1159 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1160 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1161 
definition lb_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1162 
"lb_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1163 
l = bitlen m  int prec 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1164 
in if l > 0 then Float (m div (2^nat l)) (e + l) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1165 
else Float m e)" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1166 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1167 
definition ub_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1168 
"ub_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1169 
l = bitlen m  int prec 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1170 
in if l > 0 then Float (m div (2^nat l) + 1) (e + l) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1171 
else Float m e)" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1172 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1173 
lemma lb_mult: "real (lb_mult prec x y) \<le> real (x * y)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1174 
proof (cases "normfloat (x * y)") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1175 
case (Float m e) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1176 
hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1177 
let ?l = "bitlen m  int prec" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1178 
have "real (lb_mult prec x y) \<le> real (normfloat (x * y))" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1179 
proof (cases "?l > 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1180 
case False thus ?thesis unfolding lb_mult_def Float Let_def float.cases by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1181 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1182 
case True 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1183 
have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1184 
proof  
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35032
diff
changeset

1185 
have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power real_number_of unfolding pow2_int[symmetric] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

1186 
using `?l > 0` by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1187 
also have "\<dots> \<le> real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding real_of_int_add by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1188 
also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1189 
finally show ?thesis by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1190 
qed 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

1191 
thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add mult_commute mult_assoc by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1192 
qed 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1193 
also have "\<dots> = real (x * y)" unfolding normfloat .. 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1194 
finally show ?thesis . 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1195 
qed 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1196 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1197 
lemma ub_mult: "real (x * y) \<le> real (ub_mult prec x y)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1198 
proof (cases "normfloat (x * y)") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1199 
case (Float m e) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1200 
hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1201 
let ?l = "bitlen m  int prec" 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1202 
have "real (x * y) = real (normfloat (x * y))" unfolding normfloat .. 
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1203 
also have "\<dots> \<le> real (ub_mult prec x y)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1204 
proof (cases "?l > 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1205 
case False thus ?thesis unfolding ub_mult_def Float Let_def float.cases by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1206 
next 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1207 
case True 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1208 
have "real m \<le> real (m div 2^(nat ?l) + 1) * pow2 ?l" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1209 
proof  
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1210 
have "m mod 2^(nat ?l) < 2^(nat ?l)" by (rule pos_mod_bound) auto 
44766  1211 
hence mod_uneq: "real (m mod 2^(nat ?l)) \<le> 1 * 2^(nat ?l)" unfolding mult_1 real_of_int_less_iff[symmetric] by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1212 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1213 
have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1214 
also have "\<dots> = real (m div 2^(nat ?l)) * 2^(nat ?l) + real (m mod 2^(nat ?l))" unfolding real_of_int_add by auto 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

1215 
also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding left_distrib using mod_uneq by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1216 
finally show ?thesis unfolding pow2_int[symmetric] using True by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1217 
qed 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

1218 
thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add mult_commute mult_assoc by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1219 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1220 
finally show ?thesis . 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1221 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1222 

30960  1223 
primrec float_abs :: "float \<Rightarrow> float" where 
1224 
"float_abs (Float m e) = Float \<bar>m\<bar> e" 

29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1225 

e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1226 
instantiation float :: abs begin 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1227 
definition abs_float_def: "\<bar>x\<bar> = float_abs x" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1228 
instance .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1229 
end 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1230 

31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1231 
lemma real_of_float_abs: "real \<bar>x :: float\<bar> = \<bar>real x\<bar>" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1232 
proof (cases x) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1233 
case (Float m e) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1234 
have "\<bar>real m\<bar> * pow2 e = \<bar>real m * pow2 e\<bar>" unfolding abs_mult by auto 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1235 
thus ?thesis unfolding Float abs_float_def float_abs.simps real_of_float_simp by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1236 
qed 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1237 

30960  1238 
primrec floor_fl :: "float \<Rightarrow& 