tuned proofs;
authorwenzelm
Mon Sep 19 23:18:18 2011 +0200 (2011-09-19)
changeset 450050d2d59525912
parent 45004 5bd261075711
child 45006 11a542f50fc3
tuned proofs;
src/HOL/Algebra/QuotRing.thy
     1.1 --- a/src/HOL/Algebra/QuotRing.thy	Mon Sep 19 22:48:05 2011 +0200
     1.2 +++ b/src/HOL/Algebra/QuotRing.thy	Mon Sep 19 23:18:18 2011 +0200
     1.3 @@ -10,8 +10,7 @@
     1.4  
     1.5  subsection {* Multiplication on Cosets *}
     1.6  
     1.7 -definition
     1.8 -  rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
     1.9 +definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
    1.10      ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
    1.11    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.12  
    1.13 @@ -19,86 +18,71 @@
    1.14  text {* @{const "rcoset_mult"} fulfils the properties required by
    1.15    congruences *}
    1.16  lemma (in ideal) rcoset_mult_add:
    1.17 -  "\<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> [mod I:] (I +> x) \<Otimes> (I +> y) = I +> (x \<otimes> y)"
    1.18 -apply rule
    1.19 -apply (rule, simp add: rcoset_mult_def, clarsimp)
    1.20 -defer 1
    1.21 -apply (rule, simp add: rcoset_mult_def)
    1.22 -defer 1
    1.23 +    "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> [mod I:] (I +> x) \<Otimes> (I +> y) = I +> (x \<otimes> y)"
    1.24 +  apply rule
    1.25 +  apply (rule, simp add: rcoset_mult_def, clarsimp)
    1.26 +  defer 1
    1.27 +  apply (rule, simp add: rcoset_mult_def)
    1.28 +  defer 1
    1.29  proof -
    1.30    fix z x' y'
    1.31    assume carr: "x \<in> carrier R" "y \<in> carrier R"
    1.32 -     and x'rcos: "x' \<in> I +> x"
    1.33 -     and y'rcos: "y' \<in> I +> y"
    1.34 -     and zrcos: "z \<in> I +> x' \<otimes> y'"
    1.35 +    and x'rcos: "x' \<in> I +> x"
    1.36 +    and y'rcos: "y' \<in> I +> y"
    1.37 +    and zrcos: "z \<in> I +> x' \<otimes> y'"
    1.38 +
    1.39 +  from x'rcos have "\<exists>h\<in>I. x' = h \<oplus> x"
    1.40 +    by (simp add: a_r_coset_def r_coset_def)
    1.41 +  then obtain hx where hxI: "hx \<in> I" and x': "x' = hx \<oplus> x"
    1.42 +    by fast+
    1.43  
    1.44 -  from x'rcos 
    1.45 -      have "\<exists>h\<in>I. x' = h \<oplus> x" by (simp add: a_r_coset_def r_coset_def)
    1.46 -  from this obtain hx
    1.47 -      where hxI: "hx \<in> I"
    1.48 -      and x': "x' = hx \<oplus> x"
    1.49 -      by fast+
    1.50 -  
    1.51 -  from y'rcos
    1.52 -      have "\<exists>h\<in>I. y' = h \<oplus> y" by (simp add: a_r_coset_def r_coset_def)
    1.53 -  from this
    1.54 -      obtain hy
    1.55 -      where hyI: "hy \<in> I"
    1.56 -      and y': "y' = hy \<oplus> y"
    1.57 -      by fast+
    1.58 +  from y'rcos have "\<exists>h\<in>I. y' = h \<oplus> y"
    1.59 +    by (simp add: a_r_coset_def r_coset_def)
    1.60 +  then obtain hy where hyI: "hy \<in> I" and y': "y' = hy \<oplus> y"
    1.61 +    by fast+
    1.62  
    1.63 -  from zrcos
    1.64 -      have "\<exists>h\<in>I. z = h \<oplus> (x' \<otimes> y')" by (simp add: a_r_coset_def r_coset_def)
    1.65 -  from this
    1.66 -      obtain hz
    1.67 -      where hzI: "hz \<in> I"
    1.68 -      and z: "z = hz \<oplus> (x' \<otimes> y')"
    1.69 -      by fast+
    1.70 +  from zrcos have "\<exists>h\<in>I. z = h \<oplus> (x' \<otimes> y')"
    1.71 +    by (simp add: a_r_coset_def r_coset_def)
    1.72 +  then obtain hz where hzI: "hz \<in> I" and z: "z = hz \<oplus> (x' \<otimes> y')"
    1.73 +    by fast+
    1.74  
    1.75    note carr = carr hxI[THEN a_Hcarr] hyI[THEN a_Hcarr] hzI[THEN a_Hcarr]
    1.76  
    1.77    from z have "z = hz \<oplus> (x' \<otimes> y')" .
    1.78 -  also from x' y'
    1.79 -      have "\<dots> = hz \<oplus> ((hx \<oplus> x) \<otimes> (hy \<oplus> y))" by simp
    1.80 -  also from carr
    1.81 -      have "\<dots> = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" by algebra
    1.82 -  finally
    1.83 -      have z2: "z = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" .
    1.84 +  also from x' y' have "\<dots> = hz \<oplus> ((hx \<oplus> x) \<otimes> (hy \<oplus> y))" by simp
    1.85 +  also from carr have "\<dots> = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" by algebra
    1.86 +  finally have z2: "z = (hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy) \<oplus> x \<otimes> y" .
    1.87  
    1.88 -  from hxI hyI hzI carr
    1.89 -      have "hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy \<in> I"  by (simp add: I_l_closed I_r_closed)
    1.90 +  from hxI hyI hzI carr have "hz \<oplus> (hx \<otimes> (hy \<oplus> y)) \<oplus> x \<otimes> hy \<in> I"
    1.91 +    by (simp add: I_l_closed I_r_closed)
    1.92  
    1.93 -  from this and z2
    1.94 -      have "\<exists>h\<in>I. z = h \<oplus> x \<otimes> y" by fast
    1.95 -  thus "z \<in> I +> x \<otimes> y" by (simp add: a_r_coset_def r_coset_def)
    1.96 +  with z2 have "\<exists>h\<in>I. z = h \<oplus> x \<otimes> y" by fast
    1.97 +  then show "z \<in> I +> x \<otimes> y" by (simp add: a_r_coset_def r_coset_def)
    1.98  next
    1.99    fix z
   1.100    assume xcarr: "x \<in> carrier R"
   1.101 -     and ycarr: "y \<in> carrier R"
   1.102 -     and zrcos: "z \<in> I +> x \<otimes> y"
   1.103 -  from xcarr
   1.104 -      have xself: "x \<in> I +> x" by (intro a_rcos_self)
   1.105 -  from ycarr
   1.106 -      have yself: "y \<in> I +> y" by (intro a_rcos_self)
   1.107 -
   1.108 -  from xself and yself and zrcos
   1.109 -      show "\<exists>a\<in>I +> x. \<exists>b\<in>I +> y. z \<in> I +> a \<otimes> b" by fast
   1.110 +    and ycarr: "y \<in> carrier R"
   1.111 +    and zrcos: "z \<in> I +> x \<otimes> y"
   1.112 +  from xcarr have xself: "x \<in> I +> x" by (intro a_rcos_self)
   1.113 +  from ycarr have yself: "y \<in> I +> y" by (intro a_rcos_self)
   1.114 +  show "\<exists>a\<in>I +> x. \<exists>b\<in>I +> y. z \<in> I +> a \<otimes> b"
   1.115 +    using xself and yself and zrcos by fast
   1.116  qed
   1.117  
   1.118  
   1.119  subsection {* Quotient Ring Definition *}
   1.120  
   1.121 -definition
   1.122 -  FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"  (infixl "Quot" 65)
   1.123 +definition FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"
   1.124 +    (infixl "Quot" 65)
   1.125    where "FactRing R I =
   1.126 -    \<lparr>carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I, one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"
   1.127 +    \<lparr>carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I,
   1.128 +      one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"
   1.129  
   1.130  
   1.131  subsection {* Factorization over General Ideals *}
   1.132  
   1.133  text {* The quotient is a ring *}
   1.134 -lemma (in ideal) quotient_is_ring:
   1.135 -  shows "ring (R Quot I)"
   1.136 +lemma (in ideal) quotient_is_ring: "ring (R Quot I)"
   1.137  apply (rule ringI)
   1.138     --{* abelian group *}
   1.139     apply (rule comm_group_abelian_groupI)
   1.140 @@ -112,15 +96,15 @@
   1.141        apply (clarify)
   1.142        apply (simp add: rcoset_mult_add, fast)
   1.143       --{* mult @{text one_closed} *}
   1.144 -     apply (force intro: one_closed)
   1.145 +     apply force
   1.146      --{* mult assoc *}
   1.147      apply clarify
   1.148      apply (simp add: rcoset_mult_add m_assoc)
   1.149     --{* mult one *}
   1.150     apply clarify
   1.151 -   apply (simp add: rcoset_mult_add l_one)
   1.152 +   apply (simp add: rcoset_mult_add)
   1.153    apply clarify
   1.154 -  apply (simp add: rcoset_mult_add r_one)
   1.155 +  apply (simp add: rcoset_mult_add)
   1.156   --{* distr *}
   1.157   apply clarify
   1.158   apply (simp add: rcoset_mult_add a_rcos_sum l_distr)
   1.159 @@ -131,8 +115,7 @@
   1.160  
   1.161  text {* This is a ring homomorphism *}
   1.162  
   1.163 -lemma (in ideal) rcos_ring_hom:
   1.164 -  "(op +> I) \<in> ring_hom R (R Quot I)"
   1.165 +lemma (in ideal) rcos_ring_hom: "(op +> I) \<in> ring_hom R (R Quot I)"
   1.166  apply (rule ring_hom_memI)
   1.167     apply (simp add: FactRing_def a_rcosetsI[OF a_subset])
   1.168    apply (simp add: FactRing_def rcoset_mult_add)
   1.169 @@ -140,8 +123,7 @@
   1.170  apply (simp add: FactRing_def)
   1.171  done
   1.172  
   1.173 -lemma (in ideal) rcos_ring_hom_ring:
   1.174 -  "ring_hom_ring R (R Quot I) (op +> I)"
   1.175 +lemma (in ideal) rcos_ring_hom_ring: "ring_hom_ring R (R Quot I) (op +> I)"
   1.176  apply (rule ring_hom_ringI)
   1.177       apply (rule is_ring, rule quotient_is_ring)
   1.178     apply (simp add: FactRing_def a_rcosetsI[OF a_subset])
   1.179 @@ -156,13 +138,14 @@
   1.180    shows "cring (R Quot I)"
   1.181  proof -
   1.182    interpret cring R by fact
   1.183 -  show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
   1.184 -  apply (rule quotient_is_ring)
   1.185 - apply (rule ring.axioms[OF quotient_is_ring])
   1.186 -apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric])
   1.187 -apply clarify
   1.188 -apply (simp add: rcoset_mult_add m_comm)
   1.189 -done
   1.190 +  show ?thesis
   1.191 +    apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
   1.192 +      apply (rule quotient_is_ring)
   1.193 +     apply (rule ring.axioms[OF quotient_is_ring])
   1.194 +    apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric])
   1.195 +    apply clarify
   1.196 +    apply (simp add: rcoset_mult_add m_comm)
   1.197 +    done
   1.198  qed
   1.199  
   1.200  text {* Cosets as a ring homomorphism on crings *}
   1.201 @@ -171,65 +154,57 @@
   1.202    shows "ring_hom_cring R (R Quot I) (op +> I)"
   1.203  proof -
   1.204    interpret cring R by fact
   1.205 -  show ?thesis apply (rule ring_hom_cringI)
   1.206 -  apply (rule rcos_ring_hom_ring)
   1.207 - apply (rule is_cring)
   1.208 -apply (rule quotient_is_cring)
   1.209 -apply (rule is_cring)
   1.210 -done
   1.211 +  show ?thesis
   1.212 +    apply (rule ring_hom_cringI)
   1.213 +      apply (rule rcos_ring_hom_ring)
   1.214 +     apply (rule is_cring)
   1.215 +    apply (rule quotient_is_cring)
   1.216 +   apply (rule is_cring)
   1.217 +   done
   1.218  qed
   1.219  
   1.220  
   1.221  subsection {* Factorization over Prime Ideals *}
   1.222  
   1.223  text {* The quotient ring generated by a prime ideal is a domain *}
   1.224 -lemma (in primeideal) quotient_is_domain:
   1.225 -  shows "domain (R Quot I)"
   1.226 -apply (rule domain.intro)
   1.227 - apply (rule quotient_is_cring, rule is_cring)
   1.228 -apply (rule domain_axioms.intro)
   1.229 - apply (simp add: FactRing_def) defer 1
   1.230 - apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarify)
   1.231 - apply (simp add: rcoset_mult_add) defer 1
   1.232 +lemma (in primeideal) quotient_is_domain: "domain (R Quot I)"
   1.233 +  apply (rule domain.intro)
   1.234 +   apply (rule quotient_is_cring, rule is_cring)
   1.235 +  apply (rule domain_axioms.intro)
   1.236 +   apply (simp add: FactRing_def) defer 1
   1.237 +    apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarify)
   1.238 +    apply (simp add: rcoset_mult_add) defer 1
   1.239  proof (rule ccontr, clarsimp)
   1.240    assume "I +> \<one> = I"
   1.241 -  hence "\<one> \<in> I" by (simp only: a_coset_join1 one_closed a_subgroup)
   1.242 -  hence "carrier R \<subseteq> I" by (subst one_imp_carrier, simp, fast)
   1.243 -  from this and a_subset
   1.244 -      have "I = carrier R" by fast
   1.245 -  from this and I_notcarr
   1.246 -      show "False" by fast
   1.247 +  then have "\<one> \<in> I" by (simp only: a_coset_join1 one_closed a_subgroup)
   1.248 +  then have "carrier R \<subseteq> I" by (subst one_imp_carrier, simp, fast)
   1.249 +  with a_subset have "I = carrier R" by fast
   1.250 +  with I_notcarr show False by fast
   1.251  next
   1.252    fix x y
   1.253    assume carr: "x \<in> carrier R" "y \<in> carrier R"
   1.254 -     and a: "I +> x \<otimes> y = I"
   1.255 -     and b: "I +> y \<noteq> I"
   1.256 +    and a: "I +> x \<otimes> y = I"
   1.257 +    and b: "I +> y \<noteq> I"
   1.258  
   1.259    have ynI: "y \<notin> I"
   1.260    proof (rule ccontr, simp)
   1.261      assume "y \<in> I"
   1.262 -    hence "I +> y = I" by (rule a_rcos_const)
   1.263 -    from this and b
   1.264 -        show "False" by simp
   1.265 +    then have "I +> y = I" by (rule a_rcos_const)
   1.266 +    with b show False by simp
   1.267    qed
   1.268  
   1.269 -  from carr
   1.270 -      have "x \<otimes> y \<in> I +> x \<otimes> y" by (simp add: a_rcos_self)
   1.271 -  from this
   1.272 -      have xyI: "x \<otimes> y \<in> I" by (simp add: a)
   1.273 +  from carr have "x \<otimes> y \<in> I +> x \<otimes> y" by (simp add: a_rcos_self)
   1.274 +  then have xyI: "x \<otimes> y \<in> I" by (simp add: a)
   1.275  
   1.276 -  from xyI and carr
   1.277 -      have xI: "x \<in> I \<or> y \<in> I" by (simp add: I_prime)
   1.278 -  from this and ynI
   1.279 -      have "x \<in> I" by fast
   1.280 -  thus "I +> x = I" by (rule a_rcos_const)
   1.281 +  from xyI and carr have xI: "x \<in> I \<or> y \<in> I" by (simp add: I_prime)
   1.282 +  with ynI have "x \<in> I" by fast
   1.283 +  then show "I +> x = I" by (rule a_rcos_const)
   1.284  qed
   1.285  
   1.286  text {* Generating right cosets of a prime ideal is a homomorphism
   1.287          on commutative rings *}
   1.288 -lemma (in primeideal) rcos_ring_hom_cring:
   1.289 -  shows "ring_hom_cring R (R Quot I) (op +> I)"
   1.290 -by (rule rcos_ring_hom_cring, rule is_cring)
   1.291 +lemma (in primeideal) rcos_ring_hom_cring: "ring_hom_cring R (R Quot I) (op +> I)"
   1.292 +  by (rule rcos_ring_hom_cring) (rule is_cring)
   1.293  
   1.294  
   1.295  subsection {* Factorization over Maximal Ideals *}
   1.296 @@ -243,106 +218,92 @@
   1.297    shows "field (R Quot I)"
   1.298  proof -
   1.299    interpret cring R by fact
   1.300 -  show ?thesis apply (intro cring.cring_fieldI2)
   1.301 -  apply (rule quotient_is_cring, rule is_cring)
   1.302 - defer 1
   1.303 - apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
   1.304 - apply (simp add: rcoset_mult_add) defer 1
   1.305 -proof (rule ccontr, simp)
   1.306 -  --{* Quotient is not empty *}
   1.307 -  assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
   1.308 -  hence II1: "I = I +> \<one>" by (simp add: FactRing_def)
   1.309 -  from a_rcos_self[OF one_closed]
   1.310 -  have "\<one> \<in> I" by (simp add: II1[symmetric])
   1.311 -  hence "I = carrier R" by (rule one_imp_carrier)
   1.312 -  from this and I_notcarr
   1.313 -  show "False" by simp
   1.314 -next
   1.315 -  --{* Existence of Inverse *}
   1.316 -  fix a
   1.317 -  assume IanI: "I +> a \<noteq> I"
   1.318 -    and acarr: "a \<in> carrier R"
   1.319 +  show ?thesis
   1.320 +    apply (intro cring.cring_fieldI2)
   1.321 +      apply (rule quotient_is_cring, rule is_cring)
   1.322 +     defer 1
   1.323 +     apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
   1.324 +     apply (simp add: rcoset_mult_add) defer 1
   1.325 +  proof (rule ccontr, simp)
   1.326 +    --{* Quotient is not empty *}
   1.327 +    assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
   1.328 +    then have II1: "I = I +> \<one>" by (simp add: FactRing_def)
   1.329 +    from a_rcos_self[OF one_closed] have "\<one> \<in> I"
   1.330 +      by (simp add: II1[symmetric])
   1.331 +    then have "I = carrier R" by (rule one_imp_carrier)
   1.332 +    with I_notcarr show False by simp
   1.333 +  next
   1.334 +    --{* Existence of Inverse *}
   1.335 +    fix a
   1.336 +    assume IanI: "I +> a \<noteq> I" and acarr: "a \<in> carrier R"
   1.337  
   1.338 -  --{* Helper ideal @{text "J"} *}
   1.339 -  def J \<equiv> "(carrier R #> a) <+> I :: 'a set"
   1.340 -  have idealJ: "ideal J R"
   1.341 -    apply (unfold J_def, rule add_ideals)
   1.342 -     apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr)
   1.343 -    apply (rule is_ideal)
   1.344 -    done
   1.345 +    --{* Helper ideal @{text "J"} *}
   1.346 +    def J \<equiv> "(carrier R #> a) <+> I :: 'a set"
   1.347 +    have idealJ: "ideal J R"
   1.348 +      apply (unfold J_def, rule add_ideals)
   1.349 +       apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr)
   1.350 +      apply (rule is_ideal)
   1.351 +      done
   1.352  
   1.353 -  --{* Showing @{term "J"} not smaller than @{term "I"} *}
   1.354 -  have IinJ: "I \<subseteq> J"
   1.355 -  proof (rule, simp add: J_def r_coset_def set_add_defs)
   1.356 -    fix x
   1.357 -    assume xI: "x \<in> I"
   1.358 -    have Zcarr: "\<zero> \<in> carrier R" by fast
   1.359 -    from xI[THEN a_Hcarr] acarr
   1.360 -    have "x = \<zero> \<otimes> a \<oplus> x" by algebra
   1.361 -
   1.362 -    from Zcarr and xI and this
   1.363 -    show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
   1.364 -  qed
   1.365 -
   1.366 -  --{* Showing @{term "J \<noteq> I"} *}
   1.367 -  have anI: "a \<notin> I"
   1.368 -  proof (rule ccontr, simp)
   1.369 -    assume "a \<in> I"
   1.370 -    hence "I +> a = I" by (rule a_rcos_const)
   1.371 -    from this and IanI
   1.372 -    show "False" by simp
   1.373 -  qed
   1.374 +    --{* Showing @{term "J"} not smaller than @{term "I"} *}
   1.375 +    have IinJ: "I \<subseteq> J"
   1.376 +    proof (rule, simp add: J_def r_coset_def set_add_defs)
   1.377 +      fix x
   1.378 +      assume xI: "x \<in> I"
   1.379 +      have Zcarr: "\<zero> \<in> carrier R" by fast
   1.380 +      from xI[THEN a_Hcarr] acarr
   1.381 +      have "x = \<zero> \<otimes> a \<oplus> x" by algebra
   1.382 +      with Zcarr and xI show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
   1.383 +    qed
   1.384  
   1.385 -  have aJ: "a \<in> J"
   1.386 -  proof (simp add: J_def r_coset_def set_add_defs)
   1.387 -    from acarr
   1.388 -    have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
   1.389 -    from one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup] and this
   1.390 -    show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast
   1.391 -  qed
   1.392 -
   1.393 -  from aJ and anI
   1.394 -  have JnI: "J \<noteq> I" by fast
   1.395 +    --{* Showing @{term "J \<noteq> I"} *}
   1.396 +    have anI: "a \<notin> I"
   1.397 +    proof (rule ccontr, simp)
   1.398 +      assume "a \<in> I"
   1.399 +      then have "I +> a = I" by (rule a_rcos_const)
   1.400 +      with IanI show False by simp
   1.401 +    qed
   1.402  
   1.403 -  --{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *}
   1.404 -  from idealJ and IinJ
   1.405 -  have "J = I \<or> J = carrier R"
   1.406 -  proof (rule I_maximal, unfold J_def)
   1.407 -    have "carrier R #> a \<subseteq> carrier R"
   1.408 -      using subset_refl acarr
   1.409 -      by (rule r_coset_subset_G)
   1.410 -    from this and a_subset
   1.411 -    show "carrier R #> a <+> I \<subseteq> carrier R" by (rule set_add_closed)
   1.412 -  qed
   1.413 +    have aJ: "a \<in> J"
   1.414 +    proof (simp add: J_def r_coset_def set_add_defs)
   1.415 +      from acarr
   1.416 +      have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
   1.417 +      with one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup]
   1.418 +      show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast
   1.419 +    qed
   1.420  
   1.421 -  from this and JnI
   1.422 -  have Jcarr: "J = carrier R" by simp
   1.423 +    from aJ and anI have JnI: "J \<noteq> I" by fast
   1.424  
   1.425 -  --{* Calculating an inverse for @{term "a"} *}
   1.426 -  from one_closed[folded Jcarr]
   1.427 -  have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
   1.428 -    by (simp add: J_def r_coset_def set_add_defs)
   1.429 -  from this
   1.430 -  obtain r i
   1.431 -    where rcarr: "r \<in> carrier R"
   1.432 -      and iI: "i \<in> I"
   1.433 -      and one: "\<one> = r \<otimes> a \<oplus> i"
   1.434 -    by fast
   1.435 -  from one and rcarr and acarr and iI[THEN a_Hcarr]
   1.436 -  have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
   1.437 +    --{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *}
   1.438 +    from idealJ and IinJ have "J = I \<or> J = carrier R"
   1.439 +    proof (rule I_maximal, unfold J_def)
   1.440 +      have "carrier R #> a \<subseteq> carrier R"
   1.441 +        using subset_refl acarr by (rule r_coset_subset_G)
   1.442 +      then show "carrier R #> a <+> I \<subseteq> carrier R"
   1.443 +        using a_subset by (rule set_add_closed)
   1.444 +    qed
   1.445 +
   1.446 +    with JnI have Jcarr: "J = carrier R" by simp
   1.447  
   1.448 -  --{* Lifting to cosets *}
   1.449 -  from iI
   1.450 -  have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
   1.451 -    by (intro a_rcosI, simp, intro a_subset, simp)
   1.452 -  from this and rai1
   1.453 -  have "a \<otimes> r \<in> I +> \<one>" by simp
   1.454 -  from this have "I +> \<one> = I +> a \<otimes> r"
   1.455 -    by (rule a_repr_independence, simp) (rule a_subgroup)
   1.456 +    --{* Calculating an inverse for @{term "a"} *}
   1.457 +    from one_closed[folded Jcarr]
   1.458 +    have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
   1.459 +      by (simp add: J_def r_coset_def set_add_defs)
   1.460 +    then obtain r i where rcarr: "r \<in> carrier R"
   1.461 +      and iI: "i \<in> I" and one: "\<one> = r \<otimes> a \<oplus> i" by fast
   1.462 +    from one and rcarr and acarr and iI[THEN a_Hcarr]
   1.463 +    have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
   1.464  
   1.465 -  from rcarr and this[symmetric]
   1.466 -  show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
   1.467 -qed
   1.468 +    --{* Lifting to cosets *}
   1.469 +    from iI have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
   1.470 +      by (intro a_rcosI, simp, intro a_subset, simp)
   1.471 +    with rai1 have "a \<otimes> r \<in> I +> \<one>" by simp
   1.472 +    then have "I +> \<one> = I +> a \<otimes> r"
   1.473 +      by (rule a_repr_independence, simp) (rule a_subgroup)
   1.474 +
   1.475 +    from rcarr and this[symmetric]
   1.476 +    show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
   1.477 +  qed
   1.478  qed
   1.479  
   1.480  end