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: