author | paulson |
Thu, 29 Jul 1999 12:44:57 +0200 | |
changeset 7127 | 48e235179ffb |
parent 7077 | 60b098bb8b8a |
child 7219 | 4e3f386c2e37 |
permissions | -rw-r--r-- |
5078 | 1 |
(* Title : RealAbs.ML |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
Description : Absolute value function for the reals |
|
5 |
*) |
|
6 |
||
7 |
(*---------------------------------------------------------------------------- |
|
8 |
Properties of the absolute value function over the reals |
|
9 |
(adapted version of previously proved theorems about abs) |
|
10 |
----------------------------------------------------------------------------*) |
|
5588 | 11 |
Goalw [rabs_def] "rabs r = (if 0r<=r then r else -r)"; |
5459 | 12 |
by Auto_tac; |
5078 | 13 |
qed "rabs_iff"; |
14 |
||
15 |
Goalw [rabs_def] "rabs 0r = 0r"; |
|
16 |
by (rtac (real_le_refl RS if_P) 1); |
|
17 |
qed "rabs_zero"; |
|
18 |
||
19 |
Addsimps [rabs_zero]; |
|
20 |
||
5588 | 21 |
Goalw [rabs_def] "rabs 0r = -0r"; |
5078 | 22 |
by (stac real_minus_zero 1); |
23 |
by (rtac if_cancel 1); |
|
24 |
qed "rabs_minus_zero"; |
|
25 |
||
26 |
val [prem] = goalw thy [rabs_def] "0r<=x ==> rabs x = x"; |
|
27 |
by (rtac (prem RS if_P) 1); |
|
28 |
qed "rabs_eqI1"; |
|
29 |
||
30 |
val [prem] = goalw thy [rabs_def] "0r<x ==> rabs x = x"; |
|
31 |
by (simp_tac (simpset() addsimps [(prem RS real_less_imp_le),rabs_eqI1]) 1); |
|
32 |
qed "rabs_eqI2"; |
|
33 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
34 |
Goalw [rabs_def,real_le_def] "x<0r ==> rabs x = -x"; |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
35 |
by (Asm_simp_tac 1); |
5078 | 36 |
qed "rabs_minus_eqI2"; |
37 |
||
5588 | 38 |
Goal "x<=0r ==> rabs x = -x"; |
5078 | 39 |
by (dtac real_le_imp_less_or_eq 1); |
5459 | 40 |
by (blast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1); |
5078 | 41 |
qed "rabs_minus_eqI1"; |
42 |
||
43 |
Goalw [rabs_def,real_le_def] "0r<= rabs x"; |
|
5588 | 44 |
by (Full_simp_tac 1); |
5078 | 45 |
by (blast_tac (claset() addDs [real_minus_zero_less_iff RS iffD2, |
5588 | 46 |
real_less_asym]) 1); |
5078 | 47 |
qed "rabs_ge_zero"; |
48 |
||
49 |
Goal "rabs(rabs x)=rabs x"; |
|
50 |
by (res_inst_tac [("r1","rabs x")] (rabs_iff RS ssubst) 1); |
|
51 |
by (blast_tac (claset() addIs [if_P,rabs_ge_zero]) 1); |
|
52 |
qed "rabs_idempotent"; |
|
53 |
||
54 |
Goalw [rabs_def] "(x=0r) = (rabs x = 0r)"; |
|
5588 | 55 |
by (Full_simp_tac 1); |
5078 | 56 |
qed "rabs_zero_iff"; |
57 |
||
58 |
Goal "(x ~= 0r) = (rabs x ~= 0r)"; |
|
5588 | 59 |
by (full_simp_tac (simpset() addsimps [rabs_zero_iff RS sym]) 1); |
5078 | 60 |
qed "rabs_not_zero_iff"; |
61 |
||
62 |
Goalw [rabs_def] "x<=rabs x"; |
|
5588 | 63 |
by (Full_simp_tac 1); |
5078 | 64 |
by (auto_tac (claset() addDs [not_real_leE RS real_less_imp_le], |
5588 | 65 |
simpset() addsimps [real_le_zero_iff])); |
5078 | 66 |
qed "rabs_ge_self"; |
67 |
||
5588 | 68 |
Goalw [rabs_def] "-x<=rabs x"; |
69 |
by (full_simp_tac (simpset() addsimps [real_ge_zero_iff]) 1); |
|
5078 | 70 |
qed "rabs_ge_minus_self"; |
71 |
||
72 |
(* case splits nightmare *) |
|
73 |
Goalw [rabs_def] "rabs(x*y) = (rabs x)*(rabs y)"; |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
74 |
by (auto_tac (claset(), |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
75 |
simpset() addsimps [real_minus_mult_eq1, real_minus_mult_commute, |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
76 |
real_minus_mult_eq2])); |
5078 | 77 |
by (blast_tac (claset() addDs [real_le_mult_order]) 1); |
78 |
by (auto_tac (claset() addSDs [not_real_leE],simpset())); |
|
79 |
by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]); |
|
80 |
by (EVERY[dtac real_mult_le_zero 3, assume_tac 3, dtac real_le_anti_sym 3]); |
|
81 |
by (dtac real_mult_less_zero1 5 THEN assume_tac 5); |
|
82 |
by (auto_tac (claset() addDs [real_less_asym,sym], |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
83 |
simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac)); |
5078 | 84 |
qed "rabs_mult"; |
85 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
86 |
Goalw [rabs_def] "x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))"; |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
87 |
by (auto_tac (claset(), simpset() addsimps [real_minus_rinv])); |
5078 | 88 |
by (ALLGOALS(dtac not_real_leE)); |
89 |
by (etac real_less_asym 1); |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
90 |
by (blast_tac (claset() addDs [real_le_imp_less_or_eq, real_rinv_gt_zero]) 1); |
5078 | 91 |
by (dtac (rinv_not_zero RS not_sym) 1); |
92 |
by (rtac (real_rinv_less_zero RSN (2,real_less_asym)) 1); |
|
93 |
by (assume_tac 2); |
|
94 |
by (blast_tac (claset() addSDs [real_le_imp_less_or_eq]) 1); |
|
95 |
qed "rabs_rinv"; |
|
96 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
97 |
Goal "y ~= 0r ==> rabs(x*rinv(y)) = rabs(x)*rinv(rabs(y))"; |
5078 | 98 |
by (res_inst_tac [("c1","rabs y")] (real_mult_left_cancel RS subst) 1); |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
99 |
by (asm_simp_tac (simpset() addsimps [rabs_not_zero_iff RS sym]) 1); |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
100 |
by (asm_simp_tac (simpset() addsimps [rabs_mult RS sym, real_mult_inv_right, |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
101 |
rabs_not_zero_iff RS sym] @ real_mult_ac) 1); |
5078 | 102 |
qed "rabs_mult_rinv"; |
103 |
||
104 |
Goal "rabs(x+y) <= rabs x + rabs y"; |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
105 |
by (case_tac "0r<=x+y" 1); |
5588 | 106 |
by (asm_simp_tac |
107 |
(simpset() addsimps [rabs_eqI1,real_add_le_mono,rabs_ge_self]) 1); |
|
108 |
by (asm_simp_tac |
|
109 |
(simpset() addsimps [not_real_leE,rabs_minus_eqI2,real_add_le_mono, |
|
110 |
rabs_ge_minus_self]) 1); |
|
5078 | 111 |
qed "rabs_triangle_ineq"; |
112 |
||
113 |
Goal "rabs(w + x + y + z) <= rabs(w) + rabs(x) + rabs(y) + rabs(z)"; |
|
114 |
by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
115 |
by (blast_tac (claset() addSIs [rabs_triangle_ineq RS real_le_trans, |
5588 | 116 |
real_add_left_le_mono1]) 1); |
5078 | 117 |
qed "rabs_triangle_ineq_four"; |
118 |
||
5588 | 119 |
Goalw [rabs_def] "rabs(-x)=rabs(x)"; |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
120 |
by (auto_tac (claset() addSDs [not_real_leE,real_less_asym] |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
121 |
addIs [real_le_anti_sym], |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
122 |
simpset() addsimps [real_ge_zero_iff])); |
5078 | 123 |
qed "rabs_minus_cancel"; |
124 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
125 |
Goal "rabs(x + (-y)) = rabs (y + (-x))"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
126 |
by (rtac (rabs_minus_cancel RS subst) 1); |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
127 |
by (simp_tac (simpset() addsimps [real_add_commute]) 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
128 |
qed "rabs_minus_add_cancel"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
129 |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
130 |
Goal "rabs(x + (-y)) <= rabs x + rabs y"; |
5078 | 131 |
by (res_inst_tac [("x1","y")] (rabs_minus_cancel RS subst) 1); |
132 |
by (rtac rabs_triangle_ineq 1); |
|
133 |
qed "rabs_triangle_minus_ineq"; |
|
134 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
135 |
Goal "rabs (x + y + ((-l) + (-m))) <= rabs(x + (-l)) + rabs(y + (-m))"; |
5078 | 136 |
by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); |
137 |
by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1); |
|
138 |
by (rtac (real_add_assoc RS subst) 1); |
|
139 |
by (rtac rabs_triangle_ineq 1); |
|
140 |
qed "rabs_sum_triangle_ineq"; |
|
141 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
142 |
Goal "rabs(x) <= rabs(x + (-y)) + rabs(y)"; |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
143 |
by (res_inst_tac [("j","rabs(x + (-y) + y)")] real_le_trans 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
144 |
by (simp_tac (simpset() addsimps [real_add_assoc]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
145 |
by (simp_tac (simpset() addsimps [real_add_assoc RS sym, |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
146 |
rabs_triangle_ineq]) 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
147 |
qed "rabs_triangle_ineq_minus_cancel"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
148 |
|
5078 | 149 |
Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+y) < r+s"; |
150 |
by (rtac real_le_less_trans 1); |
|
151 |
by (rtac rabs_triangle_ineq 1); |
|
152 |
by (REPEAT (ares_tac [real_add_less_mono] 1)); |
|
153 |
qed "rabs_add_less"; |
|
154 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
155 |
Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ (-y)) < r+s"; |
5078 | 156 |
by (rotate_tac 1 1); |
157 |
by (dtac (rabs_minus_cancel RS ssubst) 1); |
|
158 |
by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1); |
|
159 |
qed "rabs_add_minus_less"; |
|
160 |
||
161 |
(* lemmas manipulating terms *) |
|
162 |
Goal "(0r*x<r)=(0r<r)"; |
|
163 |
by (Simp_tac 1); |
|
164 |
qed "real_mult_0_less"; |
|
165 |
||
166 |
Goal "[| 0r<y; x<r; y*r<t*s |] ==> y*x<t*s"; |
|
5459 | 167 |
by (blast_tac (claset() addSIs [real_mult_less_mono2] |
168 |
addIs [real_less_trans]) 1); |
|
5078 | 169 |
qed "real_mult_less_trans"; |
170 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
171 |
Goal "[| 0r<=y; x<r; y*r<t*s; 0r<t*s|] ==> y*x<t*s"; |
5078 | 172 |
by (dtac real_le_imp_less_or_eq 1); |
5459 | 173 |
by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2, |
174 |
real_mult_less_trans]) 1); |
|
5078 | 175 |
qed "real_mult_le_less_trans"; |
176 |
||
177 |
(* proofs lifted from previous older version *) |
|
178 |
Goal "[| rabs x<r; rabs y<s |] ==> rabs(x*y)<r*s"; |
|
179 |
by (simp_tac (simpset() addsimps [rabs_mult]) 1); |
|
180 |
by (rtac real_mult_le_less_trans 1); |
|
181 |
by (rtac rabs_ge_zero 1); |
|
182 |
by (assume_tac 1); |
|
183 |
by (blast_tac (HOL_cs addIs [rabs_ge_zero, real_mult_less_mono1, |
|
184 |
real_le_less_trans]) 1); |
|
185 |
by (blast_tac (HOL_cs addIs [rabs_ge_zero, real_mult_order, |
|
186 |
real_le_less_trans]) 1); |
|
187 |
qed "rabs_mult_less"; |
|
188 |
||
5588 | 189 |
Goal "[| rabs x < r; rabs y < s |] ==> rabs(x)*rabs(y)<r*s"; |
5078 | 190 |
by (auto_tac (claset() addIs [rabs_mult_less], |
191 |
simpset() addsimps [rabs_mult RS sym])); |
|
192 |
qed "rabs_mult_less2"; |
|
193 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
194 |
Goal "1r < rabs x ==> rabs y <= rabs(x*y)"; |
5078 | 195 |
by (cut_inst_tac [("x1","y")] (rabs_ge_zero RS real_le_imp_less_or_eq) 1); |
196 |
by (EVERY1[etac disjE,rtac real_less_imp_le]); |
|
197 |
by (dres_inst_tac [("W","1r")] real_less_sum_gt_zero 1); |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
198 |
by (forw_inst_tac [("y","rabs x + (-1r)")] real_mult_order 1); |
5078 | 199 |
by (assume_tac 1); |
200 |
by (rtac real_sum_gt_zero_less 1); |
|
201 |
by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2, |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
202 |
real_mult_commute, rabs_mult]) 1); |
5078 | 203 |
by (dtac sym 1); |
5588 | 204 |
by (asm_full_simp_tac (simpset() addsimps [rabs_mult]) 1); |
5078 | 205 |
qed "rabs_mult_le"; |
206 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
207 |
Goal "[| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)"; |
5459 | 208 |
by (blast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1); |
5078 | 209 |
qed "rabs_mult_gt"; |
210 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
211 |
Goal "rabs(x)<r ==> 0r<r"; |
5078 | 212 |
by (blast_tac (claset() addSIs [real_le_less_trans,rabs_ge_zero]) 1); |
213 |
qed "rabs_less_gt_zero"; |
|
214 |
||
215 |
Goalw [rabs_def] "rabs 1r = 1r"; |
|
216 |
by (auto_tac (claset() addSDs [not_real_leE RS real_less_asym], |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
217 |
simpset() addsimps [real_zero_less_one])); |
5078 | 218 |
qed "rabs_one"; |
219 |
||
220 |
Goal "[| 0r < x ; x < r |] ==> rabs x < r"; |
|
221 |
by (asm_simp_tac (simpset() addsimps [rabs_eqI2]) 1); |
|
222 |
qed "rabs_lessI"; |
|
223 |
||
5588 | 224 |
Goal "rabs x =x | rabs x = -x"; |
5078 | 225 |
by (cut_inst_tac [("R1.0","0r"),("R2.0","x")] real_linear 1); |
5459 | 226 |
by (blast_tac (claset() addIs [rabs_eqI2,rabs_minus_eqI2, |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
227 |
rabs_zero,rabs_minus_zero]) 1); |
5078 | 228 |
qed "rabs_disj"; |
229 |
||
5588 | 230 |
Goal "rabs x = y ==> x = y | -x = y"; |
5078 | 231 |
by (dtac sym 1); |
232 |
by (hyp_subst_tac 1); |
|
233 |
by (res_inst_tac [("x1","x")] (rabs_disj RS disjE) 1); |
|
234 |
by (REPEAT(Asm_simp_tac 1)); |
|
235 |
qed "rabs_eq_disj"; |
|
236 |
||
5588 | 237 |
Goal "(rabs x < r) = (-r<x & x<r)"; |
5459 | 238 |
by Safe_tac; |
5078 | 239 |
by (rtac (real_less_swap_iff RS iffD2) 1); |
240 |
by (asm_simp_tac (simpset() addsimps [(rabs_ge_minus_self |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
241 |
RS real_le_less_trans)]) 1); |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
242 |
by (asm_simp_tac (simpset() addsimps [rabs_ge_self RS real_le_less_trans]) 1); |
5078 | 243 |
by (EVERY1 [dtac (real_less_swap_iff RS iffD1), rotate_tac 1, |
244 |
dtac (real_minus_minus RS subst), |
|
245 |
cut_inst_tac [("x","x")] rabs_disj, dtac disjE ]); |
|
246 |
by (assume_tac 3 THEN Auto_tac); |
|
247 |
qed "rabs_interval_iff"; |
|
248 |
||
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
249 |
Goal "(rabs x < r) = (-x < r & x < r)"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
250 |
by (auto_tac (claset(),simpset() addsimps [rabs_interval_iff])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
251 |
by (dtac (real_less_swap_iff RS iffD1) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
252 |
by (dtac (real_less_swap_iff RS iffD1) 2); |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
253 |
by Auto_tac; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
254 |
qed "rabs_interval_iff2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
255 |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
256 |
Goal "rabs x <= r ==> -r<=x & x<=r"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
257 |
by (dtac real_le_imp_less_or_eq 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
258 |
by (auto_tac (claset() addSDs [real_less_imp_le], |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
259 |
simpset() addsimps [rabs_interval_iff,rabs_ge_self])); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
260 |
by (auto_tac (claset(),simpset() addsimps [real_le_def])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
261 |
by (dtac (real_less_swap_iff RS iffD1) 1); |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
262 |
by (auto_tac (claset() addSDs [rabs_ge_minus_self RS real_le_less_trans], |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
263 |
simpset() addsimps [real_less_not_refl])); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
264 |
qed "rabs_leD"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
265 |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
266 |
Goal "[| -r<x; x<=r |] ==> rabs x <= r"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
267 |
by (dtac real_le_imp_less_or_eq 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
268 |
by (Step_tac 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
269 |
by (blast_tac (claset() addIs |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
270 |
[rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1); |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
271 |
by (auto_tac (claset() addSDs [rabs_eqI2], |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
272 |
simpset() addsimps |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
273 |
[real_le_def,real_gt_zero_iff RS sym,real_less_not_refl])); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
274 |
qed "rabs_leI1"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
275 |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
276 |
Goal "[| -r<=x; x<=r |] ==> rabs x <= r"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
277 |
by (REPEAT(dtac real_le_imp_less_or_eq 1)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
278 |
by (Step_tac 1); |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
279 |
by (blast_tac (claset() |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
280 |
addIs [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1); |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
281 |
by (auto_tac (claset() addSDs [rabs_eqI2], |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
282 |
simpset() addsimps |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
283 |
[real_le_def,real_gt_zero_iff RS sym,real_less_not_refl, |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
284 |
rabs_minus_cancel])); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
285 |
by (cut_inst_tac [("x","r")] rabs_disj 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
286 |
by (rotate_tac 1 1); |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
287 |
by (auto_tac (claset(), simpset() addsimps [real_less_not_refl])); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
288 |
qed "rabs_leI"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
289 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
290 |
Goal "(rabs x <= r) = (-r<=x & x<=r)"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
291 |
by (blast_tac (claset() addSIs [rabs_leD,rabs_leI]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
292 |
qed "rabs_le_interval_iff"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
293 |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
294 |
Goal "(rabs (x + (-y)) < r) = (y + (-r) < x & x < y + r)"; |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
295 |
by (auto_tac (claset(), simpset() addsimps [rabs_interval_iff])); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
296 |
by (ALLGOALS(dtac real_less_sum_gt_zero)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
297 |
by (ALLGOALS(dtac real_less_sum_gt_zero)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
298 |
by (ALLGOALS(rtac real_sum_gt_zero_less)); |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
299 |
by (auto_tac (claset(), |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
300 |
simpset() addsimps [real_minus_add_distrib] @ real_add_ac)); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
301 |
qed "rabs_add_minus_interval_iff"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
302 |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
303 |
Goal "0r < k ==> 0r < k + rabs(x)"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
304 |
by (res_inst_tac [("t","0r")] (real_add_zero_right RS subst) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
305 |
by (etac (rabs_ge_zero RSN (2,real_add_less_le_mono)) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
306 |
qed "rabs_add_pos_gt_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
307 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
308 |
Goal "0r < 1r + rabs(x)"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
309 |
by (rtac (real_zero_less_one RS rabs_add_pos_gt_zero) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
310 |
qed "rabs_add_one_gt_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
311 |
Addsimps [rabs_add_one_gt_zero]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
312 |