# HG changeset patch
# User wenzelm
# Date 1333999787 -7200
# Node ID c5be1120980d88dda05c2c83a56adbf1cc6b3667
# Parent  63c05991882e73aa474e4f022eab4806178d6baf
tuned proofs;

diff -r 63c05991882e -r c5be1120980d src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Mon Apr 09 20:57:23 2012 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Mon Apr 09 21:29:47 2012 +0200
@@ -60,7 +60,7 @@
 lemma principalidealI:
   fixes R (structure)
   assumes "ideal I R"
-  assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
+    and generate: "\<exists>i \<in> carrier R. I = Idl {i}"
   shows "principalideal I R"
 proof -
   interpret ideal I R by fact
@@ -82,7 +82,7 @@
 lemma maximalidealI:
   fixes R
   assumes "ideal I R"
-  assumes I_notcarr: "carrier R \<noteq> I"
+    and I_notcarr: "carrier R \<noteq> I"
     and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
   shows "maximalideal I R"
 proof -
@@ -105,8 +105,8 @@
 lemma primeidealI:
   fixes R (structure)
   assumes "ideal I R"
-  assumes "cring R"
-  assumes I_notcarr: "carrier R \<noteq> I"
+    and "cring R"
+    and I_notcarr: "carrier R \<noteq> I"
     and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
   shows "primeideal I R"
 proof -
@@ -120,8 +120,8 @@
 lemma primeidealI2:
   fixes R (structure)
   assumes "additive_subgroup I R"
-  assumes "cring R"
-  assumes I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
+    and "cring R"
+    and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
     and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
     and I_notcarr: "carrier R \<noteq> I"
     and I_prime: "\<And>a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
@@ -378,8 +378,8 @@
   with a show "H \<subseteq> I" by simp
 next
   fix x
-  assume HI: "H \<subseteq> I"
-  from Iideal and HI have "I \<in> {I. ideal I R \<and> H \<subseteq> I}" by fast
+  assume "H \<subseteq> I"
+  with Iideal have "I \<in> {I. ideal I R \<and> H \<subseteq> I}" by fast
   then show "Idl H \<subseteq> I" unfolding genideal_def by fast
 qed
 
diff -r 63c05991882e -r c5be1120980d src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Mon Apr 09 20:57:23 2012 +0200
+++ b/src/HOL/Algebra/Ring.thy	Mon Apr 09 21:29:47 2012 +0200
@@ -423,13 +423,10 @@
 proof (rule, rule)
   fix x
   assume xcarr: "x \<in> carrier R"
-  from xcarr
-      have "x = x \<otimes> \<one>" by simp
-  from this and onezero
-      have "x = x \<otimes> \<zero>" by simp
-  from this and xcarr
-      have "x = \<zero>" by simp
-  thus "x \<in> {\<zero>}" by fast
+  from xcarr have "x = x \<otimes> \<one>" by simp
+  with onezero have "x = x \<otimes> \<zero>" by simp
+  with xcarr have "x = \<zero>" by simp
+  then show "x \<in> {\<zero>}" by fast
 qed fast
 
 lemma one_zeroI:
@@ -550,11 +547,9 @@
   assumes field_Units: "Units R = carrier R - {\<zero>}"
   shows "field R"
 proof
-  from field_Units
-  have a: "\<zero> \<notin> Units R" by fast
-  have "\<one> \<in> Units R" by fast
-  from this and a
-  show "\<one> \<noteq> \<zero>" by force
+  from field_Units have "\<zero> \<notin> Units R" by fast
+  moreover have "\<one> \<in> Units R" by fast
+  ultimately show "\<one> \<noteq> \<zero>" by force
 next
   fix a b
   assume acarr: "a \<in> carrier R"
@@ -563,21 +558,15 @@
   show "a = \<zero> \<or> b = \<zero>"
   proof (cases "a = \<zero>", simp)
     assume "a \<noteq> \<zero>"
-    from this and field_Units and acarr
-    have aUnit: "a \<in> Units R" by fast
-    from bcarr
-    have "b = \<one> \<otimes> b" by algebra
-    also from aUnit acarr
-    have "... = (inv a \<otimes> a) \<otimes> b" by simp
+    with field_Units and acarr have aUnit: "a \<in> Units R" by fast
+    from bcarr have "b = \<one> \<otimes> b" by algebra
+    also from aUnit acarr have "... = (inv a \<otimes> a) \<otimes> b" by simp
     also from acarr bcarr aUnit[THEN Units_inv_closed]
     have "... = (inv a) \<otimes> (a \<otimes> b)" by algebra
-    also from ab and acarr bcarr aUnit
-    have "... = (inv a) \<otimes> \<zero>" by simp
-    also from aUnit[THEN Units_inv_closed]
-    have "... = \<zero>" by algebra
-    finally
-    have "b = \<zero>" .
-    thus "a = \<zero> \<or> b = \<zero>" by simp
+    also from ab and acarr bcarr aUnit have "... = (inv a) \<otimes> \<zero>" by simp
+    also from aUnit[THEN Units_inv_closed] have "... = \<zero>" by algebra
+    finally have "b = \<zero>" .
+    then show "a = \<zero> \<or> b = \<zero>" by simp
   qed
 qed (rule field_Units)
 
@@ -593,16 +582,10 @@
   fix x
   assume xcarr: "x \<in> carrier R"
     and "x \<noteq> \<zero>"
-  from this
-  have "\<exists>y\<in>carrier R. x \<otimes> y = \<one>" by (rule invex)
-  from this
-  obtain y
-    where ycarr: "y \<in> carrier R"
-    and xy: "x \<otimes> y = \<one>"
-    by fast
+  then have "\<exists>y\<in>carrier R. x \<otimes> y = \<one>" by (rule invex)
+  then obtain y where ycarr: "y \<in> carrier R" and xy: "x \<otimes> y = \<one>" by fast
   from xy xcarr ycarr have "y \<otimes> x = \<one>" by (simp add: m_comm)
-  from ycarr and this and xy
-  show "\<exists>y\<in>carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast
+  with ycarr and xy show "\<exists>y\<in>carrier R. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast
 qed