doc-src/IsarRef/logics.tex
author wenzelm
Mon Mar 04 22:31:21 2002 +0100 (2002-03-04)
changeset 13016 c039b8ede204
parent 13014 3c1c493e6d93
child 13024 0461b281c2b5
permissions -rw-r--r--
tuned;
wenzelm@12621
     1
wenzelm@12621
     2
\chapter{Object-logic specific elements}\label{ch:logics}
wenzelm@12621
     3
wenzelm@12621
     4
\section{General logic setup}\label{sec:object-logic}
wenzelm@12621
     5
wenzelm@12621
     6
\indexisarcmd{judgment}
wenzelm@12621
     7
\indexisarmeth{atomize}\indexisaratt{atomize}
wenzelm@12621
     8
\indexisaratt{rule-format}\indexisaratt{rulify}
wenzelm@12621
     9
wenzelm@12621
    10
\begin{matharray}{rcl}
wenzelm@12621
    11
  \isarcmd{judgment} & : & \isartrans{theory}{theory} \\
wenzelm@12621
    12
  atomize & : & \isarmeth \\
wenzelm@12621
    13
  atomize & : & \isaratt \\
wenzelm@12621
    14
  rule_format & : & \isaratt \\
wenzelm@12621
    15
  rulify & : & \isaratt \\
wenzelm@12621
    16
\end{matharray}
wenzelm@12621
    17
wenzelm@12621
    18
The very starting point for any Isabelle object-logic is a ``truth judgment''
wenzelm@12621
    19
that links object-level statements to the meta-logic (with its minimal
wenzelm@12621
    20
language of $prop$ that covers universal quantification $\Forall$ and
wenzelm@12621
    21
implication $\Imp$).  Common object-logics are sufficiently expressive to
wenzelm@12621
    22
\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own
wenzelm@12621
    23
language.  This is useful in certain situations where a rule needs to be
wenzelm@12621
    24
viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x
wenzelm@12621
    25
\in A \Imp P(x)$ versus $\forall x \in A. P(x)$).
wenzelm@12621
    26
wenzelm@12621
    27
From the following language elements, only the $atomize$ method and
wenzelm@12621
    28
$rule_format$ attribute are occasionally required by end-users, the rest is
wenzelm@12621
    29
for those who need to setup their own object-logic.  In the latter case
wenzelm@12621
    30
existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
wenzelm@12621
    31
realistic examples.
wenzelm@12621
    32
wenzelm@12621
    33
Generic tools may refer to the information provided by object-logic
wenzelm@12621
    34
declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
wenzelm@12621
    35
Reasoner \S\ref{sec:classical}).
wenzelm@12621
    36
wenzelm@12621
    37
\begin{rail}
wenzelm@12621
    38
  'judgment' constdecl
wenzelm@12621
    39
  ;
wenzelm@13014
    40
  atomize ('(' 'full' ')')?
wenzelm@13014
    41
  ;
wenzelm@13014
    42
  ruleformat ('(' 'noasm' ')')?
wenzelm@12621
    43
  ;
wenzelm@12621
    44
\end{rail}
wenzelm@12621
    45
wenzelm@12621
    46
\begin{descr}
wenzelm@13014
    47
wenzelm@12621
    48
\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
wenzelm@12621
    49
  truth judgment of the current object-logic.  Its type $\sigma$ should
wenzelm@12621
    50
  specify a coercion of the category of object-level propositions to $prop$ of
wenzelm@12621
    51
  the Pure meta-logic; the mixfix annotation $syn$ would typically just link
wenzelm@12621
    52
  the object language (internally of syntactic category $logic$) with that of
wenzelm@12621
    53
  $prop$.  Only one $\isarkeyword{judgment}$ declaration may be given in any
wenzelm@12621
    54
  theory development.
wenzelm@13014
    55
wenzelm@12621
    56
\item [$atomize$] (as a method) rewrites any non-atomic premises of a
wenzelm@12621
    57
  sub-goal, using the meta-level equations declared via $atomize$ (as an
wenzelm@12621
    58
  attribute) beforehand.  As a result, heavily nested goals become amenable to
wenzelm@12621
    59
  fundamental operations such as resolution (cf.\ the $rule$ method) and
wenzelm@13014
    60
  proof-by-assumption (cf.\ $assumption$).  Giving the ``$(full)$'' option
wenzelm@13014
    61
  here means to turn the subgoal into an object-statement (if possible),
wenzelm@13014
    62
  including the outermost parameters and assumptions as well.
wenzelm@13014
    63
wenzelm@12621
    64
  A typical collection of $atomize$ rules for a particular object-logic would
wenzelm@12621
    65
  provide an internalization for each of the connectives of $\Forall$, $\Imp$,
wenzelm@12621
    66
  and $\equiv$.  Meta-level conjunction expressed in the manner of minimal
wenzelm@12621
    67
  higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$
wenzelm@12621
    68
  should be covered as well (this is particularly important for locales, see
wenzelm@12621
    69
  \S\ref{sec:locale}).
wenzelm@13014
    70
wenzelm@12621
    71
\item [$rule_format$] rewrites a theorem by the equalities declared as
wenzelm@12621
    72
  $rulify$ rules in the current object-logic.  By default, the result is fully
wenzelm@12621
    73
  normalized, including assumptions and conclusions at any depth.  The
wenzelm@12621
    74
  $no_asm$ option restricts the transformation to the conclusion of a rule.
