# HG changeset patch # User paulson # Date 927023710 -7200 # Node ID 5f1ce866c4978719cb3cbd2773f436dd1231cf61 # Parent fb098775306cb9c2773d9e3aa5f2df00f5b1d355 locale documentation (from Florian) diff -r fb098775306c -r 5f1ce866c497 doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Tue May 18 12:34:42 1999 +0200 +++ b/doc-src/Ref/theories.tex Tue May 18 12:35:10 1999 +0200 @@ -3,7 +3,7 @@ \chapter{Theories, Terms and Types} \label{theories} \index{theories|(}\index{signatures|bold} -\index{reading!axioms|see{{\tt assume_ax}}} Theories organize the +\index{reading!axioms|see{\texttt{assume_ax}}} Theories organize the syntax, declarations and axioms of a mathematical development. They are built, starting from the {\Pure} or {\CPure} theory, by extending and merging existing theories. They have the \ML\ type @@ -54,7 +54,7 @@ $id@n$} makes $id$ a subclass of the existing classes $id@1\dots id@n$. This rules out cyclic class structures. Isabelle automatically computes the transitive closure of subclass hierarchies; it is not - necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d < + necessary to declare \texttt{c < e} in addition to \texttt{c < d} and \texttt{d < e}. \item[$default$] @@ -79,7 +79,7 @@ \item[$infix$] declares a type or constant to be an infix operator of priority $nat$ - associating to the left ({\tt infixl}) or right ({\tt infixr}). Only + associating to the left (\texttt{infixl}) or right (\texttt{infixr}). Only 2-place type constructors can have infix status; an example is {\tt ('a,'b)~"*"~(infixr~20)}, which may express binary product types. @@ -116,14 +116,14 @@ infix} status. \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf - binder} status. The declaration {\tt binder} $\cal Q$ $p$ causes + binder} status. The declaration \texttt{binder} $\cal Q$ $p$ causes ${\cal Q}\,x.F(x)$ to be treated like $f(F)$, where $p$ is the priority. \end{itemize} \item[$trans$] specifies syntactic translation rules (macros). There are three forms: - parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt + parse rules (\texttt{=>}), print rules (\texttt{<=}), and parse/print rules ({\tt ==}). \item[$rules$] @@ -178,7 +178,7 @@ \end{description} % Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix -declarations, translation rules and the {\tt ML} section in more detail. +declarations, translation rules and the \texttt{ML} section in more detail. \subsection{Definitions}\indexbold{definitions} @@ -314,6 +314,224 @@ hard to predict. Use this feature with care only. +\section{Locales} +\label{Locales} + +Locales \cite{kammueller-locales} are a concept of local proof contexts. They +are introduced as named syntactic objects within theories and can be +opened in any descendant theory. + +\subsection{Declaring Locales} + +A locale is declared in a theory section that starts with the +keyword \texttt{locale}. It consists typically of three parts, the +\texttt{fixes} part, the \texttt{assumes} part, and the \texttt{defines} part. +Appendix \ref{app:TheorySyntax} presents the full syntax. + +\subsubsection{Parts of Locales} + +The subsection introduced by the keyword \texttt{fixes} declares the locale +constants in a way that closely resembles a global \texttt{consts} +declaration. In particular, there may be an optional pretty printing syntax +for the locale constants. + +The subsequent \texttt{assumes} part specifies the locale rules. They are +defined like \texttt{rules}: by an identifier followed by the rule +given as a string. Locale rules admit the statement of local assumptions +about the locale constants. The \texttt{assumes} part is optional. Non-fixed +variables in locale rules are automatically bound by the universal quantifier +\texttt{!!} of the meta-logic. + +Finally, the \texttt{defines} part introduces the definitions that are +available in the locale. Locale constants declared in the \texttt{fixes} +section are defined using the meta-equality \texttt{==}. If the +locale constant is a functiond then its definition can (as usual) have +variables on the left-hand side acting as formal parameters; they are +considered as schematic variables and are automatically generalized by +universal quantification of the meta-logic. The right hand side of a +definition must not contain variables that are not already on the left hand +side. In so far locale definitions behave like theory level definitions. +However, the locale concept realizes \emph{dependent definitions}: any variable +that is fixed as a locale constant can occur on the right hand side of +definitions. For an illustration of these dependent definitions see the +occurrence of the locale constant \texttt{G} on the right hand side of the +definitions of the locale \texttt{group} below. Naturally, definitions can +already use the syntax of the locale constants in the \texttt{fixes} +subsection. The \texttt{defines} part is, as the \texttt{assumes} part, +optional. + +\subsubsection{Example for Definition} +The concrete syntax of locale definitions is demonstrated by example below. + +Locale \texttt{group} assumes the definition of groups in a theory +file\footnote{This and other examples are from \texttt{HOL/ex}.}. A locale +defining a convenient proof environment for group related proofs may be +added to the theory as follows: +\begin{ttbox} + locale group = + fixes + G :: "'a grouptype" + e :: "'a" + binop :: "'a => 'a => 'a" (infixr "#" 80) + inv :: "'a => 'a" ("i(_)" [90] 91) + assumes + Group_G "G: Group" + defines + e_def "e == unit G" + binop_def "x # y == bin_op G x y" + inv_def "i(x) == inverse G x" +\end{ttbox} + +\subsubsection{Polymorphism} + +In contrast to polymorphic definitions in theories, the use of the +same type variable for the declaration of different locale constants in the +fixes part means \emph{the same} type. In other words, the scope of the +polymorphic variables is extended over all constant declarations of a locale. +In the above example \texttt{'a} refers to the same type which is fixed inside +the locale. In an exported theorem (see \S\ref{sec:locale-export}) the +constructors of locale \texttt{group} are polymorphic, yet only simultaneously +instantiatable. + +\subsubsection{Nested Locales} + +A locale can be defined as the extension of a previously defined +locale. This operation of extension is optional and is syntactically +expressed as +\begin{ttbox} +locale foo = bar + ... +\end{ttbox} +The locale \texttt{foo} builds on the constants and syntax of the locale {\tt +bar}. That is, all contents of the locale \texttt{bar} can be used in +definitions and rules of the corresponding parts of the locale {\tt +foo}. Although locale \texttt{foo} assumes the \texttt{fixes} part of \texttt{bar} it +does not automatically subsume its rules and definitions. Normally, one +expects to use locale \texttt{foo} only if locale \texttt{bar} is already +active. These aspects of use and activation of locales are considered in the +subsequent section. + + +\subsection{Locale Scope} + +Locales are by default inactive, but they can be invoked. The list of +currently active locales is called \emph{scope}. The process of activating +them is called \emph{opening}; the reverse is \emph{closing}. + +\subsubsection{Scope} +The locale scope is part of each theory. It is a dynamic stack containing +all active locales at a certain point in an interactive session. +The scope lives until all locales are explicitly closed. At one time there +can be more than one locale open. The contents of these various active +locales are all visible in the scope. In case of nested locales for example, +the nesting is actually reflected to the scope, which contains the nested +locales as layers. To check the state of the scope during a development the +function \texttt{Print\_scope} may be used. It displays the names of all open +locales on the scope. The function \texttt{print\_locales} applied to a theory +displays all locales contained in that theory and in addition also the +current scope. + +The scope is manipulated by the commands for opening and closing of locales. + +\subsubsection{Opening} +Locales can be \emph{opened} at any point during a session where +we want to prove theorems concerning the locale. Opening a locale means +making its contents visible by pushing it onto the scope of the current +theory. Inside a scope of opened locales, theorems can use all definitions and +rules contained in the locales on the scope. The rules and definitions may +be accessed individually using the function \ttindex{thm}. This function is +applied to the names assigned to locale rules and definitions as +strings. The opening command is called \texttt{Open\_locale} and takes the +name of the locale to be opened as its argument. + +If one opens a locale \texttt{foo} that is defined by extension from locale +\texttt{bar}, the function \texttt{Open\_locale} checks if locale \texttt{bar} +is open. If so, then it just opens \texttt{foo}, if not, then it prints a +message and opens \texttt{bar} before opening \texttt{foo}. Naturally, this +carries on, if \texttt{bar} is again an extension. + +\subsubsection{Closing} + +\emph{Closing} means to cancel the last opened locale, pushing it out of the +scope. Theorems proved during the life cycle of this locale will be disabled, +unless they have been explicitly exported, as described below. However, when +the same locale is opened again these theorems may be used again as well, +provided that they were saved as theorems in the first place, using +\texttt{qed} or ML assignment. The command \texttt{Close\_locale} takes a +locale name as a string and checks if this locale is actually the topmost +locale on the scope. If this is the case, it removes this locale, otherwise +it prints a warning message and does not change the scope. + +\subsubsection{Export of Theorems} +\label{sec:locale-export} + +Export of theorems transports theorems out of the scope of locales. Locale +rules that have been used in the proof of an exported theorem inside the +locale are carried by the exported form of the theorem as its individual +meta-assumptions. The locale constants are universally quantified variables +in these theorems, hence such theorems can be instantiated individually. +Definitions become unfolded; locale constants that were merely used for +definitions vanish. Logically, exporting corresponds to a combined +application of introduction rules for implication and universal +quantification. Exporting forms a kind of normalization of theorems in a +locale scope. + +According to the possibility of nested locales there are two different forms +of export. The first one is realized by the function \texttt{export} that +exports theorems through all layers of opened locales of the scope. Hence, +the application of export to a theorem yields a theorem of the global level, +that is, the current theory context without any local assumptions or +definitions. + +When locales are nested we might want to export a theorem, not to the global +level of the current theory but just to the previous level. The other export +function, \texttt{Export}, transports theorems one level up in the scope; the +theorem still uses locale constants, definitions and rules of the locales +underneath. + +\subsection{Functions for Locales} +\label{Syntax} +\index{locales!functions} + +Here is a quick reference list of locale functions. +\begin{ttbox} + Open_locale : xstring -> unit + Close_locale : xstring -> unit + export : thm -> thm + Export : thm -> thm + thm : xstring -> thm + Print_scope : unit -> unit + print_locales: theory -> unit +\end{ttbox} +\begin{ttdescription} +\item[\ttindexbold{Open_locale} $xstring$] + opens the locale {\it xstring}, adding it to the scope of the theory of the + current context. If the opened locale is built by extension, the ancestors + are opened automatically. + +\item[\ttindexbold{Close_locale} $xstring$] eliminates the locale {\it + xstring} from the scope if it is the topmost item on it, otherwise it does + not change the scope and produces a warning. + +\item[\ttindexbold{export} $thm$] locale definitions become expanded in {\it + thm} and locale rules that were used in the proof of {\it thm} become part + of its individual assumptions. This normalization happens with respect to + \emph{all open locales} on the scope. + +\item[\ttindexbold{Export} $thm$] works like \texttt{export} but normalizes + theorems only up to the previous level of locales on the scope. + +\item[\ttindexbold{thm} $xstring$] applied to the name of a locale definition + or rule it returns the definition as a theorem. + +\item[\ttindexbold{Print_scope}()] prints the names of the locales in the + current scope of the current theory context. + +\item[\ttindexbold{print_locale} $theory$] prints all locales that are + contained in {\it theory} directly or indirectly. It also displays the + current scope similar to \texttt{Print\_scope}. +\end{ttdescription} + + \section{Basic operations on theories}\label{BasicOperationsOnTheories} \subsection{*Theory inclusion} @@ -524,8 +742,8 @@ \begin{ttdescription} \item[\ttindexbold{loose_bnos} $t$] returns the list of all dangling bound variable references. In - particular, {\tt Bound~0} is loose unless it is enclosed in an - abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in + particular, \texttt{Bound~0} is loose unless it is enclosed in an + abstraction. Similarly \texttt{Bound~1} is loose unless it is enclosed in at least two abstractions; if enclosed in just one, the list will contain the number 0. A well-formed term does not contain any loose variables. @@ -537,7 +755,7 @@ \item[\ttindexbold{abstract_over} $(v,t)$] forms the abstraction of~$t$ over~$v$, which may be any well-formed term. - It replaces every occurrence of \(v\) by a {\tt Bound} variable with the + It replaces every occurrence of \(v\) by a \texttt{Bound} variable with the correct index. \item[\ttindexbold{variant_abs} $(a,T,u)$] @@ -552,7 +770,7 @@ to renaming of bound variables. \begin{itemize} \item - Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible + Two constants, \texttt{Free}s, or \texttt{Var}s are \(\alpha\)-convertible if their names and types are equal. (Variables having the same name but different types are thus distinct. This confusing situation should be avoided!) @@ -573,7 +791,7 @@ A term $t$ can be {\bf certified} under a signature to ensure that every type in~$t$ is well-formed and every constant in~$t$ is a type instance of a constant declared in the signature. The term must be well-typed and its use -of bound variables must be well-formed. Meta-rules such as {\tt forall_elim} +of bound variables must be well-formed. Meta-rules such as \texttt{forall_elim} take certified terms as arguments. Certified terms belong to the abstract type \mltydx{cterm}. @@ -745,7 +963,7 @@ \end{ttdescription} A curious feature of {\ML} exceptions is that they are ordinary constructors. -The {\ML} type {\tt exn} is a datatype that can be extended at any time. (See +The {\ML} type \texttt{exn} is a datatype that can be extended at any time. (See my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially page~136.) The oracle mechanism takes advantage of this to allow an oracle to take any information whatever. @@ -766,7 +984,7 @@ solve the specified problem. \end{itemize} -A trivial example is provided in theory {\tt FOL/ex/IffOracle}. This +A trivial example is provided in theory \texttt{FOL/ex/IffOracle}. This oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with an even number of $P$s. @@ -779,20 +997,20 @@ exception IffOracleExn of int;\medskip fun mk_iff_oracle (sign, IffOracleExn n) = if n > 0 andalso n mod 2 = 0 - then Trueprop $ mk_iff n + then Trueprop \$ mk_iff n else raise IffOracleExn n; \end{ttbox} -Observe the function's two arguments, the signature {\tt sign} and the +Observe the function's two arguments, the signature \texttt{sign} and the exception given as a pattern. The function checks its argument for validity. If $n$ is positive and even then it creates a tautology containing $n$ occurrences of~$P$. Otherwise it signals error by raising its own exception (just by happy coincidence). Errors may be -signalled by other means, such as returning the theorem {\tt True}. +signalled by other means, such as returning the theorem \texttt{True}. Please ensure that the oracle's result is correctly typed; Isabelle will reject ill-typed theorems by raising a cryptic exception at top level. -The \texttt{oracle} section of {\tt IffOracle.thy} installs above +The \texttt{oracle} section of \texttt{IffOracle.thy} installs above \texttt{ML} function as follows: \begin{ttbox} IffOracle = FOL +\medskip diff -r fb098775306c -r 5f1ce866c497 doc-src/Ref/theory-syntax.tex --- a/doc-src/Ref/theory-syntax.tex Tue May 18 12:34:42 1999 +0200 +++ b/doc-src/Ref/theory-syntax.tex Tue May 18 12:35:10 1999 +0200 @@ -52,6 +52,7 @@ | axclass | instance | oracle + | locale | local | global | setup @@ -137,6 +138,22 @@ witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim) ; +locale : 'locale' name '=' ( () | name '+' ) localeBody + ; + +localeBody : localeConsts ( () | localeAsms ) ( () | localeDefs ) + ; + +localeConsts: ( 'fixes' ( ( (name '::' ( string | type )) ( () | '(' mixfix ')' ) ) + ) ) + ; + + +localeAsms: ( 'assumes' ( ( id string ) + ) ) + ; + +localeDefs: ( 'defines' ( ( id string ) +) ) + ; + oracle : 'oracle' name '=' name ;