src/HOL/Rings.thy
changeset 62366 95c6cf433c91
parent 62349 7c23469b5118
child 62376 85f38d5f8807
     1.1 --- a/src/HOL/Rings.thy	Thu Feb 18 17:52:53 2016 +0100
     1.2 +++ b/src/HOL/Rings.thy	Thu Feb 18 17:53:09 2016 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  section \<open>Rings\<close>
     1.5  
     1.6  theory Rings
     1.7 -imports Groups
     1.8 +imports Groups Set
     1.9  begin
    1.10  
    1.11  class semiring = ab_semigroup_add + semigroup_mult +
    1.12 @@ -155,6 +155,14 @@
    1.13    then show ?thesis ..
    1.14  qed
    1.15  
    1.16 +lemma subset_divisors_dvd:
    1.17 +  "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
    1.18 +  by (auto simp add: subset_iff intro: dvd_trans)
    1.19 +
    1.20 +lemma strict_subset_divisors_dvd:
    1.21 +  "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
    1.22 +  by (auto simp add: subset_iff intro: dvd_trans)
    1.23 +
    1.24  lemma one_dvd [simp]:
    1.25    "1 dvd a"
    1.26    by (auto intro!: dvdI)
    1.27 @@ -847,6 +855,10 @@
    1.28    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
    1.29    by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
    1.30  
    1.31 +lemma is_unit_mult_iff:
    1.32 +  "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
    1.33 +  by (auto dest: dvd_mult_left dvd_mult_right)
    1.34 +
    1.35  lemma unit_div [intro]:
    1.36    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
    1.37    by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)