wenzelm@13014
    75
wenzelm@12621
    76
  In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
wenzelm@12621
    77
  replace (bounded) universal quantification ($\forall$) and implication
wenzelm@12621
    78
  ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
wenzelm@12621
    79
wenzelm@12621
    80
\end{descr}
wenzelm@12621
    81
wenzelm@12621
    82
wenzelm@12621
    83
\section{HOL}
wenzelm@12621
    84
wenzelm@12621
    85
\subsection{Primitive types}\label{sec:typedef}
wenzelm@12621
    86
wenzelm@12621
    87
\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
wenzelm@12621
    88
\begin{matharray}{rcl}
wenzelm@12621
    89
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
wenzelm@12621
    90
  \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@12621
    91
\end{matharray}
wenzelm@12621
    92
wenzelm@12621
    93
\begin{rail}
wenzelm@12879
    94
  'typedecl' typespec infix?
wenzelm@12621
    95
  ;
wenzelm@13016
    96
  'typedef' parname? abstype '=' repset
wenzelm@13016
    97
  ;
wenzelm@13016
    98
wenzelm@13016
    99
  abstype: typespec infix?
wenzelm@13016
   100
  ;
wenzelm@13016
   101
  repset: term ('morphisms' name name)?
wenzelm@12621
   102
  ;
wenzelm@12621
   103
\end{rail}
wenzelm@12621
   104
wenzelm@12621
   105
\begin{descr}
wenzelm@13014
   106
  
wenzelm@12621
   107
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
wenzelm@12621
   108
  $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
wenzelm@12621
   109
  also declares type arity $t :: (term, \dots, term) term$, making $t$ an
wenzelm@12621
   110
  actual HOL type constructor.
wenzelm@13014
   111
  
wenzelm@12621
   112
\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
wenzelm@12621
   113
  non-emptiness of the set $A$.  After finishing the proof, the theory will be
wenzelm@13014
   114
  augmented by a Gordon/HOL-style type definition, which establishes a
wenzelm@13014
   115
  bijection between the representing set $A$ and the new type $t$.
wenzelm@13014
   116
  
wenzelm@13014
   117
  Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term
wenzelm@13016
   118
  constant) of the same name (an alternative base name may be given in
wenzelm@13016
   119
  parentheses).  The injection from type to set is called $Rep_t$, its inverse
wenzelm@13016
   120
  $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$
wenzelm@13016
   121
  declaration).
wenzelm@13016
   122
  
wenzelm@13016
   123
  Theorems $Rep_t$, $Rep_inverse$, and $Abs_inverse$ provide the most basic
wenzelm@13016
   124
  characterization as a corresponding injection/surjection pair (in both
wenzelm@13016
   125
  directions).  Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly
wenzelm@13016
   126
  more comfortable view on the injectivity part, suitable for automated proof
wenzelm@13016
   127
  tools (e.g.\ in $simp$ or $iff$ declarations).  Rules $Rep_t_cases$,
wenzelm@13016
   128
  $Rep_t_induct$, and $Abs_t_cases$, $Abs_t_induct$ provide alternative views
wenzelm@13016
   129
  on surjectivity; these are already declared as type or set rules for the
wenzelm@13016
   130
  generic $cases$ and $induct$ methods.
wenzelm@12621
   131
\end{descr}
wenzelm@12621
   132
wenzelm@13016
   133
Raw type declarations are rarely used in practice; the main application is
wenzelm@13014
   134
with experimental (or even axiomatic!) theory fragments.  Instead of primitive
wenzelm@13014
   135
HOL type definitions, user-level theories usually refer to higher-level
wenzelm@13014
   136
packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or
wenzelm@13014
   137
$\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
wenzelm@12621
   138
wenzelm@13014
   139
wenzelm@13014
   140
\subsection{Adhoc tuples}
wenzelm@12621
   141
wenzelm@12621
   142
\indexisarattof{HOL}{split-format}
wenzelm@12621
   143
\begin{matharray}{rcl}
wenzelm@12621
   144
  split_format^* & : & \isaratt \\
wenzelm@12621
   145
\end{matharray}
wenzelm@12621
   146
wenzelm@12621
   147
\railalias{splitformat}{split\_format}
wenzelm@12621
   148
\railterm{splitformat}
wenzelm@12621
   149
\railterm{complete}
wenzelm@12621
   150
wenzelm@12621
   151
\begin{rail}
wenzelm@12621
   152
  splitformat (((name * ) + 'and') | ('(' complete ')'))
wenzelm@12621
   153
  ;
wenzelm@12621
   154
\end{rail}
wenzelm@12621
   155
wenzelm@12621
   156
\begin{descr}
wenzelm@13014
   157
wenzelm@12621
   158
\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
wenzelm@12621
   159
  tuple types into canonical form as specified by the arguments given; $\vec
wenzelm@12621
   160
  p@i$ refers to occurrences in premise $i$ of the rule.  The
wenzelm@12621
   161
  $split_format~(complete)$ form causes \emph{all} arguments in function
wenzelm@12621
   162
  applications to be represented canonically according to their tuple type
wenzelm@12621
   163
  structure.
wenzelm@13014
   164
wenzelm@12621
   165
  Note that these operations tend to invent funny names for new local
wenzelm@12621
   166
  parameters to be introduced.
wenzelm@12621
   167
wenzelm@12621
   168
