1 (*WN060306 from isabelle-users:
2 put expressions involving plus and minus into a canonical form. Here is a possible set of
6 diff_def minus_add_distrib
8 ===========================================================================*)
11 cd ~/Isabelle2002/src/HOL/Real
12 grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml
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}
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
32 (**)"...theorem..." : first choice for one of the rule-sets
33 "...theorem..."(*??*): to be investigated
34 "...theorem... : just for documenting the contents
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"
53 "[| isUb (?R::?'a set) (?S::?'a set) (?x::?'a); (?y::?'a) : ?S |]
54 ==> ?y <= ?x" "isUbD2";
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"
65 "[| (?i::nat) : pnat; (?P::nat => bool) (Suc (0::nat));
66 !!j::nat. [| j : pnat; ?P j |] ==> ?P (Suc j) |] ==> ?P ?i"
68 "[| (?P::pnat => bool) (1::pnat); !!n::pnat. ?P n ==> ?P (pSuc n) |]
79 "pnat_add_commute"; "(?x::pnat) + (?y::pnat) = ?y + ?x"
90 "pnat_add_left_commute";
91 "pnat_add_left_cancel";
92 "pnat_add_right_cancel";
95 "pnat_less_not_refl2";
97 "Rep_pnat_not_less_one";
98 "Rep_pnat_gt_implies_not0";
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";
106 "pnat_not_add_less1";
107 "pnat_not_add_less2";
112 "pnat_less_add_eq_less";
117 "Rep_pnat_mult_1_right";
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";
124 "pnat_mult_left_commute";
127 "pnat_mult_less_mono2";
128 "pnat_mult_less_mono1";
129 "pnat_mult_less_cancel2";
130 "pnat_mult_less_cancel1";
141 "pnat_of_nat_less_iff";
143 PRat.ML:qed ------------------------------------------------------------------
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"
164 "prat_add_congruent2_lemma";
165 "prat_add_congruent2";
169 "prat_add_left_commute";
170 "pnat_mult_congruent2";
174 "prat_mult_left_commute";
180 "prat_mult_qinv_right";
183 "prat_qinv_left_ex1";
184 "prat_mult_inv_qinv";
185 "prat_as_inverse_ex";
187 "prat_add_mult_distrib";
188 "prat_add_mult_distrib2";
194 "prat_less_not_refl";
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";
205 "lemma_prat_less_linear";
208 "lemma1_qinv_prat_less";
209 "lemma2_qinv_prat_less";
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";
225 "prat_le_imp_less_or_eq";
226 "prat_less_or_eq_imp_le";
227 "prat_le_eq_less_or_eq";
229 "prat_le_less_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";
237 "prat_add_left_le2_mono1";
238 "prat_add_le2_mono1";
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";
256 "{x::prat. x < prat_of_pnat (Abs_pnat (Suc (0::nat)))}
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"
264 "empty_not_mem_preal";
266 "preal_psubset_empty";
267 "Rep_preal_psubset_empty";
270 "[| {} < (?A::prat set); ?A < UNIV;
271 ALL y::prat:?A. (ALL z::prat. z < y --> z : ?A) & Bex ?A (op < y) |]
282 "not_mem_Rep_preal_Ex";
283 "lemma_prat_less_set_mem_preal";
287 "preal_less_not_refl";
290 "preal_less_not_sym";
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";
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";
311 "preal_mult_left_commute";
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";
337 "preal_mem_mult_invD";
338 "lemma1_gleason9_34";
339 "lemma1b_gleason9_34";
340 "lemma_gleason9_34a";
342 "lemma1_gleason9_36";
343 "lemma2_gleason9_36";
345 "lemma_gleason9_36a";
346 "preal_mem_mult_invI";
348 "preal_mult_inv_right";
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";
360 "preal_le_imp_less_or_eq";
361 "preal_less_or_eq_imp_le";
368 "lemma_psubset_not_refl";
370 "subset_psubset_trans";
371 "subset_psubset_trans2";
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";
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";
422 "lemma_preal_rat_less";
423 "lemma_preal_rat_less2";
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 ---------------------------------------------------------------
433 "?x1.0 + ?y2.0 = ?x2.0 + ?y1.0 ==> ((?x1.0, ?y1.0), ?x2.0, ?y2.0) : realrel"
443 "real_minus_congruent";
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";
452 (%p1 p2. (%(x1, y1). (%(x2, y2). realrel `` {(x1 + x2, y1 + y2)}) p2) p1)"
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"
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";
482 (%(x2, y2). realrel `` {(x1 * x2 + y1 * y2, x1 * y2 + x2 * y1)})
485 "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) *
486 Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =
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"
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"
547 "real_of_preal (?z1.0 + ?z2.0) = real_of_preal ?z1.0 + real_of_preal ?z2.0"
548 "real_of_preal_mult";
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"
573 "[| ?R1.0 < ?R2.0 ==> ?P; ?R1.0 = ?R2.0 ==> ?P; ?R2.0 < ?R1.0 ==> ?P |]
576 "real_leD"; "~ ?w < ?z ==> ?z <= ?w"
579 "real_le_imp_less_or_eq";
580 "real_less_or_eq_imp_le";
582 "real_le_refl"; "?w <= ?w"
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)"
602 "real_diff_le_eq"; "(?x - ?y <= ?z) = (?x <= ?z + ?y)"
604 "real_diff_eq_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)"
605 "real_eq_diff_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)"
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"
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"
639 "real_add_less_mono";
640 "real_add_left_le_mono1";
643 "real_add_minus_positive_less_self"; "0 < ?r ==> ?u + - ?r < ?u"
644 "real_le_minus_iff"; "(- ?s <= - ?r) = (?r <= ?s)"
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";
654 "real_of_nat_one"; "real (Suc 0) = 1"
657 "real_of_nat_less_iff";
658 "real_of_nat_le_iff";
660 "real_of_nat_ge_zero";
662 "real_of_nat_inject";
663 RealOrd.ML:qed_spec_mp
666 "real_of_nat_zero_iff";
667 "real_of_nat_neg_int";
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";
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)})) =
701 {(preal_of_prat (prat_of_pnat (pnat_of_nat ?i)),
702 preal_of_prat (prat_of_pnat (pnat_of_nat ?j)))})"
706 "real_of_int_add"; "real ?x + real ?y = real (?x + ?y)"
709 "real_of_int_mult"; "real ?x * real ?y = real (?x * ?y)"
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"
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"
751 "(?i * ?u + ?m = ?j * ?u + ?n) = ((?i - ?j) * ?u + ?m = ?n)"
753 "real_less_add_iff1";
754 "real_less_add_iff2";
757 "real_mult_le_mono1";
758 "real_mult_le_mono2";
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)"
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";
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"
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"
839 "real_order_restrict";
843 "lemma_real_complete2b";
845 "real_of_nat_Suc_gt_zero";
846 "reals_Archimedean"; "0 < ?x ==> EX n. inverse (real (Suc n)) < ?x"
847 "reals_Archimedean2";
850 "abs (number_of ?v) =
851 (if neg (number_of ?v) then number_of (bin_minus ?v) else number_of ?v)"
854 "abs_zero"; "abs 0 = 0"
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"
865 "abs_mult"; "abs (?x * ?y) = abs ?x * abs ?y"
866 "abs_inverse"; "abs (inverse ?x) = inverse (abs ?x)"
868 "abs_triangle_ineq"; "abs (?x + ?y) <= abs ?x + abs ?y"
869 "abs_triangle_ineq_four";
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"
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";
883 "abs_minus_one"; "abs -1 = 1"
884 "abs_disj"; "abs ?x = ?x | abs ?x = - ?x"
886 "abs_le_interval_iff";
887 "abs_add_pos_gt_zero";
888 "abs_add_one_gt_zero";
890 "abs_circle"; "abs ?h < abs ?y - abs ?x ==> abs (?x + ?h) < abs ?y"
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)"
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"
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)"
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"
930 "two_realpow_ge_one";
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
937 "realpow_Suc_le"; "0 <= ?r & ?r < 1 ==> ?r ^ Suc ?n <= ?r ^ ?n"
939 "realpow_zero_le"; "0 <= 0 ^ ?n"
940 RealPow.ML:qed_spec_mp
944 RealPow.ML:qed_spec_mp
945 "realpow_less_le"; "0 <= ?r & ?r < 1 & ?n < ?N ==> ?r ^ ?N <= ?r ^ ?n"
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
957 "realpow_ge_ge"; "[| 1 < ?r; ?n <= ?N |] ==> ?r ^ ?n <= ?r ^ ?N"
959 RealPow.ML:qed_spec_mp
960 "realpow_Suc_ge_self";
961 "realpow_Suc_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)"
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"
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 "";