--- a/src/HOL/Rings.thy Fri Jun 19 07:53:33 2015 +0200
+++ b/src/HOL/Rings.thy Fri Jun 19 07:53:35 2015 +0200
@@ -630,6 +630,260 @@
class idom_divide = idom + semidom_divide
+class algebraic_semidom = semidom_divide
+begin
+
+lemma dvd_div_mult_self [simp]:
+ "a dvd b \<Longrightarrow> b div a * a = b"
+ by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
+
+lemma dvd_mult_div_cancel [simp]:
+ "a dvd b \<Longrightarrow> a * (b div a) = b"
+ using dvd_div_mult_self [of a b] by (simp add: ac_simps)
+
+lemma div_mult_swap:
+ assumes "c dvd b"
+ shows "a * (b div c) = (a * b) div c"
+proof (cases "c = 0")
+ case True then show ?thesis by simp
+next
+ case False from assms obtain d where "b = c * d" ..
+ moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
+ by simp
+ ultimately show ?thesis by (simp add: ac_simps)
+qed
+
+lemma dvd_div_mult:
+ assumes "c dvd b"
+ shows "b div c * a = (b * a) div c"
+ using assms div_mult_swap [of c b a] by (simp add: ac_simps)
+
+
+text \<open>Units: invertible elements in a ring\<close>
+
+abbreviation is_unit :: "'a \<Rightarrow> bool"
+where
+ "is_unit a \<equiv> a dvd 1"
+
+lemma not_is_unit_0 [simp]:
+ "\<not> is_unit 0"
+ by simp
+
+lemma unit_imp_dvd [dest]:
+ "is_unit b \<Longrightarrow> b dvd a"
+ by (rule dvd_trans [of _ 1]) simp_all
+
+lemma unit_dvdE:
+ assumes "is_unit a"
+ obtains c where "a \<noteq> 0" and "b = a * c"
+proof -
+ from assms have "a dvd b" by auto
+ then obtain c where "b = a * c" ..
+ moreover from assms have "a \<noteq> 0" by auto
+ ultimately show thesis using that by blast
+qed
+
+lemma dvd_unit_imp_unit:
+ "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
+ by (rule dvd_trans)
+
+lemma unit_div_1_unit [simp, intro]:
+ assumes "is_unit a"
+ shows "is_unit (1 div a)"
+proof -
+ from assms have "1 = 1 div a * a" by simp
+ then show "is_unit (1 div a)" by (rule dvdI)
+qed
+
+lemma is_unitE [elim?]:
+ assumes "is_unit a"
+ obtains b where "a \<noteq> 0" and "b \<noteq> 0"
+ and "is_unit b" and "1 div a = b" and "1 div b = a"
+ and "a * b = 1" and "c div a = c * b"
+proof (rule that)
+ def b \<equiv> "1 div a"
+ then show "1 div a = b" by simp
+ from b_def `is_unit a` show "is_unit b" by simp
+ from `is_unit a` and `is_unit b` show "a \<noteq> 0" and "b \<noteq> 0" by auto
+ from b_def `is_unit a` show "a * b = 1" by simp
+ then have "1 = a * b" ..
+ with b_def `b \<noteq> 0` show "1 div b = a" by simp
+ from `is_unit a` have "a dvd c" ..
+ then obtain d where "c = a * d" ..
+ with `a \<noteq> 0` `a * b = 1` show "c div a = c * b"
+ by (simp add: mult.assoc mult.left_commute [of a])
+qed
+
+lemma unit_prod [intro]:
+ "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
+ by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
+
+lemma unit_div [intro]:
+ "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
+ by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
+
+lemma mult_unit_dvd_iff:
+ assumes "is_unit b"
+ shows "a * b dvd c \<longleftrightarrow> a dvd c"
+proof
+ assume "a * b dvd c"
+ with assms show "a dvd c"
+ by (simp add: dvd_mult_left)
+next
+ assume "a dvd c"
+ then obtain k where "c = a * k" ..
+ with assms have "c = (a * b) * (1 div b * k)"
+ by (simp add: mult_ac)
+ then show "a * b dvd c" by (rule dvdI)
+qed
+
+lemma dvd_mult_unit_iff:
+ assumes "is_unit b"
+ shows "a dvd c * b \<longleftrightarrow> a dvd c"
+proof
+ assume "a dvd c * b"
+ with assms have "c * b dvd c * (b * (1 div b))"
+ by (subst mult_assoc [symmetric]) simp
+ also from `is_unit b` have "b * (1 div b) = 1" by (rule is_unitE) simp
+ finally have "c * b dvd c" by simp
+ with `a dvd c * b` show "a dvd c" by (rule dvd_trans)
+next
+ assume "a dvd c"
+ then show "a dvd c * b" by simp
+qed
+
+lemma div_unit_dvd_iff:
+ "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
+ by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
+
+lemma dvd_div_unit_iff:
+ "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
+ by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
+
+lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
+ dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>
+
+lemma unit_mult_div_div [simp]:
+ "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
+ by (erule is_unitE [of _ b]) simp
+
+lemma unit_div_mult_self [simp]:
+ "is_unit a \<Longrightarrow> b div a * a = b"
+ by (rule dvd_div_mult_self) auto
+
+lemma unit_div_1_div_1 [simp]:
+ "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
+ by (erule is_unitE) simp
+
+lemma unit_div_mult_swap:
+ "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
+ by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
+
+lemma unit_div_commute:
+ "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
+ using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
+
+lemma unit_eq_div1:
+ "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
+ by (auto elim: is_unitE)
+
+lemma unit_eq_div2:
+ "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
+ using unit_eq_div1 [of b c a] by auto
+
+lemma unit_mult_left_cancel:
+ assumes "is_unit a"
+ shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
+ using assms mult_cancel_left [of a b c] by auto
+
+lemma unit_mult_right_cancel:
+ "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
+ using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
+
+lemma unit_div_cancel:
+ assumes "is_unit a"
+ shows "b div a = c div a \<longleftrightarrow> b = c"
+proof -
+ from assms have "is_unit (1 div a)" by simp
+ then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
+ by (rule unit_mult_right_cancel)
+ with assms show ?thesis by simp
+qed
+
+
+text \<open>Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \<close>
+
+definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
+
+lemma associatedI:
+ "a dvd b \<Longrightarrow> b dvd a \<Longrightarrow> associated a b"
+ by (simp add: associated_def)
+
+lemma associatedD1:
+ "associated a b \<Longrightarrow> a dvd b"
+ by (simp add: associated_def)
+
+lemma associatedD2:
+ "associated a b \<Longrightarrow> b dvd a"
+ by (simp add: associated_def)
+
+lemma associated_refl [simp]:
+ "associated a a"
+ by (auto intro: associatedI)
+
+lemma associated_sym:
+ "associated b a \<longleftrightarrow> associated a b"
+ by (auto intro: associatedI dest: associatedD1 associatedD2)
+
+lemma associated_trans:
+ "associated a b \<Longrightarrow> associated b c \<Longrightarrow> associated a c"
+ by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2)
+
+lemma associated_0 [simp]:
+ "associated 0 b \<longleftrightarrow> b = 0"
+ "associated a 0 \<longleftrightarrow> a = 0"
+ by (auto dest: associatedD1 associatedD2)
+
+lemma associated_unit:
+ "associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
+ using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
+
+lemma is_unit_associatedI:
+ assumes "is_unit c" and "a = c * b"
+ shows "associated a b"
+proof (rule associatedI)
+ from `a = c * b` show "b dvd a" by auto
+ from `is_unit c` obtain d where "c * d = 1" by (rule is_unitE)
+ moreover from `a = c * b` have "d * a = d * (c * b)" by simp
+ ultimately have "b = a * d" by (simp add: ac_simps)
+ then show "a dvd b" ..
+qed
+
+lemma associated_is_unitE:
+ assumes "associated a b"
+ obtains c where "is_unit c" and "a = c * b"
+proof (cases "b = 0")
+ case True with assms have "is_unit 1" and "a = 1 * b" by simp_all
+ with that show thesis .
+next
+ case False
+ from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2)
+ then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE)
+ then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps)
+ with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp
+ then have "is_unit c" by auto
+ with `a = c * b` that show thesis by blast
+qed
+
+lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
+ dvd_div_unit_iff unit_div_mult_swap unit_div_commute
+ unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
+ unit_eq_div1 unit_eq_div2
+
+end
+
class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"