author | paulson |
Thu, 23 Sep 1999 18:39:05 +0200 | |
changeset 7588 | 26384af93359 |
parent 7219 | 4e3f386c2e37 |
child 8838 | 4eaa99f0d223 |
permissions | -rw-r--r-- |
5078 | 1 |
(* Title : RealAbs.ML |
7219 | 2 |
ID : $Id$ |
5078 | 3 |
Author : Jacques D. Fleuriot |
4 |
Copyright : 1998 University of Cambridge |
|
5 |
Description : Absolute value function for the reals |
|
6 |
*) |
|
7 |
||
8 |
(*---------------------------------------------------------------------------- |
|
9 |
Properties of the absolute value function over the reals |
|
10 |
(adapted version of previously proved theorems about abs) |
|
11 |
----------------------------------------------------------------------------*) |
|
5588 | 12 |
Goalw [rabs_def] "rabs r = (if 0r<=r then r else -r)"; |
5459 | 13 |
by Auto_tac; |
5078 | 14 |
qed "rabs_iff"; |
15 |
||
16 |
Goalw [rabs_def] "rabs 0r = 0r"; |
|
17 |
by (rtac (real_le_refl RS if_P) 1); |
|
18 |
qed "rabs_zero"; |
|
19 |
||
20 |
Addsimps [rabs_zero]; |
|
21 |
||
5588 | 22 |
Goalw [rabs_def] "rabs 0r = -0r"; |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
23 |
by (Simp_tac 1); |
5078 | 24 |
qed "rabs_minus_zero"; |
25 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
26 |
Goalw [rabs_def] "0r<=x ==> rabs x = x"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
27 |
by (Asm_simp_tac 1); |
5078 | 28 |
qed "rabs_eqI1"; |
29 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
30 |
Goalw [rabs_def] "0r<x ==> rabs x = x"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
31 |
by (Asm_simp_tac 1); |
5078 | 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 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
38 |
Goalw [rabs_def] "x<=0r ==> rabs x = -x"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
39 |
by (asm_full_simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
5078 | 40 |
qed "rabs_minus_eqI1"; |
41 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
42 |
Goalw [rabs_def] "0r<= rabs x"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
43 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
5078 | 44 |
qed "rabs_ge_zero"; |
45 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
46 |
Goalw [rabs_def] "rabs(rabs x)=rabs x"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
47 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
5078 | 48 |
qed "rabs_idempotent"; |
49 |
||
50 |
Goalw [rabs_def] "(x=0r) = (rabs x = 0r)"; |
|
5588 | 51 |
by (Full_simp_tac 1); |
5078 | 52 |
qed "rabs_zero_iff"; |
53 |
||
54 |
Goal "(x ~= 0r) = (rabs x ~= 0r)"; |
|
5588 | 55 |
by (full_simp_tac (simpset() addsimps [rabs_zero_iff RS sym]) 1); |
5078 | 56 |
qed "rabs_not_zero_iff"; |
57 |
||
58 |
Goalw [rabs_def] "x<=rabs x"; |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
59 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
5078 | 60 |
qed "rabs_ge_self"; |
61 |
||
5588 | 62 |
Goalw [rabs_def] "-x<=rabs x"; |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
63 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
5078 | 64 |
qed "rabs_ge_minus_self"; |
65 |
||
66 |
(* case splits nightmare *) |
|
67 |
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
|
68 |
by (auto_tac (claset(), |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
69 |
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
|
70 |
real_minus_mult_eq2])); |
5078 | 71 |
by (blast_tac (claset() addDs [real_le_mult_order]) 1); |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
72 |
by (auto_tac (claset() addSDs [not_real_leE], simpset())); |
5078 | 73 |
by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]); |
74 |
by (EVERY[dtac real_mult_le_zero 3, assume_tac 3, dtac real_le_anti_sym 3]); |
|
75 |
by (dtac real_mult_less_zero1 5 THEN assume_tac 5); |
|
76 |
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
|
77 |
simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac)); |
5078 | 78 |
qed "rabs_mult"; |
79 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
80 |
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
|
81 |
by (auto_tac (claset(), simpset() addsimps [real_minus_rinv])); |
5078 | 82 |
by (ALLGOALS(dtac not_real_leE)); |
83 |
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
|
84 |
by (blast_tac (claset() addDs [real_le_imp_less_or_eq, real_rinv_gt_zero]) 1); |
5078 | 85 |
by (dtac (rinv_not_zero RS not_sym) 1); |
86 |
by (rtac (real_rinv_less_zero RSN (2,real_less_asym)) 1); |
|
87 |
by (assume_tac 2); |
|
88 |
by (blast_tac (claset() addSDs [real_le_imp_less_or_eq]) 1); |
|
89 |
qed "rabs_rinv"; |
|
90 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
91 |
Goal "y ~= 0r ==> rabs(x*rinv(y)) = rabs(x)*rinv(rabs(y))"; |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
92 |
by (asm_simp_tac (simpset() addsimps [rabs_mult, rabs_rinv]) 1); |
5078 | 93 |
qed "rabs_mult_rinv"; |
94 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
95 |
Goalw [rabs_def] "rabs(x+y) <= rabs x + rabs y"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
96 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
5078 | 97 |
qed "rabs_triangle_ineq"; |
98 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
99 |
(*Unused, but perhaps interesting as an example*) |
5078 | 100 |
Goal "rabs(w + x + y + z) <= rabs(w) + rabs(x) + rabs(y) + rabs(z)"; |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
101 |
by (simp_tac (simpset() addsimps [rabs_triangle_ineq RS order_trans]) 1); |
5078 | 102 |
qed "rabs_triangle_ineq_four"; |
103 |
||
5588 | 104 |
Goalw [rabs_def] "rabs(-x)=rabs(x)"; |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
105 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
5078 | 106 |
qed "rabs_minus_cancel"; |
107 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
108 |
Goalw [rabs_def] "rabs(x + (-y)) = rabs (y + (-x))"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
109 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
110 |
qed "rabs_minus_add_cancel"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
111 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
112 |
Goalw [rabs_def] "rabs(x + (-y)) <= rabs x + rabs y"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
113 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
5078 | 114 |
qed "rabs_triangle_minus_ineq"; |
115 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
116 |
Goalw [rabs_def] "rabs x < r --> rabs y < s --> rabs(x+y) < r+s"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
117 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
118 |
qed_spec_mp "rabs_add_less"; |
5078 | 119 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
120 |
Goalw [rabs_def] "rabs x < r --> rabs y < s --> rabs(x+ (-y)) < r+s"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
121 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
5078 | 122 |
qed "rabs_add_minus_less"; |
123 |
||
124 |
(* lemmas manipulating terms *) |
|
125 |
Goal "(0r*x<r)=(0r<r)"; |
|
126 |
by (Simp_tac 1); |
|
127 |
qed "real_mult_0_less"; |
|
128 |
||
129 |
Goal "[| 0r<y; x<r; y*r<t*s |] ==> y*x<t*s"; |
|
5459 | 130 |
by (blast_tac (claset() addSIs [real_mult_less_mono2] |
131 |
addIs [real_less_trans]) 1); |
|
5078 | 132 |
qed "real_mult_less_trans"; |
133 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
134 |
Goal "[| 0r<=y; x<r; y*r<t*s; 0r<t*s|] ==> y*x<t*s"; |
5078 | 135 |
by (dtac real_le_imp_less_or_eq 1); |
5459 | 136 |
by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2, |
137 |
real_mult_less_trans]) 1); |
|
5078 | 138 |
qed "real_mult_le_less_trans"; |
139 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
140 |
(* proofs lifted from previous older version |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
141 |
FIXME: use a stronger version of real_mult_less_mono *) |
5078 | 142 |
Goal "[| rabs x<r; rabs y<s |] ==> rabs(x*y)<r*s"; |
143 |
by (simp_tac (simpset() addsimps [rabs_mult]) 1); |
|
144 |
by (rtac real_mult_le_less_trans 1); |
|
145 |
by (rtac rabs_ge_zero 1); |
|
146 |
by (assume_tac 1); |
|
147 |
by (blast_tac (HOL_cs addIs [rabs_ge_zero, real_mult_less_mono1, |
|
148 |
real_le_less_trans]) 1); |
|
149 |
by (blast_tac (HOL_cs addIs [rabs_ge_zero, real_mult_order, |
|
150 |
real_le_less_trans]) 1); |
|
151 |
qed "rabs_mult_less"; |
|
152 |
||
5588 | 153 |
Goal "[| rabs x < r; rabs y < s |] ==> rabs(x)*rabs(y)<r*s"; |
5078 | 154 |
by (auto_tac (claset() addIs [rabs_mult_less], |
155 |
simpset() addsimps [rabs_mult RS sym])); |
|
156 |
qed "rabs_mult_less2"; |
|
157 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
158 |
Goal "1r < rabs x ==> rabs y <= rabs(x*y)"; |
5078 | 159 |
by (cut_inst_tac [("x1","y")] (rabs_ge_zero RS real_le_imp_less_or_eq) 1); |
160 |
by (EVERY1[etac disjE,rtac real_less_imp_le]); |
|
161 |
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
|
162 |
by (forw_inst_tac [("y","rabs x + (-1r)")] real_mult_order 1); |
5078 | 163 |
by (assume_tac 1); |
164 |
by (rtac real_sum_gt_zero_less 1); |
|
165 |
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
|
166 |
real_mult_commute, rabs_mult]) 1); |
5078 | 167 |
by (dtac sym 1); |
5588 | 168 |
by (asm_full_simp_tac (simpset() addsimps [rabs_mult]) 1); |
5078 | 169 |
qed "rabs_mult_le"; |
170 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
171 |
Goal "[| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)"; |
5459 | 172 |
by (blast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1); |
5078 | 173 |
qed "rabs_mult_gt"; |
174 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
175 |
Goal "rabs(x)<r ==> 0r<r"; |
5078 | 176 |
by (blast_tac (claset() addSIs [real_le_less_trans,rabs_ge_zero]) 1); |
177 |
qed "rabs_less_gt_zero"; |
|
178 |
||
179 |
Goalw [rabs_def] "rabs 1r = 1r"; |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
180 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1]) 1); |
5078 | 181 |
qed "rabs_one"; |
182 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
183 |
Goalw [rabs_def] "rabs x =x | rabs x = -x"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
184 |
by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0])); |
5078 | 185 |
qed "rabs_disj"; |
186 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
187 |
Goalw [rabs_def] "(rabs x < r) = (-r<x & x<r)"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
188 |
by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0])); |
5078 | 189 |
qed "rabs_interval_iff"; |
190 |
||
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
191 |
Goalw [rabs_def] "(rabs x <= r) = (-r<=x & x<=r)"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
192 |
by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0])); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
193 |
qed "rabs_le_interval_iff"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
194 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
195 |
Goalw [rabs_def] "(rabs (x + (-y)) < r) = (y + (-r) < x & x < y + r)"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
196 |
by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0])); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
197 |
qed "rabs_add_minus_interval_iff"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
198 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
199 |
Goalw [rabs_def] "0r < k ==> 0r < k + rabs(x)"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
200 |
by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0])); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
201 |
qed "rabs_add_pos_gt_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
202 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
203 |
Goalw [rabs_def] "0r < 1r + rabs(x)"; |
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
204 |
by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1])); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
205 |
qed "rabs_add_one_gt_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
206 |
Addsimps [rabs_add_one_gt_zero]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
207 |