src/HOL/Algebra/Group.thy
changeset 19783 82f365a14960
parent 19699 1ecda5544e88
child 19931 fb32b43e7f80
     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Jun 06 09:28:24 2006 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Tue Jun 06 10:05:57 2006 +0200
     1.3 @@ -40,7 +40,8 @@
     1.4      let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
     1.5      in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
     1.6  
     1.7 -locale monoid = struct G +
     1.8 +locale monoid =
     1.9 +  fixes G (structure)
    1.10    assumes m_closed [intro, simp]:
    1.11           "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> carrier G"
    1.12        and m_assoc:
    1.13 @@ -51,7 +52,7 @@
    1.14        and r_one [simp]: "x \<in> carrier G \<Longrightarrow> x \<otimes> \<one> = x"
    1.15  
    1.16  lemma monoidI:
    1.17 -  includes struct G
    1.18 +  fixes G (structure)
    1.19    assumes m_closed:
    1.20        "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    1.21      and one_closed: "\<one> \<in> carrier G"
    1.22 @@ -192,7 +193,7 @@
    1.23    by (rule group.intro [OF prems]) 
    1.24  
    1.25  theorem groupI:
    1.26 -  includes struct G
    1.27 +  fixes G (structure)
    1.28    assumes m_closed [simp]:
    1.29        "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    1.30      and one_closed [simp]: "\<one> \<in> carrier G"
    1.31 @@ -359,7 +360,8 @@
    1.32  
    1.33  subsection {* Subgroups *}
    1.34  
    1.35 -locale subgroup = var H + struct G + 
    1.36 +locale subgroup =
    1.37 +  fixes H and G (structure)
    1.38    assumes subset: "H \<subseteq> carrier G"
    1.39      and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
    1.40      and  one_closed [simp]: "\<one> \<in> H"
    1.41 @@ -600,7 +602,7 @@
    1.42  lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm
    1.43  
    1.44  lemma comm_monoidI:
    1.45 -  includes struct G
    1.46 +  fixes G (structure)
    1.47    assumes m_closed:
    1.48        "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    1.49      and one_closed: "\<one> \<in> carrier G"
    1.50 @@ -645,7 +647,7 @@
    1.51                    is_group prems)
    1.52  
    1.53  lemma comm_groupI:
    1.54 -  includes struct G
    1.55 +  fixes G (structure)
    1.56    assumes m_closed:
    1.57        "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    1.58      and one_closed: "\<one> \<in> carrier G"