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