doc-src/IsarRef/hol.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 9642 d8d1f70024bd
child 9751 1287787744a7
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
     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} and \texttt{induct_tac} available, see
   117 \S\ref{sec:induct_tac}.
   118 
   119 
   120 \section{Recursive functions}
   121 
   122 \indexisarcmd{primrec}\indexisarcmd{recdef}
   123 \begin{matharray}{rcl}
   124   \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
   125   \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
   126 %FIXME
   127 %  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
   128 \end{matharray}
   129 
   130 \begin{rail}
   131   'primrec' parname? (equation + )
   132   ;
   133   'recdef' name term (equation +) hints
   134   ;
   135 
   136   equation: thmdecl? prop comment?
   137   ;
   138   hints: ('congs' thmrefs)?
   139   ;
   140 \end{rail}
   141 
   142 \begin{descr}
   143 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over
   144   datatypes.
   145 \item [$\isarkeyword{recdef}$] defines general well-founded recursive
   146   functions (using the TFL package).
   147 \end{descr}
   148 
   149 Both definitions accommodate reasoning proof by induction (cf.\ 
   150 \S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
   151 of the function definition) refers to a specific induction rule, with
   152 parameters named according to the user-specified equations.  Case names of
   153 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of
   154 $\isarkeyword{recdef}$ are numbered (starting from $1$).
   155 
   156 The equations provided by these packages may be referred later as theorem list
   157 $f\mathord.simps$, where $f$ is the (collective) name of the functions
   158 defined.  Individual equations may be named explicitly as well; note that for
   159 $\isarkeyword{recdef}$ each specification given by the user may result in
   160 several theorems.
   161 
   162 See \cite{isabelle-HOL} for further information on recursive function
   163 definitions in HOL.
   164 
   165 
   166 \section{(Co)Inductive sets}
   167 
   168 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono}
   169 \begin{matharray}{rcl}
   170   \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
   171   \isarcmd{coinductive}^* & : & \isartrans{theory}{theory} \\
   172   mono & : & \isaratt \\
   173 \end{matharray}
   174 
   175 \railalias{condefs}{con\_defs}
   176 \railterm{condefs}
   177 
   178 \begin{rail}
   179   ('inductive' | 'coinductive') (term comment? +) \\
   180     'intros' attributes? (thmdecl? prop comment? +) \\
   181     'monos' thmrefs comment? \\ condefs thmrefs comment?
   182   ;
   183   'mono' (() | 'add' | 'del')
   184   ;
   185 \end{rail}
   186 
   187 \begin{descr}
   188 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
   189   (co)inductive sets from the given introduction rules.
   190 \item [$mono$] declares monotonicity rules.  These rule are involved in the
   191   automated monotonicity proof of $\isarkeyword{inductive}$.
   192 \end{descr}
   193 
   194 See \cite{isabelle-HOL} for further information on inductive definitions in
   195 HOL.
   196 
   197 
   198 \section{Proof by cases and induction}\label{sec:induct-method}
   199 
   200 \subsection{Proof methods}\label{sec:induct-method-proper}
   201 
   202 \indexisarmeth{cases}\indexisarmeth{induct}
   203 \begin{matharray}{rcl}
   204   cases & : & \isarmeth \\
   205   induct & : & \isarmeth \\
   206 \end{matharray}
   207 
   208 The $cases$ and $induct$ methods provide a uniform interface to case analysis
   209 and induction over datatypes, inductive sets, and recursive functions.  The
   210 corresponding rules may be specified and instantiated in a casual manner.
   211 Furthermore, these methods provide named local contexts that may be invoked
   212 via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
   213 \S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
   214 about large specifications.
   215 
   216 \begin{rail}
   217   'cases' ('(simplified)')? ('(open)')? \\ (insts * 'and') rule?  ;
   218 
   219   'induct' ('(stripped)')? ('(open)')? \\ (insts * 'and') rule?
   220   ;
   221 
   222   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
   223   ;
   224 \end{rail}
   225 
   226 \begin{descr}
   227 \item [$cases~insts~R$] applies method $rule$ with an appropriate case
   228   distinction theorem, instantiated to the subjects $insts$.  Symbolic case
   229   names are bound according to the rule's local contexts.
   230   
   231   The rule is determined as follows, according to the facts and arguments
   232   passed to the $cases$ method:
   233   \begin{matharray}{llll}
   234     \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
   235                     & cases &           & \Text{classical case split} \\
   236                     & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
   237     \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
   238     \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
   239   \end{matharray}
   240   
   241   Several instantiations may be given, referring to the \emph{suffix} of
   242   premises of the case rule; within each premise, the \emph{prefix} of
   243   variables is instantiated.  In most situations, only a single term needs to
   244   be specified; this refers to the first variable of the last premise (it is
   245   usually the same for all cases).
   246 
   247   The $simplified$ option causes ``obvious cases'' of the rule to be solved
   248   beforehand, while the others are left unscathed.
   249   
   250   The $open$ option causes the parameters of the new local contexts to be
   251   exposed to the current proof context.  Thus local variables stemming from
   252   distant parts of the theory development may be introduced in an implicit
   253   manner, which can be quite confusing to the reader.  Furthermore, this
   254   option may cause unwanted hiding of existing local variables, resulting in
   255   less robust proof texts.
   256 
   257 \item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
   258   induction rules, which are determined as follows:
   259   \begin{matharray}{llll}
   260     \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
   261                     & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
   262     \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
   263     \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
   264   \end{matharray}
   265   
   266   Several instantiations may be given, each referring to some part of a mutual
   267   inductive definition or datatype --- only related partial induction rules
   268   may be used together, though.  Any of the lists of terms $P, x, \dots$
   269   refers to the \emph{suffix} of variables present in the induction rule.
   270   This enables the writer to specify only induction variables, or both
   271   predicates and variables, for example.
   272   
   273   The $stripped$ option causes implications and (bounded) universal
   274   quantifiers to be removed from each new subgoal emerging from the
   275   application of the induction rule.  This accommodates typical
   276   ``strengthening of induction'' predicates.
   277   
   278   The $open$ option has the same effect as for the $cases$ method, see above.
   279 \end{descr}
   280 
   281 Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
   282 determined by the instantiated rule \emph{before} it has been applied to the
   283 internal proof state.\footnote{As a general principle, Isar proof text may
   284   never refer to parts of proof states directly.} Thus proper use of symbolic
   285 cases usually require the rule to be instantiated fully, as far as the
   286 emerging local contexts and subgoals are concerned.  In particular, for
   287 induction both the predicates and variables have to be specified.  Otherwise
   288 the $\CASENAME$ command would refuse to invoke cases containing schematic
   289 variables.
   290 
   291 The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
   292 cases present in the current proof state.
   293 
   294 
   295 \subsection{Declaring rules}
   296 
   297 \indexisaratt{cases}\indexisaratt{induct}
   298 \begin{matharray}{rcl}
   299   cases & : & \isaratt \\
   300   induct & : & \isaratt \\
   301 \end{matharray}
   302 
   303 \begin{rail}
   304   'cases' spec
   305   ;
   306   'induct' spec
   307   ;
   308 
   309   spec: ('type' | 'set') ':' nameref
   310   ;
   311 \end{rail}
   312 
   313 The $cases$ and $induct$ attributes augment the corresponding context of rules
   314 for reasoning about inductive sets and types.  The standard rules are already
   315 declared by HOL definitional packages.  For special applications, these may be
   316 replaced manually by variant versions.
   317 
   318 Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to
   319 adjust names of cases and parameters of a rule.
   320 
   321 
   322 \subsection{Emulating tactic scripts}\label{sec:induct_tac}
   323 
   324 \indexisarmeth{case-tac}\indexisarmeth{induct-tac}
   325 \indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
   326 \begin{matharray}{rcl}
   327   case_tac^* & : & \isarmeth \\
   328   induct_tac^* & : & \isarmeth \\
   329   ind_cases^* & : & \isarmeth \\
   330   \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
   331 \end{matharray}
   332 
   333 \railalias{casetac}{case\_tac}
   334 \railterm{casetac}
   335 
   336 \railalias{inducttac}{induct\_tac}
   337 \railterm{inducttac}
   338 
   339 \railalias{indcases}{ind\_cases}
   340 \railterm{indcases}
   341 
   342 \railalias{inductivecases}{inductive\_cases}
   343 \railterm{inductivecases}
   344 
   345 \begin{rail}
   346   casetac goalspec? term rule?
   347   ;
   348   inducttac goalspec? (insts * 'and') rule?
   349   ;
   350   indcases (prop +)
   351   ;
   352   inductivecases thmdecl? (prop +) comment?
   353   ;
   354 
   355   rule: ('rule' ':' thmref)
   356   ;
   357 \end{rail}
   358 
   359 \begin{descr}
   360 \item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
   361   only (unless an alternative rule is given explicitly).  Furthermore,
   362   $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
   363   variables to be given as instantiation.  These tactic emulations feature
   364   both goal addressing and dynamic instantiation.  Note that named local
   365   contexts (see \S\ref{sec:cases}) are \emph{not} provided as would be by the
   366   proper $induct$ and $cases$ proof methods (see
   367   \S\ref{sec:induct-method-proper}).
   368   
   369 \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
   370   to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
   371   forward manner, unlike the proper $cases$ method (see
   372   \S\ref{sec:induct-method-proper}) which requires simplified cases to be
   373   solved completely.
   374   
   375   While $ind_cases$ is a proof method to apply the result immediately as
   376   elimination rules, $\isarkeyword{inductive_cases}$ provides case split
   377   theorems at the theory level for later use,
   378 \end{descr}
   379 
   380 
   381 \section{Arithmetic}
   382 
   383 \indexisarmeth{arith}\indexisaratt{arith-split}
   384 \begin{matharray}{rcl}
   385   arith & : & \isarmeth \\
   386   arith_split & : & \isaratt \\
   387 \end{matharray}
   388 
   389 \begin{rail}
   390   'arith' '!'?
   391   ;
   392 \end{rail}
   393 
   394 The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
   395 $real$).  Any current facts are inserted into the goal before running the
   396 procedure.  The ``!''~argument causes the full context of assumptions to be
   397 included.  The $arith_split$ attribute declares case split rules to be
   398 expanded before the arithmetic procedure is invoked.
   399 
   400 Note that a simpler (but faster) version of arithmetic reasoning is already
   401 performed by the Simplifier.
   402 
   403 
   404 %%% Local Variables: 
   405 %%% mode: latex
   406 %%% TeX-master: "isar-ref"
   407 %%% End: