--- a/src/HOL/ex/Locales.thy Wed Nov 07 18:16:54 2001 +0100
+++ b/src/HOL/ex/Locales.thy Wed Nov 07 18:17:16 2001 +0100
@@ -4,22 +4,22 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-header {* Locales and simple mathematical structures *}
+header {* Basic use of locales *}
theory Locales = Main:
+text {*
+ The inevitable group theory examples formulated with locales.
+*}
+
+
+subsection {* Local contexts as mathematical structures *}
+
text_raw {*
\newcommand{\isasyminv}{\isasyminverse}
\newcommand{\isasymone}{\isamath{1}}
*}
-
-subsection {* Groups *}
-
-text {*
- Locales version of the inevitable group example.
-*}
-
locale group =
fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70)
and inv :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
@@ -119,4 +119,37 @@
finally show ?thesis .
qed
-end
+
+subsection {* Referencing structures implicitly *}
+
+record 'a semigroup =
+ prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
+syntax
+ "_prod1" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
+ "_prod2" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>\<^sub>2" 70)
+ "_prod3" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>\<^sub>3" 70)
+translations
+ "x \<odot> y" \<rightleftharpoons> "(\<struct>prod) x y"
+ "x \<odot>\<^sub>2 y" \<rightleftharpoons> "(\<struct>\<struct>prod) x y"
+ "x \<odot>\<^sub>3 y" \<rightleftharpoons> "(\<struct>\<struct>\<struct>prod) x y"
+
+lemma
+ (fixes S :: "'a semigroup" (structure)
+ and T :: "'a semigroup" (structure)
+ and U :: "'a semigroup" (structure))
+ "prod S a b = a \<odot> b" ..
+
+lemma
+ (fixes S :: "'a semigroup" (structure)
+ and T :: "'a semigroup" (structure)
+ and U :: "'a semigroup" (structure))
+ "prod T a b = a \<odot>\<^sub>2 b" ..
+
+lemma
+ (fixes S :: "'a semigroup" (structure)
+ and T :: "'a semigroup" (structure)
+ and U :: "'a semigroup" (structure))
+ "prod U a b = a \<odot>\<^sub>3 b" ..
+
+end
\ No newline at end of file