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: