77 qed "real_divide_le_0_iff"; |
77 qed "real_divide_le_0_iff"; |
78 Addsimps [inst "x" "number_of ?w" real_divide_le_0_iff]; |
78 Addsimps [inst "x" "number_of ?w" real_divide_le_0_iff]; |
79 |
79 |
80 Goal "(inverse(x::real) = 0) = (x = 0)"; |
80 Goal "(inverse(x::real) = 0) = (x = 0)"; |
81 by (auto_tac (claset(), simpset() addsimps [INVERSE_ZERO])); |
81 by (auto_tac (claset(), simpset() addsimps [INVERSE_ZERO])); |
82 by (rtac ccontr 1); |
|
83 by (blast_tac (claset() addDs [real_inverse_not_zero]) 1); |
|
84 qed "real_inverse_zero_iff"; |
82 qed "real_inverse_zero_iff"; |
85 Addsimps [real_inverse_zero_iff]; |
83 Addsimps [real_inverse_zero_iff]; |
86 |
84 |
87 Goal "(x/y = 0) = (x=0 | y=(0::real))"; |
85 Goal "(x/y = 0) = (x=0 | y=(0::real))"; |
88 by (auto_tac (claset(), simpset() addsimps [real_divide_def])); |
86 by (auto_tac (claset(), simpset() addsimps [real_divide_def])); |
478 by (auto_tac (claset(), |
476 by (auto_tac (claset(), |
479 simpset() addsimps [REAL_DIVIDE_ZERO, real_divide_eq_eq, |
477 simpset() addsimps [REAL_DIVIDE_ZERO, real_divide_eq_eq, |
480 real_eq_divide_eq, real_mult_eq_cancel1])); |
478 real_eq_divide_eq, real_mult_eq_cancel1])); |
481 qed "real_divide_eq_cancel1"; |
479 qed "real_divide_eq_cancel1"; |
482 |
480 |
483 (*Moved from RealOrd.ML to use 0 *) |
|
484 Goal "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)"; |
481 Goal "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)"; |
485 by (auto_tac (claset() addIs [real_inverse_less_swap], simpset())); |
482 by (auto_tac (claset() addIs [real_inverse_less_swap], simpset())); |
486 by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1); |
|
487 by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1); |
|
488 by (auto_tac (claset() addIs [real_inverse_less_swap], |
|
489 simpset() delsimps [real_inverse_inverse] |
|
490 addsimps [real_inverse_gt_0])); |
|
491 qed "real_inverse_less_iff"; |
483 qed "real_inverse_less_iff"; |
492 |
484 |
493 Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))"; |
485 Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))"; |
494 by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, |
486 by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, |
495 real_inverse_less_iff]) 1); |
487 real_inverse_less_iff]) 1); |