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"