summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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