# HG changeset patch
# User wenzelm
# Date 1005175566 -3600
# Node ID 8504c948fae27ba127225417a541435253007a5a
# Parent  784fe681ba26f753cb93303dec6b8e4fc86aee1f
more explanations on advanced syntax;

diff -r 784fe681ba26 -r 8504c948fae2 src/HOL/ex/Locales.thy
--- a/src/HOL/ex/Locales.thy	Thu Nov 08 00:25:36 2001 +0100
+++ b/src/HOL/ex/Locales.thy	Thu Nov 08 00:26:06 2001 +0100
@@ -4,20 +4,33 @@
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-header {* Basic use of locales *}
+header {* Basic use of locales in Isabelle/Isar *}
 
 theory Locales = Main:
 
 text {*
-  The inevitable group theory examples formulated with locales.
+  Locales provide a mechanism for encapsulating local contexts.  While
+  the original version by Florian Kamm\"uller refers to the raw
+  meta-logic, the present one of Isabelle/Isar builds on top of the
+  rich infrastructure of Isar proof contexts.  Subsequently, we
+  demonstrate basic use of locales to model mathematical structures
+  (by the inevitable group theory example).
+*}
+
+text_raw {*
+  \newcommand{\isasyminv}{\isasyminverse}
+  \newcommand{\isasymone}{\isamath{1}}
+  \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
 *}
 
 
 subsection {* Local contexts as mathematical structures *}
 
