680 |
673 |
681 lemma one_le_inverse: |
674 lemma one_le_inverse: |
682 "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a" |
675 "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a" |
683 using le_imp_inverse_le [of a 1, unfolded inverse_1] . |
676 using le_imp_inverse_le [of a 1, unfolded inverse_1] . |
684 |
677 |
685 lemma pos_le_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> b / c \<longleftrightarrow> a * c \<le> b" |
678 lemma pos_le_divide_eq [field_simps]: |
686 proof - |
679 assumes "0 < c" |
687 assume less: "0<c" |
680 shows "a \<le> b / c \<longleftrightarrow> a * c \<le> b" |
688 hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)" |
681 proof - |
689 by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq) |
682 from assms have "a \<le> b / c \<longleftrightarrow> a * c \<le> (b / c) * c" |
690 also have "... = (a*c \<le> b)" |
683 using mult_le_cancel_right [of a c "b * inverse c"] by (auto simp add: field_simps) |
691 by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult.assoc) |
684 also have "... \<longleftrightarrow> a * c \<le> b" |
|
685 by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) |
692 finally show ?thesis . |
686 finally show ?thesis . |
693 qed |
687 qed |
694 |
688 |
695 lemma neg_le_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le> b / c \<longleftrightarrow> b \<le> a * c" |
689 lemma pos_less_divide_eq [field_simps]: |
696 proof - |
690 assumes "0 < c" |
697 assume less: "c<0" |
691 shows "a < b / c \<longleftrightarrow> a * c < b" |
698 hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)" |
692 proof - |
699 by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq) |
693 from assms have "a < b / c \<longleftrightarrow> a * c < (b / c) * c" |
700 also have "... = (b \<le> a*c)" |
694 using mult_less_cancel_right [of a c "b / c"] by auto |
701 by (simp add: less_imp_not_eq [OF less] divide_inverse mult.assoc) |
695 also have "... = (a*c < b)" |
|
696 by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) |
702 finally show ?thesis . |
697 finally show ?thesis . |
703 qed |
698 qed |
704 |
699 |
705 lemma pos_less_divide_eq [field_simps]: "0 < c \<Longrightarrow> a < b / c \<longleftrightarrow> a * c < b" |
700 lemma neg_less_divide_eq [field_simps]: |
706 proof - |
701 assumes "c < 0" |
707 assume less: "0<c" |
702 shows "a < b / c \<longleftrightarrow> b < a * c" |
708 hence "(a < b/c) = (a*c < (b/c)*c)" |
703 proof - |
709 by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq) |
704 from assms have "a < b / c \<longleftrightarrow> (b / c) * c < a * c" |
710 also have "... = (a*c < b)" |
705 using mult_less_cancel_right [of "b / c" c a] by auto |
711 by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult.assoc) |
706 also have "... \<longleftrightarrow> b < a * c" |
|
707 by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) |
712 finally show ?thesis . |
708 finally show ?thesis . |
713 qed |
709 qed |
714 |
710 |
715 lemma neg_less_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a < b / c \<longleftrightarrow> b < a * c" |
711 lemma neg_le_divide_eq [field_simps]: |
716 proof - |
712 assumes "c < 0" |
717 assume less: "c<0" |
713 shows "a \<le> b / c \<longleftrightarrow> b \<le> a * c" |
718 hence "(a < b/c) = ((b/c)*c < a*c)" |
714 proof - |
719 by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq) |
715 from assms have "a \<le> b / c \<longleftrightarrow> (b / c) * c \<le> a * c" |
720 also have "... = (b < a*c)" |
716 using mult_le_cancel_right [of "b * inverse c" c a] by (auto simp add: field_simps) |
721 by (simp add: less_imp_not_eq [OF less] divide_inverse mult.assoc) |
717 also have "... \<longleftrightarrow> b \<le> a * c" |
|
718 by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) |
722 finally show ?thesis . |
719 finally show ?thesis . |
723 qed |
720 qed |
724 |
721 |
725 lemma pos_divide_less_eq [field_simps]: "0 < c \<Longrightarrow> b / c < a \<longleftrightarrow> b < a * c" |
722 lemma pos_divide_le_eq [field_simps]: |
726 proof - |
723 assumes "0 < c" |
727 assume less: "0<c" |
724 shows "b / c \<le> a \<longleftrightarrow> b \<le> a * c" |
728 hence "(b/c < a) = ((b/c)*c < a*c)" |
725 proof - |
729 by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq) |
726 from assms have "b / c \<le> a \<longleftrightarrow> (b / c) * c \<le> a * c" |
730 also have "... = (b < a*c)" |
727 using mult_le_cancel_right [of "b / c" c a] by auto |
731 by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult.assoc) |
728 also have "... \<longleftrightarrow> b \<le> a * c" |
|
729 by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) |
732 finally show ?thesis . |
730 finally show ?thesis . |
733 qed |
731 qed |
734 |
732 |
735 lemma neg_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow> b / c < a \<longleftrightarrow> a * c < b" |
733 lemma pos_divide_less_eq [field_simps]: |
736 proof - |
734 assumes "0 < c" |
737 assume less: "c<0" |
735 shows "b / c < a \<longleftrightarrow> b < a * c" |
738 hence "(b/c < a) = (a*c < (b/c)*c)" |
736 proof - |
739 by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq) |
737 from assms have "b / c < a \<longleftrightarrow> (b / c) * c < a * c" |
740 also have "... = (a*c < b)" |
738 using mult_less_cancel_right [of "b / c" c a] by auto |
741 by (simp add: less_imp_not_eq [OF less] divide_inverse mult.assoc) |
739 also have "... \<longleftrightarrow> b < a * c" |
|
740 by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) |
742 finally show ?thesis . |
741 finally show ?thesis . |
743 qed |
742 qed |
744 |
743 |
745 lemma pos_divide_le_eq [field_simps]: "0 < c \<Longrightarrow> b / c \<le> a \<longleftrightarrow> b \<le> a * c" |
744 lemma neg_divide_le_eq [field_simps]: |
746 proof - |
745 assumes "c < 0" |
747 assume less: "0<c" |
746 shows "b / c \<le> a \<longleftrightarrow> a * c \<le> b" |
748 hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)" |
747 proof - |
749 by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq) |
748 from assms have "b / c \<le> a \<longleftrightarrow> a * c \<le> (b / c) * c" |
750 also have "... = (b \<le> a*c)" |
749 using mult_le_cancel_right [of a c "b / c"] by auto |
751 by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult.assoc) |
750 also have "... \<longleftrightarrow> a * c \<le> b" |
|
751 by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) |
752 finally show ?thesis . |
752 finally show ?thesis . |
753 qed |
753 qed |
754 |
754 |
755 lemma neg_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow> b / c \<le> a \<longleftrightarrow> a * c \<le> b" |
755 lemma neg_divide_less_eq [field_simps]: |
756 proof - |
756 assumes "c < 0" |
757 assume less: "c<0" |
757 shows "b / c < a \<longleftrightarrow> a * c < b" |
758 hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)" |
758 proof - |
759 by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq) |
759 from assms have "b / c < a \<longleftrightarrow> a * c < b / c * c" |
760 also have "... = (a*c \<le> b)" |
760 using mult_less_cancel_right [of a c "b / c"] by auto |
761 by (simp add: less_imp_not_eq [OF less] divide_inverse mult.assoc) |
761 also have "... \<longleftrightarrow> a * c < b" |
|
762 by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) |
762 finally show ?thesis . |
763 finally show ?thesis . |
763 qed |
764 qed |
764 |
765 |
765 text{* The following @{text field_simps} rules are necessary, as minus is always moved atop of |
766 text{* The following @{text field_simps} rules are necessary, as minus is always moved atop of |
766 division but we want to get rid of division. *} |
767 division but we want to get rid of division. *} |