--- 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
--- 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