1(* Title: ZF/ex/Ring.thy 2 3*) 4 5section \<open>Rings\<close> 6 7theory Ring imports Group begin 8 9no_notation 10 cadd (infixl "\<oplus>" 65) and 11 cmult (infixl "\<otimes>" 70) 12 13(*First, we must simulate a record declaration: 14record ring = monoid + 15 add :: "[i, i] => i" (infixl "\<oplus>\<index>" 65) 16 zero :: i ("\<zero>\<index>") 17*) 18 19definition 20 add_field :: "i => i" where 21 "add_field(M) = fst(snd(snd(snd(M))))" 22 23definition 24 ring_add :: "[i, i, i] => i" (infixl "\<oplus>\<index>" 65) where 25 "ring_add(M,x,y) = add_field(M) ` <x,y>" 26 27definition 28 zero :: "i => i" ("\<zero>\<index>") where 29 "zero(M) = fst(snd(snd(snd(snd(M)))))" 30 31 32lemma add_field_eq [simp]: "add_field(<C,M,I,A,z>) = A" 33 by (simp add: add_field_def) 34 35lemma add_eq [simp]: "ring_add(<C,M,I,A,z>, x, y) = A ` <x,y>" 36 by (simp add: ring_add_def) 37 38lemma zero_eq [simp]: "zero(<C,M,I,A,Z,z>) = Z" 39 by (simp add: zero_def) 40 41 42text \<open>Derived operations.\<close> 43 44definition 45 a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80) where 46 "a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)" 47 48definition 49 minus :: "[i,i,i] => i" ("(_ \<ominus>\<index> _)" [65,66] 65) where 50 "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)" 51 52locale abelian_monoid = fixes G (structure) 53 assumes a_comm_monoid: 54 "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)" 55 56text \<open> 57 The following definition is redundant but simple to use. 58\<close> 59 60locale abelian_group = abelian_monoid + 61 assumes a_comm_group: 62 "comm_group (<carrier(G), add_field(G), zero(G), 0>)" 63 64locale ring = abelian_group R + monoid R for R (structure) + 65 assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk> 66 \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z" 67 and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk> 68 \<Longrightarrow> z \<cdot> (x \<oplus> y) = z \<cdot> x \<oplus> z \<cdot> y" 69 70locale cring = ring + comm_monoid R 71 72locale "domain" = cring + 73 assumes one_not_zero [simp]: "\<one> \<noteq> \<zero>" 74 and integral: "\<lbrakk>a \<cdot> b = \<zero>; a \<in> carrier(R); b \<in> carrier(R)\<rbrakk> \<Longrightarrow> 75 a = \<zero> | b = \<zero>" 76 77 78subsection \<open>Basic Properties\<close> 79 80lemma (in abelian_monoid) a_monoid: 81 "monoid (<carrier(G), add_field(G), zero(G), 0>)" 82apply (insert a_comm_monoid) 83apply (simp add: comm_monoid_def) 84done 85 86lemma (in abelian_group) a_group: 87 "group (<carrier(G), add_field(G), zero(G), 0>)" 88apply (insert a_comm_group) 89apply (simp add: comm_group_def group_def) 90done 91 92 93lemma (in abelian_monoid) l_zero [simp]: 94 "x \<in> carrier(G) \<Longrightarrow> \<zero> \<oplus> x = x" 95apply (insert monoid.l_one [OF a_monoid]) 96apply (simp add: ring_add_def) 97done 98 99lemma (in abelian_monoid) zero_closed [intro, simp]: 100 "\<zero> \<in> carrier(G)" 101by (rule monoid.one_closed [OF a_monoid, simplified]) 102 103lemma (in abelian_group) a_inv_closed [intro, simp]: 104 "x \<in> carrier(G) \<Longrightarrow> \<ominus> x \<in> carrier(G)" 105by (simp add: a_inv_def group.inv_closed [OF a_group, simplified]) 106 107lemma (in abelian_monoid) a_closed [intro, simp]: 108 "[| x \<in> carrier(G); y \<in> carrier(G) |] ==> x \<oplus> y \<in> carrier(G)" 109by (rule monoid.m_closed [OF a_monoid, 110 simplified, simplified ring_add_def [symmetric]]) 111 112lemma (in abelian_group) minus_closed [intro, simp]: 113 "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<ominus> y \<in> carrier(G)" 114by (simp add: minus_def) 115 116lemma (in abelian_group) a_l_cancel [simp]: 117 "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 118 \<Longrightarrow> (x \<oplus> y = x \<oplus> z) \<longleftrightarrow> (y = z)" 119by (rule group.l_cancel [OF a_group, 120 simplified, simplified ring_add_def [symmetric]]) 121 122lemma (in abelian_group) a_r_cancel [simp]: 123 "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 124 \<Longrightarrow> (y \<oplus> x = z \<oplus> x) \<longleftrightarrow> (y = z)" 125by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]]) 126 127lemma (in abelian_monoid) a_assoc: 128 "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 129 \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" 130by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]]) 131 132lemma (in abelian_group) l_neg: 133 "x \<in> carrier(G) \<Longrightarrow> \<ominus> x \<oplus> x = \<zero>" 134by (simp add: a_inv_def 135 group.l_inv [OF a_group, simplified, simplified ring_add_def [symmetric]]) 136 137lemma (in abelian_monoid) a_comm: 138 "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x" 139by (rule comm_monoid.m_comm [OF a_comm_monoid, 140 simplified, simplified ring_add_def [symmetric]]) 141 142lemma (in abelian_monoid) a_lcomm: 143 "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 144 \<Longrightarrow> x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)" 145by (rule comm_monoid.m_lcomm [OF a_comm_monoid, 146 simplified, simplified ring_add_def [symmetric]]) 147 148lemma (in abelian_monoid) r_zero [simp]: 149 "x \<in> carrier(G) \<Longrightarrow> x \<oplus> \<zero> = x" 150 using monoid.r_one [OF a_monoid] 151 by (simp add: ring_add_def [symmetric]) 152 153lemma (in abelian_group) r_neg: 154 "x \<in> carrier(G) \<Longrightarrow> x \<oplus> (\<ominus> x) = \<zero>" 155 using group.r_inv [OF a_group] 156 by (simp add: a_inv_def ring_add_def [symmetric]) 157 158lemma (in abelian_group) minus_zero [simp]: 159 "\<ominus> \<zero> = \<zero>" 160 by (simp add: a_inv_def 161 group.inv_one [OF a_group, simplified ]) 162 163lemma (in abelian_group) minus_minus [simp]: 164 "x \<in> carrier(G) \<Longrightarrow> \<ominus> (\<ominus> x) = x" 165 using group.inv_inv [OF a_group, simplified] 166 by (simp add: a_inv_def) 167 168lemma (in abelian_group) minus_add: 169 "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y" 170 using comm_group.inv_mult [OF a_comm_group] 171 by (simp add: a_inv_def ring_add_def [symmetric]) 172 173lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm 174 175text \<open> 176 The following proofs are from Jacobson, Basic Algebra I, pp.~88--89 177\<close> 178 179context ring 180begin 181 182lemma l_null [simp]: "x \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>" 183proof - 184 assume R: "x \<in> carrier(R)" 185 then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x" 186 by (blast intro: l_distr [THEN sym]) 187 also from R have "... = \<zero> \<cdot> x \<oplus> \<zero>" by simp 188 finally have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = \<zero> \<cdot> x \<oplus> \<zero>" . 189 with R show ?thesis by (simp del: r_zero) 190qed 191 192lemma r_null [simp]: "x \<in> carrier(R) \<Longrightarrow> x \<cdot> \<zero> = \<zero>" 193proof - 194 assume R: "x \<in> carrier(R)" 195 then have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> (\<zero> \<oplus> \<zero>)" 196 by (simp add: r_distr del: l_zero r_zero) 197 also from R have "... = x \<cdot> \<zero> \<oplus> \<zero>" by simp 198 finally have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> \<zero> \<oplus> \<zero>" . 199 with R show ?thesis by (simp del: r_zero) 200qed 201 202lemma l_minus: 203 "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> \<ominus> x \<cdot> y = \<ominus> (x \<cdot> y)" 204proof - 205 assume R: "x \<in> carrier(R)" "y \<in> carrier(R)" 206 then have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = (\<ominus> x \<oplus> x) \<cdot> y" by (simp add: l_distr) 207 also from R have "... = \<zero>" by (simp add: l_neg) 208 finally have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = \<zero>" . 209 with R have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp 210 with R show ?thesis by (simp add: a_assoc r_neg) 211qed 212 213lemma r_minus: 214 "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<cdot> \<ominus> y = \<ominus> (x \<cdot> y)" 215proof - 216 assume R: "x \<in> carrier(R)" "y \<in> carrier(R)" 217 then have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = x \<cdot> (\<ominus> y \<oplus> y)" by (simp add: r_distr) 218 also from R have "... = \<zero>" by (simp add: l_neg) 219 finally have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = \<zero>" . 220 with R have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp 221 with R show ?thesis by (simp add: a_assoc r_neg) 222qed 223 224lemma minus_eq: 225 "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y = x \<oplus> \<ominus> y" 226 by (simp only: minus_def) 227 228end 229 230 231subsection \<open>Morphisms\<close> 232 233definition 234 ring_hom :: "[i,i] => i" where 235 "ring_hom(R,S) == 236 {h \<in> carrier(R) -> carrier(S). 237 (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) \<longrightarrow> 238 h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) & 239 h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)) & 240 h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}" 241 242lemma ring_hom_memI: 243 assumes hom_type: "h \<in> carrier(R) \<rightarrow> carrier(S)" 244 and hom_mult: "\<And>x y. \<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> 245 h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)" 246 and hom_add: "\<And>x y. \<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> 247 h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)" 248 and hom_one: "h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>" 249 shows "h \<in> ring_hom(R,S)" 250by (auto simp add: ring_hom_def assms) 251 252lemma ring_hom_closed: 253 "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(S)" 254by (auto simp add: ring_hom_def) 255 256lemma ring_hom_mult: 257 "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> 258 \<Longrightarrow> h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)" 259by (simp add: ring_hom_def) 260 261lemma ring_hom_add: 262 "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> 263 \<Longrightarrow> h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)" 264by (simp add: ring_hom_def) 265 266lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>" 267by (simp add: ring_hom_def) 268 269locale ring_hom_cring = R: cring R + S: cring S 270 for R (structure) and S (structure) and h + 271 assumes homh [simp, intro]: "h \<in> ring_hom(R,S)" 272 notes hom_closed [simp, intro] = ring_hom_closed [OF homh] 273 and hom_mult [simp] = ring_hom_mult [OF homh] 274 and hom_add [simp] = ring_hom_add [OF homh] 275 and hom_one [simp] = ring_hom_one [OF homh] 276 277lemma (in ring_hom_cring) hom_zero [simp]: 278 "h ` \<zero>\<^bsub>R\<^esub> = \<zero>\<^bsub>S\<^esub>" 279proof - 280 have "h ` \<zero>\<^bsub>R\<^esub> \<oplus>\<^bsub>S\<^esub> h ` \<zero> = h ` \<zero>\<^bsub>R\<^esub> \<oplus>\<^bsub>S\<^esub> \<zero>\<^bsub>S\<^esub>" 281 by (simp add: hom_add [symmetric] del: hom_add) 282 then show ?thesis by (simp del: S.r_zero) 283qed 284 285lemma (in ring_hom_cring) hom_a_inv [simp]: 286 "x \<in> carrier(R) \<Longrightarrow> h ` (\<ominus>\<^bsub>R\<^esub> x) = \<ominus>\<^bsub>S\<^esub> h ` x" 287proof - 288 assume R: "x \<in> carrier(R)" 289 then have "h ` x \<oplus>\<^bsub>S\<^esub> h ` (\<ominus> x) = h ` x \<oplus>\<^bsub>S\<^esub> (\<ominus>\<^bsub>S\<^esub> (h ` x))" 290 by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add) 291 with R show ?thesis by simp 292qed 293 294lemma (in ring) id_ring_hom [simp]: "id(carrier(R)) \<in> ring_hom(R,R)" 295apply (rule ring_hom_memI) 296apply (auto simp add: id_type) 297done 298 299end 300