\end{descr}
wenzelm@12621
   169
wenzelm@12621
   170
wenzelm@13014
   171
\section{Records}\label{sec:hol-record}
wenzelm@13014
   172
wenzelm@13014
   173
In principle, records merely generalize the concept of tuples where components
wenzelm@13014
   174
may be addressed by labels instead of just position.  The logical
wenzelm@13014
   175
infrastructure of records in Isabelle/HOL is slightly more advanced, though,
wenzelm@13014
   176
supporting truly extensible record schemes.  This admits operations that are
wenzelm@13014
   177
polymorphic with respect to record extension, yielding ``object-oriented''
wenzelm@13014
   178
effects like (single) inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for
wenzelm@13014
   179
more details on object-oriented verification and record subtyping in HOL.
wenzelm@13014
   180
wenzelm@13014
   181
wenzelm@13014
   182
\subsection{Basic concepts}
wenzelm@13014
   183
wenzelm@13014
   184
Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the
wenzelm@13014
   185
level of terms and types.  The notation is as follows:
wenzelm@13014
   186
wenzelm@13014
   187
\begin{center}
wenzelm@13014
   188
\begin{tabular}{l|l|l}
wenzelm@13014
   189
  & record terms & record types \\ \hline
wenzelm@13014
   190
  fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
wenzelm@13014
   191
  schematic & $\record{x = a\fs y = b\fs \more = m}$ &
wenzelm@13014
   192
    $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
wenzelm@13014
   193
\end{tabular}
wenzelm@13014
   194
\end{center}
wenzelm@13014
   195
wenzelm@13014
   196
\noindent The ASCII representation of $\record{x = a}$ is \texttt{(| x = a |)}.
wenzelm@13014
   197
wenzelm@13014
   198
A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
wenzelm@13014
   199
$y$ of value $b$.  The corresponding type is $\record{x \ty A\fs y \ty B}$,
wenzelm@13014
   200
assuming that $a \ty A$ and $b \ty B$.
wenzelm@12621
   201
wenzelm@13014
   202
A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
wenzelm@13014
   203
$x$ and $y$ as before, but also possibly further fields as indicated by the
wenzelm@13014
   204
``$\more$'' notation (which is actually part of the syntax).  The improper
wenzelm@13014
   205
field ``$\more$'' of a record scheme is called the \emph{more part}.
wenzelm@13014
   206
Logically it is just a free variable, which is occasionally referred to as
wenzelm@13014
   207
\emph{row variable} in the literature.  The more part of a record scheme may
wenzelm@13014
   208
be instantiated by zero or more further components.  For example, the above
wenzelm@13014
   209
scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more =
wenzelm@13014
   210
  m'}$, where $m'$ refers to a different more part.  Fixed records are special
wenzelm@13014
   211
instances of record schemes, where ``$\more$'' is properly terminated by the
wenzelm@13014
   212
$() :: unit$ element.  Actually, $\record{x = a\fs y = b}$ is just an
wenzelm@13014
   213
abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
wenzelm@13014
   214
wenzelm@13014
   215
\medskip
wenzelm@12621
   216
wenzelm@13014
   217
Two key observations make extensible records in a simply typed language like
wenzelm@13014
   218
HOL feasible:
wenzelm@13014
   219
\begin{enumerate}
wenzelm@13014
   220
\item the more part is internalized, as a free term or type variable,
wenzelm@13014
   221
\item field names are externalized, they cannot be accessed within the logic
wenzelm@13014
   222
  as first-class values.
wenzelm@13014
   223
\end{enumerate}
wenzelm@13014
   224
wenzelm@13014
   225
\medskip
wenzelm@13014
   226
wenzelm@13014
   227
In Isabelle/HOL record types have to be defined explicitly, fixing their field
wenzelm@13014
   228
names and types, and their (optional) parent record (see
wenzelm@13014
   229
{\S}\ref{sec:hol-record-def}).  Afterwards, records may be formed using above
wenzelm@13014
   230
syntax, while obeying the canonical order of fields as given by their
wenzelm@13014
   231
declaration.  The record package provides several standard operations like
wenzelm@13014
   232
selectors and updates (see {\S}\ref{sec:hol-record-ops}).  The common setup
wenzelm@13014
   233
for various generic proof tools enable succinct reasoning patterns (see
wenzelm@13014
   234
{\S}\ref{sec:hol-record-thms}).  See also the Isabelle/HOL tutorial
wenzelm@13014
   235
\cite{isabelle-hol-book} for further instructions on using records in
wenzelm@13014
   236
practice.
wenzelm@13014
   237
wenzelm@13014
   238
wenzelm@13014
   239
\subsection{Record specifications}\label{sec:hol-record-def}
wenzelm@12621
   240
wenzelm@12621
   241
\indexisarcmdof{HOL}{record}
wenzelm@12621
   242
\begin{matharray}{rcl}
wenzelm@12621
   243
  \isarcmd{record} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   244
\end{matharray}
wenzelm@12621
   245
wenzelm@12621
   246
\begin{rail}
wenzelm@12621
   247
  'record' typespec '=' (type '+')? (constdecl +)
wenzelm@12621
   248
  ;
wenzelm@12621
   249
\end{rail}
wenzelm@12621
   250
wenzelm@12621
   251
\begin{descr}
wenzelm@12621
   252
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
wenzelm@12621
   253
  defines extensible record type $(\vec\alpha)t$, derived from the optional
