src/HOL/ex/Locales.thy
 changeset 12091 08b4da78d1ad parent 12075 8d65dd96381f child 12099 8504c948fae2
```--- 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 @@
*)

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