author  hoelzl 
Mon, 06 Dec 2010 19:54:48 +0100  
changeset 41024  ba961a606c67 
parent 39161  75849a560c09 
child 41528  276078f01ada 
permissions  rwrr 
30122  1 
(* Title: HOL/Library/Float.thy 
2 
Author: Steven Obua 2008 

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

4 
*) 

29988  5 

6 
header {* FloatingPoint Numbers *} 

7 

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

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

11 

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

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

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

15 

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

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

17 

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

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

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

20 

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

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

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

23 

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

26 

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

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

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

29 

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

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

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

32 

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

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

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

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

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

37 

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

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

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

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

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

42 

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

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

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

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

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

47 

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

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

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

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

51 

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

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

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

54 

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

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

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

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

58 

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

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

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

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

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

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

64 

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

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

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

67 

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

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

69 
by (simp add: Float_num[unfolded number_of_is_id] real_of_float_simp pow2_def) 
e391eee8bf14
Implemented taylor series expansion for approximation
hoelzl
parents:
31467
diff
changeset

70 

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

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

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

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

74 

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

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

76 

19765  77 
lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

79 
have h: "! n. nat (2 + int n)  Suc 0 = nat (1 + int n)" by arith 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

80 
have g: "! a b. a  1 = a + (1::int)" by arith 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

81 
have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)" 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

82 
apply (auto, induct_tac n) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

84 
apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if]) 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23365
diff
changeset

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

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

87 
proof (induct a) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

88 
case (1 n) 
29667  89 
from pos show ?case by (simp add: algebra_simps) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

91 
case (2 n) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

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

94 
apply (subst pow2_neg[of " int n"]) 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23365
diff
changeset

95 
apply (subst pow2_neg[of "1  int n"]) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

97 
done 
19765  98 
qed 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

99 
qed 
19765  100 

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

101 
lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)" 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

102 
proof (induct b) 
19765  103 
case (1 n) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

105 
proof (induct n) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

107 
show ?case by simp 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

109 
case (Suc m) 
29667  110 
show ?case by (auto simp add: algebra_simps pow2_add1 prems) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

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

113 
case (2 n) 
19765  114 
show ?case 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

115 
proof (induct n) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

116 
case 0 
19765  117 
show ?case 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

119 
apply (subst pow2_neg[of "a + 1"]) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

120 
apply (subst pow2_neg[of "1"]) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

122 
apply (insert pow2_add1[of "a"]) 
29667  123 
apply (simp add: algebra_simps) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

124 
apply (subst pow2_neg[of "a"]) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

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

127 
case (Suc m) 
19765  128 
have a: "int m  (a + 2) = 1 + (int m  a + 1)" by arith 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

129 
have b: "int m  2 = 1 + (int m + 1)" by arith 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

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

132 
apply (subst pow2_neg[of "a + (2  int m)"]) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

133 
apply (subst pow2_neg[of "2  int m"]) 
29667  134 
apply (auto simp add: algebra_simps) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

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

137 
apply (simp only: pow2_add1) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

138 
apply (subst pow2_neg[of "int m  a + 1"]) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

139 
apply (subst pow2_neg[of "int m + 1"]) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

141 
apply (insert prems) 
29667  142 
apply (auto simp add: algebra_simps) 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

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

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

146 

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

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

148 

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

149 
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

150 

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

151 
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

152 

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

153 
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

154 

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

155 
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

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

157 

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

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

159 
"normfloat (Float a b) = (if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1)) else if a=0 then Float 0 0 else Float a b)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

161 
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

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

163 

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

164 
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

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

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

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

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

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

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

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

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

173 
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

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

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

176 

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

177 
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

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

179 

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

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

182 

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

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

184 
"0 < pow2 x" 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

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

187 
fix y 
19765  188 
have "0 <= y \<Longrightarrow> 0 < pow2 y" 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

189 
by (induct y, induct_tac n, simp_all add: pow2_add) 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

191 
note helper=this 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

193 
apply (case_tac "0 <= x") 
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

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

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

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

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

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

199 

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

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

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

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

203 
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

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

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

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

207 
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

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

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

210 
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

211 
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

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

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

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

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

216 
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

217 
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

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

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

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

221 
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

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

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

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

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

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

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

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

229 
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

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

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

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

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

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

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

236 

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

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

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

239 
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

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

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

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

243 
assume bcmp: "b > b'" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

244 
from floateq have eq: "real a * pow2 b = real a' * pow2 b'" by simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

248 
then have "(x * inverse y = z) = (x = z * y)" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32069
diff
changeset

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

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

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

252 
have eq': "real a * (pow2 (b  b')) = real a'" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

