--- a/src/HOL/Algebra/QuotRing.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/Algebra/QuotRing.thy Tue Jan 16 09:30:00 2018 +0100
@@ -84,28 +84,28 @@
text \<open>The quotient is a ring\<close>
lemma (in ideal) quotient_is_ring: "ring (R Quot I)"
apply (rule ringI)
- \<comment>\<open>abelian group\<close>
+ \<comment> \<open>abelian group\<close>
apply (rule comm_group_abelian_groupI)
apply (simp add: FactRing_def)
apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def'])
- \<comment>\<open>mult monoid\<close>
+ \<comment> \<open>mult monoid\<close>
apply (rule monoidI)
apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def
a_r_coset_def[symmetric])
- \<comment>\<open>mult closed\<close>
+ \<comment> \<open>mult closed\<close>
apply (clarify)
apply (simp add: rcoset_mult_add, fast)
- \<comment>\<open>mult \<open>one_closed\<close>\<close>
+ \<comment> \<open>mult \<open>one_closed\<close>\<close>
apply force
- \<comment>\<open>mult assoc\<close>
+ \<comment> \<open>mult assoc\<close>
apply clarify
apply (simp add: rcoset_mult_add m_assoc)
- \<comment>\<open>mult one\<close>
+ \<comment> \<open>mult one\<close>
apply clarify
apply (simp add: rcoset_mult_add)
apply clarify
apply (simp add: rcoset_mult_add)
- \<comment>\<open>distr\<close>
+ \<comment> \<open>distr\<close>
apply clarify
apply (simp add: rcoset_mult_add a_rcos_sum l_distr)
apply clarify
@@ -225,7 +225,7 @@
apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
apply (simp add: rcoset_mult_add) defer 1
proof (rule ccontr, simp)
- \<comment>\<open>Quotient is not empty\<close>
+ \<comment> \<open>Quotient is not empty\<close>
assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
then have II1: "I = I +> \<one>" by (simp add: FactRing_def)
from a_rcos_self[OF one_closed] have "\<one> \<in> I"
@@ -233,11 +233,11 @@
then have "I = carrier R" by (rule one_imp_carrier)
with I_notcarr show False by simp
next
- \<comment>\<open>Existence of Inverse\<close>
+ \<comment> \<open>Existence of Inverse\<close>
fix a
assume IanI: "I +> a \<noteq> I" and acarr: "a \<in> carrier R"
- \<comment>\<open>Helper ideal \<open>J\<close>\<close>
+ \<comment> \<open>Helper ideal \<open>J\<close>\<close>
define J :: "'a set" where "J = (carrier R #> a) <+> I"
have idealJ: "ideal J R"
apply (unfold J_def, rule add_ideals)
@@ -245,7 +245,7 @@
apply (rule is_ideal)
done
- \<comment>\<open>Showing @{term "J"} not smaller than @{term "I"}\<close>
+ \<comment> \<open>Showing @{term "J"} not smaller than @{term "I"}\<close>
have IinJ: "I \<subseteq> J"
proof (rule, simp add: J_def r_coset_def set_add_defs)
fix x
@@ -256,7 +256,7 @@
with Zcarr and xI show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
qed
- \<comment>\<open>Showing @{term "J \<noteq> I"}\<close>
+ \<comment> \<open>Showing @{term "J \<noteq> I"}\<close>
have anI: "a \<notin> I"
proof (rule ccontr, simp)
assume "a \<in> I"
@@ -274,7 +274,7 @@
from aJ and anI have JnI: "J \<noteq> I" by fast
- \<comment>\<open>Deducing @{term "J = carrier R"} because @{term "I"} is maximal\<close>
+ \<comment> \<open>Deducing @{term "J = carrier R"} because @{term "I"} is maximal\<close>
from idealJ and IinJ have "J = I \<or> J = carrier R"
proof (rule I_maximal, unfold J_def)
have "carrier R #> a \<subseteq> carrier R"
@@ -285,7 +285,7 @@
with JnI have Jcarr: "J = carrier R" by simp
- \<comment>\<open>Calculating an inverse for @{term "a"}\<close>
+ \<comment> \<open>Calculating an inverse for @{term "a"}\<close>
from one_closed[folded Jcarr]
have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
by (simp add: J_def r_coset_def set_add_defs)
@@ -294,7 +294,7 @@
from one and rcarr and acarr and iI[THEN a_Hcarr]
have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
- \<comment>\<open>Lifting to cosets\<close>
+ \<comment> \<open>Lifting to cosets\<close>
from iI have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
by (intro a_rcosI, simp, intro a_subset, simp)
with rai1 have "a \<otimes> r \<in> I +> \<one>" by simp