1 (* Title : HRealAbs.ML |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : Absolute value function for the hyperreals |
|
5 Similar to RealAbs.thy |
|
6 *) |
|
7 |
|
8 (*------------------------------------------------------------ |
|
9 absolute value on hyperreals as pointwise operation on |
|
10 equivalence class representative |
|
11 ------------------------------------------------------------*) |
|
12 |
|
13 Goalw [hrabs_def] |
|
14 "abs (Abs_hypreal (hyprel ^^ {X})) = \ |
|
15 \ Abs_hypreal(hyprel ^^ {%n. abs (X n)})"; |
|
16 by (auto_tac (claset(), |
|
17 simpset() addsimps [hypreal_zero_def, hypreal_le,hypreal_minus])); |
|
18 by (ALLGOALS(Ultra_tac THEN' arith_tac )); |
|
19 qed "hypreal_hrabs"; |
|
20 |
|
21 (*------------------------------------------------------------ |
|
22 Properties of the absolute value function over the reals |
|
23 (adapted version of previously proved theorems about abs) |
|
24 ------------------------------------------------------------*) |
|
25 |
|
26 Goal "abs (0::hypreal) = 0"; |
|
27 by (simp_tac (simpset() addsimps [hrabs_def]) 1); |
|
28 qed "hrabs_zero"; |
|
29 Addsimps [hrabs_zero]; |
|
30 |
|
31 Goal "(0::hypreal)<=x ==> abs x = x"; |
|
32 by (asm_simp_tac (simpset() addsimps [hrabs_def]) 1); |
|
33 qed "hrabs_eqI1"; |
|
34 |
|
35 Goal "(0::hypreal)<x ==> abs x = x"; |
|
36 by (asm_simp_tac (simpset() addsimps [hypreal_less_imp_le, hrabs_eqI1]) 1); |
|
37 qed "hrabs_eqI2"; |
|
38 |
|
39 Goal "x<(0::hypreal) ==> abs x = -x"; |
|
40 by (asm_simp_tac (simpset() addsimps [hypreal_le_def, hrabs_def]) 1); |
|
41 qed "hrabs_minus_eqI2"; |
|
42 |
|
43 Goal "x<=(0::hypreal) ==> abs x = -x"; |
|
44 by (auto_tac (claset() addDs [order_antisym], simpset() addsimps [hrabs_def])); |
|
45 qed "hrabs_minus_eqI1"; |
|
46 |
|
47 Goal "(0::hypreal)<= abs x"; |
|
48 by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2, |
|
49 hypreal_less_asym], |
|
50 simpset() addsimps [hypreal_le_def, hrabs_def])); |
|
51 qed "hrabs_ge_zero"; |
|
52 |
|
53 Goal "abs(abs x) = abs (x::hypreal)"; |
|
54 by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2, |
|
55 hypreal_less_asym], |
|
56 simpset() addsimps [hypreal_le_def, hrabs_def])); |
|
57 qed "hrabs_idempotent"; |
|
58 Addsimps [hrabs_idempotent]; |
|
59 |
|
60 Goalw [hrabs_def] "(abs x = (0::hypreal)) = (x=0)"; |
|
61 by (Simp_tac 1); |
|
62 qed "hrabs_zero_iff"; |
|
63 AddIffs [hrabs_zero_iff]; |
|
64 |
|
65 Goalw [hrabs_def] "(x::hypreal) <= abs x"; |
|
66 by (auto_tac (claset() addDs [not_hypreal_leE RS hypreal_less_imp_le], |
|
67 simpset() addsimps [hypreal_le_zero_iff])); |
|
68 qed "hrabs_ge_self"; |
|
69 |
|
70 Goalw [hrabs_def] "-(x::hypreal) <= abs x"; |
|
71 by (full_simp_tac (simpset() addsimps [hypreal_ge_zero_iff]) 1); |
|
72 qed "hrabs_ge_minus_self"; |
|
73 |
|
74 (* very short proof by "transfer" *) |
|
75 Goal "abs(x*(y::hypreal)) = (abs x)*(abs y)"; |
|
76 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
77 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
78 by (auto_tac (claset(), |
|
79 simpset() addsimps [hypreal_hrabs, hypreal_mult,abs_mult])); |
|
80 qed "hrabs_mult"; |
|
81 |
|
82 Goal "abs(inverse(x)) = inverse(abs(x::hypreal))"; |
|
83 by (hypreal_div_undefined_case_tac "x=0" 1); |
|
84 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
85 by (auto_tac (claset(), |
|
86 simpset() addsimps [hypreal_hrabs, |
|
87 hypreal_inverse,hypreal_zero_def])); |
|
88 by (ultra_tac (claset(), simpset() addsimps [abs_inverse]) 1); |
|
89 qed "hrabs_inverse"; |
|
90 |
|
91 Goal "abs(x+(y::hypreal)) <= abs x + abs y"; |
|
92 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
93 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
94 by (auto_tac (claset(), |
|
95 simpset() addsimps [hypreal_hrabs, hypreal_add,hypreal_le, |
|
96 abs_triangle_ineq])); |
|
97 qed "hrabs_triangle_ineq"; |
|
98 |
|
99 Goal "abs((w::hypreal) + x + y) <= abs(w) + abs(x) + abs(y)"; |
|
100 by (auto_tac (claset() addSIs [hrabs_triangle_ineq RS hypreal_le_trans, |
|
101 hypreal_add_left_le_mono1], |
|
102 simpset() addsimps [hypreal_add_assoc])); |
|
103 qed "hrabs_triangle_ineq_three"; |
|
104 |
|
105 Goalw [hrabs_def] "abs(-x)=abs((x::hypreal))"; |
|
106 by (auto_tac (claset() addSDs [not_hypreal_leE, hypreal_less_asym] |
|
107 addIs [hypreal_le_anti_sym], |
|
108 simpset() addsimps [hypreal_ge_zero_iff])); |
|
109 qed "hrabs_minus_cancel"; |
|
110 Addsimps [hrabs_minus_cancel]; |
|
111 |
|
112 val prem1::prem2::rest = goal thy |
|
113 "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"; |
|
114 by (rtac hypreal_le_less_trans 1); |
|
115 by (rtac hrabs_triangle_ineq 1); |
|
116 by (rtac ([prem1,prem2] MRS hypreal_add_less_mono) 1); |
|
117 qed "hrabs_add_less"; |
|
118 |
|
119 val prem1::prem2::rest = |
|
120 goal thy "[| abs x<r; abs y<s |] ==> abs(x*y)<r*(s::hypreal)"; |
|
121 by (simp_tac (simpset() addsimps [hrabs_mult]) 1); |
|
122 by (rtac hypreal_mult_le_less_trans 1); |
|
123 by (rtac hrabs_ge_zero 1); |
|
124 by (rtac prem2 1); |
|
125 by (rtac hypreal_mult_less_mono1 1); |
|
126 by (rtac (prem2 RS (hrabs_ge_zero RS hypreal_le_less_trans)) 1); |
|
127 by (rtac prem1 1); |
|
128 by (rtac ([prem1 RS (hrabs_ge_zero RS hypreal_le_less_trans), |
|
129 prem2 RS (hrabs_ge_zero RS hypreal_le_less_trans)] |
|
130 MRS hypreal_mult_order) 1); |
|
131 qed "hrabs_mult_less"; |
|
132 |
|
133 Goal "1hr < abs x ==> abs y <= abs(x*y)"; |
|
134 by (cut_inst_tac [("x1","y")] (hrabs_ge_zero RS hypreal_le_imp_less_or_eq) 1); |
|
135 by (EVERY1[etac disjE,rtac hypreal_less_imp_le]); |
|
136 by (dres_inst_tac [("x1","1hr")] (hypreal_less_minus_iff RS iffD1) 1); |
|
137 by (forw_inst_tac [("y","abs x +-1hr")] hypreal_mult_order 1); |
|
138 by (assume_tac 1); |
|
139 by (rtac (hypreal_less_minus_iff RS iffD2) 1); |
|
140 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2, |
|
141 hrabs_mult, hypreal_mult_commute,hypreal_minus_mult_eq2 RS sym]) 1); |
|
142 by (dtac sym 1); |
|
143 by (asm_full_simp_tac (simpset() addsimps [hypreal_le_refl,hrabs_mult]) 1); |
|
144 qed "hrabs_mult_le"; |
|
145 |
|
146 Goal "[| 1hr < abs x; r < abs y|] ==> r < abs(x*y)"; |
|
147 by (fast_tac (HOL_cs addIs [hrabs_mult_le, hypreal_less_le_trans]) 1); |
|
148 qed "hrabs_mult_gt"; |
|
149 |
|
150 Goal "abs x < r ==> (0::hypreal) < r"; |
|
151 by (blast_tac (claset() addSIs [hypreal_le_less_trans, |
|
152 hrabs_ge_zero]) 1); |
|
153 qed "hrabs_less_gt_zero"; |
|
154 |
|
155 Goalw [hrabs_def] "abs 1hr = 1hr"; |
|
156 by (auto_tac (claset() addSDs [not_hypreal_leE RS hypreal_less_asym], |
|
157 simpset() addsimps [hypreal_zero_less_one])); |
|
158 qed "hrabs_one"; |
|
159 |
|
160 Goal "abs x = (x::hypreal) | abs x = -x"; |
|
161 by (cut_inst_tac [("x","0"),("y","x")] hypreal_linear 1); |
|
162 by (fast_tac (claset() addIs [hrabs_eqI2,hrabs_minus_eqI2, |
|
163 hrabs_zero]) 1); |
|
164 qed "hrabs_disj"; |
|
165 |
|
166 Goal "abs x = (y::hypreal) ==> x = y | -x = y"; |
|
167 by (dtac sym 1); |
|
168 by (hyp_subst_tac 1); |
|
169 by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1); |
|
170 by (REPEAT(Asm_simp_tac 1)); |
|
171 qed "hrabs_eq_disj"; |
|
172 |
|
173 Goal "(abs x < (r::hypreal)) = (-r < x & x < r)"; |
|
174 by (Step_tac 1); |
|
175 by (rtac (hypreal_less_swap_iff RS iffD2) 1); |
|
176 by (asm_simp_tac (simpset() addsimps [(hrabs_ge_minus_self |
|
177 RS hypreal_le_less_trans)]) 1); |
|
178 by (asm_simp_tac (simpset() addsimps [(hrabs_ge_self |
|
179 RS hypreal_le_less_trans)]) 1); |
|
180 by (EVERY1 [dtac (hypreal_less_swap_iff RS iffD1), rotate_tac 1, |
|
181 dtac (hypreal_minus_minus RS subst), |
|
182 cut_inst_tac [("x","x")] hrabs_disj, dtac disjE ]); |
|
183 by (assume_tac 3 THEN Auto_tac); |
|
184 qed "hrabs_interval_iff"; |
|
185 |
|
186 Goal "(abs x < (r::hypreal)) = (- x < r & x < r)"; |
|
187 by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff])); |
|
188 by (dtac (hypreal_less_swap_iff RS iffD1) 1); |
|
189 by (dtac (hypreal_less_swap_iff RS iffD1) 2); |
|
190 by (Auto_tac); |
|
191 qed "hrabs_interval_iff2"; |
|
192 |
|
193 (* Needed in Geom.ML *) |
|
194 Goal "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"; |
|
195 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
196 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
197 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
198 by (auto_tac (claset(), |
|
199 simpset() addsimps [hypreal_hrabs, hypreal_minus,hypreal_add])); |
|
200 by (Ultra_tac 1 THEN arith_tac 1); |
|
201 qed "hrabs_add_lemma_disj"; |
|
202 |
|
203 (***SHOULD BE TRIVIAL GIVEN SIMPROCS |
|
204 Goal "abs((x::hypreal) + -y) = abs (y + -x)"; |
|
205 by (rtac (hrabs_minus_cancel RS subst) 1); |
|
206 by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); |
|
207 qed "hrabs_minus_add_cancel"; |
|
208 |
|
209 (* Needed in Geom.ML *) |
|
210 Goal "(x::hypreal) + - y + (z + - y) = abs (x + - z) \ |
|
211 \ ==> y = z | x = y"; |
|
212 by (rtac (hypreal_minus_eq_cancel RS subst) 1); |
|
213 by (res_inst_tac [("b1","y")] (hypreal_minus_eq_cancel RS subst) 1); |
|
214 by (rtac hrabs_add_lemma_disj 1); |
|
215 by (asm_full_simp_tac (simpset() addsimps [hrabs_minus_add_cancel] |
|
216 @ hypreal_add_ac) 1); |
|
217 qed "hrabs_add_lemma_disj2"; |
|
218 ***) |
|
219 |
|
220 (*---------------------------------------------------------- |
|
221 Relating hrabs to abs through embedding of IR into IR* |
|
222 ----------------------------------------------------------*) |
|
223 Goalw [hypreal_of_real_def] |
|
224 "abs (hypreal_of_real r) = hypreal_of_real (abs r)"; |
|
225 by (auto_tac (claset(), simpset() addsimps [hypreal_hrabs])); |
|
226 qed "hypreal_of_real_hrabs"; |
|