-text_raw {*
-  \newcommand{\isasyminv}{\isasyminverse}
-  \newcommand{\isasymone}{\isamath{1}}
+text {*
+  The following definitions of @{text group} and @{text abelian_group}
+  simply encapsulate local parameters (with private syntax) and
+  assumptions; local definitions may be given as well, but are not
+  shown here.
 *}
 
 locale group =
@@ -31,6 +44,13 @@
 locale abelian_group = group +
   assumes commute: "x \<cdot> y = y \<cdot> x"
 
+text {*
+  \medskip We may now prove theorems within a local context, just by
+  including a directive ``@{text "(\<IN> name)"}'' in the goal
+  specification.  The final result will be stored within the named
+  locale; a second copy is exported to the enclosing theory context.
+*}
+
 theorem (in group)
   right_inv: "x \<cdot> x\<inv> = \<one>"
 proof -
@@ -55,6 +75,12 @@
   finally show ?thesis .
 qed
 
+text {*
+  \medskip Apart from the named locale context we may also refer to
+  further ad-hoc elements (parameters, assumptions, etc.); these are
+  discharged when the proof is finished.
+*}
+
 theorem (in group)
   (assumes eq: "e \<cdot> x = x")
   one_equality: "\<one> = e"
@@ -92,6 +118,13 @@
   qed
 qed
 
+text {*
+  \medskip Results are automatically propagated through the hierarchy
+  of locales.  Below we establish a trivial fact of commutative
+  groups, while referring both to theorems of @{text group} and the
+  characteristic assumption of @{text abelian_group}.
+*}
+
 theorem (in abelian_group)
   inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
 proof -
@@ -100,6 +133,10 @@
   finally show ?thesis .
 qed
 
+text {*
+  \medskip Some further facts of general group theory follow.
+*}
+
 theorem (in group)
   inv_inv: "(x\<inv>)\<inv> = x"
 proof (rule inv_equality)
@@ -119,37 +156,149 @@
   finally show ?thesis .
 qed
 
+text {*
+  \bigskip We see that this representation of structures as local
+  contexts is rather light-weight and convenient to use for abstract
+  reasoning.  Here the ``components'' (the group operations) have been
+  exhibited directly as context parameters; logically this corresponds
+  to a curried predicate definition.  Occasionally, this
+  ``externalized'' version of the informal idea of classes of tuple
+  structures may cause some inconveniences, especially in
+  meta-theoretical studies (involving functors from groups to groups,
+  for example).
 
-subsection {* Referencing structures implicitly *}
+  Another drawback of the naive approach above is that concrete syntax
+  will get lost on any kind of operation on the locale itself (such as
+  renaming, copying, or instantiation).  Whenever the particular
+  terminology of local parameters is affected the associated syntax
+  would have to be changed as well, which is hard to achieve formally.
+*}
+
+
+subsection {* Referencing explicit structures implicitly *}
 
-record 'a semigroup =
+text {*
+  The issue of multiple parameters raised above may be easily
+  addressed by stating properties over a record of group operations,
+  instead of the individual constituents.
+*}
+
+record 'a group =
   prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  inv :: "'a \<Rightarrow> 'a"
+  one :: 'a
+
+text {*
+  Now concrete syntax essentially needs refer to record selections;
+  this is possible by giving defined operations with private syntax
+  within the locale (e.g.\ see appropriate examples by Kamm\"uller).
+
+  In the subsequent formulation of group structures we go one step
+  further by using \emph{implicit} references to the underlying
+  abstract entity.  To this end we define global syntax, which is
+  translated to refer to the ``current'' structure at hand, denoted by
+  the dummy item ``@{text \<struct>}'' according to the builtin syntax
+  mechanism for locales.
+*}
 
 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)
+  "_prod" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
+  "_inv" :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
+  "_one" :: 'a    ("\<one>")
 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"
+  "x \<cdot> y"  \<rightleftharpoons>  "prod \<struct> x y"
+  "x\<inv>"  \<rightleftharpoons>  "inv \<struct> x"
+  "\<one>"  \<rightleftharpoons>  "one \<struct>"
+
+text {*
+  The following locale definition introduces a single parameter, which
+  is declared as ``\isakeyword{structure}''.
+*}
+
+locale group_struct =
+  fixes G :: "'a group"    (structure)
+  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
+    and left_inv: "x\<inv> \<cdot> x = \<one>"
+    and left_one: "\<one> \<cdot> x = x"
+
+text {*
+  In its context the dummy ``@{text \<struct>}'' refers to this very
+  parameter, independently of the present naming.  We may now proceed
+  to prove results within @{text group_struct} just as before for
+  @{text group}.  Proper treatment of ``@{text \<struct>}'' is hidden in
+  concrete syntax, so the proof text is exactly the same as for @{text
+  group} given before.
+*}
+
+theorem (in group_struct)
+  right_inv: "x \<cdot> x\<inv> = \<one>"
+proof -
+  have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
+  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
+  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
+  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
+  also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
+  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
+  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
+  also have "\<dots> = \<one>" by (simp only: left_inv)
+  finally show ?thesis .
+qed
+
+theorem (in group_struct)
+  right_one: "x \<cdot> \<one> = x"
+proof -
+  have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
+  also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
+  also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
+  also have "\<dots> = x" by (simp only: left_one)
+  finally show ?thesis .
+qed
+
+text {*
+  \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.
+*}
+
+syntax
+  "_prod'" :: "'a \<Rightarrow> index \<Rightarrow> 'a \<Rightarrow> 'a"    ("(_ \<cdot>_/ _)" [70, 1000, 71] 70)
+  "_inv'" :: "'a \<Rightarrow> index \<Rightarrow> 'a"    ("(_\<inv>_)" [1000] 999)
+  "_one'" :: "index \<Rightarrow> 'a"    ("\<one>_")
+translations
+  "x \<cdot>\<^sub>2 y"  \<rightleftharpoons>  "prod \<struct>\<^sub>2 x y"
+  "x \<cdot>\<^sub>3 y"  \<rightleftharpoons>  "prod \<struct>\<^sub>3 x y"
+  "x\<inv>\<^sub>2"  \<rightleftharpoons>  "inv \<struct>\<^sub>2 x"
+  "x\<inv>\<^sub>3"  \<rightleftharpoons>  "inv \<struct>\<^sub>3 x"
+  "\<one>\<^sub>2"  \<rightleftharpoons>  "one \<struct>\<^sub>2"
+  "\<one>\<^sub>3"  \<rightleftharpoons>  "one \<struct>\<^sub>3"
+
+text {*
+  \medskip The following synthetic example demonstrates how to refer
+  to several structures of type @{text group} succinctly; one might
+  also think of working with renamed versions of the @{text
+  group_struct} locale above.
+*}
 
 lemma
-  (fixes S :: "'a semigroup" (structure)
-    and T :: "'a semigroup" (structure)
-    and U :: "'a semigroup" (structure))
-  "prod S a b = a \<odot> b" ..
+  (fixes G :: "'a group" (structure)
+    and H :: "'a group" (structure))
+  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
-  (fixes S :: "'a semigroup" (structure)
-    and T :: "'a semigroup" (structure)
-    and U :: "'a semigroup" (structure))
-  "prod T a b = a \<odot>\<^sub>2 b" ..
+text {*
+  \medskip As a minor drawback of this advanced technique we require
+  slightly more work to setup abstract and concrete syntax properly
+  (but only once in the beginning).  The resulting casual mode of
+  writing @{text "x \<cdot> y"} for @{text "prod G x y"} etc.\ mimics common
+  practice of informal mathematics quite nicely, while using a simple
+  and robust formal representation.
+*}
 
-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
+end