# HG changeset patch # User haftmann # Date 1434693215 -7200 # Node ID f16e4fb206525731f895ed9f2d8ff92dbfd84faa # Parent 0826b7025d07ee2cc09ad801598fb610d76bd353 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial diff -r 0826b7025d07 -r f16e4fb20652 CONTRIBUTORS --- a/CONTRIBUTORS Fri Jun 19 07:53:33 2015 +0200 +++ b/CONTRIBUTORS Fri Jun 19 07:53:35 2015 +0200 @@ -10,6 +10,10 @@ Generic partial division in rings as inverse operation of multiplication. +* Summer 2015: Manuel Eberl and Florian Haftmann, TUM + Type class hierarchy with common algebraic notions of + integral (semi)domains like units and associated elements. + Contributions to Isabelle2015 ----------------------------- diff -r 0826b7025d07 -r f16e4fb20652 NEWS --- a/NEWS Fri Jun 19 07:53:33 2015 +0200 +++ b/NEWS Fri Jun 19 07:53:35 2015 +0200 @@ -95,6 +95,12 @@ * Tightened specification of class semiring_no_zero_divisors. Slight INCOMPATIBILITY. +* Class algebraic_semidom introduced common algebraic notions of +integral (semi)domains like units and associated elements. Although +logically subsumed by fields, is is not a super class of these +in order not to burden fields with notions that are trivial there. +INCOMPATIBILITY. + * Former constants Fields.divide (_ / _) and Divides.div (_ div _) are logically unified to Rings.divide in syntactic type class Rings.divide, with infix syntax (_ div _). Infix syntax (_ / _) diff -r 0826b7025d07 -r f16e4fb20652 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Jun 19 07:53:33 2015 +0200 +++ b/src/HOL/Divides.thy Fri Jun 19 07:53:35 2015 +0200 @@ -22,7 +22,7 @@ and div_mult_mult1 [simp]: "c \ 0 \ (c * a) div (c * b) = a div b" begin -subclass semidom_divide +subclass algebraic_semidom proof fix b a assume "b \ 0" @@ -212,18 +212,6 @@ finally show ?thesis . qed -lemma dvd_div_mult_self [simp]: - "a dvd b \ (b div a) * a = b" - using mod_div_equality [of b a, symmetric] by simp - -lemma dvd_mult_div_cancel [simp]: - "a dvd b \ a * (b div a) = b" - using dvd_div_mult_self by (simp add: ac_simps) - -lemma dvd_div_mult: - "a dvd b \ (b div a) * c = (b * c) div a" - by (cases "a = 0") (auto elim!: dvdE simp add: mult.assoc) - lemma div_dvd_div [simp]: assumes "a dvd b" and "a dvd c" shows "b div a dvd c div a \ b dvd c" @@ -359,15 +347,6 @@ apply (simp add: no_zero_divisors) done -lemma div_mult_swap: - assumes "c dvd b" - shows "a * (b div c) = (a * b) div c" -proof - - from assms have "b div c * (a div 1) = b * a div (c * 1)" - by (simp only: div_mult_div_if_dvd one_dvd) - then show ?thesis by (simp add: mult.commute) -qed - lemma div_mult_mult2 [simp]: "c \ 0 \ (a * c) div (b * c) = a div b" by (drule div_mult_mult1) (simp add: mult.commute) @@ -1911,6 +1890,10 @@ end +lemma is_unit_int: + "is_unit (k::int) \ k = 1 \ k = - 1" + by auto + text{*Basic laws about division and remainder*} lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" diff -r 0826b7025d07 -r f16e4fb20652 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Fri Jun 19 07:53:33 2015 +0200 +++ b/src/HOL/Equiv_Relations.thy Fri Jun 19 07:53:35 2015 +0200 @@ -523,6 +523,20 @@ "equivp R \ R x y \ R y z \ R x z" by (erule equivpE, erule transpE) + +subsection \Prominent examples\ + +lemma equivp_associated: + "equivp associated" +proof (rule equivpI) + show "reflp associated" + by (rule reflpI) simp + show "symp associated" + by (rule sympI) (simp add: associated_sym) + show "transp associated" + by (rule transpI) (fact associated_trans) +qed + hide_const (open) proj end diff -r 0826b7025d07 -r f16e4fb20652 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Fri Jun 19 07:53:33 2015 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Fri Jun 19 07:53:35 2015 +0200 @@ -5,276 +5,6 @@ theory Euclidean_Algorithm imports Complex_Main begin - -context semidom_divide -begin - -lemma dvd_div_mult_self [simp]: - "a dvd b \ 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 \ 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 \Units: invertible elements in a ring\ - -abbreviation is_unit :: "'a \ bool" -where - "is_unit a \ a dvd 1" - -lemma not_is_unit_0 [simp]: - "\ is_unit 0" - by simp - -lemma unit_imp_dvd [dest]: - "is_unit b \ b dvd a" - by (rule dvd_trans [of _ 1]) simp_all - -lemma unit_dvdE: - assumes "is_unit a" - obtains c where "a \ 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 \ 0" by auto - ultimately show thesis using that by blast -qed - -lemma dvd_unit_imp_unit: - "a dvd b \ is_unit b \ 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 \ 0" and "b \ 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 \ "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 \ 0" and "b \ 0" by auto - from b_def `is_unit a` show "a * b = 1" by simp - then have "1 = a * b" .. - with b_def `b \ 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 \ 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 \ is_unit b \ is_unit (a * b)" - by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) - -lemma unit_div [intro]: - "is_unit a \ is_unit b \ 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 \ 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 \ 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 \ a div b dvd c \ a dvd c" - by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff) - -lemma dvd_div_unit_iff: - "is_unit b \ a dvd c div b \ 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 -- \FIXME consider fact collection\ - -lemma unit_mult_div_div [simp]: - "is_unit a \ b * (1 div a) = b div a" - by (erule is_unitE [of _ b]) simp - -lemma unit_div_mult_self [simp]: - "is_unit a \ b div a * a = b" - by (rule dvd_div_mult_self) auto - -lemma unit_div_1_div_1 [simp]: - "is_unit a \ 1 div (1 div a) = a" - by (erule is_unitE) simp - -lemma unit_div_mult_swap: - "is_unit c \ 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 \ (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 \ a div b = c \ a = c * b" - by (auto elim: is_unitE) - -lemma unit_eq_div2: - "is_unit b \ a = c div b \ 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 \ b = c" (is "?P \ ?Q") - using assms mult_cancel_left [of a b c] by auto - -lemma unit_mult_right_cancel: - "is_unit a \ b * a = c * a \ 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 \ b = c" -proof - - from assms have "is_unit (1 div a)" by simp - then have "b * (1 div a) = c * (1 div a) \ b = c" - by (rule unit_mult_right_cancel) - with assms show ?thesis by simp -qed - - -text \Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \ - -definition associated :: "'a \ 'a \ bool" -where - "associated a b \ a dvd b \ b dvd a" - -lemma associatedI: - "a dvd b \ b dvd a \ associated a b" - by (simp add: associated_def) - -lemma associatedD1: - "associated a b \ a dvd b" - by (simp add: associated_def) - -lemma associatedD2: - "associated a b \ 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 \ associated a b" - by (auto intro: associatedI dest: associatedD1 associatedD2) - -lemma associated_trans: - "associated a b \ associated b c \ associated a c" - by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2) - -lemma equivp_associated: - "equivp associated" -proof (rule equivpI) - show "reflp associated" - by (rule reflpI) simp - show "symp associated" - by (rule sympI) (simp add: associated_sym) - show "transp associated" - by (rule transpI) (fact associated_trans) -qed - -lemma associated_0 [simp]: - "associated 0 b \ b = 0" - "associated a 0 \ a = 0" - by (auto dest: associatedD1 associatedD2) - -lemma associated_unit: - "associated a b \ is_unit a \ 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 - -lemma is_unit_int: - "is_unit (k::int) \ k = 1 \ k = - 1" - by auto - text {* A Euclidean semiring is a semiring upon which the Euclidean algorithm can be diff -r 0826b7025d07 -r f16e4fb20652 src/HOL/Rings.thy --- 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 \ 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 \ 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 \Units: invertible elements in a ring\ + +abbreviation is_unit :: "'a \ bool" +where + "is_unit a \ a dvd 1" + +lemma not_is_unit_0 [simp]: + "\ is_unit 0" + by simp + +lemma unit_imp_dvd [dest]: + "is_unit b \ b dvd a" + by (rule dvd_trans [of _ 1]) simp_all + +lemma unit_dvdE: + assumes "is_unit a" + obtains c where "a \ 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 \ 0" by auto + ultimately show thesis using that by blast +qed + +lemma dvd_unit_imp_unit: + "a dvd b \ is_unit b \ 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 \ 0" and "b \ 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 \ "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 \ 0" and "b \ 0" by auto + from b_def `is_unit a` show "a * b = 1" by simp + then have "1 = a * b" .. + with b_def `b \ 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 \ 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 \ is_unit b \ is_unit (a * b)" + by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) + +lemma unit_div [intro]: + "is_unit a \ is_unit b \ 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 \ 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 \ 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 \ a div b dvd c \ a dvd c" + by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff) + +lemma dvd_div_unit_iff: + "is_unit b \ a dvd c div b \ 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 -- \FIXME consider fact collection\ + +lemma unit_mult_div_div [simp]: + "is_unit a \ b * (1 div a) = b div a" + by (erule is_unitE [of _ b]) simp + +lemma unit_div_mult_self [simp]: + "is_unit a \ b div a * a = b" + by (rule dvd_div_mult_self) auto + +lemma unit_div_1_div_1 [simp]: + "is_unit a \ 1 div (1 div a) = a" + by (erule is_unitE) simp + +lemma unit_div_mult_swap: + "is_unit c \ 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 \ (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 \ a div b = c \ a = c * b" + by (auto elim: is_unitE) + +lemma unit_eq_div2: + "is_unit b \ a = c div b \ 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 \ b = c" (is "?P \ ?Q") + using assms mult_cancel_left [of a b c] by auto + +lemma unit_mult_right_cancel: + "is_unit a \ b * a = c * a \ 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 \ b = c" +proof - + from assms have "is_unit (1 div a)" by simp + then have "b * (1 div a) = c * (1 div a) \ b = c" + by (rule unit_mult_right_cancel) + with assms show ?thesis by simp +qed + + +text \Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \ + +definition associated :: "'a \ 'a \ bool" +where + "associated a b \ a dvd b \ b dvd a" + +lemma associatedI: + "a dvd b \ b dvd a \ associated a b" + by (simp add: associated_def) + +lemma associatedD1: + "associated a b \ a dvd b" + by (simp add: associated_def) + +lemma associatedD2: + "associated a b \ 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 \ associated a b" + by (auto intro: associatedI dest: associatedD1 associatedD2) + +lemma associated_trans: + "associated a b \ associated b c \ associated a c" + by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2) + +lemma associated_0 [simp]: + "associated 0 b \ b = 0" + "associated a 0 \ a = 0" + by (auto dest: associatedD1 associatedD2) + +lemma associated_unit: + "associated a b \ is_unit a \ 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 \ b \ 0 \ c \ c * a \ c * b" assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ b * c"