locale documentation (from Florian)
authorpaulson
Tue May 18 12:35:10 1999 +0200 (1999-05-18)
changeset 66695f1ce866c497
parent 6668 fb098775306c
child 6670 4921b1f8ff92
locale documentation (from Florian)
doc-src/Ref/theories.tex
doc-src/Ref/theory-syntax.tex
     1.1 --- a/doc-src/Ref/theories.tex	Tue May 18 12:34:42 1999 +0200
     1.2 +++ b/doc-src/Ref/theories.tex	Tue May 18 12:35:10 1999 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  
     1.5  \chapter{Theories, Terms and Types} \label{theories}
     1.6  \index{theories|(}\index{signatures|bold}
     1.7 -\index{reading!axioms|see{{\tt assume_ax}}} Theories organize the
     1.8 +\index{reading!axioms|see{\texttt{assume_ax}}} Theories organize the
     1.9  syntax, declarations and axioms of a mathematical development.  They
    1.10  are built, starting from the {\Pure} or {\CPure} theory, by extending
    1.11  and merging existing theories.  They have the \ML\ type
    1.12 @@ -54,7 +54,7 @@
    1.13      $id@n$} makes $id$ a subclass of the existing classes $id@1\dots
    1.14    id@n$.  This rules out cyclic class structures.  Isabelle automatically
    1.15    computes the transitive closure of subclass hierarchies; it is not
    1.16 -  necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d <
    1.17 +  necessary to declare \texttt{c < e} in addition to \texttt{c < d} and \texttt{d <
    1.18      e}.
    1.19  
    1.20  \item[$default$]
    1.21 @@ -79,7 +79,7 @@
    1.22  
    1.23  \item[$infix$]
    1.24    declares a type or constant to be an infix operator of priority $nat$
    1.25 -  associating to the left ({\tt infixl}) or right ({\tt infixr}).  Only
    1.26 +  associating to the left (\texttt{infixl}) or right (\texttt{infixr}).  Only
    1.27    2-place type constructors can have infix status; an example is {\tt
    1.28    ('a,'b)~"*"~(infixr~20)}, which may express binary product types.
    1.29  
    1.30 @@ -116,14 +116,14 @@
    1.31      infix} status.
    1.32  
    1.33    \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf
    1.34 -    binder} status.  The declaration {\tt binder} $\cal Q$ $p$ causes
    1.35 +    binder} status.  The declaration \texttt{binder} $\cal Q$ $p$ causes
    1.36    ${\cal Q}\,x.F(x)$ to be treated
    1.37    like $f(F)$, where $p$ is the priority.
    1.38    \end{itemize}
    1.39  
    1.40  \item[$trans$]
    1.41    specifies syntactic translation rules (macros).  There are three forms:
    1.42 -  parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt
    1.43 +  parse rules (\texttt{=>}), print rules (\texttt{<=}), and parse/print rules ({\tt
    1.44    ==}).
    1.45  
    1.46  \item[$rules$]
    1.47 @@ -178,7 +178,7 @@
    1.48  \end{description}
    1.49  %
    1.50  Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
    1.51 -declarations, translation rules and the {\tt ML} section in more detail.
    1.52 +declarations, translation rules and the \texttt{ML} section in more detail.
    1.53  
    1.54  
    1.55  \subsection{Definitions}\indexbold{definitions}
    1.56 @@ -314,6 +314,224 @@
    1.57  hard to predict.  Use this feature with care only.
    1.58  
    1.59  
    1.60 +\section{Locales}
    1.61 +\label{Locales}
    1.62 +
    1.63 +Locales \cite{kammueller-locales} are a concept of local proof contexts.  They
    1.64 +are introduced as named syntactic objects within theories and can be
    1.65 +opened in any descendant theory.
    1.66 +
    1.67 +\subsection{Declaring Locales}
    1.68 +
    1.69 +A locale is declared in a theory section that starts with the
    1.70 +keyword \texttt{locale}.  It consists typically of three parts, the
    1.71 +\texttt{fixes} part, the \texttt{assumes} part, and the \texttt{defines} part.
    1.72 +Appendix \ref{app:TheorySyntax} presents the full syntax.
    1.73 +
    1.74 +\subsubsection{Parts of Locales}
    1.75 +
    1.76 +The subsection introduced by the keyword \texttt{fixes} declares the locale
    1.77 +constants in a way that closely resembles a global \texttt{consts}
    1.78 +declaration.  In particular, there may be an optional pretty printing syntax
    1.79 +for the locale constants.
    1.80 +
    1.81 +The subsequent \texttt{assumes} part specifies the locale rules.  They are
    1.82 +defined like \texttt{rules}: by an identifier followed by the rule
    1.83 +given as a string.  Locale rules admit the statement of local assumptions
    1.84 +about the locale constants.  The \texttt{assumes} part is optional.  Non-fixed
    1.85 +variables in locale rules are automatically bound by the universal quantifier
    1.86 +\texttt{!!} of the meta-logic.
    1.87 +
    1.88 +Finally, the \texttt{defines} part introduces the definitions that are
    1.89 +available in the locale.  Locale constants declared in the \texttt{fixes}
    1.90 +section are defined using the meta-equality \texttt{==}.  If the
    1.91 +locale constant is a functiond then its definition can (as usual) have
    1.92 +variables on the left-hand side acting as formal parameters; they are
    1.93 +considered as schematic variables and are automatically generalized by
    1.94 +universal quantification of the meta-logic.  The right hand side of a
    1.95 +definition must not contain variables that are not already on the left hand
    1.96 +side.  In so far locale definitions behave like theory level definitions.
    1.97 +However, the locale concept realizes \emph{dependent definitions}: any variable
    1.98 +that is fixed as a locale constant can occur on the right hand side of
    1.99 +definitions.  For an illustration of these dependent definitions see the
   1.100 +occurrence of the locale constant \texttt{G} on the right hand side of the
   1.101 +definitions of the locale \texttt{group} below.  Naturally, definitions can
   1.102 +already use the syntax of the locale constants in the \texttt{fixes}
   1.103 +subsection.  The \texttt{defines} part is, as the \texttt{assumes} part,
   1.104 +optional.
   1.105 +
   1.106 +\subsubsection{Example for Definition}
   1.107 +The concrete syntax of locale definitions is demonstrated by example below.
   1.108 +
   1.109 +Locale \texttt{group} assumes the definition of groups in a theory
   1.110 +file\footnote{This and other examples are from \texttt{HOL/ex}.}.  A locale
   1.111 +defining a convenient proof environment for group related proofs may be
   1.112 +added to the theory as follows:
   1.113 +\begin{ttbox}
   1.114 +  locale group =
   1.115 +    fixes 
   1.116 +      G         :: "'a grouptype"
   1.117 +      e         :: "'a"
   1.118 +      binop     :: "'a => 'a => 'a"        (infixr "#" 80)
   1.119 +      inv       :: "'a => 'a"              ("i(_)" [90] 91)
   1.120 +    assumes
   1.121 +      Group_G   "G: Group"
   1.122 +    defines
   1.123 +      e_def     "e == unit G"
   1.124 +      binop_def "x # y == bin_op G x y"
   1.125 +      inv_def   "i(x) == inverse G x"
   1.126 +\end{ttbox}
   1.127 +
   1.128 +\subsubsection{Polymorphism}
   1.129 +
   1.130 +In contrast to polymorphic definitions in theories, the use of the
   1.131 +same type variable for the declaration of different locale constants in the
   1.132 +fixes part means \emph{the same} type.  In other words, the scope of the
   1.133 +polymorphic variables is extended over all constant declarations of a locale.
   1.134 +In the above example \texttt{'a} refers to the same type which is fixed inside
   1.135 +the locale.  In an exported theorem (see \S\ref{sec:locale-export}) the
   1.136 +constructors of locale \texttt{group} are polymorphic, yet only simultaneously
   1.137 +instantiatable.
   1.138 +
   1.139 +\subsubsection{Nested Locales}
   1.140 +
   1.141 +A locale can be defined as the extension of a previously defined
   1.142 +locale.  This operation of extension is optional and is syntactically
   1.143 +expressed as 
   1.144 +\begin{ttbox}
   1.145 +locale foo = bar + ...
   1.146 +\end{ttbox}
   1.147 +The locale \texttt{foo} builds on the constants and syntax of the locale {\tt
   1.148 +bar}.  That is, all contents of the locale \texttt{bar} can be used in
   1.149 +definitions and rules of the corresponding parts of the locale {\tt
   1.150 +foo}.  Although locale \texttt{foo} assumes the \texttt{fixes} part of \texttt{bar} it
   1.151 +does not automatically subsume its rules and definitions.  Normally, one
   1.152 +expects to use locale \texttt{foo} only if locale \texttt{bar} is already
   1.153 +active.  These aspects of use and activation of locales are considered in the
   1.154 +subsequent section.
   1.155 +
   1.156 +
   1.157 +\subsection{Locale Scope}
   1.158 +
   1.159 +Locales are by default inactive, but they can be invoked.  The list of
   1.160 +currently active locales is called \emph{scope}.  The process of activating
   1.161 +them is called \emph{opening}; the reverse is \emph{closing}.
   1.162 +
   1.163 +\subsubsection{Scope}
   1.164 +The locale scope is part of each theory.  It is a dynamic stack containing
   1.165 +all active locales at a certain point in an interactive session.
   1.166 +The scope lives until all locales are explicitly closed.  At one time there
   1.167 +can be more than one locale open.  The contents of these various active
   1.168 +locales are all visible in the scope.  In case of nested locales for example,
   1.169 +the nesting is actually reflected to the scope, which contains the nested
   1.170 +locales as layers.  To check the state of the scope during a development the
   1.171 +function \texttt{Print\_scope} may be used.  It displays the names of all open
   1.172 +locales on the scope.  The function \texttt{print\_locales} applied to a theory
   1.173 +displays all locales contained in that theory and in addition also the
   1.174 +current scope.
   1.175 +
   1.176 +The scope is manipulated by the commands for opening and closing of locales. 
   1.177 +
   1.178 +\subsubsection{Opening}
   1.179 +Locales can be \emph{opened} at any point during a session where
   1.180 +we want to prove theorems concerning the locale.  Opening a locale means
   1.181 +making its contents visible by pushing it onto the scope of the current
   1.182 +theory.  Inside a scope of opened locales, theorems can use all definitions and
   1.183 +rules contained in the locales on the scope.  The rules and definitions may
   1.184 +be accessed individually using the function \ttindex{thm}.  This function is
   1.185 +applied to the names assigned to locale rules and definitions as
   1.186 +strings.  The opening command is called \texttt{Open\_locale} and takes the 
   1.187 +name of the locale to be opened as its argument.
   1.188 +
   1.189 +If one opens a locale \texttt{foo} that is defined by extension from locale
   1.190 +\texttt{bar}, the function \texttt{Open\_locale} checks if locale \texttt{bar}
   1.191 +is open.  If so, then it just opens \texttt{foo}, if not, then it prints a
   1.192 +message and opens \texttt{bar} before opening \texttt{foo}.  Naturally, this
   1.193 +carries on, if \texttt{bar} is again an extension.
   1.194 +
   1.195 +\subsubsection{Closing}
   1.196 +
   1.197 +\emph{Closing} means to cancel the last opened locale, pushing it out of the
   1.198 +scope.  Theorems proved during the life cycle of this locale will be disabled,
   1.199 +unless they have been explicitly exported, as described below.  However, when
   1.200 +the same locale is opened again these theorems may be used again as well,
   1.201 +provided that they were saved as theorems in the first place, using
   1.202 +\texttt{qed} or ML assignment.  The command \texttt{Close\_locale} takes a
   1.203 +locale name as a string and checks if this locale is actually the topmost
   1.204 +locale on the scope.  If this is the case, it removes this locale, otherwise
   1.205 +it prints a warning message and does not change the scope.
   1.206 +
   1.207 +\subsubsection{Export of Theorems}
   1.208 +\label{sec:locale-export}
   1.209 +
   1.210 +Export of theorems transports theorems out of the scope of locales.  Locale
   1.211 +rules that have been used in the proof of an exported theorem inside the
   1.212 +locale are carried by the exported form of the theorem as its individual
   1.213 +meta-assumptions.  The locale constants are universally quantified variables
   1.214 +in these theorems, hence such theorems can be instantiated individually.
   1.215 +Definitions become unfolded; locale constants that were merely used for
   1.216 +definitions vanish.  Logically, exporting corresponds to a combined
   1.217 +application of introduction rules for implication and universal
   1.218 +quantification.  Exporting forms a kind of normalization of theorems in a
   1.219 +locale scope.
   1.220 +
   1.221 +According to the possibility of nested locales there are two different forms
   1.222 +of export.  The first one is realized by the function \texttt{export} that
   1.223 +exports theorems through all layers of opened locales of the scope.  Hence,
   1.224 +the application of export to a theorem yields a theorem of the global level,
   1.225 +that is, the current theory context without any local assumptions or
   1.226 +definitions.
   1.227 +
   1.228 +When locales are nested we might want to export a theorem, not to the global
   1.229 +level of the current theory but just to the previous level.  The other export
   1.230 +function, \texttt{Export}, transports theorems one level up in the scope; the
   1.231 +theorem still uses locale constants, definitions and rules of the locales
   1.232 +underneath.
   1.233 +
   1.234 +\subsection{Functions for Locales}
   1.235 +\label{Syntax}
   1.236 +\index{locales!functions}
   1.237 +
   1.238 +Here is a quick reference list of locale functions.
   1.239 +\begin{ttbox}
   1.240 +  Open_locale  : xstring -> unit 
   1.241 +  Close_locale : xstring -> unit
   1.242 +  export       :     thm -> thm
   1.243 +  Export       :     thm -> thm
   1.244 +  thm          : xstring -> thm
   1.245 +  Print_scope  :    unit -> unit
   1.246 +  print_locales:  theory -> unit
   1.247 +\end{ttbox}
   1.248 +\begin{ttdescription}
   1.249 +\item[\ttindexbold{Open_locale} $xstring$] 
   1.250 +    opens the locale {\it xstring}, adding it to the scope of the theory of the
   1.251 +  current context.  If the opened locale is built by extension, the ancestors
   1.252 +  are opened automatically.
   1.253 +  
   1.254 +\item[\ttindexbold{Close_locale} $xstring$] eliminates the locale {\it
   1.255 +    xstring} from the scope if it is the topmost item on it, otherwise it does
   1.256 +  not change the scope and produces a warning.
   1.257 +
   1.258 +\item[\ttindexbold{export} $thm$] locale definitions become expanded in {\it
   1.259 +    thm} and locale rules that were used in the proof of {\it thm} become part
   1.260 +  of its individual assumptions.  This normalization happens with respect to
   1.261 +  \emph{all open locales} on the scope.
   1.262 +  
   1.263 +\item[\ttindexbold{Export} $thm$] works like \texttt{export} but normalizes
   1.264 +  theorems only up to the previous level of locales on the scope.
   1.265 +  
   1.266 +\item[\ttindexbold{thm} $xstring$] applied to the name of a locale definition
   1.267 +  or rule it returns the definition as a theorem.
   1.268 +  
   1.269 +\item[\ttindexbold{Print_scope}()] prints the names of the locales in the
   1.270 +  current scope of the current theory context.
   1.271 +  
   1.272 +\item[\ttindexbold{print_locale} $theory$] prints all locales that are
   1.273 +  contained in {\it theory} directly or indirectly.  It also displays the
   1.274 +  current scope similar to \texttt{Print\_scope}.
   1.275 +\end{ttdescription}
   1.276 +
   1.277 +
   1.278  \section{Basic operations on theories}\label{BasicOperationsOnTheories}
   1.279  
   1.280  \subsection{*Theory inclusion}
   1.281 @@ -524,8 +742,8 @@
   1.282  \begin{ttdescription}
   1.283  \item[\ttindexbold{loose_bnos} $t$]
   1.284    returns the list of all dangling bound variable references.  In
   1.285 -  particular, {\tt Bound~0} is loose unless it is enclosed in an
   1.286 -  abstraction.  Similarly {\tt Bound~1} is loose unless it is enclosed in
   1.287 +  particular, \texttt{Bound~0} is loose unless it is enclosed in an
   1.288 +  abstraction.  Similarly \texttt{Bound~1} is loose unless it is enclosed in
   1.289    at least two abstractions; if enclosed in just one, the list will contain
   1.290    the number 0.  A well-formed term does not contain any loose variables.
   1.291  
   1.292 @@ -537,7 +755,7 @@
   1.293  
   1.294  \item[\ttindexbold{abstract_over} $(v,t)$]
   1.295    forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
   1.296 -  It replaces every occurrence of \(v\) by a {\tt Bound} variable with the
   1.297 +  It replaces every occurrence of \(v\) by a \texttt{Bound} variable with the
   1.298    correct index.
   1.299  
   1.300  \item[\ttindexbold{variant_abs} $(a,T,u)$]
   1.301 @@ -552,7 +770,7 @@
   1.302    to renaming of bound variables.
   1.303  \begin{itemize}
   1.304    \item
   1.305 -    Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible
   1.306 +    Two constants, \texttt{Free}s, or \texttt{Var}s are \(\alpha\)-convertible
   1.307      if their names and types are equal.
   1.308      (Variables having the same name but different types are thus distinct.
   1.309      This confusing situation should be avoided!)
   1.310 @@ -573,7 +791,7 @@
   1.311  A term $t$ can be {\bf certified} under a signature to ensure that every type
   1.312  in~$t$ is well-formed and every constant in~$t$ is a type instance of a
   1.313  constant declared in the signature.  The term must be well-typed and its use
   1.314 -of bound variables must be well-formed.  Meta-rules such as {\tt forall_elim}
   1.315 +of bound variables must be well-formed.  Meta-rules such as \texttt{forall_elim}
   1.316  take certified terms as arguments.
   1.317  
   1.318  Certified terms belong to the abstract type \mltydx{cterm}.
   1.319 @@ -745,7 +963,7 @@
   1.320  \end{ttdescription}
   1.321  
   1.322  A curious feature of {\ML} exceptions is that they are ordinary constructors.
   1.323 -The {\ML} type {\tt exn} is a datatype that can be extended at any time.  (See
   1.324 +The {\ML} type \texttt{exn} is a datatype that can be extended at any time.  (See
   1.325  my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially
   1.326  page~136.)  The oracle mechanism takes advantage of this to allow an oracle to
   1.327  take any information whatever.
   1.328 @@ -766,7 +984,7 @@
   1.329    solve the specified problem.
   1.330  \end{itemize}
   1.331  
   1.332 -A trivial example is provided in theory {\tt FOL/ex/IffOracle}.  This
   1.333 +A trivial example is provided in theory \texttt{FOL/ex/IffOracle}.  This
   1.334  oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with
   1.335  an even number of $P$s.
   1.336  
   1.337 @@ -779,20 +997,20 @@
   1.338  exception IffOracleExn of int;\medskip
   1.339  fun mk_iff_oracle (sign, IffOracleExn n) =
   1.340    if n > 0 andalso n mod 2 = 0
   1.341 -  then Trueprop $ mk_iff n
   1.342 +  then Trueprop \$ mk_iff n
   1.343    else raise IffOracleExn n;
   1.344  \end{ttbox}
   1.345 -Observe the function's two arguments, the signature {\tt sign} and the
   1.346 +Observe the function's two arguments, the signature \texttt{sign} and the
   1.347  exception given as a pattern.  The function checks its argument for
   1.348  validity.  If $n$ is positive and even then it creates a tautology
   1.349  containing $n$ occurrences of~$P$.  Otherwise it signals error by
   1.350  raising its own exception (just by happy coincidence).  Errors may be
   1.351 -signalled by other means, such as returning the theorem {\tt True}.
   1.352 +signalled by other means, such as returning the theorem \texttt{True}.
   1.353  Please ensure that the oracle's result is correctly typed; Isabelle
   1.354  will reject ill-typed theorems by raising a cryptic exception at top
   1.355  level.
   1.356  
   1.357 -The \texttt{oracle} section of {\tt IffOracle.thy} installs above
   1.358 +The \texttt{oracle} section of \texttt{IffOracle.thy} installs above
   1.359  \texttt{ML} function as follows:
   1.360  \begin{ttbox}
   1.361  IffOracle = FOL +\medskip
     2.1 --- a/doc-src/Ref/theory-syntax.tex	Tue May 18 12:34:42 1999 +0200
     2.2 +++ b/doc-src/Ref/theory-syntax.tex	Tue May 18 12:35:10 1999 +0200
     2.3 @@ -52,6 +52,7 @@
     2.4          | axclass
     2.5          | instance
     2.6          | oracle
     2.7 +        | locale
     2.8          | local
     2.9          | global
    2.10          | setup
    2.11 @@ -137,6 +138,22 @@
    2.12  witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim)
    2.13          ;
    2.14  
    2.15 +locale : 'locale' name '=' ( () | name '+' ) localeBody
    2.16 +       ;
    2.17 +
    2.18 +localeBody : localeConsts ( () | localeAsms ) ( () | localeDefs )
    2.19 +       ;
    2.20 +
    2.21 +localeConsts: ( 'fixes' ( ( (name '::' ( string | type )) ( () | '(' mixfix ')' ) ) + ) )
    2.22 +       ;
    2.23 +
    2.24 +
    2.25 +localeAsms:    ( 'assumes' ( ( id string ) + ) )
    2.26 +       ;
    2.27 +
    2.28 +localeDefs:   ( 'defines' ( ( id string ) +) )
    2.29 +       ;
    2.30 +
    2.31  oracle : 'oracle' name '=' name
    2.32         ;
    2.33