wenzelm@12621
   254
  parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
wenzelm@13014
   255
wenzelm@13014
   256
  The type variables of $\tau$ and $\vec\sigma$ need to be covered by the
wenzelm@13014
   257
  (distinct) parameters $\vec\alpha$.  Type constructor $t$ has to be new,
wenzelm@13014
   258
  while $\tau$ needs to specify an instance of an existing record type.  At
wenzelm@13014
   259
  least one new field $\vec c$ has to be specified.  Basically, field names
wenzelm@13014
   260
  need to belong to a unique record.  This is not a real restriction in
wenzelm@13014
   261
  practice, since fields are qualified by the record name internally.
wenzelm@13014
   262
wenzelm@13014
   263
  The parent record specification $\tau$ is optional; if omitted $t$ becomes a
wenzelm@13014
   264
  root record.  The hierarchy of all records declared within a theory context
wenzelm@13014
   265
  forms a forest structure, i.e.\ a set of trees starting with a root record
wenzelm@13014
   266
  each.  There is no way to merge multiple parent records!
wenzelm@13014
   267
wenzelm@13014
   268
  For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the
wenzelm@13014
   269
  fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is
wenzelm@13014
   270
  $(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c
wenzelm@13014
   271
    \ty \vec\sigma\fs \more \ty \zeta}$.
wenzelm@13014
   272
wenzelm@12621
   273
\end{descr}
wenzelm@12621
   274
wenzelm@13014
   275
\subsection{Record operations}\label{sec:hol-record-ops}
wenzelm@13014
   276
wenzelm@13014
   277
Any record definition of the form presented above produces certain standard
wenzelm@13014
   278
operations.  Selectors and updates are provided for any field, including the
wenzelm@13014
   279
improper one ``$more$''.  There are also cumulative record constructor
wenzelm@13014
   280
functions.  To simplify the presentation below, we assume for now that
wenzelm@13014
   281
$(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$.
wenzelm@13014
   282
wenzelm@13014
   283
\medskip \textbf{Selectors} and \textbf{updates} are available for any field
wenzelm@13014
   284
(including ``$more$''):
wenzelm@13014
   285
\begin{matharray}{lll}
wenzelm@13014
   286
  c@i & \ty & \record{\vec c \ty \vec \sigma, \more \ty \zeta} \To \sigma@i \\
wenzelm@13014
   287
  c@i_update & \ty & \sigma@i \To \record{\vec c \ty \vec\sigma, \more \ty \zeta} \To
wenzelm@13014
   288
    \record{\vec c \ty \vec\sigma, \more \ty \zeta}
wenzelm@13014
   289
\end{matharray}
wenzelm@13014
   290
wenzelm@13014
   291
There is special syntax for application of updates: $r \, \record{x \asn a}$
wenzelm@13014
   292
abbreviates term $x_update \, a \, r$.  Further notation for repeated updates
wenzelm@13014
   293
is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z
wenzelm@13014
   294
  \asn c}$ may be written $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$.
wenzelm@13014
   295
Note that because of postfix notation the order of fields shown here is
wenzelm@13014
   296
reverse than in the actual term.  Since repeated updates are just function
wenzelm@13014
   297
applications, fields may be freely permuted in $\record{x \asn a\fs y \asn
wenzelm@13014
   298
  b\fs z \asn c}$, as far as logical equality is concerned.  Thus
wenzelm@13014
   299
commutativity of updates can be proven within the logic for any two fields,
wenzelm@13014
   300
but not as a general theorem: fields are not first-class values.
wenzelm@13014
   301
wenzelm@13014
   302
\medskip The \textbf{make} operation provides a cumulative record constructor
wenzelm@13014
   303
functions:
wenzelm@13014
   304
\begin{matharray}{lll}
wenzelm@13014
   305
  t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
wenzelm@13014
   306
\end{matharray}
wenzelm@13014
   307
wenzelm@13014
   308
\medskip We now reconsider the case of non-root records, which are derived of
wenzelm@13014
   309
some parent.  In general, the latter may depend on another parent as well,
wenzelm@13014
   310
resulting in a list of \emph{ancestor records}.  Appending the lists of fields
wenzelm@13014
   311
of all ancestors results in a certain field prefix.  The record package
wenzelm@13014
   312
automatically takes care of this by lifting operations over this context of
wenzelm@13014
   313
ancestor fields.  Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec
wenzelm@13014
   314
b \ty \vec\rho$, the above record operations will get the following types:
wenzelm@13014
   315
\begin{matharray}{lll}
wenzelm@13014
   316
  c@i & \ty & \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty
wenzelm@13014
   317
    \zeta} \To \sigma@i \\
wenzelm@13014
   318
  c@i_update & \ty & \sigma@i \To
wenzelm@13014
   319
    \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To
wenzelm@13014
   320
    \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
wenzelm@13014
   321
  t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To
wenzelm@13014
   322
    \record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\
wenzelm@13014
   323
\end{matharray}
wenzelm@13014
   324
\noindent
wenzelm@13014
   325
wenzelm@13014
   326
\medskip Some further operations address the extension aspect of a derived
wenzelm@13014
   327
record scheme specifically: $fields$ produces a record fragment consisting of
wenzelm@13014
   328
exactly the new fields introduced here (the result may serve as a more part
wenzelm@13014
   329
elsewhere); $extend$ takes a fixed record and adds a given more part;
wenzelm@13014
   330
$truncate$ restricts a record scheme to a fixed record.
wenzelm@13014
   331
wenzelm@13014
   332
\begin{matharray}{lll}
wenzelm@13014
   333
  t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
wenzelm@13014
   334
  t{\dtt}extend & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \To
wenzelm@13014
   335
    \zeta \To \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
wenzelm@13014
   336
  t{\dtt}truncate & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To
wenzelm@13014
   337
    \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\
wenzelm@13014
   338
\end{matharray}
wenzelm@13014
   339
wenzelm@13014
   340
\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ are actually coincide for root records.
wenzelm@13014
   341
wenzelm@13014
   342
wenzelm@13014
   343
\subsection{Derived rules and proof tools}\label{sec:hol-record-thms}
wenzelm@13014
   344
wenzelm@13014
   345
The record package proves several results internally, declaring these facts to
wenzelm@13014
   346
appropriate proof tools.  This enables users to reason about record structures
wenzelm@13014
   347
quite comfortably.  Assume that $t$ is a record type as specified above.
wenzelm@13014
   348
wenzelm@13014
   349
\begin{enumerate}
wenzelm@13014
   350
wenzelm@13014
   351
\item Standard conversions for selectors or updates applied to record
wenzelm@13014
   352
  constructor terms are made part of the default Simplifier context; thus
wenzelm@13014
   353
  proofs by reduction of basic operations merely require the $simp$ method
wenzelm@13014
   354
  without further arguments.  These rules are available as $t{\dtt}simps$.
wenzelm@13014
   355
wenzelm@13014
   356
\item Selectors applied to updated records are automatically reduced by an
wenzelm@13014
   357
  internal simplification procedure, which is also part of the default
wenzelm@13014
   358
  Simplifier context.
wenzelm@13014
   359
wenzelm@13014
   360
\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
wenzelm@13014
   361
  \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$
wenzelm@13014
   362
  rules.  These rules are available as $t{\dtt}iffs$.
wenzelm@13014
   363
wenzelm@13014
   364
\item The introduction rule for record equality analogous to $x~r = x~r' \Imp
wenzelm@13014
   365
  y~r = y~r' \Imp \dots \Imp r = r'$ is declared to the Simplifier, and as the
wenzelm@13014
   366
  basic rule context as ``$intro?$''.  The rule is called $t{\dtt}equality$.
wenzelm@13014
   367
wenzelm@13014
   368
\item Representations of arbitrary record expressions as canonical constructor
wenzelm@13014
   369
  terms are provided both in $cases$ and $induct$ format (cf.\ the generic
wenzelm@13014
   370
  proof methods of the same name, \S\ref{sec:cases-induct}).  Several
wenzelm@13014
   371
  variations are available, for fixed records, record schemes, more parts etc.
wenzelm@13014
   372
wenzelm@13014
   373
  The generic proof methods are sufficiently smart to pick the most sensible
wenzelm@13014
   374
  rule according to the type of the indicated record expression: users just
wenzelm@13014
   375
  need to apply something like ``$(cases r)$'' to a certain proof problem.
wenzelm@13014
   376
wenzelm@13014
   377
\item The derived record operations $t{\dtt}make$, $t{\dtt}fields$,
wenzelm@13014
   378
  $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but
wenzelm@13014
   379
  usually need to be expanded by hand, using the collective fact
wenzelm@13014
   380
  $t{\dtt}defs$.
wenzelm@13014
   381
wenzelm@13014
   382
\end{enumerate}
wenzelm@13014
   383
wenzelm@12621
   384
wenzelm@12621
   385
\subsection{Datatypes}\label{sec:hol-datatype}
wenzelm@12621
   386
wenzelm@12621
   387
\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
wenzelm@12621
   388
\begin{matharray}{rcl}
wenzelm@12621
   389
  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   390
  \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   391
\end{matharray}
wenzelm@12621
   392
wenzelm@12621
   393
\railalias{repdatatype}{rep\_datatype}
wenzelm@12621
   394
\railterm{repdatatype}
wenzelm@12621
   395
wenzelm@12621
   396
\begin{rail}
wenzelm@12621
   397
  'datatype' (dtspec + 'and')
wenzelm@12621
   398
  ;
wenzelm@12621
   399
  repdatatype (name * ) dtrules
wenzelm@12621
   400
  ;
wenzelm@12621
   401
wenzelm@12621
   402
  dtspec: parname? typespec infix? '=' (cons + '|')
wenzelm@12621
   403
  ;
wenzelm@12879
   404
  cons: name (type * ) mixfix?
wenzelm@12621
   405
  ;
wenzelm@12621
   406
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
wenzelm@12621
   407
\end{rail}
wenzelm@12621
   408
wenzelm@12621
   409
\begin{descr}
wenzelm@12621
   410
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
wenzelm@12621
   411
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
wenzelm@12621
   412
  ones, generating the standard infrastructure of derived concepts (primitive
wenzelm@12621
   413
  recursion etc.).
wenzelm@12621
   414
\end{descr}
wenzelm@12621
   415
wenzelm@12621
   416
The induction and exhaustion theorems generated provide case names according
wenzelm@12621
   417
to the constructors involved, while parameters are named after the types (see
wenzelm@12621
   418
also \S\ref{sec:cases-induct}).
wenzelm@12621
   419
wenzelm@13014
   420
