src/HOL/Algebra/Group.thy
 changeset 31727 2621a957d417 parent 30729 461ee3e49ad3 child 31754 b5260f5272a4
```--- a/src/HOL/Algebra/Group.thy	Fri Jun 19 20:22:46 2009 +0200
+++ b/src/HOL/Algebra/Group.thy	Fri Jun 19 22:49:12 2009 +0200
@@ -544,7 +544,7 @@
lemma (in group) hom_compose:
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
apply (auto simp add: hom_def funcset_compose)
done

constdefs
@@ -552,14 +552,14 @@
"G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"

lemma iso_refl: "(%x. x) \<in> G \<cong> G"
-by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
+by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)

lemma (in group) iso_sym:
"h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G")
prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv])
-apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f)
+apply (simp add: hom_def bij_betw_def Inv_f_eq f_Inv_f Pi_def)
done

lemma (in group) iso_trans:
@@ -568,11 +568,11 @@

lemma DirProd_commute_iso:
shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)"
-by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
+by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)

lemma DirProd_assoc_iso:
shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))"
-by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
+by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)

text{*Basis for homomorphism proofs: we assume two groups @{term G} and
@@ -592,7 +592,7 @@
"x \<in> carrier G ==> h x \<in> carrier H"
proof -
assume "x \<in> carrier G"
-  with homh [unfolded hom_def] show ?thesis by (auto simp add: funcset_mem)
+  with homh [unfolded hom_def] show ?thesis by (auto simp add: Pi_def)
qed

lemma (in group_hom) one_closed [simp]:```