author | nipkow |
Sat, 21 Feb 2009 09:58:26 +0100 | |
changeset 30034 | 60f64f112174 |
parent 29988 | 747f0c519090 |
child 30122 | 1c912a9d8200 |
permissions | -rw-r--r-- |
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1 |
(* Title: HOL/Library/Float.thy |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
2 |
* Author: Steven Obua 2008 |
29988 | 3 |
* Johannes HÃ\<paragraph>lzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009 |
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
4 |
*) |
29988 | 5 |
|
6 |
header {* Floating-Point Numbers *} |
|
7 |
||
20485 | 8 |
theory Float |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
27366
diff
changeset
|
9 |
imports Complex_Main |
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 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
18 |
fun Ifloat :: "float \<Rightarrow> real" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
19 |
"Ifloat (Float a b) = real a * pow2 b" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21256
diff
changeset
|
20 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
21 |
instantiation float :: zero begin |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
22 |
definition zero_float where "0 = Float 0 0" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
23 |
instance .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
24 |
end |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
25 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
26 |
instantiation float :: one begin |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
27 |
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
|
28 |
instance .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
29 |
end |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
30 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
31 |
instantiation float :: number begin |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
32 |
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
|
33 |
instance .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
34 |
end |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
35 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
36 |
fun mantissa :: "float \<Rightarrow> int" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
37 |
"mantissa (Float a b) = a" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
38 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
39 |
fun scale :: "float \<Rightarrow> int" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
40 |
"scale (Float a b) = b" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
41 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
42 |
lemma Ifloat_neg_exp: "e < 0 \<Longrightarrow> Ifloat (Float m e) = real m * inverse (2^nat (-e))" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
43 |
lemma Ifloat_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> Ifloat (Float m e) = real m * inverse (2^nat (-e))" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
44 |
lemma Ifloat_ge0_exp: "0 \<le> e \<Longrightarrow> Ifloat (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
|
45 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
46 |
lemma Float_num[simp]: shows |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
47 |
"Ifloat (Float 1 0) = 1" and "Ifloat (Float 1 1) = 2" and "Ifloat (Float 1 2) = 4" and |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
48 |
"Ifloat (Float 1 -1) = 1/2" and "Ifloat (Float 1 -2) = 1/4" and "Ifloat (Float 1 -3) = 1/8" and |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
49 |
"Ifloat (Float -1 0) = -1" and "Ifloat (Float (number_of n) 0) = number_of n" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
50 |
by auto |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
51 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
56 |
declare pow2_def[simp del] |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
57 |
|
19765 | 58 |
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
|
59 |
proof - |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
60 |
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
|
61 |
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
|
62 |
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
|
63 |
apply (auto, induct_tac n) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
64 |
apply (simp_all add: pow2_def) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
65 |
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
|
66 |
by (auto simp add: h) |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
67 |
show ?thesis |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
68 |
proof (induct a) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
69 |
case (1 n) |
29667 | 70 |
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
|
71 |
next |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
72 |
case (2 n) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
73 |
show ?case |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
74 |
apply (auto) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
75 |
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
|
76 |
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
|
77 |
apply (auto simp add: g pos) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
78 |
done |
19765 | 79 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
80 |
qed |
19765 | 81 |
|
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
82 |
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
|
83 |
proof (induct b) |
19765 | 84 |
case (1 n) |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
85 |
show ?case |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
86 |
proof (induct n) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
87 |
case 0 |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
88 |
show ?case by simp |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
89 |
next |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
90 |
case (Suc m) |
29667 | 91 |
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
|
92 |
qed |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
93 |
next |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
94 |
case (2 n) |
19765 | 95 |
show ?case |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
96 |
proof (induct n) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
97 |
case 0 |
19765 | 98 |
show ?case |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
99 |
apply (auto) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
100 |
apply (subst pow2_neg[of "a + -1"]) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
101 |
apply (subst pow2_neg[of "-1"]) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
102 |
apply (simp) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
103 |
apply (insert pow2_add1[of "-a"]) |
29667 | 104 |
apply (simp add: algebra_simps) |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
105 |
apply (subst pow2_neg[of "-a"]) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
106 |
apply (simp) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
107 |
done |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
108 |
case (Suc m) |
19765 | 109 |
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
|
110 |
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
|
111 |
show ?case |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
112 |
apply (auto) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
113 |
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
|
114 |
apply (subst pow2_neg[of "-2 - int m"]) |
29667 | 115 |
apply (auto simp add: algebra_simps) |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
116 |
apply (subst a) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
117 |
apply (subst b) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
118 |
apply (simp only: pow2_add1) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
119 |
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
|
120 |
apply (subst pow2_neg[of "int m + 1"]) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
121 |
apply auto |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
122 |
apply (insert prems) |
29667 | 123 |
apply (auto simp add: algebra_simps) |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
124 |
done |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
125 |
qed |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
126 |
qed |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
127 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
128 |
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
|
129 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
130 |
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
|
131 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
132 |
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
|
133 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
134 |
lemma float_zero[simp]: "Ifloat (Float 0 e) = 0" by simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
135 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
136 |
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
|
137 |
by arith |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21256
diff
changeset
|
138 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
139 |
function normfloat :: "float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
140 |
"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
|
141 |
by pat_completeness auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
142 |
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
|
143 |
declare normfloat.simps[simp del] |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
144 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
145 |
theorem normfloat[symmetric, simp]: "Ifloat f = Ifloat (normfloat f)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
146 |
proof (induct f rule: normfloat.induct) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
147 |
case (1 a b) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
148 |
have real2: "2 = real (2::int)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
149 |
by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
150 |
show ?case |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
151 |
apply (subst normfloat.simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
152 |
apply (auto simp add: float_zero) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
153 |
apply (subst 1[symmetric]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
154 |
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
|
155 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
156 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
157 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
158 |
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
|
159 |
by (auto simp add: pow2_def) |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
160 |
|
26313 | 161 |
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
|
162 |
by (simp add: pow2_def) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
163 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
164 |
lemma zero_less_pow2[simp]: |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
165 |
"0 < pow2 x" |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
166 |
proof - |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
167 |
{ |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
168 |
fix y |
19765 | 169 |
have "0 <= y \<Longrightarrow> 0 < pow2 y" |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
170 |
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
|
171 |
} |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
172 |
note helper=this |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
173 |
show ?thesis |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
174 |
apply (case_tac "0 <= x") |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
175 |
apply (simp add: helper) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
176 |
apply (subst pow2_neg) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
177 |
apply (simp add: helper) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
178 |
done |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
179 |
qed |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
180 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
181 |
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
|
182 |
proof (induct f rule: normfloat.induct) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
183 |
case (1 u v) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
184 |
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
|
185 |
{ |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
186 |
assume eu: "even u" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
187 |
assume z: "u \<noteq> 0" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
188 |
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
|
189 |
apply (subst normfloat.simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
190 |
by (simp add: eu z) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
191 |
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
|
192 |
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
|
193 |
} |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
194 |
note case1 = this |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
195 |
{ |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
196 |
assume "odd u \<or> u = 0" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
197 |
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
|
198 |
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
|
199 |
apply (subst normfloat.simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
200 |
apply (simp add: ou) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
201 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
202 |
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
|
203 |
then have ?case |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
204 |
apply (case_tac "u=0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
205 |
apply (auto) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
206 |
by (insert ou, auto) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
207 |
} |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
208 |
note case2 = this |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
209 |
show ?case |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
210 |
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
|
211 |
apply (rule case2) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
212 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
213 |
apply (rule case1) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
214 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
215 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
216 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
217 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
218 |
lemma float_eq_odd_helper: |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
219 |
assumes odd: "odd a'" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
220 |
and floateq: "Ifloat (Float a b) = Ifloat (Float a' b')" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
221 |
shows "b \<le> b'" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
222 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
223 |
{ |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
224 |
assume bcmp: "b > b'" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
225 |
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
|
226 |
{ |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
227 |
fix x y z :: real |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
228 |
assume "y \<noteq> 0" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
229 |
then have "(x * inverse y = z) = (x = z * y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
230 |
by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
231 |
} |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
232 |
note inverse = this |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
233 |
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
|
234 |
apply (subst diff_int_def) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
235 |
apply (subst pow2_add) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
236 |
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
|
237 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
238 |
apply (subst mult_assoc[symmetric]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
239 |
apply (subst inverse) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
240 |
apply (simp_all add: eq) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
241 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
242 |
have "\<exists> z > 0. pow2 (b-b') = 2^z" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
243 |
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
|
244 |
apply (auto) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
245 |
apply (insert bcmp) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
246 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
247 |
apply (subst pow2_int[symmetric]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
248 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
249 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
250 |
then obtain z where z: "z > 0 \<and> pow2 (b-b') = 2^z" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
251 |
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
|
252 |
by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
253 |
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
|
254 |
by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
255 |
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
|
256 |
apply (subst real_of_int_mult) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
257 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
258 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
259 |
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
|
260 |
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
|
261 |
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
|
262 |
with odd have False by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
263 |
} |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
264 |
then show ?thesis by arith |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
265 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
266 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
267 |
lemma float_eq_odd: |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
268 |
assumes odd1: "odd a" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
269 |
and odd2: "odd a'" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
270 |
and floateq: "Ifloat (Float a b) = Ifloat (Float a' b')" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
271 |
shows "a = a' \<and> b = b'" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
272 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
273 |
from |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
274 |
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
|
275 |
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
|
276 |
have beq: "b = b'" by arith |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
277 |
with floateq show ?thesis by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
278 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
279 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
280 |
theorem normfloat_unique: |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
281 |
assumes Ifloat_eq: "Ifloat f = Ifloat g" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
282 |
shows "normfloat f = normfloat g" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
283 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
284 |
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
|
285 |
from float_split[of "normfloat g"] obtain a' b' where normg:"normfloat g = Float a' b'" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
286 |
have "Ifloat (normfloat f) = Ifloat (normfloat g)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
287 |
by (simp add: Ifloat_eq) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
288 |
then have float_eq: "Ifloat (Float a b) = Ifloat (Float a' b')" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
289 |
by (simp add: normf normg) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
290 |
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
|
291 |
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
|
292 |
{ |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
293 |
assume odd: "odd a" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
294 |
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
|
295 |
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
|
296 |
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
|
297 |
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
|
298 |
} |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
299 |
note odd_case = this |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
300 |
{ |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
301 |
assume even: "even a" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
302 |
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
|
303 |
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
|
304 |
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
|
305 |
} |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
306 |
note even_case = this |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
307 |
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
|
308 |
apply (simp add: normf normg) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
309 |
apply (case_tac "even a") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
310 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
311 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
312 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
313 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
314 |
instantiation float :: plus begin |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
315 |
fun plus_float where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
316 |
[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
|
317 |
(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
|
318 |
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
|
319 |
instance .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
320 |
end |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
321 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
322 |
instantiation float :: uminus begin |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
323 |
fun uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
324 |
instance .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
325 |
end |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
326 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
327 |
instantiation float :: minus begin |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
328 |
fun minus_float where [simp del]: "(z::float) - w = z + (- w)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
329 |
instance .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
330 |
end |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
331 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
332 |
instantiation float :: times begin |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
333 |
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
|
334 |
instance .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
335 |
end |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
336 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
337 |
fun float_pprt :: "float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
338 |
"float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
339 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
340 |
fun float_nprt :: "float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
341 |
"float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
342 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
343 |
instantiation float :: ord begin |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
344 |
definition le_float_def: "z \<le> w \<equiv> Ifloat z \<le> Ifloat w" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
345 |
definition less_float_def: "z < w \<equiv> Ifloat z < Ifloat w" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
346 |
instance .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
347 |
end |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
348 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
349 |
lemma Ifloat_add[simp]: "Ifloat (a + b) = Ifloat a + Ifloat b" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
350 |
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
|
351 |
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
|
352 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
353 |
lemma Ifloat_minus[simp]: "Ifloat (- a) = - Ifloat a" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
354 |
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
|
355 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
356 |
lemma Ifloat_sub[simp]: "Ifloat (a - b) = Ifloat a - Ifloat b" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
357 |
by (cases a, cases b, simp add: minus_float.simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
358 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
359 |
lemma Ifloat_mult[simp]: "Ifloat (a*b) = Ifloat a * Ifloat b" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
360 |
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
|
361 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
362 |
lemma Ifloat_0[simp]: "Ifloat 0 = 0" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
363 |
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
|
364 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
365 |
lemma Ifloat_1[simp]: "Ifloat 1 = 1" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
366 |
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
|
367 |
|
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
368 |
lemma zero_le_float: |
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
369 |
"(0 <= Ifloat (Float a b)) = (0 <= a)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
370 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
371 |
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
|
372 |
apply (insert zero_less_pow2[of b]) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
373 |
apply (simp_all) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
374 |
done |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
375 |
|
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
376 |
lemma float_le_zero: |
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
377 |
"(Ifloat (Float a b) <= 0) = (a <= 0)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
378 |
apply auto |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
379 |
apply (auto simp add: mult_le_0_iff) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
380 |
apply (insert zero_less_pow2[of b]) |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
381 |
apply auto |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
382 |
done |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
383 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
384 |
declare Ifloat.simps[simp del] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
385 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
386 |
lemma Ifloat_pprt[simp]: "Ifloat (float_pprt a) = pprt (Ifloat a)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
387 |
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
|
388 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
389 |
lemma Ifloat_nprt[simp]: "Ifloat (float_nprt a) = nprt (Ifloat a)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
390 |
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
|
391 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
392 |
instance float :: ab_semigroup_add |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
393 |
proof (intro_classes) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
394 |
fix a b c :: float |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
395 |
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
|
396 |
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
|
397 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
398 |
fix a b :: float |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
399 |
show "a + b = b + a" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
400 |
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
|
401 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
402 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
403 |
instance float :: comm_monoid_mult |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
404 |
proof (intro_classes) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
405 |
fix a b c :: float |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
406 |
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
|
407 |
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
|
408 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
409 |
fix a b :: float |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
410 |
show "a * b = b * a" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
411 |
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
|
412 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
413 |
fix a :: float |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
414 |
show "1 * a = a" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
415 |
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
|
416 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
417 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
418 |
(* 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
|
419 |
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
|
420 |
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
|
421 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
422 |
instance float :: comm_semiring |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
423 |
proof (intro_classes) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
424 |
fix a b c :: float |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
425 |
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
|
426 |
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
|
427 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
428 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
429 |
(* 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
|
430 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
431 |
instance float :: zero_neq_one |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
432 |
proof (intro_classes) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
433 |
show "(0::float) \<noteq> 1" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
434 |
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
|
435 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
436 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
437 |
lemma float_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
|
438 |
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
|
439 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
440 |
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
|
441 |
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
|
442 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
443 |
lemma Ifloat_min: "Ifloat (min x y) = min (Ifloat x) (Ifloat y)" unfolding min_def le_float_def by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
444 |
lemma Ifloat_max: "Ifloat (max a b) = max (Ifloat a) (Ifloat b)" unfolding max_def le_float_def by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
445 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
446 |
instantiation float :: power begin |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
447 |
fun power_float where [simp del]: "(Float m e) ^ n = Float (m ^ n) (e * int n)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
448 |
instance .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
449 |
end |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
450 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
451 |
instance float :: recpower |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
452 |
proof (intro_classes) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
453 |
fix a :: float show "a ^ 0 = 1" by (cases a, auto simp add: power_float.simps one_float_def) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
454 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
455 |
fix a :: float and n :: nat show "a ^ (Suc n) = a * a ^ n" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
456 |
by (cases a, auto simp add: power_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
|
457 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
458 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
459 |
lemma float_power: "Ifloat (x ^ n) = (Ifloat x) ^ n" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
460 |
proof (cases x) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
461 |
case (Float m e) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
462 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
463 |
have "pow2 e ^ n = pow2 (e * int n)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
464 |
proof (cases "e >= 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
465 |
case True hence e_nat: "e = int (nat e)" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
466 |
hence "pow2 e ^ n = (2 ^ nat e) ^ n" using pow2_int[of "nat e"] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
467 |
thus ?thesis unfolding power_mult[symmetric] unfolding pow2_int[symmetric] int_mult e_nat[symmetric] . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
468 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
469 |
case False hence e_minus: "-e = int (nat (-e))" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
470 |
hence "pow2 (-e) ^ n = (2 ^ nat (-e)) ^ n" using pow2_int[of "nat (-e)"] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
471 |
hence "pow2 (-e) ^ n = pow2 ((-e) * int n)" unfolding power_mult[symmetric] unfolding pow2_int[symmetric] int_mult e_minus[symmetric] zmult_zminus . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
472 |
thus ?thesis unfolding pow2_neg[of "-e"] pow2_neg[of "-e * int n"] unfolding zmult_zminus zminus_zminus nonzero_power_inverse[OF pow2_neq_zero, symmetric] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
473 |
using nonzero_inverse_eq_imp_eq[OF _ pow2_neq_zero pow2_neq_zero] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
474 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
475 |
thus ?thesis by (auto simp add: Float power_mult_distrib Ifloat.simps power_float.simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
476 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
477 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
478 |
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
|
479 |
apply (subgoal_tac "0 < pow2 s") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
480 |
apply (auto simp only:) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
481 |
apply auto |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
482 |
done |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
483 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
484 |
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
|
485 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
486 |
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
|
487 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
488 |
apply simp |
24301 | 489 |
done |
490 |
||
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
491 |
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
|
492 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
493 |
apply (subgoal_tac "0 < pow2 s") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
494 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
495 |
apply simp |
24301 | 496 |
done |
497 |
||
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
498 |
lemma float_pos_m_pos: "0 < Float m e \<Longrightarrow> 0 < m" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
499 |
unfolding less_float_def Ifloat.simps Ifloat_0 zero_less_mult_iff |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
500 |
by auto |
19765 | 501 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
502 |
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
|
503 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
504 |
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
|
505 |
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
|
506 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
507 |
show "e < 0" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
508 |
proof (rule ccontr) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
509 |
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
|
510 |
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
|
511 |
from mult_mono[OF `1 \<le> real m` this `0 \<le> real m`] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
512 |
have "1 \<le> Float m e" by (simp add: le_float_def Ifloat.simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
513 |
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
|
514 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
515 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
516 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
517 |
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
|
518 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
519 |
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
|
520 |
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
|
521 |
have "real m < 2^(nat (-e))" using `Float m e < 1` |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
522 |
unfolding less_float_def Ifloat_neg_exp[OF `e < 0`] Ifloat_1 |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
523 |
real_mult_less_iff1[of _ _ 1, OF `0 < 2^(nat (-e))`, symmetric] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
524 |
real_mult_assoc by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
525 |
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
|
526 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
527 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
528 |
function bitlen :: "int \<Rightarrow> int" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
529 |
"bitlen 0 = 0" | |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
530 |
"bitlen -1 = 1" | |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
531 |
"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
|
532 |
"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
|
533 |
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
|
534 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
535 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
536 |
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
|
537 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
538 |
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
|
539 |
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
|
540 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
541 |
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
|
542 |
using `0 < x` |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
543 |
proof (induct x rule: bitlen.induct) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
544 |
fix x |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
545 |
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
|
546 |
{ 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
|
547 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
548 |
have "0 < (2::int)" by auto |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
549 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
550 |
show "?P x" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
551 |
proof (cases "x = 1") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
552 |
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
|
553 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
554 |
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
|
555 |
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
|
556 |
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
|
557 |
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
|
558 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
559 |
{ 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
|
560 |
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
|
561 |
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
|
562 |
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
|
563 |
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
|
564 |
} moreover |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
565 |
{ 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
|
566 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
567 |
have "x mod 2 < 2" using `0 < x` by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
568 |
hence "x < x - x mod 2 + 2" unfolding algebra_simps by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
569 |
thus ?thesis by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
570 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
571 |
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
|
572 |
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
|
573 |
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
|
574 |
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
|
575 |
} |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
576 |
ultimately show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
577 |
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
|
578 |
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
|
579 |
by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
580 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
581 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
582 |
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
|
583 |
thus "?P x" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
584 |
qed auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
585 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
586 |
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
|
587 |
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
|
588 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
589 |
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
|
590 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
591 |
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
|
592 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
593 |
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
|
594 |
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
|
595 |
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
|
596 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
597 |
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
|
598 |
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
|
599 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
600 |
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
|
601 |
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
|
602 |
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
|
603 |
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
|
604 |
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
|
605 |
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
|
606 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
607 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
608 |
lemma 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
|
609 |
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
|
610 |
proof (cases "0 \<le> e") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
611 |
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
|
612 |
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
|
613 |
hence "m \<noteq> 0" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
614 |
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
|
615 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
616 |
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
|
617 |
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
|
618 |
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
|
619 |
case False let ?S = "2^(nat (-e))" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
620 |
have "1 \<le> real m * inverse ?S" using assms unfolding le_float_def Ifloat_nge0_exp[OF False] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
621 |
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
|
622 |
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
|
623 |
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
|
624 |
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
|
625 |
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
|
626 |
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
|
627 |
thus ?thesis by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
628 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
629 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
630 |
lemma normalized_float: assumes "m \<noteq> 0" shows "Ifloat (Float m (- (bitlen m - 1))) = real m / 2^nat (bitlen m - 1)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
631 |
proof (cases "- (bitlen m - 1) = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
632 |
case True show ?thesis unfolding Ifloat.simps pow2_def using True by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
633 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
634 |
case False hence P: "\<not> 0 \<le> - (bitlen m - 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
|
635 |
show ?thesis unfolding Ifloat_nge0_exp[OF P] real_divide_def by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
636 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
637 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
638 |
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
|
639 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
640 |
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
|
641 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
642 |
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
|
643 |
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
|
644 |
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
|
645 |
apply (subst Bit0_def) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
646 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
647 |
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
|
648 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
649 |
done |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
650 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
651 |
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
|
652 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
653 |
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
|
654 |
by arith |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
655 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
656 |
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
|
657 |
apply (subst Bit1_def)+ |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
658 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
659 |
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
|
660 |
apply (simp only:) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
661 |
apply simp_all |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
662 |
apply (subst Bit1_def) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
663 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
664 |
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
|
665 |
apply (auto simp add: h) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
666 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
667 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
668 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
669 |
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
|
670 |
by (simp add: number_of_is_id) |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
671 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
672 |
lemma [code]: "bitlen x = |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
673 |
(if x = 0 then 0 |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
674 |
else if x = -1 then 1 |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
675 |
else (1 + (bitlen (x div 2))))" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
676 |
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
|
677 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
678 |
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
|
679 |
where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
680 |
"lapprox_posrat prec x y = |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
681 |
(let |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
682 |
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
|
683 |
d = (x * 2^l) div y |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
684 |
in normfloat (Float d (- (int l))))" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
685 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
686 |
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
|
687 |
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
|
688 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
689 |
lemma lapprox_posrat: |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
690 |
assumes x: "0 \<le> x" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
691 |
and y: "0 < y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
692 |
shows "Ifloat (lapprox_posrat prec x y) \<le> real x / real y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
693 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
694 |
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
|
695 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
696 |
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
|
697 |
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
|
698 |
also have "\<dots> \<le> (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
|
699 |
finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding real_mult_assoc by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
700 |
thus ?thesis unfolding lapprox_posrat_def Let_def normfloat Ifloat.simps |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
701 |
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
|
702 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
703 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
704 |
lemma real_of_int_div_mult: |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
705 |
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
|
706 |
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
|
707 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
708 |
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
|
709 |
by (rule zadd_left_mono, |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
710 |
auto intro!: mult_nonneg_nonneg |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
711 |
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
|
712 |
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
|
713 |
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
|
714 |
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
|
715 |
using `0 < c` by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
716 |
thus ?thesis unfolding real_mult_assoc using `0 < c` by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
717 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
718 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
719 |
lemma lapprox_posrat_bottom: assumes "0 < y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
720 |
shows "real (x div y) \<le> Ifloat (lapprox_posrat n x y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
721 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
722 |
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
|
723 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
724 |
unfolding lapprox_posrat_def Let_def Ifloat_add normfloat Ifloat.simps pow2_minus pow2_int |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
725 |
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
|
726 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
727 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
728 |
lemma lapprox_posrat_nonneg: assumes "0 \<le> x" and "0 < y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
729 |
shows "0 \<le> Ifloat (lapprox_posrat n x y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
730 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
731 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
732 |
unfolding lapprox_posrat_def Let_def Ifloat_add normfloat Ifloat.simps pow2_minus pow2_int |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
733 |
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
|
734 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
735 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
736 |
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
|
737 |
where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
738 |
"rapprox_posrat prec x y = (let |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
739 |
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
|
740 |
X = x * 2^l ; |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
741 |
d = X div y ; |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
742 |
m = X mod y |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
743 |
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
|
744 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
745 |
lemma rapprox_posrat: |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
746 |
assumes x: "0 \<le> x" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
747 |
and y: "0 < y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
748 |
shows "real x / real y \<le> Ifloat (rapprox_posrat prec x y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
749 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
750 |
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
|
751 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
752 |
proof (cases "?X mod y = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
753 |
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
|
754 |
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
|
755 |
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
|
756 |
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
|
757 |
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
|
758 |
thus ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
759 |
unfolding Ifloat.simps 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
|
760 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
761 |
case False |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
762 |
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
|
763 |
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
|
764 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
765 |
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
|
766 |
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
|
767 |
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
|
768 |
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
|
769 |
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
|
770 |
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
|
771 |
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
|
772 |
also have "\<dots> = real (?X div y + 1) * inverse (2^?l)" unfolding nonzero_mult_divide_cancel_left[OF `real y \<noteq> 0`] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
773 |
unfolding real_divide_def .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
774 |
finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat Ifloat.simps if_not_P[OF False] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
775 |
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
|
776 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
777 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
778 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
779 |
lemma rapprox_posrat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
780 |
shows "Ifloat (rapprox_posrat n x y) \<le> 1" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
781 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
782 |
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
|
783 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
784 |
proof (cases "?X mod y = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
785 |
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
|
786 |
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
|
787 |
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
|
788 |
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
|
789 |
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
|
790 |
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
|
791 |
finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
792 |
unfolding Ifloat.simps 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
|
793 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
794 |
case False |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
795 |
have "x \<noteq> y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
796 |
proof (rule ccontr) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
797 |
assume "\<not> x \<noteq> y" hence "x = y" by auto |
30034 | 798 |
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
|
799 |
thus False using False by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
800 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
801 |
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
|
802 |
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
|
803 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
804 |
from real_of_int_div4[of "?X" y] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
805 |
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[symmetric] real_number_of . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
806 |
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
|
807 |
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
|
808 |
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
|
809 |
hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
810 |
unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
811 |
by (rule mult_right_mono, auto) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
812 |
hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
813 |
thus ?thesis unfolding rapprox_posrat_def Let_def normfloat Ifloat.simps if_not_P[OF False] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
814 |
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
|
815 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
816 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
817 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
818 |
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
|
819 |
shows "0 < b div a" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
820 |
proof (rule ccontr) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
821 |
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
|
822 |
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
|
823 |
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
|
824 |
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
|
825 |
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
|
826 |
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
|
827 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
828 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
829 |
lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
830 |
shows "Ifloat (rapprox_posrat n x y) < 1" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
831 |
proof (cases "x = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
832 |
case True thus ?thesis unfolding rapprox_posrat_def True Let_def normfloat Ifloat.simps by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
833 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
834 |
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
|
835 |
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
|
836 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
837 |
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
|
838 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
839 |
proof (cases "?X mod y = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
840 |
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
|
841 |
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
|
842 |
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
|
843 |
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
|
844 |
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
|
845 |
also have "real x / real y < 1" using `0 \<le> x` and `0 < y` and `x < y` by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
846 |
finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat Ifloat.simps if_P[OF True] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
847 |
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
|
848 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
849 |
case False |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
850 |
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
|
851 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
852 |
have "0 < ?X div y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
853 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
854 |
have "2^nat (bitlen x - 1) \<le> y" and "y < 2^nat (bitlen y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
855 |
using bitlen_bounds[OF `0 < x`, THEN conjunct1] bitlen_bounds[OF `0 < y`, THEN conjunct2] `x < y` by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
856 |
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
|
857 |
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
|
858 |
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
|
859 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
860 |
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
|
861 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
862 |
have exp_eq: "nat (int (n - 1) + bitlen y) - nat (bitlen x - 1) = ?l" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
863 |
using `bitlen x \<le> bitlen y` bitlen_ge1[OF `x \<noteq> 0`] bitlen_ge1[OF `y \<noteq> 0`] `0 < n` by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
864 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
865 |
have "y * 2^nat (bitlen x - 1) \<le> y * x" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
866 |
using bitlen_bounds[OF `0 < x`, THEN conjunct1] `0 < y`[THEN less_imp_le] by (rule mult_left_mono) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
867 |
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
|
868 |
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
|
869 |
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))" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
870 |
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
|
871 |
hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
872 |
unfolding real_mult_assoc real_divide_def by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
873 |
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
|
874 |
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
|
875 |
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
|
876 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
877 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
878 |
from real_of_int_div4[of "?X" y] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
879 |
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[symmetric] real_number_of . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
880 |
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
|
881 |
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
|
882 |
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
|
883 |
hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
884 |
unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
885 |
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
|
886 |
hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
887 |
thus ?thesis unfolding rapprox_posrat_def Let_def normfloat Ifloat.simps if_not_P[OF False] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
888 |
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
|
889 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
890 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
891 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
892 |
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
|
893 |
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
|
894 |
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
|
895 |
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
|
896 |
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
|
897 |
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
|
898 |
shows P |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
899 |
proof - |
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
900 |
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
|
901 |
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
|
902 |
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
|
903 |
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
|
904 |
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
|
905 |
qed |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
906 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
907 |
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
|
908 |
where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
909 |
"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
|
910 |
| "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
|
911 |
| "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
|
912 |
| "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
|
913 |
| "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
|
914 |
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
|
915 |
termination by lexicographic_order |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
916 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
917 |
lemma compute_lapprox_rat[code]: |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
918 |
"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
|
919 |
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
|
920 |
by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
921 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
922 |
lemma lapprox_rat: "Ifloat (lapprox_rat prec x y) \<le> real x / real y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
923 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
924 |
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
|
925 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
926 |
apply (case_tac "y = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
927 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
928 |
apply (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
|
929 |
apply (simp add: lapprox_posrat) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
930 |
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
|
931 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
932 |
apply (subst minus_le_iff) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
933 |
apply (rule h[OF rapprox_posrat]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
934 |
apply (simp_all) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
935 |
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
|
936 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
937 |
apply (rule h[OF _ lapprox_posrat]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
938 |
apply (simp_all) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
939 |
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
|
940 |
apply (simp) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
941 |
apply (subst minus_le_iff) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
942 |
apply (rule h[OF rapprox_posrat]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
943 |
apply simp_all |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
944 |
apply arith |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
945 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
946 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
947 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
948 |
lemma lapprox_rat_bottom: assumes "0 \<le> x" and "0 < y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
949 |
shows "real (x div y) \<le> Ifloat (lapprox_rat n x y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
950 |
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
|
951 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
952 |
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
|
953 |
where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
954 |
"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
|
955 |
| "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
|
956 |
| "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
|
957 |
| "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
|
958 |
| "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
|
959 |
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
|
960 |
termination by lexicographic_order |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
961 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
962 |
lemma compute_rapprox_rat[code]: |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
963 |
"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
|
964 |
(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
|
965 |
by auto |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
966 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
967 |
lemma rapprox_rat: "real x / real y \<le> Ifloat (rapprox_rat prec x y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
968 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
969 |
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
|
970 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
971 |
apply (case_tac "y = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
972 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
973 |
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
|
974 |
apply (simp add: rapprox_posrat) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
975 |
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
|
976 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
977 |
apply (subst le_minus_iff) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
978 |
apply (rule h[OF _ lapprox_posrat]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
979 |
apply (simp_all) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
980 |
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
|
981 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
982 |
apply (rule h[OF rapprox_posrat]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
983 |
apply (simp_all) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
984 |
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
|
985 |
apply (simp) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
986 |
apply (subst le_minus_iff) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
987 |
apply (rule h[OF _ lapprox_posrat]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
988 |
apply simp_all |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
989 |
apply arith |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
990 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
991 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
992 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
993 |
lemma rapprox_rat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
994 |
shows "Ifloat (rapprox_rat n x y) \<le> 1" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
995 |
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
|
996 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
997 |
lemma rapprox_rat_neg: assumes "x < 0" and "0 < y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
998 |
shows "Ifloat (rapprox_rat n x y) \<le> 0" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
999 |
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
|
1000 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1001 |
lemma rapprox_rat_nonneg_neg: assumes "0 \<le> x" and "y < 0" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1002 |
shows "Ifloat (rapprox_rat n x y) \<le> 0" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1003 |
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
|
1004 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1005 |
lemma rapprox_rat_nonpos_pos: assumes "x \<le> 0" and "0 < y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1006 |
shows "Ifloat (rapprox_rat n x y) \<le> 0" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1007 |
proof (cases "x = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1008 |
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
|
1009 |
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
|
1010 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1011 |
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
|
1012 |
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
|
1013 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1014 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1015 |
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
|
1016 |
where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1017 |
"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
|
1018 |
(let |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1019 |
l = lapprox_rat prec m1 m2; |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1020 |
f = Float 1 (s1 - s2) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1021 |
in |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1022 |
f * l)" |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1023 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1024 |
lemma float_divl: "Ifloat (float_divl prec x y) \<le> Ifloat x / Ifloat y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1025 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1026 |
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
|
1027 |
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
|
1028 |
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
|
1029 |
apply (case_tac "my = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1030 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1031 |
apply (case_tac "my > 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1032 |
apply (subst pos_le_divide_eq) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1033 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1034 |
apply (subst pos_le_divide_eq) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1035 |
apply (simp add: mult_pos_pos) |
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 (subst pow2_add[symmetric]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1038 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1039 |
apply (subgoal_tac "my < 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1040 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1041 |
apply (simp add: field_simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1042 |
apply (subst pow2_add[symmetric]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1043 |
apply (simp add: field_simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1044 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1045 |
then have "Ifloat (lapprox_rat prec mx 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
|
1046 |
by (rule order_trans[OF lapprox_rat]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1047 |
then have "Ifloat (lapprox_rat prec mx my) * pow2 (sx - sy) \<le> real mx * pow2 sx / (real my * pow2 sy)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1048 |
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
|
1049 |
apply simp_all |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1050 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1051 |
then have "pow2 (sx - sy) * Ifloat (lapprox_rat prec mx my) \<le> real mx * pow2 sx / (real my * pow2 sy)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1052 |
by (simp add: algebra_simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1053 |
then show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1054 |
by (simp add: x y Let_def Ifloat.simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1055 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1056 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1057 |
lemma float_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
|
1058 |
proof (cases x, cases y) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1059 |
fix xm xe ym ye :: int |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1060 |
assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1061 |
have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def Ifloat.simps Ifloat_0 zero_le_mult_iff] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1062 |
have "0 < ym" using `0 < y`[unfolded y_eq less_float_def Ifloat.simps Ifloat_0 zero_less_mult_iff] by auto |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1063 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1064 |
have "\<And>n. 0 \<le> Ifloat (Float 1 n)" unfolding Ifloat.simps using zero_le_pow2 by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1065 |
moreover have "0 \<le> Ifloat (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`]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1066 |
ultimately show "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
|
1067 |
unfolding x_eq y_eq float_divl.simps Let_def le_float_def Ifloat_0 by (auto intro!: mult_nonneg_nonneg) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1068 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1069 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1070 |
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
|
1071 |
proof (cases x) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1072 |
case (Float m e) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1073 |
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
|
1074 |
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
|
1075 |
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
|
1076 |
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
|
1077 |
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
|
1078 |
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
|
1079 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1080 |
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
|
1081 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1082 |
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
|
1083 |
have "m < 2^?e" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1084 |
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
|
1085 |
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
|
1086 |
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
|
1087 |
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
|
1088 |
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
|
1089 |
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
|
1090 |
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
|
1091 |
also |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1092 |
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
|
1093 |
{ 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
|
1094 |
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
|
1095 |
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) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1096 |
hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding zdiv_zmult_self1[OF `m \<noteq> 0`] . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1097 |
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
|
1098 |
unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto } |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1099 |
from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib real_mult_assoc[symmetric] right_inverse[OF pow_not0] real_mult_1], of "2^?e"] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1100 |
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
|
1101 |
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
|
1102 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1103 |
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
|
1104 |
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
|
1105 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1106 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1107 |
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` |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1108 |
unfolding le_float_def Ifloat_mult normfloat Ifloat.simps pow2_minus pow2_int e_nat |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1109 |
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
|
1110 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1111 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1112 |
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
|
1113 |
where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1114 |
"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
|
1115 |
(let |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1116 |
r = rapprox_rat prec m1 m2; |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1117 |
f = Float 1 (s1 - s2) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1118 |
in |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1119 |
f * r)" |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1120 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1121 |
lemma float_divr: "Ifloat x / Ifloat y \<le> Ifloat (float_divr prec x y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1122 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1123 |
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
|
1124 |
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
|
1125 |
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
|
1126 |
apply (case_tac "my = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1127 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1128 |
apply (case_tac "my > 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1129 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1130 |
apply (subst pos_divide_le_eq) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1131 |
apply (rule mult_pos_pos)+ |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1132 |
apply simp_all |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1133 |
apply (subst pow2_add[symmetric]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1134 |
apply simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1135 |
apply (subgoal_tac "my < 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1136 |
apply auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1137 |
apply (simp add: field_simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1138 |
apply (subst pow2_add[symmetric]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1139 |
apply (simp add: field_simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1140 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1141 |
then have "Ifloat (rapprox_rat prec mx 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
|
1142 |
by (rule order_trans[OF _ rapprox_rat]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1143 |
then have "Ifloat (rapprox_rat prec mx my) * pow2 (sx - sy) \<ge> real mx * pow2 sx / (real my * pow2 sy)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1144 |
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
|
1145 |
apply simp_all |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1146 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1147 |
then show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1148 |
by (simp add: x y Let_def algebra_simps Ifloat.simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1149 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1150 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1151 |
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
|
1152 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1153 |
have "1 \<le> 1 / Ifloat x" using `0 < x` and `x < 1` unfolding less_float_def by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1154 |
also have "\<dots> \<le> Ifloat (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1155 |
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
|
1156 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1157 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1158 |
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
|
1159 |
proof (cases x, cases y) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1160 |
fix xm xe ym ye :: int |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1161 |
assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1162 |
have "xm \<le> 0" using `x \<le> 0`[unfolded x_eq le_float_def Ifloat.simps Ifloat_0 mult_le_0_iff] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1163 |
have "0 < ym" using `0 < y`[unfolded y_eq less_float_def Ifloat.simps Ifloat_0 zero_less_mult_iff] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1164 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1165 |
have "\<And>n. 0 \<le> Ifloat (Float 1 n)" unfolding Ifloat.simps using zero_le_pow2 by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1166 |
moreover have "Ifloat (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonpos_pos[OF `xm \<le> 0` `0 < ym`] . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1167 |
ultimately show "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
|
1168 |
unfolding x_eq y_eq float_divr.simps Let_def le_float_def Ifloat_0 Ifloat_mult by (auto intro!: mult_nonneg_nonpos) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1169 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1170 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1171 |
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
|
1172 |
proof (cases x, cases y) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1173 |
fix xm xe ym ye :: int |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1174 |
assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1175 |
have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def Ifloat.simps Ifloat_0 zero_le_mult_iff] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1176 |
have "ym < 0" using `y < 0`[unfolded y_eq less_float_def Ifloat.simps Ifloat_0 mult_less_0_iff] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1177 |
hence "0 < - ym" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1178 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1179 |
have "\<And>n. 0 \<le> Ifloat (Float 1 n)" unfolding Ifloat.simps using zero_le_pow2 by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1180 |
moreover have "Ifloat (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonneg_neg[OF `0 \<le> xm` `ym < 0`] . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1181 |
ultimately show "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
|
1182 |
unfolding x_eq y_eq float_divr.simps Let_def le_float_def Ifloat_0 Ifloat_mult by (auto intro!: mult_nonneg_nonpos) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1183 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1184 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1185 |
fun round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1186 |
"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
|
1187 |
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
|
1188 |
else Float m e)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1189 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1190 |
fun round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1191 |
"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
|
1192 |
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
|
1193 |
else Float m e)" |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1194 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1195 |
lemma round_up: "Ifloat x \<le> Ifloat (round_up prec x)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1196 |
proof (cases x) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1197 |
case (Float m e) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1198 |
let ?d = "bitlen m - int prec" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1199 |
let ?p = "(2::int)^nat ?d" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1200 |
have "0 < ?p" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1201 |
show "?thesis" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1202 |
proof (cases "0 < ?d") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1203 |
case True |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1204 |
hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1205 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1206 |
proof (cases "m mod ?p = 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1207 |
case True |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1208 |
have 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] . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1209 |
have "Ifloat (Float m e) = Ifloat (Float (m div ?p) (e + ?d))" unfolding Ifloat.simps arg_cong[OF m, of real] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1210 |
by (auto simp add: pow2_add `0 < ?d` pow_d) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1211 |
thus ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1212 |
unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1213 |
by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1214 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1215 |
case False |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1216 |
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
|
1217 |
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]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1218 |
finally have "Ifloat (Float m e) \<le> Ifloat (Float (m div ?p + 1) (e + ?d))" unfolding Ifloat.simps add_commute[of e] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1219 |
unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1220 |
by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1221 |
thus ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1222 |
unfolding Float round_up.simps Let_def if_not_P[OF `\<not> m mod ?p = 0`] if_P[OF `0 < ?d`] . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1223 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1224 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1225 |
case False |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1226 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1227 |
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
|
1228 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1229 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1230 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1231 |
lemma round_down: "Ifloat (round_down prec x) \<le> Ifloat x" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1232 |
proof (cases x) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1233 |
case (Float m e) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1234 |
let ?d = "bitlen m - int prec" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1235 |
let ?p = "(2::int)^nat ?d" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1236 |
have "0 < ?p" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1237 |
show "?thesis" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1238 |
proof (cases "0 < ?d") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1239 |
case True |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1240 |
hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1241 |
have "m div ?p * ?p \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1242 |
also have "\<dots> \<le> m" 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
|
1243 |
finally have "Ifloat (Float (m div ?p) (e + ?d)) \<le> Ifloat (Float m e)" unfolding Ifloat.simps add_commute[of e] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1244 |
unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1245 |
by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1246 |
thus ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1247 |
unfolding Float round_down.simps Let_def if_P[OF `0 < ?d`] . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1248 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1249 |
case False |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1250 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1251 |
unfolding Float round_down.simps Let_def if_not_P[OF False] .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1252 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1253 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1254 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1255 |
definition lb_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1256 |
"lb_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1257 |
l = bitlen m - int prec |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1258 |
in if l > 0 then Float (m div (2^nat l)) (e + l) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1259 |
else Float m e)" |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1260 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1261 |
definition ub_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1262 |
"ub_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1263 |
l = bitlen m - int prec |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1264 |
in if l > 0 then Float (m div (2^nat l) + 1) (e + l) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1265 |
else Float m e)" |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1266 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1267 |
lemma lb_mult: "Ifloat (lb_mult prec x y) \<le> Ifloat (x * y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1268 |
proof (cases "normfloat (x * y)") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1269 |
case (Float m e) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1270 |
hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1271 |
let ?l = "bitlen m - int prec" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1272 |
have "Ifloat (lb_mult prec x y) \<le> Ifloat (normfloat (x * y))" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1273 |
proof (cases "?l > 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1274 |
case False thus ?thesis unfolding lb_mult_def Float Let_def float.cases by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1275 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1276 |
case True |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1277 |
have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1278 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1279 |
have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power[symmetric] real_number_of unfolding pow2_int[symmetric] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1280 |
using `?l > 0` by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1281 |
also have "\<dots> \<le> real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding real_of_int_add by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1282 |
also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1283 |
finally show ?thesis by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1284 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1285 |
thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] Ifloat.simps pow2_add real_mult_commute real_mult_assoc by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1286 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1287 |
also have "\<dots> = Ifloat (x * y)" unfolding normfloat .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1288 |
finally show ?thesis . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1289 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1290 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1291 |
lemma ub_mult: "Ifloat (x * y) \<le> Ifloat (ub_mult prec x y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1292 |
proof (cases "normfloat (x * y)") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1293 |
case (Float m e) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1294 |
hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1295 |
let ?l = "bitlen m - int prec" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1296 |
have "Ifloat (x * y) = Ifloat (normfloat (x * y))" unfolding normfloat .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1297 |
also have "\<dots> \<le> Ifloat (ub_mult prec x y)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1298 |
proof (cases "?l > 0") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1299 |
case False thus ?thesis unfolding ub_mult_def Float Let_def float.cases by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1300 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1301 |
case True |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1302 |
have "real m \<le> real (m div 2^(nat ?l) + 1) * pow2 ?l" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1303 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1304 |
have "m mod 2^(nat ?l) < 2^(nat ?l)" by (rule pos_mod_bound) auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1305 |
hence mod_uneq: "real (m mod 2^(nat ?l)) \<le> 1 * 2^(nat ?l)" unfolding zmult_1 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
|
1306 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1307 |
have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1308 |
also have "\<dots> = real (m div 2^(nat ?l)) * 2^(nat ?l) + real (m mod 2^(nat ?l))" unfolding real_of_int_add by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1309 |
also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding real_add_mult_distrib using mod_uneq by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1310 |
finally show ?thesis unfolding pow2_int[symmetric] using True by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1311 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1312 |
thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] Ifloat.simps pow2_add real_mult_commute real_mult_assoc by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1313 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1314 |
finally show ?thesis . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1315 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1316 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1317 |
fun float_abs :: "float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1318 |
"float_abs (Float m e) = Float \<bar>m\<bar> e" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1319 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1320 |
instantiation float :: abs begin |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1321 |
definition abs_float_def: "\<bar>x\<bar> = float_abs x" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1322 |
instance .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1323 |
end |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1324 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1325 |
lemma Ifloat_abs: "Ifloat \<bar>x\<bar> = \<bar>Ifloat x\<bar>" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1326 |
proof (cases x) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1327 |
case (Float m e) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1328 |
have "\<bar>real m\<bar> * pow2 e = \<bar>real m * pow2 e\<bar>" unfolding abs_mult by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1329 |
thus ?thesis unfolding Float abs_float_def float_abs.simps Ifloat.simps by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1330 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1331 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1332 |
fun floor_fl :: "float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1333 |
"floor_fl (Float m e) = (if 0 \<le> e then Float m e |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1334 |
else Float (m div (2 ^ (nat (-e)))) 0)" |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1335 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1336 |
lemma floor_fl: "Ifloat (floor_fl x) \<le> Ifloat x" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1337 |
proof (cases x) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1338 |
case (Float m e) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1339 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1340 |
proof (cases "0 \<le> e") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1341 |
case False |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1342 |
hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1343 |
have "Ifloat (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding Ifloat.simps by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1344 |
also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1345 |
also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1346 |
also have "\<dots> = Ifloat (Float m e)" unfolding Ifloat.simps me_eq pow2_int pow2_neg[of e] .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1347 |
finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1348 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1349 |
case True thus ?thesis unfolding Float by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1350 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1351 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1352 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1353 |
lemma floor_pos_exp: assumes floor: "Float m e = floor_fl x" shows "0 \<le> e" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1354 |
proof (cases x) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1355 |
case (Float mx me) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1356 |
from floor[unfolded Float floor_fl.simps] show ?thesis by (cases "0 \<le> me", auto) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1357 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1358 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1359 |
declare floor_fl.simps[simp del] |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1360 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1361 |
fun ceiling_fl :: "float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1362 |
"ceiling_fl (Float m e) = (if 0 \<le> e then Float m e |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1363 |
else Float (m div (2 ^ (nat (-e))) + 1) 0)" |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1364 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1365 |
lemma ceiling_fl: "Ifloat x \<le> Ifloat (ceiling_fl x)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1366 |
proof (cases x) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1367 |
case (Float m e) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1368 |
show ?thesis |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1369 |
proof (cases "0 \<le> e") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1370 |
case False |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1371 |
hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1372 |
have "Ifloat (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding Ifloat.simps me_eq pow2_int pow2_neg[of e] .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1373 |
also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def .. |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1374 |
also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1375 |
also have "\<dots> = Ifloat (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding Ifloat.simps by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1376 |
finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] . |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1377 |
next |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1378 |
case True thus ?thesis unfolding Float by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1379 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1380 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1381 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1382 |
declare ceiling_fl.simps[simp del] |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1383 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1384 |
definition lb_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1385 |
"lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1386 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1387 |
definition ub_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1388 |
"ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb" |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1389 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1390 |
lemma lb_mod: fixes k :: int assumes "0 \<le> Ifloat x" and "real k * y \<le> Ifloat x" (is "?k * y \<le> ?x") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1391 |
assumes "0 < Ifloat lb" "Ifloat lb \<le> y" (is "?lb \<le> y") "y \<le> Ifloat ub" (is "y \<le> ?ub") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1392 |
shows "Ifloat (lb_mod prec x ub lb) \<le> ?x - ?k * y" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1393 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1394 |
have "?lb \<le> ?ub" by (auto!) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1395 |
have "0 \<le> ?lb" and "?lb \<noteq> 0" by (auto!) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1396 |
have "?k * y \<le> ?x" using assms by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1397 |
also have "\<dots> \<le> ?x / ?lb * ?ub" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?lb` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?lb \<noteq> 0`]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1398 |
also have "\<dots> \<le> Ifloat (ceiling_fl (float_divr prec x lb)) * ?ub" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divr ceiling_fl) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1399 |
finally show ?thesis unfolding lb_mod_def Ifloat_sub Ifloat_mult by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1400 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1401 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1402 |
lemma ub_mod: fixes k :: int assumes "0 \<le> Ifloat x" and "Ifloat x \<le> real k * y" (is "?x \<le> ?k * y") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1403 |
assumes "0 < Ifloat lb" "Ifloat lb \<le> y" (is "?lb \<le> y") "y \<le> Ifloat ub" (is "y \<le> ?ub") |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1404 |
shows "?x - ?k * y \<le> Ifloat (ub_mod prec x ub lb)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1405 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1406 |
have "?lb \<le> ?ub" by (auto!) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1407 |
hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" by (auto!) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1408 |
have "Ifloat (floor_fl (float_divl prec x ub)) * ?lb \<le> ?x / ?ub * ?lb" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divl floor_fl) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1409 |
also have "\<dots> \<le> ?x" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?ub` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?ub \<noteq> 0`]) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1410 |
also have "\<dots> \<le> ?k * y" using assms by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1411 |
finally show ?thesis unfolding ub_mod_def Ifloat_sub Ifloat_mult by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1412 |
qed |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1413 |
|
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1414 |
lemma le_float_def': "f \<le> g = (case f - g of Float a b \<Rightarrow> a \<le> 0)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1415 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1416 |
have le_transfer: "(f \<le> g) = (Ifloat (f - g) \<le> 0)" 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
|
1417 |
from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1418 |
with le_transfer have le_transfer': "f \<le> g = (Ifloat (Float a b) \<le> 0)" by simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1419 |
show ?thesis by (simp add: le_transfer' f_diff_g float_le_zero) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1420 |
qed |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1421 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1422 |
lemma float_less_zero: |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1423 |
"(Ifloat (Float a b) < 0) = (a < 0)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1424 |
apply (auto simp add: mult_less_0_iff Ifloat.simps) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1425 |
done |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1426 |
|
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1427 |
lemma less_float_def': "f < g = (case f - g of Float a b \<Rightarrow> a < 0)" |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1428 |
proof - |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1429 |
have less_transfer: "(f < g) = (Ifloat (f - g) < 0)" 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
|
1430 |
from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1431 |
with less_transfer have less_transfer': "f < g = (Ifloat (Float a b) < 0)" by simp |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1432 |
show ?thesis by (simp add: less_transfer' f_diff_g float_less_zero) |
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29667
diff
changeset
|
1433 |
qed |
20771 | 1434 |
|
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
1435 |
end |