author | fleuriot |
Thu, 21 Sep 2000 12:11:38 +0200 | |
changeset 10043 | a0364652e115 |
parent 9432 | 8b7aad2abcc9 |
child 10606 | e3229a37d53f |
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"; |
5078 | 71 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
72 |
Goalw [abs_real_def] "(x=(#0::real)) = (abs x = #0)"; |
5588 | 73 |
by (Full_simp_tac 1); |
8838 | 74 |
qed "abs_zero_iff"; |
5078 | 75 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
76 |
Goal "(x ~= (#0::real)) = (abs x ~= #0)"; |
8838 | 77 |
by (full_simp_tac (simpset() addsimps [abs_zero_iff RS sym]) 1); |
78 |
qed "abs_not_zero_iff"; |
|
5078 | 79 |
|
8838 | 80 |
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
|
81 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
8838 | 82 |
qed "abs_ge_self"; |
5078 | 83 |
|
8838 | 84 |
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
|
85 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
8838 | 86 |
qed "abs_ge_minus_self"; |
5078 | 87 |
|
8838 | 88 |
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
|
89 |
by (auto_tac (claset() addSDs [order_antisym], |
9065 | 90 |
simpset() addsimps [real_0_le_mult_iff])); |
8838 | 91 |
qed "abs_mult"; |
5078 | 92 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
93 |
Goalw [abs_real_def] "x~= (#0::real) ==> abs(rinv(x)) = rinv(abs(x))"; |
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
94 |
by (auto_tac (claset(), |
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
95 |
simpset() addsimps [real_le_less] @ |
9432 | 96 |
(map rename_numerals [real_minus_rinv, real_rinv_gt_zero]))); |
97 |
by (etac (rename_numerals (real_rinv_less_zero RSN (2,real_less_asym))) 1); |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
98 |
by (arith_tac 1); |
8838 | 99 |
qed "abs_rinv"; |
5078 | 100 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
101 |
Goal "y ~= #0 ==> abs(x*rinv(y)) = abs(x)*rinv(abs(y))"; |
8838 | 102 |
by (asm_simp_tac (simpset() addsimps [abs_mult, abs_rinv]) 1); |
103 |
qed "abs_mult_rinv"; |
|
5078 | 104 |
|
8838 | 105 |
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
|
106 |
by (Simp_tac 1); |
8838 | 107 |
qed "abs_triangle_ineq"; |
5078 | 108 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
109 |
(*Unused, but perhaps interesting as an example*) |
8838 | 110 |
Goal "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)"; |
111 |
by (simp_tac (simpset() addsimps [abs_triangle_ineq RS order_trans]) 1); |
|
112 |
qed "abs_triangle_ineq_four"; |
|
5078 | 113 |
|
8838 | 114 |
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
|
115 |
by (Simp_tac 1); |
8838 | 116 |
qed "abs_minus_cancel"; |
5078 | 117 |
|
8838 | 118 |
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
|
119 |
by (Simp_tac 1); |
8838 | 120 |
qed "abs_minus_add_cancel"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
121 |
|
8838 | 122 |
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
|
123 |
by (Simp_tac 1); |
8838 | 124 |
qed "abs_triangle_minus_ineq"; |
5078 | 125 |
|
8838 | 126 |
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
|
127 |
by (Simp_tac 1); |
8838 | 128 |
qed_spec_mp "abs_add_less"; |
5078 | 129 |
|
8838 | 130 |
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
|
131 |
by (Simp_tac 1); |
8838 | 132 |
qed "abs_add_minus_less"; |
5078 | 133 |
|
134 |
(* lemmas manipulating terms *) |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
135 |
Goal "((#0::real)*x<r)=(#0<r)"; |
5078 | 136 |
by (Simp_tac 1); |
137 |
qed "real_mult_0_less"; |
|
138 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
139 |
Goal "[| (#0::real)<y; x<r; y*r<t*s |] ==> y*x<t*s"; |
9432 | 140 |
by (blast_tac (claset() addSIs [rename_numerals real_mult_less_mono2] |
9065 | 141 |
addIs [real_less_trans]) 1); |
5078 | 142 |
qed "real_mult_less_trans"; |
143 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
144 |
Goal "[| (#0::real)<=y; x<r; y*r<t*s; #0<t*s|] ==> y*x<t*s"; |
5078 | 145 |
by (dtac real_le_imp_less_or_eq 1); |
5459 | 146 |
by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2, |
147 |
real_mult_less_trans]) 1); |
|
5078 | 148 |
qed "real_mult_le_less_trans"; |
149 |
||
8838 | 150 |
Goal "[| abs x<r; abs y<s |] ==> abs(x*y)<r*(s::real)"; |
151 |
by (simp_tac (simpset() addsimps [abs_mult]) 1); |
|
5078 | 152 |
by (rtac real_mult_le_less_trans 1); |
8838 | 153 |
by (rtac abs_ge_zero 1); |
5078 | 154 |
by (assume_tac 1); |
9432 | 155 |
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
|
156 |
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
|
157 |
abs_ge_zero] addIs [real_le_less_trans],simpset())); |
8838 | 158 |
qed "abs_mult_less"; |
5078 | 159 |
|
8838 | 160 |
Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y)<r*(s::real)"; |
161 |
by (auto_tac (claset() addIs [abs_mult_less], |
|
162 |
simpset() addsimps [abs_mult RS sym])); |
|
163 |
qed "abs_mult_less2"; |
|
5078 | 164 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
165 |
Goal "(#1::real) < abs x ==> abs y <= abs(x*y)"; |
8838 | 166 |
by (cut_inst_tac [("x1","y")] (abs_ge_zero RS real_le_imp_less_or_eq) 1); |
5078 | 167 |
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
|
168 |
by (dres_inst_tac [("W","#1")] real_less_sum_gt_zero 1); |
9065 | 169 |
by (forw_inst_tac [("y","abs x + (-#1)")] |
9432 | 170 |
(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
|
171 |
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
|
172 |
by (asm_full_simp_tac (simpset() |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
173 |
addsimps [real_add_mult_distrib2, |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
174 |
real_mult_commute, abs_mult]) 2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
175 |
by (dtac sym 2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
176 |
by (auto_tac (claset(),simpset() addsimps [abs_mult])); |
8838 | 177 |
qed "abs_mult_le"; |
5078 | 178 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
179 |
Goal "[| (#1::real) < abs x; r < abs y|] ==> r < abs(x*y)"; |
8838 | 180 |
by (blast_tac (HOL_cs addIs [abs_mult_le, real_less_le_trans]) 1); |
181 |
qed "abs_mult_gt"; |
|
5078 | 182 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
183 |
Goal "abs(x)<r ==> (#0::real)<r"; |
8838 | 184 |
by (blast_tac (claset() addSIs [real_le_less_trans,abs_ge_zero]) 1); |
185 |
qed "abs_less_gt_zero"; |
|
5078 | 186 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
187 |
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
|
188 |
by (Simp_tac 1); |
8838 | 189 |
qed "abs_one"; |
5078 | 190 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
191 |
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
|
192 |
by (Simp_tac 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
193 |
qed "abs_minus_one"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
194 |
Addsimps [abs_minus_one]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
195 |
|
8838 | 196 |
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
|
197 |
by Auto_tac; |
8838 | 198 |
qed "abs_disj"; |
5078 | 199 |
|
8838 | 200 |
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
|
201 |
by Auto_tac; |
8838 | 202 |
qed "abs_interval_iff"; |
5078 | 203 |
|
8838 | 204 |
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
|
205 |
by Auto_tac; |
8838 | 206 |
qed "abs_le_interval_iff"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
207 |
|
8838 | 208 |
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
|
209 |
by Auto_tac; |
8838 | 210 |
qed "abs_add_minus_interval_iff"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
211 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
212 |
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
|
213 |
by Auto_tac; |
8838 | 214 |
qed "abs_add_pos_gt_zero"; |
215 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
216 |
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
|
217 |
by Auto_tac; |
8838 | 218 |
qed "abs_add_one_gt_zero"; |
219 |
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
|
220 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
221 |
(* 05/2000 *) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
222 |
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
|
223 |
by Auto_tac; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
224 |
qed "abs_not_less_zero"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
225 |
Addsimps [abs_not_less_zero]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
226 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
227 |
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
|
228 |
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
|
229 |
simpset())); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
230 |
qed "abs_circle"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
231 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
232 |
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
|
233 |
by Auto_tac; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
234 |
qed "abs_le_zero_iff"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
235 |
Addsimps [abs_le_zero_iff]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
236 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
237 |
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
|
238 |
by (auto_tac (claset() addIs [abs_eqI1],simpset() |
9432 | 239 |
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
|
240 |
qed "abs_real_of_nat_cancel"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
241 |
Addsimps [abs_real_of_nat_cancel]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
242 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
243 |
Goal "~ abs(x) + (#1::real) < x"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
244 |
by (rtac real_leD 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
245 |
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
|
246 |
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
|
247 |
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
|
248 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
249 |
(* used in vector theory *) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
250 |
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
|
251 |
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
|
252 |
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
|
253 |
simpset() addsimps [real_add_assoc])); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
254 |
qed "abs_triangle_ineq_three"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
255 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
256 |
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
|
257 |
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
|
258 |
by (Auto_tac); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
259 |
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
|
260 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
261 |
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
|
262 |
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
|
263 |
by (Auto_tac); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
264 |
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
|
265 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
266 |
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
|
267 |
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
|
268 |
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
|
269 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
270 |
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
|
271 |
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
|
272 |
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
|
273 |
|
10043 | 274 |
Goalw [abs_real_def] |
275 |
" abs(x) <= abs(x + (-y)) + abs((y::real))"; |
|
276 |
by Auto_tac; |
|
277 |
qed "abs_triangle_ineq_minus_cancel"; |
|
278 |
||
279 |
Goal "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)"; |
|
280 |
by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); |
|
281 |
by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1); |
|
282 |
by (rtac (real_add_assoc RS subst) 1); |
|
283 |
by (rtac abs_triangle_ineq 1); |
|
284 |
qed "abs_sum_triangle_ineq"; |