src/HOL/Algebra/QuotRing.thy
changeset 23350 50c5b0912a0c
parent 21502 7f3ea2b3bab6
child 23463 9953ff53cc64
--- a/src/HOL/Algebra/QuotRing.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -247,23 +247,23 @@
   assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
   hence II1: "I = I +> \<one>" by (simp add: FactRing_def)
   from a_rcos_self[OF one_closed]
-      have "\<one> \<in> I" by (simp add: II1[symmetric])
+  have "\<one> \<in> I" by (simp add: II1[symmetric])
   hence "I = carrier R" by (rule one_imp_carrier)
   from this and I_notcarr
-      show "False" by simp
+  show "False" by simp
 next
   --{* Existence of Inverse *}
   fix a
   assume IanI: "I +> a \<noteq> I"
-     and acarr: "a \<in> carrier R"
+    and acarr: "a \<in> carrier R"
 
   --{* Helper ideal @{text "J"} *}
   def J \<equiv> "(carrier R #> a) <+> I :: 'a set"
   have idealJ: "ideal J R"
-      apply (unfold J_def, rule add_ideals)
-      apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr)
-      apply (rule is_ideal)
-      done
+    apply (unfold J_def, rule add_ideals)
+     apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr)
+    apply (rule is_ideal)
+    done
 
   --{* Showing @{term "J"} not smaller than @{term "I"} *}
   have IinJ: "I \<subseteq> J"
@@ -275,7 +275,7 @@
     have "x = \<zero> \<otimes> a \<oplus> x" by algebra
 
     from Zcarr and xI and this
-        show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
+    show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
   qed
 
   --{* Showing @{term "J \<noteq> I"} *}
@@ -284,57 +284,58 @@
     assume "a \<in> I"
     hence "I +> a = I" by (rule a_rcos_const)
     from this and IanI
-        show "False" by simp
+    show "False" by simp
   qed
 
   have aJ: "a \<in> J"
   proof (simp add: J_def r_coset_def set_add_defs)
     from acarr
-        have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
+    have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
     from one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup] and this
-        show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast
+    show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast
   qed
 
   from aJ and anI
-      have JnI: "J \<noteq> I" by fast
+  have JnI: "J \<noteq> I" by fast
 
   --{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *}
   from idealJ and IinJ
-      have "J = I \<or> J = carrier R"
+  have "J = I \<or> J = carrier R"
   proof (rule I_maximal, unfold J_def)
     have "carrier R #> a \<subseteq> carrier R"
-	  by (rule r_coset_subset_G) fast
+      using subset_refl acarr
+      by (rule r_coset_subset_G)
     from this and a_subset
-        show "carrier R #> a <+> I \<subseteq> carrier R" by (rule set_add_closed)
+    show "carrier R #> a <+> I \<subseteq> carrier R" by (rule set_add_closed)
   qed
 
   from this and JnI
-      have Jcarr: "J = carrier R" by simp
+  have Jcarr: "J = carrier R" by simp
 
   --{* Calculating an inverse for @{term "a"} *}
   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)
+  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)
   from this
-     obtain r i
-       where rcarr: "r \<in> carrier R"
-       and iI: "i \<in> I"
-       and one: "\<one> = r \<otimes> a \<oplus> i"
-     by fast
+  obtain r i
+    where rcarr: "r \<in> carrier R"
+      and iI: "i \<in> I"
+      and one: "\<one> = r \<otimes> a \<oplus> i"
+    by fast
   from one and rcarr and acarr and iI[THEN a_Hcarr]
-      have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
+  have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
 
   --{* Lifting to cosets *}
   from iI
-      have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
-      by (intro a_rcosI, simp, intro a_subset, simp)
+  have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
+    by (intro a_rcosI, simp, intro a_subset, simp)
   from this and rai1
-      have "a \<otimes> r \<in> I +> \<one>" by simp
+  have "a \<otimes> r \<in> I +> \<one>" by simp
   from this have "I +> \<one> = I +> a \<otimes> r"
-      by (rule a_repr_independence, simp) (rule a_subgroup)
+    by (rule a_repr_independence, simp) (rule a_subgroup)
 
   from rcarr and this[symmetric]
-      show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
+  show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
 qed
 
 end