1 (* Title : Real.ML |
1 (* Title: HOL/Real/Real.ML |
2 Author : Jacques D. Fleuriot |
2 ID: $Id$ |
3 Copyright : 1998 University of Cambridge |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Description : The reals |
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Type "real" is a linear order |
5 *) |
7 *) |
6 |
8 |
7 (*** Proving that realrel is an equivalence relation ***) |
9 |
8 |
|
9 Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \ |
|
10 \ ==> x1 + y3 = x3 + y1"; |
|
11 by (res_inst_tac [("C","y2")] preal_add_right_cancel 1); |
|
12 by (rotate_tac 1 1 THEN dtac sym 1); |
|
13 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); |
|
14 by (rtac (preal_add_left_commute RS subst) 1); |
|
15 by (res_inst_tac [("x1","x1")] (preal_add_assoc RS subst) 1); |
|
16 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); |
|
17 qed "preal_trans_lemma"; |
|
18 |
|
19 (** Natural deduction for realrel **) |
|
20 |
|
21 Goalw [realrel_def] |
|
22 "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)"; |
|
23 by (Blast_tac 1); |
|
24 qed "realrel_iff"; |
|
25 |
|
26 Goalw [realrel_def] |
|
27 "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel"; |
|
28 by (Blast_tac 1); |
|
29 qed "realrelI"; |
|
30 |
|
31 Goalw [realrel_def] |
|
32 "p: realrel --> (EX x1 y1 x2 y2. \ |
|
33 \ p = ((x1,y1),(x2,y2)) & x1 + y2 = x2 + y1)"; |
|
34 by (Blast_tac 1); |
|
35 qed "realrelE_lemma"; |
|
36 |
|
37 val [major,minor] = goal thy |
|
38 "[| p: realrel; \ |
|
39 \ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1 \ |
|
40 \ |] ==> Q |] ==> Q"; |
|
41 by (cut_facts_tac [major RS (realrelE_lemma RS mp)] 1); |
|
42 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); |
|
43 qed "realrelE"; |
|
44 |
|
45 AddSIs [realrelI]; |
|
46 AddSEs [realrelE]; |
|
47 |
|
48 Goal "(x,x): realrel"; |
|
49 by (stac surjective_pairing 1 THEN rtac (refl RS realrelI) 1); |
|
50 qed "realrel_refl"; |
|
51 |
|
52 Goalw [equiv_def, refl_def, sym_def, trans_def] |
|
53 "equiv {x::(preal*preal).True} realrel"; |
|
54 by (fast_tac (claset() addSIs [realrel_refl] |
|
55 addSEs [sym,preal_trans_lemma]) 1); |
|
56 qed "equiv_realrel"; |
|
57 |
|
58 val equiv_realrel_iff = |
|
59 [TrueI, TrueI] MRS |
|
60 ([CollectI, CollectI] MRS |
|
61 (equiv_realrel RS eq_equiv_class_iff)); |
|
62 |
|
63 Goalw [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real"; |
|
64 by (Blast_tac 1); |
|
65 qed "realrel_in_real"; |
|
66 |
|
67 Goal "inj_on Abs_real real"; |
|
68 by (rtac inj_on_inverseI 1); |
|
69 by (etac Abs_real_inverse 1); |
|
70 qed "inj_on_Abs_real"; |
|
71 |
|
72 Addsimps [equiv_realrel_iff,inj_on_Abs_real RS inj_on_iff, |
|
73 realrel_iff, realrel_in_real, Abs_real_inverse]; |
|
74 |
|
75 Addsimps [equiv_realrel RS eq_equiv_class_iff]; |
|
76 val eq_realrelD = equiv_realrel RSN (2,eq_equiv_class); |
|
77 |
|
78 Goal "inj(Rep_real)"; |
|
79 by (rtac inj_inverseI 1); |
|
80 by (rtac Rep_real_inverse 1); |
|
81 qed "inj_Rep_real"; |
|
82 |
|
83 (** real_preal: the injection from preal to real **) |
|
84 Goal "inj(real_preal)"; |
|
85 by (rtac injI 1); |
|
86 by (rewtac real_preal_def); |
|
87 by (dtac (inj_on_Abs_real RS inj_onD) 1); |
|
88 by (REPEAT (rtac realrel_in_real 1)); |
|
89 by (dtac eq_equiv_class 1); |
|
90 by (rtac equiv_realrel 1); |
|
91 by (Blast_tac 1); |
|
92 by Safe_tac; |
|
93 by (Asm_full_simp_tac 1); |
|
94 qed "inj_real_preal"; |
|
95 |
|
96 val [prem] = goal thy |
|
97 "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P"; |
|
98 by (res_inst_tac [("x1","z")] |
|
99 (rewrite_rule [real_def] Rep_real RS quotientE) 1); |
|
100 by (dres_inst_tac [("f","Abs_real")] arg_cong 1); |
|
101 by (res_inst_tac [("p","x")] PairE 1); |
|
102 by (rtac prem 1); |
|
103 by (asm_full_simp_tac (simpset() addsimps [Rep_real_inverse]) 1); |
|
104 qed "eq_Abs_real"; |
|
105 |
|
106 (**** real_minus: additive inverse on real ****) |
|
107 |
|
108 Goalw [congruent_def] |
|
109 "congruent realrel (%p. split (%x y. realrel^^{(y,x)}) p)"; |
|
110 by Safe_tac; |
|
111 by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1); |
|
112 qed "real_minus_congruent"; |
|
113 |
|
114 (*Resolve th against the corresponding facts for real_minus*) |
|
115 val real_minus_ize = RSLIST [equiv_realrel, real_minus_congruent]; |
|
116 |
|
117 Goalw [real_minus_def] |
|
118 "%~ (Abs_real(realrel^^{(x,y)})) = Abs_real(realrel ^^ {(y,x)})"; |
|
119 by (res_inst_tac [("f","Abs_real")] arg_cong 1); |
|
120 by (simp_tac (simpset() addsimps |
|
121 [realrel_in_real RS Abs_real_inverse,real_minus_ize UN_equiv_class]) 1); |
|
122 qed "real_minus"; |
|
123 |
|
124 Goal "%~ (%~ z) = z"; |
|
125 by (res_inst_tac [("z","z")] eq_Abs_real 1); |
|
126 by (asm_simp_tac (simpset() addsimps [real_minus]) 1); |
|
127 qed "real_minus_minus"; |
|
128 |
|
129 Addsimps [real_minus_minus]; |
|
130 |
|
131 Goal "inj(real_minus)"; |
|
132 by (rtac injI 1); |
|
133 by (dres_inst_tac [("f","real_minus")] arg_cong 1); |
|
134 by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1); |
|
135 qed "inj_real_minus"; |
|
136 |
|
137 Goalw [real_zero_def] "%~0r = 0r"; |
|
138 by (simp_tac (simpset() addsimps [real_minus]) 1); |
|
139 qed "real_minus_zero"; |
|
140 |
|
141 Addsimps [real_minus_zero]; |
|
142 |
|
143 Goal "(%~x = 0r) = (x = 0r)"; |
|
144 by (res_inst_tac [("z","x")] eq_Abs_real 1); |
|
145 by (auto_tac (claset(),simpset() addsimps [real_zero_def, |
|
146 real_minus] @ preal_add_ac)); |
|
147 qed "real_minus_zero_iff"; |
|
148 |
|
149 Addsimps [real_minus_zero_iff]; |
|
150 |
|
151 Goal "(%~x ~= 0r) = (x ~= 0r)"; |
|
152 by Auto_tac; |
|
153 qed "real_minus_not_zero_iff"; |
|
154 |
|
155 (*** Congruence property for addition ***) |
|
156 Goalw [congruent2_def] |
|
157 "congruent2 realrel (%p1 p2. \ |
|
158 \ split (%x1 y1. split (%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)"; |
|
159 by Safe_tac; |
|
160 by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1); |
|
161 by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1); |
|
162 by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); |
|
163 by (asm_simp_tac (simpset() addsimps preal_add_ac) 1); |
|
164 qed "real_add_congruent2"; |
|
165 |
|
166 (*Resolve th against the corresponding facts for real_add*) |
|
167 val real_add_ize = RSLIST [equiv_realrel, real_add_congruent2]; |
|
168 |
|
169 Goalw [real_add_def] |
|
170 "Abs_real(realrel^^{(x1,y1)}) + Abs_real(realrel^^{(x2,y2)}) = \ |
|
171 \ Abs_real(realrel^^{(x1+x2, y1+y2)})"; |
|
172 by (asm_simp_tac |
|
173 (simpset() addsimps [real_add_ize UN_equiv_class2]) 1); |
|
174 qed "real_add"; |
|
175 |
|
176 Goal "(z::real) + w = w + z"; |
|
177 by (res_inst_tac [("z","z")] eq_Abs_real 1); |
|
178 by (res_inst_tac [("z","w")] eq_Abs_real 1); |
|
179 by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1); |
|
180 qed "real_add_commute"; |
|
181 |
|
182 Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)"; |
|
183 by (res_inst_tac [("z","z1")] eq_Abs_real 1); |
|
184 by (res_inst_tac [("z","z2")] eq_Abs_real 1); |
|
185 by (res_inst_tac [("z","z3")] eq_Abs_real 1); |
|
186 by (asm_simp_tac (simpset() addsimps [real_add, preal_add_assoc]) 1); |
|
187 qed "real_add_assoc"; |
|
188 |
|
189 (*For AC rewriting*) |
|
190 Goal "(x::real)+(y+z)=y+(x+z)"; |
|
191 by (rtac (real_add_commute RS trans) 1); |
|
192 by (rtac (real_add_assoc RS trans) 1); |
|
193 by (rtac (real_add_commute RS arg_cong) 1); |
|
194 qed "real_add_left_commute"; |
|
195 |
|
196 (* real addition is an AC operator *) |
|
197 val real_add_ac = [real_add_assoc,real_add_commute,real_add_left_commute]; |
|
198 |
|
199 Goalw [real_preal_def,real_zero_def] "0r + z = z"; |
|
200 by (res_inst_tac [("z","z")] eq_Abs_real 1); |
|
201 by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1); |
|
202 qed "real_add_zero_left"; |
|
203 |
|
204 Goal "z + 0r = z"; |
|
205 by (simp_tac (simpset() addsimps [real_add_zero_left,real_add_commute]) 1); |
|
206 qed "real_add_zero_right"; |
|
207 |
|
208 Goalw [real_zero_def] "z + %~z = 0r"; |
|
209 by (res_inst_tac [("z","z")] eq_Abs_real 1); |
|
210 by (asm_full_simp_tac (simpset() addsimps [real_minus, |
|
211 real_add, preal_add_commute]) 1); |
|
212 qed "real_add_minus"; |
|
213 |
|
214 Goal "%~z + z = 0r"; |
|
215 by (simp_tac (simpset() addsimps |
|
216 [real_add_commute,real_add_minus]) 1); |
|
217 qed "real_add_minus_left"; |
|
218 |
|
219 Goal "? y. (x::real) + y = 0r"; |
|
220 by (blast_tac (claset() addIs [real_add_minus]) 1); |
|
221 qed "real_minus_ex"; |
|
222 |
|
223 Goal "?! y. (x::real) + y = 0r"; |
|
224 by (auto_tac (claset() addIs [real_add_minus],simpset())); |
|
225 by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1); |
|
226 by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1); |
|
227 by (asm_full_simp_tac (simpset() addsimps [real_add_commute, |
|
228 real_add_zero_right,real_add_zero_left]) 1); |
|
229 qed "real_minus_ex1"; |
|
230 |
|
231 Goal "?! y. y + (x::real) = 0r"; |
|
232 by (auto_tac (claset() addIs [real_add_minus_left],simpset())); |
|
233 by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1); |
|
234 by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1); |
|
235 by (asm_full_simp_tac (simpset() addsimps [real_add_commute, |
|
236 real_add_zero_right,real_add_zero_left]) 1); |
|
237 qed "real_minus_left_ex1"; |
|
238 |
|
239 Goal "x + y = 0r ==> x = %~y"; |
|
240 by (cut_inst_tac [("z","y")] real_add_minus_left 1); |
|
241 by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1); |
|
242 by (Blast_tac 1); |
|
243 qed "real_add_minus_eq_minus"; |
|
244 |
|
245 Goal "? y. x = %~y"; |
|
246 by (cut_inst_tac [("x","x")] real_minus_ex 1); |
|
247 by (etac exE 1 THEN dtac real_add_minus_eq_minus 1); |
|
248 by (Blast_tac 1); |
|
249 qed "real_as_add_inverse_ex"; |
|
250 |
|
251 (* real_minus_add_distrib *) |
|
252 Goal "%~(x + y) = %~x + %~y"; |
|
253 by (res_inst_tac [("z","x")] eq_Abs_real 1); |
|
254 by (res_inst_tac [("z","y")] eq_Abs_real 1); |
|
255 by (auto_tac (claset(),simpset() addsimps [real_minus,real_add])); |
|
256 qed "real_minus_add_eq"; |
|
257 |
|
258 val real_minus_add_distrib = real_minus_add_eq; |
|
259 |
|
260 Goal "((x::real) + y = x + z) = (y = z)"; |
|
261 by (Step_tac 1); |
|
262 by (dres_inst_tac [("f","%t.%~x + t")] arg_cong 1); |
|
263 by (asm_full_simp_tac (simpset() addsimps [real_add_minus_left, |
|
264 real_add_assoc RS sym,real_add_zero_left]) 1); |
|
265 qed "real_add_left_cancel"; |
|
266 |
|
267 Goal "(y + (x::real)= z + x) = (y = z)"; |
|
268 by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1); |
|
269 qed "real_add_right_cancel"; |
|
270 |
|
271 (*** Congruence property for multiplication ***) |
|
272 Goal "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> \ |
|
273 \ x * x1 + y * y1 + (x * y2 + x2 * y) = \ |
|
274 \ x * x2 + y * y2 + (x * y1 + x1 * y)"; |
|
275 by (asm_full_simp_tac (simpset() addsimps [preal_add_left_commute, |
|
276 preal_add_assoc RS sym,preal_add_mult_distrib2 RS sym]) 1); |
|
277 by (rtac (preal_mult_commute RS subst) 1); |
|
278 by (res_inst_tac [("y1","x2")] (preal_mult_commute RS subst) 1); |
|
279 by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc, |
|
280 preal_add_mult_distrib2 RS sym]) 1); |
|
281 by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1); |
|
282 qed "real_mult_congruent2_lemma"; |
|
283 |
|
284 Goal |
|
285 "congruent2 realrel (%p1 p2. \ |
|
286 \ split (%x1 y1. split (%x2 y2. realrel^^{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"; |
|
287 by (rtac (equiv_realrel RS congruent2_commuteI) 1); |
|
288 by Safe_tac; |
|
289 by (rewtac split_def); |
|
290 by (asm_simp_tac (simpset() addsimps [preal_mult_commute,preal_add_commute]) 1); |
|
291 by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma])); |
|
292 qed "real_mult_congruent2"; |
|
293 |
|
294 (*Resolve th against the corresponding facts for real_mult*) |
|
295 val real_mult_ize = RSLIST [equiv_realrel, real_mult_congruent2]; |
|
296 |
|
297 Goalw [real_mult_def] |
|
298 "Abs_real((realrel^^{(x1,y1)})) * Abs_real((realrel^^{(x2,y2)})) = \ |
|
299 \ Abs_real(realrel ^^ {(x1*x2+y1*y2,x1*y2+x2*y1)})"; |
|
300 by (simp_tac (simpset() addsimps [real_mult_ize UN_equiv_class2]) 1); |
|
301 qed "real_mult"; |
|
302 |
|
303 Goal "(z::real) * w = w * z"; |
|
304 by (res_inst_tac [("z","z")] eq_Abs_real 1); |
|
305 by (res_inst_tac [("z","w")] eq_Abs_real 1); |
|
306 by (asm_simp_tac |
|
307 (simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1); |
|
308 qed "real_mult_commute"; |
|
309 |
|
310 Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)"; |
|
311 by (res_inst_tac [("z","z1")] eq_Abs_real 1); |
|
312 by (res_inst_tac [("z","z2")] eq_Abs_real 1); |
|
313 by (res_inst_tac [("z","z3")] eq_Abs_real 1); |
|
314 by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @ |
|
315 preal_add_ac @ preal_mult_ac) 1); |
|
316 qed "real_mult_assoc"; |
|
317 |
|
318 qed_goal "real_mult_left_commute" thy |
|
319 "(z1::real) * (z2 * z3) = z2 * (z1 * z3)" |
|
320 (fn _ => [rtac (real_mult_commute RS trans) 1, rtac (real_mult_assoc RS trans) 1, |
|
321 rtac (real_mult_commute RS arg_cong) 1]); |
|
322 |
|
323 (* real multiplication is an AC operator *) |
|
324 val real_mult_ac = [real_mult_assoc, real_mult_commute, real_mult_left_commute]; |
|
325 |
|
326 Goalw [real_one_def,pnat_one_def] "1r * z = z"; |
|
327 by (res_inst_tac [("z","z")] eq_Abs_real 1); |
|
328 by (asm_full_simp_tac (simpset() addsimps [real_mult, |
|
329 preal_add_mult_distrib2,preal_mult_1_right] |
|
330 @ preal_mult_ac @ preal_add_ac) 1); |
|
331 qed "real_mult_1"; |
|
332 |
|
333 Goal "z * 1r = z"; |
|
334 by (simp_tac (simpset() addsimps [real_mult_commute, |
|
335 real_mult_1]) 1); |
|
336 qed "real_mult_1_right"; |
|
337 |
|
338 Goalw [real_zero_def,pnat_one_def] "0r * z = 0r"; |
|
339 by (res_inst_tac [("z","z")] eq_Abs_real 1); |
|
340 by (asm_full_simp_tac (simpset() addsimps [real_mult, |
|
341 preal_add_mult_distrib2,preal_mult_1_right] |
|
342 @ preal_mult_ac @ preal_add_ac) 1); |
|
343 qed "real_mult_0"; |
|
344 |
|
345 Goal "z * 0r = 0r"; |
|
346 by (simp_tac (simpset() addsimps [real_mult_commute, |
|
347 real_mult_0]) 1); |
|
348 qed "real_mult_0_right"; |
|
349 |
|
350 Addsimps [real_mult_0_right,real_mult_0]; |
|
351 |
|
352 Goal "%~(x * y) = %~x * y"; |
|
353 by (res_inst_tac [("z","x")] eq_Abs_real 1); |
|
354 by (res_inst_tac [("z","y")] eq_Abs_real 1); |
|
355 by (auto_tac (claset(),simpset() addsimps [real_minus,real_mult] |
|
356 @ preal_mult_ac @ preal_add_ac)); |
|
357 qed "real_minus_mult_eq1"; |
|
358 |
|
359 Goal "%~(x * y) = x * %~y"; |
|
360 by (res_inst_tac [("z","x")] eq_Abs_real 1); |
|
361 by (res_inst_tac [("z","y")] eq_Abs_real 1); |
|
362 by (auto_tac (claset(),simpset() addsimps [real_minus,real_mult] |
|
363 @ preal_mult_ac @ preal_add_ac)); |
|
364 qed "real_minus_mult_eq2"; |
|
365 |
|
366 Goal "%~x*%~y = x*y"; |
|
367 by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym, |
|
368 real_minus_mult_eq1 RS sym]) 1); |
|
369 qed "real_minus_mult_cancel"; |
|
370 |
|
371 Addsimps [real_minus_mult_cancel]; |
|
372 |
|
373 Goal "%~x*y = x*%~y"; |
|
374 by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym, |
|
375 real_minus_mult_eq1 RS sym]) 1); |
|
376 qed "real_minus_mult_commute"; |
|
377 |
|
378 (*----------------------------------------------------------------------------- |
|
379 |
|
380 -----------------------------------------------------------------------------*) |
|
381 |
|
382 (** Lemmas **) |
|
383 |
|
384 qed_goal "real_add_assoc_cong" thy |
|
385 "!!z. (z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" |
|
386 (fn _ => [(asm_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1)]); |
|
387 |
|
388 qed_goal "real_add_assoc_swap" thy "(z::real) + (v + w) = v + (z + w)" |
|
389 (fn _ => [(REPEAT (ares_tac [real_add_commute RS real_add_assoc_cong] 1))]); |
|
390 |
|
391 Goal "((z1::real) + z2) * w = (z1 * w) + (z2 * w)"; |
|
392 by (res_inst_tac [("z","z1")] eq_Abs_real 1); |
|
393 by (res_inst_tac [("z","z2")] eq_Abs_real 1); |
|
394 by (res_inst_tac [("z","w")] eq_Abs_real 1); |
|
395 by (asm_simp_tac |
|
396 (simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @ |
|
397 preal_add_ac @ preal_mult_ac) 1); |
|
398 qed "real_add_mult_distrib"; |
|
399 |
|
400 val real_mult_commute'= read_instantiate [("z","w")] real_mult_commute; |
|
401 |
|
402 Goal "(w::real) * (z1 + z2) = (w * z1) + (w * z2)"; |
|
403 by (simp_tac (simpset() addsimps [real_mult_commute',real_add_mult_distrib]) 1); |
|
404 qed "real_add_mult_distrib2"; |
|
405 |
|
406 val real_mult_simps = [real_mult_1, real_mult_1_right]; |
|
407 Addsimps real_mult_simps; |
|
408 |
|
409 (*** one and zero are distinct ***) |
|
410 Goalw [real_zero_def,real_one_def] "0r ~= 1r"; |
|
411 by (auto_tac (claset(),simpset() addsimps |
|
412 [preal_self_less_add_left RS preal_not_refl2])); |
|
413 qed "real_zero_not_eq_one"; |
|
414 |
|
415 (*** existence of inverse ***) |
|
416 (** lemma -- alternative definition for 0r **) |
|
417 Goalw [real_zero_def] "0r = Abs_real (realrel ^^ {(x, x)})"; |
|
418 by (auto_tac (claset(),simpset() addsimps [preal_add_commute])); |
|
419 qed "real_zero_iff"; |
|
420 |
|
421 Goalw [real_zero_def,real_one_def] |
|
422 "!!(x::real). x ~= 0r ==> ? y. x*y = 1r"; |
|
423 by (res_inst_tac [("z","x")] eq_Abs_real 1); |
|
424 by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1); |
|
425 by (auto_tac (claset() addSDs [preal_less_add_left_Ex], |
|
426 simpset() addsimps [real_zero_iff RS sym])); |
|
427 by (res_inst_tac [("x","Abs_real (realrel ^^ {(@#$#1p,pinv(D)+@#$#1p)})")] exI 1); |
|
428 by (res_inst_tac [("x","Abs_real (realrel ^^ {(pinv(D)+@#$#1p,@#$#1p)})")] exI 2); |
|
429 by (auto_tac (claset(),simpset() addsimps [real_mult, |
|
430 pnat_one_def,preal_mult_1_right,preal_add_mult_distrib2, |
|
431 preal_add_mult_distrib,preal_mult_1,preal_mult_inv_right] |
|
432 @ preal_add_ac @ preal_mult_ac)); |
|
433 qed "real_mult_inv_right_ex"; |
|
434 |
|
435 Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r"; |
|
436 by (asm_simp_tac (simpset() addsimps [real_mult_commute, |
|
437 real_mult_inv_right_ex]) 1); |
|
438 qed "real_mult_inv_left_ex"; |
|
439 |
|
440 Goalw [rinv_def] "!!(x::real). x ~= 0r ==> rinv(x)*x = 1r"; |
|
441 by (forward_tac [real_mult_inv_left_ex] 1); |
|
442 by (Step_tac 1); |
|
443 by (rtac selectI2 1); |
|
444 by Auto_tac; |
|
445 qed "real_mult_inv_left"; |
|
446 |
|
447 Goal "!!(x::real). x ~= 0r ==> x*rinv(x) = 1r"; |
|
448 by (auto_tac (claset() addIs [real_mult_commute RS subst], |
|
449 simpset() addsimps [real_mult_inv_left])); |
|
450 qed "real_mult_inv_right"; |
|
451 |
|
452 Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)"; |
|
453 by Auto_tac; |
|
454 by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1); |
|
455 by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1); |
|
456 qed "real_mult_left_cancel"; |
|
457 |
|
458 Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)"; |
|
459 by (Step_tac 1); |
|
460 by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1); |
|
461 by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1); |
|
462 qed "real_mult_right_cancel"; |
|
463 |
|
464 Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r"; |
|
465 by (forward_tac [real_mult_inv_left_ex] 1); |
|
466 by (etac exE 1); |
|
467 by (rtac selectI2 1); |
|
468 by (auto_tac (claset(),simpset() addsimps [real_mult_0, |
|
469 real_zero_not_eq_one])); |
|
470 qed "rinv_not_zero"; |
|
471 |
|
472 Addsimps [real_mult_inv_left,real_mult_inv_right]; |
|
473 |
|
474 Goal "x ~= 0r ==> rinv(rinv x) = x"; |
|
475 by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1); |
|
476 by (etac rinv_not_zero 1); |
|
477 by (auto_tac (claset() addDs [rinv_not_zero],simpset())); |
|
478 qed "real_rinv_rinv"; |
|
479 |
|
480 Goalw [rinv_def] "rinv(1r) = 1r"; |
|
481 by (cut_facts_tac [real_zero_not_eq_one RS |
|
482 not_sym RS real_mult_inv_left_ex] 1); |
|
483 by (etac exE 1); |
|
484 by (rtac selectI2 1); |
|
485 by (auto_tac (claset(),simpset() addsimps |
|
486 [real_zero_not_eq_one RS not_sym])); |
|
487 qed "real_rinv_1"; |
|
488 |
|
489 Goal "x ~= 0r ==> rinv(%~x) = %~rinv(x)"; |
|
490 by (res_inst_tac [("c1","%~x")] (real_mult_right_cancel RS iffD1) 1); |
|
491 by Auto_tac; |
|
492 qed "real_minus_rinv"; |
|
493 |
|
494 (*** theorems for ordering ***) |
|
495 (* prove introduction and elimination rules for real_less *) |
|
496 |
|
497 Goalw [real_less_def] |
|
498 "P < (Q::real) = (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \ |
|
499 \ (x1,y1::preal):Rep_real(P) & \ |
|
500 \ (x2,y2):Rep_real(Q))"; |
|
501 by (Blast_tac 1); |
|
502 qed "real_less_iff"; |
|
503 |
|
504 Goalw [real_less_def] |
|
505 "[| x1 + y2 < x2 + y1; (x1,y1::preal):Rep_real(P); \ |
|
506 \ (x2,y2):Rep_real(Q) |] ==> P < (Q::real)"; |
|
507 by (Blast_tac 1); |
|
508 qed "real_lessI"; |
|
509 |
|
510 Goalw [real_less_def] |
|
511 "!!P. [| R1 < (R2::real); \ |
|
512 \ !!x1 x2 y1 y2. x1 + y2 < x2 + y1 ==> P; \ |
|
513 \ !!x1 y1. (x1,y1::preal):Rep_real(R1) ==> P; \ |
|
514 \ !!x2 y2. (x2,y2::preal):Rep_real(R2) ==> P |] \ |
|
515 \ ==> P"; |
|
516 by Auto_tac; |
|
517 qed "real_lessE"; |
|
518 |
|
519 Goalw [real_less_def] |
|
520 "R1 < (R2::real) ==> (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \ |
|
521 \ (x1,y1::preal):Rep_real(R1) & \ |
|
522 \ (x2,y2):Rep_real(R2))"; |
|
523 by (Blast_tac 1); |
|
524 qed "real_lessD"; |
|
525 |
|
526 (* real_less is a strong order i.e nonreflexive and transitive *) |
|
527 (*** lemmas ***) |
|
528 Goal "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y"; |
|
529 by (asm_simp_tac (simpset() addsimps [preal_add_commute]) 1); |
|
530 qed "preal_lemma_eq_rev_sum"; |
|
531 |
|
532 Goal "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1"; |
|
533 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); |
|
534 qed "preal_add_left_commute_cancel"; |
|
535 |
|
536 Goal |
|
537 "!!(x::preal). [| x + y2a = x2a + y; \ |
|
538 \ x + y2b = x2b + y |] \ |
|
539 \ ==> x2a + y2b = x2b + y2a"; |
|
540 by (dtac preal_lemma_eq_rev_sum 1); |
|
541 by (assume_tac 1); |
|
542 by (thin_tac "x + y2b = x2b + y" 1); |
|
543 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); |
|
544 by (dtac preal_add_left_commute_cancel 1); |
|
545 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); |
|
546 qed "preal_lemma_for_not_refl"; |
|
547 |
|
548 Goal "~ (R::real) < R"; |
|
549 by (res_inst_tac [("z","R")] eq_Abs_real 1); |
|
550 by (auto_tac (claset(),simpset() addsimps [real_less_def])); |
|
551 by (dtac preal_lemma_for_not_refl 1); |
|
552 by (assume_tac 1 THEN rotate_tac 2 1); |
|
553 by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl])); |
|
554 qed "real_less_not_refl"; |
|
555 |
|
556 (*** y < y ==> P ***) |
|
557 bind_thm("real_less_irrefl",real_less_not_refl RS notE); |
|
558 |
|
559 Goal "!!(x::real). x < y ==> x ~= y"; |
|
560 by (auto_tac (claset(),simpset() addsimps [real_less_not_refl])); |
|
561 qed "real_not_refl2"; |
|
562 |
|
563 (* lemma re-arranging and eliminating terms *) |
|
564 Goal "!! (a::preal). [| a + b = c + d; \ |
|
565 \ x2b + d + (c + y2e) < a + y2b + (x2e + b) |] \ |
|
566 \ ==> x2b + y2e < x2e + y2b"; |
|
567 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); |
|
568 by (res_inst_tac [("C","c+d")] preal_add_left_less_cancel 1); |
|
569 by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); |
|
570 qed "preal_lemma_trans"; |
|
571 |
|
572 (** heavy re-writing involved*) |
|
573 Goal "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3"; |
|
574 by (res_inst_tac [("z","R1")] eq_Abs_real 1); |
|
575 by (res_inst_tac [("z","R2")] eq_Abs_real 1); |
|
576 by (res_inst_tac [("z","R3")] eq_Abs_real 1); |
|
577 by (auto_tac (claset(),simpset() addsimps [real_less_def])); |
|
578 by (REPEAT(rtac exI 1)); |
|
579 by (EVERY[rtac conjI 1, rtac conjI 2]); |
|
580 by (REPEAT(Blast_tac 2)); |
|
581 by (dtac preal_lemma_for_not_refl 1 THEN assume_tac 1); |
|
582 by (blast_tac (claset() addDs [preal_add_less_mono] |
|
583 addIs [preal_lemma_trans]) 1); |
|
584 qed "real_less_trans"; |
|
585 |
|
586 Goal "!! (R1::real). [| R1 < R2; R2 < R1 |] ==> P"; |
|
587 by (dtac real_less_trans 1 THEN assume_tac 1); |
|
588 by (asm_full_simp_tac (simpset() addsimps [real_less_not_refl]) 1); |
|
589 qed "real_less_asym"; |
|
590 |
|
591 (****)(****)(****)(****)(****)(****)(****)(****)(****)(****) |
|
592 (****** Map and more real_less ******) |
|
593 (*** mapping from preal into real ***) |
|
594 Goalw [real_preal_def] |
|
595 "%#((z1::preal) + z2) = %#z1 + %#z2"; |
|
596 by (asm_simp_tac (simpset() addsimps [real_add, |
|
597 preal_add_mult_distrib,preal_mult_1] addsimps preal_add_ac) 1); |
|
598 qed "real_preal_add"; |
|
599 |
|
600 Goalw [real_preal_def] |
|
601 "%#((z1::preal) * z2) = %#z1* %#z2"; |
|
602 by (full_simp_tac (simpset() addsimps [real_mult, |
|
603 preal_add_mult_distrib2,preal_mult_1, |
|
604 preal_mult_1_right,pnat_one_def] |
|
605 @ preal_add_ac @ preal_mult_ac) 1); |
|
606 qed "real_preal_mult"; |
|
607 |
|
608 Goalw [real_preal_def] |
|
609 "!!(x::preal). y < x ==> ? m. Abs_real (realrel ^^ {(x,y)}) = %#m"; |
|
610 by (auto_tac (claset() addSDs [preal_less_add_left_Ex], |
|
611 simpset() addsimps preal_add_ac)); |
|
612 qed "real_preal_ExI"; |
|
613 |
|
614 Goalw [real_preal_def] |
|
615 "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = %#m ==> y < x"; |
|
616 by (auto_tac (claset(),simpset() addsimps |
|
617 [preal_add_commute,preal_add_assoc])); |
|
618 by (asm_full_simp_tac (simpset() addsimps |
|
619 [preal_add_assoc RS sym,preal_self_less_add_left]) 1); |
|
620 qed "real_preal_ExD"; |
|
621 |
|
622 Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = %#m) = (y < x)"; |
|
623 by (blast_tac (claset() addSIs [real_preal_ExI,real_preal_ExD]) 1); |
|
624 qed "real_preal_iff"; |
|
625 |
|
626 (*** Gleason prop 9-4.4 p 127 ***) |
|
627 Goalw [real_preal_def,real_zero_def] |
|
628 "? m. (x::real) = %#m | x = 0r | x = %~(%#m)"; |
|
629 by (res_inst_tac [("z","x")] eq_Abs_real 1); |
|
630 by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac)); |
|
631 by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1); |
|
632 by (auto_tac (claset() addSDs [preal_less_add_left_Ex], |
|
633 simpset() addsimps [preal_add_assoc RS sym])); |
|
634 by (auto_tac (claset(),simpset() addsimps [preal_add_commute])); |
|
635 qed "real_preal_trichotomy"; |
|
636 |
|
637 Goal "!!P. [| !!m. x = %#m ==> P; \ |
|
638 \ x = 0r ==> P; \ |
|
639 \ !!m. x = %~(%#m) ==> P |] ==> P"; |
|
640 by (cut_inst_tac [("x","x")] real_preal_trichotomy 1); |
|
641 by Auto_tac; |
|
642 qed "real_preal_trichotomyE"; |
|
643 |
|
644 Goalw [real_preal_def] "%#m1 < %#m2 ==> m1 < m2"; |
|
645 by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac)); |
|
646 by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym])); |
|
647 by (auto_tac (claset(),simpset() addsimps preal_add_ac)); |
|
648 qed "real_preal_lessD"; |
|
649 |
|
650 Goal "m1 < m2 ==> %#m1 < %#m2"; |
|
651 by (dtac preal_less_add_left_Ex 1); |
|
652 by (auto_tac (claset(),simpset() addsimps [real_preal_add, |
|
653 real_preal_def,real_less_def])); |
|
654 by (REPEAT(rtac exI 1)); |
|
655 by (EVERY[rtac conjI 1, rtac conjI 2]); |
|
656 by (REPEAT(Blast_tac 2)); |
|
657 by (simp_tac (simpset() addsimps [preal_self_less_add_left] |
|
658 delsimps [preal_add_less_iff2]) 1); |
|
659 qed "real_preal_lessI"; |
|
660 |
|
661 Goal "(%#m1 < %#m2) = (m1 < m2)"; |
|
662 by (blast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1); |
|
663 qed "real_preal_less_iff1"; |
|
664 |
|
665 Addsimps [real_preal_less_iff1]; |
|
666 |
|
667 Goal "%~ %#m < %#m"; |
|
668 by (auto_tac (claset(),simpset() addsimps |
|
669 [real_preal_def,real_less_def,real_minus])); |
|
670 by (REPEAT(rtac exI 1)); |
|
671 by (EVERY[rtac conjI 1, rtac conjI 2]); |
|
672 by (REPEAT(Blast_tac 2)); |
|
673 by (full_simp_tac (simpset() addsimps preal_add_ac) 1); |
|
674 by (full_simp_tac (simpset() addsimps [preal_self_less_add_right, |
|
675 preal_add_assoc RS sym]) 1); |
|
676 qed "real_preal_minus_less_self"; |
|
677 |
|
678 Goalw [real_zero_def] "%~ %#m < 0r"; |
|
679 by (auto_tac (claset(),simpset() addsimps |
|
680 [real_preal_def,real_less_def,real_minus])); |
|
681 by (REPEAT(rtac exI 1)); |
|
682 by (EVERY[rtac conjI 1, rtac conjI 2]); |
|
683 by (REPEAT(Blast_tac 2)); |
|
684 by (full_simp_tac (simpset() addsimps |
|
685 [preal_self_less_add_right] @ preal_add_ac) 1); |
|
686 qed "real_preal_minus_less_zero"; |
|
687 |
|
688 Goal "~ 0r < %~ %#m"; |
|
689 by (cut_facts_tac [real_preal_minus_less_zero] 1); |
|
690 by (fast_tac (claset() addDs [real_less_trans] |
|
691 addEs [real_less_irrefl]) 1); |
|
692 qed "real_preal_not_minus_gt_zero"; |
|
693 |
|
694 Goalw [real_zero_def] " 0r < %#m"; |
|
695 by (auto_tac (claset(),simpset() addsimps |
|
696 [real_preal_def,real_less_def,real_minus])); |
|
697 by (REPEAT(rtac exI 1)); |
|
698 by (EVERY[rtac conjI 1, rtac conjI 2]); |
|
699 by (REPEAT(Blast_tac 2)); |
|
700 by (full_simp_tac (simpset() addsimps |
|
701 [preal_self_less_add_right] @ preal_add_ac) 1); |
|
702 qed "real_preal_zero_less"; |
|
703 |
|
704 Goal "~ %#m < 0r"; |
|
705 by (cut_facts_tac [real_preal_zero_less] 1); |
|
706 by (blast_tac (claset() addDs [real_less_trans] |
|
707 addEs [real_less_irrefl]) 1); |
|
708 qed "real_preal_not_less_zero"; |
|
709 |
|
710 Goal "0r < %~ %~ %#m"; |
|
711 by (simp_tac (simpset() addsimps |
|
712 [real_preal_zero_less]) 1); |
|
713 qed "real_minus_minus_zero_less"; |
|
714 |
|
715 (* another lemma *) |
|
716 Goalw [real_zero_def] " 0r < %#m + %#m1"; |
|
717 by (auto_tac (claset(),simpset() addsimps |
|
718 [real_preal_def,real_less_def,real_add])); |
|
719 by (REPEAT(rtac exI 1)); |
|
720 by (EVERY[rtac conjI 1, rtac conjI 2]); |
|
721 by (REPEAT(Blast_tac 2)); |
|
722 by (full_simp_tac (simpset() addsimps preal_add_ac) 1); |
|
723 by (full_simp_tac (simpset() addsimps [preal_self_less_add_right, |
|
724 preal_add_assoc RS sym]) 1); |
|
725 qed "real_preal_sum_zero_less"; |
|
726 |
|
727 Goal "%~ %#m < %#m1"; |
|
728 by (auto_tac (claset(),simpset() addsimps |
|
729 [real_preal_def,real_less_def,real_minus])); |
|
730 by (REPEAT(rtac exI 1)); |
|
731 by (EVERY[rtac conjI 1, rtac conjI 2]); |
|
732 by (REPEAT(Blast_tac 2)); |
|
733 by (full_simp_tac (simpset() addsimps preal_add_ac) 1); |
|
734 by (full_simp_tac (simpset() addsimps [preal_self_less_add_right, |
|
735 preal_add_assoc RS sym]) 1); |
|
736 qed "real_preal_minus_less_all"; |
|
737 |
|
738 Goal "~ %#m < %~ %#m1"; |
|
739 by (cut_facts_tac [real_preal_minus_less_all] 1); |
|
740 by (blast_tac (claset() addDs [real_less_trans] |
|
741 addEs [real_less_irrefl]) 1); |
|
742 qed "real_preal_not_minus_gt_all"; |
|
743 |
|
744 Goal "%~ %#m1 < %~ %#m2 ==> %#m2 < %#m1"; |
|
745 by (auto_tac (claset(),simpset() addsimps |
|
746 [real_preal_def,real_less_def,real_minus])); |
|
747 by (REPEAT(rtac exI 1)); |
|
748 by (EVERY[rtac conjI 1, rtac conjI 2]); |
|
749 by (REPEAT(Blast_tac 2)); |
|
750 by (auto_tac (claset(),simpset() addsimps preal_add_ac)); |
|
751 by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); |
|
752 by (auto_tac (claset(),simpset() addsimps preal_add_ac)); |
|
753 qed "real_preal_minus_less_rev1"; |
|
754 |
|
755 Goal "%#m1 < %#m2 ==> %~ %#m2 < %~ %#m1"; |
|
756 by (auto_tac (claset(),simpset() addsimps |
|
757 [real_preal_def,real_less_def,real_minus])); |
|
758 by (REPEAT(rtac exI 1)); |
|
759 by (EVERY[rtac conjI 1, rtac conjI 2]); |
|
760 by (REPEAT(Blast_tac 2)); |
|
761 by (auto_tac (claset(),simpset() addsimps preal_add_ac)); |
|
762 by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); |
|
763 by (auto_tac (claset(),simpset() addsimps preal_add_ac)); |
|
764 qed "real_preal_minus_less_rev2"; |
|
765 |
|
766 Goal "(%~ %#m1 < %~ %#m2) = (%#m2 < %#m1)"; |
|
767 by (blast_tac (claset() addSIs [real_preal_minus_less_rev1, |
|
768 real_preal_minus_less_rev2]) 1); |
|
769 qed "real_preal_minus_less_rev_iff"; |
|
770 |
|
771 Addsimps [real_preal_minus_less_rev_iff]; |
|
772 |
|
773 (*** linearity ***) |
|
774 Goal "(R1::real) < R2 | R1 = R2 | R2 < R1"; |
|
775 by (res_inst_tac [("x","R1")] real_preal_trichotomyE 1); |
|
776 by (ALLGOALS(res_inst_tac [("x","R2")] real_preal_trichotomyE)); |
|
777 by (auto_tac (claset() addSDs [preal_le_anti_sym], |
|
778 simpset() addsimps [preal_less_le_iff,real_preal_minus_less_zero, |
|
779 real_preal_zero_less,real_preal_minus_less_all])); |
|
780 qed "real_linear"; |
|
781 |
|
782 Goal "!!(R1::real). [| R1 < R2 ==> P; R1 = R2 ==> P; \ |
|
783 \ R2 < R1 ==> P |] ==> P"; |
|
784 by (cut_inst_tac [("R1.0","R1"),("R2.0","R2")] real_linear 1); |
|
785 by Auto_tac; |
|
786 qed "real_linear_less2"; |
|
787 |
|
788 (*** Properties of <= ***) |
|
789 |
|
790 Goalw [real_le_def] "~(w < z) ==> z <= (w::real)"; |
|
791 by (assume_tac 1); |
|
792 qed "real_leI"; |
|
793 |
|
794 Goalw [real_le_def] "z<=w ==> ~(w<(z::real))"; |
|
795 by (assume_tac 1); |
|
796 qed "real_leD"; |
|
797 |
|
798 val real_leE = make_elim real_leD; |
|
799 |
|
800 Goal "(~(w < z)) = (z <= (w::real))"; |
|
801 by (blast_tac (claset() addSIs [real_leI,real_leD]) 1); |
|
802 qed "real_less_le_iff"; |
|
803 |
|
804 Goalw [real_le_def] "~ z <= w ==> w<(z::real)"; |
|
805 by (Blast_tac 1); |
|
806 qed "not_real_leE"; |
|
807 |
|
808 Goalw [real_le_def] "z < w ==> z <= (w::real)"; |
|
809 by (blast_tac (claset() addEs [real_less_asym]) 1); |
|
810 qed "real_less_imp_le"; |
|
811 |
|
812 Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y"; |
|
813 by (cut_facts_tac [real_linear] 1); |
|
814 by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1); |
|
815 qed "real_le_imp_less_or_eq"; |
|
816 |
|
817 Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)"; |
|
818 by (cut_facts_tac [real_linear] 1); |
|
819 by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1); |
|
820 qed "real_less_or_eq_imp_le"; |
|
821 |
|
822 Goal "(x <= (y::real)) = (x < y | x=y)"; |
|
823 by (REPEAT(ares_tac [iffI, real_less_or_eq_imp_le, real_le_imp_less_or_eq] 1)); |
|
824 qed "real_le_eq_less_or_eq"; |
|
825 |
|
826 Goal "w <= (w::real)"; |
|
827 by (simp_tac (simpset() addsimps [real_le_eq_less_or_eq]) 1); |
|
828 qed "real_le_refl"; |
|
829 |
|
830 val prems = goal Real.thy "!!i. [| i <= j; j < k |] ==> i < (k::real)"; |
|
831 by (dtac real_le_imp_less_or_eq 1); |
|
832 by (blast_tac (claset() addIs [real_less_trans]) 1); |
|
833 qed "real_le_less_trans"; |
|
834 |
|
835 Goal "!! (i::real). [| i < j; j <= k |] ==> i < k"; |
|
836 by (dtac real_le_imp_less_or_eq 1); |
|
837 by (blast_tac (claset() addIs [real_less_trans]) 1); |
|
838 qed "real_less_le_trans"; |
|
839 |
|
840 Goal "[| i <= j; j <= k |] ==> i <= (k::real)"; |
|
841 by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq, |
|
842 rtac real_less_or_eq_imp_le, blast_tac (claset() addIs [real_less_trans])]); |
|
843 qed "real_le_trans"; |
|
844 |
|
845 Goal "[| z <= w; w <= z |] ==> z = (w::real)"; |
|
846 by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq, |
|
847 fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]); |
|
848 qed "real_le_anti_sym"; |
|
849 |
|
850 Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)"; |
|
851 by (rtac not_real_leE 1); |
|
852 by (blast_tac (claset() addDs [real_le_imp_less_or_eq]) 1); |
|
853 qed "not_less_not_eq_real_less"; |
|
854 |
|
855 Goal "(0r < %~R) = (R < 0r)"; |
|
856 by (res_inst_tac [("x","R")] real_preal_trichotomyE 1); |
|
857 by (auto_tac (claset(),simpset() addsimps [real_preal_not_minus_gt_zero, |
|
858 real_preal_not_less_zero,real_preal_zero_less, |
|
859 real_preal_minus_less_zero])); |
|
860 qed "real_minus_zero_less_iff"; |
|
861 |
|
862 Addsimps [real_minus_zero_less_iff]; |
|
863 |
|
864 Goal "(%~R < 0r) = (0r < R)"; |
|
865 by (res_inst_tac [("x","R")] real_preal_trichotomyE 1); |
|
866 by (auto_tac (claset(),simpset() addsimps [real_preal_not_minus_gt_zero, |
|
867 real_preal_not_less_zero,real_preal_zero_less, |
|
868 real_preal_minus_less_zero])); |
|
869 qed "real_minus_zero_less_iff2"; |
|
870 |
10 |
871 (** lemma **) |
11 (** lemma **) |
872 Goal "(0r < x) = (? y. x = %#y)"; |
12 Goal "(0r < x) = (? y. x = %#y)"; |
873 by (auto_tac (claset(),simpset() addsimps [real_preal_zero_less])); |
13 by (auto_tac (claset(),simpset() addsimps [real_preal_zero_less])); |
874 by (cut_inst_tac [("x","x")] real_preal_trichotomy 1); |
14 by (cut_inst_tac [("x","x")] real_preal_trichotomy 1); |
894 |
34 |
895 Goal "~ 0r < y ==> !x. y < %#x"; |
35 Goal "~ 0r < y ==> !x. y < %#x"; |
896 by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1); |
36 by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1); |
897 qed "real_less_all_real2"; |
37 qed "real_less_all_real2"; |
898 |
38 |
899 (**** Derive alternative definition for real_less ****) |
39 Goal "((x::real) < y) = (-y < -x)"; |
900 (** lemma **) |
|
901 Goal "!!(R::real). ? A. S + A = R"; |
|
902 by (res_inst_tac [("x","%~S + R")] exI 1); |
|
903 by (simp_tac (simpset() addsimps [real_add_minus, |
|
904 real_add_zero_right] @ real_add_ac) 1); |
|
905 qed "real_lemma_add_left_ex"; |
|
906 |
|
907 Goal "!!(R::real). R < S ==> ? T. R + T = S"; |
|
908 by (res_inst_tac [("x","R")] real_preal_trichotomyE 1); |
|
909 by (ALLGOALS(res_inst_tac [("x","S")] real_preal_trichotomyE)); |
|
910 by (auto_tac (claset() addSDs [preal_le_anti_sym] addSDs [preal_less_add_left_Ex], |
|
911 simpset() addsimps [preal_less_le_iff,real_preal_add,real_minus_add_eq, |
|
912 real_preal_minus_less_zero,real_less_not_refl,real_minus_ex,real_add_assoc, |
|
913 real_preal_zero_less,real_preal_minus_less_all,real_add_minus_left, |
|
914 real_preal_not_less_zero,real_add_zero_left,real_lemma_add_left_ex])); |
|
915 qed "real_less_add_left_Ex"; |
|
916 |
|
917 Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S"; |
|
918 by (res_inst_tac [("x","R")] real_preal_trichotomyE 1); |
|
919 by (ALLGOALS(res_inst_tac [("x","S")] real_preal_trichotomyE)); |
|
920 by (auto_tac (claset() addSDs [preal_less_add_left_Ex], |
|
921 simpset() addsimps [real_preal_not_minus_gt_all, |
|
922 real_preal_add, real_preal_not_less_zero,real_less_not_refl, |
|
923 real_preal_not_minus_gt_zero,real_add_zero_left,real_minus_add_eq])); |
|
924 by (res_inst_tac [("x","%#D")] exI 1); |
|
925 by (res_inst_tac [("x","%#m+%#ma")] exI 2); |
|
926 by (res_inst_tac [("x","%#m")] exI 3); |
|
927 by (res_inst_tac [("x","%#D")] exI 4); |
|
928 by (auto_tac (claset(),simpset() addsimps [real_preal_zero_less, |
|
929 real_preal_sum_zero_less,real_add_minus_left,real_add_assoc, |
|
930 real_add_minus,real_add_zero_right])); |
|
931 by (simp_tac (simpset() addsimps [real_add_assoc RS sym, |
|
932 real_add_minus_left,real_add_zero_left]) 1); |
|
933 qed "real_less_add_positive_left_Ex"; |
|
934 |
|
935 (* lemmas *) |
|
936 (** change naff name(s)! **) |
|
937 Goal "(W < S) ==> (0r < S + %~W)"; |
|
938 by (dtac real_less_add_positive_left_Ex 1); |
|
939 by (auto_tac (claset(),simpset() addsimps [real_add_minus, |
|
940 real_add_zero_right] @ real_add_ac)); |
|
941 qed "real_less_sum_gt_zero"; |
|
942 |
|
943 Goal "!!S. T = S + W ==> S = T + %~W"; |
|
944 by (asm_simp_tac (simpset() addsimps [real_add_minus, real_add_zero_right] |
|
945 @ real_add_ac) 1); |
|
946 qed "real_lemma_change_eq_subj"; |
|
947 |
|
948 (* FIXME: long! *) |
|
949 Goal "(0r < S + %~W) ==> (W < S)"; |
|
950 by (rtac ccontr 1); |
|
951 by (dtac (real_leI RS real_le_imp_less_or_eq) 1); |
|
952 by (auto_tac (claset(), |
|
953 simpset() addsimps [real_less_not_refl,real_add_minus])); |
|
954 by (EVERY1[dtac real_less_add_positive_left_Ex, etac exE, etac conjE]); |
|
955 by (asm_full_simp_tac (simpset() addsimps [real_add_zero_left]) 1); |
|
956 by (dtac real_lemma_change_eq_subj 1); |
|
957 by (auto_tac (claset(),simpset() addsimps [real_minus_minus])); |
|
958 by (dtac real_less_sum_gt_zero 1); |
|
959 by (asm_full_simp_tac (simpset() addsimps [real_minus_add_eq] @ real_add_ac) 1); |
|
960 by (EVERY1[rotate_tac 1, dtac (real_add_left_commute RS ssubst)]); |
|
961 by (auto_tac (claset() addEs [real_less_asym], |
|
962 simpset() addsimps [real_add_minus,real_add_zero_right])); |
|
963 qed "real_sum_gt_zero_less"; |
|
964 |
|
965 Goal "(0r < S + %~W) = (W < S)"; |
|
966 by (blast_tac (claset() addIs [real_less_sum_gt_zero, |
|
967 real_sum_gt_zero_less]) 1); |
|
968 qed "real_less_sum_gt_0_iff"; |
|
969 |
|
970 Goal "((x::real) < y) = (%~y < %~x)"; |
|
971 by (rtac (real_less_sum_gt_0_iff RS subst) 1); |
40 by (rtac (real_less_sum_gt_0_iff RS subst) 1); |
972 by (res_inst_tac [("W1","x")] (real_less_sum_gt_0_iff RS subst) 1); |
41 by (res_inst_tac [("W1","x")] (real_less_sum_gt_0_iff RS subst) 1); |
973 by (simp_tac (simpset() addsimps [real_add_commute]) 1); |
42 by (simp_tac (simpset() addsimps [real_add_commute]) 1); |
974 qed "real_less_swap_iff"; |
43 qed "real_less_swap_iff"; |
975 |
44 |
976 Goal "[| R + L = S; 0r < L |] ==> R < S"; |
45 Goal "[| R + L = S; 0r < L |] ==> R < S"; |
977 by (rtac (real_less_sum_gt_0_iff RS iffD1) 1); |
46 by (rtac (real_less_sum_gt_0_iff RS iffD1) 1); |
978 by (auto_tac (claset(),simpset() addsimps [ |
47 by (auto_tac (claset(), simpset() addsimps real_add_ac)); |
979 real_add_minus,real_add_zero_right] @ real_add_ac)); |
|
980 qed "real_lemma_add_positive_imp_less"; |
48 qed "real_lemma_add_positive_imp_less"; |
981 |
49 |
982 Goal "!!(R::real). ? T. 0r < T & R + T = S ==> R < S"; |
50 Goal "!!(R::real). ? T. 0r < T & R + T = S ==> R < S"; |
983 by (blast_tac (claset() addIs [real_lemma_add_positive_imp_less]) 1); |
51 by (blast_tac (claset() addIs [real_lemma_add_positive_imp_less]) 1); |
984 qed "real_ex_add_positive_left_less"; |
52 qed "real_ex_add_positive_left_less"; |
985 |
53 |
986 (*** alternative definition for real_less ***) |
54 (*Alternative definition for real_less. NOT for rewriting*) |
987 Goal "!!(R::real). (? T. 0r < T & R + T = S) = (R < S)"; |
55 Goal "!!(R::real). (R < S) = (? T. 0r < T & R + T = S)"; |
988 by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex, |
56 by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex, |
989 real_ex_add_positive_left_less]) 1); |
57 real_ex_add_positive_left_less]) 1); |
990 qed "real_less_iffdef"; |
58 qed "real_less_iff_add"; |
991 |
59 |
992 Goal "(0r < x) = (%~x < x)"; |
60 Goal "(0r < x) = (-x < x)"; |
993 by Safe_tac; |
61 by Safe_tac; |
994 by (rtac ccontr 2 THEN forward_tac |
62 by (rtac ccontr 2 THEN forward_tac |
995 [real_leI RS real_le_imp_less_or_eq] 2); |
63 [real_leI RS real_le_imp_less_or_eq] 2); |
996 by (Step_tac 2); |
64 by (Step_tac 2); |
997 by (dtac (real_minus_zero_less_iff RS iffD2) 2); |
65 by (dtac (real_minus_zero_less_iff RS iffD2) 2); |
998 by (blast_tac (claset() addIs [real_less_trans]) 2); |
66 by (blast_tac (claset() addIs [real_less_trans]) 2); |
999 by (auto_tac (claset(),simpset() addsimps |
67 by (auto_tac (claset(), |
1000 [real_gt_zero_preal_Ex,real_preal_minus_less_self])); |
68 simpset() addsimps |
|
69 [real_gt_zero_preal_Ex,real_preal_minus_less_self])); |
1001 qed "real_gt_zero_iff"; |
70 qed "real_gt_zero_iff"; |
1002 |
71 |
1003 Goal "(x < 0r) = (x < %~x)"; |
72 Goal "(x < 0r) = (x < -x)"; |
1004 by (rtac (real_minus_zero_less_iff RS subst) 1); |
73 by (rtac (real_minus_zero_less_iff RS subst) 1); |
1005 by (stac real_gt_zero_iff 1); |
74 by (stac real_gt_zero_iff 1); |
1006 by (Full_simp_tac 1); |
75 by (Full_simp_tac 1); |
1007 qed "real_lt_zero_iff"; |
76 qed "real_lt_zero_iff"; |
1008 |
77 |
1009 Goalw [real_le_def] "(0r <= x) = (%~x <= x)"; |
78 Goalw [real_le_def] "(0r <= x) = (-x <= x)"; |
1010 by (auto_tac (claset(),simpset() addsimps [real_lt_zero_iff RS sym])); |
79 by (auto_tac (claset(),simpset() addsimps [real_lt_zero_iff RS sym])); |
1011 qed "real_ge_zero_iff"; |
80 qed "real_ge_zero_iff"; |
1012 |
81 |
1013 Goalw [real_le_def] "(x <= 0r) = (x <= %~x)"; |
82 Goalw [real_le_def] "(x <= 0r) = (x <= -x)"; |
1014 by (auto_tac (claset(),simpset() addsimps [real_gt_zero_iff RS sym])); |
83 by (auto_tac (claset(),simpset() addsimps [real_gt_zero_iff RS sym])); |
1015 qed "real_le_zero_iff"; |
84 qed "real_le_zero_iff"; |
1016 |
85 |
1017 Goal "(%#m1 <= %#m2) = (m1 <= m2)"; |
86 Goal "(%#m1 <= %#m2) = (m1 <= m2)"; |
1018 by (auto_tac (claset() addSIs [preal_leI], |
87 by (auto_tac (claset() addSIs [preal_leI], |