src/HOL/Algebra/Group.thy
 changeset 19783 82f365a14960 parent 19699 1ecda5544e88 child 19931 fb32b43e7f80
```--- a/src/HOL/Algebra/Group.thy	Tue Jun 06 09:28:24 2006 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Jun 06 10:05:57 2006 +0200
@@ -40,7 +40,8 @@
let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"

-locale monoid = struct G +
+locale monoid =
+  fixes G (structure)
assumes m_closed [intro, simp]:
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> carrier G"
and m_assoc:
@@ -51,7 +52,7 @@
and r_one [simp]: "x \<in> carrier G \<Longrightarrow> x \<otimes> \<one> = x"

lemma monoidI:
-  includes struct G
+  fixes G (structure)
assumes m_closed:
"!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
and one_closed: "\<one> \<in> carrier G"
@@ -192,7 +193,7 @@
by (rule group.intro [OF prems])

theorem groupI:
-  includes struct G
+  fixes G (structure)
assumes m_closed [simp]:
"!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
and one_closed [simp]: "\<one> \<in> carrier G"
@@ -359,7 +360,8 @@

subsection {* Subgroups *}

-locale subgroup = var H + struct G +
+locale subgroup =
+  fixes H and G (structure)
assumes subset: "H \<subseteq> carrier G"
and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
and  one_closed [simp]: "\<one> \<in> H"
@@ -600,7 +602,7 @@
lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm

lemma comm_monoidI:
-  includes struct G
+  fixes G (structure)
assumes m_closed:
"!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
and one_closed: "\<one> \<in> carrier G"
@@ -645,7 +647,7 @@
is_group prems)

lemma comm_groupI:
-  includes struct G
+  fixes G (structure)
assumes m_closed:
"!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
and one_closed: "\<one> \<in> carrier G"```