src/HOL/Algebra/Group.thy
 changeset 15696 1da4ce092c0b parent 15076 4b3d280ef06a child 15763 b901a127ac73
```     1.1 --- a/src/HOL/Algebra/Group.thy	Mon Apr 11 12:18:27 2005 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Mon Apr 11 12:34:34 2005 +0200
1.3 @@ -469,7 +469,7 @@
1.4    apply (simp_all add: prems group_def group.l_inv)
1.5    done
1.6
1.7 -text{*This alternative proof of the previous result demonstrates instantiate.
1.8 +text{*This alternative proof of the previous result demonstrates interpret.
1.9     It uses @{text Prod.inv_equality} (available after instantiation) instead of
1.10     @{text "group.inv_equality [OF DirProd_group]"}. *}
1.11  lemma
1.12 @@ -478,9 +478,8 @@
1.13        and h: "h \<in> carrier H"
1.14    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
1.15  proof -
1.16 -  have "group (G \<times>\<times> H)"
1.17 -    by (blast intro: DirProd_group group.intro prems)
1.18 -  then instantiate Prod: group
1.19 +  interpret Prod: group ["G \<times>\<times> H"]
1.20 +    by (auto intro: DirProd_group group.intro group.axioms prems)
1.21    show ?thesis by (simp add: Prod.inv_equality g h)
1.22  qed
1.23
1.24 @@ -543,8 +542,19 @@
1.25    @{term H}, with a homomorphism @{term h} between them*}
1.26  locale group_hom = group G + group H + var h +
1.27    assumes homh: "h \<in> hom G H"
1.28 +(*
1.29    notes hom_mult [simp] = hom_mult [OF homh]
1.30      and hom_closed [simp] = hom_closed [OF homh]
1.31 +CB: late binding problem?
1.32 +*)
1.33 +
1.34 +lemma (in group_hom) hom_mult [simp]:
1.35 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
1.36 +  by (simp add: hom_mult [OF homh])
1.37 +
1.38 +lemma (in group_hom) hom_closed [simp]:
1.39 +  "x \<in> carrier G ==> h x \<in> carrier H"
1.40 +  by (simp add: hom_closed [OF homh])
1.41
1.42  lemma (in group_hom) one_closed [simp]:
1.43    "h \<one> \<in> carrier H"
```