diff -r 154b14fbc1d6 -r cc36d5da9bc0 src/HOL/ex/Locales.thy --- a/src/HOL/ex/Locales.thy Fri Dec 14 22:27:20 2001 +0100 +++ b/src/HOL/ex/Locales.thy Fri Dec 14 22:27:43 2001 +0100 @@ -4,31 +4,87 @@ License: GPL (GNU GENERAL PUBLIC LICENSE) *) -header {* Basic use of locales in Isabelle/Isar *} +header {* Using locales in Isabelle/Isar *} theory Locales = Main: +text_raw {* + \newcommand{\isasyminv}{\isasyminverse} + \newcommand{\isasymIN}{\isatext{\isakeyword{in}}} + \newcommand{\isasymUSES}{\isatext{\isakeyword{uses}}} +*} + +subsection {* Overview *} + text {* Locales provide a mechanism for encapsulating local contexts. The original version due to Florian Kamm\"uller \cite{Kamm-et-al:1999} - refers directly to the raw meta-logic of Isabelle. The present - version for Isabelle/Isar - \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis} builds on - top of the rich infrastructure of proof contexts instead; this also - covers essential extra-logical concepts like term abbreviations or - local theorem attributes (e.g.\ declarations of simplification - rules). + 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}. + + The present version for Isabelle/Isar builds on top of the rich + infrastructure of proof contexts + \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis}, + achieving a tight integration with Isar proof texts, and a slightly + more abstract view of the underlying concepts. An Isar proof + context encapsulates certain language elements that correspond to + @{text \} (universal quantification), @{text \} (implication), and + @{text "\"} (definitions) of the pure Isabelle framework. Moreover, + there are extra-logical concepts like term abbreviations or local + theorem attributes (declarations of simplification rules etc.) that + are indispensable in realistic applications. + + Locales support concrete syntax, providing a localized version of + the existing concept of mixfix annotations of Isabelle + \cite{Paulson:1994:Isabelle}. Furthermore, there is a separate + concept of ``implicit structures'' that admits to refer to + particular locale parameters in a casual manner (essentially derived + from the basic idea of ``anti-quotations'' or generalized de-Bruijn + indexes demonstrated in \cite[\S13--14]{Wenzel:2001:Isar-examples}). - Subsequently, we demonstrate basic use of locales to model - mathematical structures (by the inevitable group theory example). -*} + Implicit structures work particular well together with extensible + records in HOL \cite{Naraschewski-Wenzel:1998} (the + ``object-oriented'' features discussed there are not required here). + Thus we shall essentially use record types to represent polymorphic + signatures of mathematical structures, while locales describe their + logical properties as a predicate. Due to type inference of + simply-typed records we are able to give succinct specifications, + without caring about signature morphisms ourselves. Further + eye-candy is provided by the independent concept of ``indexed + concrete syntax'' for record selectors. + + Operations for building up locale contexts from existing definitions + cover common operations of \emph{merge} (disjunctive union in + canonical order) and \emph{rename} (of term parameters; types are + always inferred automatically). + + \medskip Note that the following further concepts are still + \emph{absent}: + \begin{itemize} -text_raw {* - \newcommand{\isasyminv}{\isasyminverse} - \newcommand{\isasymIN}{\isatext{\isakeyword{in}}} + \item Specific language elements for \emph{instantiation} of + locales. + + Currently users may simulate this to some extend by having primitive + Isabelle/Isar operations (@{text of} for substitution and @{text OF} + for composition, \cite{Wenzel:2001:isar-ref}) act on the + automatically exported results stemming from different contexts. + + \item Interpretation of locales, analogous to ``functors'' in + abstract algebra. + + In principle one could directly work with functions over structures + (extensible records), and predicates being derived from locale + definitions. + + \end{itemize} + + \medskip Subsequently, we demonstrate some readily available + concepts of Isabelle/Isar locales by some simple examples of + abstract algebraic reasoning. *} - subsection {* Local contexts as mathematical structures *} text {* @@ -139,8 +195,16 @@ qed text {* - \medskip Some further properties of inversion in general group - theory follow. + We see that the initial import of @{text group} within the + definition of @{text abelian_group} is actually evaluated + dynamically. Thus any results in @{text group} are made available + to the derived context of @{text abelian_group} as well. Note that + the alternative context element @{text \} would import + existing locales in a static fashion, without participating in + further facts emerging later on. + + \medskip Some more properties of inversion in general group theory + follow. *} theorem (in group) @@ -173,69 +237,67 @@ meta-theoretical studies (involving functors from groups to groups, for example). - 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. + Another minor 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 {* Explicit structures referenced implicitly *} 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. See - \cite{Naraschewski-Wenzel:1998,Nipkow-et-al:2001:HOL} on - (extensible) record types in Isabelle/HOL. + We introduce the same hierarchy of basic group structures as above, + this time using extensible record types for the signature part, + together with concrete syntax for selector functions. *} -record 'a group = - prod :: "'a \ 'a \ 'a" - inv :: "'a \ 'a" - one :: 'a +record 'a semigroup = + prod :: "'a \ 'a \ 'a" (infixl "\\" 70) + +record 'a group = "'a semigroup" + + inv :: "'a \ 'a" ("(_\\)" [1000] 999) + 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). + The mixfix annotations above include a special ``structure index + indicator'' @{text \} that makes grammer 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 \ y"} for + @{text "prod G x y"}. - 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 \}'' (according to the builtin syntax - mechanism for locales). + \medskip The following locale definitions introduce operate on a + single parameter declared as ``\isakeyword{structure}''. Type + inference takes care to fill in the appropriate record type schemes + internally. *} -syntax - "_prod" :: "'a \ 'a \ 'a" (infixl "\" 70) - "_inv" :: "'a \ 'a" ("(_\)" [1000] 999) - "_one" :: 'a ("\") -translations - "x \ y" \ "prod \ x y" - "x\" \ "inv \ x" - "\" \ "one \" +locale semigroup_struct = + fixes S :: "'a group" (structure) + assumes assoc: "(x \ y) \ z = x \ (y \ z)" -text {* - The following locale definition introduces a single parameter, which - is declared as a ``\isakeyword{structure}''. In its context the - dummy ``@{text \}'' refers to this very parameter, independently of - the present naming. -*} - -locale group_struct = - fixes G :: "'a group" (structure) - assumes assoc: "(x \ y) \ z = x \ (y \ z)" - and left_inv: "x\ \ x = \" +locale group_struct = semigroup_struct G + + assumes left_inv: "x\ \ x = \" and left_one: "\ \ x = x" text {* - We may now proceed to prove results within @{text group_struct} just - as before for @{text group}. Proper treatment of ``@{text \}'' is - hidden in concrete syntax, so the proof text is exactly the same as - before. + Note that we prefer to call the @{text group} record structure + @{text G} rather than @{text S} inherited from @{text semigroup}. + This does not affect our concrete syntax, which is only dependent on + the \emph{positional} arrangements of currently active structures + (actually only one above), rather than names. In fact, these + parameter names rarely occur in the term language at all (due to the + ``indexed syntax'' facility of Isabelle). On the other hand, names + 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. *} theorem (in group_struct) @@ -263,27 +325,14 @@ 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 "\\<^sub>1"}, @{text "\\<^sub>2"}, @{text "\\<^sub>3"}, \dots (@{text \} is the same as @{text "\\<^sub>1"}). So we are able to provide concrete syntax to cover the 2nd and 3rd group structure as well. -*} -syntax - "_prod'" :: "'a \ index \ 'a \ 'a" ("(_ \_/ _)" [70, 1000, 71] 70) - "_inv'" :: "'a \ index \ 'a" ("(_\_)" [1000] 999) - "_one'" :: "index \ 'a" ("\_") -translations - "x \\<^sub>2 y" \ "prod \\<^sub>2 x y" - "x \\<^sub>3 y" \ "prod \\<^sub>3 x y" - "x\\<^sub>2" \ "inv \\<^sub>2 x" - "x\\<^sub>3" \ "inv \\<^sub>3 x" - "\\<^sub>2" \ "one \\<^sub>2" - "\\<^sub>3" \ "one \\<^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 several renamed versions of the @{text @@ -292,7 +341,7 @@ lemma (fixes G :: "'a group" (structure) - and H :: "'a group" (structure)) + and H :: "'a group" (structure)) (* FIXME (uses group_struct G + group_struct H) *) True proof have "x \ y \ \ = prod G (prod G x y) (one G)" .. @@ -300,13 +349,4 @@ have "x \ \\<^sub>2 = prod G x (one H)" .. qed -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 \ y"} for @{text "prod G x y"} etc.\ mimics common - practice of informal mathematics quite nicely, while using a simple - and robust formal representation. -*} - end