--- a/src/ZF/ex/Group.thy Wed Jun 09 11:19:23 2004 +0200
+++ b/src/ZF/ex/Group.thy Wed Jun 09 12:24:02 2004 +0200
@@ -16,7 +16,7 @@
(*First, we must simulate a record declaration:
record monoid =
carrier :: i
- mult :: "[i,i] => i" (infixl "\<otimes>\<index>" 70)
+ mult :: "[i,i] => i" (infixl "\<cdot>\<index>" 70)
one :: i ("\<one>\<index>")
*)
@@ -261,9 +261,9 @@
shows "group_axioms (update_carrier(G,H))"
by (force intro: group_axioms.intro l_inv r_inv)
-lemma (in subgroup) groupI [intro]:
+lemma (in subgroup) is_group [intro]:
includes group G
- shows "group (update_carrier(G,H))"
+ shows "group (update_carrier(G,H))"
by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
text {*
@@ -465,7 +465,7 @@
lemma (in group) subgroup_imp_group:
"subgroup(H,G) \<Longrightarrow> group (update_carrier(G,H))"
-by (simp add: subgroup.groupI)
+by (simp add: subgroup.is_group)
lemma (in group) subgroupI:
assumes subset: "H \<subseteq> carrier(G)" and non_empty: "H \<noteq> 0"
@@ -546,7 +546,7 @@
qed
theorem (in group) AutoGroup: "group (AutoGroup(G))"
-by (simp add: AutoGroup_def Group.subgroup.groupI subgroup_auto group_BijGroup)
+by (simp add: AutoGroup_def subgroup.is_group subgroup_auto group_BijGroup)
@@ -1010,13 +1010,10 @@
"M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems)
-text{*Hack required because @{text subgroup.groupI} hides this theorem.*}
-lemmas G_groupI = groupI;
-
theorem (in normal) factorgroup_is_group:
"group (G Mod H)"
apply (simp add: FactGroup_def)
-apply (rule G_groupI)
+apply (rule groupI)
apply (simp add: setmult_closed)
apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
apply (simp add: setmult_closed rcosets_assoc)
@@ -1038,7 +1035,10 @@
by (auto simp add: FactGroup_def RCOSETS_def hom_def rcos_sum intro: lam_type)
-subsection{*Quotienting by the Kernel of a Homomorphism*}
+subsection{*The First Isomorphism Theorem*}
+
+text{*The quotient by the kernel of a homomorphism is isomorphic to the
+ range of that homomorphism.*}
constdefs
kernel :: "[i,i,i] => i"
@@ -1118,7 +1118,6 @@
qed
-
text{*Lemma for the following injectivity result*}
lemma (in group_hom) FactGroup_subset:
"\<lbrakk>g \<in> carrier(G); g' \<in> carrier(G); h ` g = h ` g'\<rbrakk>