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