See \cite{isabelle-HOL} for more details on datatypes, but beware of the
wenzelm@13014
   421
old-style theory syntax being used there!  Apart from proper proof methods for
wenzelm@13014
   422
case-analysis and induction, there are also emulations of ML tactics
wenzelm@12621
   423
\texttt{case_tac} and \texttt{induct_tac} available, see
wenzelm@13014
   424
\S\ref{sec:induct_tac}; these admit to refer directly to the internal
wenzelm@13014
   425
structure of subgoals (including internally bound parameters).
wenzelm@12621
   426
wenzelm@12621
   427
wenzelm@12621
   428
\subsection{Recursive functions}\label{sec:recursion}
wenzelm@12621
   429
wenzelm@12621
   430
\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
wenzelm@12621
   431
\begin{matharray}{rcl}
wenzelm@12621
   432
  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   433
  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   434
  \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
wenzelm@12621
   435
%FIXME
wenzelm@12621
   436
%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   437
\end{matharray}
wenzelm@12621
   438
wenzelm@12621
   439
\railalias{recdefsimp}{recdef\_simp}
wenzelm@12621
   440
\railterm{recdefsimp}
wenzelm@12621
   441
wenzelm@12621
   442
\railalias{recdefcong}{recdef\_cong}
wenzelm@12621
   443
\railterm{recdefcong}
wenzelm@12621
   444
wenzelm@12621
   445
\railalias{recdefwf}{recdef\_wf}
wenzelm@12621
   446
\railterm{recdefwf}
wenzelm@12621
   447
wenzelm@12621
   448
\railalias{recdeftc}{recdef\_tc}
wenzelm@12621
   449
\railterm{recdeftc}
wenzelm@12621
   450
wenzelm@12621
   451
\begin{rail}
wenzelm@12621
   452
  'primrec' parname? (equation + )
wenzelm@12621
   453
  ;
wenzelm@12879
   454
  'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?
wenzelm@12621
   455
  ;
wenzelm@12879
   456
  recdeftc thmdecl? tc
wenzelm@12621
   457
  ;
wenzelm@12621
   458
wenzelm@12879
   459
  equation: thmdecl? prop
wenzelm@12621
   460
  ;
wenzelm@12621
   461
  hints: '(' 'hints' (recdefmod * ) ')'
wenzelm@12621
   462
  ;
wenzelm@12621
   463
  recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
wenzelm@12621
   464
  ;
wenzelm@12621
   465
  tc: nameref ('(' nat ')')?
wenzelm@12621
   466
  ;
wenzelm@12621
   467
\end{rail}
wenzelm@12621
   468
wenzelm@12621
   469
\begin{descr}
wenzelm@12621
   470
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
wenzelm@13014
   471
  datatypes, see also \cite{isabelle-HOL} FIXME.
wenzelm@12621
   472
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
wenzelm@13014
   473
  functions (using the TFL package), see also \cite{isabelle-HOL} FIXME.  The
wenzelm@12621
   474
  $(permissive)$ option tells TFL to recover from failed proof attempts,
wenzelm@12621
   475
  returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
wenzelm@12621
   476
  $recdef_wf$ hints refer to auxiliary rules to be used in the internal
wenzelm@13014
   477
  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\
wenzelm@12621
   478
  \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
wenzelm@13014
   479
  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
wenzelm@12621
   480
  \S\ref{sec:classical}).
wenzelm@12621
   481
\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
wenzelm@12621
   482
  termination condition number $i$ (default $1$) as generated by a
wenzelm@12621
   483
  $\isarkeyword{recdef}$ definition of constant $c$.
wenzelm@13014
   484
wenzelm@12621
   485
  Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
wenzelm@12621
   486
  internal proofs without manual intervention.
wenzelm@12621
   487
\end{descr}
wenzelm@12621
   488
wenzelm@13014
   489
Both kinds of recursive definitions accommodate reasoning by induction (cf.\
wenzelm@12621
   490
\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
wenzelm@12621
   491
the function definition) refers to a specific induction rule, with parameters
wenzelm@12621
   492
named according to the user-specified equations.  Case names of
wenzelm@12621
   493
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
wenzelm@12621
   494
$\isarkeyword{recdef}$ are numbered (starting from $1$).
wenzelm@12621
   495
wenzelm@12621
   496
The equations provided by these packages may be referred later as theorem list
wenzelm@12621
   497
$f\mathord.simps$, where $f$ is the (collective) name of the functions
wenzelm@12621
   498
defined.  Individual equations may be named explicitly as well; note that for
wenzelm@12621
   499
$\isarkeyword{recdef}$ each specification given by the user may result in
wenzelm@12621
   500
several theorems.
wenzelm@12621
   501
wenzelm@12621
   502
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
wenzelm@12621
   503
the following attributes.
wenzelm@12621
   504
wenzelm@12621
   505
\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
wenzelm@12621
   506
\begin{matharray}{rcl}
wenzelm@12621
   507
  recdef_simp & : & \isaratt \\
wenzelm@12621
   508
  recdef_cong & : & \isaratt \\
wenzelm@12621
   509
  recdef_wf & : & \isaratt \\
wenzelm@12621
   510
\end{matharray}
wenzelm@12621
   511
wenzelm@12621
   512
\railalias{recdefsimp}{recdef\_simp}
wenzelm@12621
   513
\railterm{recdefsimp}
wenzelm@12621
   514
