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"
from acarr
-        have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
+    have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
-        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"
+  have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
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