# HG changeset patch # User ballarin # Date 1082108144 -7200 # Node ID 7b8d56b4ac60fdb119136e5efbddae3170f75e5f # Parent 6cf696e5ef7f052e9dd6e306810aeee23c55c10a Added Locales Tutorial. diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/IsaMakefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/IsaMakefile Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,33 @@ + +## targets + +default: Locales +images: +test: Locales + +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src +OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log +USEDIR = $(ISATOOL) usedir -i true -d "" -D generated + + +## Locales + +Locales: $(LOG)/HOL-Locales.gz + +HOL: + @cd $(SRC)/HOL; $(ISATOOL) make HOL + +$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Locales.thy + @$(USEDIR) $(OUT)/HOL Locales + + +## clean + +clean: + @rm -f $(LOG)/HOL-Locales.gz diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/Locales.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/Locales.thy Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,1173 @@ +(* + Title: Locales in Isabelle/Isar + Id: $Id$ + Author: Clemens Ballarin, started 31 January 2003 + Copyright (c) 2003 by Clemens Ballarin +*) + +(*<*) +theory Locales = Main: + +ML_setup {* print_mode := "type_brackets" :: !print_mode; *} +(*>*) + +section {* Overview *} + +text {* + 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} +*} + +section {* Locales: Beyond Proof Contexts *} + +text {* + 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. +*} + +section {* Simple Locales *} + +subsection {* Syntax and Terminology *} + +text {* + 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 (@{text "\"}), entailment + (@{text "\"}) and equality (@{text "\"}). Variables (not bound + variables) are sometimes preceded by a question mark. The logic is + typed. Type variables are denoted by @{text "'a"}, @{text "'b"} + etc., and @{text "\"} is the function type. Double brackets @{text + "\"} and @{text "\"} are used to abbreviate nested entailment. +*} + +subsection {* Parameters, Assumptions and Facts *} + +text {* + From a logical point of view a \emph{context} is a formula schema of + the form +\[ + @{text "\x\<^sub>1\x\<^sub>n. \ C\<^sub>1; \ ;C\<^sub>m \ \ \"} +\] + The variables $@{text "x\<^sub>1"}, \ldots, @{text "x\<^sub>n"}$ are + called \emph{parameters}, the premises $@{text "C\<^sub>1"}, \ldots, + @{text "C\<^sub>n"}$ \emph{assumptions}. A formula @{text "F"} + holds in this context if +\begin{equation} +\label{eq-fact-in-context} + @{text "\x\<^sub>1\x\<^sub>n. \ C\<^sub>1; \ ;C\<^sub>m \ \ F"} +\end{equation} + is valid. The formula is called a \emph{fact} of the context. + + A locale allows fixing the parameters @{text + "x\<^sub>1, \, x\<^sub>n"} and making the assumptions @{text + "C\<^sub>1, \, C\<^sub>m"}. This implicitly builds the context in + which the formula @{text "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. +*} + +locale semi = + fixes prod :: "['a, 'a] \ 'a" (infixl "\" 70) + assumes assoc: "(x \ y) \ z = x \ (y \ z)" + +text {* + The parameter @{term prod} has a + syntax annotation allowing the infix ``@{text "\"}'' in the + assumption of associativity. Parameters may have arbitrary mixfix + syntax, like constants. In the example, the type of @{term 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 + @{term "semi"} is +\[ + @{text "\prod. \ \x y z. prod (prod x y) z = prod x (prod y z) + \ \ \"} +\] + The locale can be extended to commutative semigroups. +*} + +locale comm_semi = semi + + assumes comm: "x \ y = y \ x" + +text {* + This locale \emph{imports} all elements of @{term "semi"}. The + latter locale is called the import of @{term "comm_semi"}. The + definition adds commutativity, hence its context is +\begin{align*% +} + @{text "\prod. \ "} & + @{text "\x y z. prod (prod x y) z = prod x (prod y z);"} \\ + & @{text "\x y. prod x y = prod y x \ \ \"} +\end{align*% +} + One may now derive facts --- for example, left-commutativity --- in + the context of @{term "comm_semi"} by specifying this locale as + target, and by referring to the names of the assumptions @{text + assoc} and @{text comm} in the proof. +*} + +theorem (in comm_semi) lcomm: + "x \ (y \ z) = y \ (x \ z)" +proof - + have "x \ (y \ z) = (x \ y) \ z" by (simp add: assoc) + also have "\ = (y \ x) \ z" by (simp add: comm) + also have "\ = y \ (x \ z)" by (simp add: assoc) + finally show ?thesis . +qed + +text {* + In this equational Isar proof, ``@{text "\"}'' refers to the + right hand side of the preceding equation. + After the proof is finished, the fact @{text "lcomm"} is added to + the locale @{term "comm_semi"}. This is done by adding a + \textbf{notes} element to the internal representation of the locale, + as explained the next section. +*} + +subsection {* Locale Predicates and the Internal Representation of + Locales *} + +text {* +\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 @{term semi} generates the \emph{locale + predicate} @{term semi} over the type of the parameter @{term prod}, + hence the predicate's type is @{typ "(['a, 'a] \ 'a) + \ bool"}. Its + definition is +\begin{equation} + \tag*{@{thm [source] semi_def}:} @{thm semi_def}. +\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 @{term comm_semi}. Two + predicates are defined. The predicate + @{term comm_semi_axioms} corresponds to the new assumptions and is + called \emph{delta predicate}, the locale + predicate @{term comm_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. +*} +(*<*) +ML_setup {* + val [comm_semi_ax1, comm_semi_ax2] = thms "comm_semi.axioms"; + bind_thm ("comm_semi_ax1", comm_semi_ax1); + bind_thm ("comm_semi_ax2", comm_semi_ax2); +*} +(*>*) +text {* + 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 @{text semi} and @{text comm_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 @{term semi}. + \begin{gather} + \tag*{@{thm [source] semi_def}:} @{thm semi_def} \\ + \tag*{@{thm [source] semi.intro}:} @{thm semi.intro} + \end{gather} + \hrule + \caption{Theorems for the locale predicate @{term "semi"}.} + \label{fig-theorems-semi} + \end{figure} + + \begin{figure}[h] + \hrule + \vspace{2ex} + Theorems generated for the predicate @{term "comm_semi_axioms"}. + \begin{gather} + \tag*{@{thm [source] comm_semi_axioms_def}:} @{thm + comm_semi_axioms_def} \\ + \tag*{@{thm [source] comm_semi_axioms.intro}:} @{thm + comm_semi_axioms.intro} + \end{gather} + Theorems generated for the predicate @{term "comm_semi"}. + \begin{gather} + \tag*{@{thm [source] comm_semi_def}:} @{thm + comm_semi_def} \\ + \tag*{@{thm [source] comm_semi.intro}:} @{thm + comm_semi.intro} \\ + \tag*{@{thm [source] comm_semi.axioms}:} \mbox{} \\ + \notag @{thm comm_semi_ax1} \\ + \notag @{thm comm_semi_ax2} + \end{gather} + \hrule + \caption{Theorems for the predicates @{term "comm_semi_axioms"} and + @{term "comm_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 @{term semi} is +\[ +\begin{array}{ll} + \textbf{fixes} & @{text prod} :: @{typ [quotes] "['a, 'a] \ 'a"} + (\textbf{infixl} @{text [quotes] "\"} 70) \\ + \textbf{assumes} & @{text [quotes] "semi prod"} \\ + \textbf{notes} & @{text assoc}: @{text [quotes] "?x \ ?y \ ?z = ?x \ (?y \ + ?z)"} +\end{array} +\] + and the internal representation of @{text [quotes] comm_semi} is +\begin{equation} +\label{eq-comm-semi} +\begin{array}{ll} + \textbf{fixes} & @{text prod} :: @{typ [quotes] "['a, 'a] \ 'a"} + ~(\textbf{infixl}~@{text [quotes] "\"}~70) \\ + \textbf{assumes} & @{text [quotes] "semi prod"} \\ + \textbf{notes} & @{text assoc}: @{text [quotes] "?x \ ?y \ ?z = ?x \ (?y \ + ?z)"} \\ + \textbf{assumes} & @{text [quotes] "comm_semi_axioms prod"} \\ + \textbf{notes} & @{text comm}: @{text [quotes] "?x \ ?y = ?y \ ?x"} \\ + \textbf{notes} & @{text lcomm}: @{text [quotes] "?x \ (?y \ ?z) = ?y \ (?x \ + ?z)"} +\end{array} +\end{equation} + The \textbf{notes} elements store facts of the + locales. The facts @{text assoc} and @{text comm} were added + during the declaration of the locales. They stem from assumptions, + which are trivially facts. The fact @{text 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 + @{text "[simp]"}. 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. +*} + +subsection {* Definitions *} + +text {* + 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 + @{text "p x\<^sub>1 \ x\<^sub>n \ t"} as an assumption, where @{term p} is a + parameter of the locale (possibly an imported parameter), and @{text + t} a term that may contain the @{text "x\<^sub>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 + @{term p} \emph{defined parameter}. +*} + +locale semi2 = semi + + fixes rprod (infixl "\" 70) + defines rprod_def: "rprod x y \ y \ x " + +text {* + This locale extends @{term semi} by a second binary operation @{text + [quotes] \} that is like @{text [quotes] \} but with + reversed arguments. The + definition of the locale generates the predicate @{term semi2}, + which is equivalent to @{text semi}, but no @{term "semi2_axioms"}. + The difference between \textbf{assumes} and \textbf{defines} lies in + the way parameters are treated on export. +*} + +subsection {* Export *} + +text {* + 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*{@{thm [source] semi.assoc}:} @{thm semi.assoc}. +\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 @{text [quotes] \} defined in the locale + @{text semi2} is also associative. +*} + +theorem (in semi2) r_assoc: "(x \ y) \ z = x \ (y \ z)" + by (simp only: rprod_def assoc) + +text {* + The exported fact is +\begin{equation} + \tag*{@{thm [source] semi2.r_assoc}:} @{thm semi2.r_assoc}. +\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 @{text "semi2.rprod_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.} +*} + +section {* Locale Expressions *} + +text {* + 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. +*} + +subsection {* Rename and Merge *} + +text {* + 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 @{text G} representing the group could be changed to + @{text R}. Besides of this stylistic use, renaming is important in + combination with merge. Both operations are used in the following + specification of semigroup homomorphisms. +*} + +locale semi_hom = comm_semi sum + comm_semi + + fixes hom + assumes hom: "hom (sum x y) = hom x \ hom y" + +text {* + This locale defines a context with three parameters @{text "sum"}, + @{text "prod"} and @{text "hom"}. Only the second parameter has + mixfix syntax. The first two are associative operations, + the first of type @{typ "['a, 'a] \ 'a"}, the second of + type @{typ "['b, 'b] \ '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 @{text "semi"} is + @{text "prod.assoc"}. Renaming parameters of a target also renames + the qualifier of facts. Hence, associativity of @{text "sum"} is + @{text "sum.assoc"}. Several parameters are separated by + underscores in qualifiers. For example, the full name of the fact + @{text "hom"} in the locale @{text "semi_hom"} is @{text + "sum_prod_hom.hom"}. + + The following example is quite artificial, it illustrates the use of + facts, though. +*} + +theorem (in semi_hom) "hom x \ (hom y \ hom z) = hom (sum x (sum y z))" +proof - + have "hom x \ (hom y \ hom z) = hom y \ (hom x \ hom z)" + by (simp add: prod.lcomm) + also have "\ = hom (sum y (sum x z))" by (simp add: hom) + also have "\ = hom (sum x (sum y z))" by (simp add: sum.lcomm) + finally show ?thesis . +qed + +text {* + Importing via a locale expression imports all facts of + the imported locales, hence both @{text "sum.lcomm"} and @{text + "prod.lcomm"} are + available in @{text "hom_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. +*} + +subsection {* Normal Forms *} + +text_raw {* +\label{sec-normal-forms} +\newcommand{\I}{\mathcal{I}} +\newcommand{\F}{\mathcal{F}} +\newcommand{\N}{\mathcal{N}} +\newcommand{\C}{\mathcal{C}} +\newcommand{\App}{\mathbin{\overline{@}}} +*} + +text {* + 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 @{text semi} and @{text + "comm_semi"}. We have $\I(@{text semi}) = \varepsilon$ and + $\I(@{text "comm_semi"}) = @{text semi}$, and the context fragments + are +\begin{align*% +} + \F(@{text semi}) & = \left[ +\begin{array}{ll} + \textbf{fixes} & @{text prod} :: @{typ [quotes] "['a, 'a] \ 'a"} + ~(\textbf{infixl}~@{text [quotes] "\"}~70) \\ + \textbf{assumes} & @{text [quotes] "semi prod"} \\ + \textbf{notes} & @{text assoc}: @{text [quotes]"?x \ ?y \ ?z = ?x \ (?y \ + ?z)"} +\end{array} \right], \\ + \F(@{text "comm_semi"}) & = \left[ +\begin{array}{ll} + \textbf{assumes} & @{text [quotes] "comm_semi_axioms prod"} \\ + \textbf{notes} & @{text comm}: @{text [quotes] "?x \ ?y = ?y \ ?x"} \\ + \textbf{notes} & @{text lcomm}: @{text [quotes] "?x \ (?y \ ?z) = ?y \ (?x \ + ?z)"} +\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} +*} + +subsection {* Examples *} + +text {* +\paragraph{Example 2.} + We obtain the context fragment $\C(@{text "comm_semi"})$ of the + locale @{text "comm_semi"}. First, the parameters are computed. +\begin{align*% +} + \pi(@{text "semi"}) & = [@{text prod}] \\ + \pi(@{text "comm_semi"}) & = \pi(@{text "semi"}) \App [] + = [@{text prod}] +\end{align*% +} + Next, the normal form of the locale expression + @{text "comm_semi"} is obtained. +\begin{align*% +} + \N(@{text "semi"}) & = [@{text semi} @{text prod}] \\ + \N(@{text "comm_semi"}) & = \N(@{text "semi"}) \App + [@{text "comm_semi prod"}] + = [@{text "semi prod"}, @{text "comm_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 @{text prod} --- for example, @{text "prod.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 @{text "comm_semi sum"} involves + renaming. Computing parameters yields $\pi(@{text "comm_semi sum"}) + = [@{text sum}]$, the normal form is +\begin{align*% +} + \N(@{text "comm_semi sum"}) & = + \N(@{text "comm_semi"})[@{text sum}/@{text prod}] = + [@{text "semi sum"}, @{text "comm_semi sum"}] +\end{align*% +} + and the list of context elements +\[ +\begin{array}{ll} + \textbf{fixes} & @{text sum} :: @{typ [quotes] "['a, 'a] \ 'a"} \\ + \textbf{assumes} & @{text [quotes] "semi sum"} \\ + \textbf{notes} & @{text sum.assoc}: @{text [quotes] "sum (sum ?x ?y) ?z + = sum ?x (sum ?y ?z)"} \\ + \textbf{assumes} & @{text [quotes] "comm_semi_axioms sum"} \\ + \textbf{notes} & @{text sum.comm}: @{text [quotes] "sum ?x ?y = sum + ?y ?x"} \\ + \textbf{notes} & @{text sum.lcomm}: @{text [quotes] "sum ?x (sum ?y ?z) + = sum ?y (sum ?x ?z)"} +\end{array} +\] + +\paragraph{Example 4.} + The context defined by the locale @{text "semi_hom"} involves + merging two copies of @{text "comm_semi"}. We obtain the parameter + list and normal form: +\begin{align*% +} + \pi(@{text "semi_hom"}) & = \pi(@{text "comm_semi sum"} + + @{text "comm_semi"}) \App [@{text hom}] \\ + & = (\pi(@{text "comm_semi sum"}) \App \pi(@{text "comm_semi"})) + \App [@{text hom}] \\ + & = ([@{text sum}] \App [@{text prod}]) \App [@{text hom}] + = [@{text sum}, @{text prod}, @{text hom}] \\ + \N(@{text "semi_hom"}) & = + \N(@{text "comm_semi sum"} + @{text "comm_semi"}) \App \\ + & \phantom{==} + [@{text "semi_hom sum prod hom"}] \\ + & = (\N(@{text "comm_semi sum"}) \App \N(@{text "comm_semi"})) \App \\ + & \phantom{==} + [@{text "semi_hom sum prod hom"}] \\ + & = ([@{text "semi sum"}, @{text "comm_semi sum"}] \App %\\ +% & \phantom{==} + [@{text "semi prod"}, @{text "comm_semi prod"}]) \App \\ + & \phantom{==} + [@{text "semi_hom sum prod hom"}] \\ + & = [@{text "semi sum"}, @{text "comm_semi sum"}, + @{text "semi prod"}, @{text "comm_semi prod"}, \\ + & \phantom{==} + @{text "semi_hom sum prod hom"}]. +\end{align*% +} + Hence $\C(@{text "semi_hom"})$, shown below, is again well-formed. +\[ +\begin{array}{ll} + \textbf{fixes} & @{text sum} :: @{typ [quotes] "['a, 'a] \ 'a"} \\ + \textbf{assumes} & @{text [quotes] "semi sum"} \\ + \textbf{notes} & @{text sum.assoc}: @{text [quotes] "sum (sum ?x ?y) ?z + = sum ?x (sum ?y ?z)"} \\ + \textbf{assumes} & @{text [quotes] "comm_semi_axioms sum"} \\ + \textbf{notes} & @{text sum.comm}: @{text [quotes] "sum ?x ?y = sum ?y ?x"} \\ + \textbf{notes} & @{text sum.lcomm}: @{text [quotes] "sum ?x (sum ?y ?z) + = sum ?y (sum ?x ?z)"} \\ + \textbf{fixes} & @{text prod} :: @{typ [quotes] "['b, 'b] \ 'b"} + ~(\textbf{infixl}~@{text [quotes] "\"}~70) \\ + \textbf{assumes} & @{text [quotes] "semi prod"} \\ + \textbf{notes} & @{text prod.assoc}: @{text [quotes] "?x \ ?y \ ?z = ?x \ (?y \ + ?z)"} \\ + \textbf{assumes} & @{text [quotes] "comm_semi_axioms prod"} \\ + \textbf{notes} & @{text prod.comm}: @{text [quotes] "?x \ ?y = ?y \ ?x"} \\ + \textbf{notes} & @{text prod.lcomm}: @{text [quotes] "?x \ (?y \ ?z) = ?y \ (?x \ + ?z)"} \\ + \textbf{fixes} & @{text hom} :: @{typ [quotes] "'a \ 'b"} \\ + \textbf{assumes} & @{text [quotes] "semi_hom_axioms sum"} \\ + \textbf{notes} & @{text "sum_prod_hom.hom"}: + @{text "hom (sum x y) = hom x \ 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. +*} + +locale monad = + fixes prod :: "['a, 'a] \ 'a" (infixl "\" 70) and one :: 'a ("\" 100) + assumes l_one: "\ \ x = x" and r_one: "x \ \ = x" + +text {* + Monoids are both semigroups and monads and one would want to + specify them as locale expression @{text "semi + monad"}. + Unfortunately, this expression is not well-formed. Its normal form +\begin{align*% +} + \N(@{text "monad"}) & = [@{text "monad prod"}] \\ + \N(@{text "semi"}+@{text "monad"}) & = + \N(@{text "semi"}) \App \N(@{text "monad"}) + = [@{text "semi prod"}, @{text "monad prod"}] +\end{align*% +} + leads to a list containing the context element +\[ + \textbf{fixes}~@{text prod} :: @{typ [quotes] "['a, 'a] \ 'a"} + ~(\textbf{infixl}~@{text [quotes] "\"}~70) +\] + twice and thus violating the first criterion of well-formedness. To + avoid this problem, one can + introduce a new locale @{text 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 @{text magma}. +*} + +locale magma = fixes prod (infixl "\" 70) + +locale semi' = magma + assumes assoc: "(x \ y) \ z = x \ (y \ z)" +locale monad' = magma + fixes one ("\" 100) + assumes l_one: "\ \ x = x" and r_one: "x \ \ = x" + +text {* + Normalisation now yields +\begin{align*% +} + \N(@{text "semi' + monad'"}) & = + \N(@{text "semi'"}) \App \N(@{text "monad'"}) \\ + & = (\N(@{text magma}) \App [@{text "semi' prod"}]) \App + (\N(@{text magma}) \App [@{text "monad' prod"}]) \\ + & = [@{text "magma prod"}, @{text "semi' prod"}] \App + [@{text "magma prod"}, @{text "monad' prod"}]) \\ + & = [@{text "magma prod"}, @{text "semi' prod"}, + @{text "monad' prod"}] +\end{align*% +} + where the second occurrence of @{text "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 @{term 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} @{text "x_"} +\end{center} + The use of the internal variable @{text "x_"} + enforces that the parameter is renamed before being used, because + internal variables may not occur in the input syntax. +*} + +subsection {* Includes *} + +text {* +\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. +*} + +theorem lcomm2: + includes comm_semi shows "x \ (y \ z) = y \ (x \ z)" +proof - + have "x \ (y \ z) = (x \ y) \ z" by (simp add: assoc) + also have "\ = (y \ x) \ z" by (simp add: comm) + also have "\ = y \ (x \ z)" by (simp add: assoc) + finally show ?thesis . +qed + +text {* + This proof is identical to the proof of @{text lcomm}. The use of + \textbf{includes} provides the same context and facts as when using + @{term comm_semi} as target. On the other hand, @{thm [source] + lcomm2} is not added as a fact to the locale @{term comm_semi}, but + is directly visible in the theory. The theorem is +\[ + @{thm lcomm2}. +\] + 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. +*} + +section {* Structures *} + +text {* +\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 @{text "'a semi_type"} be a not further specified type that + represents semigroups over the carrier type @{typ "'a"}. Let @{text + "s_op"} be an operation that maps an object of @{text "'a semi_type"} to + a binary operation. +*} + +typedecl 'a semi_type +consts s_op :: "['a semi_type, 'a, 'a] \ 'a" (infixl "\\" 70) + +text {* + Although @{text "s_op"} is a ternary operation, it is declared + infix. The syntax annotation contains the token @{text \} + (\verb.\.), 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: +*} + +locale comm_semi' = + fixes G :: "'a semi_type" (structure) + assumes assoc: "(x \ y) \ z = x \ (y \ z)" and comm: "x \ y = y \ x" + +text {* + Here @{text "x \ y"} is equivalent to @{text "x \\<^sub>1 y"} and + abbreviates @{term "s_op G x y"}. A specification of homomorphisms + requires a second structural parameter. +*} + +locale semi'_hom = comm_semi' + comm_semi' H + + fixes hom + assumes hom: "hom (x \ y) = hom x \\<^sub>2 hom y" + +text {* + The parameter @{text H} is defined in the second \textbf{fixes} + element of $\C(@{term "semi'_comm"})$. Hence @{text "\\<^sub>2"} + abbreviates @{term "s_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. *} + +record 'a semi = prod :: "['a, 'a] \ 'a" (infixl "\\" 70) + +text {* + This declares the types @{typ "'a semi"} and @{typ "('a, 'b) + semi_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. +*} + +locale semi_w_records = struct G + + assumes assoc: "(x \ y) \ z = x \ (y \ z)" + +text {* + The type @{typ "('a, 'b) semi_scheme"} is inferred for the parameter @{term + G}. Using subtyping on records, the specification can be extended + to groups easily. +*} + +record 'a group = "'a semi" + + one :: "'a" ("l\" 100) + inv :: "'a \ 'a" ("inv\ _" [81] 80) +locale group_w_records = semi_w_records + + assumes l_one: "l \ x = x" and l_inv: "inv x \ x = l" + +text {* + Finally, the predefined locale +\begin{center} + \textbf{locale} \textit{struct} = \textbf{fixes} @{text "S_"} + \textbf{(structure)}. +\end{center} + is analogous to @{text "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. +*} + +section {* Conclusions and Outlook *} + +text {* + 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 +(*>*) \ No newline at end of file diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/ROOT.ML Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,6 @@ +(* + no_document use_thy "ThisTheory"; + use_thy "ThatTheory"; +*) + +use_thy "Locales"; diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/document/root.bib Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,154 @@ +@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 diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/document/root.tex Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,48 @@ +\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} diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/generated/Locales.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/generated/Locales.tex Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,1221 @@ +% +\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.\.), 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: diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/generated/isabelle.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/generated/isabelle.sty Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,168 @@ +%% +%% Author: Markus Wenzel, TU Muenchen +%% License: GPL (GNU GENERAL PUBLIC LICENSE) +%% +%% 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}% +} diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/generated/isabellesym.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/generated/isabellesym.sty Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,354 @@ +%% +%% Author: Markus Wenzel, TU Muenchen +%% License: GPL (GNU GENERAL PUBLIC LICENSE) +%% +%% 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{~~}} diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/generated/pdfsetup.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/generated/pdfsetup.sty Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,12 @@ +%% +%% Author: Markus Wenzel, TU Muenchen +%% License: GPL (GNU GENERAL PUBLIC LICENSE) +%% +%% 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}}{}} diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/generated/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/generated/root.bib Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,154 @@ +@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 diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/generated/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/generated/root.tex Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,48 @@ +\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} diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Locales/generated/session.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Locales/generated/session.tex Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,6 @@ +\input{Locales.tex} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/Makefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/Makefile Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,40 @@ +# +# $Id$ +# + +## targets + +default: dvi + +## paths + +TEXPATH = Locales/generated/: + +## dependencies + +include ../Makefile.in + +NAME = locales + +FILES = locales.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 + +dvi: $(NAME).dvi + +$(NAME).dvi: $(FILES) + env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME) + env BIBINPUTS=$(TEXPATH) $(BIBTEX) $(NAME) + env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME) + env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME) + env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME) + +pdf: $(NAME).pdf + +$(NAME).pdf: $(FILES) + env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME) + env BIBINPUTS=$(TEXPATH) $(BIBTEX) $(NAME) + env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME) + env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME) + env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME) diff -r 6cf696e5ef7f -r 7b8d56b4ac60 doc-src/Locales/locales.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Locales/locales.tex Fri Apr 16 11:35:44 2004 +0200 @@ -0,0 +1,48 @@ +\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}