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