merged
authorpaulson
Sun Jul 22 13:29:41 2018 +0200 (12 months ago)
changeset 68674f4ac69fe4509
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.118 -   apply (simp add: rcoset_mult_add)
   1.119 -  apply clarify
   1.120 -  apply (simp add: rcoset_mult_add)
   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)