--- a/src/ZF/ex/Group.thy Wed Jan 12 15:22:24 2011 +0100
+++ b/src/ZF/ex/Group.thy Wed Jan 12 15:38:57 2011 +0100
@@ -148,7 +148,7 @@
qed
show ?thesis
by (blast intro: group.intro monoid.intro group_axioms.intro
- prems r_one inv_ex)
+ assms r_one inv_ex)
qed
lemma (in group) inv [simp]:
@@ -177,26 +177,26 @@
subsection {* Cancellation Laws and Basic Properties *}
lemma (in group) l_cancel [simp]:
- assumes [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
+ assumes "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
shows "(x \<cdot> y = x \<cdot> z) <-> (y = z)"
proof
assume eq: "x \<cdot> y = x \<cdot> z"
hence "(inv x \<cdot> x) \<cdot> y = (inv x \<cdot> x) \<cdot> z"
- by (simp only: m_assoc inv_closed prems)
- thus "y = z" by simp
+ by (simp only: m_assoc inv_closed assms)
+ thus "y = z" by (simp add: assms)
next
assume eq: "y = z"
then show "x \<cdot> y = x \<cdot> z" by simp
qed
lemma (in group) r_cancel [simp]:
- assumes [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
+ assumes "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
shows "(y \<cdot> x = z \<cdot> x) <-> (y = z)"
proof
assume eq: "y \<cdot> x = z \<cdot> x"
then have "y \<cdot> (x \<cdot> inv x) = z \<cdot> (x \<cdot> inv x)"
- by (simp only: m_assoc [symmetric] inv_closed prems)
- thus "y = z" by simp
+ by (simp only: m_assoc [symmetric] inv_closed assms)
+ thus "y = z" by (simp add: assms)
next
assume eq: "y = z"
thus "y \<cdot> x = z \<cdot> x" by simp
@@ -338,7 +338,7 @@
and h: "h \<in> carrier(H)"
shows "inv \<^bsub>G \<Otimes> H\<^esub> <g, h> = <inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h>"
apply (rule group.inv_equality [OF DirProdGroup_group])
- apply (simp_all add: prems group.l_inv)
+ apply (simp_all add: assms group.l_inv)
done
subsection {* Isomorphisms *}
@@ -445,7 +445,7 @@
also from x have "... = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)"
by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
finally have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)" .
- with x show ?thesis by (simp del: inv add: is_group)
+ with x show ?thesis by (simp del: inv)
qed
subsection {* Commutative Structures *}
@@ -482,7 +482,7 @@
lemma (in group) subgroup_self: "subgroup (carrier(G),G)"
-by (simp add: subgroup_def prems)
+by (simp add: subgroup_def)
lemma (in group) subgroup_imp_group:
"subgroup(H,G) \<Longrightarrow> group (update_carrier(G,H))"
@@ -493,8 +493,8 @@
and inv: "!!a. a \<in> H ==> inv a \<in> H"
and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
shows "subgroup(H,G)"
-proof (simp add: subgroup_def prems)
- show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
+proof (simp add: subgroup_def assms)
+ show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: assms)
qed
@@ -783,8 +783,7 @@
apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
apply (rule_tac x = x in bexI)
apply (rule bexI [of _ "\<one>"])
-apply (auto simp add: subgroup.m_closed subgroup.one_closed
- r_one subgroup.subset [THEN subsetD])
+apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
done
@@ -792,27 +791,27 @@
lemma (in normal) rcos_inv:
assumes x: "x \<in> carrier(G)"
- shows "set_inv (H #> x) = H #> (inv x)"
+ shows "set_inv (H #> x) = H #> (inv x)"
proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe intro!: equalityI)
fix h
- assume "h \<in> H"
- show "inv x \<cdot> inv h \<in> (\<Union>j\<in>H. {j \<cdot> inv x})"
- proof (rule UN_I)
- show "inv x \<cdot> inv h \<cdot> x \<in> H"
- by (simp add: inv_op_closed1 prems)
- show "inv x \<cdot> inv h \<in> {inv x \<cdot> inv h \<cdot> x \<cdot> inv x}"
- by (simp add: prems m_assoc)
- qed
-next
- fix h
- assume "h \<in> H"
- show "h \<cdot> inv x \<in> (\<Union>j\<in>H. {inv x \<cdot> inv j})"
- proof (rule UN_I)
- show "x \<cdot> inv h \<cdot> inv x \<in> H"
- by (simp add: inv_op_closed2 prems)
- show "h \<cdot> inv x \<in> {inv x \<cdot> inv (x \<cdot> inv h \<cdot> inv x)}"
- by (simp add: prems m_assoc [symmetric] inv_mult_group)
- qed
+ assume h: "h \<in> H"
+ {
+ show "inv x \<cdot> inv h \<in> (\<Union>j\<in>H. {j \<cdot> inv x})"
+ proof (rule UN_I)
+ show "inv x \<cdot> inv h \<cdot> x \<in> H"
+ by (simp add: inv_op_closed1 h x)
+ show "inv x \<cdot> inv h \<in> {inv x \<cdot> inv h \<cdot> x \<cdot> inv x}"
+ by (simp add: h x m_assoc)
+ qed
+ next
+ show "h \<cdot> inv x \<in> (\<Union>j\<in>H. {inv x \<cdot> inv j})"
+ proof (rule UN_I)
+ show "x \<cdot> inv h \<cdot> inv x \<in> H"
+ by (simp add: inv_op_closed2 h x)
+ show "h \<cdot> inv x \<in> {inv x \<cdot> inv (x \<cdot> inv h \<cdot> inv x)}"
+ by (simp add: h x m_assoc [symmetric] inv_mult_group)
+ qed
+ }
qed
@@ -844,7 +843,7 @@
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
\<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<cdot> y)"
by (simp add: setmult_rcos_assoc coset_mult_assoc
- subgroup_mult_id subset prems normal.axioms)
+ subgroup_mult_id subset normal_axioms normal.axioms)
lemma (in normal) rcos_sum:
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
@@ -854,7 +853,7 @@
lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
-- {* generalizes @{text subgroup_mult_id} *}
by (auto simp add: RCOSETS_def subset
- setmult_rcos_assoc subgroup_mult_id prems normal.axioms)
+ setmult_rcos_assoc subgroup_mult_id normal_axioms normal.axioms)
subsubsection{*Two distinct right cosets are disjoint*}
@@ -881,7 +880,7 @@
fix x y
assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)"
and "inv x \<cdot> y \<in> H"
- hence "inv (inv x \<cdot> y) \<in> H" by (simp add: m_inv_closed)
+ hence "inv (inv x \<cdot> y) \<in> H" by simp
thus "inv y \<cdot> x \<in> H" by (simp add: inv_mult_group)
qed
next
@@ -932,7 +931,7 @@
interpret subgroup H G by fact
show "PROP ?P"
apply (simp add: RCOSETS_def r_coset_def)
- apply (blast intro: rcos_equation prems sym)
+ apply (blast intro: rcos_equation assms sym)
done
qed
@@ -962,7 +961,7 @@
show ?thesis
apply (rule equalityI)
apply (force simp add: RCOSETS_def r_coset_def)
- apply (auto simp add: RCOSETS_def intro: rcos_self prems)
+ apply (auto simp add: RCOSETS_def intro: rcos_self assms)
done
qed
@@ -1051,7 +1050,7 @@
lemma (in normal) rcosets_inv_mult_group_eq:
"M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
-by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems normal.axioms)
+by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal_axioms normal.axioms)
theorem (in normal) factorgroup_is_group:
"group (G Mod H)"
@@ -1090,12 +1089,12 @@
lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
apply (rule subgroup.intro)
-apply (auto simp add: kernel_def group.intro prems)
+apply (auto simp add: kernel_def group.intro)
done
text{*The kernel of a homomorphism is a normal subgroup*}
lemma (in group_hom) normal_kernel: "(kernel(G,H,h)) \<lhd> G"
-apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
+apply (simp add: group.normal_inv_iff subgroup_kernel group.intro)
apply (simp add: kernel_def)
done
--- a/src/ZF/ex/Ring.thy Wed Jan 12 15:22:24 2011 +0100
+++ b/src/ZF/ex/Ring.thy Wed Jan 12 15:38:57 2011 +0100
@@ -200,7 +200,7 @@
proof -
assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
then have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = (\<ominus> x \<oplus> x) \<cdot> y" by (simp add: l_distr)
- also from R have "... = \<zero>" by (simp add: l_neg l_null)
+ also from R have "... = \<zero>" by (simp add: l_neg)
finally have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = \<zero>" .
with R have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
with R show ?thesis by (simp add: a_assoc r_neg)
@@ -211,7 +211,7 @@
proof -
assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
then have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = x \<cdot> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
- also from R have "... = \<zero>" by (simp add: l_neg r_null)
+ also from R have "... = \<zero>" by (simp add: l_neg)
finally have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = \<zero>" .
with R have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
with R show ?thesis by (simp add: a_assoc r_neg)
@@ -243,7 +243,7 @@
h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
and hom_one: "h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
shows "h \<in> ring_hom(R,S)"
-by (auto simp add: ring_hom_def prems)
+by (auto simp add: ring_hom_def assms)
lemma ring_hom_closed:
"\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(S)"