255 
apply (subst pow2_neg[where x = "b'"]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

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

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

261 
have "\<exists> z > 0. pow2 (bb') = 2^z" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

262 
apply (rule exI[where x="nat (b  b')"]) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

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

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

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

269 
then obtain z where z: "z > 0 \<and> pow2 (bb') = 2^z" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

270 
with eq' have "real a * 2^z = real a'" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

272 
then have "real a * real ((2::int)^z) = real a'" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

274 
then have "real (a * 2^z) = real a'" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

278 
then have a'_rep: "a * 2^z = a'" by arith 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

279 
then have "a' = a*2^z" by simp 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

281 
with odd have False by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

285 

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

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

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

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

289 
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

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

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

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

293 
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

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

295 
have beq: "b = b'" by arith 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

298 

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

299 
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

300 
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

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

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

303 
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

304 
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

305 
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

306 
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

307 
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

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

309 
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

310 
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

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

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

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

314 
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

315 
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

316 
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

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

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

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

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

321 
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

322 
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

323 
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

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

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

326 
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

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

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

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

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

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

332 

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

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

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

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

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

337 
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

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

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

340 

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

341 
instantiation float :: uminus begin 
30960  342 
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

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

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

345 

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

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

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

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

350 

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

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

352 
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

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

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

355 

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

358 

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

361 

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

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

363 
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

364 
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

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

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

367 

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

368 
lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

369 
by (cases a, cases b, simp add: algebra_simps plus_float.simps, 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

370 
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

371 

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

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

373 
by (cases a, simp add: uminus_float.simps) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

374 

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

375 
lemma real_of_float_sub[simp]: "real (a  b) = real a  real (b :: float)" 
30960  376 
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

377 

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

378 
lemma real_of_float_mult[simp]: "real (a*b) = real a * real (b :: float)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

379 
by (cases a, cases b, simp add: times_float.simps pow2_add) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

380 

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

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

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

383 

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

384 
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

385 
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

386 

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

387 
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

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

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

390 
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

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

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

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

394 

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

395 
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

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

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

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

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

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

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

402 

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

403 
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

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

405 
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

406 
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

407 
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

408 
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

409 
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

410 

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

411 
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

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

413 
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

414 
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

415 
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

416 
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

417 
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

418 

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

420 

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

421 
lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

422 
by (cases a, auto simp add: float_pprt.simps zero_le_float float_le_zero float_zero) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

423 

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

424 
lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

425 
by (cases a, auto simp add: float_nprt.simps zero_le_float float_le_zero float_zero) 
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 
instance float :: ab_semigroup_add 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

430 
show "a + b + c = a + (b + c)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

431 
by (cases a, cases b, cases c, auto simp add: algebra_simps power_add[symmetric] plus_float.simps) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

434 
show "a + b = b + a" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

435 
by (cases a, cases b, simp add: plus_float.simps) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

437 

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

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

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

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

441 
show "a * b * c = a * (b * c)" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

442 
by (cases a, cases b, cases c, simp add: times_float.simps) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

445 
show "a * b = b * a" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

446 
by (cases a, cases b, simp add: times_float.simps) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

449 
show "1 * a = a" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

450 
by (cases a, simp add: times_float.simps one_float_def) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

452 

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

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

454 
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

455 
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

456 

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

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

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

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

460 
show "(a + b) * c = a * c + b * c" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

461 
by (cases a, cases b, cases c, simp, simp add: plus_float.simps times_float.simps algebra_simps) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

463 

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

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

465 

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

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

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

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

469 
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

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

471 

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

472 
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

473 
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

474 

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

475 
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

476 
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

477 

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

478 
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

479 
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

480 

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

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

483 

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

484 
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

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

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

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

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

489 

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

490 
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

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

492 
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

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

494 
apply simp 
24301  495 
done 
496 

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

497 
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

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

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

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

501 
apply simp 
24301  502 
done 
503 

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

504 
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

505 
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

506 
by auto 
19765  507 

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

508 
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

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

510 
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

511 
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

512 

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

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

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

515 
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

516 
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

517 
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

518 
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

519 
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

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

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

522 

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

523 
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

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

525 
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

526 
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

527 
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

528 
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

529 
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

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

531 
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

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

533 

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

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

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

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

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

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

539 
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

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

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

542 
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

543 

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

544 
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

545 
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

546 

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

547 
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

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

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

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

551 
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

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

553 

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

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

555 

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

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

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

558 
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

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

560 
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

561 
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

562 
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

563 
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

564 

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

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

566 
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

567 
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

568 
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

569 
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

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

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

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

573 
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

574 
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

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

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

577 
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

578 
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

579 
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

580 
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

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

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

583 
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

584 
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

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

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

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

588 
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

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

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

591 

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

592 
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

593 
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

594 

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

595 
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

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

597 
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

598 

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

599 
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

600 
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

601 
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

602 

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

603 
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

604 
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

605 

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

606 
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

607 
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

608 
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

609 
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

610 
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

611 
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

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

613 

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

614 
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

615 
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

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

617 
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

618 
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

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

620 
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

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

622 
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

623 
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

624 
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

625 
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

626 
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

627 
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

628 
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

629 
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

630 
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

631 
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

632 
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

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

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

635 

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

636 
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

637 
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

638 
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

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

640 
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

641 
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

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

643 

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

644 
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

645 

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

646 
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

647 

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

648 
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

649 
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

650 
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

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

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

653 
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

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

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

656 

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

657 
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

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

659 
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

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

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

662 
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

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

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

665 
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

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

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

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

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

670 
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

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

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

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

674 

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

675 
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

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

677 

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

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

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

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

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

682 
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

683 

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

684 
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

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

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

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

688 
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

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

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

691 

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

692 
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

693 
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

694 

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

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

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

697 
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

698 
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

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

700 
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

701 

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

702 
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

703 
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

704 
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

705 
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

706 
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

707 
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

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

709 

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

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

711 
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

712 
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

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

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

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

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

717 
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

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

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

720 
hence "real (x div y) * 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

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

722 
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

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

724 

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

725 
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

726 
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

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

728 
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

729 
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

730 
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

731 
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

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

733 

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

734 
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

735 
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

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

737 
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

738 
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

739 
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

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

741 

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

742 
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

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

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

745 
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

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

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

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

749 
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

750 

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

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

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

753 
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

754 
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

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

756 
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

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

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

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

760 
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

761 
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

762 
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

763 
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

764 
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

765 
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

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

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

768 
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

769 
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

770 

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

771 
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

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

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

774 
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

775 
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

776 
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

777 
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

778 
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

779 
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

780 
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

781 
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

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

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

784 

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

785 
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

786 
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

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

788 
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

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

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

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

792 
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

793 
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

794 
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

795 
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

796 
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

797 
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

798 
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

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

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

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

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

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

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

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

807 
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

808 
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

809 

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

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

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

812 
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

813 
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

814 
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

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

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

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

818 
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

819 
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

820 
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

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

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

823 

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

824 
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

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

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

827 
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

828 
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

829 
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

830 
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

831 
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

832 
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

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

834 

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

835 
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

836 
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

837 
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

838 
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

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

840 
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

841 
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

842 

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

843 
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

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

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

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

847 
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

848 
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

849 
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

850 
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

851 
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

852 
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

853 
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

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

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

856 
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

857 

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

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

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

860 
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

861 
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

862 
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

863 
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

864 
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

865 

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

866 
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

867 

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

868 
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

869 
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

870 

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

871 
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

872 
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

873 
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

874 
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

875 
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

876 
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

877 
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

878 
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

879 
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

880 
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

881 
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

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

883 

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

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

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

886 
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

887 
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

888 
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

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

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

891 
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

892 
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

893 
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

894 
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

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

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

897 

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

898 
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

899 
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

900 
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

901 
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

902 
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

903 
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

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

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

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

907 
from Y have "y = 0 \<Longrightarrow> P" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

908 
moreover { assume "0 < y" have P proof (cases "0 \<le> x") case True with A and `0 < y` show P by auto next case False with B and `0 < y` show P by auto qed } 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

909 
moreover { assume "y < 0" have P proof (cases "0 \<le> x") case True with D and `y < 0` show P by auto next case False with C and `y < 0` show P by auto qed } 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

910 
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

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

912 

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

913 
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

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

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

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

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

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

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

920 
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

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

922 

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

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

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

925 
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

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

927 

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

928 
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

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

930 
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

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

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

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

934 
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

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

936 
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

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

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

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

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

941 
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

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

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

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

945 
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

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

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

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

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

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

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

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

953 

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

954 
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

955 
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

956 
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

957 

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

958 
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

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

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

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

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

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

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

965 
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

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

967 

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

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

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

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

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

972 

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

973 
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

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

975 
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

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

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

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

979 
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

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

981 
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

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

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

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

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

986 
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

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

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

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

990 
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

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

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

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

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

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

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

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

998 

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

999 
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

1000 
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

1001 
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

1002 

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

1003 
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

1004 
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

1005 
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

1006 

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

1007 
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

1008 
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

1009 
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

1010 

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

1011 
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

1012 
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

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

1014 
case True hence "0 \<le> x" by auto show ?thesis unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`] 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1015 
unfolding True rapprox_posrat_def Let_def by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

1018 
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

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

1020 

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

1021 
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

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

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

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

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

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

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

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

1029 

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

1030 
lemma float_divl: "real (float_divl 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

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

1032 
from float_split[of x] obtain mx sx where x: "x = Float mx sx" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1033 
from float_split[of y] obtain my sy where y: "y = Float my sy" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1034 
have "real mx / real my \<le> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx  sy))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1051 
then have "real (lapprox_rat prec mx my) \<le> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx  sy))" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1052 
by (rule order_trans[OF lapprox_rat]) 
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

1053 
then have "real (lapprox_rat prec mx my) * pow2 (sx  sy) \<le> real mx * pow2 sx / (real my * pow2 sy)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

1057 
then have "pow2 (sx  sy) * real (lapprox_rat prec mx my) \<le> real mx * pow2 sx / (real my * pow2 sy)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

1060 
by (simp add: x y Let_def real_of_float_simp) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

1062 

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

1063 
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

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

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

1066 
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

1067 
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

1068 
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 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

1069 

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

1071 
moreover have "0 \<le> real (lapprox_rat prec xm ym)" by (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]], auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`]) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1072 
ultimately show "0 \<le> float_divl prec x 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

