doc-src/IsarRef/hol.tex
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9935 a87965201c34
child 9949 1741a61d4b33
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     1 
     2 \chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools}
     3 
     4 \section{Miscellaneous attributes}
     5 
     6 \indexisaratt{rule-format}
     7 \begin{matharray}{rcl}
     8   rule_format & : & \isaratt \\
     9 \end{matharray}
    10 
    11 \railalias{ruleformat}{rule\_format}
    12 \railterm{ruleformat}
    13 
    14 \begin{rail}
    15   ruleformat ('(' noasm ')')?
    16   ;
    17 \end{rail}
    18 
    19 \begin{descr}
    20   
    21 \item [$rule_format$] causes a theorem to be put into standard object-rule
    22   form, replacing implication and (bounded) universal quantification of HOL by
    23   the corresponding meta-logical connectives.  By default, the result is fully
    24   normalized, including assumptions and conclusions at any depth.  The
    25   $no_asm$ option restricts the transformation to the conclusion of a rule.
    26 \end{descr}
    27 
    28 
    29 \section{Primitive types}
    30 
    31 \indexisarcmd{typedecl}\indexisarcmd{typedef}
    32 \begin{matharray}{rcl}
    33   \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
    34   \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
    35 \end{matharray}
    36 
    37 \begin{rail}
    38   'typedecl' typespec infix? comment?
    39   ;
    40   'typedef' parname? typespec infix? \\ '=' term comment?
    41   ;
    42 \end{rail}
    43 
    44 \begin{descr}
    45 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
    46   $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
    47   also declares type arity $t :: (term, \dots, term) term$, making $t$ an
    48   actual HOL type constructor.
    49 \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
    50   non-emptiness of the set $A$.  After finishing the proof, the theory will be
    51   augmented by a Gordon/HOL-style type definition.  See \cite{isabelle-HOL}
    52   for more information.  Note that user-level theories usually do not directly
    53   refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
    54   packages such as $\isarkeyword{record}$ (see \S\ref{sec:record}) and
    55   $\isarkeyword{datatype}$ (see \S\ref{sec:datatype}).
    56 \end{descr}
    57 
    58 
    59 \section{Records}\label{sec:record}
    60 
    61 \indexisarcmd{record}
    62 \begin{matharray}{rcl}
    63   \isarcmd{record} & : & \isartrans{theory}{theory} \\
    64 \end{matharray}
    65 
    66 \begin{rail}
    67   'record' typespec '=' (type '+')? (field +)
    68   ;
    69 
    70   field: name '::' type comment?
    71   ;
    72 \end{rail}
    73 
    74 \begin{descr}
    75 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
    76   defines extensible record type $(\vec\alpha)t$, derived from the optional
    77   parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
    78   See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
    79   simply-typed extensible records.
    80 \end{descr}
    81 
    82 
    83 \section{Datatypes}\label{sec:datatype}
    84 
    85 \indexisarcmd{datatype}\indexisarcmd{rep-datatype}
    86 \begin{matharray}{rcl}
    87   \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
    88   \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
    89 \end{matharray}
    90 
    91 \railalias{repdatatype}{rep\_datatype}
    92 \railterm{repdatatype}
    93 
    94 \begin{rail}
    95   'datatype' (dtspec + 'and')
    96   ;
    97   repdatatype (name * ) dtrules
    98   ;
    99 
   100   dtspec: parname? typespec infix? '=' (cons + '|')
   101   ;
   102   cons: name (type * ) mixfix? comment?
   103   ;
   104   dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
   105 \end{rail}
   106 
   107 \begin{descr}
   108 \item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
   109 \item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
   110   ones, generating the standard infrastructure of derived concepts (primitive
   111   recursion etc.).
   112 \end{descr}
   113 
   114 The induction and exhaustion theorems generated provide case names according
   115 to the constructors involved, while parameters are named after the types (see
   116 also \S\ref{sec:induct-method}).
   117 
   118 See \cite{isabelle-HOL} for more details on datatypes.  Note that the theory
   119 syntax above has been slightly simplified over the old version, usually
   120 requiring more quotes and less parentheses.  Apart from proper proof methods
   121 for case-analysis and induction, there are also emulations of ML tactics
   122 \texttt{case_tac} and \texttt{induct_tac} available, see
   123 \S\ref{sec:induct_tac}.
   124 
   125 
   126 \section{Recursive functions}
   127 
   128 \indexisarcmd{primrec}\indexisarcmd{recdef}
   129 \begin{matharray}{rcl}
   130   \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
   131   \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
   132 %FIXME
   133 %  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
   134 \end{matharray}
   135 
   136 \begin{rail}
   137   'primrec' parname? (equation + )
   138   ;
   139   'recdef' name term (eqn + ) hints?
   140   ;
   141 
   142   equation: thmdecl? eqn
   143   ;
   144   eqn: prop comment?
   145   ;
   146   hints: '(' 'hints' (recdefmod * ) ')'
   147   ;
   148   recdefmod: (('simp' | 'cong' | 'wf' | 'split' | 'iff') (() | 'add' | 'del') ':' thmrefs) | clamod
   149   ;
   150 \end{rail}
   151 
   152 \begin{descr}
   153 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over
   154   datatypes, see also \cite{isabelle-HOL}.
   155 \item [$\isarkeyword{recdef}$] defines general well-founded recursive
   156   functions (using the TFL package), see also \cite{isabelle-HOL}.  The
   157   $simp$, $cong$, and $wf$ hints refer to auxiliary rules to be used in the
   158   internal automated proof process of TFL; the other declarations refer to the
   159   Simplifier and Classical reasoner (\S\ref{sec:simplifier},
   160   \S\ref{sec:classical}, \S\ref{sec:clasimp}) that are used internally.
   161 \end{descr}
   162 
   163 Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 
   164 \S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
   165 of the function definition) refers to a specific induction rule, with
   166 parameters named according to the user-specified equations.  Case names of
   167 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of
   168 $\isarkeyword{recdef}$ are numbered (starting from $1$).
   169 
   170 The equations provided by these packages may be referred later as theorem list
   171 $f\mathord.simps$, where $f$ is the (collective) name of the functions
   172 defined.  Individual equations may be named explicitly as well; note that for
   173 $\isarkeyword{recdef}$ each specification given by the user may result in
   174 several theorems.
   175 
   176 \medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
   177 the following attributes.
   178 
   179 \indexisaratt{recdef-simp}\indexisaratt{recdef-cong}\indexisaratt{recdef-wf}
   180 \begin{matharray}{rcl}
   181   recdef_simp & : & \isaratt \\
   182   recdef_cong & : & \isaratt \\
   183   recdef_wf & : & \isaratt \\
   184 \end{matharray}
   185 
   186 \railalias{recdefsimp}{recdef\_simp}
   187 \railterm{recdefsimp}
   188 
   189 \railalias{recdefcong}{recdef\_cong}
   190 \railterm{recdefcong}
   191 
   192 \railalias{recdefwf}{recdef\_wf}
   193 \railterm{recdefwf}
   194 
   195 \begin{rail}
   196   (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
   197   ;
   198 \end{rail}
   199 
   200 
   201 \section{(Co)Inductive sets}
   202 
   203 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono}
   204 \begin{matharray}{rcl}
   205   \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
   206   \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
   207   mono & : & \isaratt \\
   208 \end{matharray}
   209 
   210 \railalias{condefs}{con\_defs}
   211 \railterm{condefs}
   212 
   213 \begin{rail}
   214   ('inductive' | 'coinductive') sets intros monos?
   215   ;
   216   'mono' (() | 'add' | 'del')
   217   ;
   218 
   219   sets: (term comment? +)
   220   ;
   221   intros: 'intros' attributes? (thmdecl? prop comment? +)
   222   ;
   223   monos: 'monos' thmrefs comment?
   224   ;
   225 \end{rail}
   226 
   227 \begin{descr}
   228 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
   229   (co)inductive sets from the given introduction rules.
   230 \item [$mono$] declares monotonicity rules.  These rule are involved in the
   231   automated monotonicity proof of $\isarkeyword{inductive}$.
   232 \end{descr}
   233 
   234 See \cite{isabelle-HOL} for further information on inductive definitions in
   235 HOL.
   236 
   237 
   238 \section{Proof by cases and induction}\label{sec:induct-method}
   239 
   240 \subsection{Proof methods}\label{sec:induct-method-proper}
   241 
   242 \indexisarmeth{cases}\indexisarmeth{induct}
   243 \begin{matharray}{rcl}
   244   cases & : & \isarmeth \\
   245   induct & : & \isarmeth \\
   246 \end{matharray}
   247 
   248 The $cases$ and $induct$ methods provide a uniform interface to case analysis
   249 and induction over datatypes, inductive sets, and recursive functions.  The
   250 corresponding rules may be specified and instantiated in a casual manner.
   251 Furthermore, these methods provide named local contexts that may be invoked
   252 via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
   253 \S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
   254 about large specifications.
   255 
   256 \begin{rail}
   257   'cases' simplified? open? args rule?
   258   ;
   259   'induct' stripped? open? args rule?
   260   ;
   261 
   262   simplified: '(' 'simplified' ')'
   263   ;
   264   stripped: '(' 'stripped' ')'
   265   ;
   266   open: '(' 'open' ')'
   267   ;
   268   args: (insts * 'and') 
   269   ;
   270   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
   271   ;
   272 \end{rail}
   273 
   274 \begin{descr}
   275 \item [$cases~insts~R$] applies method $rule$ with an appropriate case
   276   distinction theorem, instantiated to the subjects $insts$.  Symbolic case
   277   names are bound according to the rule's local contexts.
   278   
   279   The rule is determined as follows, according to the facts and arguments
   280   passed to the $cases$ method:
   281   \begin{matharray}{llll}
   282     \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
   283                     & cases &           & \Text{classical case split} \\
   284                     & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
   285     \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
   286     \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
   287   \end{matharray}
   288   
   289   Several instantiations may be given, referring to the \emph{suffix} of
   290   premises of the case rule; within each premise, the \emph{prefix} of
   291   variables is instantiated.  In most situations, only a single term needs to
   292   be specified; this refers to the first variable of the last premise (it is
   293   usually the same for all cases).
   294 
   295   The $simplified$ option causes ``obvious cases'' of the rule to be solved
   296   beforehand, while the others are left unscathed.
   297   
   298   The $open$ option causes the parameters of the new local contexts to be
   299   exposed to the current proof context.  Thus local variables stemming from
   300   distant parts of the theory development may be introduced in an implicit
   301   manner, which can be quite confusing to the reader.  Furthermore, this
   302   option may cause unwanted hiding of existing local variables, resulting in
   303   less robust proof texts.
   304 
   305 \item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
   306   induction rules, which are determined as follows:
   307   \begin{matharray}{llll}
   308     \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
   309                     & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
   310     \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
   311     \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
   312   \end{matharray}
   313   
   314   Several instantiations may be given, each referring to some part of a mutual
   315   inductive definition or datatype --- only related partial induction rules
   316   may be used together, though.  Any of the lists of terms $P, x, \dots$
   317   refers to the \emph{suffix} of variables present in the induction rule.
   318   This enables the writer to specify only induction variables, or both
   319   predicates and variables, for example.
   320   
   321   The $stripped$ option causes implications and (bounded) universal
   322   quantifiers to be removed from each new subgoal emerging from the
   323   application of the induction rule.  This accommodates typical
   324   ``strengthening of induction'' predicates.
   325   
   326   The $open$ option has the same effect as for the $cases$ method, see above.
   327 \end{descr}
   328 
   329 Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
   330 determined by the instantiated rule \emph{before} it has been applied to the
   331 internal proof state.\footnote{As a general principle, Isar proof text may
   332   never refer to parts of proof states directly.} Thus proper use of symbolic
   333 cases usually require the rule to be instantiated fully, as far as the
   334 emerging local contexts and subgoals are concerned.  In particular, for
   335 induction both the predicates and variables have to be specified.  Otherwise
   336 the $\CASENAME$ command would refuse to invoke cases containing schematic
   337 variables.
   338 
   339 The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
   340 cases present in the current proof state.
   341 
   342 
   343 \subsection{Declaring rules}
   344 
   345 \indexisaratt{cases}\indexisaratt{induct}
   346 \begin{matharray}{rcl}
   347   cases & : & \isaratt \\
   348   induct & : & \isaratt \\
   349 \end{matharray}
   350 
   351 \begin{rail}
   352   'cases' spec
   353   ;
   354   'induct' spec
   355   ;
   356 
   357   spec: ('type' | 'set') ':' nameref
   358   ;
   359 \end{rail}
   360 
   361 The $cases$ and $induct$ attributes augment the corresponding context of rules
   362 for reasoning about inductive sets and types.  The standard rules are already
   363 declared by HOL definitional packages.  For special applications, these may be
   364 replaced manually by variant versions.
   365 
   366 Refer to the $case_names$ and $params$ attributes (see \S\ref{sec:cases}) to
   367 adjust names of cases and parameters of a rule.
   368 
   369 
   370 \subsection{Emulating tactic scripts}\label{sec:induct_tac}
   371 
   372 \indexisarmeth{case-tac}\indexisarmeth{induct-tac}
   373 \indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
   374 \begin{matharray}{rcl}
   375   case_tac^* & : & \isarmeth \\
   376   induct_tac^* & : & \isarmeth \\
   377   ind_cases^* & : & \isarmeth \\
   378   \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
   379 \end{matharray}
   380 
   381 \railalias{casetac}{case\_tac}
   382 \railterm{casetac}
   383 
   384 \railalias{inducttac}{induct\_tac}
   385 \railterm{inducttac}
   386 
   387 \railalias{indcases}{ind\_cases}
   388 \railterm{indcases}
   389 
   390 \railalias{inductivecases}{inductive\_cases}
   391 \railterm{inductivecases}
   392 
   393 \begin{rail}
   394   casetac goalspec? term rule?
   395   ;
   396   inducttac goalspec? (insts * 'and') rule?
   397   ;
   398   indcases (prop +)
   399   ;
   400   inductivecases thmdecl? (prop +) comment?
   401   ;
   402 
   403   rule: ('rule' ':' thmref)
   404   ;
   405 \end{rail}
   406 
   407 \begin{descr}
   408 \item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
   409   only (unless an alternative rule is given explicitly).  Furthermore,
   410   $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
   411   variables to be given as instantiation.  These tactic emulations feature
   412   both goal addressing and dynamic instantiation.  Note that named local
   413   contexts (see \S\ref{sec:cases}) are \emph{not} provided as would be by the
   414   proper $induct$ and $cases$ proof methods (see
   415   \S\ref{sec:induct-method-proper}).
   416   
   417 \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
   418   to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
   419   forward manner, unlike the proper $cases$ method (see
   420   \S\ref{sec:induct-method-proper}) which requires simplified cases to be
   421   solved completely.
   422   
   423   While $ind_cases$ is a proof method to apply the result immediately as
   424   elimination rules, $\isarkeyword{inductive_cases}$ provides case split
   425   theorems at the theory level for later use,
   426 \end{descr}
   427 
   428 
   429 \section{Arithmetic}
   430 
   431 \indexisarmeth{arith}\indexisaratt{arith-split}
   432 \begin{matharray}{rcl}
   433   arith & : & \isarmeth \\
   434   arith_split & : & \isaratt \\
   435 \end{matharray}
   436 
   437 \begin{rail}
   438   'arith' '!'?
   439   ;
   440 \end{rail}
   441 
   442 The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
   443 $real$).  Any current facts are inserted into the goal before running the
   444 procedure.  The ``!''~argument causes the full context of assumptions to be
   445 included.  The $arith_split$ attribute declares case split rules to be
   446 expanded before the arithmetic procedure is invoked.
   447 
   448 Note that a simpler (but faster) version of arithmetic reasoning is already
   449 performed by the Simplifier.
   450 
   451 
   452 %%% Local Variables: 
   453 %%% mode: latex
   454 %%% TeX-master: "isar-ref"
   455 %%% End: