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"
```