1098 |
1098 |
1099 lemma sgn_less [simp]: |
1099 lemma sgn_less [simp]: |
1100 "sgn a < 0 \<longleftrightarrow> a < 0" |
1100 "sgn a < 0 \<longleftrightarrow> a < 0" |
1101 unfolding sgn_if by auto |
1101 unfolding sgn_if by auto |
1102 |
1102 |
1103 (* The int instances are proved, these generic ones are tedious to prove here. |
1103 lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k" |
1104 And not very useful, as int seems to be the only instance. |
1104 by (simp add: abs_if) |
1105 If needed, they should be proved later, when metis is available. |
1105 |
1106 lemma dvd_abs[simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k" |
1106 lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k" |
1107 proof- |
1107 by (simp add: abs_if) |
1108 have "\<forall>k.\<exists>ka. - (m * k) = m * ka" |
|
1109 by(simp add: mult_minus_right[symmetric] del: mult_minus_right) |
|
1110 moreover |
|
1111 have "\<forall>k.\<exists>ka. m * k = - (m * ka)" |
|
1112 by(auto intro!: minus_minus[symmetric] |
|
1113 simp add: mult_minus_right[symmetric] simp del: mult_minus_right) |
|
1114 ultimately show ?thesis by (auto simp: abs_if dvd_def) |
|
1115 qed |
|
1116 |
|
1117 lemma dvd_abs2[simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k" |
|
1118 proof- |
|
1119 have "\<forall>k.\<exists>ka. - (m * k) = m * ka" |
|
1120 by(simp add: mult_minus_right[symmetric] del: mult_minus_right) |
|
1121 moreover |
|
1122 have "\<forall>k.\<exists>ka. - (m * ka) = m * k" |
|
1123 by(auto intro!: minus_minus |
|
1124 simp add: mult_minus_right[symmetric] simp del: mult_minus_right) |
|
1125 ultimately show ?thesis |
|
1126 by (auto simp add:abs_if dvd_def minus_equation_iff[of k]) |
|
1127 qed |
|
1128 *) |
|
1129 |
1108 |
1130 end |
1109 end |
1131 |
1110 |
1132 class ordered_field = field + ordered_idom |
1111 class ordered_field = field + ordered_idom |
1133 |
1112 |