wenzelm@12621
   515
\railalias{recdefcong}{recdef\_cong}
wenzelm@12621
   516
\railterm{recdefcong}
wenzelm@12621
   517
wenzelm@12621
   518
\railalias{recdefwf}{recdef\_wf}
wenzelm@12621
   519
\railterm{recdefwf}
wenzelm@12621
   520
wenzelm@12621
   521
\begin{rail}
wenzelm@12621
   522
  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
wenzelm@12621
   523
  ;
wenzelm@12621
   524
\end{rail}
wenzelm@12621
   525
wenzelm@12621
   526
wenzelm@12621
   527
\subsection{(Co)Inductive sets}\label{sec:hol-inductive}
wenzelm@12621
   528
wenzelm@12621
   529
\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
wenzelm@12621
   530
\begin{matharray}{rcl}
wenzelm@12621
   531
  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   532
  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   533
  mono & : & \isaratt \\
wenzelm@12621
   534
\end{matharray}
wenzelm@12621
   535
wenzelm@12621
   536
\railalias{condefs}{con\_defs}
wenzelm@12621
   537
\railterm{condefs}
wenzelm@12621
   538
wenzelm@12621
   539
\begin{rail}
wenzelm@12621
   540
  ('inductive' | 'coinductive') sets intros monos?
wenzelm@12621
   541
  ;
wenzelm@12621
   542
  'mono' (() | 'add' | 'del')
wenzelm@12621
   543
  ;
wenzelm@12621
   544
wenzelm@12879
   545
  sets: (term +)
wenzelm@12621
   546
  ;
wenzelm@12879
   547
  intros: 'intros' (thmdecl? prop +)
wenzelm@12621
   548
  ;
wenzelm@12879
   549
  monos: 'monos' thmrefs
wenzelm@12621
   550
  ;
wenzelm@12621
   551
\end{rail}
wenzelm@12621
   552
wenzelm@12621
   553
\begin{descr}
wenzelm@12621
   554
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
wenzelm@12621
   555
  (co)inductive sets from the given introduction rules.
wenzelm@12621
   556
\item [$mono$] declares monotonicity rules.  These rule are involved in the
wenzelm@12621
   557
  automated monotonicity proof of $\isarkeyword{inductive}$.
wenzelm@12621
   558
\end{descr}
wenzelm@12621
   559
wenzelm@13014
   560
See \cite{isabelle-HOL} FIXME for further information on inductive definitions
wenzelm@13014
   561
in HOL.
wenzelm@12621
   562
wenzelm@12621
   563
wenzelm@12621
   564
\subsection{Arithmetic proof support}
wenzelm@12621
   565
wenzelm@12621
   566
\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
wenzelm@12621
   567
\begin{matharray}{rcl}
wenzelm@12621
   568
  arith & : & \isarmeth \\
wenzelm@12621
   569
  arith_split & : & \isaratt \\
wenzelm@12621
   570
\end{matharray}
wenzelm@12621
   571
wenzelm@12621
   572
\begin{rail}
wenzelm@12621
   573
  'arith' '!'?
wenzelm@12621
   574
  ;
wenzelm@12621
   575
\end{rail}
wenzelm@12621
   576
wenzelm@12621
   577
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
wenzelm@12621
   578
$real$).  Any current facts are inserted into the goal before running the
wenzelm@12621
   579
procedure.  The ``!''~argument causes the full context of assumptions to be
wenzelm@12621
   580
included.  The $arith_split$ attribute declares case split rules to be
wenzelm@12621
   581
expanded before the arithmetic procedure is invoked.
wenzelm@12621
   582
wenzelm@12621
   583
Note that a simpler (but faster) version of arithmetic reasoning is already
wenzelm@12621
   584
performed by the Simplifier.
wenzelm@12621
   585
wenzelm@12621
   586
wenzelm@12621
   587
\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
wenzelm@12621
   588
wenzelm@12621
   589
The following important tactical tools of Isabelle/HOL have been ported to
wenzelm@12621
   590
Isar.  These should be never used in proper proof texts!
wenzelm@12621
   591
wenzelm@12621
   592
\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
wenzelm@12621
   593
\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
wenzelm@12621
   594
\begin{matharray}{rcl}
wenzelm@12621
   595
  case_tac^* & : & \isarmeth \\
wenzelm@12621
   596
  induct_tac^* & : & \isarmeth \\
wenzelm@12621
   597
  ind_cases^* & : & \isarmeth \\
wenzelm@12621
   598
  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   599
\end{matharray}
wenzelm@12621
   600
wenzelm@12621
   601
\railalias{casetac}{case\_tac}
wenzelm@12621
   602
\railterm{casetac}
wenzelm@12621
   603
wenzelm@12621
   604
\railalias{inducttac}{induct\_tac}
wenzelm@12621
   605
\railterm{inducttac}
wenzelm@12621
   606
wenzelm@12621
   607
\railalias{indcases}{ind\_cases}
wenzelm@12621
   608
\railterm{indcases}
wenzelm@12621
   609
wenzelm@12621
   610
\railalias{inductivecases}{inductive\_cases}
wenzelm@12621
   611
\railterm{inductivecases}
wenzelm@12621
   612
wenzelm@12621
   613
\begin{rail}
wenzelm@12621
   614
  casetac goalspec? term rule?
wenzelm@12621
   615
  ;
