|
1 (*WN060306 from isabelle-users: |
|
2 put expressions involving plus and minus into a canonical form. Here is a possible set of |
|
3 rules: |
|
4 |
|
5 add_assoc add_commute |
|
6 diff_def minus_add_distrib |
|
7 minus_minus minus_zero |
|
8 ===========================================================================*) |
|
9 |
|
10 (* |
|
11 cd ~/Isabelle2002/src/HOL/Real |
|
12 grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml |
|
13 WN 9.8.02 |
|
14 |
|
15 ML> thy; |
|
16 val it = |
|
17 {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, Sum_Type, |
|
18 Relation, Record, Inductive, Transitive_Closure, Wellfounded_Recursion, |
|
19 NatDef, Nat, NatArith, Divides, Power, SetInterval, Finite_Set, Equiv, |
|
20 IntDef, Int, Datatype_Universe, Datatype, Numeral, Bin, IntArith, |
|
21 Wellfounded_Relations, Recdef, IntDiv, IntPower, NatBin, NatSimprocs, |
|
22 Relation_Power, PreList, List, Map, Hilbert_Choice, Main, Lubs, PNat, PRat, |
|
23 PReal, RealDef, RealOrd, RealInt, RealBin, RealArith0, RealArith, |
|
24 RComplete, RealAbs, RealPow, Ring_and_Field, Complex_Numbers, Real} |
|
25 : theory |
|
26 |
|
27 theories with their respective theorems found by |
|
28 grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml; |
|
29 theories listed in the the order as found in Real.thy above |
|
30 |
|
31 comments |
|
32 (**)"...theorem..." : first choice for one of the rule-sets |
|
33 "...theorem..."(*??*): to be investigated |
|
34 "...theorem... : just for documenting the contents |
|
35 *) |
|
36 |
|
37 Lubs.ML:qed ----------------------------------------------------------------- |
|
38 "setleI"; "ALL y::?'a:?S::?'a set. y <= (?x::?'a) ==> ?S *<= ?x" |
|
39 "setleD"; "[| (?S::?'a set) *<= (?x::?'a); (?y::?'a) : ?S |] ==> ?y <= ?x" |
|
40 "setgeI"; "Ball (?S::?'a set) (op <= (?x::?'a)) ==> ?x <=* ?S" |
|
41 "setgeD"; "[| (?x::?'a) <=* (?S::?'a set); (?y::?'a) : ?S |] ==> ?x <= ?y" |
|
42 "leastPD1"; |
|
43 "leastPD2"; |
|
44 "leastPD3"; |
|
45 "isLubD1"; |
|
46 "isLubD1a"; |
|
47 "isLub_isUb"; |
|
48 "isLubD2"; |
|
49 "isLubD3"; |
|
50 "isLubI1"; |
|
51 "isLubI2"; |
|
52 "isUbD"; |
|
53 "[| isUb (?R::?'a set) (?S::?'a set) (?x::?'a); (?y::?'a) : ?S |] |
|
54 ==> ?y <= ?x" "isUbD2"; |
|
55 "isUbD2a"; |
|
56 "isUbI"; |
|
57 "isLub_le_isUb"; |
|
58 "isLub_ubs"; |
|
59 PNat.ML:qed ------------------------------------------------------------------ |
|
60 "pnat_fun_mono"; "mono (%X::nat set. {Suc (0::nat)} Un Suc ` X)" |
|
61 "one_RepI"; "Suc (0::nat) : pnat" |
|
62 "pnat_Suc_RepI"; |
|
63 "two_RepI"; |
|
64 "PNat_induct"; |
|
65 "[| (?i::nat) : pnat; (?P::nat => bool) (Suc (0::nat)); |
|
66 !!j::nat. [| j : pnat; ?P j |] ==> ?P (Suc j) |] ==> ?P ?i" |
|
67 "pnat_induct"; |
|
68 "[| (?P::pnat => bool) (1::pnat); !!n::pnat. ?P n ==> ?P (pSuc n) |] |
|
69 ==> ?P (?n::pnat)" |
|
70 "pnat_diff_induct"; |
|
71 "pnatE"; |
|
72 "inj_on_Abs_pnat"; |
|
73 "inj_Rep_pnat"; |
|
74 "zero_not_mem_pnat"; |
|
75 "mem_pnat_gt_zero"; |
|
76 "gt_0_mem_pnat"; |
|
77 "mem_pnat_gt_0_iff"; |
|
78 "Rep_pnat_gt_zero"; |
|
79 "pnat_add_commute"; "(?x::pnat) + (?y::pnat) = ?y + ?x" |
|
80 "Collect_pnat_gt_0"; |
|
81 "pSuc_not_one"; |
|
82 "inj_pSuc"; |
|
83 "pSuc_pSuc_eq"; |
|
84 "n_not_pSuc_n"; |
|
85 "not1_implies_pSuc"; |
|
86 "pSuc_is_plus_one"; |
|
87 "sum_Rep_pnat"; |
|
88 "sum_Rep_pnat_sum"; |
|
89 "pnat_add_assoc"; |
|
90 "pnat_add_left_commute"; |
|
91 "pnat_add_left_cancel"; |
|
92 "pnat_add_right_cancel"; |
|
93 "pnat_no_add_ident"; |
|
94 "pnat_less_not_refl"; |
|
95 "pnat_less_not_refl2"; |
|
96 "Rep_pnat_not_less0"; |
|
97 "Rep_pnat_not_less_one"; |
|
98 "Rep_pnat_gt_implies_not0"; |
|
99 "pnat_less_linear"; |
|
100 "Rep_pnat_le_one"; |
|
101 "lemma_less_ex_sum_Rep_pnat"; |
|
102 "pnat_le_iff_Rep_pnat_le"; |
|
103 "pnat_add_left_cancel_le"; |
|
104 "pnat_add_left_cancel_less"; |
|
105 "pnat_add_lessD1"; |
|
106 "pnat_not_add_less1"; |
|
107 "pnat_not_add_less2"; |
|
108 PNat.ML:qed_spec_mp |
|
109 "pnat_add_leD1"; |
|
110 "pnat_add_leD2"; |
|
111 PNat.ML:qed |
|
112 "pnat_less_add_eq_less"; |
|
113 "pnat_less_iff"; |
|
114 "pnat_linear_Ex_eq"; |
|
115 "pnat_eq_lessI"; |
|
116 "Rep_pnat_mult_1"; |
|
117 "Rep_pnat_mult_1_right"; |
|
118 "mult_Rep_pnat"; |
|
119 "mult_Rep_pnat_mult"; |
|
120 "pnat_mult_commute"; "(?m::pnat) * (?n::pnat) = ?n * ?m" |
|
121 "pnat_add_mult_distrib"; |
|
122 "pnat_add_mult_distrib2"; |
|
123 "pnat_mult_assoc"; |
|
124 "pnat_mult_left_commute"; |
|
125 "pnat_mult_1"; |
|
126 "pnat_mult_1_left"; |
|
127 "pnat_mult_less_mono2"; |
|
128 "pnat_mult_less_mono1"; |
|
129 "pnat_mult_less_cancel2"; |
|
130 "pnat_mult_less_cancel1"; |
|
131 "pnat_mult_cancel2"; |
|
132 "pnat_mult_cancel1"; |
|
133 "pnat_same_multI2"; |
|
134 "eq_Abs_pnat"; |
|
135 "pnat_one_iff"; |
|
136 "pnat_two_eq"; |
|
137 "inj_pnat_of_nat"; |
|
138 "nat_add_one_less"; |
|
139 "nat_add_one_less1"; |
|
140 "pnat_of_nat_add"; |
|
141 "pnat_of_nat_less_iff"; |
|
142 "pnat_of_nat_mult"; |
|
143 PRat.ML:qed ------------------------------------------------------------------ |
|
144 "prat_trans_lemma"; |
|
145 "[| (?x1.0::pnat) * (?y2.0::pnat) = (?x2.0::pnat) * (?y1.0::pnat); |
|
146 ?x2.0 * (?y3.0::pnat) = (?x3.0::pnat) * ?y2.0 |] |
|
147 ==> ?x1.0 * ?y3.0 = ?x3.0 * ?y1.0" |
|
148 "ratrel_iff"; |
|
149 "ratrelI"; |
|
150 "ratrelE_lemma"; |
|
151 "ratrelE"; |
|
152 "ratrel_refl"; |
|
153 "equiv_ratrel"; |
|
154 "ratrel_in_prat"; |
|
155 "inj_on_Abs_prat"; |
|
156 "inj_Rep_prat"; |
|
157 "inj_prat_of_pnat"; |
|
158 "eq_Abs_prat"; |
|
159 "qinv_congruent"; |
|
160 "qinv"; |
|
161 "qinv_qinv"; |
|
162 "inj_qinv"; |
|
163 "qinv_1"; |
|
164 "prat_add_congruent2_lemma"; |
|
165 "prat_add_congruent2"; |
|
166 "prat_add"; |
|
167 "prat_add_commute"; |
|
168 "prat_add_assoc"; |
|
169 "prat_add_left_commute"; |
|
170 "pnat_mult_congruent2"; |
|
171 "prat_mult"; |
|
172 "prat_mult_commute"; |
|
173 "prat_mult_assoc"; |
|
174 "prat_mult_left_commute"; |
|
175 "prat_mult_1"; |
|
176 "prat_mult_1_right"; |
|
177 "prat_of_pnat_add"; |
|
178 "prat_of_pnat_mult"; |
|
179 "prat_mult_qinv"; |
|
180 "prat_mult_qinv_right"; |
|
181 "prat_qinv_ex"; |
|
182 "prat_qinv_ex1"; |
|
183 "prat_qinv_left_ex1"; |
|
184 "prat_mult_inv_qinv"; |
|
185 "prat_as_inverse_ex"; |
|
186 "qinv_mult_eq"; |
|
187 "prat_add_mult_distrib"; |
|
188 "prat_add_mult_distrib2"; |
|
189 "prat_less_iff"; |
|
190 "prat_lessI"; |
|
191 "prat_lessE_lemma"; |
|
192 "prat_lessE"; |
|
193 "prat_less_trans"; |
|
194 "prat_less_not_refl"; |
|
195 "prat_less_not_sym"; |
|
196 "lemma_prat_dense"; |
|
197 "prat_lemma_dense"; |
|
198 "prat_dense"; |
|
199 "prat_add_less2_mono1"; |
|
200 "prat_add_less2_mono2"; |
|
201 "prat_mult_less2_mono1"; |
|
202 "prat_mult_left_less2_mono1"; |
|
203 "lemma_prat_add_mult_mono"; |
|
204 "qless_Ex"; |
|
205 "lemma_prat_less_linear"; |
|
206 "prat_linear"; |
|
207 "prat_linear_less2"; |
|
208 "lemma1_qinv_prat_less"; |
|
209 "lemma2_qinv_prat_less"; |
|
210 "qinv_prat_less"; |
|
211 "prat_qinv_gt_1"; |
|
212 "prat_qinv_is_gt_1"; |
|
213 "prat_less_1_2"; |
|
214 "prat_less_qinv_2_1"; |
|
215 "prat_mult_qinv_less_1"; |
|
216 "prat_self_less_add_self"; |
|
217 "prat_self_less_add_right"; |
|
218 "prat_self_less_add_left"; |
|
219 "prat_self_less_mult_right"; |
|
220 "prat_leI"; |
|
221 "prat_leD"; |
|
222 "prat_less_le_iff"; |
|
223 "not_prat_leE"; |
|
224 "prat_less_imp_le"; |
|
225 "prat_le_imp_less_or_eq"; |
|
226 "prat_less_or_eq_imp_le"; |
|
227 "prat_le_eq_less_or_eq"; |
|
228 "prat_le_refl"; |
|
229 "prat_le_less_trans"; |
|
230 "prat_le_trans"; |
|
231 "not_less_not_eq_prat_less"; |
|
232 "prat_add_less_mono"; |
|
233 "prat_mult_less_mono"; |
|
234 "prat_mult_left_le2_mono1"; |
|
235 "prat_mult_le2_mono1"; |
|
236 "qinv_prat_le"; |
|
237 "prat_add_left_le2_mono1"; |
|
238 "prat_add_le2_mono1"; |
|
239 "prat_add_le_mono"; |
|
240 "prat_add_right_less_cancel"; |
|
241 "prat_add_left_less_cancel"; |
|
242 "Abs_prat_mult_qinv"; |
|
243 "lemma_Abs_prat_le1"; |
|
244 "lemma_Abs_prat_le2"; |
|
245 "lemma_Abs_prat_le3"; |
|
246 "pre_lemma_gleason9_34"; |
|
247 "pre_lemma_gleason9_34b"; |
|
248 "prat_of_pnat_less_iff"; |
|
249 "lemma_prat_less_1_memEx"; |
|
250 "lemma_prat_less_1_set_non_empty"; |
|
251 "empty_set_psubset_lemma_prat_less_1_set"; |
|
252 "lemma_prat_less_1_not_memEx"; |
|
253 "lemma_prat_less_1_set_not_rat_set"; |
|
254 "lemma_prat_less_1_set_psubset_rat_set"; |
|
255 "preal_1"; |
|
256 "{x::prat. x < prat_of_pnat (Abs_pnat (Suc (0::nat)))} |
|
257 : {A::prat set. |
|
258 {} < A & |
|
259 A < UNIV & |
|
260 (ALL y::prat:A. (ALL z::prat. z < y --> z : A) & Bex A (op < y))}" |
|
261 PReal.ML:qed ----------------------------------------------------------------- |
|
262 "inj_on_Abs_preal"; "inj_on Abs_preal preal" |
|
263 "inj_Rep_preal"; |
|
264 "empty_not_mem_preal"; |
|
265 "one_set_mem_preal"; |
|
266 "preal_psubset_empty"; |
|
267 "Rep_preal_psubset_empty"; |
|
268 "mem_Rep_preal_Ex"; |
|
269 "prealI1"; |
|
270 "[| {} < (?A::prat set); ?A < UNIV; |
|
271 ALL y::prat:?A. (ALL z::prat. z < y --> z : ?A) & Bex ?A (op < y) |] |
|
272 ==> ?A : preal" |
|
273 "prealI2"; |
|
274 "prealE_lemma"; |
|
275 "prealE_lemma1"; |
|
276 "prealE_lemma2"; |
|
277 "prealE_lemma3"; |
|
278 "prealE_lemma3a"; |
|
279 "prealE_lemma3b"; |
|
280 "prealE_lemma4"; |
|
281 "prealE_lemma4a"; |
|
282 "not_mem_Rep_preal_Ex"; |
|
283 "lemma_prat_less_set_mem_preal"; |
|
284 "lemma_prat_set_eq"; |
|
285 "inj_preal_of_prat"; |
|
286 "not_in_preal_ub"; |
|
287 "preal_less_not_refl"; |
|
288 "preal_not_refl2"; |
|
289 "preal_less_trans"; |
|
290 "preal_less_not_sym"; |
|
291 "preal_linear"; |
|
292 "(?r1.0::preal) < (?r2.0::preal) | ?r1.0 = ?r2.0 | ?r2.0 < ?r1.0" |
|
293 "preal_linear_less2"; |
|
294 "preal_add_commute"; "(?x::preal) + (?y::preal) = ?y + ?x" |
|
295 "preal_add_set_not_empty"; |
|
296 "preal_not_mem_add_set_Ex"; |
|
297 "preal_add_set_not_prat_set"; |
|
298 "preal_add_set_lemma3"; |
|
299 "preal_add_set_lemma4"; |
|
300 "preal_mem_add_set"; |
|
301 "preal_add_assoc"; |
|
302 "preal_add_left_commute"; |
|
303 "preal_mult_commute"; "(?x::preal) * (?y::preal) = ?y * ?x" |
|
304 "preal_mult_set_not_empty"; |
|
305 "preal_not_mem_mult_set_Ex"; |
|
306 "preal_mult_set_not_prat_set"; |
|
307 "preal_mult_set_lemma3"; |
|
308 "preal_mult_set_lemma4"; |
|
309 "preal_mem_mult_set"; |
|
310 "preal_mult_assoc"; |
|
311 "preal_mult_left_commute"; |
|
312 "preal_mult_1"; |
|
313 "preal_mult_1_right"; |
|
314 "preal_add_assoc_cong"; |
|
315 "preal_add_assoc_swap"; |
|
316 "mem_Rep_preal_addD"; |
|
317 "mem_Rep_preal_addI"; |
|
318 "mem_Rep_preal_add_iff"; |
|
319 "mem_Rep_preal_multD"; |
|
320 "mem_Rep_preal_multI"; |
|
321 "mem_Rep_preal_mult_iff"; |
|
322 "lemma_add_mult_mem_Rep_preal"; |
|
323 "lemma_add_mult_mem_Rep_preal1"; |
|
324 "lemma_preal_add_mult_distrib"; |
|
325 "lemma_preal_add_mult_distrib2"; |
|
326 "preal_add_mult_distrib2"; |
|
327 "preal_add_mult_distrib"; |
|
328 "qinv_not_mem_Rep_preal_Ex"; |
|
329 "lemma_preal_mem_inv_set_ex"; |
|
330 "preal_inv_set_not_empty"; |
|
331 "qinv_mem_Rep_preal_Ex"; |
|
332 "preal_not_mem_inv_set_Ex"; |
|
333 "preal_inv_set_not_prat_set"; |
|
334 "preal_inv_set_lemma3"; |
|
335 "preal_inv_set_lemma4"; |
|
336 "preal_mem_inv_set"; |
|
337 "preal_mem_mult_invD"; |
|
338 "lemma1_gleason9_34"; |
|
339 "lemma1b_gleason9_34"; |
|
340 "lemma_gleason9_34a"; |
|
341 "lemma_gleason9_34"; |
|
342 "lemma1_gleason9_36"; |
|
343 "lemma2_gleason9_36"; |
|
344 "lemma_gleason9_36"; |
|
345 "lemma_gleason9_36a"; |
|
346 "preal_mem_mult_invI"; |
|
347 "preal_mult_inv"; |
|
348 "preal_mult_inv_right"; |
|
349 "eq_Abs_preal"; |
|
350 "Rep_preal_self_subset"; |
|
351 "Rep_preal_sum_not_subset"; |
|
352 "Rep_preal_sum_not_eq"; |
|
353 "preal_self_less_add_left"; |
|
354 "preal_self_less_add_right"; |
|
355 "preal_leD"; |
|
356 "not_preal_leE"; |
|
357 "preal_leI"; |
|
358 "preal_less_le_iff"; |
|
359 "preal_less_imp_le"; |
|
360 "preal_le_imp_less_or_eq"; |
|
361 "preal_less_or_eq_imp_le"; |
|
362 "preal_le_refl"; |
|
363 "preal_le_trans"; |
|
364 "preal_le_anti_sym"; |
|
365 "preal_neq_iff"; |
|
366 "preal_less_le"; |
|
367 "lemma_psubset_mem"; |
|
368 "lemma_psubset_not_refl"; |
|
369 "psubset_trans"; |
|
370 "subset_psubset_trans"; |
|
371 "subset_psubset_trans2"; |
|
372 "psubsetD"; |
|
373 "lemma_ex_mem_less_left_add1"; |
|
374 "preal_less_set_not_empty"; |
|
375 "lemma_ex_not_mem_less_left_add1"; |
|
376 "preal_less_set_not_prat_set"; |
|
377 "preal_less_set_lemma3"; |
|
378 "preal_less_set_lemma4"; |
|
379 "preal_mem_less_set"; |
|
380 "preal_less_add_left_subsetI"; |
|
381 "lemma_sum_mem_Rep_preal_ex"; |
|
382 "preal_less_add_left_subsetI2"; |
|
383 "preal_less_add_left"; |
|
384 "preal_less_add_left_Ex"; |
|
385 "preal_add_less2_mono1"; |
|
386 "preal_add_less2_mono2"; |
|
387 "preal_mult_less_mono1"; |
|
388 "preal_mult_left_less_mono1"; |
|
389 "preal_mult_left_le_mono1"; |
|
390 "preal_mult_le_mono1"; |
|
391 "preal_add_left_le_mono1"; |
|
392 "preal_add_le_mono1"; |
|
393 "preal_add_right_less_cancel"; |
|
394 "preal_add_left_less_cancel"; |
|
395 "preal_add_less_iff1"; |
|
396 "preal_add_less_iff2"; |
|
397 "preal_add_less_mono"; |
|
398 "preal_mult_less_mono"; |
|
399 "preal_add_right_cancel"; |
|
400 "preal_add_left_cancel"; |
|
401 "preal_add_left_cancel_iff"; |
|
402 "preal_add_right_cancel_iff"; |
|
403 "preal_sup_mem_Ex"; |
|
404 "preal_sup_set_not_empty"; |
|
405 "preal_sup_not_mem_Ex"; |
|
406 "preal_sup_not_mem_Ex1"; |
|
407 "preal_sup_set_not_prat_set"; |
|
408 "preal_sup_set_not_prat_set1"; |
|
409 "preal_sup_set_lemma3"; |
|
410 "preal_sup_set_lemma3_1"; |
|
411 "preal_sup_set_lemma4"; |
|
412 "preal_sup_set_lemma4_1"; |
|
413 "preal_sup"; |
|
414 "preal_sup1"; |
|
415 "preal_psup_leI"; |
|
416 "preal_psup_leI2"; |
|
417 "preal_psup_leI2b"; |
|
418 "preal_psup_leI2a"; |
|
419 "psup_le_ub"; |
|
420 "psup_le_ub1"; |
|
421 "preal_complete"; |
|
422 "lemma_preal_rat_less"; |
|
423 "lemma_preal_rat_less2"; |
|
424 "preal_of_prat_add"; |
|
425 "lemma_preal_rat_less3"; |
|
426 "lemma_preal_rat_less4"; |
|
427 "preal_of_prat_mult"; |
|
428 "preal_of_prat_less_iff"; "(preal_of_prat ?p < preal_of_prat ?q) = (?p < ?q)" |
|
429 RealDef.ML:qed --------------------------------------------------------------- |
|
430 "preal_trans_lemma"; |
|
431 "realrel_iff"; |
|
432 "realrelI"; |
|
433 "?x1.0 + ?y2.0 = ?x2.0 + ?y1.0 ==> ((?x1.0, ?y1.0), ?x2.0, ?y2.0) : realrel" |
|
434 "realrelE_lemma"; |
|
435 "realrelE"; |
|
436 "realrel_refl"; |
|
437 "equiv_realrel"; |
|
438 "realrel_in_real"; |
|
439 "inj_on_Abs_REAL"; |
|
440 "inj_Rep_REAL"; |
|
441 "inj_real_of_preal"; |
|
442 "eq_Abs_REAL"; |
|
443 "real_minus_congruent"; |
|
444 "real_minus"; |
|
445 "- Abs_REAL (realrel `` {(?x, ?y)}) = Abs_REAL (realrel `` {(?y, ?x)})" |
|
446 "real_minus_minus"; (**)"- (- (?z::real)) = ?z" |
|
447 "inj_real_minus"; "inj uminus" |
|
448 "real_minus_zero"; (**)"- 0 = 0" |
|
449 "real_minus_zero_iff"; (**)"(- ?x = 0) = (?x = 0)" |
|
450 "real_add_congruent2"; |
|
451 "congruent2 realrel |
|
452 (%p1 p2. (%(x1, y1). (%(x2, y2). realrel `` {(x1 + x2, y1 + y2)}) p2) p1)" |
|
453 "real_add"; |
|
454 "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) + |
|
455 Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) = |
|
456 Abs_REAL (realrel `` {(?x1.0 + ?x2.0, ?y1.0 + ?y2.0)})" |
|
457 "real_add_commute"; (**)"(?z::real) + (?w::real) = ?w + ?z" |
|
458 "real_add_assoc"; (**) |
|
459 "real_add_left_commute"; (**) |
|
460 "real_add_zero_left"; (**)"0 + ?z = ?z" |
|
461 "real_add_zero_right"; (**) |
|
462 "real_add_minus"; (**)"?z + - ?z = 0" |
|
463 "real_add_minus_left"; (**) |
|
464 "real_add_minus_cancel"; (**)"?z + (- ?z + ?w) = ?w" |
|
465 "real_minus_add_cancel"; (**)"- ?z + (?z + ?w) = ?w" |
|
466 "real_minus_ex"; "EX y. ?x + y = 0" |
|
467 "real_minus_ex1"; |
|
468 "real_minus_left_ex1"; "EX! y. y + ?x = 0" |
|
469 "real_add_minus_eq_minus";"?x + ?y = 0 ==> ?x = - ?y" |
|
470 "real_as_add_inverse_ex"; "EX y. ?x = - y" |
|
471 "real_minus_add_distrib"; (**)"- (?x + ?y) = - ?x + - ?y" |
|
472 "real_add_left_cancel"; "(?x + ?y = ?x + ?z) = (?y = ?z)" |
|
473 "real_add_right_cancel"; "(?y + ?x = ?z + ?x) = (?y = ?z)" |
|
474 "real_diff_0"; (**)"0 - ?x = - ?x" |
|
475 "real_diff_0_right"; (**)"?x - 0 = ?x" |
|
476 "real_diff_self"; (**)"?x - ?x = 0" |
|
477 "real_mult_congruent2_lemma"; |
|
478 "real_mult_congruent2"; |
|
479 "congruent2 realrel |
|
480 (%p1 p2. |
|
481 (%(x1, y1). |
|
482 (%(x2, y2). realrel `` {(x1 * x2 + y1 * y2, x1 * y2 + x2 * y1)}) |
|
483 p2) p1)" |
|
484 "real_mult"; |
|
485 "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) * |
|
486 Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) = |
|
487 Abs_REAL |
|
488 (realrel `` |
|
489 {(?x1.0 * ?x2.0 + ?y1.0 * ?y2.0, ?x1.0 * ?y2.0 + ?x2.0 * ?y1.0)})" |
|
490 "real_mult_commute"; (**)"?z * ?w = ?w * ?z" |
|
491 "real_mult_assoc"; (**) |
|
492 "real_mult_left_commute"; |
|
493 (**)"?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)" |
|
494 "real_mult_1"; (**)"1 * ?z = ?z" |
|
495 "real_mult_1_right"; (**)"?z * 1 = ?z" |
|
496 "real_mult_0"; (**) |
|
497 "real_mult_0_right"; (**)"?z * 0 = 0" |
|
498 "real_mult_minus_eq1"; (**)"- ?x * ?y = - (?x * ?y)" |
|
499 "real_mult_minus_eq2"; (**)"?x * - ?y = - (?x * ?y)" |
|
500 "real_mult_minus_1"; (**)"- 1 * ?z = - ?z" |
|
501 "real_mult_minus_1_right";(**)"?z * - 1 = - ?z" |
|
502 "real_minus_mult_cancel"; (**)"- ?x * - ?y = ?x * ?y" |
|
503 "real_minus_mult_commute";(**)"- ?x * ?y = ?x * - ?y" |
|
504 "real_add_assoc_cong"; |
|
505 "?z + ?v = ?z' + ?v' ==> ?z + (?v + ?w) = ?z' + (?v' + ?w)" |
|
506 "real_add_assoc_swap"; (**)"?z + (?v + ?w) = ?v + (?z + ?w)" |
|
507 "real_add_mult_distrib"; (**)"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w" |
|
508 "real_add_mult_distrib2"; (**)"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0" |
|
509 "real_diff_mult_distrib"; (**)"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w" |
|
510 "real_diff_mult_distrib2";(**)"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0" |
|
511 "real_zero_not_eq_one"; |
|
512 "real_zero_iff"; "0 = Abs_REAL (realrel `` {(?x, ?x)})" |
|
513 "real_mult_inv_right_ex"; "?x ~= 0 ==> EX y. ?x * y = 1" |
|
514 "real_mult_inv_left_ex"; "?x ~= 0 ==> inverse ?x * ?x = 1" |
|
515 "real_mult_inv_left"; |
|
516 "real_mult_inv_right"; "?x ~= 0 ==> ?x * inverse ?x = 1" |
|
517 "INVERSE_ZERO"; "inverse 0 = 0" |
|
518 "DIVISION_BY_ZERO"; (*NOT for adding to default simpset*)"?a / 0 = 0" |
|
519 "real_mult_left_cancel"; (**)"?c ~= 0 ==> (?c * ?a = ?c * ?b) = (?a = ?b)" |
|
520 "real_mult_right_cancel"; (**)"?c ~= 0 ==> (?a * ?c = ?b * ?c) = (?a = ?b)" |
|
521 "real_mult_left_cancel_ccontr"; "?c * ?a ~= ?c * ?b ==> ?a ~= ?b" |
|
522 "real_mult_right_cancel_ccontr"; "?a * ?c ~= ?b * ?c ==> ?a ~= ?b" |
|
523 "real_inverse_not_zero"; "?x ~= 0 ==> inverse ?x ~= 0" |
|
524 "real_mult_not_zero"; "[| ?x ~= 0; ?y ~= 0 |] ==> ?x * ?y ~= 0" |
|
525 "real_inverse_inverse"; "inverse (inverse ?x) = ?x" |
|
526 "real_inverse_1"; "inverse 1 = 1" |
|
527 "real_minus_inverse"; "inverse (- ?x) = - inverse ?x" |
|
528 "real_inverse_distrib"; "inverse (?x * ?y) = inverse ?x * inverse ?y" |
|
529 "real_times_divide1_eq"; (**)"?x * (?y / ?z) = ?x * ?y / ?z" |
|
530 "real_times_divide2_eq"; (**)"?y / ?z * ?x = ?y * ?x / ?z" |
|
531 "real_divide_divide1_eq"; (**)"?x / (?y / ?z) = ?x * ?z / ?y" |
|
532 "real_divide_divide2_eq"; (**)"?x / ?y / ?z = ?x / (?y * ?z)" |
|
533 "real_minus_divide_eq"; (**)"- ?x / ?y = - (?x / ?y)" |
|
534 "real_divide_minus_eq"; (**)"?x / - ?y = - (?x / ?y)" |
|
535 "real_add_divide_distrib"; (**)"(?x + ?y) / ?z = ?x / ?z + ?y / ?z" |
|
536 "preal_lemma_eq_rev_sum"; |
|
537 "[| ?x = ?y; ?x1.0 = ?y1.0 |] ==> ?x + ?y1.0 = ?x1.0 + ?y" |
|
538 "preal_add_left_commute_cancel"; |
|
539 "?x + (?b + ?y) = ?x1.0 + (?b + ?y1.0) ==> ?x + ?y = ?x1.0 + ?y1.0" |
|
540 "preal_lemma_for_not_refl"; |
|
541 "real_less_not_refl"; "~ ?R < ?R" |
|
542 "real_not_refl2"; |
|
543 "preal_lemma_trans"; |
|
544 "real_less_trans"; |
|
545 "real_less_not_sym"; |
|
546 "real_of_preal_add"; |
|
547 "real_of_preal (?z1.0 + ?z2.0) = real_of_preal ?z1.0 + real_of_preal ?z2.0" |
|
548 "real_of_preal_mult"; |
|
549 "real_of_preal_ExI"; |
|
550 "real_of_preal_ExD"; |
|
551 "real_of_preal_iff"; |
|
552 "real_of_preal_trichotomy"; |
|
553 "real_of_preal_trichotomyE"; |
|
554 "real_of_preal_lessD"; |
|
555 "real_of_preal_lessI"; |
|
556 "?m1.0 < ?m2.0 ==> real_of_preal ?m1.0 < real_of_preal ?m2.0" |
|
557 "real_of_preal_less_iff1"; |
|
558 "real_of_preal_minus_less_self"; |
|
559 "real_of_preal_minus_less_zero"; |
|
560 "real_of_preal_not_minus_gt_zero"; |
|
561 "real_of_preal_zero_less"; |
|
562 "real_of_preal_not_less_zero"; |
|
563 "real_minus_minus_zero_less"; |
|
564 "real_of_preal_sum_zero_less"; |
|
565 "real_of_preal_minus_less_all"; |
|
566 "real_of_preal_not_minus_gt_all"; |
|
567 "real_of_preal_minus_less_rev1"; |
|
568 "real_of_preal_minus_less_rev2"; |
|
569 "real_of_preal_minus_less_rev_iff"; |
|
570 "real_linear"; "?R1.0 < ?R2.0 | ?R1.0 = ?R2.0 | ?R2.0 < ?R1.0" |
|
571 "real_neq_iff"; |
|
572 "real_linear_less2"; |
|
573 "[| ?R1.0 < ?R2.0 ==> ?P; ?R1.0 = ?R2.0 ==> ?P; ?R2.0 < ?R1.0 ==> ?P |] |
|
574 ==> ?P" |
|
575 "real_leI"; |
|
576 "real_leD"; "~ ?w < ?z ==> ?z <= ?w" |
|
577 "real_less_le_iff"; |
|
578 "not_real_leE"; |
|
579 "real_le_imp_less_or_eq"; |
|
580 "real_less_or_eq_imp_le"; |
|
581 "real_le_less"; |
|
582 "real_le_refl"; "?w <= ?w" |
|
583 "real_le_linear"; |
|
584 "real_le_trans"; "[| ?i <= ?j; ?j <= ?k |] ==> ?i <= ?k" |
|
585 "real_le_anti_sym"; "[| ?z <= ?w; ?w <= ?z |] ==> ?z = ?w" |
|
586 "not_less_not_eq_real_less"; |
|
587 "real_less_le"; "(?w < ?z) = (?w <= ?z & ?w ~= ?z)" |
|
588 "real_minus_zero_less_iff"; |
|
589 "real_minus_zero_less_iff2"; |
|
590 "real_less_add_positive_left_Ex"; |
|
591 "real_less_sum_gt_zero"; "?W < ?S ==> 0 < ?S + - ?W" |
|
592 "real_lemma_change_eq_subj"; |
|
593 "real_sum_gt_zero_less"; "0 < ?S + - ?W ==> ?W < ?S" |
|
594 "real_less_sum_gt_0_iff"; "(0 < ?S + - ?W) = (?W < ?S)" |
|
595 "real_less_eq_diff"; "(?x < ?y) = (?x - ?y < 0)" |
|
596 "real_add_diff_eq"; (**)"?x + (?y - ?z) = ?x + ?y - ?z" |
|
597 "real_diff_add_eq"; (**)"?x - ?y + ?z = ?x + ?z - ?y" |
|
598 "real_diff_diff_eq"; (**)"?x - ?y - ?z = ?x - (?y + ?z)" |
|
599 "real_diff_diff_eq2"; (**)"?x - (?y - ?z) = ?x + ?z - ?y" |
|
600 "real_diff_less_eq"; "(?x - ?y < ?z) = (?x < ?z + ?y)" |
|
601 "real_less_diff_eq"; |
|
602 "real_diff_le_eq"; "(?x - ?y <= ?z) = (?x <= ?z + ?y)" |
|
603 "real_le_diff_eq"; |
|
604 "real_diff_eq_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)" |
|
605 "real_eq_diff_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)" |
|
606 "real_less_eqI"; |
|
607 "real_le_eqI"; |
|
608 "real_eq_eqI"; "?x - ?y = ?x' - ?y' ==> (?x = ?y) = (?x' = ?y')" |
|
609 RealOrd.ML:qed --------------------------------------------------------------- |
|
610 "real_add_cancel_21"; "(?x + (?y + ?z) = ?y + ?u) = (?x + ?z = ?u)" |
|
611 "real_add_cancel_end"; "(?x + (?y + ?z) = ?y) = (?x = - ?z)" |
|
612 "real_minus_diff_eq"; (*??*)"- (?x - ?y) = ?y - ?x" |
|
613 "real_gt_zero_preal_Ex"; |
|
614 "real_gt_preal_preal_Ex"; |
|
615 "real_ge_preal_preal_Ex"; |
|
616 "real_less_all_preal"; "?y <= 0 ==> ALL x. ?y < real_of_preal x" |
|
617 "real_less_all_real2"; |
|
618 "real_lemma_add_positive_imp_less"; |
|
619 "real_ex_add_positive_left_less";"EX T. 0 < T & ?R + T = ?S ==> ?R < ?S" |
|
620 "real_less_iff_add"; |
|
621 "real_of_preal_le_iff"; |
|
622 "real_mult_order"; "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x * ?y" |
|
623 "neg_real_mult_order"; |
|
624 "real_mult_less_0"; "[| 0 < ?x; ?y < 0 |] ==> ?x * ?y < 0" |
|
625 "real_zero_less_one"; "0 < 1" |
|
626 "real_add_right_cancel_less"; "(?v + ?z < ?w + ?z) = (?v < ?w)" |
|
627 "real_add_left_cancel_less"; |
|
628 "real_add_right_cancel_le"; |
|
629 "real_add_left_cancel_le"; |
|
630 "real_add_less_le_mono"; "[| ?w' < ?w; ?z' <= ?z |] ==> ?w' + ?z' < ?w + ?z" |
|
631 "real_add_le_less_mono"; "[| ?w' <= ?w; ?z' < ?z |] ==> ?w' + ?z' < ?w + ?z" |
|
632 "real_add_less_mono2"; |
|
633 "real_less_add_right_cancel"; |
|
634 "real_less_add_left_cancel"; "?C + ?A < ?C + ?B ==> ?A < ?B" |
|
635 "real_le_add_right_cancel"; |
|
636 "real_le_add_left_cancel"; "?C + ?A <= ?C + ?B ==> ?A <= ?B" |
|
637 "real_add_order"; "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x + ?y" |
|
638 "real_le_add_order"; |
|
639 "real_add_less_mono"; |
|
640 "real_add_left_le_mono1"; |
|
641 "real_add_le_mono"; |
|
642 "real_less_Ex"; |
|
643 "real_add_minus_positive_less_self"; "0 < ?r ==> ?u + - ?r < ?u" |
|
644 "real_le_minus_iff"; "(- ?s <= - ?r) = (?r <= ?s)" |
|
645 "real_le_square"; |
|
646 "real_of_posnat_one"; |
|
647 "real_of_posnat_two"; |
|
648 "real_of_posnat_add"; "real_of_posnat ?n1.0 + real_of_posnat ?n2.0 = |
|
649 real_of_posnat (?n1.0 + ?n2.0) + 1" |
|
650 "real_of_posnat_add_one"; |
|
651 "real_of_posnat_Suc"; |
|
652 "inj_real_of_posnat"; |
|
653 "real_of_nat_zero"; |
|
654 "real_of_nat_one"; "real (Suc 0) = 1" |
|
655 "real_of_nat_add"; |
|
656 "real_of_nat_Suc"; |
|
657 "real_of_nat_less_iff"; |
|
658 "real_of_nat_le_iff"; |
|
659 "inj_real_of_nat"; |
|
660 "real_of_nat_ge_zero"; |
|
661 "real_of_nat_mult"; |
|
662 "real_of_nat_inject"; |
|
663 RealOrd.ML:qed_spec_mp |
|
664 "real_of_nat_diff"; |
|
665 RealOrd.ML:qed |
|
666 "real_of_nat_zero_iff"; |
|
667 "real_of_nat_neg_int"; |
|
668 "real_inverse_gt_0"; |
|
669 "real_inverse_less_0"; |
|
670 "real_mult_less_mono1"; |
|
671 "real_mult_less_mono2"; |
|
672 "real_mult_less_cancel1"; |
|
673 "(?k * ?m < ?k * ?n) = (0 < ?k & ?m < ?n | ?k < 0 & ?n < ?m)" |
|
674 "real_mult_less_cancel2"; |
|
675 "real_mult_less_iff1"; |
|
676 "real_mult_less_iff2"; |
|
677 "real_mult_le_cancel_iff1"; |
|
678 "real_mult_le_cancel_iff2"; |
|
679 "real_mult_le_less_mono1"; |
|
680 "real_mult_less_mono"; |
|
681 "real_mult_less_mono'"; |
|
682 "real_gt_zero"; "1 <= ?x ==> 0 < ?x" |
|
683 "real_mult_self_le"; "[| 1 < ?r; 1 <= ?x |] ==> ?x <= ?r * ?x" |
|
684 "real_mult_self_le2"; |
|
685 "real_inverse_less_swap"; |
|
686 "real_mult_is_0"; |
|
687 "real_inverse_add"; |
|
688 "real_minus_zero_le_iff"; |
|
689 "real_minus_zero_le_iff2"; |
|
690 "real_sum_squares_cancel"; "?x * ?x + ?y * ?y = 0 ==> ?x = 0" |
|
691 "real_sum_squares_cancel2"; "?x * ?x + ?y * ?y = 0 ==> ?y = 0" |
|
692 "real_0_less_mult_iff"; |
|
693 "real_0_le_mult_iff"; |
|
694 "real_mult_less_0_iff"; "(?x * ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)" |
|
695 "real_mult_le_0_iff"; |
|
696 RealInt.ML:qed --------------------------------------------------------------- |
|
697 "real_of_int_congruent"; |
|
698 "real_of_int"; "real (Abs_Integ (intrel `` {(?i, ?j)})) = |
|
699 Abs_REAL |
|
700 (realrel `` |
|
701 {(preal_of_prat (prat_of_pnat (pnat_of_nat ?i)), |
|
702 preal_of_prat (prat_of_pnat (pnat_of_nat ?j)))})" |
|
703 "inj_real_of_int"; |
|
704 "real_of_int_zero"; |
|
705 "real_of_one"; |
|
706 "real_of_int_add"; "real ?x + real ?y = real (?x + ?y)" |
|
707 "real_of_int_minus"; |
|
708 "real_of_int_diff"; |
|
709 "real_of_int_mult"; "real ?x * real ?y = real (?x * ?y)" |
|
710 "real_of_int_Suc"; |
|
711 "real_of_int_real_of_nat"; |
|
712 "real_of_nat_real_of_int"; |
|
713 "real_of_int_zero_cancel"; |
|
714 "real_of_int_less_cancel"; |
|
715 "real_of_int_inject"; |
|
716 "real_of_int_less_mono"; |
|
717 "real_of_int_less_iff"; |
|
718 "real_of_int_le_iff"; |
|
719 RealBin.ML:qed --------------------------------------------------------------- |
|
720 "real_number_of"; "real (number_of ?w) = number_of ?w" |
|
721 "real_numeral_0_eq_0"; |
|
722 "real_numeral_1_eq_1"; |
|
723 "add_real_number_of"; |
|
724 "minus_real_number_of"; |
|
725 "diff_real_number_of"; |
|
726 "mult_real_number_of"; |
|
727 "real_mult_2"; (**)"2 * ?z = ?z + ?z" |
|
728 "real_mult_2_right"; (**)"?z * 2 = ?z + ?z" |
|
729 "eq_real_number_of"; |
|
730 "less_real_number_of"; |
|
731 "le_real_number_of_eq_not_less"; |
|
732 "real_minus_1_eq_m1"; "- 1 = -1"(*uminus.. = "-.."*) |
|
733 "real_mult_minus1"; (**)"-1 * ?z = - ?z" |
|
734 "real_mult_minus1_right"; (**)"?z * -1 = - ?z" |
|
735 "zero_less_real_of_nat_iff";"(0 < real ?n) = (0 < ?n)" |
|
736 "zero_le_real_of_nat_iff"; |
|
737 "real_add_number_of_left"; |
|
738 "real_mult_number_of_left"; |
|
739 "number_of ?v * (number_of ?w * ?z) = number_of (bin_mult ?v ?w) * ?z" |
|
740 "real_add_number_of_diff1"; |
|
741 "real_add_number_of_diff2";"number_of ?v + (?c - number_of ?w) = |
|
742 number_of (bin_add ?v (bin_minus ?w)) + ?c" |
|
743 "real_of_nat_number_of"; |
|
744 "real (number_of ?v) = (if neg (number_of ?v) then 0 else number_of ?v)" |
|
745 "real_less_iff_diff_less_0"; "(?x < ?y) = (?x - ?y < 0)" |
|
746 "real_eq_iff_diff_eq_0"; |
|
747 "real_le_iff_diff_le_0"; |
|
748 "left_real_add_mult_distrib"; |
|
749 (**)"?i * ?u + (?j * ?u + ?k) = (?i + ?j) * ?u + ?k" |
|
750 "real_eq_add_iff1"; |
|
751 "(?i * ?u + ?m = ?j * ?u + ?n) = ((?i - ?j) * ?u + ?m = ?n)" |
|
752 "real_eq_add_iff2"; |
|
753 "real_less_add_iff1"; |
|
754 "real_less_add_iff2"; |
|
755 "real_le_add_iff1"; |
|
756 "real_le_add_iff2"; |
|
757 "real_mult_le_mono1"; |
|
758 "real_mult_le_mono2"; |
|
759 "real_mult_le_mono"; |
|
760 "[| ?i <= ?j; ?k <= ?l; 0 <= ?j; 0 <= ?k |] ==> ?i * ?k <= ?j * ?l" |
|
761 RealArith0.ML:qed ------------------------------------------------------------ |
|
762 "real_diff_minus_eq"; (**)"?x - - ?y = ?x + ?y" |
|
763 "real_0_divide"; (**)"0 / ?x = 0" |
|
764 "real_0_less_inverse_iff"; "(0 < inverse ?x) = (0 < ?x)" |
|
765 "real_inverse_less_0_iff"; |
|
766 "real_0_le_inverse_iff"; |
|
767 "real_inverse_le_0_iff"; |
|
768 "REAL_DIVIDE_ZERO"; "?x / 0 = 0"(*!!!*) |
|
769 "real_inverse_eq_divide"; |
|
770 "real_0_less_divide_iff";"(0 < ?x / ?y) = (0 < ?x & 0 < ?y | ?x < 0 & ?y < 0)" |
|
771 "real_divide_less_0_iff";"(?x / ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)" |
|
772 "real_0_le_divide_iff"; |
|
773 "real_divide_le_0_iff"; |
|
774 "(?x / ?y <= 0) = ((?x <= 0 | ?y <= 0) & (0 <= ?x | 0 <= ?y))" |
|
775 "real_inverse_zero_iff"; |
|
776 "real_divide_eq_0_iff"; "(?x / ?y = 0) = (?x = 0 | ?y = 0)"(*!!!*) |
|
777 "real_divide_self_eq"; "?h ~= 0 ==> ?h / ?h = 1"(**) |
|
778 "real_minus_less_minus"; "(- ?y < - ?x) = (?x < ?y)" |
|
779 "real_mult_less_mono1_neg"; "[| ?i < ?j; ?k < 0 |] ==> ?j * ?k < ?i * ?k" |
|
780 "real_mult_less_mono2_neg"; |
|
781 "real_mult_le_mono1_neg"; |
|
782 "real_mult_le_mono2_neg"; |
|
783 "real_mult_less_cancel2"; |
|
784 "real_mult_le_cancel2"; |
|
785 "real_mult_less_cancel1"; |
|
786 "real_mult_le_cancel1"; |
|
787 "real_mult_eq_cancel1"; "(?k * ?m = ?k * ?n) = (?k = 0 | ?m = ?n)" |
|
788 "real_mult_eq_cancel2"; "(?m * ?k = ?n * ?k) = (?k = 0 | ?m = ?n)" |
|
789 "real_mult_div_cancel1"; (**)"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n" |
|
790 "real_mult_div_cancel_disj"; |
|
791 "?k * ?m / (?k * ?n) = (if ?k = 0 then 0 else ?m / ?n)" |
|
792 "pos_real_le_divide_eq"; |
|
793 "neg_real_le_divide_eq"; |
|
794 "pos_real_divide_le_eq"; |
|
795 "neg_real_divide_le_eq"; |
|
796 "pos_real_less_divide_eq"; |
|
797 "neg_real_less_divide_eq"; |
|
798 "pos_real_divide_less_eq"; |
|
799 "neg_real_divide_less_eq"; |
|
800 "real_eq_divide_eq"; (**)"?z ~= 0 ==> (?x = ?y / ?z) = (?x * ?z = ?y)" |
|
801 "real_divide_eq_eq"; (**)"?z ~= 0 ==> (?y / ?z = ?x) = (?y = ?x * ?z)" |
|
802 "real_divide_eq_cancel2"; "(?m / ?k = ?n / ?k) = (?k = 0 | ?m = ?n)" |
|
803 "real_divide_eq_cancel1"; "(?k / ?m = ?k / ?n) = (?k = 0 | ?m = ?n)" |
|
804 "real_inverse_less_iff"; |
|
805 "real_inverse_le_iff"; |
|
806 "real_divide_1"; (**)"?x / 1 = ?x" |
|
807 "real_divide_minus1"; (**)"?x / -1 = - ?x" |
|
808 "real_minus1_divide"; (**)"-1 / ?x = - (1 / ?x)" |
|
809 "real_lbound_gt_zero"; |
|
810 "[| 0 < ?d1.0; 0 < ?d2.0 |] ==> EX e. 0 < e & e < ?d1.0 & e < ?d2.0" |
|
811 "real_inverse_eq_iff"; "(inverse ?x = inverse ?y) = (?x = ?y)" |
|
812 "real_divide_eq_iff"; "(?z / ?x = ?z / ?y) = (?z = 0 | ?x = ?y)" |
|
813 "real_less_minus"; "(?x < - ?y) = (?y < - ?x)" |
|
814 "real_minus_less"; "(- ?x < ?y) = (- ?y < ?x)" |
|
815 "real_le_minus"; |
|
816 "real_minus_le"; "(- ?x <= ?y) = (- ?y <= ?x)" |
|
817 "real_equation_minus"; (**)"(?x = - ?y) = (?y = - ?x)" |
|
818 "real_minus_equation"; (**)"(- ?x = ?y) = (- ?y = ?x)" |
|
819 "real_add_minus_iff"; (**)"(?x + - ?a = 0) = (?x = ?a)" |
|
820 "real_minus_eq_cancel"; (**)"(- ?b = - ?a) = (?b = ?a)" |
|
821 "real_add_eq_0_iff"; (**)"(?x + ?y = 0) = (?y = - ?x)" |
|
822 "real_add_less_0_iff"; "(?x + ?y < 0) = (?y < - ?x)" |
|
823 "real_0_less_add_iff"; |
|
824 "real_add_le_0_iff"; |
|
825 "real_0_le_add_iff"; |
|
826 "real_0_less_diff_iff"; "(0 < ?x - ?y) = (?y < ?x)" |
|
827 "real_0_le_diff_iff"; |
|
828 "real_minus_diff_eq"; (**)"- (?x - ?y) = ?y - ?x" |
|
829 "real_less_half_sum"; "?x < ?y ==> ?x < (?x + ?y) / 2" |
|
830 "real_gt_half_sum"; |
|
831 "real_dense"; "?x < ?y ==> EX r. ?x < r & r < ?y" |
|
832 RealArith ///!!!///----------------------------------------------------------- |
|
833 RComplete.ML:qed ------------------------------------------------------------- |
|
834 "real_sum_of_halves"; (**)"?x / 2 + ?x / 2 = ?x" |
|
835 "real_sup_lemma1"; |
|
836 "real_sup_lemma2"; |
|
837 "posreal_complete"; |
|
838 "real_isLub_unique"; |
|
839 "real_order_restrict"; |
|
840 "posreals_complete"; |
|
841 "real_sup_lemma3"; |
|
842 "lemma_le_swap2"; |
|
843 "lemma_real_complete2b"; |
|
844 "reals_complete"; |
|
845 "real_of_nat_Suc_gt_zero"; |
|
846 "reals_Archimedean"; "0 < ?x ==> EX n. inverse (real (Suc n)) < ?x" |
|
847 "reals_Archimedean2"; |
|
848 RealAbs.ML:qed |
|
849 "abs_nat_number_of"; |
|
850 "abs (number_of ?v) = |
|
851 (if neg (number_of ?v) then number_of (bin_minus ?v) else number_of ?v)" |
|
852 "abs_split"; |
|
853 "abs_iff"; |
|
854 "abs_zero"; "abs 0 = 0" |
|
855 "abs_one"; |
|
856 "abs_eqI1"; |
|
857 "abs_eqI2"; |
|
858 "abs_minus_eqI2"; |
|
859 "abs_minus_eqI1"; |
|
860 "abs_ge_zero"; "0 <= abs ?x" |
|
861 "abs_idempotent"; "abs (abs ?x) = abs ?x" |
|
862 "abs_zero_iff"; "(abs ?x = 0) = (?x = 0)" |
|
863 "abs_ge_self"; "?x <= abs ?x" |
|
864 "abs_ge_minus_self"; |
|
865 "abs_mult"; "abs (?x * ?y) = abs ?x * abs ?y" |
|
866 "abs_inverse"; "abs (inverse ?x) = inverse (abs ?x)" |
|
867 "abs_mult_inverse"; |
|
868 "abs_triangle_ineq"; "abs (?x + ?y) <= abs ?x + abs ?y" |
|
869 "abs_triangle_ineq_four"; |
|
870 "abs_minus_cancel"; |
|
871 "abs_minus_add_cancel"; |
|
872 "abs_triangle_minus_ineq"; |
|
873 RealAbs.ML:qed_spec_mp |
|
874 "abs_add_less"; "[| abs ?x < ?r; abs ?y < ?s |] ==> abs (?x + ?y) < ?r + ?s" |
|
875 RealAbs.ML:qed |
|
876 "abs_add_minus_less"; |
|
877 "real_mult_0_less"; "(0 * ?x < ?r) = (0 < ?r)" |
|
878 "real_mult_less_trans"; |
|
879 "real_mult_le_less_trans"; |
|
880 "abs_mult_less"; |
|
881 "abs_mult_less2"; |
|
882 "abs_less_gt_zero"; |
|
883 "abs_minus_one"; "abs -1 = 1" |
|
884 "abs_disj"; "abs ?x = ?x | abs ?x = - ?x" |
|
885 "abs_interval_iff"; |
|
886 "abs_le_interval_iff"; |
|
887 "abs_add_pos_gt_zero"; |
|
888 "abs_add_one_gt_zero"; |
|
889 "abs_not_less_zero"; |
|
890 "abs_circle"; "abs ?h < abs ?y - abs ?x ==> abs (?x + ?h) < abs ?y" |
|
891 "abs_le_zero_iff"; |
|
892 "real_0_less_abs_iff"; |
|
893 "abs_real_of_nat_cancel"; |
|
894 "abs_add_one_not_less_self"; |
|
895 "abs_triangle_ineq_three"; "abs (?w + ?x + ?y) <= abs ?w + abs ?x + abs ?y" |
|
896 "abs_diff_less_imp_gt_zero"; |
|
897 "abs_diff_less_imp_gt_zero2"; |
|
898 "abs_diff_less_imp_gt_zero3"; |
|
899 "abs_diff_less_imp_gt_zero4"; |
|
900 "abs_triangle_ineq_minus_cancel"; |
|
901 "abs_sum_triangle_ineq"; |
|
902 "abs (?x + ?y + (- ?l + - ?m)) <= abs (?x + - ?l) + abs (?y + - ?m)" |
|
903 RealPow.ML:qed |
|
904 "realpow_zero"; "0 ^ Suc ?n = 0" |
|
905 RealPow.ML:qed_spec_mp |
|
906 "realpow_not_zero"; "?r ~= 0 ==> ?r ^ ?n ~= 0" |
|
907 "realpow_zero_zero"; "?r ^ ?n = 0 ==> ?r = 0" |
|
908 "realpow_inverse"; "inverse (?r ^ ?n) = inverse ?r ^ ?n" |
|
909 "realpow_abs"; "abs (?r ^ ?n) = abs ?r ^ ?n" |
|
910 "realpow_add"; (**)"?r ^ (?n + ?m) = ?r ^ ?n * ?r ^ ?m" |
|
911 "realpow_one"; (**)"?r ^ 1 = ?r" |
|
912 "realpow_two"; (**)"?r ^ Suc (Suc 0) = ?r * ?r" |
|
913 RealPow.ML:qed_spec_mp |
|
914 "realpow_gt_zero"; "0 < ?r ==> 0 < ?r ^ ?n" |
|
915 "realpow_ge_zero"; "0 <= ?r ==> 0 <= ?r ^ ?n" |
|
916 "realpow_le"; "0 <= ?x & ?x <= ?y ==> ?x ^ ?n <= ?y ^ ?n" |
|
917 "realpow_less"; |
|
918 RealPow.ML:qed |
|
919 "realpow_eq_one"; (**)"1 ^ ?n = 1" |
|
920 "abs_realpow_minus_one"; "abs (-1 ^ ?n) = 1" |
|
921 "realpow_mult"; (**)"(?r * ?s) ^ ?n = ?r ^ ?n * ?s ^ ?n" |
|
922 "realpow_two_le"; "0 <= ?r ^ Suc (Suc 0)" |
|
923 "abs_realpow_two"; |
|
924 "realpow_two_abs"; "abs ?x ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)" |
|
925 "realpow_two_gt_one"; |
|
926 RealPow.ML:qed_spec_mp |
|
927 "realpow_ge_one"; "1 < ?r ==> 1 <= ?r ^ ?n" |
|
928 RealPow.ML:qed |
|
929 "realpow_ge_one2"; |
|
930 "two_realpow_ge_one"; |
|
931 "two_realpow_gt"; |
|
932 "realpow_minus_one"; (**)"-1 ^ (2 * ?n) = 1" |
|
933 "realpow_minus_one_odd"; "-1 ^ Suc (2 * ?n) = - 1" |
|
934 "realpow_minus_one_even"; |
|
935 RealPow.ML:qed_spec_mp |
|
936 "realpow_Suc_less"; |
|
937 "realpow_Suc_le"; "0 <= ?r & ?r < 1 ==> ?r ^ Suc ?n <= ?r ^ ?n" |
|
938 RealPow.ML:qed |
|
939 "realpow_zero_le"; "0 <= 0 ^ ?n" |
|
940 RealPow.ML:qed_spec_mp |
|
941 "realpow_Suc_le2"; |
|
942 RealPow.ML:qed |
|
943 "realpow_Suc_le3"; |
|
944 RealPow.ML:qed_spec_mp |
|
945 "realpow_less_le"; "0 <= ?r & ?r < 1 & ?n < ?N ==> ?r ^ ?N <= ?r ^ ?n" |
|
946 RealPow.ML:qed |
|
947 "realpow_le_le"; "[| 0 <= ?r; ?r < 1; ?n <= ?N |] ==> ?r ^ ?N <= ?r ^ ?n" |
|
948 "realpow_Suc_le_self"; |
|
949 "realpow_Suc_less_one"; |
|
950 RealPow.ML:qed_spec_mp |
|
951 "realpow_le_Suc"; |
|
952 "realpow_less_Suc"; |
|
953 "realpow_le_Suc2"; |
|
954 "realpow_gt_ge"; |
|
955 "realpow_gt_ge2"; |
|
956 RealPow.ML:qed |
|
957 "realpow_ge_ge"; "[| 1 < ?r; ?n <= ?N |] ==> ?r ^ ?n <= ?r ^ ?N" |
|
958 "realpow_ge_ge2"; |
|
959 RealPow.ML:qed_spec_mp |
|
960 "realpow_Suc_ge_self"; |
|
961 "realpow_Suc_ge_self2"; |
|
962 RealPow.ML:qed |
|
963 "realpow_ge_self"; |
|
964 "realpow_ge_self2"; |
|
965 RealPow.ML:qed_spec_mp |
|
966 "realpow_minus_mult"; "0 < ?n ==> ?x ^ (?n - 1) * ?x = ?x ^ ?n" |
|
967 "realpow_two_mult_inverse"; |
|
968 "?r ~= 0 ==> ?r * inverse ?r ^ Suc (Suc 0) = inverse ?r" |
|
969 "realpow_two_minus"; "(- ?x) ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)" |
|
970 "realpow_two_diff"; |
|
971 "realpow_two_disj"; |
|
972 "realpow_diff"; |
|
973 "[| ?x ~= 0; ?m <= ?n |] ==> ?x ^ (?n - ?m) = ?x ^ ?n * inverse (?x ^ ?m)" |
|
974 "realpow_real_of_nat"; |
|
975 "realpow_real_of_nat_two_pos"; "0 < real (Suc (Suc 0) ^ ?n)" |
|
976 RealPow.ML:qed_spec_mp |
|
977 "realpow_increasing"; |
|
978 "realpow_Suc_cancel_eq"; |
|
979 "[| 0 <= ?x; 0 <= ?y; ?x ^ Suc ?n = ?y ^ Suc ?n |] ==> ?x = ?y" |
|
980 RealPow.ML:qed |
|
981 "realpow_eq_0_iff"; "(?x ^ ?n = 0) = (?x = 0 & 0 < ?n)" |
|
982 "zero_less_realpow_abs_iff"; |
|
983 "zero_le_realpow_abs"; |
|
984 "real_of_int_power"; "real ?x ^ ?n = real (?x ^ ?n)" |
|
985 "power_real_number_of"; "number_of ?v ^ ?n = real (number_of ?v ^ ?n)" |
|
986 Ring_and_Field ---///!!!///--------------------------------------------------- |
|
987 Complex_Numbers --///!!!///--------------------------------------------------- |
|
988 Real -------------///!!!///--------------------------------------------------- |
|
989 real_arith0.ML:qed ""; |
|
990 real_arith0.ML:qed ""; |
|
991 real_arith0.ML:qed ""; |
|
992 real_arith0.ML:qed ""; |
|
993 real_arith0.ML:qed ""; |
|
994 real_arith0.ML:qed ""; |
|
995 real_arith0.ML:qed ""; |
|
996 real_arith0.ML:qed ""; |
|
997 real_arith0.ML:qed ""; |
|
998 |
|
999 |
|
1000 |
|
1001 |
|
1002 |
|
1003 |
|
1004 |
|
1005 |