1073 
unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0 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

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

1075 

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

1076 
lemma float_divl_pos_less1_bound: assumes "0 < x" and "x < 1" and "0 < prec" shows "1 \<le> float_divl prec 1 x" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

1080 
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

1081 
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

1082 
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

1083 
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

1084 
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

1085 

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

1086 
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

1087 

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

1088 
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

1089 
have "m < 2^?e" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

1091 
have "(2::int)^nat (bitlen m  1) < 2^?e" by (rule order_le_less_trans) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1092 
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

1093 
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

1094 
hence "(2::real)^?b \<le> 2^?e" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

1096 
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

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

1098 
let ?d = "real (2 ^ nat (int prec + bitlen m  1) div m) * inverse (2 ^ nat (int prec + bitlen m  1))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1099 
{ have "2^(prec  1) * m \<le> 2^(prec  1) * 2^?b" using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono, auto) 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1100 
also have "\<dots> = 2 ^ nat (int prec + bitlen m  1)" unfolding pow_split zpower_zadd_distrib by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1101 
finally have "2^(prec  1) * m div m \<le> 2 ^ nat (int prec + bitlen m  1) div m" using `0 < m` by (rule zdiv_mono1) 
30181  1102 
hence "2^(prec  1) \<le> 2 ^ nat (int prec + bitlen m  1) div m" 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

