author paulson Sun Jul 22 13:29:41 2018 +0200 (12 months ago) changeset 68674 f4ac69fe4509 parent 68672 9247996782c9 parent 68673 22d10f94811e child 68676 74cb08ff2e66
merged
```     1.1 --- a/src/HOL/Algebra/QuotRing.thy	Sun Jul 22 13:00:38 2018 +0200
1.2 +++ b/src/HOL/Algebra/QuotRing.thy	Sun Jul 22 13:29:41 2018 +0200
1.3 @@ -16,61 +16,34 @@
1.4    where "rcoset_mult R I A B = (\<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b))"
1.5
1.6
1.7 -text \<open>@{const "rcoset_mult"} fulfils the properties required by
1.8 -  congruences\<close>
1.9 +text \<open>@{const "rcoset_mult"} fulfils the properties required by congruences\<close>
1.10  lemma (in ideal) rcoset_mult_add:
1.11 -    "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> [mod I:] (I +> x) \<Otimes> (I +> y) = I +> (x \<otimes> y)"
1.12 -  apply rule
1.13 -  apply (rule, simp add: rcoset_mult_def, clarsimp)
1.14 -  defer 1
1.15 -  apply (rule, simp add: rcoset_mult_def)
1.16 -  defer 1
1.17 +  assumes "x \<in> carrier R" "y \<in> carrier R"
1.18 +  shows "[mod I:] (I +> x) \<Otimes> (I +> y) = I +> (x \<otimes> y)"
1.19  proof -
1.20 -  fix z x' y'
1.21 -  assume carr: "x \<in> carrier R" "y \<in> carrier R"
1.22 -    and x'rcos: "x' \<in> I +> x"
1.23 -    and y'rcos: "y' \<in> I +> y"
1.24 -    and zrcos: "z \<in> I +> x' \<otimes> y'"
1.25 -
1.26 -  from x'rcos have "\<exists>h\<in>I. x' = h \<oplus> x"
1.27 -    by (simp add: a_r_coset_def r_coset_def)
1.28 -  then obtain hx where hxI: "hx \<in> I" and x': "x' = hx \<oplus> x"
1.29 -    by fast+
1.30 -
1.31 -  from y'rcos have "\<exists>h\<in>I. y' = h \<oplus> y"
1.32 -    by (simp add: a_r_coset_def r_coset_def)
1.33 -  then obtain hy where hyI: "hy \<in> I" and y': "y' = hy \<oplus> y"
1.34 -    by fast+
1.35 -
1.36 -  from zrcos have "\<exists>h\<in>I. z = h \<oplus> (x' \<otimes> y')"
1.37 -    by (simp add: a_r_coset_def r_coset_def)
1.38 -  then obtain hz where hzI: "hz \<in> I" and z: "z = hz \<oplus> (x' \<otimes> y')"
1.39 -    by fast+
1.40 -
1.41 -  note carr = carr hxI[THEN a_Hcarr] hyI[THEN a_Hcarr] hzI[THEN a_Hcarr]
1.42 -
1.43 -  from z have "z = hz \<oplus> (x' \<otimes> y')" .
1.44 -  also from x' y' have "\<dots> = hz \<oplus> ((hx \<oplus> x) \<otimes> (hy \<oplus> y))" by simp
1.45 -  also from carr have "\<dots> = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" by algebra
1.46 -  finally have z2: "z = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" .
1.47 -
1.48 -  from hxI hyI hzI carr have "hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy \<in> I"
1.49 -    by (simp add: I_l_closed I_r_closed)
1.50 -
1.51 -  with z2 have "\<exists>h\<in>I. z = h \<oplus> x \<otimes> y" by fast
1.52 -  then show "z \<in> I +> x \<otimes> y" by (simp add: a_r_coset_def r_coset_def)
1.53 -next
1.54 -  fix z
1.55 -  assume xcarr: "x \<in> carrier R"
1.56 -    and ycarr: "y \<in> carrier R"
1.57 -    and zrcos: "z \<in> I +> x \<otimes> y"
1.58 -  from xcarr have xself: "x \<in> I +> x" by (intro a_rcos_self)
1.59 -  from ycarr have yself: "y \<in> I +> y" by (intro a_rcos_self)
1.60 -  show "\<exists>a\<in>I +> x. \<exists>b\<in>I +> y. z \<in> I +> a \<otimes> b"
1.61 -    using xself and yself and zrcos by fast
1.62 +  have 1: "z \<in> I +> x \<otimes> y"
1.63 +    if x'rcos: "x' \<in> I +> x" and y'rcos: "y' \<in> I +> y" and zrcos: "z \<in> I +> x' \<otimes> y'" for z x' y'
1.64 +  proof -
1.65 +    from that
1.66 +    obtain hx hy hz where hxI: "hx \<in> I" and x': "x' = hx \<oplus> x" and hyI: "hy \<in> I" and y': "y' = hy \<oplus> y"
1.67 +      and hzI: "hz \<in> I" and z: "z = hz \<oplus> (x' \<otimes> y')"
1.68 +      by (auto simp: a_r_coset_def r_coset_def)
1.69 +    note carr = assms hxI[THEN a_Hcarr] hyI[THEN a_Hcarr] hzI[THEN a_Hcarr]
1.70 +    from z  x' y' have "z = hz \<oplus> ((hx \<oplus> x) \<otimes> (hy \<oplus> y))" by simp
1.71 +    also from carr have "\<dots> = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" by algebra
1.72 +    finally have z2: "z = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" .
1.73 +    from hxI hyI hzI carr have "hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy \<in> I"
1.74 +      by (simp add: I_l_closed I_r_closed)
1.75 +    with z2 show ?thesis
1.76 +      by (auto simp add: a_r_coset_def r_coset_def)
1.77 +  qed
1.78 +  have 2: "\<exists>a\<in>I +> x. \<exists>b\<in>I +> y. z \<in> I +> a \<otimes> b" if "z \<in> I +> x \<otimes> y" for z
1.79 +    using assms a_rcos_self that by blast
1.80 +  show ?thesis
1.81 +    unfolding rcoset_mult_def using assms
1.82 +    by (auto simp: intro!: 1 2)
1.83  qed
1.84
1.85 -
1.86  subsection \<open>Quotient Ring Definition\<close>
1.87
1.88  definition FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"
1.89 @@ -79,59 +52,30 @@
1.90      \<lparr>carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I,
1.91        one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"
1.92
1.93 +lemmas FactRing_simps = FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric]
1.94
1.95  subsection \<open>Factorization over General Ideals\<close>
1.96
1.97  text \<open>The quotient is a ring\<close>
1.98  lemma (in ideal) quotient_is_ring: "ring (R Quot I)"
1.99 -apply (rule ringI)
1.100 -   \<comment> \<open>abelian group\<close>
1.101 -   apply (rule comm_group_abelian_groupI)
1.102 -   apply (simp add: FactRing_def)
1.103 -   apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def'])
1.104 -  \<comment> \<open>mult monoid\<close>
1.105 -  apply (rule monoidI)
1.106 -      apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def
1.107 -             a_r_coset_def[symmetric])
1.108 -      \<comment> \<open>mult closed\<close>
1.109 -      apply (clarify)
1.110 -      apply (simp add: rcoset_mult_add, fast)
1.111 -     \<comment> \<open>mult \<open>one_closed\<close>\<close>
1.112 -     apply force
1.113 -    \<comment> \<open>mult assoc\<close>
1.114 -    apply clarify
1.115 -    apply (simp add: rcoset_mult_add m_assoc)
1.116 -   \<comment> \<open>mult one\<close>
1.117 -   apply clarify
1.119 -  apply clarify
1.121 - \<comment> \<open>distr\<close>
1.122 - apply clarify
1.123 - apply (simp add: rcoset_mult_add a_rcos_sum l_distr)
1.124 -apply clarify
1.125 -apply (simp add: rcoset_mult_add a_rcos_sum r_distr)
1.126 -done
1.127 +proof (rule ringI)
1.128 +  show "abelian_group (R Quot I)"
1.129 +    apply (rule comm_group_abelian_groupI)
1.130 +    apply (simp add: FactRing_def a_factorgroup_is_comm_group[unfolded A_FactGroup_def'])
1.131 +    done
1.132 +  show "Group.monoid (R Quot I)"
1.133 +    by (rule monoidI)
1.134 +      (auto simp add: FactRing_simps rcoset_mult_add m_assoc)
1.135 +qed (auto simp: FactRing_simps rcoset_mult_add a_rcos_sum l_distr r_distr)
1.136
1.137
1.138  text \<open>This is a ring homomorphism\<close>
1.139
1.140  lemma (in ideal) rcos_ring_hom: "((+>) I) \<in> ring_hom R (R Quot I)"
1.141 -apply (rule ring_hom_memI)
1.142 -   apply (simp add: FactRing_def a_rcosetsI[OF a_subset])
1.143 -  apply (simp add: FactRing_def rcoset_mult_add)
1.144 - apply (simp add: FactRing_def a_rcos_sum)
1.145 -apply (simp add: FactRing_def)
1.146 -done
1.147 +  by (simp add: ring_hom_memI FactRing_def a_rcosetsI[OF a_subset] rcoset_mult_add a_rcos_sum)
1.148
1.149  lemma (in ideal) rcos_ring_hom_ring: "ring_hom_ring R (R Quot I) ((+>) I)"
1.150 -apply (rule ring_hom_ringI)
1.151 -     apply (rule is_ring, rule quotient_is_ring)
1.152 -   apply (simp add: FactRing_def a_rcosetsI[OF a_subset])
1.153 -  apply (simp add: FactRing_def rcoset_mult_add)
1.154 - apply (simp add: FactRing_def a_rcos_sum)
1.155 -apply (simp add: FactRing_def)
1.156 -done
1.157 +  by (simp add: local.ring_axioms quotient_is_ring rcos_ring_hom ring_hom_ringI2)
1.158
1.159  text \<open>The quotient of a cring is also commutative\<close>
1.160  lemma (in ideal) quotient_is_cring:
1.161 @@ -140,12 +84,9 @@
1.162  proof -
1.163    interpret cring R by fact
1.164    show ?thesis
1.165 -    apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
1.166 -      apply (rule quotient_is_ring)
1.167 +    apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro quotient_is_ring)
1.168       apply (rule ring.axioms[OF quotient_is_ring])
1.169 -    apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric])
1.170 -    apply clarify
1.171 -    apply (simp add: rcoset_mult_add m_comm)
1.172 +    apply (auto simp add: FactRing_simps rcoset_mult_add m_comm)
1.173      done
1.174  qed
1.175
1.176 @@ -169,37 +110,19 @@
1.177
1.178  text \<open>The quotient ring generated by a prime ideal is a domain\<close>
1.179  lemma (in primeideal) quotient_is_domain: "domain (R Quot I)"
1.180 -  apply (rule domain.intro)
1.181 -   apply (rule quotient_is_cring, rule is_cring)
1.182 -  apply (rule domain_axioms.intro)
1.183 -   apply (simp add: FactRing_def) defer 1
1.184 -    apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarify)
1.185 -    apply (simp add: rcoset_mult_add) defer 1
1.186 -proof (rule ccontr, clarsimp)
1.187 -  assume "I +> \<one> = I"
1.188 -  then have "\<one> \<in> I" by (simp only: a_coset_join1 one_closed a_subgroup)
1.189 -  then have "carrier R \<subseteq> I" by (subst one_imp_carrier, simp, fast)
1.190 -  with a_subset have "I = carrier R" by fast
1.191 -  with I_notcarr show False by fast
1.192 -next
1.193 -  fix x y
1.194 -  assume carr: "x \<in> carrier R" "y \<in> carrier R"
1.195 +proof -
1.196 +  have 1: "I +> \<one> = I \<Longrightarrow> False"
1.197 +    using I_notcarr a_rcos_self one_imp_carrier by blast
1.198 +  have 2: "I +> x = I"
1.199 +    if  carr: "x \<in> carrier R" "y \<in> carrier R"
1.200      and a: "I +> x \<otimes> y = I"
1.201 -    and b: "I +> y \<noteq> I"
1.202 -
1.203 -  have ynI: "y \<notin> I"
1.204 -  proof (rule ccontr, simp)
1.205 -    assume "y \<in> I"
1.206 -    then have "I +> y = I" by (rule a_rcos_const)
1.207 -    with b show False by simp
1.208 -  qed
1.209 -
1.210 -  from carr have "x \<otimes> y \<in> I +> x \<otimes> y" by (simp add: a_rcos_self)
1.211 -  then have xyI: "x \<otimes> y \<in> I" by (simp add: a)
1.212 -
1.213 -  from xyI and carr have xI: "x \<in> I \<or> y \<in> I" by (simp add: I_prime)
1.214 -  with ynI have "x \<in> I" by fast
1.215 -  then show "I +> x = I" by (rule a_rcos_const)
1.216 +    and b: "I +> y \<noteq> I" for x y
1.217 +    by (metis I_prime a a_rcos_const a_rcos_self b m_closed that)
1.218 +  show ?thesis
1.219 +    apply (intro domain.intro quotient_is_cring is_cring domain_axioms.intro)
1.220 +     apply (metis "1" FactRing_def monoid.simps(2) ring.simps(1))
1.221 +    apply (simp add: FactRing_simps)
1.222 +    by (metis "2" rcoset_mult_add)
1.223  qed
1.224
1.225  text \<open>Generating right cosets of a prime ideal is a homomorphism
1.226 @@ -210,88 +133,58 @@
1.227
1.228  subsection \<open>Factorization over Maximal Ideals\<close>
1.229
1.230 -text \<open>In a commutative ring, the quotient ring over a maximal ideal
1.231 -        is a field.
1.232 -        The proof follows ``W. Adkins, S. Weintraub: Algebra --
1.233 -        An Approach via Module Theory''\<close>
1.234 -lemma (in maximalideal) quotient_is_field:
1.235 +text \<open>In a commutative ring, the quotient ring over a maximal ideal is a field.
1.236 +        The proof follows ``W. Adkins, S. Weintraub: Algebra -- An Approach via Module Theory''\<close>
1.237 +proposition (in maximalideal) quotient_is_field:
1.238    assumes "cring R"
1.239    shows "field (R Quot I)"
1.240  proof -
1.241    interpret cring R by fact
1.242 -  show ?thesis
1.243 -    apply (intro cring.cring_fieldI2)
1.244 -      apply (rule quotient_is_cring, rule is_cring)
1.245 -     defer 1
1.246 -     apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
1.247 -     apply (simp add: rcoset_mult_add) defer 1
1.248 -  proof (rule ccontr, simp)
1.249 -    \<comment> \<open>Quotient is not empty\<close>
1.250 +  have 1: "\<zero>\<^bsub>R Quot I\<^esub> \<noteq> \<one>\<^bsub>R Quot I\<^esub>"  \<comment> \<open>Quotient is not empty\<close>
1.251 +  proof
1.252      assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
1.253      then have II1: "I = I +> \<one>" by (simp add: FactRing_def)
1.254 -    from a_rcos_self[OF one_closed] have "\<one> \<in> I"
1.255 -      by (simp add: II1[symmetric])
1.256 -    then have "I = carrier R" by (rule one_imp_carrier)
1.257 +    then have "I = carrier R"
1.258 +      using a_rcos_self one_imp_carrier by blast
1.259      with I_notcarr show False by simp
1.260 -  next
1.261 +  qed
1.262 +  have 2: "\<exists>y\<in>carrier R. I +> a \<otimes> y = I +> \<one>" if IanI: "I +> a \<noteq> I" and acarr: "a \<in> carrier R" for a
1.263      \<comment> \<open>Existence of Inverse\<close>
1.264 -    fix a
1.265 -    assume IanI: "I +> a \<noteq> I" and acarr: "a \<in> carrier R"
1.266 -
1.267 +  proof -
1.268      \<comment> \<open>Helper ideal \<open>J\<close>\<close>
1.269      define J :: "'a set" where "J = (carrier R #> a) <+> I"
1.270      have idealJ: "ideal J R"
1.271 -      apply (unfold J_def, rule add_ideals)
1.272 -       apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr)
1.273 -      apply (rule is_ideal)
1.274 -      done
1.275 -
1.276 -    \<comment> \<open>Showing @{term "J"} not smaller than @{term "I"}\<close>
1.277 +      using J_def acarr add_ideals cgenideal_eq_rcos cgenideal_ideal is_ideal by auto
1.278      have IinJ: "I \<subseteq> J"
1.279 -    proof (rule, simp add: J_def r_coset_def set_add_defs)
1.280 +    proof (clarsimp simp: J_def r_coset_def set_add_defs)
1.281        fix x
1.282        assume xI: "x \<in> I"
1.283 -      have Zcarr: "\<zero> \<in> carrier R" by fast
1.284 -      from xI[THEN a_Hcarr] acarr
1.285 -      have "x = \<zero> \<otimes> a \<oplus> x" by algebra
1.286 -      with Zcarr and xI show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
1.287 -    qed
1.288 -
1.289 -    \<comment> \<open>Showing @{term "J \<noteq> I"}\<close>
1.290 -    have anI: "a \<notin> I"
1.291 -    proof (rule ccontr, simp)
1.292 -      assume "a \<in> I"
1.293 -      then have "I +> a = I" by (rule a_rcos_const)
1.294 -      with IanI show False by simp
1.295 +      have "x = \<zero> \<otimes> a \<oplus> x"
1.296 +        by (simp add: acarr xI)
1.297 +      with xI show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
1.298      qed
1.299 -
1.300 -    have aJ: "a \<in> J"
1.301 -    proof (simp add: J_def r_coset_def set_add_defs)
1.302 -      from acarr
1.303 -      have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
1.304 -      with one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup]
1.305 -      show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast
1.306 +    have JnI: "J \<noteq> I"
1.307 +    proof -
1.308 +      have "a \<notin> I"
1.309 +        using IanI a_rcos_const by blast
1.310 +      moreover have "a \<in> J"
1.311 +      proof (simp add: J_def r_coset_def set_add_defs)
1.312 +        from acarr
1.313 +        have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
1.314 +        with one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup]
1.315 +        show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast
1.316 +      qed
1.317 +      ultimately show ?thesis by blast
1.318      qed
1.319 -
1.320 -    from aJ and anI have JnI: "J \<noteq> I" by fast
1.321 -
1.322 -    \<comment> \<open>Deducing @{term "J = carrier R"} because @{term "I"} is maximal\<close>
1.323 -    from idealJ and IinJ have "J = I \<or> J = carrier R"
1.324 -    proof (rule I_maximal, unfold J_def)
1.325 -      have "carrier R #> a \<subseteq> carrier R"
1.326 -        using subset_refl acarr by (rule r_coset_subset_G)
1.327 -      then show "carrier R #> a <+> I \<subseteq> carrier R"
1.328 -        using a_subset by (rule set_add_closed)
1.329 -    qed
1.330 -
1.331 -    with JnI have Jcarr: "J = carrier R" by simp
1.332 +    then have Jcarr: "J = carrier R"
1.333 +      using I_maximal IinJ additive_subgroup.a_subset idealJ ideal_def by blast
1.334
1.335      \<comment> \<open>Calculating an inverse for @{term "a"}\<close>
1.336      from one_closed[folded Jcarr]
1.337 -    have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
1.338 -      by (simp add: J_def r_coset_def set_add_defs)
1.339 -    then obtain r i where rcarr: "r \<in> carrier R"
1.340 -      and iI: "i \<in> I" and one: "\<one> = r \<otimes> a \<oplus> i" by fast
1.341 +    obtain r i where rcarr: "r \<in> carrier R"
1.342 +      and iI: "i \<in> I" and one: "\<one> = r \<otimes> a \<oplus> i"
1.343 +      by (auto simp add: J_def r_coset_def set_add_defs)
1.344 +
1.345      from one and rcarr and acarr and iI[THEN a_Hcarr]
1.346      have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
1.347
1.348 @@ -305,6 +198,10 @@
1.349      from rcarr and this[symmetric]
1.350      show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
1.351    qed
1.352 +  show ?thesis
1.353 +    apply (intro cring.cring_fieldI2 quotient_is_cring is_cring 1)
1.354 +     apply (clarsimp simp add: FactRing_simps rcoset_mult_add 2)
1.355 +    done
1.356  qed
1.357
1.358
1.359 @@ -916,7 +813,7 @@
1.360  proof -
1.361    fix X assume "X \<in> carrier (R Quot (a_kernel R S h))"
1.362    thus "\<exists>x \<in> carrier R. X = (a_kernel R S h) +> x"
1.363 -    unfolding FactRing_def RCOSETS_def A_RCOSETS_def by (simp add: a_r_coset_def)
1.364 +    unfolding FactRing_simps by (simp add: a_r_coset_def)
1.365  qed
1.366
1.367  lemma (in ring_hom_ring) the_elem_wf:
1.368 @@ -989,7 +886,7 @@
1.369        by (metis image_iff)
1.370      hence "the_elem (h ` ((a_kernel R S h) +> x)) = y" by simp
1.371      moreover have "(a_kernel R S h) +> x \<in> carrier (R Quot (a_kernel R S h))"
1.372 -     unfolding FactRing_def RCOSETS_def A_RCOSETS_def by (auto simp add: x a_r_coset_def)
1.373 +     unfolding FactRing_simps by (auto simp add: x a_r_coset_def)
1.374      ultimately show "y \<in> (\<lambda>X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h))" by blast
1.375    qed
1.376  qed
```
```     2.1 --- a/src/HOL/Algebra/Ring.thy	Sun Jul 22 13:00:38 2018 +0200
2.2 +++ b/src/HOL/Algebra/Ring.thy	Sun Jul 22 13:29:41 2018 +0200
2.3 @@ -332,7 +332,7 @@
2.4    assumes "cring R"
2.5    shows "comm_monoid R"
2.6      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"
2.7 -  using assms cring_def apply auto by (simp add: assms cring.axioms(1) ringE(3))
2.8 +  using assms cring_def by auto (simp add: assms cring.axioms(1) ringE(3))
2.9
2.10  lemma (in cring) is_cring:
2.11    "cring R" by (rule cring_axioms)
2.12 @@ -481,10 +481,7 @@
2.13  qed
2.14
2.15  lemma carrier_one_zero: "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
2.16 -  apply rule
2.17 -   apply (erule one_zeroI)
2.18 -  apply (erule one_zeroD)
2.19 -  done
2.20 +  using one_zeroD by blast
2.21
2.22  lemma carrier_one_not_zero: "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
2.23    by (simp add: carrier_one_zero)
2.24 @@ -687,19 +684,22 @@
2.25  text \<open>Another variant to show that something is a field\<close>
2.26  lemma (in cring) cring_fieldI2:
2.27    assumes notzero: "\<zero> \<noteq> \<one>"
2.28 -  and invex: "\<And>a. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a \<otimes> b = \<one>"
2.29 +    and invex: "\<And>a. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a \<otimes> b = \<one>"
2.30    shows "field R"
2.31 -  apply (rule cring_fieldI, simp add: Units_def)
2.32 -  apply (rule, clarsimp)
2.33 -  apply (simp add: notzero)
2.34 -proof (clarsimp)
2.35 -  fix x
2.36 -  assume xcarr: "x \<in> carrier R"
2.37 -    and "x \<noteq> \<zero>"
2.38 -  then have "\<exists>y\<in>carrier R. x \<otimes> y = \<one>" by (rule invex)
2.39 -  then obtain y where ycarr: "y \<in> carrier R" and xy: "x \<otimes> y = \<one>" by fast
2.40 -  from xy xcarr ycarr have "y \<otimes> x = \<one>" by (simp add: m_comm)
2.41 -  with ycarr and xy show "\<exists>y\<in>carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast
2.42 +proof -
2.43 +  have *: "carrier R - {\<zero>} \<subseteq> {y \<in> carrier R. \<exists>x\<in>carrier R. x \<otimes> y = \<one> \<and> y \<otimes> x = \<one>}"
2.44 +  proof (clarsimp)
2.45 +    fix x
2.46 +    assume xcarr: "x \<in> carrier R" and "x \<noteq> \<zero>"
2.47 +    obtain y where ycarr: "y \<in> carrier R" and xy: "x \<otimes> y = \<one>"
2.48 +      using \<open>x \<noteq> \<zero>\<close> invex xcarr by blast
2.49 +    with ycarr and xy show "\<exists>y\<in>carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>"
2.50 +      using m_comm xcarr by fastforce
2.51 +  qed
2.52 +  show ?thesis
2.53 +    apply (rule cring_fieldI, simp add: Units_def)
2.54 +    using *
2.55 +    using group_l_invI notzero set_diff_eq by auto
2.56  qed
2.57
2.58
2.59 @@ -859,57 +859,36 @@
2.60
2.61  subsection\<open>Jeremy Avigad's @{text"More_Ring"} material\<close>
2.62
2.63 -lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> \<noteq> \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
2.64 -  apply (unfold_locales)
2.65 -    apply (use cring_axioms in auto)
2.66 -   apply (rule trans)
2.67 -    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
2.68 -     apply assumption
2.69 -    apply (subst m_assoc)
2.70 -       apply auto
2.71 -  apply (unfold Units_def)
2.72 -  apply auto
2.73 -  done
2.74 +lemma (in cring) field_intro2:
2.75 +  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"
2.76 +  shows "field R"
2.77 +proof unfold_locales
2.78 +  show "\<one> \<noteq> \<zero>" using assms by auto
2.79 +  show "\<lbrakk>a \<otimes> b = \<zero>; a \<in> carrier R;
2.80 +            b \<in> carrier R\<rbrakk>
2.81 +           \<Longrightarrow> a = \<zero> \<or> b = \<zero>" for a b
2.82 +    by (metis un Units_l_cancel insert_Diff_single insert_iff r_null zero_closed)
2.83 +qed (use assms in \<open>auto simp: Units_def\<close>)
2.84
2.85  lemma (in monoid) inv_char:
2.86 -  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
2.87 -  apply (subgoal_tac "x \<in> Units G")
2.88 -   apply (subgoal_tac "y = inv x \<otimes> \<one>")
2.89 -    apply simp
2.90 -   apply (erule subst)
2.91 -   apply (subst m_assoc [symmetric])
2.92 -      apply auto
2.93 -  apply (unfold Units_def)
2.94 -  apply auto
2.95 -  done
2.96 +  assumes "x \<in> carrier G" "y \<in> carrier G" "x \<otimes> y = \<one>" "y \<otimes> x = \<one>"
2.97 +  shows "inv x = y"
2.98 +  using assms inv_unique' by auto
2.99
2.100  lemma (in comm_monoid) comm_inv_char: "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
2.101    by (simp add: inv_char m_comm)
2.102
2.103  lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
2.104 -  apply (rule inv_char)
2.105 -     apply (auto simp add: l_minus r_minus)
2.106 -  done
2.107 +  by (simp add: inv_char local.ring_axioms ring.r_minus)
2.108
2.109  lemma (in monoid) inv_eq_imp_eq: "x \<in> Units G \<Longrightarrow> y \<in> Units G \<Longrightarrow> inv x = inv y \<Longrightarrow> x = y"
2.110 -  apply (subgoal_tac "inv (inv x) = inv (inv y)")
2.111 -   apply (subst (asm) Units_inv_inv)+
2.112 -    apply auto
2.113 -  done
2.114 +  by (metis Units_inv_inv)
2.115
2.116  lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
2.117 -  apply (unfold Units_def)
2.118 -  apply auto
2.119 -  apply (rule_tac x = "\<ominus> \<one>" in bexI)
2.120 -   apply auto
2.121 -  apply (simp add: l_minus r_minus)
2.122 -  done
2.123 +  by (simp add: Units_def) (metis add.l_inv_ex local.minus_minus minus_equality one_closed r_minus r_one)
2.124
2.125  lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
2.126 -  apply auto
2.127 -  apply (subst Units_inv_inv [symmetric])
2.128 -   apply auto
2.129 -  done
2.130 +  by (metis Units_inv_inv inv_neg_one)
2.131
2.132  lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
2.133    by (metis Units_inv_inv inv_one)
```