author | paulson |
Fri, 05 Dec 2003 10:28:02 +0100 | |
changeset 14275 | 031a5a051bb4 |
parent 14270 | 342451d763f9 |
child 14288 | d149e3cbdb39 |
permissions | -rw-r--r-- |
10722 | 1 |
theory RealArith = RealArith0 |
14275
031a5a051bb4
Converting more of the "real" development to Isar scripts
paulson
parents:
14270
diff
changeset
|
2 |
files ("real_arith.ML"): |
031a5a051bb4
Converting more of the "real" development to Isar scripts
paulson
parents:
14270
diff
changeset
|
3 |
|
031a5a051bb4
Converting more of the "real" development to Isar scripts
paulson
parents:
14270
diff
changeset
|
4 |
use "real_arith.ML" |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
5 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
6 |
setup real_arith_setup |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
7 |
|
14269 | 8 |
subsection{*Absolute Value Function for the Reals*} |
9 |
||
10 |
(** abs (absolute value) **) |
|
11 |
||
12 |
lemma abs_nat_number_of: |
|
13 |
"abs (number_of v :: real) = |
|
14 |
(if neg (number_of v) then number_of (bin_minus v) |
|
15 |
else number_of v)" |
|
16 |
apply (simp add: real_abs_def bin_arith_simps minus_real_number_of le_real_number_of_eq_not_less less_real_number_of real_of_int_le_iff) |
|
17 |
done |
|
18 |
||
19 |
declare abs_nat_number_of [simp] |
|
20 |
||
21 |
lemma abs_split [arith_split]: |
|
22 |
"P(abs (x::real)) = ((0 <= x --> P x) & (x < 0 --> P(-x)))" |
|
23 |
apply (unfold real_abs_def, auto) |
|
24 |
done |
|
25 |
||
26 |
||
27 |
(*---------------------------------------------------------------------------- |
|
28 |
Properties of the absolute value function over the reals |
|
29 |
(adapted version of previously proved theorems about abs) |
|
30 |
----------------------------------------------------------------------------*) |
|
31 |
||
32 |
lemma abs_iff: "abs (r::real) = (if 0<=r then r else -r)" |
|
33 |
apply (unfold real_abs_def, auto) |
|
34 |
done |
|
35 |
||
36 |
lemma abs_zero: "abs 0 = (0::real)" |
|
37 |
by (unfold real_abs_def, auto) |
|
38 |
declare abs_zero [simp] |
|
39 |
||
40 |
lemma abs_one: "abs (1::real) = 1" |
|
41 |
by (unfold real_abs_def, simp) |
|
42 |
declare abs_one [simp] |
|
43 |
||
44 |
lemma abs_eqI1: "(0::real)<=x ==> abs x = x" |
|
45 |
by (unfold real_abs_def, simp) |
|
46 |
||
47 |
lemma abs_eqI2: "(0::real) < x ==> abs x = x" |
|
48 |
by (unfold real_abs_def, simp) |
|
49 |
||
50 |
lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x" |
|
51 |
by (unfold real_abs_def real_le_def, simp) |
|
52 |
||
53 |
lemma abs_minus_eqI1: "x<=(0::real) ==> abs x = -x" |
|
54 |
by (unfold real_abs_def, simp) |
|
55 |
||
56 |
lemma abs_ge_zero: "(0::real)<= abs x" |
|
57 |
by (unfold real_abs_def, simp) |
|
58 |
declare abs_ge_zero [simp] |
|
59 |
||
60 |
lemma abs_idempotent: "abs(abs x)=abs (x::real)" |
|
61 |
by (unfold real_abs_def, simp) |
|
62 |
declare abs_idempotent [simp] |
|
63 |
||
64 |
lemma abs_zero_iff: "(abs x = 0) = (x=(0::real))" |
|
65 |
by (unfold real_abs_def, simp) |
|
66 |
declare abs_zero_iff [iff] |
|
67 |
||
68 |
lemma abs_ge_self: "x<=abs (x::real)" |
|
69 |
by (unfold real_abs_def, simp) |
|
70 |
||
71 |
lemma abs_ge_minus_self: "-x<=abs (x::real)" |
|
72 |
by (unfold real_abs_def, simp) |
|
73 |
||
74 |
lemma abs_mult: "abs (x * y) = abs x * abs (y::real)" |
|
75 |
apply (unfold real_abs_def) |
|
76 |
apply (auto dest!: order_antisym simp add: real_0_le_mult_iff) |
|
77 |
done |
|
78 |
||
79 |
lemma abs_inverse: "abs(inverse(x::real)) = inverse(abs(x))" |
|
80 |
apply (unfold real_abs_def) |
|
81 |
apply (case_tac "x=0") |
|
82 |
apply (auto simp add: real_minus_inverse real_le_less INVERSE_ZERO real_inverse_gt_0) |
|
83 |
done |
|
84 |
||
85 |
lemma abs_mult_inverse: "abs (x * inverse y) = (abs x) * inverse (abs (y::real))" |
|
86 |
by (simp add: abs_mult abs_inverse) |
|
87 |
||
88 |
lemma abs_triangle_ineq: "abs(x+y) <= abs x + abs (y::real)" |
|
89 |
by (unfold real_abs_def, simp) |
|
90 |
||
91 |
(*Unused, but perhaps interesting as an example*) |
|
92 |
lemma abs_triangle_ineq_four: "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)" |
|
93 |
by (simp add: abs_triangle_ineq [THEN order_trans]) |
|
94 |
||
95 |
lemma abs_minus_cancel: "abs(-x)=abs(x::real)" |
|
96 |
by (unfold real_abs_def, simp) |
|
97 |
declare abs_minus_cancel [simp] |
|
98 |
||
99 |
lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" |
|
100 |
by (unfold real_abs_def, simp) |
|
101 |
||
102 |
lemma abs_triangle_minus_ineq: "abs(x + (-y)) <= abs x + abs (y::real)" |
|
103 |
by (unfold real_abs_def, simp) |
|
104 |
||
105 |
lemma abs_add_less [rule_format (no_asm)]: "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)" |
|
106 |
by (unfold real_abs_def, simp) |
|
107 |
||
108 |
lemma abs_add_minus_less: "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)" |
|
109 |
by (unfold real_abs_def, simp) |
|
110 |
||
111 |
(* lemmas manipulating terms *) |
|
112 |
lemma real_mult_0_less: "((0::real)*x < r)=(0 < r)" |
|
113 |
by simp |
|
114 |
||
115 |
lemma real_mult_less_trans: "[| (0::real) < y; x < r; y*r < t*s |] ==> y*x < t*s" |
|
116 |
by (blast intro!: real_mult_less_mono2 intro: order_less_trans) |
|
117 |
||
118 |
(*USED ONLY IN NEXT THM*) |
|
119 |
lemma real_mult_le_less_trans: |
|
120 |
"[| (0::real)<=y; x < r; y*r < t*s; 0 < t*s|] ==> y*x < t*s" |
|
121 |
apply (drule order_le_imp_less_or_eq) |
|
122 |
apply (fast elim: real_mult_0_less [THEN iffD2] real_mult_less_trans) |
|
123 |
done |
|
124 |
||
125 |
lemma abs_mult_less: "[| abs x < r; abs y < s |] ==> abs(x*y) < r*(s::real)" |
|
126 |
apply (simp add: abs_mult) |
|
127 |
apply (rule real_mult_le_less_trans) |
|
128 |
apply (rule abs_ge_zero, assumption) |
|
129 |
apply (rule_tac [2] real_mult_order) |
|
130 |
apply (auto intro!: real_mult_less_mono1 abs_ge_zero intro: order_le_less_trans) |
|
131 |
done |
|
132 |
||
133 |
lemma abs_mult_less2: "[| abs x < r; abs y < s |] ==> abs(x)*abs(y) < r*(s::real)" |
|
134 |
by (auto intro: abs_mult_less simp add: abs_mult [symmetric]) |
|
135 |
||
136 |
lemma abs_less_gt_zero: "abs(x) < r ==> (0::real) < r" |
|
137 |
by (blast intro!: order_le_less_trans abs_ge_zero) |
|
138 |
||
139 |
lemma abs_minus_one: "abs (-1) = (1::real)" |
|
140 |
by (unfold real_abs_def, simp) |
|
141 |
declare abs_minus_one [simp] |
|
142 |
||
143 |
lemma abs_disj: "abs x =x | abs x = -(x::real)" |
|
144 |
by (unfold real_abs_def, auto) |
|
145 |
||
146 |
lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))" |
|
147 |
by (unfold real_abs_def, auto) |
|
148 |
||
149 |
lemma abs_le_interval_iff: "(abs x <= r) = (-r<=x & x<=(r::real))" |
|
150 |
by (unfold real_abs_def, auto) |
|
151 |
||
152 |
lemma abs_add_pos_gt_zero: "(0::real) < k ==> 0 < k + abs(x)" |
|
153 |
by (unfold real_abs_def, auto) |
|
154 |
||
155 |
lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)" |
|
156 |
by (unfold real_abs_def, auto) |
|
157 |
declare abs_add_one_gt_zero [simp] |
|
158 |
||
159 |
lemma abs_not_less_zero: "~ abs x < (0::real)" |
|
160 |
by (unfold real_abs_def, auto) |
|
161 |
declare abs_not_less_zero [simp] |
|
162 |
||
163 |
lemma abs_circle: "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)" |
|
164 |
by (auto intro: abs_triangle_ineq [THEN order_le_less_trans]) |
|
165 |
||
166 |
lemma abs_le_zero_iff: "(abs x <= (0::real)) = (x = 0)" |
|
167 |
by (unfold real_abs_def, auto) |
|
168 |
declare abs_le_zero_iff [simp] |
|
169 |
||
170 |
lemma real_0_less_abs_iff: "((0::real) < abs x) = (x ~= 0)" |
|
171 |
by (simp add: real_abs_def, arith) |
|
172 |
declare real_0_less_abs_iff [simp] |
|
173 |
||
174 |
lemma abs_real_of_nat_cancel: "abs (real x) = real (x::nat)" |
|
175 |
by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) |
|
176 |
declare abs_real_of_nat_cancel [simp] |
|
177 |
||
178 |
lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x" |
|
179 |
apply (rule real_leD) |
|
180 |
apply (auto intro: abs_ge_self [THEN order_trans]) |
|
181 |
done |
|
182 |
declare abs_add_one_not_less_self [simp] |
|
183 |
||
184 |
(* used in vector theory *) |
|
185 |
lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)" |
|
14270 | 186 |
by (auto intro!: abs_triangle_ineq [THEN order_trans] real_add_left_mono |
187 |
simp add: real_add_assoc) |
|
14269 | 188 |
|
189 |
lemma abs_diff_less_imp_gt_zero: "abs(x - y) < y ==> (0::real) < y" |
|
190 |
apply (unfold real_abs_def) |
|
191 |
apply (case_tac "0 <= x - y", auto) |
|
192 |
done |
|
193 |
||
194 |
lemma abs_diff_less_imp_gt_zero2: "abs(x - y) < x ==> (0::real) < x" |
|
195 |
apply (unfold real_abs_def) |
|
196 |
apply (case_tac "0 <= x - y", auto) |
|
197 |
done |
|
198 |
||
199 |
lemma abs_diff_less_imp_gt_zero3: "abs(x - y) < y ==> (0::real) < x" |
|
200 |
by (auto simp add: abs_interval_iff) |
|
201 |
||
202 |
lemma abs_diff_less_imp_gt_zero4: "abs(x - y) < -y ==> x < (0::real)" |
|
203 |
by (auto simp add: abs_interval_iff) |
|
204 |
||
205 |
lemma abs_triangle_ineq_minus_cancel: |
|
206 |
"abs(x) <= abs(x + (-y)) + abs((y::real))" |
|
207 |
apply (unfold real_abs_def, auto) |
|
208 |
done |
|
209 |
||
210 |
lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)" |
|
211 |
apply (simp add: real_add_assoc) |
|
212 |
apply (rule_tac x1 = y in real_add_left_commute [THEN ssubst]) |
|
213 |
apply (rule real_add_assoc [THEN subst]) |
|
214 |
apply (rule abs_triangle_ineq) |
|
215 |
done |
|
216 |
||
217 |
ML |
|
218 |
{* |
|
219 |
val abs_nat_number_of = thm"abs_nat_number_of"; |
|
220 |
val abs_split = thm"abs_split"; |
|
221 |
val abs_iff = thm"abs_iff"; |
|
222 |
val abs_zero = thm"abs_zero"; |
|
223 |
val abs_one = thm"abs_one"; |
|
224 |
val abs_eqI1 = thm"abs_eqI1"; |
|
225 |
val abs_eqI2 = thm"abs_eqI2"; |
|
226 |
val abs_minus_eqI2 = thm"abs_minus_eqI2"; |
|
227 |
val abs_minus_eqI1 = thm"abs_minus_eqI1"; |
|
228 |
val abs_ge_zero = thm"abs_ge_zero"; |
|
229 |
val abs_idempotent = thm"abs_idempotent"; |
|
230 |
val abs_zero_iff = thm"abs_zero_iff"; |
|
231 |
val abs_ge_self = thm"abs_ge_self"; |
|
232 |
val abs_ge_minus_self = thm"abs_ge_minus_self"; |
|
233 |
val abs_mult = thm"abs_mult"; |
|
234 |
val abs_inverse = thm"abs_inverse"; |
|
235 |
val abs_mult_inverse = thm"abs_mult_inverse"; |
|
236 |
val abs_triangle_ineq = thm"abs_triangle_ineq"; |
|
237 |
val abs_triangle_ineq_four = thm"abs_triangle_ineq_four"; |
|
238 |
val abs_minus_cancel = thm"abs_minus_cancel"; |
|
239 |
val abs_minus_add_cancel = thm"abs_minus_add_cancel"; |
|
240 |
val abs_triangle_minus_ineq = thm"abs_triangle_minus_ineq"; |
|
241 |
val abs_add_less = thm"abs_add_less"; |
|
242 |
val abs_add_minus_less = thm"abs_add_minus_less"; |
|
243 |
val real_mult_0_less = thm"real_mult_0_less"; |
|
244 |
val real_mult_less_trans = thm"real_mult_less_trans"; |
|
245 |
val real_mult_le_less_trans = thm"real_mult_le_less_trans"; |
|
246 |
val abs_mult_less = thm"abs_mult_less"; |
|
247 |
val abs_mult_less2 = thm"abs_mult_less2"; |
|
248 |
val abs_less_gt_zero = thm"abs_less_gt_zero"; |
|
249 |
val abs_minus_one = thm"abs_minus_one"; |
|
250 |
val abs_disj = thm"abs_disj"; |
|
251 |
val abs_interval_iff = thm"abs_interval_iff"; |
|
252 |
val abs_le_interval_iff = thm"abs_le_interval_iff"; |
|
253 |
val abs_add_pos_gt_zero = thm"abs_add_pos_gt_zero"; |
|
254 |
val abs_add_one_gt_zero = thm"abs_add_one_gt_zero"; |
|
255 |
val abs_not_less_zero = thm"abs_not_less_zero"; |
|
256 |
val abs_circle = thm"abs_circle"; |
|
257 |
val abs_le_zero_iff = thm"abs_le_zero_iff"; |
|
258 |
val real_0_less_abs_iff = thm"real_0_less_abs_iff"; |
|
259 |
val abs_real_of_nat_cancel = thm"abs_real_of_nat_cancel"; |
|
260 |
val abs_add_one_not_less_self = thm"abs_add_one_not_less_self"; |
|
261 |
val abs_triangle_ineq_three = thm"abs_triangle_ineq_three"; |
|
262 |
val abs_diff_less_imp_gt_zero = thm"abs_diff_less_imp_gt_zero"; |
|
263 |
val abs_diff_less_imp_gt_zero2 = thm"abs_diff_less_imp_gt_zero2"; |
|
264 |
val abs_diff_less_imp_gt_zero3 = thm"abs_diff_less_imp_gt_zero3"; |
|
265 |
val abs_diff_less_imp_gt_zero4 = thm"abs_diff_less_imp_gt_zero4"; |
|
266 |
val abs_triangle_ineq_minus_cancel = thm"abs_triangle_ineq_minus_cancel"; |
|
267 |
val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq"; |
|
268 |
*} |
|
269 |
||
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
270 |
end |