1103 
hence "2^(prec  1) * inverse (2 ^ nat (int prec + bitlen m  1)) \<le> ?d" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1104 
unfolding real_of_int_le_iff[of "2^(prec  1)", symmetric] by auto } 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
35344
diff
changeset

1105 
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

1106 
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

1107 
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

1108 

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

1109 
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

1110 
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

1111 

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

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

1113 
unfolding one_float_def Float float_divl.simps Let_def lapprox_rat.simps(2)[OF zero_le_one `0 < m`] lapprox_posrat_def `bitlen 1 = 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

1114 
unfolding le_float_def real_of_float_mult normfloat real_of_float_simp 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

1115 
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

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

1117 

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

1118 
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

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

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

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

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

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

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

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

1126 

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

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

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

1129 
from float_split[of x] obtain mx sx where x: "x = Float mx sx" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1130 
from float_split[of y] obtain my sy where y: "y = Float my sy" by auto 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1131 
have "real mx / real my \<ge> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx  sy))" 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1147 
then have "real (rapprox_rat prec mx my) \<ge> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx  sy))" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1148 
by (rule order_trans[OF _ rapprox_rat]) 
31098
73dd67adf90a
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents:
31021
diff
changeset

1149 
then have "real (rapprox_rat prec mx my) * pow2 (sx  sy) \<ge> real mx * pow2 sx / (real my * pow2 sy)" 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

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

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

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

1154 
by (simp add: x y Let_def algebra_simps real_of_float_simp) 
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

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

1156 

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

1157 
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

1158 
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

1159 
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

1160 
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

1161 
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

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

1163 

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

1164 
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

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

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

1167 
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

1168 
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

1169 
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

1170 

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

1171 
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

1172 
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

1173 
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

1174 
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

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

1176 

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

1177 
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

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

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

1180 
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

1181 
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

1182 
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

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

1184 

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

1185 
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

1186 
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

1187 
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

1188 
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

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

1190 

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

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

1193 
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

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

1195 

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

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

1198 
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

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

1200 

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

1201 
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

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

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

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

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

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

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

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

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

1210 
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

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

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

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

1214 
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

1215 
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

1216 
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

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

1218 
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

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

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

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

1222 
have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] .. 
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset

1223 
also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib zmult_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

1224 
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

1225 
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

1226 
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

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

1228 
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

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

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

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

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

1233 
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

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

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

1236 

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

1237 
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

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

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

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

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

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

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

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

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

1246 
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

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