--- a/doc-src/Locales/IsaMakefile Fri Aug 19 22:44:36 2005 +0200
+++ b/doc-src/Locales/IsaMakefile Fri Aug 19 22:50:20 2005 +0200
@@ -13,7 +13,7 @@
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
-USEDIR = $(ISATOOL) usedir -i true -d "" -D generated
+USEDIR = $(ISATOOL) usedir -d false -D document
## Locales
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Locales/Locales/document/Locales.tex Fri Aug 19 22:50:20 2005 +0200
@@ -0,0 +1,1320 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Locales}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isamarkuptrue%
+%
+\isamarkupsection{Overview%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The present text is based on~\cite{Ballarin2004a}. It was updated
+ for for Isabelle2005, but does not cover locale interpretation.
+
+ Locales are an extension of the Isabelle proof assistant. They
+ provide support for modular reasoning. Locales were initially
+ developed by Kamm\"uller~\cite{Kammuller2000} to support reasoning
+ in abstract algebra, but are applied also in other domains --- for
+ example, bytecode verification~\cite{Klein2003}.
+
+ Kamm\"uller's original design, implemented in Isabelle99, provides, in
+ addition to
+ means for declaring locales, a set of ML functions that were used
+ along with ML tactics in a proof. In the meantime, the input format
+ for proof in Isabelle has changed and users write proof
+ scripts in ML only rarely if at all. Two new proof styles are
+ available, and can
+ be used interchangeably: linear proof scripts that closely resemble ML
+ tactics, and the structured Isar proof language by
+ Wenzel~\cite{Wenzel2002a}. Subsequently, Wenzel re-implemented
+ locales for
+ the new proof format. The implementation, available with
+ Isabelle2003, constitutes a complete re-design and exploits that
+ both Isar and locales are based on the notion of context,
+ and thus locales are seen as a natural extension of Isar.
+ Nevertheless, locales can also be used with proof scripts:
+ their use does not require a deep understanding of the structured
+ Isar proof style.
+
+ At the same time, Wenzel considerably extended locales. The most
+ important addition are locale expressions, which allow to combine
+ locales more freely. Previously only
+ linear inheritance was possible. Now locales support multiple
+ inheritance through a normalisation algorithm. New are also
+ structures, which provide special syntax for locale parameters that
+ represent algebraic structures.
+
+ Unfortunately, Wenzel provided only an implementation but hardly any
+ documentation. Besides providing documentation, the present paper
+ is a high-level description of locales, and in particular locale
+ expressions. It is meant as a first step towards the semantics of
+ locales, and also as a base for comparing locales with module concepts
+ in other provers. It also constitutes the base for future
+ extensions of locales in Isabelle.
+ The description was derived mainly by experimenting
+ with locales and partially also by inspecting the code.
+
+ The main contribution of the author of the present paper is the
+ abstract description of Wenzel's version of locales, and in
+ particular of the normalisation algorithm for locale expressions (see
+ Section~\ref{sec-normal-forms}). Contributions to the
+ implementation are confined to bug fixes and to provisions that
+ enable the use of locales with linear proof scripts.
+
+ Concepts are introduced along with examples, so that the text can be
+ used as tutorial. It is assumed that the reader is somewhat
+ familiar with Isabelle proof scripts. Examples have been phrased as
+ structured
+ Isar proofs. However, in order to understand the key concepts,
+ including locales expressions and their normalisation, detailed
+ knowledge of Isabelle is not necessary.
+
+\nocite{Nipkow2003,Wenzel2002b,Wenzel2003}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Locales: Beyond Proof Contexts%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In tactic-based provers the application of a sequence of proof
+ tactics leads to a proof state. This state is usually hard to
+ predict from looking at the tactic script, unless one replays the
+ proof step-by-step. The structured proof language Isar is
+ different. It is additionally based on \emph{proof contexts},
+ which are directly visible in Isar scripts, and since tactic
+ sequences tend to be short, this commonly leads to clearer proof
+ scripts.
+
+ Goals are stated with the \textbf{theorem}
+ command. This is followed by a proof. When discharging a goal
+ requires an elaborate argument
+ (rather than the application of a single tactic) a new context
+ may be entered (\textbf{proof}). Inside the context, variables may
+ be fixed (\textbf{fix}), assumptions made (\textbf{assume}) and
+ intermediate goals stated (\textbf{have}) and proved. The
+ assumptions must be dischargeable by premises of the surrounding
+ goal, and once this goal has been proved (\textbf{show}) the proof context
+ can be closed (\textbf{qed}). Contexts inherit from surrounding
+ contexts, but it is not possible
+ to export from them (with exception of the proved goal);
+ they ``disappear'' after the closing \textbf{qed}.
+ Facts may have attributes --- for example, identifying them as
+ default to the simplifier or classical reasoner.
+
+ Locales extend proof contexts in various ways:
+ \begin{itemize}
+ \item
+ Locales are usually \emph{named}. This makes them persistent.
+ \item
+ Fixed variables may have \emph{syntax}.
+ \item
+ It is possible to \emph{add} and \emph{export} facts.
+ \item
+ Locales can be combined and modified with \emph{locale
+ expressions}.
+ \end{itemize}
+ The Locales facility extends the Isar language: it provides new ways
+ of stating and managing facts, but it does not modify the language
+ for proofs. Its purpose is to support writing modular proofs.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Simple Locales%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Syntax and Terminology%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The grammar of Isar is extended by commands for locales as shown in
+ Figure~\ref{fig-grammar}.
+ A key concept, introduced by Wenzel, is that
+ locales are (internally) lists
+ of \emph{context elements}. There are five kinds, identified
+ by the keywords \textbf{fixes}, \textbf{constrains},
+ \textbf{assumes}, \textbf{defines} and \textbf{notes}.
+
+ \begin{figure}
+ \hrule
+ \vspace{2ex}
+ \begin{small}
+ \begin{tabular}{l>$c<$l}
+ \textit{attr-name} & ::=
+ & \textit{name} $|$ \textit{attribute} $|$
+ \textit{name} \textit{attribute} \\
+
+ \textit{locale-expr} & ::=
+ & \textit{locale-expr1} ( ``\textbf{+}'' \textit{locale-expr1} )$^*$ \\
+ \textit{locale-expr1} & ::=
+ & ( \textit{qualified-name} $|$
+ ``\textbf{(}'' \textit{locale-expr} ``\textbf{)}'' ) \\
+ & & ( \textit{name} [ \textit{mixfix} ] $|$ ``\textbf{\_}'' )$^*$ \\
+
+ \textit{fixes} & ::=
+ & \textit{name} [ ``\textbf{::}'' \textit{type} ]
+ [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
+ \textit{mixfix} ] \\
+ \textit{constrains} & ::=
+ & \textit{name} ``\textbf{::}'' \textit{type} \\
+ \textit{assumes} & ::=
+ & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
+ \textit{defines} & ::=
+ & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
+ \textit{notes} & ::=
+ & [ \textit{attr-name} ``\textbf{=}'' ]
+ ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
+
+ \textit{element} & ::=
+ & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
+ & |
+ & \textbf{constrains} \textit{constrains}
+ ( \textbf{and} \textit{constrains} )$^*$ \\
+ & |
+ & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\
+ & |
+ & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
+ & |
+ & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
+ \textit{element1} & ::=
+ & \textit{element} \\
+ & | & \textbf{includes} \textit{locale-expr} \\
+
+ \textit{locale} & ::=
+ & \textit{element}$^+$ \\
+ & | & \textit{locale-expr} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
+
+ \textit{in-target} & ::=
+ & ``\textbf{(}'' \textbf{in} \textit{qualified-name} ``\textbf{)}'' \\
+
+ \textit{theorem} & ::= & ( \textbf{theorem} $|$ \textbf{lemma} $|$
+ \textbf{corollary} ) [ \textit{in-target} ] [ \textit{attr-name} ] \\
+
+ \textit{theory-level} & ::= & \ldots \\
+ & | & \textbf{locale} \textit{name} [ ``\textbf{=}''
+ \textit{locale} ] \\
+ % note: legacy "locale (open)" omitted.
+ & | & ( \textbf{theorems} $|$ \textbf{lemmas} ) \\
+ & & [ \textit{in-target} ] [ \textit{attr-name} ``\textbf{=}'' ]
+ ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
+ & | & \textbf{declare} [ \textit{in-target} ] ( \textit{qualified-name}
+ [ \textit{attribute} ] )$^+$ \\
+ & | & \textit{theorem} \textit{proposition} \textit{proof} \\
+ & | & \textit{theorem} \textit{element1}$^*$
+ \textbf{shows} \textit{proposition} \textit{proof} \\
+ & | & \textbf{print\_locale} \textit{locale} \\
+ & | & \textbf{print\_locales}
+ \end{tabular}
+ \end{small}
+ \vspace{2ex}
+ \hrule
+ \caption{Locales extend the grammar of Isar.}
+ \label{fig-grammar}
+ \end{figure}
+
+ At the theory level --- that is, at the outer syntactic level of an
+ Isabelle input file --- \textbf{locale} declares a named
+ locale. Other kinds of locales,
+ locale expressions and unnamed locales, will be introduced later. When
+ declaring a named locale, it is possible to \emph{import} another
+ named locale, or indeed several ones by importing a locale
+ expression. The second part of the declaration, also optional,
+ consists of a number of context element declarations.
+
+ A number of Isar commands have an additional, optional \emph{target}
+ argument, which always refers to a named locale. These commands
+ are \textbf{theorem} (together with \textbf{lemma} and
+ \textbf{corollary}), \textbf{theorems} (and
+ \textbf{lemmas}), and \textbf{declare}. The effect of specifying a target is
+ that these commands focus on the specified locale, not the
+ surrounding theory. Commands that are used to
+ prove new theorems will add them not to the theory, but to the
+ locale. Similarly, \textbf{declare} modifies attributes of theorems
+ that belong to the specified target. Additionally, for
+ \textbf{theorem} (and related commands), theorems stored in the target
+ can be used in the associated proof scripts.
+
+ The Locales package provides a \emph{long goals format} for
+ propositions stated with \textbf{theorem} (and friends). While
+ normally a goal is just a formula, a long goal is a list of context
+ elements, followed by the keyword \textbf{shows}, followed by the
+ formula. Roughly speaking, the context elements are
+ (additional) premises. For an example, see
+ Section~\ref{sec-includes}. The list of context elements in a long goal
+ is also called \emph{unnamed locale}.
+
+ Finally, there are two commands to inspect locales when working in
+ interactive mode: \textbf{print\_locales} prints the names of all
+ targets
+ visible in the current theory, \textbf{print\_locale} outputs the
+ elements of a named locale or locale expression.
+
+ The following presentation will use notation of
+ Isabelle's meta logic, hence a few sentences to explain this.
+ The logical
+ primitives are universal quantification (\isa{{\isasymAnd}}), entailment
+ (\isa{{\isasymLongrightarrow}}) and equality (\isa{{\isasymequiv}}). Variables (not bound
+ variables) are sometimes preceded by a question mark. The logic is
+ typed. Type variables are denoted by \isa{{\isacharprime}a}, \isa{{\isacharprime}b}
+ etc., and \isa{{\isasymRightarrow}} is the function type. Double brackets \isa{{\isasymlbrakk}} and \isa{{\isasymrbrakk}} are used to abbreviate nested entailment.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Parameters, Assumptions and Facts%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+From a logical point of view a \emph{context} is a formula schema of
+ the form
+\[
+ \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}{\isasymdots}x\isactrlsub n{\isachardot}\ {\isasymlbrakk}\ C\isactrlsub {\isadigit{1}}{\isacharsemicolon}\ {\isasymdots}\ {\isacharsemicolon}C\isactrlsub m\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymdots}}
+\]
+ The variables $\isa{x\isactrlsub {\isadigit{1}}}, \ldots, \isa{x\isactrlsub n}$ are
+ called \emph{parameters}, the premises $\isa{C\isactrlsub {\isadigit{1}}}, \ldots,
+ \isa{C\isactrlsub n}$ \emph{assumptions}. A formula \isa{F}
+ holds in this context if
+\begin{equation}
+\label{eq-fact-in-context}
+ \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}{\isasymdots}x\isactrlsub n{\isachardot}\ {\isasymlbrakk}\ C\isactrlsub {\isadigit{1}}{\isacharsemicolon}\ {\isasymdots}\ {\isacharsemicolon}C\isactrlsub m\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ F}
+\end{equation}
+ is valid. The formula is called a \emph{fact} of the context.
+
+ A locale allows fixing the parameters \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n} and making the assumptions \isa{C\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ C\isactrlsub m}. This implicitly builds the context in
+ which the formula \isa{F} can be established.
+ Parameters of a locale correspond to the context element
+ \textbf{fixes}, and assumptions may be declared with
+ \textbf{assumes}. Using these context elements one can define
+ the specification of semigroups.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{locale}\ semi\ {\isacharequal}\isanewline
+\ \ \isakeyword{fixes}\ prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymcdot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymcdot}\ y{\isacharparenright}\ {\isasymcdot}\ z\ {\isacharequal}\ x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The parameter \isa{prod} has a
+ syntax annotation enabling the infix ``\isa{{\isasymcdot}}'' in the
+ assumption of associativity. Parameters may have arbitrary mixfix
+ syntax, like constants. In the example, the type of \isa{prod} is
+ specified explicitly. This is not necessary. If no type is
+ specified, a most general type is inferred simultaneously for all
+ parameters, taking into account all assumptions (and type
+ specifications of parameters, if present).%
+\footnote{Type inference also takes into account type constraints,
+ definitions and import, as introduced later.}
+
+ Free variables in assumptions are implicitly universally quantified,
+ unless they are parameters. Hence the context defined by the locale
+ \isa{semi} is
+\[
+ \isa{{\isasymAnd}prod{\isachardot}\ {\isasymlbrakk}\ {\isasymAnd}x\ y\ z{\isachardot}\ prod\ {\isacharparenleft}prod\ x\ y{\isacharparenright}\ z\ {\isacharequal}\ prod\ x\ {\isacharparenleft}prod\ y\ z{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymdots}}
+\]
+ The locale can be extended to commutative semigroups.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{locale}\ comm{\isacharunderscore}semi\ {\isacharequal}\ semi\ {\isacharplus}\isanewline
+\ \ \isakeyword{assumes}\ comm{\isacharcolon}\ {\isachardoublequote}x\ {\isasymcdot}\ y\ {\isacharequal}\ y\ {\isasymcdot}\ x{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This locale \emph{imports} all elements of \isa{semi}. The
+ latter locale is called the import of \isa{comm{\isacharunderscore}semi}. The
+ definition adds commutativity, hence its context is
+\begin{align*%
+}
+ \isa{{\isasymAnd}prod{\isachardot}\ {\isasymlbrakk}} &
+ \isa{{\isasymAnd}x\ y\ z{\isachardot}\ prod\ {\isacharparenleft}prod\ x\ y{\isacharparenright}\ z\ {\isacharequal}\ prod\ x\ {\isacharparenleft}prod\ y\ z{\isacharparenright}{\isacharsemicolon}} \\
+ & \isa{{\isasymAnd}x\ y{\isachardot}\ prod\ x\ y\ {\isacharequal}\ prod\ y\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymdots}}
+\end{align*%
+}
+ One may now derive facts --- for example, left-commutativity --- in
+ the context of \isa{comm{\isacharunderscore}semi} by specifying this locale as
+ target, and by referring to the names of the assumptions \isa{assoc} and \isa{comm} in the proof.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{theorem}\ {\isacharparenleft}\isakeyword{in}\ comm{\isacharunderscore}semi{\isacharparenright}\ lcomm{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}\ {\isacharequal}\ y\ {\isasymcdot}\ {\isacharparenleft}x\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharminus}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymcdot}\ y{\isacharparenright}\ {\isasymcdot}\ z{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymcdot}\ x{\isacharparenright}\ {\isasymcdot}\ z{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ comm{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ y\ {\isasymcdot}\ {\isacharparenleft}x\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In this equational Isar proof, ``\isa{{\isasymdots}}'' refers to the
+ right hand side of the preceding equation.
+ After the proof is finished, the fact \isa{lcomm} is added to
+ the locale \isa{comm{\isacharunderscore}semi}. This is done by adding a
+ \textbf{notes} element to the internal representation of the locale,
+ as explained the next section.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Locale Predicates and the Internal Representation of
+ Locales%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec-locale-predicates}
+ In mathematical texts, often arbitrary but fixed objects with
+ certain properties are considered --- for instance, an arbitrary but
+ fixed group $G$ --- with the purpose of establishing facts valid for
+ any group. These facts are subsequently used on other objects that
+ also have these properties.
+
+ Locales permit the same style of reasoning. Exporting a fact $F$
+ generalises the fixed parameters and leads to a (valid) formula of the
+ form of equation~(\ref{eq-fact-in-context}). If a locale has many
+ assumptions
+ (possibly accumulated through a number of imports) this formula can
+ become large and cumbersome. Therefore, Wenzel introduced
+ predicates that abbreviate the assumptions of locales. These
+ predicates are not confined to the locale but are visible in the
+ surrounding theory.
+
+ The definition of the locale \isa{semi} generates the \emph{locale
+ predicate} \isa{semi} over the type of the parameter \isa{prod},
+ hence the predicate's type is \isa{{\isacharparenleft}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ bool}. Its
+ definition is
+\begin{equation}
+ \tag*{\isa{semi{\isacharunderscore}def}:} \isa{semi\ {\isacharquery}prod\ {\isasymequiv}\ {\isasymforall}x\ y\ z{\isachardot}\ {\isacharquery}prod\ {\isacharparenleft}{\isacharquery}prod\ x\ y{\isacharparenright}\ z\ {\isacharequal}\ {\isacharquery}prod\ x\ {\isacharparenleft}{\isacharquery}prod\ y\ z{\isacharparenright}}.
+\end{equation}
+ In the case where the locale has no import, the generated
+ predicate abbreviates all assumptions and is over the parameters
+ that occur in these assumptions.
+
+ The situation is more complicated when a locale extends
+ another locale, as is the case for \isa{comm{\isacharunderscore}semi}. Two
+ predicates are defined. The predicate
+ \isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms} corresponds to the new assumptions and is
+ called \emph{delta predicate}, the locale
+ predicate \isa{comm{\isacharunderscore}semi} captures the content of all the locale,
+ including the import.
+ If a locale has neither assumptions nor import, no predicate is
+ defined. If a locale has import but no assumptions, only the locale
+ predicate is defined.%
+\end{isamarkuptext}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The Locales package generates a number of theorems for locale and
+ delta predicates. All predicates have a definition and an
+ introduction rule. Locale predicates that are defined in terms of
+ other predicates (which is the case if and only if the locale has
+ import) also have a number of elimination rules (called
+ \emph{axioms}). All generated theorems for the predicates of the
+ locales \isa{semi} and \isa{comm{\isacharunderscore}semi} are shown in
+ Figures~\ref{fig-theorems-semi} and~\ref{fig-theorems-comm-semi},
+ respectively.
+ \begin{figure}
+ \hrule
+ \vspace{2ex}
+ Theorems generated for the predicate \isa{semi}.
+ \begin{gather}
+ \tag*{\isa{semi{\isacharunderscore}def}:} \isa{semi\ {\isacharquery}prod\ {\isasymequiv}\ {\isasymforall}x\ y\ z{\isachardot}\ {\isacharquery}prod\ {\isacharparenleft}{\isacharquery}prod\ x\ y{\isacharparenright}\ z\ {\isacharequal}\ {\isacharquery}prod\ x\ {\isacharparenleft}{\isacharquery}prod\ y\ z{\isacharparenright}} \\
+ \tag*{\isa{semi{\isachardot}intro}:} \isa{{\isacharparenleft}{\isasymAnd}x\ y\ z{\isachardot}\ {\isacharquery}prod\ {\isacharparenleft}{\isacharquery}prod\ x\ y{\isacharparenright}\ z\ {\isacharequal}\ {\isacharquery}prod\ x\ {\isacharparenleft}{\isacharquery}prod\ y\ z{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ semi\ {\isacharquery}prod}
+ \end{gather}
+ \hrule
+ \caption{Theorems for the locale predicate \isa{semi}.}
+ \label{fig-theorems-semi}
+ \end{figure}
+
+ \begin{figure}[h]
+ \hrule
+ \vspace{2ex}
+ Theorems generated for the predicate \isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms}.
+ \begin{gather}
+ \tag*{\isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms{\isacharunderscore}def}:} \isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms\ {\isacharquery}prod\ {\isasymequiv}\ {\isasymforall}x\ y{\isachardot}\ {\isacharquery}prod\ x\ y\ {\isacharequal}\ {\isacharquery}prod\ y\ x} \\
+ \tag*{\isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms{\isachardot}intro}:} \isa{{\isacharparenleft}{\isasymAnd}x\ y{\isachardot}\ {\isacharquery}prod\ x\ y\ {\isacharequal}\ {\isacharquery}prod\ y\ x{\isacharparenright}\ {\isasymLongrightarrow}\ comm{\isacharunderscore}semi{\isacharunderscore}axioms\ {\isacharquery}prod}
+ \end{gather}
+ Theorems generated for the predicate \isa{comm{\isacharunderscore}semi}.
+ \begin{gather}
+ \tag*{\isa{comm{\isacharunderscore}semi{\isacharunderscore}def}:} \isa{comm{\isacharunderscore}semi\ {\isacharquery}prod\ {\isasymequiv}\ semi\ {\isacharquery}prod\ {\isasymand}\ comm{\isacharunderscore}semi{\isacharunderscore}axioms\ {\isacharquery}prod} \\
+ \tag*{\isa{comm{\isacharunderscore}semi{\isachardot}intro}:} \isa{{\isasymlbrakk}semi\ {\isacharquery}prod{\isacharsemicolon}\ comm{\isacharunderscore}semi{\isacharunderscore}axioms\ {\isacharquery}prod{\isasymrbrakk}\ {\isasymLongrightarrow}\ comm{\isacharunderscore}semi\ {\isacharquery}prod} \\
+ \tag*{\isa{comm{\isacharunderscore}semi{\isachardot}axioms}:} \mbox{} \\
+ \notag \isa{comm{\isacharunderscore}semi\ {\isacharquery}prod\ {\isasymLongrightarrow}\ semi\ {\isacharquery}prod} \\
+ \notag \isa{comm{\isacharunderscore}semi\ {\isacharquery}prod\ {\isasymLongrightarrow}\ comm{\isacharunderscore}semi{\isacharunderscore}axioms\ {\isacharquery}prod}
+ \end{gather}
+ \hrule
+ \caption{Theorems for the predicates \isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms} and
+ \isa{comm{\isacharunderscore}semi}.}
+ \label{fig-theorems-comm-semi}
+ \end{figure}
+ Note that the theorems generated by a locale
+ definition may be inspected immediately after the definition in the
+ Proof General interface \cite{Aspinall2000} of Isabelle through
+ the menu item ``Isabelle/Isar$>$Show me $\ldots>$Theorems''.
+
+ Locale and delta predicates are used also in the internal
+ representation of locales as lists of context elements. While all
+ \textbf{fixes} in a
+ declaration generate internal \textbf{fixes}, all assumptions
+ of one locale declaration contribute to one internal \textbf{assumes}
+ element. The internal representation of \isa{semi} is
+\[
+\begin{array}{ll}
+ \textbf{fixes} & \isa{prod} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}}
+ (\textbf{infixl} \isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}} 70) \\
+ \textbf{assumes} & \isa{{\isachardoublequote}semi\ prod{\isachardoublequote}} \\
+ \textbf{notes} & \isa{assoc}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}}
+\end{array}
+\]
+ and the internal representation of \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isachardoublequote}} is
+\begin{equation}
+\label{eq-comm-semi}
+\begin{array}{ll}
+ \textbf{fixes} & \isa{prod} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}}
+ ~(\textbf{infixl}~\isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}}~70) \\
+ \textbf{assumes} & \isa{{\isachardoublequote}semi\ prod{\isachardoublequote}} \\
+ \textbf{notes} & \isa{assoc}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
+ \textbf{assumes} & \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isacharunderscore}axioms\ prod{\isachardoublequote}} \\
+ \textbf{notes} & \isa{comm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}x{\isachardoublequote}} \\
+ \textbf{notes} & \isa{lcomm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}}
+\end{array}
+\end{equation}
+ The \textbf{notes} elements store facts of the
+ locales. The facts \isa{assoc} and \isa{comm} were added
+ during the declaration of the locales. They stem from assumptions,
+ which are trivially facts. The fact \isa{lcomm} was
+ added later, after finishing the proof in the respective
+ \textbf{theorem} command above.
+
+ By using \textbf{notes} in a declaration, facts can be added
+ to a locale directly. Of course, these must be theorems.
+ Typical use of this feature includes adding theorems that are not
+ usually used as a default rewrite rules by the simplifier to the
+ simpset of the locale by a \textbf{notes} element with the attribute
+ \isa{{\isacharbrackleft}simp{\isacharbrackright}}. This way it is also possible to add specialised
+ versions of
+ theorems to a locale by instantiating locale parameters for unknowns
+ or locale assumptions for premises.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Definitions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Definitions were available in Kamm\"uller's version of Locales, and
+ they are in Wenzel's.
+ The context element \textbf{defines} adds a definition of the form
+ \isa{p\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t} as an assumption, where \isa{p} is a
+ parameter of the locale (possibly an imported parameter), and \isa{t} a term that may contain the \isa{x\isactrlsub i}. The parameter may
+ neither occur in a previous \textbf{assumes} or \textbf{defines}
+ element, nor on the right hand side of the definition. Hence
+ recursion is not allowed.
+ The parameter may, however, occur in subsequent \textbf{assumes} and
+ on the right hand side of subsequent \textbf{defines}. We call
+ \isa{p} \emph{defined parameter}.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{locale}\ semi{\isadigit{2}}\ {\isacharequal}\ semi\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ rprod\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ \isakeyword{defines}\ rprod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}rprod\ x\ y\ {\isasymequiv}\ y\ {\isasymcdot}\ x\ {\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This locale extends \isa{semi} by a second binary operation \isa{{\isachardoublequote}{\isasymodot}{\isachardoublequote}} that is like \isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}} but with
+ reversed arguments. The
+ definition of the locale generates the predicate \isa{semi{\isadigit{2}}},
+ which is equivalent to \isa{semi}, but no \isa{semi{\isadigit{2}}{\isacharunderscore}axioms}.
+ The difference between \textbf{assumes} and \textbf{defines} lies in
+ the way parameters are treated on export.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Export%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A fact is exported out
+ of a locale by generalising over the parameters and adding
+ assumptions as premises. For brevity of the exported theorems,
+ locale predicates are used. Exported facts are referenced by
+ writing qualified names consisting of the locale name and the fact name ---
+ for example,
+\begin{equation}
+ \tag*{\isa{semi{\isachardot}assoc}:} \isa{semi\ {\isacharquery}prod\ {\isasymLongrightarrow}\ {\isacharquery}prod\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}prod\ {\isacharquery}x\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}}.
+\end{equation}
+ Defined parameters receive special treatment. Instead of adding a
+ premise for the definition, the definition is unfolded in the
+ exported theorem. In order to illustrate this we prove that the
+ reverse operation \isa{{\isachardoublequote}{\isasymodot}{\isachardoublequote}} defined in the locale
+ \isa{semi{\isadigit{2}}} is also associative.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{theorem}\ {\isacharparenleft}\isakeyword{in}\ semi{\isadigit{2}}{\isacharparenright}\ r{\isacharunderscore}assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ rprod{\isacharunderscore}def\ assoc{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The exported fact is
+\begin{equation}
+ \tag*{\isa{semi{\isadigit{2}}{\isachardot}r{\isacharunderscore}assoc}:} \isa{semi{\isadigit{2}}\ {\isacharquery}prod\ {\isasymLongrightarrow}\ {\isacharquery}prod\ {\isacharquery}z\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}y\ {\isacharquery}x{\isacharparenright}\ {\isacharequal}\ {\isacharquery}prod\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}z\ {\isacharquery}y{\isacharparenright}\ {\isacharquery}x}.
+\end{equation}
+ The defined parameter is not present but is replaced by its
+ definition. Note that the definition itself is not exported, hence
+ there is no \isa{semi{\isadigit{2}}{\isachardot}rprod{\isacharunderscore}def}.%
+\footnote{The definition could alternatively be exported using a
+ let-construct if there was one in Isabelle's meta-logic. Let is
+ usually defined in object-logics.}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Locale Expressions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Locale expressions provide a simple language for combining
+ locales. They are an effective means of building complex
+ specifications from simple ones. Locale expressions are the main
+ innovation of the version of Locales discussed here. Locale
+ expressions are also reason for introducing locale predicates.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Rename and Merge%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The grammar of locale expressions is part of the grammar in
+ Figure~\ref{fig-grammar}. Locale names are locale
+ expressions, and
+ further expressions are obtained by \emph{rename} and \emph{merge}.
+\begin{description}
+\item[Rename.]
+ The locale expression $e\: q_1 \ldots q_n$ denotes
+ the locale of $e$ where pa\-ra\-me\-ters, in the order in
+ which they are fixed, are renamed to $q_1$ to $q_n$.
+ The expression is only well-formed if $n$ does not
+ exceed the number of parameters of $e$. Underscores denote
+ parameters that are not renamed.
+ Renaming by default removes mixfix syntax, but new syntax may be
+ specified.
+\item[Merge.]
+ The locale expression $e_1 + e_2$ denotes
+ the locale obtained by merging the locales of $e_1$
+ and $e_2$. This locale contains the context elements
+ of $e_1$, followed by the context elements of $e_2$.
+
+ In actual fact, the semantics of the merge operation
+ is more complicated. If $e_1$ and $e_2$ are expressions containing
+ the same name, followed by
+ identical parameter lists, then the merge of both will contain
+ the elements of those locales only once. Details are explained in
+ Section~\ref{sec-normal-forms} below.
+
+ The merge operation is associative but not commutative. The latter
+ is because parameters of $e_1$ appear
+ before parameters of $e_2$ in the composite expression.
+\end{description}
+
+ Rename can be used if a different parameter name seems more
+ appropriate --- for example, when moving from groups to rings, a
+ parameter \isa{G} representing the group could be changed to
+ \isa{R}. Besides of this stylistic use, renaming is important in
+ combination with merge. Both operations are used in the following
+ specification of semigroup homomorphisms.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{locale}\ semi{\isacharunderscore}hom\ {\isacharequal}\ comm{\isacharunderscore}semi\ sum\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\ {\isacharplus}\ comm{\isacharunderscore}semi\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ hom\isanewline
+\ \ \isakeyword{assumes}\ hom{\isacharcolon}\ {\isachardoublequote}hom\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isacharequal}\ hom\ x\ {\isasymcdot}\ hom\ y{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This locale defines a context with three parameters \isa{sum},
+ \isa{prod} and \isa{hom}. The first two parameters have
+ mixfix syntax. They are associative operations,
+ the first of type \isa{{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a}, the second of
+ type \isa{{\isacharbrackleft}{\isacharprime}b{\isacharcomma}\ {\isacharprime}b{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}b}.
+
+ How are facts that are imported via a locale expression identified?
+ Facts are always introduced in a named locale (either in the
+ locale's declaration, or by using the locale as target in
+ \textbf{theorem}), and their names are
+ qualified by the parameter names of this locale.
+ Hence the full name of associativity in \isa{semi} is
+ \isa{prod{\isachardot}assoc}. Renaming parameters of a target also renames
+ the qualifier of facts. Hence, associativity of \isa{sum} is
+ \isa{sum{\isachardot}assoc}. Several parameters are separated by
+ underscores in qualifiers. For example, the full name of the fact
+ \isa{hom} in the locale \isa{semi{\isacharunderscore}hom} is \isa{sum{\isacharunderscore}prod{\isacharunderscore}hom{\isachardot}hom}.
+
+ The following example is quite artificial, it illustrates the use of
+ facts, though.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{theorem}\ {\isacharparenleft}\isakeyword{in}\ semi{\isacharunderscore}hom{\isacharparenright}\ {\isachardoublequote}hom\ x\ {\isasymcdot}\ {\isacharparenleft}hom\ y\ {\isasymcdot}\ hom\ z{\isacharparenright}\ {\isacharequal}\ hom\ {\isacharparenleft}x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharminus}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}hom\ x\ {\isasymcdot}\ {\isacharparenleft}hom\ y\ {\isasymcdot}\ hom\ z{\isacharparenright}\ {\isacharequal}\ hom\ y\ {\isasymcdot}\ {\isacharparenleft}hom\ x\ {\isasymcdot}\ hom\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ prod{\isachardot}lcomm{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ hom\ {\isacharparenleft}y\ {\isasymoplus}\ {\isacharparenleft}x\ {\isasymoplus}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ hom{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ hom\ {\isacharparenleft}x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ sum{\isachardot}lcomm{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Importing via a locale expression imports all facts of
+ the imported locales, hence both \isa{sum{\isachardot}lcomm} and \isa{prod{\isachardot}lcomm} are
+ available in \isa{hom{\isacharunderscore}semi}. The import is dynamic --- that is,
+ whenever facts are added to a locale, they automatically
+ become available in subsequent \textbf{theorem} commands that use
+ the locale as a target, or a locale importing the locale.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Normal Forms%
+}
+%
+\label{sec-normal-forms}
+\newcommand{\I}{\mathcal{I}}
+\newcommand{\F}{\mathcal{F}}
+\newcommand{\N}{\mathcal{N}}
+\newcommand{\C}{\mathcal{C}}
+\newcommand{\App}{\mathbin{\overline{@}}}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Locale expressions are interpreted in a two-step process. First, an
+ expression is normalised, then it is converted to a list of context
+ elements.
+
+ Normal forms are based on \textbf{locale} declarations. These
+ consist of an import section followed by a list of context
+ elements. Let $\I(l)$ denote the locale expression imported by
+ locale $l$. If $l$ has no import then $\I(l) = \varepsilon$.
+ Likewise, let $\F(l)$ denote the list of context elements, also
+ called the \emph{context fragment} of $l$. Note that $\F(l)$
+ contains only those context elements that are stated in the
+ declaration of $l$, not imported ones.
+
+\paragraph{Example 1.} Consider the locales \isa{semi} and \isa{comm{\isacharunderscore}semi}. We have $\I(\isa{semi}) = \varepsilon$ and
+ $\I(\isa{comm{\isacharunderscore}semi}) = \isa{semi}$, and the context fragments
+ are
+\begin{align*%
+}
+ \F(\isa{semi}) & = \left[
+\begin{array}{ll}
+ \textbf{fixes} & \isa{prod} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}}
+ ~(\textbf{infixl}~\isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}}~70) \\
+ \textbf{assumes} & \isa{{\isachardoublequote}semi\ prod{\isachardoublequote}} \\
+ \textbf{notes} & \isa{assoc}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}}
+\end{array} \right], \\
+ \F(\isa{comm{\isacharunderscore}semi}) & = \left[
+\begin{array}{ll}
+ \textbf{assumes} & \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isacharunderscore}axioms\ prod{\isachardoublequote}} \\
+ \textbf{notes} & \isa{comm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}x{\isachardoublequote}} \\
+ \textbf{notes} & \isa{lcomm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}}
+\end{array} \right].
+\end{align*%
+}
+ Let $\pi_0(\F(l))$ denote the list of parameters defined in the
+ \textbf{fixes} elements of $\F(l)$ in the order of their occurrence.
+ The list of parameters of a locale expression $\pi(e)$ is defined as
+ follows:
+\begin{align*%
+}
+ \pi(l) & = \pi(\I(l)) \App \pi_0(\F(l)) \text{, for named locale $l$.} \\
+ \pi(e\: q_1 \ldots q_n) & = \text{$[q_1, \ldots, q_n, p_{n+1}, \ldots,
+ p_{m}]$, where $\pi(e) = [p_1, \ldots, p_m]$.} \\
+ \pi(e_1 + e_2) & = \pi(e_1) \App \pi(e_2)
+\end{align*%
+}
+ The operation $\App$ concatenates two lists but omits elements from
+ the second list that are also present in the first list.
+ It is not possible to rename more parameters than there
+ are present in an expression --- that is, $n \le m$ --- otherwise
+ the renaming is illegal. If $q_i
+ = \_$ then the $i$th entry of the resulting list is $p_i$.
+
+ In the normalisation phase, imports of named locales are unfolded, and
+ renames and merges are recursively propagated to the imported locale
+ expressions. The result is a list of locale names, each with a full
+ list of parameters, where locale names occurring with the same parameter
+ list twice are removed. Let $\N$ denote normalisation. It is defined
+ by these equations:
+\begin{align*%
+}
+ \N(l) & = \N(\I(l)) \App [l\:\pi(l)] \text{, for named locale $l$.} \\
+ \N(e\: q_1 \ldots q_n) & = \N(e)\:[q_1 \ldots q_n/\pi(e)] \\
+ \N(e_1 + e_2) & = \N(e_1) \App \N(e_2)
+\end{align*%
+}
+ Normalisation yields a list of \emph{identifiers}. An identifier
+ consists of a locale name and a (possibly empty) list of parameters.
+
+ In the second phase, the list of identifiers $\N(e)$ is converted to
+ a list of context elements $\C(e)$ by converting each identifier to
+ a list of context elements, and flattening the obtained list.
+ Conversion of the identifier $l\:q_1 \ldots q_n$ yields the list of
+ context elements $\F(l)$, but with the following modifications:
+\begin{itemize}
+\item
+ Rename the parameter in the $i$th \textbf{fixes} element of $\F(l)$
+ to $q_i$, $i = 1, \ldots, n$. If the parameter name is actually
+ changed then delete the syntax annotation. Renaming a parameter may
+ also change its type.
+\item
+ Perform the same renamings on all occurrences of parameters (fixed
+ variables) in \textbf{assumes}, \textbf{defines} and \textbf{notes}
+ elements.
+\item
+ Qualify names of facts by $q_1\_\ldots\_q_n$.
+\end{itemize}
+ The locale expression is \emph{well-formed} if it contains no
+ illegal renamings and the following conditions on $\C(e)$ hold,
+ otherwise the expression is rejected:
+\begin{itemize}
+\item Parameters in \textbf{fixes} are distinct;
+\item Free variables in \textbf{assumes} and
+ \textbf{defines} occur in preceding \textbf{fixes};%
+\footnote{This restriction is relaxed for contexts obtained with
+ \textbf{includes}, see Section~\ref{sec-includes}.}
+\item Parameters defined in \textbf{defines} must neither occur in
+ preceding \textbf{assumes} nor \textbf{defines}.
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\paragraph{Example 2.}
+ We obtain the context fragment $\C(\isa{comm{\isacharunderscore}semi})$ of the
+ locale \isa{comm{\isacharunderscore}semi}. First, the parameters are computed.
+\begin{align*%
+}
+ \pi(\isa{semi}) & = [\isa{prod}] \\
+ \pi(\isa{comm{\isacharunderscore}semi}) & = \pi(\isa{semi}) \App []
+ = [\isa{prod}]
+\end{align*%
+}
+ Next, the normal form of the locale expression
+ \isa{comm{\isacharunderscore}semi} is obtained.
+\begin{align*%
+}
+ \N(\isa{semi}) & = [\isa{semi} \isa{prod}] \\
+ \N(\isa{comm{\isacharunderscore}semi}) & = \N(\isa{semi}) \App
+ [\isa{comm{\isacharunderscore}semi\ prod}]
+ = [\isa{semi\ prod}, \isa{comm{\isacharunderscore}semi\ prod}]
+\end{align*%
+}
+ Converting this to a list of context elements leads to the
+ list~(\ref{eq-comm-semi}) shown in
+ Section~\ref{sec-locale-predicates}, but with fact names qualified
+ by \isa{prod} --- for example, \isa{prod{\isachardot}assoc}.
+ Qualification was omitted to keep the presentation simple.
+ Isabelle's scoping rules identify the most recent fact with
+ qualified name $x.a$ when a fact with name $a$ is requested.
+
+\paragraph{Example 3.}
+ The locale expression \isa{comm{\isacharunderscore}semi\ sum} involves
+ renaming. Computing parameters yields $\pi(\isa{comm{\isacharunderscore}semi\ sum})
+ = [\isa{sum}]$, the normal form is
+\begin{align*%
+}
+ \N(\isa{comm{\isacharunderscore}semi\ sum}) & =
+ \N(\isa{comm{\isacharunderscore}semi})[\isa{sum}/\isa{prod}] =
+ [\isa{semi\ sum}, \isa{comm{\isacharunderscore}semi\ sum}]
+\end{align*%
+}
+ and the list of context elements
+\[
+\begin{array}{ll}
+ \textbf{fixes} & \isa{sum} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}}
+ ~(\textbf{infixl}~\isa{{\isachardoublequote}{\isasymoplus}{\isachardoublequote}}~65) \\
+ \textbf{assumes} & \isa{{\isachardoublequote}semi\ sum{\isachardoublequote}} \\
+ \textbf{notes} & \isa{sum{\isachardot}assoc}: \isa{{\isachardoublequote}{\isacharparenleft}{\isacharquery}x\ {\isasymoplus}\ {\isacharquery}y{\isacharparenright}\ {\isasymoplus}\ {\isacharquery}z\ {\isacharequal}\ sum\ {\isacharquery}x\ {\isacharparenleft}sum\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
+ \textbf{assumes} & \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isacharunderscore}axioms\ sum{\isachardoublequote}} \\
+ \textbf{notes} & \isa{sum{\isachardot}comm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymoplus}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}y\ {\isasymoplus}\ {\isacharquery}x{\isachardoublequote}} \\
+ \textbf{notes} & \isa{sum{\isachardot}lcomm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymoplus}\ {\isacharparenleft}{\isacharquery}y\ {\isasymoplus}\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ {\isacharquery}y\ {\isasymoplus}\ {\isacharparenleft}{\isacharquery}x\ {\isasymoplus}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}}
+\end{array}
+\]
+
+\paragraph{Example 4.}
+ The context defined by the locale \isa{semi{\isacharunderscore}hom} involves
+ merging two copies of \isa{comm{\isacharunderscore}semi}. We obtain the parameter
+ list and normal form:
+\begin{align*%
+}
+ \pi(\isa{semi{\isacharunderscore}hom}) & = \pi(\isa{comm{\isacharunderscore}semi\ sum} +
+ \isa{comm{\isacharunderscore}semi}) \App [\isa{hom}] \\
+ & = (\pi(\isa{comm{\isacharunderscore}semi\ sum}) \App \pi(\isa{comm{\isacharunderscore}semi}))
+ \App [\isa{hom}] \\
+ & = ([\isa{sum}] \App [\isa{prod}]) \App [\isa{hom}]
+ = [\isa{sum}, \isa{prod}, \isa{hom}] \\
+ \N(\isa{semi{\isacharunderscore}hom}) & =
+ \N(\isa{comm{\isacharunderscore}semi\ sum} + \isa{comm{\isacharunderscore}semi}) \App \\
+ & \phantom{==}
+ [\isa{semi{\isacharunderscore}hom\ sum\ prod\ hom}] \\
+ & = (\N(\isa{comm{\isacharunderscore}semi\ sum}) \App \N(\isa{comm{\isacharunderscore}semi})) \App \\
+ & \phantom{==}
+ [\isa{semi{\isacharunderscore}hom\ sum\ prod\ hom}] \\
+ & = ([\isa{semi\ sum}, \isa{comm{\isacharunderscore}semi\ sum}] \App %\\
+% & \phantom{==}
+ [\isa{semi\ prod}, \isa{comm{\isacharunderscore}semi\ prod}]) \App \\
+ & \phantom{==}
+ [\isa{semi{\isacharunderscore}hom\ sum\ prod\ hom}] \\
+ & = [\isa{semi\ sum}, \isa{comm{\isacharunderscore}semi\ sum},
+ \isa{semi\ prod}, \isa{comm{\isacharunderscore}semi\ prod}, \\
+ & \phantom{==}
+ \isa{semi{\isacharunderscore}hom\ sum\ prod\ hom}].
+\end{align*%
+}
+ Hence $\C(\isa{semi{\isacharunderscore}hom})$, shown below, is again well-formed.
+\[
+\begin{array}{ll}
+ \textbf{fixes} & \isa{sum} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}}
+ ~(\textbf{infixl}~\isa{{\isachardoublequote}{\isasymoplus}{\isachardoublequote}}~65) \\
+ \textbf{assumes} & \isa{{\isachardoublequote}semi\ sum{\isachardoublequote}} \\
+ \textbf{notes} & \isa{sum{\isachardot}assoc}: \isa{{\isachardoublequote}{\isacharparenleft}{\isacharquery}x\ {\isasymoplus}\ {\isacharquery}y{\isacharparenright}\ {\isasymoplus}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}x\ {\isasymoplus}\ {\isacharparenleft}{\isacharquery}y\ {\isasymoplus}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
+ \textbf{assumes} & \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isacharunderscore}axioms\ sum{\isachardoublequote}} \\
+ \textbf{notes} & \isa{sum{\isachardot}comm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymoplus}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}y\ {\isasymoplus}\ {\isacharquery}x{\isachardoublequote}} \\
+ \textbf{notes} & \isa{sum{\isachardot}lcomm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymoplus}\ {\isacharparenleft}{\isacharquery}y\ {\isasymoplus}\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ {\isacharquery}y\ {\isasymoplus}\ {\isacharparenleft}{\isacharquery}x\ {\isasymoplus}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
+ \textbf{fixes} & \isa{prod} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}b{\isacharcomma}\ {\isacharprime}b{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequote}}
+ ~(\textbf{infixl}~\isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}}~70) \\
+ \textbf{assumes} & \isa{{\isachardoublequote}semi\ prod{\isachardoublequote}} \\
+ \textbf{notes} & \isa{prod{\isachardot}assoc}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
+ \textbf{assumes} & \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isacharunderscore}axioms\ prod{\isachardoublequote}} \\
+ \textbf{notes} & \isa{prod{\isachardot}comm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}x{\isachardoublequote}} \\
+ \textbf{notes} & \isa{prod{\isachardot}lcomm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
+ \textbf{fixes} & \isa{hom} :: \isa{{\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequote}} \\
+ \textbf{assumes} & \isa{{\isachardoublequote}semi{\isacharunderscore}hom{\isacharunderscore}axioms\ sum{\isachardoublequote}} \\
+ \textbf{notes} & \isa{sum{\isacharunderscore}prod{\isacharunderscore}hom{\isachardot}hom}:
+ \isa{hom\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isacharequal}\ hom\ x\ {\isasymcdot}\ hom\ y}
+\end{array}
+\]
+
+\paragraph{Example 5.}
+ In this example, a locale expression leading to a list of context
+ elements that is not well-defined is encountered, and it is illustrated
+ how normalisation deals with multiple inheritance.
+ Consider the specification of monads (in the algebraic sense)
+ and monoids.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{locale}\ monad\ {\isacharequal}\isanewline
+\ \ \isakeyword{fixes}\ prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymcdot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequote}{\isasymone}{\isachardoublequote}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ l{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymcdot}\ x\ {\isacharequal}\ x{\isachardoublequote}\ \isakeyword{and}\ r{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}x\ {\isasymcdot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Monoids are both semigroups and monads and one would want to
+ specify them as locale expression \isa{semi\ {\isacharplus}\ monad}.
+ Unfortunately, this expression is not well-formed. Its normal form
+\begin{align*%
+}
+ \N(\isa{monad}) & = [\isa{monad\ prod}] \\
+ \N(\isa{semi}+\isa{monad}) & =
+ \N(\isa{semi}) \App \N(\isa{monad})
+ = [\isa{semi\ prod}, \isa{monad\ prod}]
+\end{align*%
+}
+ leads to a list containing the context element
+\[
+ \textbf{fixes}~\isa{prod} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}}
+ ~(\textbf{infixl}~\isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}}~70)
+\]
+ twice and thus violating the first criterion of well-formedness. To
+ avoid this problem, one can
+ introduce a new locale \isa{magma} with the sole purpose of fixing the
+ parameter and defining its syntax. The specifications of semigroup
+ and monad are changed so that they import \isa{magma}.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{locale}\ magma\ {\isacharequal}\ \isakeyword{fixes}\ prod\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymcdot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{locale}\ semi{\isacharprime}\ {\isacharequal}\ magma\ {\isacharplus}\ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymcdot}\ y{\isacharparenright}\ {\isasymcdot}\ z\ {\isacharequal}\ x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{locale}\ monad{\isacharprime}\ {\isacharequal}\ magma\ {\isacharplus}\ \isakeyword{fixes}\ one\ {\isacharparenleft}{\isachardoublequote}{\isasymone}{\isachardoublequote}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ l{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymcdot}\ x\ {\isacharequal}\ x{\isachardoublequote}\ \isakeyword{and}\ r{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}x\ {\isasymcdot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Normalisation now yields
+\begin{align*%
+}
+ \N(\isa{semi{\isacharprime}\ {\isacharplus}\ monad{\isacharprime}}) & =
+ \N(\isa{semi{\isacharprime}}) \App \N(\isa{monad{\isacharprime}}) \\
+ & = (\N(\isa{magma}) \App [\isa{semi{\isacharprime}\ prod}]) \App
+ (\N(\isa{magma}) \App [\isa{monad{\isacharprime}\ prod}]) \\
+ & = [\isa{magma\ prod}, \isa{semi{\isacharprime}\ prod}] \App
+ [\isa{magma\ prod}, \isa{monad{\isacharprime}\ prod}]) \\
+ & = [\isa{magma\ prod}, \isa{semi{\isacharprime}\ prod},
+ \isa{monad{\isacharprime}\ prod}]
+\end{align*%
+}
+ where the second occurrence of \isa{magma\ prod} is eliminated.
+ The reader is encouraged to check, using the \textbf{print\_locale}
+ command, that the list of context elements generated from this is
+ indeed well-formed.
+
+ It follows that importing
+ parameters is more flexible than fixing them using a context element.
+ The Locale package provides the predefined locale \isa{var} that
+ can be used to import parameters if no
+ particular mixfix syntax is required.
+ Its definition is
+\begin{center}
+ \textbf{locale} \isa{var} = \textbf{fixes} \isa{x{\isacharunderscore}}
+\end{center}
+ The use of the internal variable \isa{x{\isacharunderscore}}
+ enforces that the parameter is renamed before being used, because
+ internal variables may not occur in the input syntax. Using
+ \isa{var}, the locale \isa{magma} could have been replaced by
+ the locale expression
+\begin{center}
+ \isa{var} \isa{prod} (\textbf{infixl} \isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}} 70)
+\end{center}
+ in the above locale declarations.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Includes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec-includes}
+ The context element \textbf{includes} takes a locale expression $e$
+ as argument. It can only occur in long goals, where it
+ adds, like a target, locale context to the proof context. Unlike
+ with targets, the proved theorem is not stored
+ in the locale. Instead, it is exported immediately.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{theorem}\ lcomm{\isadigit{2}}{\isacharcolon}\isanewline
+\ \ \isakeyword{includes}\ comm{\isacharunderscore}semi\ \isakeyword{shows}\ {\isachardoublequote}x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}\ {\isacharequal}\ y\ {\isasymcdot}\ {\isacharparenleft}x\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharminus}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymcdot}\ y{\isacharparenright}\ {\isasymcdot}\ z{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymcdot}\ x{\isacharparenright}\ {\isasymcdot}\ z{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ comm{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ y\ {\isasymcdot}\ {\isacharparenleft}x\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This proof is identical to the proof of \isa{lcomm}. The use of
+ \textbf{includes} provides the same context and facts as when using
+ \isa{comm{\isacharunderscore}semi} as target. On the other hand, \isa{lcomm{\isadigit{2}}} is not added as a fact to the locale \isa{comm{\isacharunderscore}semi}, but
+ is directly visible in the theory. The theorem is
+\[
+ \isa{comm{\isacharunderscore}semi\ {\isacharquery}prod\ {\isasymLongrightarrow}\ {\isacharquery}prod\ {\isacharquery}x\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ {\isacharquery}prod\ {\isacharquery}y\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}}.
+\]
+ Note that it is possible to
+ combine a target and (several) \textbf{includes} in a goal statement, thus
+ using contexts of several locales but storing the theorem in only
+ one of them.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Structures%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec-structures}
+ The specifications of semigroups and monoids that served as examples
+ in previous sections modelled each operation of an algebraic
+ structure as a single parameter. This is rather inconvenient for
+ structures with many operations, and also unnatural. In accordance
+ to mathematical texts, one would rather fix two groups instead of
+ two sets of operations.
+
+ The approach taken in Isabelle is to encode algebraic structures
+ with suitable types (in Isabelle/HOL usually records). An issue to
+ be addressed by
+ locales is syntax for algebraic structures. This is the purpose of
+ the \textbf{(structure)} annotation in \textbf{fixes}, introduced by
+ Wenzel. We illustrate this, independently of record types, with a
+ different formalisation of semigroups.
+
+ Let \isa{{\isacharprime}a\ semi{\isacharunderscore}type} be a not further specified type that
+ represents semigroups over the carrier type \isa{{\isacharprime}a}. Let \isa{s{\isacharunderscore}op} be an operation that maps an object of \isa{{\isacharprime}a\ semi{\isacharunderscore}type} to
+ a binary operation.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{typedecl}\ {\isacharprime}a\ semi{\isacharunderscore}type\isanewline
+\isamarkupfalse%
+\isacommand{consts}\ s{\isacharunderscore}op\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a\ semi{\isacharunderscore}type{\isacharcomma}\ {\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymstar}{\isasymindex}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Although \isa{s{\isacharunderscore}op} is a ternary operation, it is declared
+ infix. The syntax annotation contains the token \isa{{\isasymindex}}
+ (\verb.\<index>.), which refers to the first argument. This syntax is only
+ effective in the context of a locale, and only if the first argument
+ is a
+ \emph{structural} parameter --- that is, a parameter with annotation
+ \textbf{(structure)}. The token has the effect of subscripting the
+ parameter --- by bracketing it between \verb.\<^bsub>. and \verb.\<^esub>..
+ Additionally, the subscript of the first structural parameter may be
+ omitted, as in this specification of semigroups with structures:%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{locale}\ comm{\isacharunderscore}semi{\isacharprime}\ {\isacharequal}\isanewline
+\ \ \isakeyword{fixes}\ G\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ semi{\isacharunderscore}type{\isachardoublequote}\ {\isacharparenleft}\isakeyword{structure}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymstar}\ y{\isacharparenright}\ {\isasymstar}\ z\ {\isacharequal}\ x\ {\isasymstar}\ {\isacharparenleft}y\ {\isasymstar}\ z{\isacharparenright}{\isachardoublequote}\ \isakeyword{and}\ comm{\isacharcolon}\ {\isachardoublequote}x\ {\isasymstar}\ y\ {\isacharequal}\ y\ {\isasymstar}\ x{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Here \isa{x\ {\isasymstar}\ y} is equivalent to \isa{x\ {\isasymstar}\isactrlbsub G\isactrlesub \ y} and
+ abbreviates \isa{s{\isacharunderscore}op\ G\ x\ y}. A specification of homomorphisms
+ requires a second structural parameter.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{locale}\ semi{\isacharprime}{\isacharunderscore}hom\ {\isacharequal}\ comm{\isacharunderscore}semi{\isacharprime}\ {\isacharplus}\ comm{\isacharunderscore}semi{\isacharprime}\ H\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ hom\isanewline
+\ \ \isakeyword{assumes}\ hom{\isacharcolon}\ {\isachardoublequote}hom\ {\isacharparenleft}x\ {\isasymstar}\ y{\isacharparenright}\ {\isacharequal}\ hom\ x\ {\isasymstar}\isactrlbsub H\isactrlesub \ hom\ y{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The parameter \isa{H} is defined in the second \textbf{fixes}
+ element of $\C(\isa{semi{\isacharprime}{\isacharunderscore}comm})$. Hence \isa{{\isasymstar}\isactrlbsub H\isactrlesub }
+ abbreviates \isa{s{\isacharunderscore}op\ H\ x\ y}. The same construction can be done
+ with records instead of an \textit{ad-hoc} type.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{record}\ {\isacharprime}a\ semi\ {\isacharequal}\ prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymbullet}{\isasymindex}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This declares the types \isa{{\isacharprime}a\ semi} and \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ semi{\isacharunderscore}scheme}. The latter is an extensible record, where the second
+ type argument is the type of the extension field. For details on
+ records, see \cite{NipkowEtAl2002} Chapter~8.3.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{locale}\ semi{\isacharunderscore}w{\isacharunderscore}records\ {\isacharequal}\ struct\ G\ {\isacharplus}\isanewline
+\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymbullet}\ y{\isacharparenright}\ {\isasymbullet}\ z\ {\isacharequal}\ x\ {\isasymbullet}\ {\isacharparenleft}y\ {\isasymbullet}\ z{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ semi{\isacharunderscore}scheme} is inferred for the parameter \isa{G}. Using subtyping on records, the specification can be extended
+ to groups easily.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{record}\ {\isacharprime}a\ group\ {\isacharequal}\ {\isachardoublequote}{\isacharprime}a\ semi{\isachardoublequote}\ {\isacharplus}\isanewline
+\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}{\isachardoublequote}l{\isasymindex}{\isachardoublequote}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}{\isachardoublequote}inv{\isasymindex}\ {\isacharunderscore}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{1}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isacommand{locale}\ group{\isacharunderscore}w{\isacharunderscore}records\ {\isacharequal}\ semi{\isacharunderscore}w{\isacharunderscore}records\ {\isacharplus}\isanewline
+\ \ \isakeyword{assumes}\ l{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}l\ {\isasymbullet}\ x\ {\isacharequal}\ x{\isachardoublequote}\ \isakeyword{and}\ l{\isacharunderscore}inv{\isacharcolon}\ {\isachardoublequote}inv\ x\ {\isasymbullet}\ x\ {\isacharequal}\ l{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Finally, the predefined locale
+\begin{center}
+ \textbf{locale} \textit{struct} = \textbf{fixes} \isa{S{\isacharunderscore}}
+ \textbf{(structure)}.
+\end{center}
+ is analogous to \isa{var}.
+ More examples on the use of structures, including groups, rings and
+ polynomials can be found in the Isabelle distribution in the
+ session HOL-Algebra.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Conclusions and Outlook%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Locales provide a simple means of modular reasoning. They enable to
+ abbreviate frequently occurring context statements and maintain facts
+ valid in these contexts. Importantly, using structures, they allow syntax to be
+ effective only in certain contexts, and thus to mimic common
+ practice in mathematics, where notation is chosen very flexibly.
+ This is also known as literate formalisation \cite{Bailey1998}.
+ Locale expressions allow to duplicate and merge
+ specifications. This is a necessity, for example, when reasoning about
+ homomorphisms. Normalisation makes it possible to deal with
+ diamond-shaped inheritance structures, and generally with directed
+ acyclic graphs. The combination of locales with record
+ types in higher-order logic provides an effective means for
+ specifying algebraic structures: locale import and record subtyping
+ provide independent hierarchies for specifications and structure
+ elements. Rich examples for this can be found in
+ the Isabelle distribution in the session HOL-Algebra.
+
+ The primary reason for writing this report was to provide a better
+ understanding of locales in Isar. Wenzel provided hardly any
+ documentation, with the exception of \cite{Wenzel2002b}. The
+ present report should make it easier for users of Isabelle to take
+ advantage of locales.
+
+ The report is also a base for future extensions. These include
+ improved syntax for structures. Identifying them by numbers seems
+ unnatural and can be confusing if more than two structures are
+ involved --- for example, when reasoning about universal
+ properties --- and numbering them by order of occurrence seems
+ arbitrary. Another desirable feature is \emph{instantiation}. One
+ may, in the course of a theory development, construct objects that
+ fulfil the specification of a locale. These objects are possibly
+ defined in the context of another locale. Instantiation should make it
+ simple to specialise abstract facts for the object under
+ consideration and to use the specified facts.
+
+ A detailed comparison of locales with module systems in type theory
+ has not been undertaken yet, but could be beneficial. For example,
+ a module system for Coq has recently been presented by Chrzaszcz
+ \cite{Chrzaszcz2003,Chrzaszcz2004}. While the
+ latter usually constitute extensions of the calculus, locales are
+ a rather thin layer that does not change Isabelle's meta logic.
+ Locales mainly manage specifications and facts. Functors, like
+ the constructor for polynomial rings, remain objects of the
+ logic.
+
+ \textbf{Acknowledgements.} Lawrence C.\ Paulson and Norbert
+ Schirmer made useful comments on a draft of this paper.%
+\end{isamarkuptext}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Locales/Locales/document/isabelle.sty Fri Aug 19 22:50:20 2005 +0200
@@ -0,0 +1,191 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%%
+%% macros for Isabelle generated LaTeX output
+%%
+%% $Id$
+
+%%% Simple document preparation (based on theory token language and symbols)
+
+% isabelle environments
+
+\newcommand{\isabellecontext}{UNKNOWN}
+
+\newcommand{\isastyle}{\small\tt\slshape}
+\newcommand{\isastyleminor}{\small\tt\slshape}
+\newcommand{\isastylescript}{\footnotesize\tt\slshape}
+\newcommand{\isastyletext}{\normalsize\rm}
+\newcommand{\isastyletxt}{\rm}
+\newcommand{\isastylecmt}{\rm}
+
+%symbol markup -- \emph achieves decent spacing via italic corrections
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isatext}[1]{\emph{#1}}
+\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
+\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
+\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
+\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
+\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
+
+
+\newdimen\isa@parindent\newdimen\isa@parskip
+
+\newenvironment{isabellebody}{%
+\isamarkuptrue\par%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isastyle}{\par}
+
+\newenvironment{isabelle}
+{\begin{trivlist}\begin{isabellebody}\item\relax}
+{\end{isabellebody}\end{trivlist}}
+
+\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
+
+\newcommand{\isaindent}[1]{\hphantom{#1}}
+\newcommand{\isanewline}{\mbox{}\par\mbox{}}
+\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
+\newcommand{\isadigit}[1]{#1}
+
+\chardef\isacharbang=`\!
+\chardef\isachardoublequote=`\"
+\chardef\isacharhash=`\#
+\chardef\isachardollar=`\$
+\chardef\isacharpercent=`\%
+\chardef\isacharampersand=`\&
+\chardef\isacharprime=`\'
+\chardef\isacharparenleft=`\(
+\chardef\isacharparenright=`\)
+\chardef\isacharasterisk=`\*
+\chardef\isacharplus=`\+
+\chardef\isacharcomma=`\,
+\chardef\isacharminus=`\-
+\chardef\isachardot=`\.
+\chardef\isacharslash=`\/
+\chardef\isacharcolon=`\:
+\chardef\isacharsemicolon=`\;
+\chardef\isacharless=`\<
+\chardef\isacharequal=`\=
+\chardef\isachargreater=`\>
+\chardef\isacharquery=`\?
+\chardef\isacharat=`\@
+\chardef\isacharbrackleft=`\[
+\chardef\isacharbackslash=`\\
+\chardef\isacharbrackright=`\]
+\chardef\isacharcircum=`\^
+\chardef\isacharunderscore=`\_
+\chardef\isacharbackquote=`\`
+\chardef\isacharbraceleft=`\{
+\chardef\isacharbar=`\|
+\chardef\isacharbraceright=`\}
+\chardef\isachartilde=`\~
+
+
+% keyword and section markup
+
+\newcommand{\isakeywordcharunderscore}{\_}
+\newcommand{\isakeyword}[1]
+{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
+\newcommand{\isacommand}[1]{\isakeyword{#1}}
+
+\newcommand{\isamarkupheader}[1]{\section{#1}}
+\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
+\newcommand{\isamarkupsection}[1]{\section{#1}}
+\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkupsect}[1]{\section{#1}}
+\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
+
+\newif\ifisamarkup
+\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
+\newcommand{\isaendpar}{\par\medskip}
+\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
+\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+
+
+% alternative styles
+
+\newcommand{\isabellestyle}{}
+\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
+
+\newcommand{\isabellestylett}{%
+\renewcommand{\isastyle}{\small\tt}%
+\renewcommand{\isastyleminor}{\small\tt}%
+\renewcommand{\isastylescript}{\footnotesize\tt}%
+}
+\newcommand{\isabellestyleit}{%
+\renewcommand{\isastyle}{\small\it}%
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastylescript}{\footnotesize\it}%
+\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
+\renewcommand{\isacharbang}{\isamath{!}}%
+\renewcommand{\isachardoublequote}{}%
+\renewcommand{\isacharhash}{\isamath{\#}}%
+\renewcommand{\isachardollar}{\isamath{\$}}%
+\renewcommand{\isacharpercent}{\isamath{\%}}%
+\renewcommand{\isacharampersand}{\isamath{\&}}%
+\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
+\renewcommand{\isacharparenleft}{\isamath{(}}%
+\renewcommand{\isacharparenright}{\isamath{)}}%
+\renewcommand{\isacharasterisk}{\isamath{*}}%
+\renewcommand{\isacharplus}{\isamath{+}}%
+\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
+\renewcommand{\isacharminus}{\isamath{-}}%
+\renewcommand{\isachardot}{\isamath{\mathord.}}%
+\renewcommand{\isacharslash}{\isamath{/}}%
+\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
+\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
+\renewcommand{\isacharless}{\isamath{<}}%
+\renewcommand{\isacharequal}{\isamath{=}}%
+\renewcommand{\isachargreater}{\isamath{>}}%
+\renewcommand{\isacharat}{\isamath{@}}%
+\renewcommand{\isacharbrackleft}{\isamath{[}}%
+\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
+\renewcommand{\isacharbrackright}{\isamath{]}}%
+\renewcommand{\isacharunderscore}{\mbox{-}}%
+\renewcommand{\isacharbraceleft}{\isamath{\{}}%
+\renewcommand{\isacharbar}{\isamath{\mid}}%
+\renewcommand{\isacharbraceright}{\isamath{\}}}%
+\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
+}
+
+\newcommand{\isabellestylesl}{%
+\isabellestyleit%
+\renewcommand{\isastyle}{\small\sl}%
+\renewcommand{\isastyleminor}{\sl}%
+\renewcommand{\isastylescript}{\footnotesize\sl}%
+}
+
+
+% tagged regions
+
+%plain TeX version of comment package -- much faster!
+\let\isafmtname\fmtname\def\fmtname{plain}
+\usepackage{comment}
+\let\fmtname\isafmtname
+
+\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
+
+\newcommand{\isakeeptag}[1]%
+{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isadroptag}[1]%
+{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isafoldtag}[1]%
+{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
+
+\isakeeptag{theory}
+\isakeeptag{proof}
+\isakeeptag{ML}
+\isakeeptag{visible}
+\isadroptag{invisible}
+
+\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Locales/Locales/document/isabellesym.sty Fri Aug 19 22:50:20 2005 +0200
@@ -0,0 +1,362 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%%
+%% definitions of standard Isabelle symbols
+%%
+%% $Id$
+
+% symbol definitions
+
+\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
+\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
+\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
+\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
+\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
+\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
+\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
+\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
+\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
+\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
+\newcommand{\isasymA}{\isamath{\mathcal{A}}}
+\newcommand{\isasymB}{\isamath{\mathcal{B}}}
+\newcommand{\isasymC}{\isamath{\mathcal{C}}}
+\newcommand{\isasymD}{\isamath{\mathcal{D}}}
+\newcommand{\isasymE}{\isamath{\mathcal{E}}}
+\newcommand{\isasymF}{\isamath{\mathcal{F}}}
+\newcommand{\isasymG}{\isamath{\mathcal{G}}}
+\newcommand{\isasymH}{\isamath{\mathcal{H}}}
+\newcommand{\isasymI}{\isamath{\mathcal{I}}}
+\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
+\newcommand{\isasymK}{\isamath{\mathcal{K}}}
+\newcommand{\isasymL}{\isamath{\mathcal{L}}}
+\newcommand{\isasymM}{\isamath{\mathcal{M}}}
+\newcommand{\isasymN}{\isamath{\mathcal{N}}}
+\newcommand{\isasymO}{\isamath{\mathcal{O}}}
+\newcommand{\isasymP}{\isamath{\mathcal{P}}}
+\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
+\newcommand{\isasymR}{\isamath{\mathcal{R}}}
+\newcommand{\isasymS}{\isamath{\mathcal{S}}}
+\newcommand{\isasymT}{\isamath{\mathcal{T}}}
+\newcommand{\isasymU}{\isamath{\mathcal{U}}}
+\newcommand{\isasymV}{\isamath{\mathcal{V}}}
+\newcommand{\isasymW}{\isamath{\mathcal{W}}}
+\newcommand{\isasymX}{\isamath{\mathcal{X}}}
+\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
+\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
+\newcommand{\isasyma}{\isamath{\mathrm{a}}}
+\newcommand{\isasymb}{\isamath{\mathrm{b}}}
+\newcommand{\isasymc}{\isamath{\mathrm{c}}}
+\newcommand{\isasymd}{\isamath{\mathrm{d}}}
+\newcommand{\isasyme}{\isamath{\mathrm{e}}}
+\newcommand{\isasymf}{\isamath{\mathrm{f}}}
+\newcommand{\isasymg}{\isamath{\mathrm{g}}}
+\newcommand{\isasymh}{\isamath{\mathrm{h}}}
+\newcommand{\isasymi}{\isamath{\mathrm{i}}}
+\newcommand{\isasymj}{\isamath{\mathrm{j}}}
+\newcommand{\isasymk}{\isamath{\mathrm{k}}}
+\newcommand{\isasyml}{\isamath{\mathrm{l}}}
+\newcommand{\isasymm}{\isamath{\mathrm{m}}}
+\newcommand{\isasymn}{\isamath{\mathrm{n}}}
+\newcommand{\isasymo}{\isamath{\mathrm{o}}}
+\newcommand{\isasymp}{\isamath{\mathrm{p}}}
+\newcommand{\isasymq}{\isamath{\mathrm{q}}}
+\newcommand{\isasymr}{\isamath{\mathrm{r}}}
+\newcommand{\isasyms}{\isamath{\mathrm{s}}}
+\newcommand{\isasymt}{\isamath{\mathrm{t}}}
+\newcommand{\isasymu}{\isamath{\mathrm{u}}}
+\newcommand{\isasymv}{\isamath{\mathrm{v}}}
+\newcommand{\isasymw}{\isamath{\mathrm{w}}}
+\newcommand{\isasymx}{\isamath{\mathrm{x}}}
+\newcommand{\isasymy}{\isamath{\mathrm{y}}}
+\newcommand{\isasymz}{\isamath{\mathrm{z}}}
+\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
+\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
+\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
+\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
+\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
+\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
+\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
+\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
+\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
+\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
+\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
+\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
+\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
+\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
+\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
+\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
+\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
+\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
+\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
+\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
+\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
+\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
+\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
+\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
+\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
+\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
+\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
+\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
+\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
+\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
+\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
+\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
+\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
+\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
+\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
+\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
+\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
+\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
+\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
+\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
+\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
+\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
+\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
+\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
+\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
+\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
+\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
+\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
+\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
+\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
+\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
+\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
+\newcommand{\isasymalpha}{\isamath{\alpha}}
+\newcommand{\isasymbeta}{\isamath{\beta}}
+\newcommand{\isasymgamma}{\isamath{\gamma}}
+\newcommand{\isasymdelta}{\isamath{\delta}}
+\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
+\newcommand{\isasymzeta}{\isamath{\zeta}}
+\newcommand{\isasymeta}{\isamath{\eta}}
+\newcommand{\isasymtheta}{\isamath{\vartheta}}
+\newcommand{\isasymiota}{\isamath{\iota}}
+\newcommand{\isasymkappa}{\isamath{\kappa}}
+\newcommand{\isasymlambda}{\isamath{\lambda}}
+\newcommand{\isasymmu}{\isamath{\mu}}
+\newcommand{\isasymnu}{\isamath{\nu}}
+\newcommand{\isasymxi}{\isamath{\xi}}
+\newcommand{\isasympi}{\isamath{\pi}}
+\newcommand{\isasymrho}{\isamath{\varrho}}
+\newcommand{\isasymsigma}{\isamath{\sigma}}
+\newcommand{\isasymtau}{\isamath{\tau}}
+\newcommand{\isasymupsilon}{\isamath{\upsilon}}
+\newcommand{\isasymphi}{\isamath{\varphi}}
+\newcommand{\isasymchi}{\isamath{\chi}}
+\newcommand{\isasympsi}{\isamath{\psi}}
+\newcommand{\isasymomega}{\isamath{\omega}}
+\newcommand{\isasymGamma}{\isamath{\Gamma}}
+\newcommand{\isasymDelta}{\isamath{\Delta}}
+\newcommand{\isasymTheta}{\isamath{\Theta}}
+\newcommand{\isasymLambda}{\isamath{\Lambda}}
+\newcommand{\isasymXi}{\isamath{\Xi}}
+\newcommand{\isasymPi}{\isamath{\Pi}}
+\newcommand{\isasymSigma}{\isamath{\Sigma}}
+\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
+\newcommand{\isasymPhi}{\isamath{\Phi}}
+\newcommand{\isasymPsi}{\isamath{\Psi}}
+\newcommand{\isasymOmega}{\isamath{\Omega}}
+\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
+\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
+\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
+\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
+\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
+\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
+\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
+\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
+\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
+\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
+\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
+\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
+\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
+\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
+\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
+\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
+\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
+\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
+\newcommand{\isasymmapsto}{\isamath{\mapsto}}
+\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
+\newcommand{\isasymmidarrow}{\isamath{\relbar}}
+\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
+\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
+\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
+\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
+\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
+\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
+\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
+\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
+\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
+\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
+\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
+\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
+\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
+\newcommand{\isasymup}{\isamath{\uparrow}}
+\newcommand{\isasymUp}{\isamath{\Uparrow}}
+\newcommand{\isasymdown}{\isamath{\downarrow}}
+\newcommand{\isasymDown}{\isamath{\Downarrow}}
+\newcommand{\isasymupdown}{\isamath{\updownarrow}}
+\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
+\newcommand{\isasymlangle}{\isamath{\langle}}
+\newcommand{\isasymrangle}{\isamath{\rangle}}
+\newcommand{\isasymlceil}{\isamath{\lceil}}
+\newcommand{\isasymrceil}{\isamath{\rceil}}
+\newcommand{\isasymlfloor}{\isamath{\lfloor}}
+\newcommand{\isasymrfloor}{\isamath{\rfloor}}
+\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
+\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
+\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
+\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
+\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
+\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
+\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
+\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
+\newcommand{\isasymnot}{\isamath{\neg}}
+\newcommand{\isasymbottom}{\isamath{\bot}}
+\newcommand{\isasymtop}{\isamath{\top}}
+\newcommand{\isasymand}{\isamath{\wedge}}
+\newcommand{\isasymAnd}{\isamath{\bigwedge}}
+\newcommand{\isasymor}{\isamath{\vee}}
+\newcommand{\isasymOr}{\isamath{\bigvee}}
+\newcommand{\isasymforall}{\isamath{\forall\,}}
+\newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
+\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
+\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
+\newcommand{\isasymturnstile}{\isamath{\vdash}}
+\newcommand{\isasymTurnstile}{\isamath{\models}}
+\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
+\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
+\newcommand{\isasymstileturn}{\isamath{\dashv}}
+\newcommand{\isasymsurd}{\isamath{\surd}}
+\newcommand{\isasymle}{\isamath{\le}}
+\newcommand{\isasymge}{\isamath{\ge}}
+\newcommand{\isasymlless}{\isamath{\ll}}
+\newcommand{\isasymggreater}{\isamath{\gg}}
+\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
+\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
+\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
+\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
+\newcommand{\isasymin}{\isamath{\in}}
+\newcommand{\isasymnotin}{\isamath{\notin}}
+\newcommand{\isasymsubset}{\isamath{\subset}}
+\newcommand{\isasymsupset}{\isamath{\supset}}
+\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
+\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
+\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
+\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
+\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
+\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
+\newcommand{\isasyminter}{\isamath{\cap}}
+\newcommand{\isasymInter}{\isamath{\bigcap\,}}
+\newcommand{\isasymunion}{\isamath{\cup}}
+\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
+\newcommand{\isasymsqunion}{\isamath{\sqcup}}
+\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
+\newcommand{\isasymsqinter}{\isamath{\sqcap}}
+\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
+\newcommand{\isasymuplus}{\isamath{\uplus}}
+\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
+\newcommand{\isasymnoteq}{\isamath{\not=}}
+\newcommand{\isasymsim}{\isamath{\sim}}
+\newcommand{\isasymdoteq}{\isamath{\doteq}}
+\newcommand{\isasymsimeq}{\isamath{\simeq}}
+\newcommand{\isasymapprox}{\isamath{\approx}}
+\newcommand{\isasymasymp}{\isamath{\asymp}}
+\newcommand{\isasymcong}{\isamath{\cong}}
+\newcommand{\isasymsmile}{\isamath{\smile}}
+\newcommand{\isasymequiv}{\isamath{\equiv}}
+\newcommand{\isasymfrown}{\isamath{\frown}}
+\newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
+\newcommand{\isasymbowtie}{\isamath{\bowtie}}
+\newcommand{\isasymprec}{\isamath{\prec}}
+\newcommand{\isasymsucc}{\isamath{\succ}}
+\newcommand{\isasympreceq}{\isamath{\preceq}}
+\newcommand{\isasymsucceq}{\isamath{\succeq}}
+\newcommand{\isasymparallel}{\isamath{\parallel}}
+\newcommand{\isasymbar}{\isamath{\mid}}
+\newcommand{\isasymplusminus}{\isamath{\pm}}
+\newcommand{\isasymminusplus}{\isamath{\mp}}
+\newcommand{\isasymtimes}{\isamath{\times}}
+\newcommand{\isasymdiv}{\isamath{\div}}
+\newcommand{\isasymcdot}{\isamath{\cdot}}
+\newcommand{\isasymstar}{\isamath{\star}}
+\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
+\newcommand{\isasymcirc}{\isamath{\circ}}
+\newcommand{\isasymdagger}{\isamath{\dagger}}
+\newcommand{\isasymddagger}{\isamath{\ddagger}}
+\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
+\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
+\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
+\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
+\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
+\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
+\newcommand{\isasymtriangle}{\isamath{\triangle}}
+\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
+\newcommand{\isasymoplus}{\isamath{\oplus}}
+\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
+\newcommand{\isasymotimes}{\isamath{\otimes}}
+\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
+\newcommand{\isasymodot}{\isamath{\odot}}
+\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
+\newcommand{\isasymominus}{\isamath{\ominus}}
+\newcommand{\isasymoslash}{\isamath{\oslash}}
+\newcommand{\isasymdots}{\isamath{\dots}}
+\newcommand{\isasymcdots}{\isamath{\cdots}}
+\newcommand{\isasymSum}{\isamath{\sum\,}}
+\newcommand{\isasymProd}{\isamath{\prod\,}}
+\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
+\newcommand{\isasyminfinity}{\isamath{\infty}}
+\newcommand{\isasymintegral}{\isamath{\int\,}}
+\newcommand{\isasymointegral}{\isamath{\oint\,}}
+\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
+\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
+\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
+\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
+\newcommand{\isasymaleph}{\isamath{\aleph}}
+\newcommand{\isasymemptyset}{\isamath{\emptyset}}
+\newcommand{\isasymnabla}{\isamath{\nabla}}
+\newcommand{\isasympartial}{\isamath{\partial}}
+\newcommand{\isasymRe}{\isamath{\Re}}
+\newcommand{\isasymIm}{\isamath{\Im}}
+\newcommand{\isasymflat}{\isamath{\flat}}
+\newcommand{\isasymnatural}{\isamath{\natural}}
+\newcommand{\isasymsharp}{\isamath{\sharp}}
+\newcommand{\isasymangle}{\isamath{\angle}}
+\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
+\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
+\newcommand{\isasymhyphen}{\isatext{\rm-}}
+\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
+\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
+\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
+\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
+\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
+\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
+\newcommand{\isasymsection}{\isatext{\rm\S}}
+\newcommand{\isasymparagraph}{\isatext{\rm\P}}
+\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
+\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
+\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
+\newcommand{\isasympounds}{\isamath{\pounds}}
+\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
+\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
+\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
+\newcommand{\isasymamalg}{\isamath{\amalg}}
+\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
+\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
+\newcommand{\isasymwp}{\isamath{\wp}}
+\newcommand{\isasymwrong}{\isamath{\wr}}
+\newcommand{\isasymstruct}{\isamath{\diamond}}
+\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymindex}{\isatext{\i}}
+\newcommand{\isasymdieresis}{\isatext{\"\relax}}
+\newcommand{\isasymcedilla}{\isatext{\c\relax}}
+\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+\newcommand{\isasymspacespace}{\isamath{~~}}
+\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Locales/Locales/document/pdfsetup.sty Fri Aug 19 22:50:20 2005 +0200
@@ -0,0 +1,12 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%%
+%% smart url or hyperref setup
+%%
+%% $Id$
+
+\@ifundefined{pdfoutput}
+{\usepackage{url}}
+{\usepackage{color}\definecolor{darkblue}{rgb}{0,0,0.5}
+ \usepackage[pdftex,a4paper,colorlinks=true,linkcolor=darkblue,citecolor=darkblue,filecolor=darkblue,pagecolor=darkblue,urlcolor=darkblue]{hyperref}
+ \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Locales/Locales/document/session.tex Fri Aug 19 22:50:20 2005 +0200
@@ -0,0 +1,6 @@
+\input{Locales.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/Locales/Locales/generated/Locales.tex Fri Aug 19 22:44:36 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1221 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Locales}%
-\isanewline
-\isamarkupfalse%
-\isamarkupfalse%
-%
-\isamarkupsection{Overview%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Locales are an extension of the Isabelle proof assistant. They
- provide support for modular reasoning. Locales were initially
- developed by Kamm\"uller~\cite{Kammuller2000} to support reasoning
- in abstract algebra, but are applied also in other domains --- for
- example, bytecode verification~\cite{Klein2003}.
-
- Kamm\"uller's original design, implemented in Isabelle99, provides, in
- addition to
- means for declaring locales, a set of ML functions that were used
- along with ML tactics in a proof. In the meantime, the input format
- for proof in Isabelle has changed and users write proof
- scripts in ML only rarely if at all. Two new proof styles are
- available, and can
- be used interchangeably: linear proof scripts that closely resemble ML
- tactics, and the structured Isar proof language by
- Wenzel~\cite{Wenzel2002a}. Subsequently, Wenzel re-implemented
- locales for
- the new proof format. The implementation, available with
- Isabelle2003, constitutes a complete re-design and exploits that
- both Isar and locales are based on the notion of context,
- and thus locales are seen as a natural extension of Isar.
- Nevertheless, locales can also be used with proof scripts:
- their use does not require a deep understanding of the structured
- Isar proof style.
-
- At the same time, Wenzel considerably extended locales. The most
- important addition are locale expressions, which allow to combine
- locales more freely. Previously only
- linear inheritance was possible. Now locales support multiple
- inheritance through a normalisation algorithm. New are also
- structures, which provide special syntax for locale parameters that
- represent algebraic structures.
-
- Unfortunately, Wenzel provided only an implementation but hardly any
- documentation. Besides providing documentation, the present paper
- is a high-level description of locales, and in particular locale
- expressions. It is meant as a first step towards the semantics of
- locales, and also as a base for comparing locales with module concepts
- in other provers. It also constitutes the base for future
- extensions of locales in Isabelle.
- The description was derived mainly by experimenting
- with locales and partially also by inspecting the code.
-
- The main contribution of the author of the present paper is the
- abstract description of Wenzel's version of locales, and in
- particular of the normalisation algorithm for locale expressions (see
- Section~\ref{sec-normal-forms}). Contributions to the
- implementation are confined to bug fixes and to provisions that
- enable the use of locales with linear proof scripts.
-
- Concepts are introduced along with examples, so that the text can be
- used as tutorial. It is assumed that the reader is somewhat
- familiar with Isabelle proof scripts. Examples have been phrased as
- structured
- Isar proofs. However, in order to understand the key concepts,
- including locales expressions and their normalisation, detailed
- knowledge of Isabelle is not necessary.
-
-\nocite{Nipkow2003,Wenzel2002b,Wenzel2003}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Locales: Beyond Proof Contexts%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In tactic-based provers the application of a sequence of proof
- tactics leads to a proof state. This state is usually hard to
- predict from looking at the tactic script, unless one replays the
- proof step-by-step. The structured proof language Isar is
- different. It is additionally based on \emph{proof contexts},
- which are directly visible in Isar scripts, and since tactic
- sequences tend to be short, this commonly leads to clearer proof
- scripts.
-
- Goals are stated with the \textbf{theorem}
- command. This is followed by a proof. When discharging a goal
- requires an elaborate argument
- (rather than the application of a single tactic) a new context
- may be entered (\textbf{proof}). Inside the context, variables may
- be fixed (\textbf{fix}), assumptions made (\textbf{assume}) and
- intermediate goals stated (\textbf{have}) and proved. The
- assumptions must be dischargeable by premises of the surrounding
- goal, and once this goal has been proved (\textbf{show}) the proof context
- can be closed (\textbf{qed}). Contexts inherit from surrounding
- contexts, but it is not possible
- to export from them (with exception of the proved goal);
- they ``disappear'' after the closing \textbf{qed}.
- Facts may have attributes --- for example, identifying them as
- default to the simplifier or classical reasoner.
-
- Locales extend proof contexts in various ways:
- \begin{itemize}
- \item
- Locales are usually \emph{named}. This makes them persistent.
- \item
- Fixed variables may have \emph{syntax}.
- \item
- It is possible to \emph{add} and \emph{export} facts.
- \item
- Locales can be combined and modified with \emph{locale
- expressions}.
- \end{itemize}
- The Locales facility extends the Isar language: it provides new ways
- of stating and managing facts, but it does not modify the language
- for proofs. Its purpose is to support writing modular proofs.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Simple Locales%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Syntax and Terminology%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The grammar of Isar is extended by commands for locales as shown in
- Figure~\ref{fig-grammar}.
- A key concept, introduced by Wenzel, is that
- locales are (internally) lists
- of \emph{context elements}. There are four kinds, identified
- by the keywords \textbf{fixes}, \textbf{assumes}, \textbf{defines} and
- \textbf{notes}.
-
- \begin{figure}
- \hrule
- \vspace{2ex}
- \begin{small}
- \begin{tabular}{l>$c<$l}
- \textit{attr-name} & ::=
- & \textit{name} $|$ \textit{attribute} $|$
- \textit{name} \textit{attribute} \\
-
- \textit{locale-expr} & ::=
- & \textit{locale-expr1} ( ``\textbf{+}'' \textit{locale-expr1} )$^*$ \\
- \textit{locale-expr1} & ::=
- & ( \textit{qualified-name} $|$
- ``\textbf{(}'' \textit{locale-expr} ``\textbf{)}'' )
- ( \textit{name} $|$ ``\textbf{\_}'' )$^*$ \\
-
- \textit{fixes} & ::=
- & \textit{name} [ ``\textbf{::}'' \textit{type} ]
- [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
- \textit{mixfix} ] \\
- \textit{assumes} & ::=
- & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
- \textit{defines} & ::=
- & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
- \textit{notes} & ::=
- & [ \textit{attr-name} ``\textbf{=}'' ]
- ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
-
- \textit{element} & ::=
- & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
- & |
- & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\
- & |
- & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
- & |
- & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
- & | & \textbf{includes} \textit{locale-expr} \\
-
- \textit{locale} & ::=
- & \textit{element}$^+$ \\
- & | & \textit{locale-expr} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
-
- \textit{in-target} & ::=
- & ``\textbf{(}'' \textbf{in} \textit{qualified-name} ``\textbf{)}'' \\
-
- \textit{theorem} & ::= & ( \textbf{theorem} $|$ \textbf{lemma} $|$
- \textbf{corollary} ) [ \textit{in-target} ] [ \textit{attr-name} ] \\
-
- \textit{theory-level} & ::= & \ldots \\
- & | & \textbf{locale} \textit{name} [ ``\textbf{=}''
- \textit{locale} ] \\
- % note: legacy "locale (open)" omitted.
- & | & ( \textbf{theorems} $|$ \textbf{lemmas} ) \\
- & & [ \textit{in-target} ] [ \textit{attr-name} ``\textbf{=}'' ]
- ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
- & | & \textbf{declare} [ \textit{in-target} ] ( \textit{qualified-name}
- [ \textit{attribute} ] )$^+$ \\
- & | & \textit{theorem} \textit{proposition} \textit{proof} \\
- & | & \textit{theorem} \textit{element}$^*$
- \textbf{shows} \textit{proposition} \textit{proof} \\
- & | & \textbf{print\_locale} \textit{locale} \\
- & | & \textbf{print\_locales}
- \end{tabular}
- \end{small}
- \vspace{2ex}
- \hrule
- \caption{Locales extend the grammar of Isar.}
- \label{fig-grammar}
- \end{figure}
-
- At the theory level --- that is, at the outer syntactic level of an
- Isabelle input file --- \textbf{locale} declares a named
- locale. Other kinds of locales,
- locale expressions and unnamed locales, will be introduced later. When
- declaring a named locale, it is possible to \emph{import} another
- named locale, or indeed several ones by importing a locale
- expression. The second part of the declaration, also optional,
- consists of a number of context element declarations. Here, a fifth
- kind, \textbf{includes}, is available.
-
- A number of Isar commands have an additional, optional \emph{target}
- argument, which always refers to a named locale. These commands
- are \textbf{theorem} (together with \textbf{lemma} and
- \textbf{corollary}), \textbf{theorems} (and
- \textbf{lemmas}), and \textbf{declare}. The effect of specifying a target is
- that these commands focus on the specified locale, not the
- surrounding theory. Commands that are used to
- prove new theorems will add them not to the theory, but to the
- locale. Similarly, \textbf{declare} modifies attributes of theorems
- that belong to the specified target. Additionally, for
- \textbf{theorem} (and related commands), theorems stored in the target
- can be used in the associated proof scripts.
-
- The Locales package permits a \emph{long goals format} for
- propositions stated with \textbf{theorem} (and friends). While
- normally a goal is just a formula, a long goal is a list of context
- elements, followed by the keyword \textbf{shows}, followed by the
- formula. Roughly speaking, the context elements are
- (additional) premises. For an example, see
- Section~\ref{sec-includes}. The list of context elements in a long goal
- is also called \emph{unnamed locale}.
-
- Finally, there are two commands to inspect locales when working in
- interactive mode: \textbf{print\_locales} prints the names of all
- targets
- visible in the current theory, \textbf{print\_locale} outputs the
- elements of a named locale or locale expression.
-
- The following presentation will use notation of
- Isabelle's meta logic, hence a few sentences to explain this.
- The logical
- primitives are universal quantification (\isa{{\isasymAnd}}), entailment
- (\isa{{\isasymLongrightarrow}}) and equality (\isa{{\isasymequiv}}). Variables (not bound
- variables) are sometimes preceded by a question mark. The logic is
- typed. Type variables are denoted by \isa{{\isacharprime}a}, \isa{{\isacharprime}b}
- etc., and \isa{{\isasymRightarrow}} is the function type. Double brackets \isa{{\isasymlbrakk}} and \isa{{\isasymrbrakk}} are used to abbreviate nested entailment.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Parameters, Assumptions and Facts%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-From a logical point of view a \emph{context} is a formula schema of
- the form
-\[
- \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}{\isasymdots}x\isactrlsub n{\isachardot}\ {\isasymlbrakk}\ C\isactrlsub {\isadigit{1}}{\isacharsemicolon}\ {\isasymdots}\ {\isacharsemicolon}C\isactrlsub m\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymdots}}
-\]
- The variables $\isa{x\isactrlsub {\isadigit{1}}}, \ldots, \isa{x\isactrlsub n}$ are
- called \emph{parameters}, the premises $\isa{C\isactrlsub {\isadigit{1}}}, \ldots,
- \isa{C\isactrlsub n}$ \emph{assumptions}. A formula \isa{F}
- holds in this context if
-\begin{equation}
-\label{eq-fact-in-context}
- \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}{\isasymdots}x\isactrlsub n{\isachardot}\ {\isasymlbrakk}\ C\isactrlsub {\isadigit{1}}{\isacharsemicolon}\ {\isasymdots}\ {\isacharsemicolon}C\isactrlsub m\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ F}
-\end{equation}
- is valid. The formula is called a \emph{fact} of the context.
-
- A locale allows fixing the parameters \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n} and making the assumptions \isa{C\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ C\isactrlsub m}. This implicitly builds the context in
- which the formula \isa{F} can be established.
- Parameters of a locale correspond to the context element
- \textbf{fixes}, and assumptions may be declared with
- \textbf{assumes}. Using these context elements one can define
- the specification of semigroups.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{locale}\ semi\ {\isacharequal}\isanewline
-\ \ \isakeyword{fixes}\ prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymcdot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymcdot}\ y{\isacharparenright}\ {\isasymcdot}\ z\ {\isacharequal}\ x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-The parameter \isa{prod} has a
- syntax annotation allowing the infix ``\isa{{\isasymcdot}}'' in the
- assumption of associativity. Parameters may have arbitrary mixfix
- syntax, like constants. In the example, the type of \isa{prod} is
- specified explicitly. This is not necessary. If no type is
- specified, a most general type is inferred simultaneously for all
- parameters, taking into account all assumptions (and type
- specifications of parameters, if present).%
-\footnote{Type inference also takes into account definitions and
- import, as introduced later.}
-
- Free variables in assumptions are implicitly universally quantified,
- unless they are parameters. Hence the context defined by the locale
- \isa{semi} is
-\[
- \isa{{\isasymAnd}prod{\isachardot}\ {\isasymlbrakk}\ {\isasymAnd}x\ y\ z{\isachardot}\ prod\ {\isacharparenleft}prod\ x\ y{\isacharparenright}\ z\ {\isacharequal}\ prod\ x\ {\isacharparenleft}prod\ y\ z{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymdots}}
-\]
- The locale can be extended to commutative semigroups.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{locale}\ comm{\isacharunderscore}semi\ {\isacharequal}\ semi\ {\isacharplus}\isanewline
-\ \ \isakeyword{assumes}\ comm{\isacharcolon}\ {\isachardoublequote}x\ {\isasymcdot}\ y\ {\isacharequal}\ y\ {\isasymcdot}\ x{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-This locale \emph{imports} all elements of \isa{semi}. The
- latter locale is called the import of \isa{comm{\isacharunderscore}semi}. The
- definition adds commutativity, hence its context is
-\begin{align*%
-}
- \isa{{\isasymAnd}prod{\isachardot}\ {\isasymlbrakk}} &
- \isa{{\isasymAnd}x\ y\ z{\isachardot}\ prod\ {\isacharparenleft}prod\ x\ y{\isacharparenright}\ z\ {\isacharequal}\ prod\ x\ {\isacharparenleft}prod\ y\ z{\isacharparenright}{\isacharsemicolon}} \\
- & \isa{{\isasymAnd}x\ y{\isachardot}\ prod\ x\ y\ {\isacharequal}\ prod\ y\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymdots}}
-\end{align*%
-}
- One may now derive facts --- for example, left-commutativity --- in
- the context of \isa{comm{\isacharunderscore}semi} by specifying this locale as
- target, and by referring to the names of the assumptions \isa{assoc} and \isa{comm} in the proof.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{theorem}\ {\isacharparenleft}\isakeyword{in}\ comm{\isacharunderscore}semi{\isacharparenright}\ lcomm{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}\ {\isacharequal}\ y\ {\isasymcdot}\ {\isacharparenleft}x\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
-\isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymcdot}\ y{\isacharparenright}\ {\isasymcdot}\ z{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymcdot}\ x{\isacharparenright}\ {\isasymcdot}\ z{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ comm{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ y\ {\isasymcdot}\ {\isacharparenleft}x\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{finally}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
-\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-In this equational Isar proof, ``\isa{{\isasymdots}}'' refers to the
- right hand side of the preceding equation.
- After the proof is finished, the fact \isa{lcomm} is added to
- the locale \isa{comm{\isacharunderscore}semi}. This is done by adding a
- \textbf{notes} element to the internal representation of the locale,
- as explained the next section.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Locale Predicates and the Internal Representation of
- Locales%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec-locale-predicates}
- In mathematical texts, often arbitrary but fixed objects with
- certain properties are considered --- for instance, an arbitrary but
- fixed group $G$ --- with the purpose of establishing facts valid for
- any group. These facts are subsequently used on other objects that
- also have these properties.
-
- Locales permit the same style of reasoning. Exporting a fact $F$
- generalises the fixed parameters and leads to a (valid) formula of the
- form of equation~(\ref{eq-fact-in-context}). If a locale has many
- assumptions
- (possibly accumulated through a number of imports) this formula can
- become large and cumbersome. Therefore, Wenzel introduced
- predicates that abbreviate the assumptions of locales. These
- predicates are not confined to the locale but are visible in the
- surrounding theory.
-
- The definition of the locale \isa{semi} generates the \emph{locale
- predicate} \isa{semi} over the type of the parameter \isa{prod},
- hence the predicate's type is \isa{{\isacharparenleft}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ bool}. Its
- definition is
-\begin{equation}
- \tag*{\isa{semi{\isacharunderscore}def}:} \isa{semi\ {\isacharquery}prod\ {\isasymequiv}\ {\isasymforall}x\ y\ z{\isachardot}\ {\isacharquery}prod\ {\isacharparenleft}{\isacharquery}prod\ x\ y{\isacharparenright}\ z\ {\isacharequal}\ {\isacharquery}prod\ x\ {\isacharparenleft}{\isacharquery}prod\ y\ z{\isacharparenright}}.
-\end{equation}
- In the case where the locale has no import, the generated
- predicate abbreviates all assumptions and is over the parameters
- that occur in these assumptions.
-
- The situation is more complicated when a locale extends
- another locale, as is the case for \isa{comm{\isacharunderscore}semi}. Two
- predicates are defined. The predicate
- \isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms} corresponds to the new assumptions and is
- called \emph{delta predicate}, the locale
- predicate \isa{comm{\isacharunderscore}semi} captures the content of all the locale,
- including the import.
- If a locale has neither assumptions nor import, no predicate is
- defined. If a locale has import but no assumptions, only the locale
- predicate is defined.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-The Locales package generates a number of theorems for locale and
- delta predicates. All predicates have a definition and an
- introduction rule. Locale predicates that are defined in terms of
- other predicates (which is the case if and only if the locale has
- import) also have a number of elimination rules (called
- \emph{axioms}). All generated theorems for the predicates of the
- locales \isa{semi} and \isa{comm{\isacharunderscore}semi} are shown in
- Figures~\ref{fig-theorems-semi} and~\ref{fig-theorems-comm-semi},
- respectively.
- \begin{figure}
- \hrule
- \vspace{2ex}
- Theorems generated for the predicate \isa{semi}.
- \begin{gather}
- \tag*{\isa{semi{\isacharunderscore}def}:} \isa{semi\ {\isacharquery}prod\ {\isasymequiv}\ {\isasymforall}x\ y\ z{\isachardot}\ {\isacharquery}prod\ {\isacharparenleft}{\isacharquery}prod\ x\ y{\isacharparenright}\ z\ {\isacharequal}\ {\isacharquery}prod\ x\ {\isacharparenleft}{\isacharquery}prod\ y\ z{\isacharparenright}} \\
- \tag*{\isa{semi{\isachardot}intro}:} \isa{{\isacharparenleft}{\isasymAnd}x\ y\ z{\isachardot}\ {\isacharquery}prod\ {\isacharparenleft}{\isacharquery}prod\ x\ y{\isacharparenright}\ z\ {\isacharequal}\ {\isacharquery}prod\ x\ {\isacharparenleft}{\isacharquery}prod\ y\ z{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ semi\ {\isacharquery}prod}
- \end{gather}
- \hrule
- \caption{Theorems for the locale predicate \isa{semi}.}
- \label{fig-theorems-semi}
- \end{figure}
-
- \begin{figure}[h]
- \hrule
- \vspace{2ex}
- Theorems generated for the predicate \isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms}.
- \begin{gather}
- \tag*{\isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms{\isacharunderscore}def}:} \isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms\ {\isacharquery}prod\ {\isasymequiv}\ {\isasymforall}x\ y{\isachardot}\ {\isacharquery}prod\ x\ y\ {\isacharequal}\ {\isacharquery}prod\ y\ x} \\
- \tag*{\isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms{\isachardot}intro}:} \isa{{\isacharparenleft}{\isasymAnd}x\ y{\isachardot}\ {\isacharquery}prod\ x\ y\ {\isacharequal}\ {\isacharquery}prod\ y\ x{\isacharparenright}\ {\isasymLongrightarrow}\ comm{\isacharunderscore}semi{\isacharunderscore}axioms\ {\isacharquery}prod}
- \end{gather}
- Theorems generated for the predicate \isa{comm{\isacharunderscore}semi}.
- \begin{gather}
- \tag*{\isa{comm{\isacharunderscore}semi{\isacharunderscore}def}:} \isa{comm{\isacharunderscore}semi\ {\isacharquery}prod\ {\isasymequiv}\ semi\ {\isacharquery}prod\ {\isasymand}\ comm{\isacharunderscore}semi{\isacharunderscore}axioms\ {\isacharquery}prod} \\
- \tag*{\isa{comm{\isacharunderscore}semi{\isachardot}intro}:} \isa{{\isasymlbrakk}semi\ {\isacharquery}prod{\isacharsemicolon}\ comm{\isacharunderscore}semi{\isacharunderscore}axioms\ {\isacharquery}prod{\isasymrbrakk}\ {\isasymLongrightarrow}\ comm{\isacharunderscore}semi\ {\isacharquery}prod} \\
- \tag*{\isa{comm{\isacharunderscore}semi{\isachardot}axioms}:} \mbox{} \\
- \notag \isa{comm{\isacharunderscore}semi\ {\isacharquery}prod\ {\isasymLongrightarrow}\ semi\ {\isacharquery}prod} \\
- \notag \isa{comm{\isacharunderscore}semi\ {\isacharquery}prod\ {\isasymLongrightarrow}\ comm{\isacharunderscore}semi{\isacharunderscore}axioms\ {\isacharquery}prod}
- \end{gather}
- \hrule
- \caption{Theorems for the predicates \isa{comm{\isacharunderscore}semi{\isacharunderscore}axioms} and
- \isa{comm{\isacharunderscore}semi}.}
- \label{fig-theorems-comm-semi}
- \end{figure}
- Note that the theorems generated by a locale
- definition may be inspected immediately after the definition in the
- Proof General interface \cite{Aspinall2000} of Isabelle through
- the menu item ``Isabelle/Isar$>$Show me $\ldots>$Theorems''.
-
- Locale and delta predicates are used also in the internal
- representation of locales as lists of context elements. While all
- \textbf{fixes} in a
- declaration generate internal \textbf{fixes}, all assumptions
- of one locale declaration contribute to one internal \textbf{assumes}
- element. The internal representation of \isa{semi} is
-\[
-\begin{array}{ll}
- \textbf{fixes} & \isa{prod} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}}
- (\textbf{infixl} \isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}} 70) \\
- \textbf{assumes} & \isa{{\isachardoublequote}semi\ prod{\isachardoublequote}} \\
- \textbf{notes} & \isa{assoc}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}}
-\end{array}
-\]
- and the internal representation of \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isachardoublequote}} is
-\begin{equation}
-\label{eq-comm-semi}
-\begin{array}{ll}
- \textbf{fixes} & \isa{prod} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}}
- ~(\textbf{infixl}~\isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}}~70) \\
- \textbf{assumes} & \isa{{\isachardoublequote}semi\ prod{\isachardoublequote}} \\
- \textbf{notes} & \isa{assoc}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
- \textbf{assumes} & \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isacharunderscore}axioms\ prod{\isachardoublequote}} \\
- \textbf{notes} & \isa{comm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}x{\isachardoublequote}} \\
- \textbf{notes} & \isa{lcomm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}}
-\end{array}
-\end{equation}
- The \textbf{notes} elements store facts of the
- locales. The facts \isa{assoc} and \isa{comm} were added
- during the declaration of the locales. They stem from assumptions,
- which are trivially facts. The fact \isa{lcomm} was
- added later, after finishing the proof in the respective
- \textbf{theorem} command above.
-
- By using \textbf{notes} in a declaration, facts can be added
- to a locale directly. Of course, these must be theorems.
- Typical use of this feature includes adding theorems that are not
- usually used as a default rewrite rules by the simplifier to the
- simpset of the locale by a \textbf{notes} element with the attribute
- \isa{{\isacharbrackleft}simp{\isacharbrackright}}. This way it is also possible to add specialised
- versions of
- theorems to a locale by instantiating locale parameters for unknowns
- or locale assumptions for premises.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Definitions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Definitions were available in Kamm\"uller's version of Locales, and
- they are in Wenzel's.
- The context element \textbf{defines} adds a definition of the form
- \isa{p\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t} as an assumption, where \isa{p} is a
- parameter of the locale (possibly an imported parameter), and \isa{t} a term that may contain the \isa{x\isactrlsub i}. The parameter may
- neither occur in a previous \textbf{assumes} or \textbf{defines}
- element, nor on the right hand side of the definition. Hence
- recursion is not allowed.
- The parameter may, however, occur in subsequent \textbf{assumes} and
- on the right hand side of subsequent \textbf{defines}. We call
- \isa{p} \emph{defined parameter}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{locale}\ semi{\isadigit{2}}\ {\isacharequal}\ semi\ {\isacharplus}\isanewline
-\ \ \isakeyword{fixes}\ rprod\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \isakeyword{defines}\ rprod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}rprod\ x\ y\ {\isasymequiv}\ y\ {\isasymcdot}\ x\ {\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-This locale extends \isa{semi} by a second binary operation \isa{{\isachardoublequote}{\isasymodot}{\isachardoublequote}} that is like \isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}} but with
- reversed arguments. The
- definition of the locale generates the predicate \isa{semi{\isadigit{2}}},
- which is equivalent to \isa{semi}, but no \isa{semi{\isadigit{2}}{\isacharunderscore}axioms}.
- The difference between \textbf{assumes} and \textbf{defines} lies in
- the way parameters are treated on export.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Export%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-A fact is exported out
- of a locale by generalising over the parameters and adding
- assumptions as premises. For brevity of the exported theorems,
- locale predicates are used. Exported facts are referenced by
- writing qualified names consisting of the locale name and the fact name ---
- for example,
-\begin{equation}
- \tag*{\isa{semi{\isachardot}assoc}:} \isa{semi\ {\isacharquery}prod\ {\isasymLongrightarrow}\ {\isacharquery}prod\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}prod\ {\isacharquery}x\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}}.
-\end{equation}
- Defined parameters receive special treatment. Instead of adding a
- premise for the definition, the definition is unfolded in the
- exported theorem. In order to illustrate this we prove that the
- reverse operation \isa{{\isachardoublequote}{\isasymodot}{\isachardoublequote}} defined in the locale
- \isa{semi{\isadigit{2}}} is also associative.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{theorem}\ {\isacharparenleft}\isakeyword{in}\ semi{\isadigit{2}}{\isacharparenright}\ r{\isacharunderscore}assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ rprod{\isacharunderscore}def\ assoc{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-The exported fact is
-\begin{equation}
- \tag*{\isa{semi{\isadigit{2}}{\isachardot}r{\isacharunderscore}assoc}:} \isa{semi{\isadigit{2}}\ {\isacharquery}prod\ {\isasymLongrightarrow}\ {\isacharquery}prod\ {\isacharquery}z\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}y\ {\isacharquery}x{\isacharparenright}\ {\isacharequal}\ {\isacharquery}prod\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}z\ {\isacharquery}y{\isacharparenright}\ {\isacharquery}x}.
-\end{equation}
- The defined parameter is not present but is replaced by its
- definition. Note that the definition itself is not exported, hence
- there is no \isa{semi{\isadigit{2}}{\isachardot}rprod{\isacharunderscore}def}.%
-\footnote{The definition could alternatively be exported using a
- let-construct if there was one in Isabelle's meta-logic. Let is
- usually defined in object-logics.}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Locale Expressions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Locale expressions provide a simple language for combining
- locales. They are an effective means of building complex
- specifications from simple ones. Locale expressions are the main
- innovation of the version of Locales discussed here. Locale
- expressions are also reason for introducing locale predicates.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Rename and Merge%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The grammar of locale expressions is part of the grammar in
- Figure~\ref{fig-grammar}. Locale names are locale
- expressions, and
- further expressions are obtained by \emph{rename} and \emph{merge}.
-\begin{description}
-\item[Rename.]
- The locale expression $e\: q_1 \ldots q_n$ denotes
- the locale of $e$ where pa\-ra\-me\-ters, in the order in
- which they are fixed, are renamed to $q_1$ to $q_n$.
- The expression is only well-formed if $n$ does not
- exceed the number of parameters of $e$. Underscores denote
- parameters that are not renamed.
- Parameters whose names are changed lose mixfix syntax,
- and there is currently no way to re-equip them with such.
-\item[Merge.]
- The locale expression $e_1 + e_2$ denotes
- the locale obtained by merging the locales of $e_1$
- and $e_2$. This locale contains the context elements
- of $e_1$, followed by the context elements of $e_2$.
-
- In actual fact, the semantics of the merge operation
- is more complicated. If $e_1$ and $e_2$ are expressions containing
- the same name, followed by
- identical parameter lists, then the merge of both will contain
- the elements of those locales only once. Details are explained in
- Section~\ref{sec-normal-forms} below.
-
- The merge operation is associative but not commutative. The latter
- is because parameters of $e_1$ appear
- before parameters of $e_2$ in the composite expression.
-\end{description}
-
- Rename can be used if a different parameter name seems more
- appropriate --- for example, when moving from groups to rings, a
- parameter \isa{G} representing the group could be changed to
- \isa{R}. Besides of this stylistic use, renaming is important in
- combination with merge. Both operations are used in the following
- specification of semigroup homomorphisms.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{locale}\ semi{\isacharunderscore}hom\ {\isacharequal}\ comm{\isacharunderscore}semi\ sum\ {\isacharplus}\ comm{\isacharunderscore}semi\ {\isacharplus}\isanewline
-\ \ \isakeyword{fixes}\ hom\isanewline
-\ \ \isakeyword{assumes}\ hom{\isacharcolon}\ {\isachardoublequote}hom\ {\isacharparenleft}sum\ x\ y{\isacharparenright}\ {\isacharequal}\ hom\ x\ {\isasymcdot}\ hom\ y{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-This locale defines a context with three parameters \isa{sum},
- \isa{prod} and \isa{hom}. Only the second parameter has
- mixfix syntax. The first two are associative operations,
- the first of type \isa{{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a}, the second of
- type \isa{{\isacharbrackleft}{\isacharprime}b{\isacharcomma}\ {\isacharprime}b{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}b}.
-
- How are facts that are imported via a locale expression identified?
- Facts are always introduced in a named locale (either in the
- locale's declaration, or by using the locale as target in
- \textbf{theorem}), and their names are
- qualified by the parameter names of this locale.
- Hence the full name of associativity in \isa{semi} is
- \isa{prod{\isachardot}assoc}. Renaming parameters of a target also renames
- the qualifier of facts. Hence, associativity of \isa{sum} is
- \isa{sum{\isachardot}assoc}. Several parameters are separated by
- underscores in qualifiers. For example, the full name of the fact
- \isa{hom} in the locale \isa{semi{\isacharunderscore}hom} is \isa{sum{\isacharunderscore}prod{\isacharunderscore}hom{\isachardot}hom}.
-
- The following example is quite artificial, it illustrates the use of
- facts, though.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{theorem}\ {\isacharparenleft}\isakeyword{in}\ semi{\isacharunderscore}hom{\isacharparenright}\ {\isachardoublequote}hom\ x\ {\isasymcdot}\ {\isacharparenleft}hom\ y\ {\isasymcdot}\ hom\ z{\isacharparenright}\ {\isacharequal}\ hom\ {\isacharparenleft}sum\ x\ {\isacharparenleft}sum\ y\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
-\isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}hom\ x\ {\isasymcdot}\ {\isacharparenleft}hom\ y\ {\isasymcdot}\ hom\ z{\isacharparenright}\ {\isacharequal}\ hom\ y\ {\isasymcdot}\ {\isacharparenleft}hom\ x\ {\isasymcdot}\ hom\ z{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ prod{\isachardot}lcomm{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ hom\ {\isacharparenleft}sum\ y\ {\isacharparenleft}sum\ x\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ hom{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ hom\ {\isacharparenleft}sum\ x\ {\isacharparenleft}sum\ y\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ sum{\isachardot}lcomm{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{finally}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
-\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-Importing via a locale expression imports all facts of
- the imported locales, hence both \isa{sum{\isachardot}lcomm} and \isa{prod{\isachardot}lcomm} are
- available in \isa{hom{\isacharunderscore}semi}. The import is dynamic --- that is,
- whenever facts are added to a locale, they automatically
- become available in subsequent \textbf{theorem} commands that use
- the locale as a target, or a locale importing the locale.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Normal Forms%
-}
-\isamarkuptrue%
-%
-\label{sec-normal-forms}
-\newcommand{\I}{\mathcal{I}}
-\newcommand{\F}{\mathcal{F}}
-\newcommand{\N}{\mathcal{N}}
-\newcommand{\C}{\mathcal{C}}
-\newcommand{\App}{\mathbin{\overline{@}}}
-%
-\begin{isamarkuptext}%
-Locale expressions are interpreted in a two-step process. First, an
- expression is normalised, then it is converted to a list of context
- elements.
-
- Normal forms are based on \textbf{locale} declarations. These
- consist of an import section followed by a list of context
- elements. Let $\I(l)$ denote the locale expression imported by
- locale $l$. If $l$ has no import then $\I(l) = \varepsilon$.
- Likewise, let $\F(l)$ denote the list of context elements, also
- called the \emph{context fragment} of $l$. Note that $\F(l)$
- contains only those context elements that are stated in the
- declaration of $l$, not imported ones.
-
-\paragraph{Example 1.} Consider the locales \isa{semi} and \isa{comm{\isacharunderscore}semi}. We have $\I(\isa{semi}) = \varepsilon$ and
- $\I(\isa{comm{\isacharunderscore}semi}) = \isa{semi}$, and the context fragments
- are
-\begin{align*%
-}
- \F(\isa{semi}) & = \left[
-\begin{array}{ll}
- \textbf{fixes} & \isa{prod} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}}
- ~(\textbf{infixl}~\isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}}~70) \\
- \textbf{assumes} & \isa{{\isachardoublequote}semi\ prod{\isachardoublequote}} \\
- \textbf{notes} & \isa{assoc}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}}
-\end{array} \right], \\
- \F(\isa{comm{\isacharunderscore}semi}) & = \left[
-\begin{array}{ll}
- \textbf{assumes} & \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isacharunderscore}axioms\ prod{\isachardoublequote}} \\
- \textbf{notes} & \isa{comm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}x{\isachardoublequote}} \\
- \textbf{notes} & \isa{lcomm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}}
-\end{array} \right].
-\end{align*%
-}
- Let $\pi_0(\F(l))$ denote the list of parameters defined in the
- \textbf{fixes} elements of $\F(l)$ in the order of their occurrence.
- The list of parameters of a locale expression $\pi(e)$ is defined as
- follows:
-\begin{align*%
-}
- \pi(l) & = \pi(\I(l)) \App \pi_0(\F(l)) \text{, for named locale $l$.} \\
- \pi(e\: q_1 \ldots q_n) & = \text{$[q_1, \ldots, q_n, p_{n+1}, \ldots,
- p_{m}]$, where $\pi(e) = [p_1, \ldots, p_m]$.} \\
- \pi(e_1 + e_2) & = \pi(e_1) \App \pi(e_2)
-\end{align*%
-}
- The operation $\App$ concatenates two lists but omits elements from
- the second list that are also present in the first list.
- It is not possible to rename more parameters than there
- are present in an expression --- that is, $n \le m$ --- otherwise
- the renaming is illegal. If $q_i
- = \_$ then the $i$th entry of the resulting list is $p_i$.
-
- In the normalisation phase, imports of named locales are unfolded, and
- renames and merges are recursively propagated to the imported locale
- expressions. The result is a list of locale names, each with a full
- list of parameters, where locale names occurring with the same parameter
- list twice are removed. Let $\N$ denote normalisation. It is defined
- by these equations:
-\begin{align*%
-}
- \N(l) & = \N(\I(l)) \App [l\:\pi(l)] \text{, for named locale $l$.} \\
- \N(e\: q_1 \ldots q_n) & = \N(e)\:[q_1 \ldots q_n/\pi(e)] \\
- \N(e_1 + e_2) & = \N(e_1) \App \N(e_2)
-\end{align*%
-}
- Normalisation yields a list of \emph{identifiers}. An identifier
- consists of a locale name and a (possibly empty) list of parameters.
-
- In the second phase, the list of identifiers $\N(e)$ is converted to
- a list of context elements $\C(e)$ by converting each identifier to
- a list of context elements, and flattening the obtained list.
- Conversion of the identifier $l\:q_1 \ldots q_n$ yields the list of
- context elements $\F(l)$, but with the following modifications:
-\begin{itemize}
-\item
- Rename the parameter in the $i$th \textbf{fixes} element of $\F(l)$
- to $q_i$, $i = 1, \ldots, n$. If the parameter name is actually
- changed then delete the syntax annotation. Renaming a parameter may
- also change its type.
-\item
- Perform the same renamings on all occurrences of parameters (fixed
- variables) in \textbf{assumes}, \textbf{defines} and \textbf{notes}
- elements.
-\item
- Qualify names of facts by $q_1\_\ldots\_q_n$.
-\end{itemize}
- The locale expression is \emph{well-formed} if it contains no
- illegal renamings and the following conditions on $\C(e)$ hold,
- otherwise the expression is rejected:
-\begin{itemize}
-\item Parameters in \textbf{fixes} are distinct;
-\item Free variables in \textbf{assumes} and
- \textbf{defines} occur in preceding \textbf{fixes};%
-\footnote{This restriction is relaxed for contexts obtained with
- \textbf{includes}, see Section~\ref{sec-includes}.}
-\item Parameters defined in \textbf{defines} must neither occur in
- preceding \textbf{assumes} nor \textbf{defines}.
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Examples%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\paragraph{Example 2.}
- We obtain the context fragment $\C(\isa{comm{\isacharunderscore}semi})$ of the
- locale \isa{comm{\isacharunderscore}semi}. First, the parameters are computed.
-\begin{align*%
-}
- \pi(\isa{semi}) & = [\isa{prod}] \\
- \pi(\isa{comm{\isacharunderscore}semi}) & = \pi(\isa{semi}) \App []
- = [\isa{prod}]
-\end{align*%
-}
- Next, the normal form of the locale expression
- \isa{comm{\isacharunderscore}semi} is obtained.
-\begin{align*%
-}
- \N(\isa{semi}) & = [\isa{semi} \isa{prod}] \\
- \N(\isa{comm{\isacharunderscore}semi}) & = \N(\isa{semi}) \App
- [\isa{comm{\isacharunderscore}semi\ prod}]
- = [\isa{semi\ prod}, \isa{comm{\isacharunderscore}semi\ prod}]
-\end{align*%
-}
- Converting this to a list of context elements leads to the
- list~(\ref{eq-comm-semi}) shown in
- Section~\ref{sec-locale-predicates}, but with fact names qualified
- by \isa{prod} --- for example, \isa{prod{\isachardot}assoc}.
- Qualification was omitted to keep the presentation simple.
- Isabelle's scoping rules identify the most recent fact with
- qualified name $x.a$ when a fact with name $a$ is requested.
-
-\paragraph{Example 3.}
- The locale expression \isa{comm{\isacharunderscore}semi\ sum} involves
- renaming. Computing parameters yields $\pi(\isa{comm{\isacharunderscore}semi\ sum})
- = [\isa{sum}]$, the normal form is
-\begin{align*%
-}
- \N(\isa{comm{\isacharunderscore}semi\ sum}) & =
- \N(\isa{comm{\isacharunderscore}semi})[\isa{sum}/\isa{prod}] =
- [\isa{semi\ sum}, \isa{comm{\isacharunderscore}semi\ sum}]
-\end{align*%
-}
- and the list of context elements
-\[
-\begin{array}{ll}
- \textbf{fixes} & \isa{sum} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}} \\
- \textbf{assumes} & \isa{{\isachardoublequote}semi\ sum{\isachardoublequote}} \\
- \textbf{notes} & \isa{sum{\isachardot}assoc}: \isa{{\isachardoublequote}sum\ {\isacharparenleft}sum\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharquery}z\ {\isacharequal}\ sum\ {\isacharquery}x\ {\isacharparenleft}sum\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
- \textbf{assumes} & \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isacharunderscore}axioms\ sum{\isachardoublequote}} \\
- \textbf{notes} & \isa{sum{\isachardot}comm}: \isa{{\isachardoublequote}sum\ {\isacharquery}x\ {\isacharquery}y\ {\isacharequal}\ sum\ {\isacharquery}y\ {\isacharquery}x{\isachardoublequote}} \\
- \textbf{notes} & \isa{sum{\isachardot}lcomm}: \isa{{\isachardoublequote}sum\ {\isacharquery}x\ {\isacharparenleft}sum\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ sum\ {\isacharquery}y\ {\isacharparenleft}sum\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}}
-\end{array}
-\]
-
-\paragraph{Example 4.}
- The context defined by the locale \isa{semi{\isacharunderscore}hom} involves
- merging two copies of \isa{comm{\isacharunderscore}semi}. We obtain the parameter
- list and normal form:
-\begin{align*%
-}
- \pi(\isa{semi{\isacharunderscore}hom}) & = \pi(\isa{comm{\isacharunderscore}semi\ sum} +
- \isa{comm{\isacharunderscore}semi}) \App [\isa{hom}] \\
- & = (\pi(\isa{comm{\isacharunderscore}semi\ sum}) \App \pi(\isa{comm{\isacharunderscore}semi}))
- \App [\isa{hom}] \\
- & = ([\isa{sum}] \App [\isa{prod}]) \App [\isa{hom}]
- = [\isa{sum}, \isa{prod}, \isa{hom}] \\
- \N(\isa{semi{\isacharunderscore}hom}) & =
- \N(\isa{comm{\isacharunderscore}semi\ sum} + \isa{comm{\isacharunderscore}semi}) \App \\
- & \phantom{==}
- [\isa{semi{\isacharunderscore}hom\ sum\ prod\ hom}] \\
- & = (\N(\isa{comm{\isacharunderscore}semi\ sum}) \App \N(\isa{comm{\isacharunderscore}semi})) \App \\
- & \phantom{==}
- [\isa{semi{\isacharunderscore}hom\ sum\ prod\ hom}] \\
- & = ([\isa{semi\ sum}, \isa{comm{\isacharunderscore}semi\ sum}] \App %\\
-% & \phantom{==}
- [\isa{semi\ prod}, \isa{comm{\isacharunderscore}semi\ prod}]) \App \\
- & \phantom{==}
- [\isa{semi{\isacharunderscore}hom\ sum\ prod\ hom}] \\
- & = [\isa{semi\ sum}, \isa{comm{\isacharunderscore}semi\ sum},
- \isa{semi\ prod}, \isa{comm{\isacharunderscore}semi\ prod}, \\
- & \phantom{==}
- \isa{semi{\isacharunderscore}hom\ sum\ prod\ hom}].
-\end{align*%
-}
- Hence $\C(\isa{semi{\isacharunderscore}hom})$, shown below, is again well-formed.
-\[
-\begin{array}{ll}
- \textbf{fixes} & \isa{sum} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}} \\
- \textbf{assumes} & \isa{{\isachardoublequote}semi\ sum{\isachardoublequote}} \\
- \textbf{notes} & \isa{sum{\isachardot}assoc}: \isa{{\isachardoublequote}sum\ {\isacharparenleft}sum\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharquery}z\ {\isacharequal}\ sum\ {\isacharquery}x\ {\isacharparenleft}sum\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
- \textbf{assumes} & \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isacharunderscore}axioms\ sum{\isachardoublequote}} \\
- \textbf{notes} & \isa{sum{\isachardot}comm}: \isa{{\isachardoublequote}sum\ {\isacharquery}x\ {\isacharquery}y\ {\isacharequal}\ sum\ {\isacharquery}y\ {\isacharquery}x{\isachardoublequote}} \\
- \textbf{notes} & \isa{sum{\isachardot}lcomm}: \isa{{\isachardoublequote}sum\ {\isacharquery}x\ {\isacharparenleft}sum\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ sum\ {\isacharquery}y\ {\isacharparenleft}sum\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
- \textbf{fixes} & \isa{prod} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}b{\isacharcomma}\ {\isacharprime}b{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequote}}
- ~(\textbf{infixl}~\isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}}~70) \\
- \textbf{assumes} & \isa{{\isachardoublequote}semi\ prod{\isachardoublequote}} \\
- \textbf{notes} & \isa{prod{\isachardot}assoc}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z\ {\isacharequal}\ {\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
- \textbf{assumes} & \isa{{\isachardoublequote}comm{\isacharunderscore}semi{\isacharunderscore}axioms\ prod{\isachardoublequote}} \\
- \textbf{notes} & \isa{prod{\isachardot}comm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharquery}x{\isachardoublequote}} \\
- \textbf{notes} & \isa{prod{\isachardot}lcomm}: \isa{{\isachardoublequote}{\isacharquery}x\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}y\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ {\isacharquery}y\ {\isasymcdot}\ {\isacharparenleft}{\isacharquery}x\ {\isasymcdot}\ {\isacharquery}z{\isacharparenright}{\isachardoublequote}} \\
- \textbf{fixes} & \isa{hom} :: \isa{{\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequote}} \\
- \textbf{assumes} & \isa{{\isachardoublequote}semi{\isacharunderscore}hom{\isacharunderscore}axioms\ sum{\isachardoublequote}} \\
- \textbf{notes} & \isa{sum{\isacharunderscore}prod{\isacharunderscore}hom{\isachardot}hom}:
- \isa{hom\ {\isacharparenleft}sum\ x\ y{\isacharparenright}\ {\isacharequal}\ hom\ x\ {\isasymcdot}\ hom\ y}
-\end{array}
-\]
-
-\paragraph{Example 5.}
- In this example, a locale expression leading to a list of context
- elements that is not well-defined is encountered, and it is illustrated
- how normalisation deals with multiple inheritance.
- Consider the specification of monads (in the algebraic sense)
- and monoids.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{locale}\ monad\ {\isacharequal}\isanewline
-\ \ \isakeyword{fixes}\ prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymcdot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequote}{\isasymone}{\isachardoublequote}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \isakeyword{assumes}\ l{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymcdot}\ x\ {\isacharequal}\ x{\isachardoublequote}\ \isakeyword{and}\ r{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}x\ {\isasymcdot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-Monoids are both semigroups and monads and one would want to
- specify them as locale expression \isa{semi\ {\isacharplus}\ monad}.
- Unfortunately, this expression is not well-formed. Its normal form
-\begin{align*%
-}
- \N(\isa{monad}) & = [\isa{monad\ prod}] \\
- \N(\isa{semi}+\isa{monad}) & =
- \N(\isa{semi}) \App \N(\isa{monad})
- = [\isa{semi\ prod}, \isa{monad\ prod}]
-\end{align*%
-}
- leads to a list containing the context element
-\[
- \textbf{fixes}~\isa{prod} :: \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}}
- ~(\textbf{infixl}~\isa{{\isachardoublequote}{\isasymcdot}{\isachardoublequote}}~70)
-\]
- twice and thus violating the first criterion of well-formedness. To
- avoid this problem, one can
- introduce a new locale \isa{magma} with the sole purpose of fixing the
- parameter and defining its syntax. The specifications of semigroup
- and monad are changed so that they import \isa{magma}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{locale}\ magma\ {\isacharequal}\ \isakeyword{fixes}\ prod\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymcdot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isanewline
-\isamarkupfalse%
-\isacommand{locale}\ semi{\isacharprime}\ {\isacharequal}\ magma\ {\isacharplus}\ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymcdot}\ y{\isacharparenright}\ {\isasymcdot}\ z\ {\isacharequal}\ x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
-\isamarkupfalse%
-\isacommand{locale}\ monad{\isacharprime}\ {\isacharequal}\ magma\ {\isacharplus}\ \isakeyword{fixes}\ one\ {\isacharparenleft}{\isachardoublequote}{\isasymone}{\isachardoublequote}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \isakeyword{assumes}\ l{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymcdot}\ x\ {\isacharequal}\ x{\isachardoublequote}\ \isakeyword{and}\ r{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}x\ {\isasymcdot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-Normalisation now yields
-\begin{align*%
-}
- \N(\isa{semi{\isacharprime}\ {\isacharplus}\ monad{\isacharprime}}) & =
- \N(\isa{semi{\isacharprime}}) \App \N(\isa{monad{\isacharprime}}) \\
- & = (\N(\isa{magma}) \App [\isa{semi{\isacharprime}\ prod}]) \App
- (\N(\isa{magma}) \App [\isa{monad{\isacharprime}\ prod}]) \\
- & = [\isa{magma\ prod}, \isa{semi{\isacharprime}\ prod}] \App
- [\isa{magma\ prod}, \isa{monad{\isacharprime}\ prod}]) \\
- & = [\isa{magma\ prod}, \isa{semi{\isacharprime}\ prod},
- \isa{monad{\isacharprime}\ prod}]
-\end{align*%
-}
- where the second occurrence of \isa{magma\ prod} is eliminated.
- The reader is encouraged to check, using the \textbf{print\_locale}
- command, that the list of context elements generated from this is
- indeed well-formed.
-
- It follows that importing
- parameters is more flexible than fixing them using a context element.
- The Locale package provides the predefined locale \isa{var} that
- can be used to import parameters if no
- particular mixfix syntax is required.
- Its definition is
-\begin{center}
- \textbf{locale} \textit{var} = \textbf{fixes} \isa{x{\isacharunderscore}}
-\end{center}
- The use of the internal variable \isa{x{\isacharunderscore}}
- enforces that the parameter is renamed before being used, because
- internal variables may not occur in the input syntax.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Includes%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec-includes}
- The context element \textbf{includes} takes a locale expression $e$
- as argument. It can occur at any point in a locale declaration, and
- it adds $\C(e)$ to the current context.
-
- If \textbf{includes} $e$ appears as context element in the
- declaration of a named locale $l$, the included context is only
- visible in subsequent context elements, but it is not propagated to
- $l$. That is, if $l$ is later used as a target, context elements
- from $\C(e)$ are not added to the context. Although it is
- conceivable that this mechanism could be used to add only selected
- facts from $e$ to $l$ (with \textbf{notes} elements following
- \textbf{includes} $e$), currently no useful applications of this are
- known.
-
- The more common use of \textbf{includes} $e$ is in long goals, where it
- adds, like a target, locale context to the proof context. Unlike
- with targets, the proved theorem is not stored
- in the locale. Instead, it is exported immediately.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{theorem}\ lcomm{\isadigit{2}}{\isacharcolon}\isanewline
-\ \ \isakeyword{includes}\ comm{\isacharunderscore}semi\ \isakeyword{shows}\ {\isachardoublequote}x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}\ {\isacharequal}\ y\ {\isasymcdot}\ {\isacharparenleft}x\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
-\isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}x\ {\isasymcdot}\ {\isacharparenleft}y\ {\isasymcdot}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymcdot}\ y{\isacharparenright}\ {\isasymcdot}\ z{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymcdot}\ x{\isacharparenright}\ {\isasymcdot}\ z{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ comm{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ y\ {\isasymcdot}\ {\isacharparenleft}x\ {\isasymcdot}\ z{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{finally}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
-\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-This proof is identical to the proof of \isa{lcomm}. The use of
- \textbf{includes} provides the same context and facts as when using
- \isa{comm{\isacharunderscore}semi} as target. On the other hand, \isa{lcomm{\isadigit{2}}} is not added as a fact to the locale \isa{comm{\isacharunderscore}semi}, but
- is directly visible in the theory. The theorem is
-\[
- \isa{comm{\isacharunderscore}semi\ {\isacharquery}prod\ {\isasymLongrightarrow}\ {\isacharquery}prod\ {\isacharquery}x\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ {\isacharquery}prod\ {\isacharquery}y\ {\isacharparenleft}{\isacharquery}prod\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}}.
-\]
- Note that it is possible to
- combine a target and (several) \textbf{includes} in a goal statement, thus
- using contexts of several locales but storing the theorem in only
- one of them.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Structures%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec-structures}
- The specifications of semigroups and monoids that served as examples
- in previous sections modelled each operation of an algebraic
- structure as a single parameter. This is rather inconvenient for
- structures with many operations, and also unnatural. In accordance
- to mathematical texts, one would rather fix two groups instead of
- two sets of operations.
-
- The approach taken in Isabelle is to encode algebraic structures
- with suitable types (in Isabelle/HOL usually records). An issue to
- be addressed by
- locales is syntax for algebraic structures. This is the purpose of
- the \textbf{(structure)} annotation in \textbf{fixes}, introduced by
- Wenzel. We illustrate this, independently of record types, with a
- different formalisation of semigroups.
-
- Let \isa{{\isacharprime}a\ semi{\isacharunderscore}type} be a not further specified type that
- represents semigroups over the carrier type \isa{{\isacharprime}a}. Let \isa{s{\isacharunderscore}op} be an operation that maps an object of \isa{{\isacharprime}a\ semi{\isacharunderscore}type} to
- a binary operation.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{typedecl}\ {\isacharprime}a\ semi{\isacharunderscore}type\isanewline
-\isamarkupfalse%
-\isacommand{consts}\ s{\isacharunderscore}op\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a\ semi{\isacharunderscore}type{\isacharcomma}\ {\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymstar}{\isasymindex}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-Although \isa{s{\isacharunderscore}op} is a ternary operation, it is declared
- infix. The syntax annotation contains the token \isa{{\isasymindex}}
- (\verb.\<index>.), which refers to the first argument. This syntax is only
- effective in the context of a locale, and only if the first argument
- is a
- \emph{structural} parameter --- that is, a parameter with annotation
- \textbf{(structure)}. The token has the effect of replacing the
- parameter with a subscripted number, the index of the structural
- parameter in the locale. This replacement takes place both for
- printing and
- parsing. Subscripted $1$ for the first structural
- parameter may be omitted, as in this specification of semigroups with
- structures:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{locale}\ comm{\isacharunderscore}semi{\isacharprime}\ {\isacharequal}\isanewline
-\ \ \isakeyword{fixes}\ G\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ semi{\isacharunderscore}type{\isachardoublequote}\ {\isacharparenleft}\isakeyword{structure}{\isacharparenright}\isanewline
-\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymstar}\ y{\isacharparenright}\ {\isasymstar}\ z\ {\isacharequal}\ x\ {\isasymstar}\ {\isacharparenleft}y\ {\isasymstar}\ z{\isacharparenright}{\isachardoublequote}\ \isakeyword{and}\ comm{\isacharcolon}\ {\isachardoublequote}x\ {\isasymstar}\ y\ {\isacharequal}\ y\ {\isasymstar}\ x{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-Here \isa{x\ {\isasymstar}\ y} is equivalent to \isa{x\ {\isasymstar}\isactrlsub {\isadigit{1}}\ y} and
- abbreviates \isa{s{\isacharunderscore}op\ G\ x\ y}. A specification of homomorphisms
- requires a second structural parameter.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{locale}\ semi{\isacharprime}{\isacharunderscore}hom\ {\isacharequal}\ comm{\isacharunderscore}semi{\isacharprime}\ {\isacharplus}\ comm{\isacharunderscore}semi{\isacharprime}\ H\ {\isacharplus}\isanewline
-\ \ \isakeyword{fixes}\ hom\isanewline
-\ \ \isakeyword{assumes}\ hom{\isacharcolon}\ {\isachardoublequote}hom\ {\isacharparenleft}x\ {\isasymstar}\ y{\isacharparenright}\ {\isacharequal}\ hom\ x\ {\isasymstar}\isactrlsub {\isadigit{2}}\ hom\ y{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-The parameter \isa{H} is defined in the second \textbf{fixes}
- element of $\C(\isa{semi{\isacharprime}{\isacharunderscore}comm})$. Hence \isa{{\isasymstar}\isactrlsub {\isadigit{2}}}
- abbreviates \isa{s{\isacharunderscore}op\ H\ x\ y}. The same construction can be done
- with records instead of an \textit{ad-hoc} type. In general, the
- $i$th structural parameter is addressed by index $i$. Only the
- index $1$ may be omitted.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{record}\ {\isacharprime}a\ semi\ {\isacharequal}\ prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharbrackleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}a{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymbullet}{\isasymindex}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-This declares the types \isa{{\isacharprime}a\ semi} and \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ semi{\isacharunderscore}scheme}. The latter is an extensible record, where the second
- type argument is the type of the extension field. For details on
- records, see \cite{NipkowEtAl2002} Chapter~8.3.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{locale}\ semi{\isacharunderscore}w{\isacharunderscore}records\ {\isacharequal}\ struct\ G\ {\isacharplus}\isanewline
-\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymbullet}\ y{\isacharparenright}\ {\isasymbullet}\ z\ {\isacharequal}\ x\ {\isasymbullet}\ {\isacharparenleft}y\ {\isasymbullet}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-The type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ semi{\isacharunderscore}scheme} is inferred for the parameter \isa{G}. Using subtyping on records, the specification can be extended
- to groups easily.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{record}\ {\isacharprime}a\ group\ {\isacharequal}\ {\isachardoublequote}{\isacharprime}a\ semi{\isachardoublequote}\ {\isacharplus}\isanewline
-\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}{\isachardoublequote}l{\isasymindex}{\isachardoublequote}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ {\isacharparenleft}{\isachardoublequote}inv{\isasymindex}\ {\isacharunderscore}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{1}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isamarkupfalse%
-\isacommand{locale}\ group{\isacharunderscore}w{\isacharunderscore}records\ {\isacharequal}\ semi{\isacharunderscore}w{\isacharunderscore}records\ {\isacharplus}\isanewline
-\ \ \isakeyword{assumes}\ l{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}l\ {\isasymbullet}\ x\ {\isacharequal}\ x{\isachardoublequote}\ \isakeyword{and}\ l{\isacharunderscore}inv{\isacharcolon}\ {\isachardoublequote}inv\ x\ {\isasymbullet}\ x\ {\isacharequal}\ l{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-Finally, the predefined locale
-\begin{center}
- \textbf{locale} \textit{struct} = \textbf{fixes} \isa{S{\isacharunderscore}}
- \textbf{(structure)}.
-\end{center}
- is analogous to \isa{var}.
- More examples on the use of structures, including groups, rings and
- polynomials can be found in the Isabelle distribution in the
- session HOL-Algebra.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Conclusions and Outlook%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Locales provide a simple means of modular reasoning. They allow to
- abbreviate frequently occurring context statements and maintain facts
- valid in these contexts. Importantly, using structures, they allow syntax to be
- effective only in certain contexts, and thus to mimic common
- practice in mathematics, where notation is chosen very flexibly.
- This is also known as literate formalisation \cite{Bailey1998}.
- Locale expressions allow to duplicate and merge
- specifications. This is a necessity, for example, when reasoning about
- homomorphisms. Normalisation makes it possible to deal with
- diamond-shaped inheritance structures, and generally with directed
- acyclic graphs. The combination of locales with record
- types in higher-order logic provides an effective means for
- specifying algebraic structures: locale import and record subtyping
- provide independent hierarchies for specifications and structure
- elements. Rich examples for this can be found in
- the Isabelle distribution in the session HOL-Algebra.
-
- The primary reason for writing this report was to provide a better
- understanding of locales in Isar. Wenzel provided hardly any
- documentation, with the exception of \cite{Wenzel2002b}. The
- present report should make it easier for users of Isabelle to take
- advantage of locales.
-
- The report is also a base for future extensions. These include
- improved syntax for structures. Identifying them by numbers seems
- unnatural and can be confusing if more than two structures are
- involved --- for example, when reasoning about universal
- properties --- and numbering them by order of occurrence seems
- arbitrary. Another desirable feature is \emph{instantiation}. One
- may, in the course of a theory development, construct objects that
- fulfil the specification of a locale. These objects are possibly
- defined in the context of another locale. Instantiation should make it
- simple to specialise abstract facts for the object under
- consideration and to use the specified facts.
-
- A detailed comparison of locales with module systems in type theory
- has not been undertaken yet, but could be beneficial. For example,
- a module system for Coq has recently been presented by Chrzaszcz
- \cite{Chrzaszcz2003}. While the
- latter usually constitute extensions of the calculus, locales are
- a rather thin layer that does not change Isabelle's meta logic.
- Locales mainly manage specifications and facts. Functors, like
- the constructor for polynomial rings, remain objects of the
- logic.
-
- \textbf{Acknowledgements.} Lawrence C.\ Paulson and Norbert
- Schirmer made useful comments on a draft of this paper.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/Locales/Locales/generated/isabelle.sty Fri Aug 19 22:44:36 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,167 +0,0 @@
-%%
-%% Author: Markus Wenzel, TU Muenchen
-%%
-%% macros for Isabelle generated LaTeX output
-%%
-
-%%% Simple document preparation (based on theory token language and symbols)
-
-% isabelle environments
-
-\newcommand{\isabellecontext}{UNKNOWN}
-
-\newcommand{\isastyle}{\small\tt\slshape}
-\newcommand{\isastyleminor}{\small\tt\slshape}
-\newcommand{\isastylescript}{\footnotesize\tt\slshape}
-\newcommand{\isastyletext}{\normalsize\rm}
-\newcommand{\isastyletxt}{\rm}
-\newcommand{\isastylecmt}{\rm}
-
-%symbol markup -- \emph achieves decent spacing via italic corrections
-\newcommand{\isamath}[1]{\emph{$#1$}}
-\newcommand{\isatext}[1]{\emph{#1}}
-\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
-
-% somewhat hackish: spanning sub/super scripts (\<^bsub>..\<^esub>)
-\newcommand{\isactrlbsub}{%
-\def\isatext##1{\isastylescript##1}\begin{math}_\bgroup}
-\newcommand{\isactrlesub}{\egroup\end{math}}
-\newcommand{\isactrlbsup}{%
-\def\isatext##1{\isastylescript##1}\begin{math}^\bgroup}
-\newcommand{\isactrlesup}{\egroup\end{math}}
-
-\newdimen\isa@parindent\newdimen\isa@parskip
-
-\newenvironment{isabellebody}{%
-\isamarkuptrue\par%
-\isa@parindent\parindent\parindent0pt%
-\isa@parskip\parskip\parskip0pt%
-\isastyle}{\par}
-
-\newenvironment{isabelle}
-{\begin{trivlist}\begin{isabellebody}\item\relax}
-{\end{isabellebody}\end{trivlist}}
-
-\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
-
-\newcommand{\isaindent}[1]{\hphantom{#1}}
-\newcommand{\isanewline}{\mbox{}\par\mbox{}}
-\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
-\newcommand{\isadigit}[1]{#1}
-
-\chardef\isacharbang=`\!
-\chardef\isachardoublequote=`\"
-\chardef\isacharhash=`\#
-\chardef\isachardollar=`\$
-\chardef\isacharpercent=`\%
-\chardef\isacharampersand=`\&
-\chardef\isacharprime=`\'
-\chardef\isacharparenleft=`\(
-\chardef\isacharparenright=`\)
-\chardef\isacharasterisk=`\*
-\chardef\isacharplus=`\+
-\chardef\isacharcomma=`\,
-\chardef\isacharminus=`\-
-\chardef\isachardot=`\.
-\chardef\isacharslash=`\/
-\chardef\isacharcolon=`\:
-\chardef\isacharsemicolon=`\;
-\chardef\isacharless=`\<
-\chardef\isacharequal=`\=
-\chardef\isachargreater=`\>
-\chardef\isacharquery=`\?
-\chardef\isacharat=`\@
-\chardef\isacharbrackleft=`\[
-\chardef\isacharbackslash=`\\
-\chardef\isacharbrackright=`\]
-\chardef\isacharcircum=`\^
-\chardef\isacharunderscore=`\_
-\chardef\isacharbackquote=`\`
-\chardef\isacharbraceleft=`\{
-\chardef\isacharbar=`\|
-\chardef\isacharbraceright=`\}
-\chardef\isachartilde=`\~
-
-
-% keyword and section markup
-
-\newcommand{\isakeywordcharunderscore}{\_}
-\newcommand{\isakeyword}[1]
-{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
-\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
-\newcommand{\isacommand}[1]{\isakeyword{#1}}
-
-\newcommand{\isamarkupheader}[1]{\section{#1}}
-\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
-\newcommand{\isamarkupsection}[1]{\section{#1}}
-\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
-\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
-\newcommand{\isamarkupsect}[1]{\section{#1}}
-\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
-\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
-
-\newif\ifisamarkup
-\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
-\newcommand{\isaendpar}{\par\medskip}
-\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
-\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
-\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
-
-
-% alternative styles
-
-\newcommand{\isabellestyle}{}
-\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
-
-\newcommand{\isabellestylett}{%
-\renewcommand{\isastyle}{\small\tt}%
-\renewcommand{\isastyleminor}{\small\tt}%
-\renewcommand{\isastylescript}{\footnotesize\tt}%
-}
-\newcommand{\isabellestyleit}{%
-\renewcommand{\isastyle}{\small\it}%
-\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isastylescript}{\footnotesize\it}%
-\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbang}{\isamath{!}}%
-\renewcommand{\isachardoublequote}{}%
-\renewcommand{\isacharhash}{\isamath{\#}}%
-\renewcommand{\isachardollar}{\isamath{\$}}%
-\renewcommand{\isacharpercent}{\isamath{\%}}%
-\renewcommand{\isacharampersand}{\isamath{\&}}%
-\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
-\renewcommand{\isacharparenleft}{\isamath{(}}%
-\renewcommand{\isacharparenright}{\isamath{)}}%
-\renewcommand{\isacharasterisk}{\isamath{*}}%
-\renewcommand{\isacharplus}{\isamath{+}}%
-\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
-\renewcommand{\isacharminus}{\isamath{-}}%
-\renewcommand{\isachardot}{\isamath{\mathord.}}%
-\renewcommand{\isacharslash}{\isamath{/}}%
-\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
-\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
-\renewcommand{\isacharless}{\isamath{<}}%
-\renewcommand{\isacharequal}{\isamath{=}}%
-\renewcommand{\isachargreater}{\isamath{>}}%
-\renewcommand{\isacharat}{\isamath{@}}%
-\renewcommand{\isacharbrackleft}{\isamath{[}}%
-\renewcommand{\isacharbrackright}{\isamath{]}}%
-\renewcommand{\isacharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbraceleft}{\isamath{\{}}%
-\renewcommand{\isacharbar}{\isamath{\mid}}%
-\renewcommand{\isacharbraceright}{\isamath{\}}}%
-\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
-}
-
-\newcommand{\isabellestylesl}{%
-\isabellestyleit%
-\renewcommand{\isastyle}{\small\sl}%
-\renewcommand{\isastyleminor}{\sl}%
-\renewcommand{\isastylescript}{\footnotesize\sl}%
-}
--- a/doc-src/Locales/Locales/generated/isabellesym.sty Fri Aug 19 22:44:36 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,353 +0,0 @@
-%%
-%% Author: Markus Wenzel, TU Muenchen
-%%
-%% definitions of standard Isabelle symbols
-%%
-
-% symbol definitions
-
-\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssym
-\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssym
-\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssym
-\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssym
-\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssym
-\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssym
-\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssym
-\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssym
-\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssym
-\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssym
-\newcommand{\isasymA}{\isamath{\mathcal{A}}}
-\newcommand{\isasymB}{\isamath{\mathcal{B}}}
-\newcommand{\isasymC}{\isamath{\mathcal{C}}}
-\newcommand{\isasymD}{\isamath{\mathcal{D}}}
-\newcommand{\isasymE}{\isamath{\mathcal{E}}}
-\newcommand{\isasymF}{\isamath{\mathcal{F}}}
-\newcommand{\isasymG}{\isamath{\mathcal{G}}}
-\newcommand{\isasymH}{\isamath{\mathcal{H}}}
-\newcommand{\isasymI}{\isamath{\mathcal{I}}}
-\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
-\newcommand{\isasymK}{\isamath{\mathcal{K}}}
-\newcommand{\isasymL}{\isamath{\mathcal{L}}}
-\newcommand{\isasymM}{\isamath{\mathcal{M}}}
-\newcommand{\isasymN}{\isamath{\mathcal{N}}}
-\newcommand{\isasymO}{\isamath{\mathcal{O}}}
-\newcommand{\isasymP}{\isamath{\mathcal{P}}}
-\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
-\newcommand{\isasymR}{\isamath{\mathcal{R}}}
-\newcommand{\isasymS}{\isamath{\mathcal{S}}}
-\newcommand{\isasymT}{\isamath{\mathcal{T}}}
-\newcommand{\isasymU}{\isamath{\mathcal{U}}}
-\newcommand{\isasymV}{\isamath{\mathcal{V}}}
-\newcommand{\isasymW}{\isamath{\mathcal{W}}}
-\newcommand{\isasymX}{\isamath{\mathcal{X}}}
-\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
-\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
-\newcommand{\isasyma}{\isamath{\mathrm{a}}}
-\newcommand{\isasymb}{\isamath{\mathrm{b}}}
-\newcommand{\isasymc}{\isamath{\mathrm{c}}}
-\newcommand{\isasymd}{\isamath{\mathrm{d}}}
-\newcommand{\isasyme}{\isamath{\mathrm{e}}}
-\newcommand{\isasymf}{\isamath{\mathrm{f}}}
-\newcommand{\isasymg}{\isamath{\mathrm{g}}}
-\newcommand{\isasymh}{\isamath{\mathrm{h}}}
-\newcommand{\isasymi}{\isamath{\mathrm{i}}}
-\newcommand{\isasymj}{\isamath{\mathrm{j}}}
-\newcommand{\isasymk}{\isamath{\mathrm{k}}}
-\newcommand{\isasyml}{\isamath{\mathrm{l}}}
-\newcommand{\isasymm}{\isamath{\mathrm{m}}}
-\newcommand{\isasymn}{\isamath{\mathrm{n}}}
-\newcommand{\isasymo}{\isamath{\mathrm{o}}}
-\newcommand{\isasymp}{\isamath{\mathrm{p}}}
-\newcommand{\isasymq}{\isamath{\mathrm{q}}}
-\newcommand{\isasymr}{\isamath{\mathrm{r}}}
-\newcommand{\isasyms}{\isamath{\mathrm{s}}}
-\newcommand{\isasymt}{\isamath{\mathrm{t}}}
-\newcommand{\isasymu}{\isamath{\mathrm{u}}}
-\newcommand{\isasymv}{\isamath{\mathrm{v}}}
-\newcommand{\isasymw}{\isamath{\mathrm{w}}}
-\newcommand{\isasymx}{\isamath{\mathrm{x}}}
-\newcommand{\isasymy}{\isamath{\mathrm{y}}}
-\newcommand{\isasymz}{\isamath{\mathrm{z}}}
-\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
-\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
-\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
-\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
-\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
-\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
-\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
-\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
-\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
-\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
-\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
-\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
-\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
-\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
-\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
-\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
-\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
-\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
-\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
-\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
-\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
-\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
-\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
-\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
-\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
-\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
-\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
-\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
-\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
-\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
-\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
-\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
-\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
-\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
-\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
-\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
-\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
-\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
-\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
-\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
-\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
-\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
-\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
-\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
-\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
-\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
-\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
-\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
-\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
-\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
-\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
-\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
-\newcommand{\isasymalpha}{\isamath{\alpha}}
-\newcommand{\isasymbeta}{\isamath{\beta}}
-\newcommand{\isasymgamma}{\isamath{\gamma}}
-\newcommand{\isasymdelta}{\isamath{\delta}}
-\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
-\newcommand{\isasymzeta}{\isamath{\zeta}}
-\newcommand{\isasymeta}{\isamath{\eta}}
-\newcommand{\isasymtheta}{\isamath{\vartheta}}
-\newcommand{\isasymiota}{\isamath{\iota}}
-\newcommand{\isasymkappa}{\isamath{\kappa}}
-\newcommand{\isasymlambda}{\isamath{\lambda}}
-\newcommand{\isasymmu}{\isamath{\mu}}
-\newcommand{\isasymnu}{\isamath{\nu}}
-\newcommand{\isasymxi}{\isamath{\xi}}
-\newcommand{\isasympi}{\isamath{\pi}}
-\newcommand{\isasymrho}{\isamath{\varrho}}
-\newcommand{\isasymsigma}{\isamath{\sigma}}
-\newcommand{\isasymtau}{\isamath{\tau}}
-\newcommand{\isasymupsilon}{\isamath{\upsilon}}
-\newcommand{\isasymphi}{\isamath{\varphi}}
-\newcommand{\isasymchi}{\isamath{\chi}}
-\newcommand{\isasympsi}{\isamath{\psi}}
-\newcommand{\isasymomega}{\isamath{\omega}}
-\newcommand{\isasymGamma}{\isamath{\Gamma}}
-\newcommand{\isasymDelta}{\isamath{\Delta}}
-\newcommand{\isasymTheta}{\isamath{\Theta}}
-\newcommand{\isasymLambda}{\isamath{\Lambda}}
-\newcommand{\isasymXi}{\isamath{\Xi}}
-\newcommand{\isasymPi}{\isamath{\Pi}}
-\newcommand{\isasymSigma}{\isamath{\Sigma}}
-\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
-\newcommand{\isasymPhi}{\isamath{\Phi}}
-\newcommand{\isasymPsi}{\isamath{\Psi}}
-\newcommand{\isasymOmega}{\isamath{\Omega}}
-\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
-\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
-\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
-\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
-\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
-\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
-\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
-\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
-\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
-\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
-\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
-\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
-\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
-\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
-\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
-\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
-\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
-\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
-\newcommand{\isasymmapsto}{\isamath{\mapsto}}
-\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
-\newcommand{\isasymmidarrow}{\isamath{\relbar}}
-\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
-\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
-\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
-\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
-\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
-\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
-\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
-\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
-\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssym
-\newcommand{\isasymup}{\isamath{\uparrow}}
-\newcommand{\isasymUp}{\isamath{\Uparrow}}
-\newcommand{\isasymdown}{\isamath{\downarrow}}
-\newcommand{\isasymDown}{\isamath{\Downarrow}}
-\newcommand{\isasymupdown}{\isamath{\updownarrow}}
-\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
-\newcommand{\isasymlangle}{\isamath{\langle}}
-\newcommand{\isasymrangle}{\isamath{\rangle}}
-\newcommand{\isasymlceil}{\isamath{\lceil}}
-\newcommand{\isasymrceil}{\isamath{\rceil}}
-\newcommand{\isasymlfloor}{\isamath{\lfloor}}
-\newcommand{\isasymrfloor}{\isamath{\rfloor}}
-\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
-\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
-\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
-\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
-\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
-\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
-\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
-\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
-\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
-\newcommand{\isasymnot}{\isamath{\neg}}
-\newcommand{\isasymbottom}{\isamath{\bot}}
-\newcommand{\isasymtop}{\isamath{\top}}
-\newcommand{\isasymand}{\isamath{\wedge}}
-\newcommand{\isasymAnd}{\isamath{\bigwedge}}
-\newcommand{\isasymor}{\isamath{\vee}}
-\newcommand{\isasymOr}{\isamath{\bigvee}}
-\newcommand{\isasymforall}{\isamath{\forall\,}}
-\newcommand{\isasymexists}{\isamath{\exists\,}}
-\newcommand{\isasymbox}{\isamath{\Box}} %requires amssym
-\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssym
-\newcommand{\isasymturnstile}{\isamath{\vdash}}
-\newcommand{\isasymTurnstile}{\isamath{\models}}
-\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
-\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
-\newcommand{\isasymstileturn}{\isamath{\dashv}}
-\newcommand{\isasymsurd}{\isamath{\surd}}
-\newcommand{\isasymle}{\isamath{\le}}
-\newcommand{\isasymge}{\isamath{\ge}}
-\newcommand{\isasymlless}{\isamath{\ll}}
-\newcommand{\isasymggreater}{\isamath{\gg}}
-\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
-\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
-\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
-\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
-\newcommand{\isasymin}{\isamath{\in}}
-\newcommand{\isasymnotin}{\isamath{\notin}}
-\newcommand{\isasymsubset}{\isamath{\subset}}
-\newcommand{\isasymsupset}{\isamath{\supset}}
-\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
-\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
-\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
-\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssym
-\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
-\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
-\newcommand{\isasyminter}{\isamath{\cap}}
-\newcommand{\isasymInter}{\isamath{\bigcap\,}}
-\newcommand{\isasymunion}{\isamath{\cup}}
-\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
-\newcommand{\isasymsqunion}{\isamath{\sqcup}}
-\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
-\newcommand{\isasymsqinter}{\isamath{\sqcap}}
-\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires masmath
-\newcommand{\isasymuplus}{\isamath{\uplus}}
-\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
-\newcommand{\isasymnoteq}{\isamath{\not=}}
-\newcommand{\isasymsim}{\isamath{\sim}}
-\newcommand{\isasymdoteq}{\isamath{\doteq}}
-\newcommand{\isasymsimeq}{\isamath{\simeq}}
-\newcommand{\isasymapprox}{\isamath{\approx}}
-\newcommand{\isasymasymp}{\isamath{\asymp}}
-\newcommand{\isasymcong}{\isamath{\cong}}
-\newcommand{\isasymsmile}{\isamath{\smile}}
-\newcommand{\isasymequiv}{\isamath{\equiv}}
-\newcommand{\isasymfrown}{\isamath{\frown}}
-\newcommand{\isasympropto}{\isamath{\propto}}
-\newcommand{\isasymbowtie}{\isamath{\bowtie}}
-\newcommand{\isasymprec}{\isamath{\prec}}
-\newcommand{\isasymsucc}{\isamath{\succ}}
-\newcommand{\isasympreceq}{\isamath{\preceq}}
-\newcommand{\isasymsucceq}{\isamath{\succeq}}
-\newcommand{\isasymparallel}{\isamath{\parallel}}
-\newcommand{\isasymbar}{\isamath{\mid}}
-\newcommand{\isasymplusminus}{\isamath{\pm}}
-\newcommand{\isasymminusplus}{\isamath{\mp}}
-\newcommand{\isasymtimes}{\isamath{\times}}
-\newcommand{\isasymdiv}{\isamath{\div}}
-\newcommand{\isasymcdot}{\isamath{\cdot}}
-\newcommand{\isasymstar}{\isamath{\star}}
-\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
-\newcommand{\isasymcirc}{\isamath{\circ}}
-\newcommand{\isasymdagger}{\isamath{\dagger}}
-\newcommand{\isasymddagger}{\isamath{\ddagger}}
-\newcommand{\isasymlhd}{\isamath{\lhd}}
-\newcommand{\isasymrhd}{\isamath{\rhd}}
-\newcommand{\isasymunlhd}{\isamath{\unlhd}}
-\newcommand{\isasymunrhd}{\isamath{\unrhd}}
-\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
-\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
-\newcommand{\isasymtriangle}{\isamath{\triangle}}
-\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
-\newcommand{\isasymoplus}{\isamath{\oplus}}
-\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
-\newcommand{\isasymotimes}{\isamath{\otimes}}
-\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
-\newcommand{\isasymodot}{\isamath{\odot}}
-\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
-\newcommand{\isasymominus}{\isamath{\ominus}}
-\newcommand{\isasymoslash}{\isamath{\oslash}}
-\newcommand{\isasymdots}{\isamath{\dots}}
-\newcommand{\isasymcdots}{\isamath{\cdots}}
-\newcommand{\isasymSum}{\isamath{\sum\,}}
-\newcommand{\isasymProd}{\isamath{\prod\,}}
-\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
-\newcommand{\isasyminfinity}{\isamath{\infty}}
-\newcommand{\isasymintegral}{\isamath{\int\,}}
-\newcommand{\isasymointegral}{\isamath{\oint\,}}
-\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
-\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
-\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
-\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
-\newcommand{\isasymaleph}{\isamath{\aleph}}
-\newcommand{\isasymemptyset}{\isamath{\emptyset}}
-\newcommand{\isasymnabla}{\isamath{\nabla}}
-\newcommand{\isasympartial}{\isamath{\partial}}
-\newcommand{\isasymRe}{\isamath{\Re}}
-\newcommand{\isasymIm}{\isamath{\Im}}
-\newcommand{\isasymflat}{\isamath{\flat}}
-\newcommand{\isasymnatural}{\isamath{\natural}}
-\newcommand{\isasymsharp}{\isamath{\sharp}}
-\newcommand{\isasymangle}{\isamath{\angle}}
-\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
-\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
-\newcommand{\isasymhyphen}{\isatext{\rm-}}
-\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
-\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
-\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
-\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
-\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
-\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
-\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
-\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
-\newcommand{\isasymsection}{\isatext{\rm\S}}
-\newcommand{\isasymparagraph}{\isatext{\rm\P}}
-\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
-\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
-\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
-\newcommand{\isasympounds}{\isamath{\pounds}}
-\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
-\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
-\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
-\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
-\newcommand{\isasymamalg}{\isamath{\amalg}}
-\newcommand{\isasymmho}{\isamath{\mho}} %requires amssym
-\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssym
-\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssym
-\newcommand{\isasymwp}{\isamath{\wp}}
-\newcommand{\isasymwrong}{\isamath{\wr}}
-\newcommand{\isasymstruct}{\isamath{\diamond}}
-\newcommand{\isasymacute}{\isatext{\'\relax}}
-\newcommand{\isasymindex}{\isatext{\i}}
-\newcommand{\isasymdieresis}{\isatext{\"\relax}}
-\newcommand{\isasymcedilla}{\isatext{\c\relax}}
-\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
-\newcommand{\isasymspacespace}{\isamath{~~}}
--- a/doc-src/Locales/Locales/generated/pdfsetup.sty Fri Aug 19 22:44:36 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-%%
-%% Author: Markus Wenzel, TU Muenchen
-%%
-%% smart url or hyperref setup
-%%
-
-\@ifundefined{pdfoutput}
-{\usepackage{url}}
-{\usepackage{color}\definecolor{darkblue}{rgb}{0,0,0.5}
- \usepackage[pdftex,a4paper,colorlinks=true,linkcolor=darkblue,citecolor=darkblue,filecolor=darkblue,pagecolor=darkblue,urlcolor=darkblue]{hyperref}
- \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}
--- a/doc-src/Locales/Locales/generated/root.bib Fri Aug 19 22:44:36 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,154 +0,0 @@
-@phdthesis{Bailey1998,
- author = "Anthony Bailey",
- title = "The machine-checked literate formalisation of algebra in type theory",
- school = "University of Manchester",
- month = jan,
- year = 1998,
- available = { CB }
-}
-
-@phdthesis{Kammuller1999a,
- author = "Florian Kamm{\"u}ller",
- title = "Modular Reasoning in {Isabelle}",
- school = "University of Cambridge, Computer Laboratory",
- note = "Available as Technical Report No. 470.",
- month = aug,
- year = 1999,
- available = { CB }
-}
-
-% TYPES 98
-
-@inproceedings{Kammuller1999b,
- author = "Florian Kamm{\"u}ller",
- title = "Modular Structures as Dependent Types in {Isabelle}",
- pages = "121--132",
- crossref = "AltenkirchEtAl1999",
- available = { CB }
-}
-
-@proceedings{AltenkirchEtAl1999,
- editor = "Thorsten Altenkirch and Wolfgang Naraschewski and Bernhard Reus",
- title = "Types for Proofs and Programs: International Workshop, {TYPES} '98, {Kloster Irsee, Germany, March 27--31, 1998}, Selected Papers",
- booktitle = "TYPES '98",
- publisher = "Springer",
- series = "LNCS",
- number = 1657,
- year = 1999
-}
-% CADE-17
-
-@inproceedings{Kammuller2000,
- author = "Florian Kamm{\"u}ller",
- title = "Modular Reasoning in {Isabelle}",
- pages = "99--114",
- crossref = "McAllester2000",
- available = { CB }
-}
-
-@proceedings{McAllester2000,
- editor = "David McAllester",
- title = "17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17--20, 2000: Proceedings",
- booktitle = "CADE 17",
- publisher = "Springer",
- series = "LNCS",
- number = 1831,
- year = 2000
-}
-
-@book{NipkowEtAl2002,
- author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
- title = "{Isabelle/HOL}: A Proof Assistant for Higher-Order Logic",
- publisher = "Springer",
- series = "LNCS",
- number = 2283,
- year = 2002,
- available = { CB }
-}
-
-% TYPES 2002
-
-@inproceedings{Nipkow2003,
- author = "Tobias Nipkow",
- title = "Structured Proofs in {Isar/HOL}",
- pages = "259--278",
- crossref = "GeuversWiedijk2003"
-}
-
-@proceedings{GeuversWiedijk2003,
- editor = "H. Geuvers and F. Wiedijk",
- title = "Types for Proofs and Programs (TYPES 2002)",
- booktitle = "TYPES 2002",
- publisher = "Springer",
- series = "LNCS",
- number = 2646,
- year = 2003
-}
-
-@phdthesis{Wenzel2002a,
- author = "Markus Wenzel",
- title = "{Isabelle/Isar} --- a versatile environment for human-readable formal proof documents",
- school = "Technische Universit{\"a}t M{\"u}nchen",
- note = "Electronically published as http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html.",
- year = 2002
-}
-
-@unpublished{Wenzel2002b,
- author = "Markus Wenzel",
- title = "Using locales in {Isabelle/Isar}",
- note = "Part of the Isabelle2003 distribution, file src/HOL/ex/Locales.thy. Distribution of Isabelle available at http://isabelle.in.tum.de",
- year = 2002
-}
-
-@unpublished{Wenzel2003,
- author = "Markus Wenzel",
- title = "The {Isabelle/Isar} Reference Manual",
- note = "Part of the Isabelle2003 distribution, available at http://isabelle.in.tum.de",
- year = 2003
-}
-
-% TPHOLs 2003
-
-@inproceedings{Chrzaszcz2003,
- author = "Jacek Chrzaszcz",
- title = "Implementing Modules in the {Coq} System",
- pages = "270--286",
- crossref = "BasinWolff2003",
- available = { CB }
-}
-
-@proceedings{BasinWolff2003,
- editor = "David Basin and Burkhart Wolff",
- title = "Theorem proving in higher order logics: 16th International Conference, TPHOLs 2003, Rome, Italy, September 2003: proceedings",
- booktitle = "TPHOLs 2003",
- publisher = "Springer",
- series = "LNCS",
- number = 2758,
- year = 2003
-}
-
-@PhdThesis{Klein2003,
- author = "Gerwin Klein",
- title = "Verified Java Bytecode Verification",
- school = "Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen",
- year = 2003
-}
-
-% TACAS 2000
-
-@inproceedings{Aspinall2000,
- author = "David Aspinall",
- title = "Proof General: A Generic Tool for Proof Development",
- pages = "38--42",
- crossref = "GrafSchwartzbach2000"
-}
-
-@proceedings{GrafSchwartzbach2000,
- editor = {Susanne Graf and Michael I. Schwartzbach},
- title = {Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, Germany, March 25 -- April 2, 2000, Proceedings},
- booktitle = "TACAS 2000",
- publisher = {Springer},
- series = {LNCS},
- number = {1785},
- year = {2000},
-}
\ No newline at end of file
--- a/doc-src/Locales/Locales/generated/root.tex Fri Aug 19 22:44:36 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-\documentclass[leqno]{article}
-\usepackage{isabelle,isabellesym}
-
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{array}
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\isabellestyle{tt}
-%\renewcommand{\isacharunderscore}{\_}%
-% the latter is not necessary with \isabellestyle{tt}
-
-\begin{document}
-
-\title{Locales and Locale Expressions in Isabelle/Isar}
-\author{Clemens Ballarin \\
- Fakult\"at f\"ur Informatik \\ Technische Universit\"at M\"unchen \\
- 85748 Garching, Germany \\
- ballarin@in.tum.de}
-\date{}
-
-\maketitle
-
-\begin{abstract}
- Locales provide a module system for the Isabelle proof assistant.
- Recently, locales have been ported to the new Isar format for
- structured proofs. At the same time, they have been extended by
- locale expressions, a language for composing locale specifications,
- and by structures, which provide syntax for algebraic structures.
- The present paper presents both and is suitable as a tutorial to
- locales in Isar, because it covers both basics and recent
- extensions, and contains many examples.
-\end{abstract}
-
-%\tableofcontents
-
-\parindent 0pt\parskip 0.5ex
-
-% include generated text of all theories
-\input{session}
-
-\bibliographystyle{plain}
-\bibliography{root}
-
-\end{document}
--- a/doc-src/Locales/Locales/generated/session.tex Fri Aug 19 22:44:36 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-\input{Locales.tex}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/Locales/Makefile Fri Aug 19 22:44:36 2005 +0200
+++ b/doc-src/Locales/Makefile Fri Aug 19 22:50:20 2005 +0200
@@ -8,7 +8,7 @@
## paths
-TEXPATH = Locales/generated/:
+TEXPATH = Locales/document/:
## dependencies
@@ -16,10 +16,10 @@
NAME = locales
-FILES = Locales/generated/root.tex Locales/generated/root.bib \
- Locales/generated/session.tex Locales/generated/Locales.tex \
- Locales/generated/isabelle.sty Locales/generated/isabellesym.sty \
- Locales/generated/pdfsetup.sty
+FILES = Locales/document/root.tex Locales/document/root.bib \
+ Locales/document/session.tex Locales/document/Locales.tex \
+ Locales/document/isabelle.sty Locales/document/isabellesym.sty \
+ Locales/document/pdfsetup.sty
dvi: $(NAME).dvi