src/HOL/Algebra/Group.thy
changeset 29237 e90d9d51106b
parent 28823 dcbef866c9e2
child 29240 bb81c3709fb6
     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Dec 16 15:09:37 2008 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Tue Dec 16 21:10:53 2008 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*
     1.5    Title:  HOL/Algebra/Group.thy
     1.6 -  Id:     $Id$
     1.7    Author: Clemens Ballarin, started 4 February 2003
     1.8  
     1.9  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
    1.10 @@ -425,7 +424,7 @@
    1.11    assumes "group G"
    1.12    shows "group (G\<lparr>carrier := H\<rparr>)"
    1.13  proof -
    1.14 -  interpret group [G] by fact
    1.15 +  interpret group G by fact
    1.16    show ?thesis
    1.17      apply (rule monoid.group_l_invI)
    1.18      apply (unfold_locales) [1]
    1.19 @@ -489,8 +488,8 @@
    1.20    assumes "monoid G" and "monoid H"
    1.21    shows "monoid (G \<times>\<times> H)"
    1.22  proof -
    1.23 -  interpret G: monoid [G] by fact
    1.24 -  interpret H: monoid [H] by fact
    1.25 +  interpret G!: monoid G by fact
    1.26 +  interpret H!: monoid H by fact
    1.27    from assms
    1.28    show ?thesis by (unfold monoid_def DirProd_def, auto) 
    1.29  qed
    1.30 @@ -501,8 +500,8 @@
    1.31    assumes "group G" and "group H"
    1.32    shows "group (G \<times>\<times> H)"
    1.33  proof -
    1.34 -  interpret G: group [G] by fact
    1.35 -  interpret H: group [H] by fact
    1.36 +  interpret G!: group G by fact
    1.37 +  interpret H!: group H by fact
    1.38    show ?thesis by (rule groupI)
    1.39       (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
    1.40             simp add: DirProd_def)
    1.41 @@ -526,9 +525,9 @@
    1.42        and h: "h \<in> carrier H"
    1.43    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
    1.44  proof -
    1.45 -  interpret G: group [G] by fact
    1.46 -  interpret H: group [H] by fact
    1.47 -  interpret Prod: group ["G \<times>\<times> H"]
    1.48 +  interpret G!: group G by fact
    1.49 +  interpret H!: group H by fact
    1.50 +  interpret Prod!: group "G \<times>\<times> H"
    1.51      by (auto intro: DirProd_group group.intro group.axioms assms)
    1.52    show ?thesis by (simp add: Prod.inv_equality g h)
    1.53  qed
    1.54 @@ -587,7 +586,8 @@
    1.55  
    1.56  text{*Basis for homomorphism proofs: we assume two groups @{term G} and
    1.57    @{term H}, with a homomorphism @{term h} between them*}
    1.58 -locale group_hom = group G + group H + var h +
    1.59 +locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
    1.60 +  fixes h
    1.61    assumes homh: "h \<in> hom G H"
    1.62    notes hom_mult [simp] = hom_mult [OF homh]
    1.63      and hom_closed [simp] = hom_closed [OF homh]