author | paulson |
Wed, 14 Jun 2000 17:47:18 +0200 | |
changeset 9065 | 15f82c9aa331 |
parent 9043 | ca761fe227d8 |
child 9432 | 8b7aad2abcc9 |
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 |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
16 |
(simpset_of Int.thy addsimps |
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 |
arith_tac_split_thms := !arith_tac_split_thms @ [abs_split]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
30 |
|
5078 | 31 |
(*---------------------------------------------------------------------------- |
32 |
Properties of the absolute value function over the reals |
|
33 |
(adapted version of previously proved theorems about abs) |
|
34 |
----------------------------------------------------------------------------*) |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
35 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
36 |
Goalw [abs_real_def] "abs (r::real) = (if #0<=r then r else -r)"; |
5459 | 37 |
by Auto_tac; |
8838 | 38 |
qed "abs_iff"; |
5078 | 39 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
40 |
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
|
41 |
by Auto_tac; |
8838 | 42 |
qed "abs_zero"; |
43 |
Addsimps [abs_zero]; |
|
5078 | 44 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
45 |
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
|
46 |
by (Simp_tac 1); |
8838 | 47 |
qed "abs_minus_zero"; |
5078 | 48 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
49 |
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
|
50 |
by (Asm_simp_tac 1); |
8838 | 51 |
qed "abs_eqI1"; |
5078 | 52 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
53 |
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
|
54 |
by (Asm_simp_tac 1); |
8838 | 55 |
qed "abs_eqI2"; |
5078 | 56 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
57 |
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
|
58 |
by (Asm_simp_tac 1); |
8838 | 59 |
qed "abs_minus_eqI2"; |
5078 | 60 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
61 |
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
|
62 |
by (Asm_simp_tac 1); |
8838 | 63 |
qed "abs_minus_eqI1"; |
5078 | 64 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
65 |
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
|
66 |
by (Simp_tac 1); |
8838 | 67 |
qed "abs_ge_zero"; |
5078 | 68 |
|
8838 | 69 |
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
|
70 |
by (Simp_tac 1); |
8838 | 71 |
qed "abs_idempotent"; |
5078 | 72 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
73 |
Goalw [abs_real_def] "(x=(#0::real)) = (abs x = #0)"; |
5588 | 74 |
by (Full_simp_tac 1); |
8838 | 75 |
qed "abs_zero_iff"; |
5078 | 76 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
77 |
Goal "(x ~= (#0::real)) = (abs x ~= #0)"; |
8838 | 78 |
by (full_simp_tac (simpset() addsimps [abs_zero_iff RS sym]) 1); |
79 |
qed "abs_not_zero_iff"; |
|
5078 | 80 |
|
8838 | 81 |
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
|
82 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
8838 | 83 |
qed "abs_ge_self"; |
5078 | 84 |
|
8838 | 85 |
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
|
86 |
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1); |
8838 | 87 |
qed "abs_ge_minus_self"; |
5078 | 88 |
|
8838 | 89 |
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
|
90 |
by (auto_tac (claset() addSDs [order_antisym], |
9065 | 91 |
simpset() addsimps [real_0_le_mult_iff])); |
8838 | 92 |
qed "abs_mult"; |
5078 | 93 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
94 |
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
|
95 |
by (auto_tac (claset(), |
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
96 |
simpset() addsimps [real_le_less] @ |
9065 | 97 |
(map (rename_numerals thy) [real_minus_rinv, real_rinv_gt_zero]))); |
98 |
by (etac (rename_numerals thy (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
|
99 |
by (arith_tac 1); |
8838 | 100 |
qed "abs_rinv"; |
5078 | 101 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
102 |
Goal "y ~= #0 ==> abs(x*rinv(y)) = abs(x)*rinv(abs(y))"; |
8838 | 103 |
by (asm_simp_tac (simpset() addsimps [abs_mult, abs_rinv]) 1); |
104 |
qed "abs_mult_rinv"; |
|
5078 | 105 |
|
8838 | 106 |
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
|
107 |
by (Simp_tac 1); |
8838 | 108 |
qed "abs_triangle_ineq"; |
5078 | 109 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
110 |
(*Unused, but perhaps interesting as an example*) |
8838 | 111 |
Goal "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)"; |
112 |
by (simp_tac (simpset() addsimps [abs_triangle_ineq RS order_trans]) 1); |
|
113 |
qed "abs_triangle_ineq_four"; |
|
5078 | 114 |
|
8838 | 115 |
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
|
116 |
by (Simp_tac 1); |
8838 | 117 |
qed "abs_minus_cancel"; |
5078 | 118 |
|
8838 | 119 |
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
|
120 |
by (Simp_tac 1); |
8838 | 121 |
qed "abs_minus_add_cancel"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
122 |
|
8838 | 123 |
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
|
124 |
by (Simp_tac 1); |
8838 | 125 |
qed "abs_triangle_minus_ineq"; |
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_spec_mp "abs_add_less"; |
5078 | 130 |
|
8838 | 131 |
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
|
132 |
by (Simp_tac 1); |
8838 | 133 |
qed "abs_add_minus_less"; |
5078 | 134 |
|
135 |
(* lemmas manipulating terms *) |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
136 |
Goal "((#0::real)*x<r)=(#0<r)"; |
5078 | 137 |
by (Simp_tac 1); |
138 |
qed "real_mult_0_less"; |
|
139 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
140 |
Goal "[| (#0::real)<y; x<r; y*r<t*s |] ==> y*x<t*s"; |
9065 | 141 |
by (blast_tac (claset() addSIs [rename_numerals thy real_mult_less_mono2] |
142 |
addIs [real_less_trans]) 1); |
|
5078 | 143 |
qed "real_mult_less_trans"; |
144 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
145 |
Goal "[| (#0::real)<=y; x<r; y*r<t*s; #0<t*s|] ==> y*x<t*s"; |
5078 | 146 |
by (dtac real_le_imp_less_or_eq 1); |
5459 | 147 |
by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2, |
148 |
real_mult_less_trans]) 1); |
|
5078 | 149 |
qed "real_mult_le_less_trans"; |
150 |
||
8838 | 151 |
Goal "[| abs x<r; abs y<s |] ==> abs(x*y)<r*(s::real)"; |
152 |
by (simp_tac (simpset() addsimps [abs_mult]) 1); |
|
5078 | 153 |
by (rtac real_mult_le_less_trans 1); |
8838 | 154 |
by (rtac abs_ge_zero 1); |
5078 | 155 |
by (assume_tac 1); |
9065 | 156 |
by (rtac (rename_numerals thy real_mult_order) 2); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
157 |
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
|
158 |
abs_ge_zero] addIs [real_le_less_trans],simpset())); |
8838 | 159 |
qed "abs_mult_less"; |
5078 | 160 |
|
8838 | 161 |
Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y)<r*(s::real)"; |
162 |
by (auto_tac (claset() addIs [abs_mult_less], |
|
163 |
simpset() addsimps [abs_mult RS sym])); |
|
164 |
qed "abs_mult_less2"; |
|
5078 | 165 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
166 |
Goal "(#1::real) < abs x ==> abs y <= abs(x*y)"; |
8838 | 167 |
by (cut_inst_tac [("x1","y")] (abs_ge_zero RS real_le_imp_less_or_eq) 1); |
5078 | 168 |
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
|
169 |
by (dres_inst_tac [("W","#1")] real_less_sum_gt_zero 1); |
9065 | 170 |
by (forw_inst_tac [("y","abs x + (-#1)")] |
171 |
(rename_numerals thy real_mult_order) 1); |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
172 |
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
|
173 |
by (asm_full_simp_tac (simpset() |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
174 |
addsimps [real_add_mult_distrib2, |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
175 |
real_mult_commute, abs_mult]) 2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
176 |
by (dtac sym 2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
177 |
by (auto_tac (claset(),simpset() addsimps [abs_mult])); |
8838 | 178 |
qed "abs_mult_le"; |
5078 | 179 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
180 |
Goal "[| (#1::real) < abs x; r < abs y|] ==> r < abs(x*y)"; |
8838 | 181 |
by (blast_tac (HOL_cs addIs [abs_mult_le, real_less_le_trans]) 1); |
182 |
qed "abs_mult_gt"; |
|
5078 | 183 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
184 |
Goal "abs(x)<r ==> (#0::real)<r"; |
8838 | 185 |
by (blast_tac (claset() addSIs [real_le_less_trans,abs_ge_zero]) 1); |
186 |
qed "abs_less_gt_zero"; |
|
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); |
8838 | 190 |
qed "abs_one"; |
5078 | 191 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
192 |
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
|
193 |
by (Simp_tac 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
194 |
qed "abs_minus_one"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
195 |
Addsimps [abs_minus_one]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
196 |
|
8838 | 197 |
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
|
198 |
by Auto_tac; |
8838 | 199 |
qed "abs_disj"; |
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_interval_iff"; |
5078 | 204 |
|
8838 | 205 |
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
|
206 |
by Auto_tac; |
8838 | 207 |
qed "abs_le_interval_iff"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
208 |
|
8838 | 209 |
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
|
210 |
by Auto_tac; |
8838 | 211 |
qed "abs_add_minus_interval_iff"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
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) < k ==> #0 < k + 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_pos_gt_zero"; |
216 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
217 |
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
|
218 |
by Auto_tac; |
8838 | 219 |
qed "abs_add_one_gt_zero"; |
220 |
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
|
221 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
222 |
(* 05/2000 *) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
223 |
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
|
224 |
by Auto_tac; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
225 |
qed "abs_not_less_zero"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
226 |
Addsimps [abs_not_less_zero]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
227 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
228 |
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
|
229 |
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
|
230 |
simpset())); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
231 |
qed "abs_circle"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
232 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
233 |
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
|
234 |
by Auto_tac; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
235 |
qed "abs_le_zero_iff"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
236 |
Addsimps [abs_le_zero_iff]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
237 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
238 |
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
|
239 |
by (auto_tac (claset() addIs [abs_eqI1],simpset() |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
240 |
addsimps [rename_numerals thy real_of_nat_ge_zero])); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
241 |
qed "abs_real_of_nat_cancel"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
242 |
Addsimps [abs_real_of_nat_cancel]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
243 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
244 |
Goal "~ abs(x) + (#1::real) < x"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
245 |
by (rtac real_leD 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
246 |
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
|
247 |
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
|
248 |
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
|
249 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
250 |
(* used in vector theory *) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
251 |
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
|
252 |
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
|
253 |
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
|
254 |
simpset() addsimps [real_add_assoc])); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
255 |
qed "abs_triangle_ineq_three"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
256 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
257 |
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
|
258 |
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
|
259 |
by (Auto_tac); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
260 |
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
|
261 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
262 |
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
|
263 |
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
|
264 |
by (Auto_tac); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
265 |
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
|
266 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
267 |
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
|
268 |
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
|
269 |
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
|
270 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
271 |
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
|
272 |
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
|
273 |
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
|
274 |