1(* Title: HOL/Algebra/Ring.thy 2 Author: Clemens Ballarin, started 9 December 1996 3 4With contributions by Martin Baillon. 5*) 6 7theory Ring 8imports FiniteProduct 9begin 10 11section \<open>The Algebraic Hierarchy of Rings\<close> 12 13subsection \<open>Abelian Groups\<close> 14 15record 'a ring = "'a monoid" + 16 zero :: 'a ("\<zero>\<index>") 17 add :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<oplus>\<index>" 65) 18 19abbreviation 20 add_monoid :: "('a, 'm) ring_scheme \<Rightarrow> ('a, 'm) monoid_scheme" 21 where "add_monoid R \<equiv> \<lparr> carrier = carrier R, mult = add R, one = zero R, \<dots> = (undefined :: 'm) \<rparr>" 22 23text \<open>Derived operations.\<close> 24 25definition 26 a_inv :: "[('a, 'm) ring_scheme, 'a ] \<Rightarrow> 'a" ("\<ominus>\<index> _" [81] 80) 27 where "a_inv R = m_inv (add_monoid R)" 28 29definition 30 a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" ("(_ \<ominus>\<index> _)" [65,66] 65) 31 where "x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)" 32 33definition 34 add_pow :: "[_, ('b :: semiring_1), 'a] \<Rightarrow> 'a" ("[_] \<cdot>\<index> _" [81, 81] 80) 35 where "add_pow R k a = pow (add_monoid R) a k" 36 37locale abelian_monoid = 38 fixes G (structure) 39 assumes a_comm_monoid: 40 "comm_monoid (add_monoid G)" 41 42definition 43 finsum :: "[('b, 'm) ring_scheme, 'a \<Rightarrow> 'b, 'a set] \<Rightarrow> 'b" where 44 "finsum G = finprod (add_monoid G)" 45 46syntax 47 "_finsum" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" 48 ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10) 49translations 50 "\<Oplus>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finsum G (\<lambda>i. b) A" 51 \<comment> \<open>Beware of argument permutation!\<close> 52 53 54locale abelian_group = abelian_monoid + 55 assumes a_comm_group: 56 "comm_group (add_monoid G)" 57 58 59subsection \<open>Basic Properties\<close> 60 61lemma abelian_monoidI: 62 fixes R (structure) 63 assumes "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier R" 64 and "\<zero> \<in> carrier R" 65 and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" 66 and "\<And>x. x \<in> carrier R \<Longrightarrow> \<zero> \<oplus> x = x" 67 and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x" 68 shows "abelian_monoid R" 69 by (auto intro!: abelian_monoid.intro comm_monoidI intro: assms) 70 71lemma abelian_monoidE: 72 fixes R (structure) 73 assumes "abelian_monoid R" 74 shows "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier R" 75 and "\<zero> \<in> carrier R" 76 and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" 77 and "\<And>x. x \<in> carrier R \<Longrightarrow> \<zero> \<oplus> x = x" 78 and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x" 79 using assms unfolding abelian_monoid_def comm_monoid_def comm_monoid_axioms_def monoid_def by auto 80 81lemma abelian_groupI: 82 fixes R (structure) 83 assumes "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier R" 84 and "\<zero> \<in> carrier R" 85 and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" 86 and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x" 87 and "\<And>x. x \<in> carrier R \<Longrightarrow> \<zero> \<oplus> x = x" 88 and "\<And>x. x \<in> carrier R \<Longrightarrow> \<exists>y \<in> carrier R. y \<oplus> x = \<zero>" 89 shows "abelian_group R" 90 by (auto intro!: abelian_group.intro abelian_monoidI 91 abelian_group_axioms.intro comm_monoidI comm_groupI 92 intro: assms) 93 94lemma abelian_groupE: 95 fixes R (structure) 96 assumes "abelian_group R" 97 shows "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y \<in> carrier R" 98 and "\<zero> \<in> carrier R" 99 and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" 100 and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x" 101 and "\<And>x. x \<in> carrier R \<Longrightarrow> \<zero> \<oplus> x = x" 102 and "\<And>x. x \<in> carrier R \<Longrightarrow> \<exists>y \<in> carrier R. y \<oplus> x = \<zero>" 103 using abelian_group.a_comm_group assms comm_groupE by fastforce+ 104 105lemma (in abelian_monoid) a_monoid: 106 "monoid (add_monoid G)" 107by (rule comm_monoid.axioms, rule a_comm_monoid) 108 109lemma (in abelian_group) a_group: 110 "group (add_monoid G)" 111 by (simp add: group_def a_monoid) 112 (simp add: comm_group.axioms group.axioms a_comm_group) 113 114lemmas monoid_record_simps = partial_object.simps monoid.simps 115 116text \<open>Transfer facts from multiplicative structures via interpretation.\<close> 117 118sublocale abelian_monoid < 119 add: monoid "(add_monoid G)" 120 rewrites "carrier (add_monoid G) = carrier G" 121 and "mult (add_monoid G) = add G" 122 and "one (add_monoid G) = zero G" 123 and "(\<lambda>a k. pow (add_monoid G) a k) = (\<lambda>a k. add_pow G k a)" 124 by (rule a_monoid) (auto simp add: add_pow_def) 125 126context abelian_monoid 127begin 128 129lemmas a_closed = add.m_closed 130lemmas zero_closed = add.one_closed 131lemmas a_assoc = add.m_assoc 132lemmas l_zero = add.l_one 133lemmas r_zero = add.r_one 134lemmas minus_unique = add.inv_unique 135 136end 137 138sublocale abelian_monoid < 139 add: comm_monoid "(add_monoid G)" 140 rewrites "carrier (add_monoid G) = carrier G" 141 and "mult (add_monoid G) = add G" 142 and "one (add_monoid G) = zero G" 143 and "finprod (add_monoid G) = finsum G" 144 and "pow (add_monoid G) = (\<lambda>a k. add_pow G k a)" 145 by (rule a_comm_monoid) (auto simp: finsum_def add_pow_def) 146 147context abelian_monoid begin 148 149lemmas a_comm = add.m_comm 150lemmas a_lcomm = add.m_lcomm 151lemmas a_ac = a_assoc a_comm a_lcomm 152 153lemmas finsum_empty = add.finprod_empty 154lemmas finsum_insert = add.finprod_insert 155lemmas finsum_zero = add.finprod_one 156lemmas finsum_closed = add.finprod_closed 157lemmas finsum_Un_Int = add.finprod_Un_Int 158lemmas finsum_Un_disjoint = add.finprod_Un_disjoint 159lemmas finsum_addf = add.finprod_multf 160lemmas finsum_cong' = add.finprod_cong' 161lemmas finsum_0 = add.finprod_0 162lemmas finsum_Suc = add.finprod_Suc 163lemmas finsum_Suc2 = add.finprod_Suc2 164lemmas finsum_infinite = add.finprod_infinite 165 166lemmas finsum_cong = add.finprod_cong 167text \<open>Usually, if this rule causes a failed congruence proof error, 168 the reason is that the premise \<open>g \<in> B \<rightarrow> carrier G\<close> cannot be shown. 169 Adding @{thm [source] Pi_def} to the simpset is often useful.\<close> 170 171lemmas finsum_reindex = add.finprod_reindex 172 173(* The following would be wrong. Needed is the equivalent of [^] for addition, 174 or indeed the canonical embedding from Nat into the monoid. 175 176lemma finsum_const: 177 assumes fin [simp]: "finite A" 178 and a [simp]: "a : carrier G" 179 shows "finsum G (%x. a) A = a [^] card A" 180 using fin apply induct 181 apply force 182 apply (subst finsum_insert) 183 apply auto 184 apply (force simp add: Pi_def) 185 apply (subst m_comm) 186 apply auto 187done 188*) 189 190lemmas finsum_singleton = add.finprod_singleton 191 192end 193 194sublocale abelian_group < 195 add: group "(add_monoid G)" 196 rewrites "carrier (add_monoid G) = carrier G" 197 and "mult (add_monoid G) = add G" 198 and "one (add_monoid G) = zero G" 199 and "m_inv (add_monoid G) = a_inv G" 200 and "pow (add_monoid G) = (\<lambda>a k. add_pow G k a)" 201 by (rule a_group) (auto simp: m_inv_def a_inv_def add_pow_def) 202 203context abelian_group 204begin 205 206lemmas a_inv_closed = add.inv_closed 207 208lemma minus_closed [intro, simp]: 209 "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G" 210 by (simp add: a_minus_def) 211 212lemmas l_neg = add.l_inv [simp del] 213lemmas r_neg = add.r_inv [simp del] 214lemmas minus_minus = add.inv_inv 215lemmas a_inv_inj = add.inv_inj 216lemmas minus_equality = add.inv_equality 217 218end 219 220sublocale abelian_group < 221 add: comm_group "(add_monoid G)" 222 rewrites "carrier (add_monoid G) = carrier G" 223 and "mult (add_monoid G) = add G" 224 and "one (add_monoid G) = zero G" 225 and "m_inv (add_monoid G) = a_inv G" 226 and "finprod (add_monoid G) = finsum G" 227 and "pow (add_monoid G) = (\<lambda>a k. add_pow G k a)" 228 by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def add_pow_def) 229 230lemmas (in abelian_group) minus_add = add.inv_mult 231 232text \<open>Derive an \<open>abelian_group\<close> from a \<open>comm_group\<close>\<close> 233 234lemma comm_group_abelian_groupI: 235 fixes G (structure) 236 assumes cg: "comm_group (add_monoid G)" 237 shows "abelian_group G" 238proof - 239 interpret comm_group "(add_monoid G)" 240 by (rule cg) 241 show "abelian_group G" .. 242qed 243 244 245subsection \<open>Rings: Basic Definitions\<close> 246 247locale semiring = abelian_monoid (* for add *) R + monoid (* for mult *) R for R (structure) + 248 assumes l_distr: "\<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" 249 and r_distr: "\<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" 250 and l_null[simp]: "x \<in> carrier R \<Longrightarrow> \<zero> \<otimes> x = \<zero>" 251 and r_null[simp]: "x \<in> carrier R \<Longrightarrow> x \<otimes> \<zero> = \<zero>" 252 253locale ring = abelian_group (* for add *) R + monoid (* for mult *) R for R (structure) + 254 assumes "\<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" 255 and "\<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" 256 257locale cring = ring + comm_monoid (* for mult *) R 258 259locale "domain" = cring + 260 assumes one_not_zero [simp]: "\<one> \<noteq> \<zero>" 261 and integral: "\<lbrakk> a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> a = \<zero> \<or> b = \<zero>" 262 263locale field = "domain" + 264 assumes field_Units: "Units R = carrier R - {\<zero>}" 265 266 267subsection \<open>Rings\<close> 268 269lemma ringI: 270 fixes R (structure) 271 assumes "abelian_group R" 272 and "monoid R" 273 and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" 274 and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" 275 shows "ring R" 276 by (auto intro: ring.intro 277 abelian_group.axioms ring_axioms.intro assms) 278 279lemma ringE: 280 fixes R (structure) 281 assumes "ring R" 282 shows "abelian_group R" 283 and "monoid R" 284 and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" 285 and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" 286 using assms unfolding ring_def ring_axioms_def by auto 287 288context ring begin 289 290lemma is_abelian_group: "abelian_group R" .. 291 292lemma is_monoid: "monoid R" 293 by (auto intro!: monoidI m_assoc) 294 295lemma is_ring: "ring R" 296 by (rule ring_axioms) 297 298end 299thm monoid_record_simps 300lemmas ring_record_simps = monoid_record_simps ring.simps 301 302lemma cringI: 303 fixes R (structure) 304 assumes abelian_group: "abelian_group R" 305 and comm_monoid: "comm_monoid R" 306 and l_distr: "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> 307 (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" 308 shows "cring R" 309proof (intro cring.intro ring.intro) 310 show "ring_axioms R" 311 \<comment> \<open>Right-distributivity follows from left-distributivity and 312 commutativity.\<close> 313 proof (rule ring_axioms.intro) 314 fix x y z 315 assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R" 316 note [simp] = comm_monoid.axioms [OF comm_monoid] 317 abelian_group.axioms [OF abelian_group] 318 abelian_monoid.a_closed 319 320 from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" 321 by (simp add: comm_monoid.m_comm [OF comm_monoid.intro]) 322 also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr) 323 also from R have "... = z \<otimes> x \<oplus> z \<otimes> y" 324 by (simp add: comm_monoid.m_comm [OF comm_monoid.intro]) 325 finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" . 326 qed (rule l_distr) 327qed (auto intro: cring.intro 328 abelian_group.axioms comm_monoid.axioms ring_axioms.intro assms) 329 330lemma cringE: 331 fixes R (structure) 332 assumes "cring R" 333 shows "comm_monoid R" 334 and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z" 335 using assms cring_def by auto (simp add: assms cring.axioms(1) ringE(3)) 336 337lemma (in cring) is_cring: 338 "cring R" by (rule cring_axioms) 339 340lemma (in ring) minus_zero [simp]: "\<ominus> \<zero> = \<zero>" 341 by (simp add: a_inv_def) 342 343subsubsection \<open>Normaliser for Rings\<close> 344 345lemma (in abelian_group) r_neg1: 346 "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> (\<ominus> x) \<oplus> (x \<oplus> y) = y" 347proof - 348 assume G: "x \<in> carrier G" "y \<in> carrier G" 349 then have "(\<ominus> x \<oplus> x) \<oplus> y = y" 350 by (simp only: l_neg l_zero) 351 with G show ?thesis by (simp add: a_ac) 352qed 353 354lemma (in abelian_group) r_neg2: 355 "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> x \<oplus> ((\<ominus> x) \<oplus> y) = y" 356proof - 357 assume G: "x \<in> carrier G" "y \<in> carrier G" 358 then have "(x \<oplus> \<ominus> x) \<oplus> y = y" 359 by (simp only: r_neg l_zero) 360 with G show ?thesis 361 by (simp add: a_ac) 362qed 363 364context ring begin 365 366text \<open> 367 The following proofs are from Jacobson, Basic Algebra I, pp.~88--89. 368\<close> 369 370sublocale semiring 371proof - 372 note [simp] = ring_axioms[unfolded ring_def ring_axioms_def] 373 show "semiring R" 374 proof (unfold_locales) 375 fix x 376 assume R: "x \<in> carrier R" 377 then have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = (\<zero> \<oplus> \<zero>) \<otimes> x" 378 by (simp del: l_zero r_zero) 379 also from R have "... = \<zero> \<otimes> x \<oplus> \<zero>" by simp 380 finally have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = \<zero> \<otimes> x \<oplus> \<zero>" . 381 with R show "\<zero> \<otimes> x = \<zero>" by (simp del: r_zero) 382 from R have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> (\<zero> \<oplus> \<zero>)" 383 by (simp del: l_zero r_zero) 384 also from R have "... = x \<otimes> \<zero> \<oplus> \<zero>" by simp 385 finally have "x \<otimes> \<zero> \<oplus> x \<otimes> \<zero> = x \<otimes> \<zero> \<oplus> \<zero>" . 386 with R show "x \<otimes> \<zero> = \<zero>" by (simp del: r_zero) 387 qed auto 388qed 389 390lemma l_minus: 391 "\<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> (\<ominus> x) \<otimes> y = \<ominus> (x \<otimes> y)" 392proof - 393 assume R: "x \<in> carrier R" "y \<in> carrier R" 394 then have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = (\<ominus> x \<oplus> x) \<otimes> y" by (simp add: l_distr) 395 also from R have "... = \<zero>" by (simp add: l_neg) 396 finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" . 397 with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp 398 with R show ?thesis by (simp add: a_assoc r_neg) 399qed 400 401lemma r_minus: 402 "\<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<otimes> (\<ominus> y) = \<ominus> (x \<otimes> y)" 403proof - 404 assume R: "x \<in> carrier R" "y \<in> carrier R" 405 then have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = x \<otimes> (\<ominus> y \<oplus> y)" by (simp add: r_distr) 406 also from R have "... = \<zero>" by (simp add: l_neg) 407 finally have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y = \<zero>" . 408 with R have "x \<otimes> (\<ominus> y) \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp 409 with R show ?thesis by (simp add: a_assoc r_neg ) 410qed 411 412end 413 414lemma (in abelian_group) minus_eq: "x \<ominus> y = x \<oplus> (\<ominus> y)" 415 by (rule a_minus_def) 416 417text \<open>Setup algebra method: 418 compute distributive normal form in locale contexts\<close> 419 420 421ML_file "ringsimp.ML" 422 423attribute_setup algebra = \<open> 424 Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true) 425 -- Scan.lift Args.name -- Scan.repeat Args.term 426 >> (fn ((b, n), ts) => if b then Ringsimp.add_struct (n, ts) else Ringsimp.del_struct (n, ts)) 427\<close> "theorems controlling algebra method" 428 429method_setup algebra = \<open> 430 Scan.succeed (SIMPLE_METHOD' o Ringsimp.algebra_tac) 431\<close> "normalisation of algebraic structure" 432 433lemmas (in semiring) semiring_simprules 434 [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = 435 a_closed zero_closed m_closed one_closed 436 a_assoc l_zero a_comm m_assoc l_one l_distr r_zero 437 a_lcomm r_distr l_null r_null 438 439lemmas (in ring) ring_simprules 440 [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = 441 a_closed zero_closed a_inv_closed minus_closed m_closed one_closed 442 a_assoc l_zero l_neg a_comm m_assoc l_one l_distr minus_eq 443 r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero 444 a_lcomm r_distr l_null r_null l_minus r_minus 445 446lemmas (in cring) 447 [algebra del: ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = 448 _ 449 450lemmas (in cring) cring_simprules 451 [algebra add: cring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] = 452 a_closed zero_closed a_inv_closed minus_closed m_closed one_closed 453 a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq 454 r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero 455 a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus 456 457lemma (in semiring) nat_pow_zero: 458 "(n::nat) \<noteq> 0 \<Longrightarrow> \<zero> [^] n = \<zero>" 459 by (induct n) simp_all 460 461context semiring begin 462 463lemma one_zeroD: 464 assumes onezero: "\<one> = \<zero>" 465 shows "carrier R = {\<zero>}" 466proof (rule, rule) 467 fix x 468 assume xcarr: "x \<in> carrier R" 469 from xcarr have "x = x \<otimes> \<one>" by simp 470 with onezero have "x = x \<otimes> \<zero>" by simp 471 with xcarr have "x = \<zero>" by simp 472 then show "x \<in> {\<zero>}" by fast 473qed fast 474 475lemma one_zeroI: 476 assumes carrzero: "carrier R = {\<zero>}" 477 shows "\<one> = \<zero>" 478proof - 479 from one_closed and carrzero 480 show "\<one> = \<zero>" by simp 481qed 482 483lemma carrier_one_zero: "(carrier R = {\<zero>}) = (\<one> = \<zero>)" 484 using one_zeroD by blast 485 486lemma carrier_one_not_zero: "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)" 487 by (simp add: carrier_one_zero) 488 489end 490 491text \<open>Two examples for use of method algebra\<close> 492 493lemma 494 fixes R (structure) and S (structure) 495 assumes "ring R" "cring S" 496 assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S" 497 shows "a \<oplus> (\<ominus> (a \<oplus> (\<ominus> b))) = b \<and> c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c" 498proof - 499 interpret ring R by fact 500 interpret cring S by fact 501 from RS show ?thesis by algebra 502qed 503 504lemma 505 fixes R (structure) 506 assumes "ring R" 507 assumes R: "a \<in> carrier R" "b \<in> carrier R" 508 shows "a \<ominus> (a \<ominus> b) = b" 509proof - 510 interpret ring R by fact 511 from R show ?thesis by algebra 512qed 513 514 515subsubsection \<open>Sums over Finite Sets\<close> 516 517lemma (in semiring) finsum_ldistr: 518 "\<lbrakk> finite A; a \<in> carrier R; f: A \<rightarrow> carrier R \<rbrakk> \<Longrightarrow> 519 (\<Oplus> i \<in> A. (f i)) \<otimes> a = (\<Oplus> i \<in> A. ((f i) \<otimes> a))" 520proof (induct set: finite) 521 case empty then show ?case by simp 522next 523 case (insert x F) then show ?case by (simp add: Pi_def l_distr) 524qed 525 526lemma (in semiring) finsum_rdistr: 527 "\<lbrakk> finite A; a \<in> carrier R; f: A \<rightarrow> carrier R \<rbrakk> \<Longrightarrow> 528 a \<otimes> (\<Oplus> i \<in> A. (f i)) = (\<Oplus> i \<in> A. (a \<otimes> (f i)))" 529proof (induct set: finite) 530 case empty then show ?case by simp 531next 532 case (insert x F) then show ?case by (simp add: Pi_def r_distr) 533qed 534 535(* ************************************************************************** *) 536(* Contributed by Paulo E. de Vilhena. *) 537 538text \<open>A quick detour\<close> 539 540lemma add_pow_int_ge: "(k :: int) \<ge> 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = [ nat k ] \<cdot>\<^bsub>R\<^esub> a" 541 by (simp add: add_pow_def int_pow_def nat_pow_def) 542 543lemma add_pow_int_lt: "(k :: int) < 0 \<Longrightarrow> [ k ] \<cdot>\<^bsub>R\<^esub> a = \<ominus>\<^bsub>R\<^esub> ([ nat (- k) ] \<cdot>\<^bsub>R\<^esub> a)" 544 by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def) 545 546corollary (in semiring) add_pow_ldistr: 547 assumes "a \<in> carrier R" "b \<in> carrier R" 548 shows "([(k :: nat)] \<cdot> a) \<otimes> b = [k] \<cdot> (a \<otimes> b)" 549proof - 550 have "([k] \<cdot> a) \<otimes> b = (\<Oplus> i \<in> {..< k}. a) \<otimes> b" 551 using add.finprod_const[OF assms(1), of "{..<k}"] by simp 552 also have " ... = (\<Oplus> i \<in> {..< k}. (a \<otimes> b))" 553 using finsum_ldistr[of "{..<k}" b "\<lambda>x. a"] assms by simp 554 also have " ... = [k] \<cdot> (a \<otimes> b)" 555 using add.finprod_const[of "a \<otimes> b" "{..<k}"] assms by simp 556 finally show ?thesis . 557qed 558 559corollary (in semiring) add_pow_rdistr: 560 assumes "a \<in> carrier R" "b \<in> carrier R" 561 shows "a \<otimes> ([(k :: nat)] \<cdot> b) = [k] \<cdot> (a \<otimes> b)" 562proof - 563 have "a \<otimes> ([k] \<cdot> b) = a \<otimes> (\<Oplus> i \<in> {..< k}. b)" 564 using add.finprod_const[OF assms(2), of "{..<k}"] by simp 565 also have " ... = (\<Oplus> i \<in> {..< k}. (a \<otimes> b))" 566 using finsum_rdistr[of "{..<k}" a "\<lambda>x. b"] assms by simp 567 also have " ... = [k] \<cdot> (a \<otimes> b)" 568 using add.finprod_const[of "a \<otimes> b" "{..<k}"] assms by simp 569 finally show ?thesis . 570qed 571 572(* For integers, we need the uniqueness of the additive inverse *) 573lemma (in ring) add_pow_ldistr_int: 574 assumes "a \<in> carrier R" "b \<in> carrier R" 575 shows "([(k :: int)] \<cdot> a) \<otimes> b = [k] \<cdot> (a \<otimes> b)" 576proof (cases "k \<ge> 0") 577 case True thus ?thesis 578 using add_pow_int_ge[of k R] add_pow_ldistr[OF assms] by auto 579next 580 case False thus ?thesis 581 using add_pow_int_lt[of k R a] add_pow_int_lt[of k R "a \<otimes> b"] 582 add_pow_ldistr[OF assms, of "nat (- k)"] assms l_minus by auto 583qed 584 585lemma (in ring) add_pow_rdistr_int: 586 assumes "a \<in> carrier R" "b \<in> carrier R" 587 shows "a \<otimes> ([(k :: int)] \<cdot> b) = [k] \<cdot> (a \<otimes> b)" 588proof (cases "k \<ge> 0") 589 case True thus ?thesis 590 using add_pow_int_ge[of k R] add_pow_rdistr[OF assms] by auto 591next 592 case False thus ?thesis 593 using add_pow_int_lt[of k R b] add_pow_int_lt[of k R "a \<otimes> b"] 594 add_pow_rdistr[OF assms, of "nat (- k)"] assms r_minus by auto 595qed 596 597 598subsection \<open>Integral Domains\<close> 599 600context "domain" begin 601 602lemma zero_not_one [simp]: "\<zero> \<noteq> \<one>" 603 by (rule not_sym) simp 604 605lemma integral_iff: (* not by default a simp rule! *) 606 "\<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> (a \<otimes> b = \<zero>) = (a = \<zero> \<or> b = \<zero>)" 607proof 608 assume "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b = \<zero>" 609 then show "a = \<zero> \<or> b = \<zero>" by (simp add: integral) 610next 611 assume "a \<in> carrier R" "b \<in> carrier R" "a = \<zero> \<or> b = \<zero>" 612 then show "a \<otimes> b = \<zero>" by auto 613qed 614 615lemma m_lcancel: 616 assumes prem: "a \<noteq> \<zero>" 617 and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R" 618 shows "(a \<otimes> b = a \<otimes> c) = (b = c)" 619proof 620 assume eq: "a \<otimes> b = a \<otimes> c" 621 with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra 622 with R have "a = \<zero> \<or> (b \<ominus> c) = \<zero>" by (simp add: integral_iff) 623 with prem and R have "b \<ominus> c = \<zero>" by auto 624 with R have "b = b \<ominus> (b \<ominus> c)" by algebra 625 also from R have "b \<ominus> (b \<ominus> c) = c" by algebra 626 finally show "b = c" . 627next 628 assume "b = c" then show "a \<otimes> b = a \<otimes> c" by simp 629qed 630 631lemma m_rcancel: 632 assumes prem: "a \<noteq> \<zero>" 633 and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R" 634 shows conc: "(b \<otimes> a = c \<otimes> a) = (b = c)" 635proof - 636 from prem and R have "(a \<otimes> b = a \<otimes> c) = (b = c)" by (rule m_lcancel) 637 with R show ?thesis by algebra 638qed 639 640end 641 642 643subsection \<open>Fields\<close> 644 645text \<open>Field would not need to be derived from domain, the properties 646 for domain follow from the assumptions of field\<close> 647 648lemma fieldE : 649 fixes R (structure) 650 assumes "field R" 651 shows "cring R" 652 and one_not_zero : "\<one> \<noteq> \<zero>" 653 and integral: "\<And>a b. \<lbrakk> a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> a = \<zero> \<or> b = \<zero>" 654 and field_Units: "Units R = carrier R - {\<zero>}" 655 using assms unfolding field_def field_axioms_def domain_def domain_axioms_def by simp_all 656 657lemma (in cring) cring_fieldI: 658 assumes field_Units: "Units R = carrier R - {\<zero>}" 659 shows "field R" 660proof 661 from field_Units have "\<zero> \<notin> Units R" by fast 662 moreover have "\<one> \<in> Units R" by fast 663 ultimately show "\<one> \<noteq> \<zero>" by force 664next 665 fix a b 666 assume acarr: "a \<in> carrier R" 667 and bcarr: "b \<in> carrier R" 668 and ab: "a \<otimes> b = \<zero>" 669 show "a = \<zero> \<or> b = \<zero>" 670 proof (cases "a = \<zero>", simp) 671 assume "a \<noteq> \<zero>" 672 with field_Units and acarr have aUnit: "a \<in> Units R" by fast 673 from bcarr have "b = \<one> \<otimes> b" by algebra 674 also from aUnit acarr have "... = (inv a \<otimes> a) \<otimes> b" by simp 675 also from acarr bcarr aUnit[THEN Units_inv_closed] 676 have "... = (inv a) \<otimes> (a \<otimes> b)" by algebra 677 also from ab and acarr bcarr aUnit have "... = (inv a) \<otimes> \<zero>" by simp 678 also from aUnit[THEN Units_inv_closed] have "... = \<zero>" by algebra 679 finally have "b = \<zero>" . 680 then show "a = \<zero> \<or> b = \<zero>" by simp 681 qed 682qed (rule field_Units) 683 684text \<open>Another variant to show that something is a field\<close> 685lemma (in cring) cring_fieldI2: 686 assumes notzero: "\<zero> \<noteq> \<one>" 687 and invex: "\<And>a. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a \<otimes> b = \<one>" 688 shows "field R" 689proof - 690 have *: "carrier R - {\<zero>} \<subseteq> {y \<in> carrier R. \<exists>x\<in>carrier R. x \<otimes> y = \<one> \<and> y \<otimes> x = \<one>}" 691 proof (clarsimp) 692 fix x 693 assume xcarr: "x \<in> carrier R" and "x \<noteq> \<zero>" 694 obtain y where ycarr: "y \<in> carrier R" and xy: "x \<otimes> y = \<one>" 695 using \<open>x \<noteq> \<zero>\<close> invex xcarr by blast 696 with ycarr and xy show "\<exists>y\<in>carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" 697 using m_comm xcarr by fastforce 698 qed 699 show ?thesis 700 apply (rule cring_fieldI, simp add: Units_def) 701 using * 702 using group_l_invI notzero set_diff_eq by auto 703qed 704 705 706subsection \<open>Morphisms\<close> 707 708definition 709 ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set" 710 where "ring_hom R S = 711 {h. h \<in> carrier R \<rightarrow> carrier S \<and> 712 (\<forall>x y. x \<in> carrier R \<and> y \<in> carrier R \<longrightarrow> 713 h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y \<and> h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) \<and> 714 h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}" 715 716lemma ring_hom_memI: 717 fixes R (structure) and S (structure) 718 assumes "\<And>x. x \<in> carrier R \<Longrightarrow> h x \<in> carrier S" 719 and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" 720 and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y" 721 and "h \<one> = \<one>\<^bsub>S\<^esub>" 722 shows "h \<in> ring_hom R S" 723 by (auto simp add: ring_hom_def assms Pi_def) 724 725lemma ring_hom_memE: 726 fixes R (structure) and S (structure) 727 assumes "h \<in> ring_hom R S" 728 shows "\<And>x. x \<in> carrier R \<Longrightarrow> h x \<in> carrier S" 729 and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" 730 and "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y" 731 and "h \<one> = \<one>\<^bsub>S\<^esub>" 732 using assms unfolding ring_hom_def by auto 733 734lemma ring_hom_closed: 735 "\<lbrakk> h \<in> ring_hom R S; x \<in> carrier R \<rbrakk> \<Longrightarrow> h x \<in> carrier S" 736 by (auto simp add: ring_hom_def funcset_mem) 737 738lemma ring_hom_mult: 739 fixes R (structure) and S (structure) 740 shows "\<lbrakk> h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y" 741 by (simp add: ring_hom_def) 742 743lemma ring_hom_add: 744 fixes R (structure) and S (structure) 745 shows "\<lbrakk> h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y" 746 by (simp add: ring_hom_def) 747 748lemma ring_hom_one: 749 fixes R (structure) and S (structure) 750 shows "h \<in> ring_hom R S \<Longrightarrow> h \<one> = \<one>\<^bsub>S\<^esub>" 751 by (simp add: ring_hom_def) 752 753lemma ring_hom_zero: 754 fixes R (structure) and S (structure) 755 assumes "h \<in> ring_hom R S" "ring R" "ring S" 756 shows "h \<zero> = \<zero>\<^bsub>S\<^esub>" 757proof - 758 have "h \<zero> = h \<zero> \<oplus>\<^bsub>S\<^esub> h \<zero>" 759 using ring_hom_add[OF assms(1), of \<zero> \<zero>] assms(2) 760 by (simp add: ring.ring_simprules(2) ring.ring_simprules(15)) 761 thus ?thesis 762 by (metis abelian_group.l_neg assms ring.is_abelian_group ring.ring_simprules(18) ring.ring_simprules(2) ring_hom_closed) 763qed 764 765locale ring_hom_cring = 766 R?: cring R + S?: cring S for R (structure) and S (structure) + fixes h 767 assumes homh [simp, intro]: "h \<in> ring_hom R S" 768 notes hom_closed [simp, intro] = ring_hom_closed [OF homh] 769 and hom_mult [simp] = ring_hom_mult [OF homh] 770 and hom_add [simp] = ring_hom_add [OF homh] 771 and hom_one [simp] = ring_hom_one [OF homh] 772 773lemma (in ring_hom_cring) hom_zero [simp]: "h \<zero> = \<zero>\<^bsub>S\<^esub>" 774proof - 775 have "h \<zero> \<oplus>\<^bsub>S\<^esub> h \<zero> = h \<zero> \<oplus>\<^bsub>S\<^esub> \<zero>\<^bsub>S\<^esub>" 776 by (simp add: hom_add [symmetric] del: hom_add) 777 then show ?thesis by (simp del: S.r_zero) 778qed 779 780lemma (in ring_hom_cring) hom_a_inv [simp]: 781 "x \<in> carrier R \<Longrightarrow> h (\<ominus> x) = \<ominus>\<^bsub>S\<^esub> h x" 782proof - 783 assume R: "x \<in> carrier R" 784 then have "h x \<oplus>\<^bsub>S\<^esub> h (\<ominus> x) = h x \<oplus>\<^bsub>S\<^esub> (\<ominus>\<^bsub>S\<^esub> h x)" 785 by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add) 786 with R show ?thesis by simp 787qed 788 789lemma (in ring_hom_cring) hom_finsum [simp]: 790 assumes "f: A \<rightarrow> carrier R" 791 shows "h (\<Oplus> i \<in> A. f i) = (\<Oplus>\<^bsub>S\<^esub> i \<in> A. (h o f) i)" 792 using assms by (induct A rule: infinite_finite_induct, auto simp: Pi_def) 793 794lemma (in ring_hom_cring) hom_finprod: 795 assumes "f: A \<rightarrow> carrier R" 796 shows "h (\<Otimes> i \<in> A. f i) = (\<Otimes>\<^bsub>S\<^esub> i \<in> A. (h o f) i)" 797 using assms by (induct A rule: infinite_finite_induct, auto simp: Pi_def) 798 799declare ring_hom_cring.hom_finprod [simp] 800 801lemma id_ring_hom [simp]: "id \<in> ring_hom R R" 802 by (auto intro!: ring_hom_memI) 803 804(* Next lemma contributed by Paulo Em��lio de Vilhena. *) 805 806lemma ring_hom_trans: 807 "\<lbrakk> f \<in> ring_hom R S; g \<in> ring_hom S T \<rbrakk> \<Longrightarrow> g \<circ> f \<in> ring_hom R T" 808 by (rule ring_hom_memI) (auto simp add: ring_hom_closed ring_hom_mult ring_hom_add ring_hom_one) 809 810subsection\<open>Jeremy Avigad's @{text"More_Finite_Product"} material\<close> 811 812(* need better simplification rules for rings *) 813(* the next one holds more generally for abelian groups *) 814 815lemma (in cring) sum_zero_eq_neg: "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y" 816 by (metis minus_equality) 817 818lemma (in domain) square_eq_one: 819 fixes x 820 assumes [simp]: "x \<in> carrier R" 821 and "x \<otimes> x = \<one>" 822 shows "x = \<one> \<or> x = \<ominus>\<one>" 823proof - 824 have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>" 825 by (simp add: ring_simprules) 826 also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>" 827 by (simp add: ring_simprules) 828 finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" . 829 then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>" 830 by (intro integral) auto 831 then show ?thesis 832 by (metis add.inv_closed add.inv_solve_right assms(1) l_zero one_closed zero_closed) 833qed 834 835lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>" 836 by (metis Units_closed Units_l_inv square_eq_one) 837 838 839text \<open> 840 The following translates theorems about groups to the facts about 841 the units of a ring. (The list should be expanded as more things are 842 needed.) 843\<close> 844 845lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)" 846 by (rule finite_subset) auto 847 848lemma (in monoid) units_of_pow: 849 fixes n :: nat 850 shows "x \<in> Units G \<Longrightarrow> x [^]\<^bsub>units_of G\<^esub> n = x [^]\<^bsub>G\<^esub> n" 851 apply (induct n) 852 apply (auto simp add: units_group group.is_monoid 853 monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult) 854 done 855 856lemma (in cring) units_power_order_eq_one: 857 "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a [^] card(Units R) = \<one>" 858 by (metis comm_group.power_order_eq_one units_comm_group units_of_carrier units_of_one units_of_pow) 859 860subsection\<open>Jeremy Avigad's @{text"More_Ring"} material\<close> 861 862lemma (in cring) field_intro2: 863 assumes "\<zero>\<^bsub>R\<^esub> \<noteq> \<one>\<^bsub>R\<^esub>" and un: "\<And>x. x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>} \<Longrightarrow> x \<in> Units R" 864 shows "field R" 865proof unfold_locales 866 show "\<one> \<noteq> \<zero>" using assms by auto 867 show "\<lbrakk>a \<otimes> b = \<zero>; a \<in> carrier R; 868 b \<in> carrier R\<rbrakk> 869 \<Longrightarrow> a = \<zero> \<or> b = \<zero>" for a b 870 by (metis un Units_l_cancel insert_Diff_single insert_iff r_null zero_closed) 871qed (use assms in \<open>auto simp: Units_def\<close>) 872 873lemma (in monoid) inv_char: 874 assumes "x \<in> carrier G" "y \<in> carrier G" "x \<otimes> y = \<one>" "y \<otimes> x = \<one>" 875 shows "inv x = y" 876 using assms inv_unique' by auto 877 878lemma (in comm_monoid) comm_inv_char: "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> inv x = y" 879 by (simp add: inv_char m_comm) 880 881lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>" 882 by (simp add: inv_char local.ring_axioms ring.r_minus) 883 884lemma (in monoid) inv_eq_imp_eq: "x \<in> Units G \<Longrightarrow> y \<in> Units G \<Longrightarrow> inv x = inv y \<Longrightarrow> x = y" 885 by (metis Units_inv_inv) 886 887lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R" 888 by (simp add: Units_def) (metis add.l_inv_ex local.minus_minus minus_equality one_closed r_minus r_one) 889 890lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>" 891 by (metis Units_inv_inv inv_neg_one) 892 893lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>" 894 by (metis Units_inv_inv inv_one) 895 896end 897