wenzelm@12621
   616
  inducttac goalspec? (insts * 'and') rule?
wenzelm@12621
   617
  ;
wenzelm@12621
   618
  indcases (prop +)
wenzelm@12621
   619
  ;
wenzelm@13014
   620
  inductivecases (thmdecl? (prop +) + 'and')
wenzelm@12621
   621
  ;
wenzelm@12621
   622
wenzelm@12621
   623
  rule: ('rule' ':' thmref)
wenzelm@12621
   624
  ;
wenzelm@12621
   625
\end{rail}
wenzelm@12621
   626
wenzelm@12621
   627
\begin{descr}
wenzelm@12621
   628
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
wenzelm@12621
   629
  only (unless an alternative rule is given explicitly).  Furthermore,
wenzelm@12621
   630
  $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
wenzelm@12621
   631
  variables to be given as instantiation.  These tactic emulations feature
wenzelm@12621
   632
  both goal addressing and dynamic instantiation.  Note that named rule cases
wenzelm@12621
   633
  are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
wenzelm@12621
   634
  methods (see \S\ref{sec:cases-induct}).
wenzelm@13014
   635
wenzelm@12621
   636
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
wenzelm@12621
   637
  to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
wenzelm@12621
   638
  forward manner.
wenzelm@13014
   639
wenzelm@12621
   640
  While $ind_cases$ is a proof method to apply the result immediately as
wenzelm@12621
   641
  elimination rules, $\isarkeyword{inductive_cases}$ provides case split
wenzelm@12621
   642
  theorems at the theory level for later use,
wenzelm@12621
   643
\end{descr}
wenzelm@12621
   644
wenzelm@12621
   645
wenzelm@12621
   646
\section{HOLCF}
wenzelm@12621
   647
wenzelm@12621
   648
\subsection{Mixfix syntax for continuous operations}
wenzelm@12621
   649
wenzelm@12621
   650
\indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs}
wenzelm@12621
   651
wenzelm@12621
   652
\begin{matharray}{rcl}
wenzelm@12621
   653
  \isarcmd{consts} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   654
  \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   655
\end{matharray}
wenzelm@12621
   656
wenzelm@12621
   657
HOLCF provides a separate type for continuous functions $\alpha \rightarrow
wenzelm@12621
   658
\beta$, with an explicit application operator $f \cdot x$.  Isabelle mixfix
wenzelm@12621
   659
syntax normally refers directly to the pure meta-level function type $\alpha
wenzelm@12621
   660
\To \beta$, with application $f\,x$.
wenzelm@12621
   661
wenzelm@12621
   662
The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ have the same outer syntax as
wenzelm@12621
   663
the pure versions (cf.\ \S\ref{sec:consts}).  Internally, declarations
wenzelm@12621
   664
involving continuous function types are treated specifically, transforming the
wenzelm@12621
   665
syntax template accordingly and generating syntax translation rules for the
wenzelm@12621
   666
abstract and concrete representation of application.
wenzelm@12621
   667
wenzelm@12621
   668
The behavior for plain meta-level function types is unchanged.  Mixed
wenzelm@12621
   669
continuous and meta-level application is \emph{not} supported.
wenzelm@12621
   670
wenzelm@12621
   671
\subsection{Recursive domains}
wenzelm@12621
   672
wenzelm@12621
   673
\indexisarcmdof{HOLCF}{domain}
wenzelm@12621
   674
\begin{matharray}{rcl}
wenzelm@12621
   675
  \isarcmd{domain} & : & \isartrans{theory}{theory} \\
wenzelm@12621
   676
\end{matharray}
wenzelm@12621
   677
wenzelm@12621
   678
\begin{rail}
wenzelm@12621
   679
  'domain' parname? (dmspec + 'and')
wenzelm@12621
   680
  ;
wenzelm@12621
   681
wenzelm@12621
   682
  dmspec: typespec '=' (cons + '|')
wenzelm@12621
   683
  ;
wenzelm@12879
   684
  cons: name (type * ) mixfix?
wenzelm@12621
   685
  ;
wenzelm@12621
   686
  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
wenzelm@12621
   687
\end{rail}
wenzelm@12621
   688
wenzelm@13014
   689
Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
wenzelm@12621
   690
\S\ref{sec:hol-datatype}).  Mutual recursive is supported, but no nesting nor
wenzelm@12621
   691
arbitrary branching.  Domain constructors may be strict (default) or lazy, the
wenzelm@13014
   692
latter admits to introduce infinitary objects in the typical LCF manner (e.g.\
wenzelm@13014
   693
lazy lists).  See also \cite{MuellerNvOS99} for a general discussion of HOLCF
wenzelm@13014
   694
domains.
wenzelm@12621
   695
wenzelm@12621
   696
wenzelm@12621
   697
\section{ZF}
wenzelm@12621
   698
wenzelm@12621
   699
\subsection{Type checking}
wenzelm@12621
   700
wenzelm@12621
   701
FIXME
wenzelm@12621
   702
wenzelm@12621
   703
\subsection{Inductive sets and datatypes}
wenzelm@12621
   704
wenzelm@12621
   705
FIXME
wenzelm@12621
   706
wenzelm@12621
   707
wenzelm@13014
   708
%%% Local Variables:
wenzelm@12621
   709
%%% mode: latex
wenzelm@12621
   710
%%% TeX-master: "isar-ref"
wenzelm@13014
   711
%%% End: