14369
|
1 |
(* Title: HOL/HyperBin.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1999 University of Cambridge
|
|
5 |
*)
|
|
6 |
|
|
7 |
header{*Binary arithmetic and Simplification for the Hyperreals*}
|
|
8 |
|
|
9 |
theory HyperArith = HyperOrd
|
|
10 |
files ("hypreal_arith.ML"):
|
|
11 |
|
|
12 |
subsection{*Binary Arithmetic for the Hyperreals*}
|
|
13 |
|
|
14 |
instance hypreal :: number ..
|
|
15 |
|
|
16 |
defs (overloaded)
|
|
17 |
hypreal_number_of_def:
|
|
18 |
"number_of v == hypreal_of_real (number_of v)"
|
|
19 |
(*::bin=>hypreal ::bin=>real*)
|
|
20 |
--{*This case is reduced to that for the reals.*}
|
|
21 |
|
|
22 |
|
|
23 |
|
|
24 |
subsubsection{*Embedding the Reals into the Hyperreals*}
|
|
25 |
|
|
26 |
lemma hypreal_number_of [simp]: "hypreal_of_real (number_of w) = number_of w"
|
|
27 |
by (simp add: hypreal_number_of_def)
|
|
28 |
|
|
29 |
lemma hypreal_numeral_0_eq_0: "Numeral0 = (0::hypreal)"
|
|
30 |
by (simp add: hypreal_number_of_def)
|
|
31 |
|
|
32 |
lemma hypreal_numeral_1_eq_1: "Numeral1 = (1::hypreal)"
|
|
33 |
by (simp add: hypreal_number_of_def)
|
|
34 |
|
|
35 |
subsubsection{*Addition*}
|
|
36 |
|
|
37 |
lemma add_hypreal_number_of [simp]:
|
|
38 |
"(number_of v :: hypreal) + number_of v' = number_of (bin_add v v')"
|
|
39 |
by (simp only: hypreal_number_of_def hypreal_of_real_add [symmetric]
|
|
40 |
add_real_number_of)
|
|
41 |
|
|
42 |
|
|
43 |
subsubsection{*Subtraction*}
|
|
44 |
|
|
45 |
lemma minus_hypreal_number_of [simp]:
|
|
46 |
"- (number_of w :: hypreal) = number_of (bin_minus w)"
|
|
47 |
by (simp only: hypreal_number_of_def minus_real_number_of
|
|
48 |
hypreal_of_real_minus [symmetric])
|
|
49 |
|
|
50 |
lemma diff_hypreal_number_of [simp]:
|
|
51 |
"(number_of v :: hypreal) - number_of w =
|
|
52 |
number_of (bin_add v (bin_minus w))"
|
|
53 |
by (unfold hypreal_number_of_def hypreal_diff_def, simp)
|
|
54 |
|
|
55 |
|
|
56 |
subsubsection{*Multiplication*}
|
|
57 |
|
|
58 |
lemma mult_hypreal_number_of [simp]:
|
|
59 |
"(number_of v :: hypreal) * number_of v' = number_of (bin_mult v v')"
|
|
60 |
by (simp only: hypreal_number_of_def hypreal_of_real_mult [symmetric] mult_real_number_of)
|
|
61 |
|
|
62 |
text{*Lemmas for specialist use, NOT as default simprules*}
|
|
63 |
lemma hypreal_mult_2: "2 * z = (z+z::hypreal)"
|
|
64 |
proof -
|
|
65 |
have eq: "(2::hypreal) = 1 + 1"
|
|
66 |
by (simp add: hypreal_numeral_1_eq_1 [symmetric])
|
|
67 |
thus ?thesis by (simp add: eq left_distrib)
|
|
68 |
qed
|
|
69 |
|
|
70 |
lemma hypreal_mult_2_right: "z * 2 = (z+z::hypreal)"
|
|
71 |
by (subst hypreal_mult_commute, rule hypreal_mult_2)
|
|
72 |
|
|
73 |
|
|
74 |
subsubsection{*Comparisons*}
|
|
75 |
|
|
76 |
(** Equals (=) **)
|
|
77 |
|
|
78 |
lemma eq_hypreal_number_of [simp]:
|
|
79 |
"((number_of v :: hypreal) = number_of v') =
|
|
80 |
iszero (number_of (bin_add v (bin_minus v')))"
|
|
81 |
apply (simp only: hypreal_number_of_def hypreal_of_real_eq_iff eq_real_number_of)
|
|
82 |
done
|
|
83 |
|
|
84 |
|
|
85 |
(** Less-than (<) **)
|
|
86 |
|
|
87 |
(*"neg" is used in rewrite rules for binary comparisons*)
|
|
88 |
lemma less_hypreal_number_of [simp]:
|
|
89 |
"((number_of v :: hypreal) < number_of v') =
|
|
90 |
neg (number_of (bin_add v (bin_minus v')))"
|
|
91 |
by (simp only: hypreal_number_of_def hypreal_of_real_less_iff less_real_number_of)
|
|
92 |
|
|
93 |
|
|
94 |
|
|
95 |
text{*New versions of existing theorems involving 0, 1*}
|
|
96 |
|
|
97 |
lemma hypreal_minus_1_eq_m1 [simp]: "- 1 = (-1::hypreal)"
|
|
98 |
by (simp add: hypreal_numeral_1_eq_1 [symmetric])
|
|
99 |
|
|
100 |
lemma hypreal_mult_minus1 [simp]: "-1 * z = -(z::hypreal)"
|
|
101 |
proof -
|
|
102 |
have "-1 * z = (- 1) * z" by (simp add: hypreal_minus_1_eq_m1)
|
|
103 |
also have "... = - (1 * z)" by (simp only: minus_mult_left)
|
|
104 |
also have "... = -z" by simp
|
|
105 |
finally show ?thesis .
|
|
106 |
qed
|
|
107 |
|
|
108 |
lemma hypreal_mult_minus1_right [simp]: "(z::hypreal) * -1 = -z"
|
|
109 |
by (subst hypreal_mult_commute, rule hypreal_mult_minus1)
|
|
110 |
|
|
111 |
|
|
112 |
subsection{*Simplification of Arithmetic when Nested to the Right*}
|
|
113 |
|
|
114 |
lemma hypreal_add_number_of_left [simp]:
|
|
115 |
"number_of v + (number_of w + z) = (number_of(bin_add v w) + z::hypreal)"
|
|
116 |
by (simp add: add_assoc [symmetric])
|
|
117 |
|
|
118 |
lemma hypreal_mult_number_of_left [simp]:
|
|
119 |
"number_of v *(number_of w * z) = (number_of(bin_mult v w) * z::hypreal)"
|
|
120 |
by (simp add: hypreal_mult_assoc [symmetric])
|
|
121 |
|
|
122 |
lemma hypreal_add_number_of_diff1:
|
|
123 |
"number_of v + (number_of w - c) = number_of(bin_add v w) - (c::hypreal)"
|
|
124 |
by (simp add: hypreal_diff_def hypreal_add_number_of_left)
|
|
125 |
|
|
126 |
lemma hypreal_add_number_of_diff2 [simp]:
|
|
127 |
"number_of v + (c - number_of w) =
|
|
128 |
number_of (bin_add v (bin_minus w)) + (c::hypreal)"
|
|
129 |
apply (subst diff_hypreal_number_of [symmetric])
|
|
130 |
apply (simp only: hypreal_diff_def add_ac)
|
|
131 |
done
|
|
132 |
|
|
133 |
|
|
134 |
declare hypreal_numeral_0_eq_0 [simp] hypreal_numeral_1_eq_1 [simp]
|
|
135 |
|
|
136 |
|
|
137 |
|
|
138 |
use "hypreal_arith.ML"
|
10751
|
139 |
|
|
140 |
setup hypreal_arith_setup
|
|
141 |
|
14329
|
142 |
text{*Used once in NSA*}
|
|
143 |
lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y"
|
14369
|
144 |
by arith
|
14329
|
145 |
|
|
146 |
|
14309
|
147 |
subsubsection{*Division By @{term 1} and @{term "-1"}*}
|
|
148 |
|
|
149 |
lemma hypreal_divide_minus1 [simp]: "x/-1 = -(x::hypreal)"
|
|
150 |
by simp
|
|
151 |
|
|
152 |
lemma hypreal_minus1_divide [simp]: "-1/(x::hypreal) = - (1/x)"
|
|
153 |
by (simp add: hypreal_divide_def hypreal_minus_inverse)
|
|
154 |
|
|
155 |
|
14369
|
156 |
|
|
157 |
|
|
158 |
(** number_of related to hypreal_of_real.
|
|
159 |
Could similar theorems be useful for other injections? **)
|
|
160 |
|
|
161 |
lemma number_of_less_hypreal_of_real_iff [simp]:
|
|
162 |
"(number_of w < hypreal_of_real z) = (number_of w < z)"
|
|
163 |
apply (subst hypreal_of_real_less_iff [symmetric])
|
|
164 |
apply (simp (no_asm))
|
|
165 |
done
|
|
166 |
|
|
167 |
lemma number_of_le_hypreal_of_real_iff [simp]:
|
|
168 |
"(number_of w <= hypreal_of_real z) = (number_of w <= z)"
|
|
169 |
apply (subst hypreal_of_real_le_iff [symmetric])
|
|
170 |
apply (simp (no_asm))
|
|
171 |
done
|
|
172 |
|
|
173 |
lemma hypreal_of_real_eq_number_of_iff [simp]:
|
|
174 |
"(hypreal_of_real z = number_of w) = (z = number_of w)"
|
|
175 |
apply (subst hypreal_of_real_eq_iff [symmetric])
|
|
176 |
apply (simp (no_asm))
|
|
177 |
done
|
|
178 |
|
|
179 |
lemma hypreal_of_real_less_number_of_iff [simp]:
|
|
180 |
"(hypreal_of_real z < number_of w) = (z < number_of w)"
|
|
181 |
apply (subst hypreal_of_real_less_iff [symmetric])
|
|
182 |
apply (simp (no_asm))
|
|
183 |
done
|
|
184 |
|
|
185 |
lemma hypreal_of_real_le_number_of_iff [simp]:
|
|
186 |
"(hypreal_of_real z <= number_of w) = (z <= number_of w)"
|
|
187 |
apply (subst hypreal_of_real_le_iff [symmetric])
|
|
188 |
apply (simp (no_asm))
|
|
189 |
done
|
|
190 |
|
14309
|
191 |
(*
|
|
192 |
FIXME: we should have this, as for type int, but many proofs would break.
|
|
193 |
It replaces x+-y by x-y.
|
|
194 |
Addsimps [symmetric hypreal_diff_def]
|
|
195 |
*)
|
|
196 |
|
14369
|
197 |
ML
|
|
198 |
{*
|
|
199 |
val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus";
|
|
200 |
*}
|
|
201 |
|
10751
|
202 |
end
|