author | paulson |
Thu, 15 Nov 2001 16:12:49 +0100 | |
changeset 12196 | a3be6b3a9c0b |
parent 12018 | ec054019c910 |
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 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
11 |
Goalw [real_abs_def] |
9013
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@ |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
18 |
[minus_real_number_of, le_real_number_of_eq_not_less, |
9013
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 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
24 |
Goalw [real_abs_def] |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
25 |
"P(abs (x::real)) = ((0 <= x --> P x) & (x < 0 --> P(-x)))"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
26 |
by Auto_tac; |
9013
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 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
35 |
Goalw [real_abs_def] "abs (r::real) = (if 0<=r then r else -r)"; |
5459 | 36 |
by Auto_tac; |
8838 | 37 |
qed "abs_iff"; |
5078 | 38 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
39 |
Goalw [real_abs_def] "abs 0 = (0::real)"; |
9013
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 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
44 |
Goalw [real_abs_def] "abs (1::real) = 1"; |
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); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
46 |
qed "abs_one"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
47 |
Addsimps [abs_one]; |
5078 | 48 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
49 |
Goalw [real_abs_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 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
53 |
Goalw [real_abs_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 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
57 |
Goalw [real_abs_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 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
61 |
Goalw [real_abs_def] "x<=(0::real) ==> abs x = -x"; |
9013
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 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
65 |
Goalw [real_abs_def] "(0::real)<= abs x"; |
9013
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"; |
12196 | 68 |
Addsimps [abs_ge_zero]; |
5078 | 69 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
70 |
Goalw [real_abs_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
|
71 |
by (Simp_tac 1); |
8838 | 72 |
qed "abs_idempotent"; |
10690 | 73 |
Addsimps [abs_idempotent]; |
5078 | 74 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
75 |
Goalw [real_abs_def] "(abs x = 0) = (x=(0::real))"; |
5588 | 76 |
by (Full_simp_tac 1); |
8838 | 77 |
qed "abs_zero_iff"; |
10699 | 78 |
AddIffs [abs_zero_iff]; |
5078 | 79 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
80 |
Goalw [real_abs_def] "x<=abs (x::real)"; |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
81 |
by (Simp_tac 1); |
8838 | 82 |
qed "abs_ge_self"; |
5078 | 83 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
84 |
Goalw [real_abs_def] "-x<=abs (x::real)"; |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
85 |
by (Simp_tac 1); |
8838 | 86 |
qed "abs_ge_minus_self"; |
5078 | 87 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
88 |
Goalw [real_abs_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 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
93 |
Goalw [real_abs_def] "abs(inverse(x::real)) = inverse(abs(x))"; |
10648 | 94 |
by (real_div_undefined_case_tac "x=0" 1); |
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
95 |
by (auto_tac (claset(), |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
96 |
simpset() addsimps [real_minus_inverse, real_le_less, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
97 |
INVERSE_ZERO, real_inverse_gt_0])); |
10606 | 98 |
qed "abs_inverse"; |
5078 | 99 |
|
10648 | 100 |
Goal "abs (x * inverse y) = (abs x) * inverse (abs (y::real))"; |
10606 | 101 |
by (asm_simp_tac (simpset() addsimps [abs_mult, abs_inverse]) 1); |
102 |
qed "abs_mult_inverse"; |
|
5078 | 103 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
104 |
Goalw [real_abs_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
|
105 |
by (Simp_tac 1); |
8838 | 106 |
qed "abs_triangle_ineq"; |
5078 | 107 |
|
7588
26384af93359
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents:
7219
diff
changeset
|
108 |
(*Unused, but perhaps interesting as an example*) |
8838 | 109 |
Goal "abs(w + x + y + z) <= abs(w) + abs(x) + abs(y) + abs(z::real)"; |
110 |
by (simp_tac (simpset() addsimps [abs_triangle_ineq RS order_trans]) 1); |
|
111 |
qed "abs_triangle_ineq_four"; |
|
5078 | 112 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
113 |
Goalw [real_abs_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
|
114 |
by (Simp_tac 1); |
8838 | 115 |
qed "abs_minus_cancel"; |
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
116 |
Addsimps [abs_minus_cancel]; |
5078 | 117 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
118 |
Goalw [real_abs_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 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
122 |
Goalw [real_abs_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 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
126 |
Goalw [real_abs_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 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
130 |
Goalw [real_abs_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 *) |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
135 |
Goal "((0::real)*x < r)=(0 < r)"; |
5078 | 136 |
by (Simp_tac 1); |
137 |
qed "real_mult_0_less"; |
|
138 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
139 |
Goal "[| (0::real) < y; x < r; y*r < t*s |] ==> y*x < t*s"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
140 |
by (blast_tac (claset() addSIs [real_mult_less_mono2] |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
141 |
addIs [order_less_trans]) 1); |
5078 | 142 |
qed "real_mult_less_trans"; |
143 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
144 |
Goal "[| (0::real)<=y; x < r; y*r < t*s; 0 < t*s|] ==> y*x < t*s"; |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
145 |
by (dtac order_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 |
||
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
150 |
Goal "[| abs x < r; abs y < s |] ==> abs(x*y) < r*(s::real)"; |
8838 | 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); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
155 |
by (rtac real_mult_order 2); |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
156 |
by (auto_tac (claset() addSIs [real_mult_less_mono1, abs_ge_zero] |
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
157 |
addIs [order_le_less_trans], |
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
158 |
simpset())); |
8838 | 159 |
qed "abs_mult_less"; |
5078 | 160 |
|
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
161 |
Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y) < r*(s::real)"; |
8838 | 162 |
by (auto_tac (claset() addIs [abs_mult_less], |
163 |
simpset() addsimps [abs_mult RS sym])); |
|
164 |
qed "abs_mult_less2"; |
|
5078 | 165 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
166 |
Goal "abs(x) < r ==> (0::real) < r"; |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
167 |
by (blast_tac (claset() addSIs [order_le_less_trans,abs_ge_zero]) 1); |
8838 | 168 |
qed "abs_less_gt_zero"; |
5078 | 169 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
170 |
Goalw [real_abs_def] "abs (-1) = (1::real)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
171 |
by (Simp_tac 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
172 |
qed "abs_minus_one"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
173 |
Addsimps [abs_minus_one]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
174 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
175 |
Goalw [real_abs_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
|
176 |
by Auto_tac; |
8838 | 177 |
qed "abs_disj"; |
5078 | 178 |
|
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
179 |
Goalw [real_abs_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
|
180 |
by Auto_tac; |
8838 | 181 |
qed "abs_interval_iff"; |
5078 | 182 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
183 |
Goalw [real_abs_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
|
184 |
by Auto_tac; |
8838 | 185 |
qed "abs_le_interval_iff"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
186 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
187 |
Goalw [real_abs_def] "(0::real) < k ==> 0 < k + abs(x)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
188 |
by Auto_tac; |
8838 | 189 |
qed "abs_add_pos_gt_zero"; |
190 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
191 |
Goalw [real_abs_def] "(0::real) < 1 + abs(x)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
192 |
by Auto_tac; |
8838 | 193 |
qed "abs_add_one_gt_zero"; |
194 |
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
|
195 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
196 |
Goalw [real_abs_def] "~ abs x < (0::real)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
197 |
by Auto_tac; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
198 |
qed "abs_not_less_zero"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
199 |
Addsimps [abs_not_less_zero]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
200 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
201 |
Goal "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)"; |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
202 |
by (auto_tac (claset() addIs [abs_triangle_ineq RS order_le_less_trans], |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
203 |
simpset())); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
204 |
qed "abs_circle"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
205 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
206 |
Goalw [real_abs_def] "(abs x <= (0::real)) = (x = 0)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
207 |
by Auto_tac; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
208 |
qed "abs_le_zero_iff"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
209 |
Addsimps [abs_le_zero_iff]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
210 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
211 |
Goal "((0::real) < abs x) = (x ~= 0)"; |
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
212 |
by (simp_tac (simpset() addsimps [real_abs_def]) 1); |
10648 | 213 |
by (arith_tac 1); |
214 |
qed "real_0_less_abs_iff"; |
|
215 |
Addsimps [real_0_less_abs_iff]; |
|
216 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10752
diff
changeset
|
217 |
Goal "abs (real x) = real (x::nat)"; |
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
218 |
by (auto_tac (claset() addIs [abs_eqI1], |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
219 |
simpset() addsimps [real_of_nat_ge_zero])); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
220 |
qed "abs_real_of_nat_cancel"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
221 |
Addsimps [abs_real_of_nat_cancel]; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
222 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
223 |
Goal "~ abs(x) + (1::real) < x"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
224 |
by (rtac real_leD 1); |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
225 |
by (auto_tac (claset() addIs [abs_ge_self RS order_trans], simpset())); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
226 |
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
|
227 |
Addsimps [abs_add_one_not_less_self]; |
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
228 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
229 |
(* used in vector theory *) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
230 |
Goal "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)"; |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10715
diff
changeset
|
231 |
by (auto_tac (claset() addSIs [abs_triangle_ineq RS order_trans, |
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
232 |
real_add_left_le_mono1], |
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
233 |
simpset() addsimps [real_add_assoc])); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
234 |
qed "abs_triangle_ineq_three"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
235 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
236 |
Goalw [real_abs_def] "abs(x - y) < y ==> (0::real) < y"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
237 |
by (case_tac "0 <= x - y" 1); |
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
238 |
by Auto_tac; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
239 |
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
|
240 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
241 |
Goalw [real_abs_def] "abs(x - y) < x ==> (0::real) < x"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
242 |
by (case_tac "0 <= x - y" 1); |
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
243 |
by Auto_tac; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
244 |
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
|
245 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
246 |
Goal "abs(x - y) < y ==> (0::real) < x"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
247 |
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
|
248 |
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
|
249 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
250 |
Goal "abs(x - y) < -y ==> x < (0::real)"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset
|
251 |
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
|
252 |
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
|
253 |
|
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
254 |
Goalw [real_abs_def] |
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10699
diff
changeset
|
255 |
"abs(x) <= abs(x + (-y)) + abs((y::real))"; |
10043 | 256 |
by Auto_tac; |
257 |
qed "abs_triangle_ineq_minus_cancel"; |
|
258 |
||
259 |
Goal "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)"; |
|
260 |
by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); |
|
261 |
by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1); |
|
262 |
by (rtac (real_add_assoc RS subst) 1); |
|
263 |
by (rtac abs_triangle_ineq 1); |
|
264 |
qed "abs_sum_triangle_ineq"; |