src/HOL/Rings.thy
 changeset 60688 01488b559910 parent 60685 cb21b7022b00 child 60690 a9e45c9588c3
```     1.1 --- a/src/HOL/Rings.thy	Wed Jul 08 14:01:40 2015 +0200
1.2 +++ b/src/HOL/Rings.thy	Wed Jul 08 14:01:41 2015 +0200
1.3 @@ -636,6 +636,13 @@
1.4  class algebraic_semidom = semidom_divide
1.5  begin
1.6
1.7 +text \<open>
1.8 +  Class @{class algebraic_semidom} enriches a integral domain
1.9 +  by notions from algebra, like units in a ring.
1.10 +  It is a separate class to avoid spoiling fields with notions
1.11 +  which are degenerated there.
1.12 +\<close>
1.13 +
1.14  lemma dvd_div_mult_self [simp]:
1.15    "a dvd b \<Longrightarrow> b div a * a = b"
1.16    by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
1.17 @@ -834,84 +841,11 @@
1.18      by (rule dvd_div_mult2_eq)
1.19  qed
1.20
1.21 -
1.22 -text \<open>Associated elements in a ring --- an equivalence relation induced
1.23 -  by the quasi-order divisibility.\<close>
1.24 -
1.25 -definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.26 -where
1.27 -  "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
1.28 -
1.29 -lemma associatedI:
1.30 -  "a dvd b \<Longrightarrow> b dvd a \<Longrightarrow> associated a b"
1.31 -  by (simp add: associated_def)
1.32 -
1.33 -lemma associatedD1:
1.34 -  "associated a b \<Longrightarrow> a dvd b"
1.35 -  by (simp add: associated_def)
1.36 -
1.37 -lemma associatedD2:
1.38 -  "associated a b \<Longrightarrow> b dvd a"
1.39 -  by (simp add: associated_def)
1.40 -
1.41 -lemma associated_refl [simp]:
1.42 -  "associated a a"
1.43 -  by (auto intro: associatedI)
1.44 -
1.45 -lemma associated_sym:
1.46 -  "associated b a \<longleftrightarrow> associated a b"
1.47 -  by (auto intro: associatedI dest: associatedD1 associatedD2)
1.48 -
1.49 -lemma associated_trans:
1.50 -  "associated a b \<Longrightarrow> associated b c \<Longrightarrow> associated a c"
1.51 -  by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2)
1.52 -
1.53 -lemma associated_0 [simp]:
1.54 -  "associated 0 b \<longleftrightarrow> b = 0"
1.55 -  "associated a 0 \<longleftrightarrow> a = 0"
1.56 -  by (auto dest: associatedD1 associatedD2)
1.57 -
1.58 -lemma associated_unit:
1.59 -  "associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
1.60 -  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
1.61 -
1.62 -lemma is_unit_associatedI:
1.63 -  assumes "is_unit c" and "a = c * b"
1.64 -  shows "associated a b"
1.65 -proof (rule associatedI)
1.66 -  from `a = c * b` show "b dvd a" by auto
1.67 -  from `is_unit c` obtain d where "c * d = 1" by (rule is_unitE)
1.68 -  moreover from `a = c * b` have "d * a = d * (c * b)" by simp
1.69 -  ultimately have "b = a * d" by (simp add: ac_simps)
1.70 -  then show "a dvd b" ..
1.71 -qed
1.72 -
1.73 -lemma associated_is_unitE:
1.74 -  assumes "associated a b"
1.75 -  obtains c where "is_unit c" and "a = c * b"
1.76 -proof (cases "b = 0")
1.77 -  case True with assms have "is_unit 1" and "a = 1 * b" by simp_all
1.78 -  with that show thesis .
1.79 -next
1.80 -  case False
1.81 -  from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2)
1.82 -  then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE)
1.83 -  then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps)
1.84 -  with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp
1.85 -  then have "is_unit c" by auto
1.86 -  with `a = c * b` that show thesis by blast
1.87 -qed
1.88 -
1.89  lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
1.90    dvd_div_unit_iff unit_div_mult_swap unit_div_commute
1.91    unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
1.92    unit_eq_div1 unit_eq_div2
1.93
1.94 -end
1.95 -
1.96 -context algebraic_semidom
1.97 -begin
1.98 -
1.99  lemma is_unit_divide_mult_cancel_left:
1.100    assumes "a \<noteq> 0" and "is_unit b"
1.101    shows "a div (a * b) = 1 div b"
1.102 @@ -941,6 +875,16 @@
1.103    assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
1.104  begin
1.105
1.106 +text \<open>
1.107 +  Class @{class normalization_semidom} cultivates the idea that
1.108 +  each integral domain can be split into equivalence classes
1.109 +  whose representants are associated, i.e. divide each other.
1.110 +  @{const normalize} specifies a canonical representant for each equivalence
1.111 +  class.  The rationale behind this is that it is easier to reason about equality
1.112 +  than equivalences, hence we prefer to think about equality of normalized
1.113 +  values rather than associated elements.
1.114 +\<close>
1.115 +
1.116  lemma unit_factor_dvd [simp]:
1.117    "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
1.118    by (rule unit_imp_dvd) simp
1.119 @@ -1140,54 +1084,74 @@
1.120    then show ?thesis by simp
1.121  qed
1.122
1.123 -lemma associated_normalize_left [simp]:
1.124 -  "associated (normalize a) b \<longleftrightarrow> associated a b"
1.125 -  by (auto simp add: associated_def)
1.126 +text \<open>
1.127 +  We avoid an explicit definition of associated elements but prefer
1.128 +  explicit normalisation instead.  In theory we could define an abbreviation
1.129 +  like @{prop "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is
1.130 +  counterproductive without suggestive infix syntax, which we do not want
1.131 +  to sacrifice for this purpose here.
1.132 +\<close>
1.133
1.134 -lemma associated_normalize_right [simp]:
1.135 -  "associated a (normalize b) \<longleftrightarrow> associated a b"
1.136 -  by (auto simp add: associated_def)
1.137 -
1.138 -lemma associated_iff_normalize:
1.139 -  "associated a b \<longleftrightarrow> normalize a = normalize b" (is "?P \<longleftrightarrow> ?Q")
1.140 +lemma associatedI:
1.141 +  assumes "a dvd b" and "b dvd a"
1.142 +  shows "normalize a = normalize b"
1.143  proof (cases "a = 0 \<or> b = 0")
1.144 -  case True then show ?thesis by auto
1.145 +  case True with assms show ?thesis by auto
1.146  next
1.147    case False
1.148 -  show ?thesis
1.149 -  proof
1.150 -    assume ?P then show ?Q
1.151 -      by (rule associated_is_unitE) (simp add: normalize_mult is_unit_normalize)
1.152 +  from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
1.153 +  moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
1.154 +  ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps)
1.155 +  with False have "1 = c * d"
1.156 +    unfolding mult_cancel_left by simp
1.157 +  then have "is_unit c" and "is_unit d" by auto
1.158 +  with a b show ?thesis by (simp add: normalize_mult is_unit_normalize)
1.159 +qed
1.160 +
1.161 +lemma associatedD1:
1.162 +  "normalize a = normalize b \<Longrightarrow> a dvd b"
1.163 +  using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
1.164 +  by simp
1.165 +
1.166 +lemma associatedD2:
1.167 +  "normalize a = normalize b \<Longrightarrow> b dvd a"
1.168 +  using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
1.169 +  by simp
1.170 +
1.171 +lemma associated_unit:
1.172 +  "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
1.173 +  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
1.174 +
1.175 +lemma associated_iff_dvd:
1.176 +  "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" (is "?P \<longleftrightarrow> ?Q")
1.177 +proof
1.178 +  assume ?Q then show ?P by (auto intro!: associatedI)
1.179 +next
1.180 +  assume ?P
1.181 +  then have "unit_factor a * normalize a = unit_factor a * normalize b"
1.182 +    by simp
1.183 +  then have *: "normalize b * unit_factor a = a"
1.184 +    by (simp add: ac_simps)
1.185 +  show ?Q
1.186 +  proof (cases "a = 0 \<or> b = 0")
1.187 +    case True with \<open>?P\<close> show ?thesis by auto
1.188    next
1.189 -    from False have *: "is_unit (unit_factor a div unit_factor b)"
1.190 -      by auto
1.191 -    assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b"
1.192 -      by simp
1.193 -    then have "a = unit_factor a * (b div unit_factor b)"
1.194 -      by simp
1.195 -    with False have "a = (unit_factor a div unit_factor b) * b"
1.196 -      by (simp add: unit_div_commute unit_div_mult_swap [symmetric])
1.197 -    with * show ?P
1.198 -      by (rule is_unit_associatedI)
1.199 +    case False
1.200 +    then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
1.201 +      by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
1.202 +    with * show ?thesis by simp
1.203    qed
1.204  qed
1.205
1.206  lemma associated_eqI:
1.207 -  assumes "associated a b"
1.208 -  assumes "a \<noteq> 0 \<Longrightarrow> unit_factor a = 1" and "b \<noteq> 0 \<Longrightarrow> unit_factor b = 1"
1.209 +  assumes "a dvd b" and "b dvd a"
1.210 +  assumes "normalize a = a" and "normalize b = b"
1.211    shows "a = b"
1.212 -proof (cases "a = 0")
1.213 -  case True with assms show ?thesis by simp
1.214 -next
1.215 -  case False with assms have "b \<noteq> 0" by auto
1.216 -  with False assms have "unit_factor a = unit_factor b"
1.217 -    by simp
1.218 -  moreover from assms have "normalize a = normalize b"
1.219 -    by (simp add: associated_iff_normalize)
1.220 -  ultimately have "unit_factor a * normalize a = unit_factor b * normalize b"
1.221 -    by simp
1.222 -  then show ?thesis
1.223 -    by simp
1.224 +proof -
1.225 +  from assms have "normalize a = normalize b"
1.226 +    unfolding associated_iff_dvd by simp
1.227 +  with \<open>normalize a = a\<close> have "a = normalize b" by simp
1.228 +  with \<open>normalize b = b\<close> show "a = b" by simp
1.229  qed
1.230
1.231  end
```