doc-src/IsarRef/hol.tex
author wenzelm
Sat Apr 01 20:21:39 2000 +0200 (2000-04-01)
changeset 8657 b9475dad85ed
parent 8547 93b8685d004b
child 8665 403c2985e65e
permissions -rw-r--r--
recdef: admit names/atts;
     1 
     2 \chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools}
     3 
     4 \section{Miscellaneous attributes}
     5 
     6 \indexisaratt{rulify}\indexisaratt{rulify-prems}
     7 \begin{matharray}{rcl}
     8   rulify & : & \isaratt \\
     9   rulify_prems & : & \isaratt \\
    10 \end{matharray}
    11 
    12 \begin{descr}
    13 
    14 \item [$rulify$] puts a theorem into object-rule form, replacing implication
    15   and universal quantification of HOL by the corresponding meta-logical
    16   connectives.  This is the same operation as performed by the
    17   \texttt{qed_spec_mp} ML function.
    18   
    19 \item [$rulify_prems$] is similar to $rulify$, but acts on the premises of a
    20   rule.
    21 
    22 \end{descr}
    23 
    24 
    25 \section{Primitive types}
    26 
    27 \indexisarcmd{typedecl}\indexisarcmd{typedef}
    28 \begin{matharray}{rcl}
    29   \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
    30   \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
    31 \end{matharray}
    32 
    33 \begin{rail}
    34   'typedecl' typespec infix? comment?
    35   ;
    36   'typedef' parname? typespec infix? \\ '=' term comment?
    37   ;
    38 \end{rail}
    39 
    40 \begin{descr}
    41 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
    42   $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
    43   also declares type arity $t :: (term, \dots, term) term$, making $t$ an
    44   actual HOL type constructor.
    45 \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
    46   non-emptiness of the set $A$.  After finishing the proof, the theory will be
    47   augmented by a Gordon/HOL-style type definition.  See \cite{isabelle-HOL}
    48   for more information.  Note that user-level theories usually do not directly
    49   refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
    50   packages such as $\isarkeyword{record}$ (see \S\ref{sec:record}) and
    51   $\isarkeyword{datatype}$ (see \S\ref{sec:datatype}).
    52 \end{descr}
    53 
    54 
    55 \section{Records}\label{sec:record}
    56 
    57 %FIXME record_split method
    58 \indexisarcmd{record}
    59 \begin{matharray}{rcl}
    60   \isarcmd{record} & : & \isartrans{theory}{theory} \\
    61 \end{matharray}
    62 
    63 \begin{rail}
    64   'record' typespec '=' (type '+')? (field +)
    65   ;
    66 
    67   field: name '::' type comment?
    68   ;
    69 \end{rail}
    70 
    71 \begin{descr}
    72 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
    73   defines extensible record type $(\vec\alpha)t$, derived from the optional
    74   parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
    75   See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
    76   simply-typed extensible records.
    77 \end{descr}
    78 
    79 
    80 \section{Datatypes}\label{sec:datatype}
    81 
    82 \indexisarcmd{datatype}\indexisarcmd{rep-datatype}
    83 \begin{matharray}{rcl}
    84   \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
    85   \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
    86 \end{matharray}
    87 
    88 \railalias{repdatatype}{rep\_datatype}
    89 \railterm{repdatatype}
    90 
    91 \begin{rail}
    92   'datatype' (parname? typespec infix? \\ '=' (constructor + '|') + 'and')
    93   ;
    94   repdatatype (name * ) \\ 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    95   ;
    96 
    97   constructor: name (type * ) mixfix? comment?
    98   ;
    99 \end{rail}
   100 
   101 \begin{descr}
   102 \item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
   103 \item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
   104   ones, generating the standard infrastructure of derived concepts (primitive
   105   recursion etc.).
   106 \end{descr}
   107 
   108 The induction and exhaustion theorems generated provide case names according
   109 to the constructors involved, while parameters are named after the types (see
   110 also \S\ref{sec:induct-method}).
   111 
   112 See \cite{isabelle-HOL} for more details on datatypes.  Note that the theory
   113 syntax above has been slightly simplified over the old version, usually
   114 requiring more quotes and less parentheses.  Apart from proper proof methods
   115 for case-analysis and induction, there are also emulations of ML tactics
   116 \texttt{case_tac}\indexisarmeth{case-tac} and
   117 \texttt{induct_tac}\indexisarmeth{induct-tac} available, with similar syntax
   118 as $subgoal_tac$, see \S\ref{sec:tactical-proof}.
   119 
   120 
   121 \section{Recursive functions}
   122 
   123 \indexisarcmd{primrec}\indexisarcmd{recdef}
   124 \begin{matharray}{rcl}
   125   \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
   126   \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
   127 %FIXME
   128 %  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
   129 \end{matharray}
   130 
   131 \begin{rail}
   132   'primrec' parname? (equation + )
   133   ;
   134   'recdef' name term (equation +) hints
   135   ;
   136 
   137   equation: thmdecl? prop comment?
   138   ;
   139   hints: ('congs' thmrefs)? ('simpset' name)?
   140   ;
   141 \end{rail}
   142 
   143 \begin{descr}
   144 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over
   145   datatypes.
   146 \item [$\isarkeyword{recdef}$] defines general well-founded recursive
   147   functions (using the TFL package).
   148 \end{descr}
   149 
   150 Both definitions accommodate reasoning proof by induction (cf.\ 
   151 \S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
   152 of the function definition) refers to a specific induction rule, with
   153 parameters named according to the user-specified equations.  Case names of
   154 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of
   155 $\isarkeyword{recdef}$ are numbered (starting from $1$).
   156 
   157 The equations provided by these packages may be referred later as theorem list
   158 $f\mathord.simps$, where $f$ is the (collective) name of the functions
   159 defined.  Individual equations may be named explicitly as well; note that for
   160 $\isarkeyword{recdef}$ each specification given by the user may result in
   161 several theorems.
   162 
   163 See \cite{isabelle-HOL} for further information on recursive function
   164 definitions in HOL.
   165 
   166 
   167 \section{(Co)Inductive sets}
   168 
   169 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases}
   170 \indexisaratt{mono}
   171 \begin{matharray}{rcl}
   172   \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
   173   \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
   174   mono & : & \isaratt \\
   175   \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
   176 \end{matharray}
   177 
   178 \railalias{condefs}{con\_defs}
   179 \railalias{indcases}{inductive\_cases}
   180 \railterm{condefs,indcases}
   181 
   182 \begin{rail}
   183   ('inductive' | 'coinductive') (term comment? +) \\
   184     'intrs' attributes? (thmdecl? prop comment? +) \\
   185     'monos' thmrefs comment? \\ condefs thmrefs comment?
   186   ;
   187   indcases thmdef? nameref ':' \\ (prop +) comment?
   188   ;
   189   'mono' (() | 'add' | 'del')
   190   ;
   191 \end{rail}
   192 
   193 \begin{descr}
   194 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
   195   (co)inductive sets from the given introduction rules.
   196 \item [$mono$] declares monotonicity rules.  These rule are involved in the
   197   automated monotonicity proof of $\isarkeyword{inductive}$.
   198 \item [$\isarkeyword{inductive_cases}$] creates instances of elimination rules
   199   of (co)inductive sets, solving obvious cases by simplification.
   200   
   201   The $cases$ proof method (see \S\ref{sec:induct-method}) provides a more
   202   direct way for reasoning by cases (including optional simplification).
   203   
   204   Unlike the \texttt{mk_cases} ML function exported with any inductive
   205   definition \cite{isabelle-HOL}, $\isarkeyword{inductive_cases}$ it does
   206   \emph{not} modify cases by simplification that are not solved completely
   207   anyway (e.g.\ due to contradictory assumptions).  Thus
   208   $\isarkeyword{inductive_cases}$ conforms to the way Isar proofs are
   209   conducted, rather than old-style tactic scripts.
   210 \end{descr}
   211 
   212 See \cite{isabelle-HOL} for further information on inductive definitions in
   213 HOL.
   214 
   215 
   216 \section{Proof by cases and induction}\label{sec:induct-method}
   217 
   218 \subsection{Proof methods}
   219 
   220 \indexisarmeth{cases}\indexisarmeth{induct}
   221 \begin{matharray}{rcl}
   222   cases & : & \isarmeth \\
   223   induct & : & \isarmeth \\
   224 \end{matharray}
   225 
   226 The $cases$ and $induct$ methods provide a uniform interface to case analysis
   227 and induction over datatypes, inductive sets, and recursive functions.  The
   228 corresponding rules may be specified and instantiated in a casual manner.
   229 Furthermore, these methods provide named local contexts that may be invoked
   230 via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
   231 \S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
   232 about large specifications.
   233 
   234 \begin{rail}
   235   'cases' ('simplified' ':')? term? rule?  ;
   236 
   237   'induct' ('stripped' ':')? (inst * 'and') rule?
   238   ;
   239 
   240   inst: (term +)
   241   ;
   242   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
   243   ;
   244 \end{rail}
   245 
   246 \begin{descr}
   247 \item [$cases~t~R$] applies method $rule$ with an appropriate case distinction
   248   theorem, instantiated to the subject $t$.  Symbolic case names are bound
   249   according to the rule's local contexts.
   250   
   251   The rule is determined as follows, according to the facts and arguments
   252   passed to the $cases$ method:
   253   \begin{matharray}{llll}
   254     \text{facts}    &       & \text{arguments} & \text{rule} \\\hline
   255                     & cases &           & \text{classical case split} \\
   256                     & cases & t         & \text{datatype exhaustion (type of $t$)} \\
   257     \edrv a \in A   & cases & \dots     & \text{inductive set elimination (of $A$)} \\
   258     \dots           & cases & \dots ~ R & \text{explicit rule $R$} \\
   259   \end{matharray}
   260 
   261   The $simplified$ option causes ``obvious cases'' of the rule to be solved
   262   beforehand, while the others are left unscathed.
   263   
   264 \item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
   265   induction rules, which are determined as follows:
   266   \begin{matharray}{llll}
   267     \text{facts}    &        & \text{arguments} & \text{rule} \\\hline
   268                     & induct & P ~ x ~ \dots & \text{datatype induction (type of $x$)} \\
   269     \edrv x \in A   & induct & \dots         & \text{set induction (of $A$)} \\
   270     \dots           & induct & \dots ~ R     & \text{explicit rule $R$} \\
   271   \end{matharray}
   272   
   273   Several instantiations may be given, each referring to some part of a mutual
   274   inductive definition or datatype --- only related partial induction rules
   275   may be used together, though.  Any of the lists of terms $P, x, \dots$
   276   refers to the \emph{suffix} of variables present in the induction rule.
   277   This enables the writer to specify only induction variables, or both
   278   predicates and variables, for example.
   279   
   280   The $stripped$ option causes implications and (bounded) universal
   281   quantifiers to be removed from each new subgoal emerging from the
   282   application of the induction rule.  This accommodates typical
   283   ``strengthening of induction'' predicates.
   284 \end{descr}
   285 
   286 Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
   287 determined by the instantiated rule \emph{before} it has been applied to the
   288 internal proof state.\footnote{As a general principle, Isar proof text may
   289   never refer to parts of proof states directly.} Thus proper use of symbolic
   290 cases usually require the rule to be instantiated fully, as far as the
   291 emerging local contexts and subgoals are concerned.  In particular, for
   292 induction both the predicates and variables have to be specified.  Otherwise
   293 the $\CASENAME$ command would refuse to invoke cases containing schematic
   294 variables.
   295 
   296 The $\isarkeyword{print_cases}$ command (\S\ref{sec:diag}) prints all named
   297 cases present in the current proof state.
   298 
   299 
   300 \subsection{Declaring rules}
   301 
   302 \indexisaratt{cases}\indexisaratt{induct}
   303 \begin{matharray}{rcl}
   304   cases & : & \isaratt \\
   305   induct & : & \isaratt \\
   306 \end{matharray}
   307 
   308 \begin{rail}
   309   'cases' spec
   310   ;
   311   'induct' spec
   312   ;
   313 
   314   spec: ('type' | 'set') ':' nameref
   315   ;
   316 \end{rail}
   317 
   318 The $cases$ and $induct$ attributes augment the corresponding context of rules
   319 for reasoning about inductive sets and types.  The standard rules are already
   320 declared by HOL definitional packages.  For special applications, these may be
   321 replaced manually by variant versions.
   322 
   323 Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to
   324 adjust names of cases and parameters of a rule.
   325 
   326 
   327 \section{Arithmetic}
   328 
   329 \indexisarmeth{arith}
   330 \begin{matharray}{rcl}
   331   arith & : & \isarmeth \\
   332 \end{matharray}
   333 
   334 \begin{rail}
   335   'arith' '!'?
   336   ;
   337 \end{rail}
   338 
   339 The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
   340 $real$).  Any current facts are inserted into the goal before running the
   341 procedure.  The ``!''~argument causes the full context of assumptions to be
   342 included as well.
   343 
   344 Note that a simpler (but faster) version of arithmetic reasoning is already
   345 performed by the Simplifier.
   346 
   347 
   348 %%% Local Variables: 
   349 %%% mode: latex
   350 %%% TeX-master: "isar-ref"
   351 %%% End: