equal
deleted
inserted
replaced
763 by (simp add: real_divide_def zero_le_mult_iff, auto) |
763 by (simp add: real_divide_def zero_le_mult_iff, auto) |
764 |
764 |
765 lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" |
765 lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" |
766 by arith |
766 by arith |
767 |
767 |
768 lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)" |
768 lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)" |
769 by auto |
769 by auto |
770 |
770 |
771 lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)" |
771 lemma real_add_less_0_iff: "(x+y < (0::real)) = (y < -x)" |
772 by auto |
772 by auto |
773 |
773 |
774 lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)" |
774 lemma real_0_less_add_iff: "((0::real) < x+y) = (-x < y)" |
775 by auto |
775 by auto |
776 |
776 |
777 lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)" |
777 lemma real_add_le_0_iff: "(x+y \<le> (0::real)) = (y \<le> -x)" |
778 by auto |
778 by auto |
779 |
779 |
780 lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)" |
780 lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (-x \<le> y)" |
781 by auto |
781 by auto |
782 |
782 |
783 |
783 |
784 (** Simprules combining x-y and 0 (needed??) **) |
784 (** Simprules combining x-y and 0 (needed??) **) |
785 |
785 |
858 |
858 |
859 |
859 |
860 ML |
860 ML |
861 {* |
861 {* |
862 val real_0_le_divide_iff = thm"real_0_le_divide_iff"; |
862 val real_0_le_divide_iff = thm"real_0_le_divide_iff"; |
863 val real_add_minus_iff = thm"real_add_minus_iff"; |
|
864 val real_add_eq_0_iff = thm"real_add_eq_0_iff"; |
|
865 val real_add_less_0_iff = thm"real_add_less_0_iff"; |
|
866 val real_0_less_add_iff = thm"real_0_less_add_iff"; |
|
867 val real_add_le_0_iff = thm"real_add_le_0_iff"; |
|
868 val real_0_le_add_iff = thm"real_0_le_add_iff"; |
|
869 val real_0_less_diff_iff = thm"real_0_less_diff_iff"; |
863 val real_0_less_diff_iff = thm"real_0_less_diff_iff"; |
870 val real_0_le_diff_iff = thm"real_0_le_diff_iff"; |
864 val real_0_le_diff_iff = thm"real_0_le_diff_iff"; |
871 val real_lbound_gt_zero = thm"real_lbound_gt_zero"; |
865 val real_lbound_gt_zero = thm"real_lbound_gt_zero"; |
872 val real_less_half_sum = thm"real_less_half_sum"; |
866 val real_less_half_sum = thm"real_less_half_sum"; |
873 val real_gt_half_sum = thm"real_gt_half_sum"; |
867 val real_gt_half_sum = thm"real_gt_half_sum"; |