# HG changeset patch
# User wenzelm
# Date 1008891484 -3600
# Node ID ff84d5f140854d5dabb60596ae3dbad6122906f1
# Parent  6226b35c04ca08a5843d57a2ac68c4388a7a8d65
tuned;

diff -r 6226b35c04ca -r ff84d5f14085 src/HOL/ex/Locales.thy
--- a/src/HOL/ex/Locales.thy	Thu Dec 20 21:15:37 2001 +0100
+++ b/src/HOL/ex/Locales.thy	Fri Dec 21 00:38:04 2001 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/ex/Locales.thy
     ID:         $Id$
-    Author:     Markus Wenzel, LMU Muenchen
+    Author:     Markus Wenzel, LMU München
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
@@ -18,7 +18,7 @@
 
 text {*
   Locales provide a mechanism for encapsulating local contexts.  The
-  original version due to Florian Kamm\"uller \cite{Kamm-et-al:1999}
+  original version due to Florian Kammüller \cite{Kamm-et-al:1999}
   refers directly to the raw meta-logic of Isabelle.  Semantically, a
   locale is just a (curried) predicate of the pure meta-logic
   \cite{Paulson:1989}.
@@ -94,7 +94,7 @@
   shown here.
 *}
 
-locale group =
+locale group_context =
   fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
     and inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
     and one :: 'a    ("\<one>")
@@ -102,7 +102,7 @@
     and left_inv: "x\<inv> \<cdot> x = \<one>"
     and left_one: "\<one> \<cdot> x = x"
 
-locale abelian_group = group +
+locale abelian_group_context = group_context +
   assumes commute: "x \<cdot> y = y \<cdot> x"
 
 text {*
@@ -112,7 +112,7 @@
   locale; a second copy is exported to the enclosing theory context.
 *}
 
-theorem (in group)
+theorem (in group_context)
   right_inv: "x \<cdot> x\<inv> = \<one>"
 proof -
   have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
@@ -126,7 +126,7 @@
   finally show ?thesis .
 qed
 
-theorem (in group)
+theorem (in group_context)
   right_one: "x \<cdot> \<one> = x"
 proof -
   have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
@@ -142,7 +142,7 @@
   these are discharged when the proof is finished.
 *}
 
-theorem (in group)
+theorem (in group_context)
   (assumes eq: "e \<cdot> x = x")
   one_equality: "\<one> = e"
 proof -
@@ -154,7 +154,7 @@
   finally show ?thesis .
 qed
 
-theorem (in group)
+theorem (in group_context)
   (assumes eq: "x' \<cdot> x = \<one>")
   inv_equality: "x\<inv> = x'"
 proof -
@@ -166,7 +166,7 @@
   finally show ?thesis .
 qed
 
-theorem (in group)
+theorem (in group_context)
   inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"
 proof (rule inv_equality)
   show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"
@@ -186,7 +186,7 @@
   group} and the additional assumption of @{text abelian_group}.
 *}
 
-theorem (in abelian_group)
+theorem (in abelian_group_context)
   inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
 proof -
   have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)
@@ -207,13 +207,13 @@
   follow.
 *}
 
-theorem (in group)
+theorem (in group_context)
   inv_inv: "(x\<inv>)\<inv> = x"
 proof (rule inv_equality)
   show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
 qed
 
-theorem (in group)
+theorem (in group_context)
   (assumes eq: "x\<inv> = y\<inv>")
   inv_inject: "x = y"
 proof -
@@ -263,7 +263,7 @@
 
 text {*
   The mixfix annotations above include a special ``structure index
-  indicator'' @{text \<index>} that makes grammer productions dependent on
+  indicator'' @{text \<index>} that makes gammer productions dependent on
   certain parameters that have been declared as ``structure'' in a
   locale context later on.  Thus we achieve casual notation as
   encountered in informal mathematics, e.g.\ @{text "x \<cdot> y"} for
@@ -275,11 +275,11 @@
   internally.
 *}
 
-locale semigroup_struct =
+locale semigroup =
   fixes S :: "'a group"    (structure)
   assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
 
-locale group_struct = semigroup_struct G +
+locale group = semigroup G +
   assumes left_inv: "x\<inv> \<cdot> x = \<one>"
     and left_one: "\<one> \<cdot> x = x"
 
@@ -294,13 +294,12 @@
   of locale facts will get qualified accordingly, e.g. @{text S.assoc}
   versus @{text G.assoc}.
 
-  \medskip We may now proceed to prove results within @{text
-  group_struct} just as before for @{text group}.  The subsequent
-  proof texts are exactly the same as despite the more advanced
-  internal arrangement.
+  \medskip We may now proceed to prove results within @{text group}
+  just as before for @{text group}.  The subsequent proof texts are
+  exactly the same as despite the more advanced internal arrangement.
 *}
 
-theorem (in group_struct)
+theorem (in group)
   right_inv: "x \<cdot> x\<inv> = \<one>"
 proof -
   have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
@@ -314,7 +313,7 @@
   finally show ?thesis .
 qed
 
-theorem (in group_struct)
+theorem (in group)
   right_one: "x \<cdot> \<one> = x"
 proof -
   have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
@@ -325,28 +324,26 @@
 qed
 
 text {*
-  FIXME
-  \medskip Several implicit structures may be active at the same time
-  (say up to 3 in practice).  The concrete syntax facility for locales
-  actually maintains indexed dummies @{text "\<struct>\<^sub>1"}, @{text
-  "\<struct>\<^sub>2"}, @{text "\<struct>\<^sub>3"}, \dots (@{text \<struct>} is the same as
-  @{text "\<struct>\<^sub>1"}).  So we are able to provide concrete syntax to
-  cover the 2nd and 3rd group structure as well.
+  \medskip Several implicit structures may be active at the same time.
+  The concrete syntax facility for locales actually maintains indexed
+  structures that may be references implicitly --- via mixfix
+  annotations that have been decorated by an ``index argument''
+  (@{text \<index>}).
 
-  \medskip The following synthetic example demonstrates how to refer
-  to several structures of type @{text group} succinctly; one might
-  also think of working with several renamed versions of the @{text
-  group_struct} locale above.
+  The following synthetic example demonstrates how to refer to several
+  structures of type @{text group} succinctly.  We work with two
+  versions of the @{text group} locale above.
 *}
 
-lemma
-  (fixes G :: "'a group" (structure)
-    and H :: "'a group" (structure))  (* FIXME (uses group_struct G + group_struct H) *)
-  True
-proof
-  have "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" ..
-  have "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" ..
-  have "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" ..
-qed
+lemma (uses group G + group H)
+  "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
+  "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" and
+  "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" by (rule refl)+
+
+text {*
+  Note that the trivial statements above need to be given as a
+  simultaneous goal in order to have type-inference make the implicit
+  typing of structures @{text G} and @{text H} agree.
+*}
 
 end