author  huffman 
Sun, 25 Mar 2012 20:15:39 +0200  
changeset 47108  2a1953f0d20d 
parent 46670  e9aa6d151329 
child 47165  9344891b504b 
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 

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

13 
[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

14 

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

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

16 

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

17 
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

18 
"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

19 

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 
defs (overloaded) 
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31863
diff
changeset

21 
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

22 

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

25 

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

26 
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

27 
"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

28 

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 
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

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

31 

46573  32 
instantiation float :: zero 
33 
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 

46573  38 
instantiation float :: one 
39 
begin 

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

40 
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

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

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

43 

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

44 
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

45 
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

46 

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

47 
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

48 
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

49 
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

50 

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

51 
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

52 
"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

53 
"real (Float 1 1) = 1/2" and "real (Float 1 2) = 1/4" and "real (Float 1 3) = 1/8" and 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

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

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

56 

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

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

59 

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

60 
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

61 
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

62 
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

63 

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

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

65 
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

66 

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

67 
declare pow2_def[simp del] 
19765  68 

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

69 
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

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

71 

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

72 
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

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

74 

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

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

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

77 

41528  78 
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

79 

41528  80 
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

81 

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

82 
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

83 

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

84 
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

85 

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

86 
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

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

88 

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

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

92 
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

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

94 
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

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

96 

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

97 
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

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

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

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

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

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

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

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

106 
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

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

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

109 

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

110 
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

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

112 

26313  113 
lemma pow2_int: "pow2 (int c) = 2^c" 
46573  114 
by (simp add: pow2_def) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

115 

46573  116 
lemma zero_less_pow2[simp]: "0 < pow2 x" 
45495
c55a07526dbe
cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents:
44766
diff
changeset

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

118 

46573  119 
lemma normfloat_imp_odd_or_zero: 
120 
"normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)" 

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

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

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

123 
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

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

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

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

127 
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

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

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

130 
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

131 
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

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

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

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

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

136 
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

137 
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

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

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

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

141 
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

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

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

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

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

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

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

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

149 
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

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

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

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

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

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

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

156 

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

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

158 
assumes odd: "odd a'" 
46573  159 
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

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

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

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

163 
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

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

165 

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

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

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

168 
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

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

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

171 
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

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

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

174 
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

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

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

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

178 

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

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

180 
assumes odd1: "odd a" 
46573  181 
and odd2: "odd a'" 
182 
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

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

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

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

186 
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

187 
float_eq_odd_helper[OF odd1 floateq[symmetric]] 
41528  188 
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

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

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

191 

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

192 
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

193 
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

194 
shows "normfloat f = normfloat g" 
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 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

197 
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

198 
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

199 
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

200 
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

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

202 
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

203 
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

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

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

207 
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

208 
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

209 
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

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

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

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

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

214 
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

215 
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

216 
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

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

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

219 
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

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

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

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

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

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

225 

46573  226 
instantiation float :: plus 
227 
begin 

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

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

229 
[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

230 
(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

231 
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

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

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

234 

46573  235 
instantiation float :: uminus 
236 
begin 

30960  237 
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

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

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

240 

46573  241 
instantiation float :: minus 
242 
begin 

243 
definition minus_float where "(z::float)  w = z + ( w)" 

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

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

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

246 

46573  247 
instantiation float :: times 
248 
begin 

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

249 
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

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

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

252 

30960  253 
primrec float_pprt :: "float \<Rightarrow> float" where 
254 
"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

255 

30960  256 
primrec float_nprt :: "float \<Rightarrow> float" where 
257 
"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

258 

46573  259 
instantiation float :: ord 
260 
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

261 
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

262 
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

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

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

265 

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

266 
lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)" 
41528  267 
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

268 
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

269 

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

270 
lemma real_of_float_minus[simp]: "real ( a) =  real (a :: float)" 
46573  271 
by (cases a) simp 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

272 

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

273 
lemma real_of_float_sub[simp]: "real (a  b) = real a  real (b :: float)" 
41528  274 
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

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_mult[simp]: "real (a*b) = real a * real (b :: float)" 
41528  277 
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

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_0[simp]: "real (0 :: float) = 0" 
46573  280 
by (auto simp add: zero_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_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

283 
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

284 

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

285 
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

286 
"(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

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

288 
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

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

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

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

292 

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

293 
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

294 
"(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

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

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

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

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

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

300 

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

301 
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

302 
"(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

303 
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

304 
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

305 
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

306 
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

307 
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

308 

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 
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

310 
"(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

311 
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

312 
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

313 
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

314 
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

315 
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

316 

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

317 
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

318 

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

319 
lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)" 
41528  320 
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

321 

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

322 
lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)" 
41528  323 
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

324 

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

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

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

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

328 
show "a + b + c = a + (b + c)" 
41528  329 
by (cases a, cases b, cases c) 
330 
(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

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

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

333 
show "a + b = b + a" 
41528  334 
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

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

336 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

337 
instance float :: numeral .. 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

338 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

339 
lemma Float_add_same_scale: "Float x e + Float y e = Float (x + y) e" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

340 
by (simp add: plus_float.simps) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

341 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

342 
(* FIXME: define other constant for code_unfold_post *) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

343 
lemma numeral_float_Float (*[code_unfold_post]*): 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

344 
"numeral k = Float (numeral k) 0" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

345 
by (induct k, simp_all only: numeral.simps one_float_def 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

346 
Float_add_same_scale) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

347 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

348 
lemma float_number_of[simp]: "real (numeral x :: float) = numeral x" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

349 
by (simp only: numeral_float_Float Float_num) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

350 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

351 

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

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

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

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

355 
show "a * b * c = a * (b * c)" 
41528  356 
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

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

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

359 
show "a * b = b * a" 
41528  360 
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

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

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

363 
show "1 * a = a" 
41528  364 
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

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

366 

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

367 
(* 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

368 
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

369 
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

370 

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

371 
instance float :: comm_semiring 
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 
fix a b c :: float 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

374 
show "(a + b) * c = a * c + b * c" 
41528  375 
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

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

377 

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

378 
(* 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

379 

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

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

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

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

383 
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

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

385 

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

386 
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

387 
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

388 

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

389 
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

390 
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

391 

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

392 
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

393 
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

394 

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

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

397 

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

398 
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

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

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

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

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

403 

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

404 
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

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

406 
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

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

408 
apply simp 
24301  409 
done 
410 

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

411 
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

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

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

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

415 
apply simp 
24301  416 
done 
417 

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

418 
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

419 
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

420 
by auto 
19765  421 

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

422 
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

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

424 
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

425 
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

426 

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

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

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

429 
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

430 
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

431 
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

432 
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

433 
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

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

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

436 

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

437 
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

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

439 
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

440 
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

441 
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

442 
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

443 
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

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

445 
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

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

447 

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

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

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

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

451 
"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

452 
"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

453 
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

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

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

456 
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

457 

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

458 
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

459 
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

460 

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

461 
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

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

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

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

465 
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

466 
{ 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

467 

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

468 
have "0 < (2::int)" 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 
show "?P x" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

472 
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

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

474 
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

475 
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

476 
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

477 
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

478 

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

479 
{ 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

480 
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

481 
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

482 
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

483 
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

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

485 
{ 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

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

487 
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

488 
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

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

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

491 
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

492 
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

493 
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

494 
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

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

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

497 
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

498 
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

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

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

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

502 
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

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

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

505 

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

506 
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

507 
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

508 

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

509 
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

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

511 
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

512 

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

513 
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

514 
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

515 
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

516 

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

517 
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

518 
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

519 

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

520 
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

521 
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

522 
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

523 
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

524 
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

525 
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

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

527 

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

528 
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

529 
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

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

531 
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

532 
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

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

534 
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

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

536 
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

537 
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

538 
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

539 
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

540 
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

541 
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

542 
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

543 
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

544 
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

545 
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

546 
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

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

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

549 

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

550 
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

551 
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

552 
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

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

554 
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

555 
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

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

557 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

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

559 
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

560 

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

561 
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

562 

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

563 
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

564 
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

565 
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

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

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

568 
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

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

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

571 

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

572 
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

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

574 
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

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

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

577 
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

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

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

580 
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

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

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

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

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

585 
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

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

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

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

589 

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

590 
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

591 
by (simp add: number_of_is_id) 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

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

593 

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

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

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

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

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

598 
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

599 

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

600 
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

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

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

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

604 
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

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

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

607 

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

608 
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

609 
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

610 

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

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

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

613 
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

614 
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

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

616 
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

617 

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

618 
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

619 
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

620 
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

621 
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

622 
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

623 
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

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

625 

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

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

627 
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

628 
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

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

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

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

633 
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

634 
hence "real (x div y) * real c \<le> real (x * c div y)" 
44766  635 
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

636 
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

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

638 
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

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

640 

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

641 
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

642 
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

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

644 
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

645 
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

646 
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

647 
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

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

649 

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

650 
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

651 
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

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

653 
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

654 
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

655 
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

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

657 

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

658 
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

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

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

661 
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

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

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

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

665 
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

666 

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

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

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

669 
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

670 
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

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

672 
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

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

674 
proof (cases "?X mod y = 0") 
46670  675 
case True hence "y dvd ?X" using `0 < y` by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

676 
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

677 
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

678 
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

679 
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

680 
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

681 
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

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

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

684 
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

685 
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

686 

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

687 
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

688 
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  689 
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

690 
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

691 
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

692 
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

693 
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

694 
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

695 
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

696 
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

697 
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

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

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

700 

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

701 
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

702 
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

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

704 
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

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

706 
proof (cases "?X mod y = 0") 
46670  707 
case True hence "y dvd ?X" using `0 < y` by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

708 
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

709 
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

710 
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

711 
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

712 
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

713 
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

714 
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

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

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

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

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

719 
assume "\<not> x \<noteq> y" hence "x = y" by auto 
30034  720 
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

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

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

723 
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

724 
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

725 

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

726 
from real_of_int_div4[of "?X" y] 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

727 
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_numeral . 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

728 
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

729 
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

730 
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

731 
hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

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

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

734 
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

735 
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

736 
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

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

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

739 

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

740 
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

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

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

743 
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

744 
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

745 
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

746 
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

747 
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

748 
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

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

750 

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

751 
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

752 
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

753 
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

754 
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

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

756 
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

757 
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

758 

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

759 
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

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

761 
proof (cases "?X mod y = 0") 
46670  762 
case True hence "y dvd ?X" using `0 < y` by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

763 
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

764 
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

765 
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

766 
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

767 
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

768 
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

769 
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

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

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

772 
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

773 

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

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

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

776 
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

777 
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

778 
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

779 
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

780 
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

781 

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

782 
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

783 

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

784 
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

785 
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

786 

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

787 
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

788 
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

789 
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

790 
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

791 
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

792 
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

793 
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

794 
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

795 
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

796 
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

797 
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

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

799 

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

800 
from real_of_int_div4[of "?X" y] 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

801 
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_numeral . 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

802 
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

803 
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

804 
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

805 
hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

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

807 
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

808 
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

809 
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

810 
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

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

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

813 

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

814 
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

815 
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

816 
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

817 
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

818 
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

819 
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

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

821 
proof  
41528  822 
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

823 
from Y have "y = 0 \<Longrightarrow> P" by auto 
41528  824 
moreover { 
825 
assume "0 < y" 

826 
have P 

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

828 
case True 

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

830 
next 

831 
case False 

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

833 
qed 

834 
} 

835 
moreover { 

836 
assume "y < 0" 

837 
have P 

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

839 
case True 

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

841 
next 

842 
case False 

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

844 
qed 

845 
} 

846 
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

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

848 

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

849 
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

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

851 
"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

852 
 "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

853 
 "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

854 
 "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

855 
 "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

856 
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

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

858 

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

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

860 
"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

861 
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

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

863 

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

864 
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

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

866 
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

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

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

869 
apply simp 
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> 0 < y") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

872 
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

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

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

875 
apply (rule h[OF rapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

877 
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

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

879 
apply (rule h[OF _ lapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

881 
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

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

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

884 
apply (rule h[OF rapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

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

889 

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

890 
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

891 
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

892 
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

893 

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

894 
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

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

896 
"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

897 
 "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

898 
 "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

899 
 "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

900 
 "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

901 
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

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

903 

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

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

905 
"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

906 
(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

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

908 

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

909 
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

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

911 
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

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

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

914 
apply simp 
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> 0 < y") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

917 
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

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

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

920 
apply (rule h[OF _ lapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

922 
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

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

924 
apply (rule h[OF rapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

926 
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

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

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

929 
apply (rule h[OF _ lapprox_posrat]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

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

934 

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

935 
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

936 
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

937 
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

938 

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

939 
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

940 
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

941 
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

942 

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

943 
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

944 
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

945 
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

946 

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

947 
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

948 
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

949 
proof (cases "x = 0") 
41528  950 
case True 
951 
hence "0 \<le> x" by auto show ?thesis 

952 
unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`] 

953 
unfolding True rapprox_posrat_def Let_def 

954 
by auto 

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

955 
next 
41528  956 
case False 
957 
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

958 
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

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

960 

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

961 
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

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

963 
"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

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

965 
l = lapprox_rat prec m1 m2; 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

966 
f = Float 1 (s1  s2) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

968 
f * l)" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

969 

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

970 
lemma float_divl: "real (float_divl prec x y) \<le> real x / real y" 
45772  971 
using lapprox_rat[of prec "mantissa x" "mantissa y"] 
972 
by (cases x y rule: float.exhaust[case_product float.exhaust]) 

973 
(simp split: split_if_asm 

974 
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

975 

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

976 
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

977 
proof (cases x, cases y) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

978 
fix xm xe ym ye :: int 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

979 
assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye" 
41528  980 
have "0 \<le> xm" 
981 
using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] 

982 
by auto 

983 
have "0 < ym" 

984 
using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] 

985 
by auto 

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

986 

41528  987 
have "\<And>n. 0 \<le> real (Float 1 n)" 
988 
unfolding real_of_float_simp using zero_le_pow2 by auto 

989 
moreover have "0 \<le> real (lapprox_rat prec xm ym)" 

990 
apply (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]]) 

991 
apply (auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`]) 

992 
done 

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

993 
ultimately show "0 \<le> float_divl prec x y" 
41528  994 
unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0 
995 
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

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

997 

41528  998 
lemma float_divl_pos_less1_bound: 
999 
assumes "0 < x" and "x < 1" and "0 < prec" 

1000 
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

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

1002 
case (Float m e) 
41528  1003 
from `0 < x` `x < 1` have "0 < m" "e < 0" 
1004 
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

1005 
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

1006 
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

1007 
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

1008 
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

1009 
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

1010 

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

1011 
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

1012 

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

1013 
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

1014 
have "m < 2^?e" by auto 
41528  1015 
with bitlen_bounds[OF `0 < m`, THEN conjunct1] have "(2::int)^nat (bitlen m  1) < 2^?e" 
1016 
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

1017 
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

1018 
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

1019 
hence "(2::real)^?b \<le> 2^?e" by auto 
41528  1020 
hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)" 
1021 
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

1022 
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

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

1024 
let ?d = "real (2 ^ nat (int prec + bitlen m  1) div m) * inverse (2 ^ nat (int prec + bitlen m  1))" 
41528  1025 
{ 
1026 
have "2^(prec  1) * m \<le> 2^(prec  1) * 2^?b" 

1027 
using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto 

1028 
also have "\<dots> = 2 ^ nat (int prec + bitlen m  1)" 

44766  1029 
unfolding pow_split power_add by auto 
41528  1030 
finally have "2^(prec  1) * m div m \<le> 2 ^ nat (int prec + bitlen m  1) div m" 
1031 
using `0 < m` by (rule zdiv_mono1) 

1032 
hence "2^(prec  1) \<le> 2 ^ nat (int prec + bitlen m  1) div m" 

1033 
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

1034 
hence "2^(prec  1) * inverse (2 ^ nat (int prec + bitlen m  1)) \<le> ?d" 
41528  1035 
unfolding real_of_int_le_iff[of "2^(prec  1)", symmetric] by auto 
1036 
} 

1037 
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

1038 
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

1039 
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

1040 

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

1041 
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

1042 
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

1043 

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

1044 
show ?thesis 
41528  1045 
unfolding one_float_def Float float_divl.simps Let_def 
1046 
lapprox_rat.simps(2)[OF zero_le_one `0 < m`] 

1047 
lapprox_posrat_def `bitlen 1 = 1` 

1048 
unfolding le_float_def real_of_float_mult normfloat real_of_float_simp 

1049 
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

1050 
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

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

1052 

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

1053 
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

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

1055 
"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

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

1057 
r = rapprox_rat prec m1 m2; 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1058 
f = Float 1 (s1  s2) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

1060 
f * r)" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1061 

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

1062 
lemma float_divr: "real x / real y \<le> real (float_divr prec x y)" 
45772  1063 
using rapprox_rat[of "mantissa x" "mantissa y" prec] 
1064 
by (cases x y rule: float.exhaust[case_product float.exhaust]) 

1065 
(simp split: split_if_asm 

1066 
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

1067 

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

1068 
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

1069 
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

1070 
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

1071 
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

1072 
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

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

1074 

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

1075 
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

1076 
proof (cases x, cases y) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1077 
fix xm xe ym ye :: int 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1078 
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

1079 
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

1080 
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

1081 

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

1082 
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

1083 
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

1084 
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

1085 
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

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

1087 

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

1088 
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

1089 
proof (cases x, cases y) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1090 
fix xm xe ym ye :: int 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1091 
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

1092 
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

1093 
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

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

1095 

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

1096 
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

1097 
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

1098 
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

1099 
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

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

1101 

30960  1102 
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

1103 
"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

1104 
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

1105 
else Float m e)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1106 

30960  1107 
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

1108 
"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

1109 
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

1110 
else Float m e)" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1111 

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

1112 
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

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

1114 
case (Float m e) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1115 
let ?d = "bitlen m  int prec" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1116 
let ?p = "(2::int)^nat ?d" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1117 
have "0 < ?p" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

1119 
proof (cases "0 < ?d") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1120 
case True 
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35032
diff
changeset

1121 
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

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

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

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

1125 
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

1126 
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

1127 
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

1128 
thus ?thesis 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

1129 
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

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

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

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

1133 
have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] .. 
44766  1134 
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

1135 
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

1136 
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

1137 
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

1138 
thus ?thesis 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

1139 
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

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

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

1142 
case False 
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 
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

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

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

1147 

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

1148 
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

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

1150 
case (Float m e) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1151 
let ?d = "bitlen m  int prec" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1152 
let ?p = "(2::int)^nat ?d" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1153 
have "0 < ?p" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

1155 
proof (cases "0 < ?d") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1156 
case True 
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35032
diff
changeset

1157 
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

1158 
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

1159 
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

1160 
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

1161 
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

1162 
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

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

1164 
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

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

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

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

1168 
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

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

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

1171 

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

1172 
definition lb_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where 
46573  1173 
"lb_mult prec x y = 
1174 
(case normfloat (x * y) of Float m e \<Rightarrow> 

1175 
let 

1176 
l = bitlen m  int prec 

1177 
in if l > 0 then Float (m div (2^nat l)) (e + l) 

1178 
else Float m e)" 

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

1179 

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

1180 
definition ub_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where 
46573  1181 
"ub_mult prec x y = 
1182 
(case normfloat (x * y) of Float m e \<Rightarrow> 

1183 
let 

1184 
l = bitlen m  int prec 

1185 
in if l > 0 then Float (m div (2^nat l) + 1) (e + l) 

1186 
else Float m e)" 

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

1187 

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

1188 
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

1189 
proof (cases "normfloat (x * y)") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1190 
case (Float m e) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1191 
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

1192 
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

1193 
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

1194 
proof (cases "?l > 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1195 
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

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

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

1198 
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

1199 
proof  
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46670
diff
changeset

1200 
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_numeral unfolding pow2_int[symmetric] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

1201 
using `?l > 0` by auto 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1202 
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

1203 
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

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

1205 
qed 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

1206 
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

1207 
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

1208 
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

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

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

1211 

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

1212 
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

1213 
proof (cases "normfloat (x * y)") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1214 
case (Float m e) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1215 
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

1216 
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

1217 
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

1218 
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

1219 
proof (cases "?l > 0") 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1220 
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

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

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

1223 
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

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

1225 
have "m mod 2^(nat ?l) < 2^(nat ?l)" by (rule pos_mod_bound) auto 
44766  1226 
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

1227 

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

1228 
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

1229 
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

1230 
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

1231 
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

1232 
qed 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

1233 
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

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

1235 
finally show ?thesis . 
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 float_abs :: "float \<Rightarrow> float" where 
1239 
"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
