author | paulson |
Tue, 19 Dec 2000 15:06:59 +0100 | |
changeset 10699 | f0c3da8477e9 |
parent 10690 | cd80241125b0 |
child 10715 | c838477b5c18 |
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 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
8 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
9 |
(** abs (absolute value) **) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
10 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
11 |
Goalw [abs_real_def] |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
12 |
"abs (number_of v :: real) = \ |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
13 |
\ (if neg (number_of v) then number_of (bin_minus v) \ |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
14 |
\ else number_of v)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
15 |
by (simp_tac |
9432 | 16 |
(simpset () addsimps |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
17 |
bin_arith_simps@ |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
18 |
[minus_real_number_of, zero_eq_numeral_0, le_real_number_of_eq_not_less, |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
19 |
less_real_number_of, real_of_int_le_iff]) 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
20 |
qed "abs_nat_number_of"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
21 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
22 |
Addsimps [abs_nat_number_of]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
23 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
24 |
Goalw [abs_real_def] |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
25 |
"P(abs (x::real)) = ((#0 <= x --> P x) & (x < #0 --> P(-x)))"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
26 |
by(auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0])); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
27 |
qed "abs_split"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
28 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
29 |
|
5078 | 30 |
(*---------------------------------------------------------------------------- |
31 |
Properties of the absolute value function over the reals |
|
32 |
(adapted version of previously proved theorems about abs) |
|
33 |
----------------------------------------------------------------------------*) |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
34 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
35 |
Goalw [abs_real_def] "abs (r::real) = (if #0<=r then r else -r)"; |
5459 | 36 |
by Auto_tac; |
8838 | 37 |
qed "abs_iff"; |
5078 | 38 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
39 |
Goalw [abs_real_def] "abs #0 = (#0::real)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
40 |
by Auto_tac; |
8838 | 41 |
qed "abs_zero"; |
42 |
Addsimps [abs_zero]; |
|
5078 | 43 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
44 |
Goalw [abs_real_def] "abs (#0::real) = -#0"; |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
45 |
by (Simp_tac 1); |
8838 | 46 |
qed "abs_minus_zero"; |
5078 | 47 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
48 |
Goalw [abs_real_def] "(#0::real)<=x ==> abs x = x"; |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
49 |
by (Asm_simp_tac 1); |
8838 | 50 |
qed "abs_eqI1"; |
5078 | 51 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
52 |
Goalw [abs_real_def] "(#0::real)<x ==> abs x = x"; |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
53 |
by (Asm_simp_tac 1); |
8838 | 54 |
qed "abs_eqI2"; |
5078 | 55 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
56 |
Goalw [abs_real_def,real_le_def] "x<(#0::real) ==> abs x = -x"; |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
57 |
by (Asm_simp_tac 1); |
8838 | 58 |
qed "abs_minus_eqI2"; |
5078 | 59 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
60 |
Goalw [abs_real_def] "x<=(#0::real) ==> abs x = -x"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
61 |
by (Asm_simp_tac 1); |
8838 | 62 |
qed "abs_minus_eqI1"; |
5078 | 63 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
64 |
Goalw [abs_real_def] "(#0::real)<= abs x"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
65 |
by (Simp_tac 1); |
8838 | 66 |
qed "abs_ge_zero"; |
5078 | 67 |
|
8838 | 68 |
Goalw [abs_real_def] "abs(abs x)=abs (x::real)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
69 |
by (Simp_tac 1); |
8838 | 70 |
qed "abs_idempotent"; |
10690 | 71 |
Addsimps [abs_idempotent]; |
5078 | 72 |
|
10699 | 73 |
Goalw [abs_real_def] "(abs x = #0) = (x=(#0::real))"; |
5588 | 74 |
by (Full_simp_tac 1); |
8838 | 75 |
qed "abs_zero_iff"; |
10699 | 76 |
AddIffs [abs_zero_iff]; |
5078 | 77 |
|
8838 | 78 |
Goalw [abs_real_def] "x<=abs (x::real)"; |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
79 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
8838 | 80 |
qed "abs_ge_self"; |
5078 | 81 |
|
8838 | 82 |
Goalw [abs_real_def] "-x<=abs (x::real)"; |
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
83 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
8838 | 84 |
qed "abs_ge_minus_self"; |
5078 | 85 |
|
8838 | 86 |
Goalw [abs_real_def] "abs (x * y) = abs x * abs (y::real)"; |
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
87 |
by (auto_tac (claset() addSDs [order_antisym], |
9065 | 88 |
simpset() addsimps [real_0_le_mult_iff])); |
8838 | 89 |
qed "abs_mult"; |
5078 | 90 |
|
10648 | 91 |
Goalw [abs_real_def] "abs(inverse(x::real)) = inverse(abs(x))"; |
92 |
by (real_div_undefined_case_tac "x=0" 1); |
|
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
93 |
by (auto_tac (claset(), |
10648 | 94 |
simpset() addsimps [real_minus_inverse, real_le_less] @ |
95 |
(map rename_numerals [INVERSE_ZERO, real_inverse_gt_zero]))); |
|
10606 | 96 |
qed "abs_inverse"; |
5078 | 97 |
|
10648 | 98 |
Goal "abs (x * inverse y) = (abs x) * inverse (abs (y::real))"; |
10606 | 99 |
by (asm_simp_tac (simpset() addsimps [abs_mult, abs_inverse]) 1); |
100 |
qed "abs_mult_inverse"; |
|
5078 | 101 |
|
8838 | 102 |
Goalw [abs_real_def] "abs(x+y) <= abs x + abs (y::real)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
103 |
by (Simp_tac 1); |
8838 | 104 |
qed "abs_triangle_ineq"; |
5078 | 105 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
106 |
(*Unused, but perhaps interesting as an example*) |
8838 | 107 |
Goal "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)"; |
108 |
by (simp_tac (simpset() addsimps [abs_triangle_ineq RS order_trans]) 1); |
|
109 |
qed "abs_triangle_ineq_four"; |
|
5078 | 110 |
|
8838 | 111 |
Goalw [abs_real_def] "abs(-x)=abs(x::real)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
112 |
by (Simp_tac 1); |
8838 | 113 |
qed "abs_minus_cancel"; |
5078 | 114 |
|
8838 | 115 |
Goalw [abs_real_def] "abs(x + (-y)) = abs (y + (-(x::real)))"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
116 |
by (Simp_tac 1); |
8838 | 117 |
qed "abs_minus_add_cancel"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
118 |
|
8838 | 119 |
Goalw [abs_real_def] "abs(x + (-y)) <= abs x + abs (y::real)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
120 |
by (Simp_tac 1); |
8838 | 121 |
qed "abs_triangle_minus_ineq"; |
5078 | 122 |
|
8838 | 123 |
Goalw [abs_real_def] "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
124 |
by (Simp_tac 1); |
8838 | 125 |
qed_spec_mp "abs_add_less"; |
5078 | 126 |
|
8838 | 127 |
Goalw [abs_real_def] "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
128 |
by (Simp_tac 1); |
8838 | 129 |
qed "abs_add_minus_less"; |
5078 | 130 |
|
131 |
(* lemmas manipulating terms *) |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
132 |
Goal "((#0::real)*x<r)=(#0<r)"; |
5078 | 133 |
by (Simp_tac 1); |
134 |
qed "real_mult_0_less"; |
|
135 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
136 |
Goal "[| (#0::real)<y; x<r; y*r<t*s |] ==> y*x<t*s"; |
9432 | 137 |
by (blast_tac (claset() addSIs [rename_numerals real_mult_less_mono2] |
9065 | 138 |
addIs [real_less_trans]) 1); |
5078 | 139 |
qed "real_mult_less_trans"; |
140 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
141 |
Goal "[| (#0::real)<=y; x<r; y*r<t*s; #0<t*s|] ==> y*x<t*s"; |
5078 | 142 |
by (dtac real_le_imp_less_or_eq 1); |
5459 | 143 |
by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2, |
144 |
real_mult_less_trans]) 1); |
|
5078 | 145 |
qed "real_mult_le_less_trans"; |
146 |
||
8838 | 147 |
Goal "[| abs x<r; abs y<s |] ==> abs(x*y)<r*(s::real)"; |
148 |
by (simp_tac (simpset() addsimps [abs_mult]) 1); |
|
5078 | 149 |
by (rtac real_mult_le_less_trans 1); |
8838 | 150 |
by (rtac abs_ge_zero 1); |
5078 | 151 |
by (assume_tac 1); |
9432 | 152 |
by (rtac (rename_numerals real_mult_order) 2); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
153 |
by (auto_tac (claset() addSIs [real_mult_less_mono1, |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
154 |
abs_ge_zero] addIs [real_le_less_trans],simpset())); |
8838 | 155 |
qed "abs_mult_less"; |
5078 | 156 |
|
8838 | 157 |
Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y)<r*(s::real)"; |
158 |
by (auto_tac (claset() addIs [abs_mult_less], |
|
159 |
simpset() addsimps [abs_mult RS sym])); |
|
160 |
qed "abs_mult_less2"; |
|
5078 | 161 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
162 |
Goal "(#1::real) < abs x ==> abs y <= abs(x*y)"; |
8838 | 163 |
by (cut_inst_tac [("x1","y")] (abs_ge_zero RS real_le_imp_less_or_eq) 1); |
5078 | 164 |
by (EVERY1[etac disjE,rtac real_less_imp_le]); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
165 |
by (dres_inst_tac [("W","#1")] real_less_sum_gt_zero 1); |
9065 | 166 |
by (forw_inst_tac [("y","abs x + (-#1)")] |
9432 | 167 |
(rename_numerals real_mult_order) 1); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
168 |
by (rtac real_sum_gt_zero_less 2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
169 |
by (asm_full_simp_tac (simpset() |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
170 |
addsimps [real_add_mult_distrib2, |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
171 |
real_mult_commute, abs_mult]) 2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
172 |
by (dtac sym 2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
173 |
by (auto_tac (claset(),simpset() addsimps [abs_mult])); |
8838 | 174 |
qed "abs_mult_le"; |
5078 | 175 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
176 |
Goal "[| (#1::real) < abs x; r < abs y|] ==> r < abs(x*y)"; |
8838 | 177 |
by (blast_tac (HOL_cs addIs [abs_mult_le, real_less_le_trans]) 1); |
178 |
qed "abs_mult_gt"; |
|
5078 | 179 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
180 |
Goal "abs(x)<r ==> (#0::real)<r"; |
8838 | 181 |
by (blast_tac (claset() addSIs [real_le_less_trans,abs_ge_zero]) 1); |
182 |
qed "abs_less_gt_zero"; |
|
5078 | 183 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
184 |
Goalw [abs_real_def] "abs #1 = (#1::real)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
185 |
by (Simp_tac 1); |
8838 | 186 |
qed "abs_one"; |
5078 | 187 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
188 |
Goalw [abs_real_def] "abs (-#1) = (#1::real)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
189 |
by (Simp_tac 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
190 |
qed "abs_minus_one"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
191 |
Addsimps [abs_minus_one]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
192 |
|
8838 | 193 |
Goalw [abs_real_def] "abs x =x | abs x = -(x::real)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
194 |
by Auto_tac; |
8838 | 195 |
qed "abs_disj"; |
5078 | 196 |
|
8838 | 197 |
Goalw [abs_real_def] "(abs x < r) = (-r<x & x<(r::real))"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
198 |
by Auto_tac; |
8838 | 199 |
qed "abs_interval_iff"; |
5078 | 200 |
|
8838 | 201 |
Goalw [abs_real_def] "(abs x <= r) = (-r<=x & x<=(r::real))"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
202 |
by Auto_tac; |
8838 | 203 |
qed "abs_le_interval_iff"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
204 |
|
8838 | 205 |
Goalw [abs_real_def] "(abs (x + (-y)) < r) = (y + (-r) < x & x < y + (r::real))"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
206 |
by Auto_tac; |
8838 | 207 |
qed "abs_add_minus_interval_iff"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
208 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
209 |
Goalw [abs_real_def] "(#0::real) < k ==> #0 < k + abs(x)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
210 |
by Auto_tac; |
8838 | 211 |
qed "abs_add_pos_gt_zero"; |
212 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
213 |
Goalw [abs_real_def] "(#0::real) < #1 + abs(x)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
214 |
by Auto_tac; |
8838 | 215 |
qed "abs_add_one_gt_zero"; |
216 |
Addsimps [abs_add_one_gt_zero]; |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
217 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
218 |
(* 05/2000 *) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
219 |
Goalw [abs_real_def] "~ abs x < (#0::real)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
220 |
by Auto_tac; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
221 |
qed "abs_not_less_zero"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
222 |
Addsimps [abs_not_less_zero]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
223 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
224 |
Goal "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
225 |
by (auto_tac (claset() addIs [abs_triangle_ineq RS real_le_less_trans], |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
226 |
simpset())); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
227 |
qed "abs_circle"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
228 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
229 |
Goalw [abs_real_def] "(abs x <= (#0::real)) = (x = #0)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
230 |
by Auto_tac; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
231 |
qed "abs_le_zero_iff"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
232 |
Addsimps [abs_le_zero_iff]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
233 |
|
10648 | 234 |
Goal "((#0::real) < abs x) = (x ~= 0)"; |
235 |
by (simp_tac (simpset() addsimps [abs_real_def]) 1); |
|
236 |
by (arith_tac 1); |
|
237 |
qed "real_0_less_abs_iff"; |
|
238 |
Addsimps [real_0_less_abs_iff]; |
|
239 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
240 |
Goal "abs (real_of_nat x) = real_of_nat x"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
241 |
by (auto_tac (claset() addIs [abs_eqI1],simpset() |
9432 | 242 |
addsimps [rename_numerals real_of_nat_ge_zero])); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
243 |
qed "abs_real_of_nat_cancel"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
244 |
Addsimps [abs_real_of_nat_cancel]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
245 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
246 |
Goal "~ abs(x) + (#1::real) < x"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
247 |
by (rtac real_leD 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
248 |
by (auto_tac (claset() addIs [abs_ge_self RS real_le_trans],simpset())); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
249 |
qed "abs_add_one_not_less_self"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
250 |
Addsimps [abs_add_one_not_less_self]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
251 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
252 |
(* used in vector theory *) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
253 |
Goal "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
254 |
by (auto_tac (claset() addSIs [(abs_triangle_ineq |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
255 |
RS real_le_trans),real_add_left_le_mono1], |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
256 |
simpset() addsimps [real_add_assoc])); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
257 |
qed "abs_triangle_ineq_three"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
258 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
259 |
Goalw [abs_real_def] "abs(x - y) < y ==> (#0::real) < y"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
260 |
by (case_tac "#0 <= x - y" 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
261 |
by (Auto_tac); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
262 |
qed "abs_diff_less_imp_gt_zero"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
263 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
264 |
Goalw [abs_real_def] "abs(x - y) < x ==> (#0::real) < x"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
265 |
by (case_tac "#0 <= x - y" 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
266 |
by (Auto_tac); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
267 |
qed "abs_diff_less_imp_gt_zero2"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
268 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
269 |
Goal "abs(x - y) < y ==> (#0::real) < x"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
270 |
by (auto_tac (claset(),simpset() addsimps [abs_interval_iff])); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
271 |
qed "abs_diff_less_imp_gt_zero3"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
272 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
273 |
Goal "abs(x - y) < -y ==> x < (#0::real)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
274 |
by (auto_tac (claset(),simpset() addsimps [abs_interval_iff])); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
275 |
qed "abs_diff_less_imp_gt_zero4"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
276 |
|
10043 | 277 |
Goalw [abs_real_def] |
278 |
" abs(x) <= abs(x + (-y)) + abs((y::real))"; |
|
279 |
by Auto_tac; |
|
280 |
qed "abs_triangle_ineq_minus_cancel"; |
|
281 |
||
282 |
Goal "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)"; |
|
283 |
by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); |
|
284 |
by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1); |
|
285 |
by (rtac (real_add_assoc RS subst) 1); |
|
286 |
by (rtac abs_triangle_ineq 1); |
|
287 |
qed "abs_sum_triangle_ineq"; |