doc-src/IsarRef/Thy/HOL_Specific.thy
 author wenzelm Wed Oct 15 21:06:15 2008 +0200 (2008-10-15) changeset 28603 b40800eef8a7 parent 28562 4e74209f113e child 28687 150a8a1eae1a permissions -rw-r--r--
     1 (* $Id$ *)

     2

     3 theory HOL_Specific

     4 imports Main

     5 begin

     6

     7 chapter {* Isabelle/HOL \label{ch:hol} *}

     8

     9 section {* Primitive types \label{sec:hol-typedef} *}

    10

    11 text {*

    12   \begin{matharray}{rcl}

    13     @{command_def (HOL) "typedecl"} & : & \isartrans{theory}{theory} \\

    14     @{command_def (HOL) "typedef"} & : & \isartrans{theory}{proof(prove)} \\

    15   \end{matharray}

    16

    17   \begin{rail}

    18     'typedecl' typespec infix?

    19     ;

    20     'typedef' altname? abstype '=' repset

    21     ;

    22

    23     altname: '(' (name | 'open' | 'open' name) ')'

    24     ;

    25     abstype: typespec infix?

    26     ;

    27     repset: term ('morphisms' name name)?

    28     ;

    29   \end{rail}

    30

    31   \begin{descr}

    32

    33   \item [@{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n)

    34   t"}] is similar to the original @{command "typedecl"} of

    35   Isabelle/Pure (see \secref{sec:types-pure}), but also declares type

    36   arity @{text "t :: (type, \<dots>, type) type"}, making @{text t} an

    37   actual HOL type constructor.   %FIXME check, update

    38

    39   \item [@{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n)

    40   t = A"}] sets up a goal stating non-emptiness of the set @{text A}.

    41   After finishing the proof, the theory will be augmented by a

    42   Gordon/HOL-style type definition, which establishes a bijection

    43   between the representing set @{text A} and the new type @{text t}.

    44

    45   Technically, @{command (HOL) "typedef"} defines both a type @{text

    46   t} and a set (term constant) of the same name (an alternative base

    47   name may be given in parentheses).  The injection from type to set

    48   is called @{text Rep_t}, its inverse @{text Abs_t} (this may be

    49   changed via an explicit @{keyword (HOL) "morphisms"} declaration).

    50

    51   Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text

    52   Abs_t_inverse} provide the most basic characterization as a

    53   corresponding injection/surjection pair (in both directions).  Rules

    54   @{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly

    55   more convenient view on the injectivity part, suitable for automated

    56   proof tools (e.g.\ in @{attribute simp} or @{attribute iff}

    57   declarations).  Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and

    58   @{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views

    59   on surjectivity; these are already declared as set or type rules for

    60   the generic @{method cases} and @{method induct} methods.

    61

    62   An alternative name may be specified in parentheses; the default is

    63   to use @{text t} as indicated before.  The @{text "(open)"}''

    64   declaration suppresses a separate constant definition for the

    65   representing set.

    66

    67   \end{descr}

    68

    69   Note that raw type declarations are rarely used in practice; the

    70   main application is with experimental (or even axiomatic!) theory

    71   fragments.  Instead of primitive HOL type definitions, user-level

    72   theories usually refer to higher-level packages such as @{command

    73   (HOL) "record"} (see \secref{sec:hol-record}) or @{command (HOL)

    74   "datatype"} (see \secref{sec:hol-datatype}).

    75 *}

    76

    77

    78 section {* Adhoc tuples *}

    79

    80 text {*

    81   \begin{matharray}{rcl}

    82     @{attribute (HOL) split_format}@{text "\<^sup>*"} & : & \isaratt \\

    83   \end{matharray}

    84

    85   \begin{rail}

    86     'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))

    87     ;

    88   \end{rail}

    89

    90   \begin{descr}

    91

    92   \item [@{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m

    93   \<AND> \<dots> \<AND> q\<^sub>1 \<dots> q\<^sub>n"}] puts expressions of

    94   low-level tuple types into canonical form as specified by the

    95   arguments given; the @{text i}-th collection of arguments refers to

    96   occurrences in premise @{text i} of the rule.  The @{text

    97   "(complete)"}'' option causes \emph{all} arguments in function

    98   applications to be represented canonically according to their tuple

    99   type structure.

   100

   101   Note that these operations tend to invent funny names for new local

   102   parameters to be introduced.

   103

   104   \end{descr}

   105 *}

   106

   107

   108 section {* Records \label{sec:hol-record} *}

   109

   110 text {*

   111   In principle, records merely generalize the concept of tuples, where

   112   components may be addressed by labels instead of just position.  The

   113   logical infrastructure of records in Isabelle/HOL is slightly more

   114   advanced, though, supporting truly extensible record schemes.  This

   115   admits operations that are polymorphic with respect to record

   116   extension, yielding object-oriented'' effects like (single)

   117   inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for more

   118   details on object-oriented verification and record subtyping in HOL.

   119 *}

   120

   121

   122 subsection {* Basic concepts *}

   123

   124 text {*

   125   Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records

   126   at the level of terms and types.  The notation is as follows:

   127

   128   \begin{center}

   129   \begin{tabular}{l|l|l}

   130     & record terms & record types \\ \hline

   131     fixed & @{text "\<lparr>x = a, y = b\<rparr>"} & @{text "\<lparr>x :: A, y :: B\<rparr>"} \\

   132     schematic & @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} &

   133       @{text "\<lparr>x :: A, y :: B, \<dots> :: M\<rparr>"} \\

   134   \end{tabular}

   135   \end{center}

   136

   137   \noindent The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text

   138   "(| x = a |)"}.

   139

   140   A fixed record @{text "\<lparr>x = a, y = b\<rparr>"} has field @{text x} of value

   141   @{text a} and field @{text y} of value @{text b}.  The corresponding

   142   type is @{text "\<lparr>x :: A, y :: B\<rparr>"}, assuming that @{text "a :: A"}

   143   and @{text "b :: B"}.

   144

   145   A record scheme like @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} contains fields

   146   @{text x} and @{text y} as before, but also possibly further fields

   147   as indicated by the @{text "\<dots>"}'' notation (which is actually part

   148   of the syntax).  The improper field @{text "\<dots>"}'' of a record

   149   scheme is called the \emph{more part}.  Logically it is just a free

   150   variable, which is occasionally referred to as row variable'' in

   151   the literature.  The more part of a record scheme may be

   152   instantiated by zero or more further components.  For example, the

   153   previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z =

   154   c, \<dots> = m'\<rparr>"}, where @{text m'} refers to a different more part.

   155   Fixed records are special instances of record schemes, where

   156   @{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}

   157   element.  In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation

   158   for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}.

   159

   160   \medskip Two key observations make extensible records in a simply

   161   typed language like HOL work out:

   162

   163   \begin{enumerate}

   164

   165   \item the more part is internalized, as a free term or type

   166   variable,

   167

   168   \item field names are externalized, they cannot be accessed within

   169   the logic as first-class values.

   170

   171   \end{enumerate}

   172

   173   \medskip In Isabelle/HOL record types have to be defined explicitly,

   174   fixing their field names and types, and their (optional) parent

   175   record.  Afterwards, records may be formed using above syntax, while

   176   obeying the canonical order of fields as given by their declaration.

   177   The record package provides several standard operations like

   178   selectors and updates.  The common setup for various generic proof

   179   tools enable succinct reasoning patterns.  See also the Isabelle/HOL

   180   tutorial \cite{isabelle-hol-book} for further instructions on using

   181   records in practice.

   182 *}

   183

   184

   185 subsection {* Record specifications *}

   186

   187 text {*

   188   \begin{matharray}{rcl}

   189     @{command_def (HOL) "record"} & : & \isartrans{theory}{theory} \\

   190   \end{matharray}

   191

   192   \begin{rail}

   193     'record' typespec '=' (type '+')? (constdecl +)

   194     ;

   195   \end{rail}

   196

   197   \begin{descr}

   198

   199   \item [@{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t

   200   = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1 \<dots> c\<^sub>n :: \<sigma>\<^sub>n"}] defines

   201   extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},

   202   derived from the optional parent record @{text "\<tau>"} by adding new

   203   field components @{text "c\<^sub>i :: \<sigma>\<^sub>i"} etc.

   204

   205   The type variables of @{text "\<tau>"} and @{text "\<sigma>\<^sub>i"} need to be

   206   covered by the (distinct) parameters @{text "\<alpha>\<^sub>1, \<dots>,

   207   \<alpha>\<^sub>m"}.  Type constructor @{text t} has to be new, while @{text

   208   \<tau>} needs to specify an instance of an existing record type.  At

   209   least one new field @{text "c\<^sub>i"} has to be specified.

   210   Basically, field names need to belong to a unique record.  This is

   211   not a real restriction in practice, since fields are qualified by

   212   the record name internally.

   213

   214   The parent record specification @{text \<tau>} is optional; if omitted

   215   @{text t} becomes a root record.  The hierarchy of all records

   216   declared within a theory context forms a forest structure, i.e.\ a

   217   set of trees starting with a root record each.  There is no way to

   218   merge multiple parent records!

   219

   220   For convenience, @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} is made a

   221   type abbreviation for the fixed record type @{text "\<lparr>c\<^sub>1 ::

   222   \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"}, likewise is @{text

   223   "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme"} made an abbreviation for

   224   @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::

   225   \<zeta>\<rparr>"}.

   226

   227   \end{descr}

   228 *}

   229

   230

   231 subsection {* Record operations *}

   232

   233 text {*

   234   Any record definition of the form presented above produces certain

   235   standard operations.  Selectors and updates are provided for any

   236   field, including the improper one @{text more}''.  There are also

   237   cumulative record constructor functions.  To simplify the

   238   presentation below, we assume for now that @{text "(\<alpha>\<^sub>1, \<dots>,

   239   \<alpha>\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 ::

   240   \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"}.

   241

   242   \medskip \textbf{Selectors} and \textbf{updates} are available for

   243   any field (including @{text more}''):

   244

   245   \begin{matharray}{lll}

   246     @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\

   247     @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\

   248   \end{matharray}

   249

   250   There is special syntax for application of updates: @{text "r\<lparr>x :=

   251   a\<rparr>"} abbreviates term @{text "x_update a r"}.  Further notation for

   252   repeated updates is also available: @{text "r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z :=

   253   c\<rparr>"} may be written @{text "r\<lparr>x := a, y := b, z := c\<rparr>"}.  Note that

   254   because of postfix notation the order of fields shown here is

   255   reverse than in the actual term.  Since repeated updates are just

   256   function applications, fields may be freely permuted in @{text "\<lparr>x

   257   := a, y := b, z := c\<rparr>"}, as far as logical equality is concerned.

   258   Thus commutativity of independent updates can be proven within the

   259   logic for any two fields, but not as a general theorem.

   260

   261   \medskip The \textbf{make} operation provides a cumulative record

   262   constructor function:

   263

   264   \begin{matharray}{lll}

   265     @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\

   266   \end{matharray}

   267

   268   \medskip We now reconsider the case of non-root records, which are

   269   derived of some parent.  In general, the latter may depend on

   270   another parent as well, resulting in a list of \emph{ancestor

   271   records}.  Appending the lists of fields of all ancestors results in

   272   a certain field prefix.  The record package automatically takes care

   273   of this by lifting operations over this context of ancestor fields.

   274   Assuming that @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} has ancestor

   275   fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"},

   276   the above record operations will get the following types:

   277

   278   \medskip

   279   \begin{tabular}{lll}

   280     @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\

   281     @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow>

   282       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>

   283       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\

   284     @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>

   285       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\

   286   \end{tabular}

   287   \medskip

   288

   289   \noindent Some further operations address the extension aspect of a

   290   derived record scheme specifically: @{text "t.fields"} produces a

   291   record fragment consisting of exactly the new fields introduced here

   292   (the result may serve as a more part elsewhere); @{text "t.extend"}

   293   takes a fixed record and adds a given more part; @{text

   294   "t.truncate"} restricts a record scheme to a fixed record.

   295

   296   \medskip

   297   \begin{tabular}{lll}

   298     @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\

   299     @{text "t.extend"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow>

   300       \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\

   301     @{text "t.truncate"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\

   302   \end{tabular}

   303   \medskip

   304

   305   \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide

   306   for root records.

   307 *}

   308

   309

   310 subsection {* Derived rules and proof tools *}

   311

   312 text {*

   313   The record package proves several results internally, declaring

   314   these facts to appropriate proof tools.  This enables users to

   315   reason about record structures quite conveniently.  Assume that

   316   @{text t} is a record type as specified above.

   317

   318   \begin{enumerate}

   319

   320   \item Standard conversions for selectors or updates applied to

   321   record constructor terms are made part of the default Simplifier

   322   context; thus proofs by reduction of basic operations merely require

   323   the @{method simp} method without further arguments.  These rules

   324   are available as @{text "t.simps"}, too.

   325

   326   \item Selectors applied to updated records are automatically reduced

   327   by an internal simplification procedure, which is also part of the

   328   standard Simplifier setup.

   329

   330   \item Inject equations of a form analogous to @{prop "(x, y) = (x',

   331   y') \<equiv> x = x' \<and> y = y'"} are declared to the Simplifier and Classical

   332   Reasoner as @{attribute iff} rules.  These rules are available as

   333   @{text "t.iffs"}.

   334

   335   \item The introduction rule for record equality analogous to @{text

   336   "x r = x r' \<Longrightarrow> y r = y r' \<dots> \<Longrightarrow> r = r'"} is declared to the Simplifier,

   337   and as the basic rule context as @{attribute intro}@{text "?"}''.

   338   The rule is called @{text "t.equality"}.

   339

   340   \item Representations of arbitrary record expressions as canonical

   341   constructor terms are provided both in @{method cases} and @{method

   342   induct} format (cf.\ the generic proof methods of the same name,

   343   \secref{sec:cases-induct}).  Several variations are available, for

   344   fixed records, record schemes, more parts etc.

   345

   346   The generic proof methods are sufficiently smart to pick the most

   347   sensible rule according to the type of the indicated record

   348   expression: users just need to apply something like @{text "(cases

   349   r)"}'' to a certain proof problem.

   350

   351   \item The derived record operations @{text "t.make"}, @{text

   352   "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not}

   353   treated automatically, but usually need to be expanded by hand,

   354   using the collective fact @{text "t.defs"}.

   355

   356   \end{enumerate}

   357 *}

   358

   359

   360 section {* Datatypes \label{sec:hol-datatype} *}

   361

   362 text {*

   363   \begin{matharray}{rcl}

   364     @{command_def (HOL) "datatype"} & : & \isartrans{theory}{theory} \\

   365   @{command_def (HOL) "rep_datatype"} & : & \isartrans{theory}{proof} \\

   366   \end{matharray}

   367

   368   \begin{rail}

   369     'datatype' (dtspec + 'and')

   370     ;

   371     'rep\_datatype' ('(' (name +) ')')? (term +)

   372     ;

   373

   374     dtspec: parname? typespec infix? '=' (cons + '|')

   375     ;

   376     cons: name (type *) mixfix?

   377   \end{rail}

   378

   379   \begin{descr}

   380

   381   \item [@{command (HOL) "datatype"}] defines inductive datatypes in

   382   HOL.

   383

   384   \item [@{command (HOL) "rep_datatype"}] represents existing types as

   385   inductive ones, generating the standard infrastructure of derived

   386   concepts (primitive recursion etc.).

   387

   388   \end{descr}

   389

   390   The induction and exhaustion theorems generated provide case names

   391   according to the constructors involved, while parameters are named

   392   after the types (see also \secref{sec:cases-induct}).

   393

   394   See \cite{isabelle-HOL} for more details on datatypes, but beware of

   395   the old-style theory syntax being used there!  Apart from proper

   396   proof methods for case-analysis and induction, there are also

   397   emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)

   398   induct_tac} available, see \secref{sec:hol-induct-tac}; these admit

   399   to refer directly to the internal structure of subgoals (including

   400   internally bound parameters).

   401 *}

   402

   403

   404 section {* Recursive functions \label{sec:recursion} *}

   405

   406 text {*

   407   \begin{matharray}{rcl}

   408     @{command_def (HOL) "primrec"} & : & \isarkeep{local{\dsh}theory} \\

   409     @{command_def (HOL) "fun"} & : & \isarkeep{local{\dsh}theory} \\

   410     @{command_def (HOL) "function"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\

   411     @{command_def (HOL) "termination"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\

   412   \end{matharray}

   413

   414   \begin{rail}

   415     'primrec' target? fixes 'where' equations

   416     ;

   417     equations: (thmdecl? prop + '|')

   418     ;

   419     ('fun' | 'function') target? functionopts? fixes 'where' clauses

   420     ;

   421     clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')

   422     ;

   423     functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'

   424     ;

   425     'termination' ( term )?

   426   \end{rail}

   427

   428   \begin{descr}

   429

   430   \item [@{command (HOL) "primrec"}] defines primitive recursive

   431   functions over datatypes, see also \cite{isabelle-HOL}.

   432

   433   \item [@{command (HOL) "function"}] defines functions by general

   434   wellfounded recursion. A detailed description with examples can be

   435   found in \cite{isabelle-function}. The function is specified by a

   436   set of (possibly conditional) recursive equations with arbitrary

   437   pattern matching. The command generates proof obligations for the

   438   completeness and the compatibility of patterns.

   439

   440   The defined function is considered partial, and the resulting

   441   simplification rules (named @{text "f.psimps"}) and induction rule

   442   (named @{text "f.pinduct"}) are guarded by a generated domain

   443   predicate @{text "f_dom"}. The @{command (HOL) "termination"}

   444   command can then be used to establish that the function is total.

   445

   446   \item [@{command (HOL) "fun"}] is a shorthand notation for

   447   @{command (HOL) "function"}~@{text "(sequential)"}, followed by

   448   automated proof attempts regarding pattern matching and termination.

   449   See \cite{isabelle-function} for further details.

   450

   451   \item [@{command (HOL) "termination"}~@{text f}] commences a

   452   termination proof for the previously defined function @{text f}.  If

   453   this is omitted, the command refers to the most recent function

   454   definition.  After the proof is closed, the recursive equations and

   455   the induction principle is established.

   456

   457   \end{descr}

   458

   459   %FIXME check

   460

   461   Recursive definitions introduced by the @{command (HOL) "function"}

   462   command accommodate

   463   reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text

   464   "c.induct"} (where @{text c} is the name of the function definition)

   465   refers to a specific induction rule, with parameters named according

   466   to the user-specified equations.

   467   For the @{command (HOL) "primrec"} the induction principle coincides

   468   with structural recursion on the datatype the recursion is carried

   469   out.

   470   Case names of @{command (HOL)

   471   "primrec"} are that of the datatypes involved, while those of

   472   @{command (HOL) "function"} are numbered (starting from 1).

   473

   474   The equations provided by these packages may be referred later as

   475   theorem list @{text "f.simps"}, where @{text f} is the (collective)

   476   name of the functions defined.  Individual equations may be named

   477   explicitly as well.

   478

   479   The @{command (HOL) "function"} command accepts the following

   480   options.

   481

   482   \begin{descr}

   483

   484   \item [@{text sequential}] enables a preprocessor which

   485   disambiguates overlapping patterns by making them mutually disjoint.

   486   Earlier equations take precedence over later ones.  This allows to

   487   give the specification in a format very similar to functional

   488   programming.  Note that the resulting simplification and induction

   489   rules correspond to the transformed specification, not the one given

   490   originally. This usually means that each equation given by the user

   491   may result in several theroems.  Also note that this automatic

   492   transformation only works for ML-style datatype patterns.

   493

   494   \item [@{text domintros}] enables the automated generation of

   495   introduction rules for the domain predicate. While mostly not

   496   needed, they can be helpful in some proofs about partial functions.

   497

   498   \item [@{text tailrec}] generates the unconstrained recursive

   499   equations even without a termination proof, provided that the

   500   function is tail-recursive. This currently only works

   501

   502   \item [@{text "default d"}] allows to specify a default value for a

   503   (partial) function, which will ensure that @{text "f x = d x"}

   504   whenever @{text "x \<notin> f_dom"}.

   505

   506   \end{descr}

   507 *}

   508

   509

   510 subsection {* Proof methods related to recursive definitions *}

   511

   512 text {*

   513   \begin{matharray}{rcl}

   514     @{method_def (HOL) pat_completeness} & : & \isarmeth \\

   515     @{method_def (HOL) relation} & : & \isarmeth \\

   516     @{method_def (HOL) lexicographic_order} & : & \isarmeth \\

   517   \end{matharray}

   518

   519   \begin{rail}

   520     'relation' term

   521     ;

   522     'lexicographic\_order' (clasimpmod *)

   523     ;

   524   \end{rail}

   525

   526   \begin{descr}

   527

   528   \item [@{method (HOL) pat_completeness}] is a specialized method to

   529   solve goals regarding the completeness of pattern matching, as

   530   required by the @{command (HOL) "function"} package (cf.\

   531   \cite{isabelle-function}).

   532

   533   \item [@{method (HOL) relation}~@{text R}] introduces a termination

   534   proof using the relation @{text R}.  The resulting proof state will

   535   contain goals expressing that @{text R} is wellfounded, and that the

   536   arguments of recursive calls decrease with respect to @{text R}.

   537   Usually, this method is used as the initial proof step of manual

   538   termination proofs.

   539

   540   \item [@{method (HOL) "lexicographic_order"}] attempts a fully

   541   automated termination proof by searching for a lexicographic

   542   combination of size measures on the arguments of the function. The

   543   method accepts the same arguments as the @{method auto} method,

   544   which it uses internally to prove local descents.  The same context

   545   modifiers as for @{method auto} are accepted, see

   546   \secref{sec:clasimp}.

   547

   548   In case of failure, extensive information is printed, which can help

   549   to analyse the situation (cf.\ \cite{isabelle-function}).

   550

   551   \end{descr}

   552 *}

   553

   554

   555 subsection {* Old-style recursive function definitions (TFL) *}

   556

   557 text {*

   558   The old TFL commands @{command (HOL) "recdef"} and @{command (HOL)

   559   "recdef_tc"} for defining recursive are mostly obsolete; @{command

   560   (HOL) "function"} or @{command (HOL) "fun"} should be used instead.

   561

   562   \begin{matharray}{rcl}

   563     @{command_def (HOL) "recdef"} & : & \isartrans{theory}{theory} \\

   564     @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & \isartrans{theory}{proof(prove)} \\

   565   \end{matharray}

   566

   567   \begin{rail}

   568     'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?

   569     ;

   570     recdeftc thmdecl? tc

   571     ;

   572     hints: '(' 'hints' (recdefmod *) ')'

   573     ;

   574     recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod

   575     ;

   576     tc: nameref ('(' nat ')')?

   577     ;

   578   \end{rail}

   579

   580   \begin{descr}

   581

   582   \item [@{command (HOL) "recdef"}] defines general well-founded

   583   recursive functions (using the TFL package), see also

   584   \cite{isabelle-HOL}.  The @{text "(permissive)"}'' option tells

   585   TFL to recover from failed proof attempts, returning unfinished

   586   results.  The @{text recdef_simp}, @{text recdef_cong}, and @{text

   587   recdef_wf} hints refer to auxiliary rules to be used in the internal

   588   automated proof process of TFL.  Additional @{syntax clasimpmod}

   589   declarations (cf.\ \secref{sec:clasimp}) may be given to tune the

   590   context of the Simplifier (cf.\ \secref{sec:simplifier}) and

   591   Classical reasoner (cf.\ \secref{sec:classical}).

   592

   593   \item [@{command (HOL) "recdef_tc"}~@{text "c (i)"}] recommences the

   594   proof for leftover termination condition number @{text i} (default

   595   1) as generated by a @{command (HOL) "recdef"} definition of

   596   constant @{text c}.

   597

   598   Note that in most cases, @{command (HOL) "recdef"} is able to finish

   599   its internal proofs without manual intervention.

   600

   601   \end{descr}

   602

   603   \medskip Hints for @{command (HOL) "recdef"} may be also declared

   604   globally, using the following attributes.

   605

   606   \begin{matharray}{rcl}

   607     @{attribute_def (HOL) recdef_simp} & : & \isaratt \\

   608     @{attribute_def (HOL) recdef_cong} & : & \isaratt \\

   609     @{attribute_def (HOL) recdef_wf} & : & \isaratt \\

   610   \end{matharray}

   611

   612   \begin{rail}

   613     ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')

   614     ;

   615   \end{rail}

   616 *}

   617

   618

   619 section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}

   620

   621 text {*

   622   An \textbf{inductive definition} specifies the least predicate (or

   623   set) @{text R} closed under given rules: applying a rule to elements

   624   of @{text R} yields a result within @{text R}.  For example, a

   625   structural operational semantics is an inductive definition of an

   626   evaluation relation.

   627

   628   Dually, a \textbf{coinductive definition} specifies the greatest

   629   predicate~/ set @{text R} that is consistent with given rules: every

   630   element of @{text R} can be seen as arising by applying a rule to

   631   elements of @{text R}.  An important example is using bisimulation

   632   relations to formalise equivalence of processes and infinite data

   633   structures.

   634

   635   \medskip The HOL package is related to the ZF one, which is

   636   described in a separate paper,\footnote{It appeared in CADE

   637   \cite{paulson-CADE}; a longer version is distributed with Isabelle.}

   638   which you should refer to in case of difficulties.  The package is

   639   simpler than that of ZF thanks to implicit type-checking in HOL.

   640   The types of the (co)inductive predicates (or sets) determine the

   641   domain of the fixedpoint definition, and the package does not have

   642   to use inference rules for type-checking.

   643

   644   \begin{matharray}{rcl}

   645     @{command_def (HOL) "inductive"} & : & \isarkeep{local{\dsh}theory} \\

   646     @{command_def (HOL) "inductive_set"} & : & \isarkeep{local{\dsh}theory} \\

   647     @{command_def (HOL) "coinductive"} & : & \isarkeep{local{\dsh}theory} \\

   648     @{command_def (HOL) "coinductive_set"} & : & \isarkeep{local{\dsh}theory} \\

   649     @{attribute_def (HOL) mono} & : & \isaratt \\

   650   \end{matharray}

   651

   652   \begin{rail}

   653     ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\

   654     ('where' clauses)? ('monos' thmrefs)?

   655     ;

   656     clauses: (thmdecl? prop + '|')

   657     ;

   658     'mono' (() | 'add' | 'del')

   659     ;

   660   \end{rail}

   661

   662   \begin{descr}

   663

   664   \item [@{command (HOL) "inductive"} and @{command (HOL)

   665   "coinductive"}] define (co)inductive predicates from the

   666   introduction rules given in the @{keyword "where"} part.  The

   667   optional @{keyword "for"} part contains a list of parameters of the

   668   (co)inductive predicates that remain fixed throughout the

   669   definition.  The optional @{keyword "monos"} section contains

   670   \emph{monotonicity theorems}, which are required for each operator

   671   applied to a recursive set in the introduction rules.  There

   672   \emph{must} be a theorem of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"},

   673   for each premise @{text "M R\<^sub>i t"} in an introduction rule!

   674

   675   \item [@{command (HOL) "inductive_set"} and @{command (HOL)

   676   "coinductive_set"}] are wrappers for to the previous commands,

   677   allowing the definition of (co)inductive sets.

   678

   679   \item [@{attribute (HOL) mono}] declares monotonicity rules.  These

   680   rule are involved in the automated monotonicity proof of @{command

   681   (HOL) "inductive"}.

   682

   683   \end{descr}

   684 *}

   685

   686

   687 subsection {* Derived rules *}

   688

   689 text {*

   690   Each (co)inductive definition @{text R} adds definitions to the

   691   theory and also proves some theorems:

   692

   693   \begin{description}

   694

   695   \item [@{text R.intros}] is the list of introduction rules as proven

   696   theorems, for the recursive predicates (or sets).  The rules are

   697   also available individually, using the names given them in the

   698   theory file;

   699

   700   \item [@{text R.cases}] is the case analysis (or elimination) rule;

   701

   702   \item [@{text R.induct} or @{text R.coinduct}] is the (co)induction

   703   rule.

   704

   705   \end{description}

   706

   707   When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are

   708   defined simultaneously, the list of introduction rules is called

   709   @{text "R\<^sub>1_\<dots>_R\<^sub>n.intros"}, the case analysis rules are

   710   called @{text "R\<^sub>1.cases, \<dots>, R\<^sub>n.cases"}, and the list

   711   of mutual induction rules is called @{text

   712   "R\<^sub>1_\<dots>_R\<^sub>n.inducts"}.

   713 *}

   714

   715

   716 subsection {* Monotonicity theorems *}

   717

   718 text {*

   719   Each theory contains a default set of theorems that are used in

   720   monotonicity proofs.  New rules can be added to this set via the

   721   @{attribute (HOL) mono} attribute.  The HOL theory @{text Inductive}

   722   shows how this is done.  In general, the following monotonicity

   723   theorems may be added:

   724

   725   \begin{itemize}

   726

   727   \item Theorems of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"}, for proving

   728   monotonicity of inductive definitions whose introduction rules have

   729   premises involving terms such as @{text "M R\<^sub>i t"}.

   730

   731   \item Monotonicity theorems for logical operators, which are of the

   732   general form @{text "(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>"}.  For example, in

   733   the case of the operator @{text "\<or>"}, the corresponding theorem is

   734   $  735 \infer{@{text "P\<^sub>1 \<or> P\<^sub>2 \<longrightarrow> Q\<^sub>1 \<or> Q\<^sub>2"}}{@{text "P\<^sub>1 \<longrightarrow> Q\<^sub>1"} & @{text "P\<^sub>2 \<longrightarrow> Q\<^sub>2"}}   736$

   737

   738   \item De Morgan style equations for reasoning about the polarity''

   739   of expressions, e.g.

   740   $  741 @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad   742 @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}   743$

   744

   745   \item Equations for reducing complex operators to more primitive

   746   ones whose monotonicity can easily be proved, e.g.

   747   $  748 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad   749 @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}   750$

   751

   752   \end{itemize}

   753

   754   %FIXME: Example of an inductive definition

   755 *}

   756

   757

   758 section {* Arithmetic proof support *}

   759

   760 text {*

   761   \begin{matharray}{rcl}

   762     @{method_def (HOL) arith} & : & \isarmeth \\

   763     @{attribute_def (HOL) arith_split} & : & \isaratt \\

   764   \end{matharray}

   765

   766   The @{method (HOL) arith} method decides linear arithmetic problems

   767   (on types @{text nat}, @{text int}, @{text real}).  Any current

   768   facts are inserted into the goal before running the procedure.

   769

   770   The @{attribute (HOL) arith_split} attribute declares case split

   771   rules to be expanded before the arithmetic procedure is invoked.

   772

   773   Note that a simpler (but faster) version of arithmetic reasoning is

   774   already performed by the Simplifier.

   775 *}

   776

   777

   778 section {* Invoking automated reasoning tools -- The Sledgehammer *}

   779

   780 text {*

   781   Isabelle/HOL includes a generic \emph{ATP manager} that allows

   782   external automated reasoning tools to crunch a pending goal.

   783   Supported provers include E\footnote{\url{http://www.eprover.org}},

   784   SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire.

   785   There is also a wrapper to invoke provers remotely via the

   786   SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}}

   787   web service.

   788

   789   The problem passed to external provers consists of the goal together

   790   with a smart selection of lemmas from the current theory context.

   791   The result of a successful proof search is some source text that

   792   usually reconstructs the proof within Isabelle, without requiring

   793   external provers again.  The Metis

   794   prover\footnote{\url{http://www.gilith.com/software/metis/}} that is

   795   integrated into Isabelle/HOL is being used here.

   796

   797   In this mode of operation, heavy means of automated reasoning are

   798   used as a strong relevance filter, while the main proof checking

   799   works via explicit inferences going through the Isabelle kernel.

   800   Moreover, rechecking Isabelle proof texts with already specified

   801   auxiliary facts is much faster than performing fully automated

   802   search over and over again.

   803

   804   \begin{matharray}{rcl}

   805     @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\

   806     @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

   807     @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\

   808     @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\

   809     @{method_def (HOL) metis} & : & \isarmeth \\

   810   \end{matharray}

   811

   812   \begin{rail}

   813   'sledgehammer' (nameref *)

   814   ;

   815

   816   'metis' thmrefs

   817   ;

   818   \end{rail}

   819

   820   \begin{descr}

   821

   822   \item [@{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \<dots>

   823   prover\<^sub>n"}] invokes the specified automated theorem provers on

   824   the first subgoal.  Provers are run in parallel, the first

   825   successful result is displayed, and the other attempts are

   826   terminated.

   827

   828   Provers are defined in the theory context, see also @{command (HOL)

   829   print_atps}.  If no provers are given as arguments to @{command

   830   (HOL) sledgehammer}, the system refers to the default defined as

   831   ATP provers'' preference by the user interface.

   832

   833   There are additional preferences for timeout (default: 60 seconds),

   834   and the maximum number of independent prover processes (default: 5);

   835   excessive provers are automatically terminated.

   836

   837   \item [@{command (HOL) print_atps}] prints the list of automated

   838   theorem provers available to the @{command (HOL) sledgehammer}

   839   command.

   840

   841   \item [@{command (HOL) atp_info}] prints information about presently

   842   running provers, including elapsed runtime, and the remaining time

   843   until timeout.

   844

   845   \item [@{command (HOL) atp_kill}] terminates all presently running

   846   provers.

   847

   848   \item [@{method (HOL) metis}~@{text "facts"}] invokes the Metis

   849   prover with the given facts.  Metis is an automated proof tool of

   850   medium strength, but is fully integrated into Isabelle/HOL, with

   851   explicit inferences going through the kernel.  Thus its results are

   852   guaranteed to be correct by construction''.

   853

   854   Note that all facts used with Metis need to be specified as explicit

   855   arguments.  There are no rule declarations as for other Isabelle

   856   provers, like @{method blast} or @{method fast}.

   857

   858   \end{descr}

   859 *}

   860

   861

   862 section {* Unstructured cases analysis and induction \label{sec:hol-induct-tac} *}

   863

   864 text {*

   865   The following tools of Isabelle/HOL support cases analysis and

   866   induction in unstructured tactic scripts; see also

   867   \secref{sec:cases-induct} for proper Isar versions of similar ideas.

   868

   869   \begin{matharray}{rcl}

   870     @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\

   871     @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\

   872     @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\

   873     @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & \isartrans{theory}{theory} \\

   874   \end{matharray}

   875

   876   \begin{rail}

   877     'case\_tac' goalspec? term rule?

   878     ;

   879     'induct\_tac' goalspec? (insts * 'and') rule?

   880     ;

   881     'ind\_cases' (prop +) ('for' (name +)) ?

   882     ;

   883     'inductive\_cases' (thmdecl? (prop +) + 'and')

   884     ;

   885

   886     rule: ('rule' ':' thmref)

   887     ;

   888   \end{rail}

   889

   890   \begin{descr}

   891

   892   \item [@{method (HOL) case_tac} and @{method (HOL) induct_tac}]

   893   admit to reason about inductive types.  Rules are selected according

   894   to the declarations by the @{attribute cases} and @{attribute

   895   induct} attributes, cf.\ \secref{sec:cases-induct}.  The @{command

   896   (HOL) datatype} package already takes care of this.

   897

   898   These unstructured tactics feature both goal addressing and dynamic

   899   instantiation.  Note that named rule cases are \emph{not} provided

   900   as would be by the proper @{method cases} and @{method induct} proof

   901   methods (see \secref{sec:cases-induct}).  Unlike the @{method

   902   induct} method, @{method induct_tac} does not handle structured rule

   903   statements, only the compact object-logic conclusion of the subgoal

   904   being addressed.

   905

   906   \item [@{method (HOL) ind_cases} and @{command (HOL)

   907   "inductive_cases"}] provide an interface to the internal @{ML_text

   908   mk_cases} operation.  Rules are simplified in an unrestricted

   909   forward manner.

   910

   911   While @{method (HOL) ind_cases} is a proof method to apply the

   912   result immediately as elimination rules, @{command (HOL)

   913   "inductive_cases"} provides case split theorems at the theory level

   914   for later use.  The @{keyword "for"} argument of the @{method (HOL)

   915   ind_cases} method allows to specify a list of variables that should

   916   be generalized before applying the resulting rule.

   917

   918   \end{descr}

   919 *}

   920

   921

   922 section {* Executable code *}

   923

   924 text {*

   925   Isabelle/Pure provides two generic frameworks to support code

   926   generation from executable specifications.  Isabelle/HOL

   927   instantiates these mechanisms in a way that is amenable to end-user

   928   applications.

   929

   930   One framework generates code from both functional and relational

   931   programs to SML.  See \cite{isabelle-HOL} for further information

   932   (this actually covers the new-style theory format as well).

   933

   934   \begin{matharray}{rcl}

   935     @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

   936     @{command_def (HOL) "code_module"} & : & \isartrans{theory}{theory} \\

   937     @{command_def (HOL) "code_library"} & : & \isartrans{theory}{theory} \\

   938     @{command_def (HOL) "consts_code"} & : & \isartrans{theory}{theory} \\

   939     @{command_def (HOL) "types_code"} & : & \isartrans{theory}{theory} \\

   940     @{attribute_def (HOL) code} & : & \isaratt \\

   941   \end{matharray}

   942

   943   \begin{rail}

   944   'value' term

   945   ;

   946

   947   ( 'code\_module' | 'code\_library' ) modespec ? name ? \\

   948     ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\

   949     'contains' ( ( name '=' term ) + | term + )

   950   ;

   951

   952   modespec: '(' ( name * ) ')'

   953   ;

   954

   955   'consts\_code' (codespec +)

   956   ;

   957

   958   codespec: const template attachment ?

   959   ;

   960

   961   'types\_code' (tycodespec +)

   962   ;

   963

   964   tycodespec: name template attachment ?

   965   ;

   966

   967   const: term

   968   ;

   969

   970   template: '(' string ')'

   971   ;

   972

   973   attachment: 'attach' modespec ? verblbrace text verbrbrace

   974   ;

   975

   976   'code' (name)?

   977   ;

   978   \end{rail}

   979

   980   \begin{descr}

   981

   982   \item [@{command (HOL) "value"}~@{text t}] evaluates and prints a

   983   term using the code generator.

   984

   985   \end{descr}

   986

   987   \medskip The other framework generates code from functional programs

   988   (including overloading using type classes) to SML \cite{SML}, OCaml

   989   \cite{OCaml} and Haskell \cite{haskell-revised-report}.

   990   Conceptually, code generation is split up in three steps:

   991   \emph{selection} of code theorems, \emph{translation} into an

   992   abstract executable view and \emph{serialization} to a specific

   993   \emph{target language}.  See \cite{isabelle-codegen} for an

   994   introduction on how to use it.

   995

   996   \begin{matharray}{rcl}

   997     @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

   998     @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

   999     @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

  1000     @{command_def (HOL) "code_datatype"} & : & \isartrans{theory}{theory} \\

  1001     @{command_def (HOL) "code_const"} & : & \isartrans{theory}{theory} \\

  1002     @{command_def (HOL) "code_type"} & : & \isartrans{theory}{theory} \\

  1003     @{command_def (HOL) "code_class"} & : & \isartrans{theory}{theory} \\

  1004     @{command_def (HOL) "code_instance"} & : & \isartrans{theory}{theory} \\

  1005     @{command_def (HOL) "code_monad"} & : & \isartrans{theory}{theory} \\

  1006     @{command_def (HOL) "code_reserved"} & : & \isartrans{theory}{theory} \\

  1007     @{command_def (HOL) "code_include"} & : & \isartrans{theory}{theory} \\

  1008     @{command_def (HOL) "code_modulename"} & : & \isartrans{theory}{theory} \\

  1009     @{command_def (HOL) "code_abort"} & : & \isartrans{theory}{theory} \\

  1010     @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\

  1011     @{attribute_def (HOL) code} & : & \isaratt \\

  1012   \end{matharray}

  1013

  1014   \begin{rail}

  1015     'export\_code' ( constexpr + ) ? \\

  1016       ( ( 'in' target ( 'module\_name' string ) ? \\

  1017         ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?

  1018     ;

  1019

  1020     'code\_thms' ( constexpr + ) ?

  1021     ;

  1022

  1023     'code\_deps' ( constexpr + ) ?

  1024     ;

  1025

  1026     const: term

  1027     ;

  1028

  1029     constexpr: ( const | 'name.*' | '*' )

  1030     ;

  1031

  1032     typeconstructor: nameref

  1033     ;

  1034

  1035     class: nameref

  1036     ;

  1037

  1038     target: 'OCaml' | 'SML' | 'Haskell'

  1039     ;

  1040

  1041     'code\_datatype' const +

  1042     ;

  1043

  1044     'code\_const' (const + 'and') \\

  1045       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )

  1046     ;

  1047

  1048     'code\_type' (typeconstructor + 'and') \\

  1049       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )

  1050     ;

  1051

  1052     'code\_class' (class + 'and') \\

  1053       ( ( '(' target \\

  1054         ( ( string ('where' \\

  1055           ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )

  1056     ;

  1057

  1058     'code\_instance' (( typeconstructor '::' class ) + 'and') \\

  1059       ( ( '(' target ( '-' ? + 'and' ) ')' ) + )

  1060     ;

  1061

  1062     'code\_monad' const const target

  1063     ;

  1064

  1065     'code\_reserved' target ( string + )

  1066     ;

  1067

  1068     'code\_include' target ( string ( string | '-') )

  1069     ;

  1070

  1071     'code\_modulename' target ( ( string string ) + )

  1072     ;

  1073

  1074     'code\_abort' ( const + )

  1075     ;

  1076

  1077     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string

  1078     ;

  1079

  1080     'code' ( 'inline' ) ? ( 'del' ) ?

  1081     ;

  1082   \end{rail}

  1083

  1084   \begin{descr}

  1085

  1086   \item [@{command (HOL) "export_code"}] is the canonical interface

  1087   for generating and serializing code: for a given list of constants,

  1088   code is generated for the specified target languages.  Abstract code

  1089   is cached incrementally.  If no constant is given, the currently

  1090   cached code is serialized.  If no serialization instruction is

  1091   given, only abstract code is cached.

  1092

  1093   Constants may be specified by giving them literally, referring to

  1094   all executable contants within a certain theory by giving @{text

  1095   "name.*"}, or referring to \emph{all} executable constants currently

  1096   available by giving @{text "*"}.

  1097

  1098   By default, for each involved theory one corresponding name space

  1099   module is generated.  Alternativly, a module name may be specified

  1100   after the @{keyword "module_name"} keyword; then \emph{all} code is

  1101   placed in this module.

  1102

  1103   For \emph{SML} and \emph{OCaml}, the file specification refers to a

  1104   single file; for \emph{Haskell}, it refers to a whole directory,

  1105   where code is generated in multiple files reflecting the module

  1106   hierarchy.  The file specification @{text "-"}'' denotes standard

  1107   output.  For \emph{SML}, omitting the file specification compiles

  1108   code internally in the context of the current ML session.

  1109

  1110   Serializers take an optional list of arguments in parentheses.  For

  1111   \emph{Haskell} a module name prefix may be given using the @{text

  1112   "root:"}'' argument; @{text string_classes}'' adds a @{verbatim

  1113   "deriving (Read, Show)"}'' clause to each appropriate datatype

  1114   declaration.

  1115

  1116   \item [@{command (HOL) "code_thms"}] prints a list of theorems

  1117   representing the corresponding program containing all given

  1118   constants; if no constants are given, the currently cached code

  1119   theorems are printed.

  1120

  1121   \item [@{command (HOL) "code_deps"}] visualizes dependencies of

  1122   theorems representing the corresponding program containing all given

  1123   constants; if no constants are given, the currently cached code

  1124   theorems are visualized.

  1125

  1126   \item [@{command (HOL) "code_datatype"}] specifies a constructor set

  1127   for a logical type.

  1128

  1129   \item [@{command (HOL) "code_const"}] associates a list of constants

  1130   with target-specific serializations; omitting a serialization

  1131   deletes an existing serialization.

  1132

  1133   \item [@{command (HOL) "code_type"}] associates a list of type

  1134   constructors with target-specific serializations; omitting a

  1135   serialization deletes an existing serialization.

  1136

  1137   \item [@{command (HOL) "code_class"}] associates a list of classes

  1138   with target-specific class names; in addition, constants associated

  1139   with this class may be given target-specific names used for instance

  1140   declarations; omitting a serialization deletes an existing

  1141   serialization.  This applies only to \emph{Haskell}.

  1142

  1143   \item [@{command (HOL) "code_instance"}] declares a list of type

  1144   constructor / class instance relations as already present'' for a

  1145   given target.  Omitting a @{text "-"}'' deletes an existing

  1146   already present'' declaration.  This applies only to

  1147   \emph{Haskell}.

  1148

  1149   \item [@{command (HOL) "code_monad"}] provides an auxiliary

  1150   mechanism to generate monadic code for Haskell.

  1151

  1152   \item [@{command (HOL) "code_reserved"}] declares a list of names as

  1153   reserved for a given target, preventing it to be shadowed by any

  1154   generated code.

  1155

  1156   \item [@{command (HOL) "code_include"}] adds arbitrary named content

  1157   (include'') to generated code.  A @{text "-"}'' as last argument

  1158   will remove an already added include''.

  1159

  1160   \item [@{command (HOL) "code_modulename"}] declares aliasings from

  1161   one module name onto another.

  1162

  1163   \item [@{command (HOL) "code_abort"}] declares constants which

  1164   are not required to have a definition by means of defining equations;

  1165   if needed these are implemented by program abort instead.

  1166

  1167   \item [@{attribute (HOL) code}] explicitly selects (or

  1168   with option @{text "del"}'' deselects) a defining equation for

  1169   code generation.  Usually packages introducing defining equations

  1170   provide a reasonable default setup for selection.

  1171

  1172   \item [@{attribute (HOL) code}@{text inline}] declares (or with

  1173   option @{text "del"}'' removes) inlining theorems which are

  1174   applied as rewrite rules to any defining equation during

  1175   preprocessing.

  1176

  1177   \item [@{command (HOL) "print_codesetup"}] gives an overview on

  1178   selected defining equations, code generator datatypes and

  1179   preprocessor setup.

  1180

  1181   \end{descr}

  1182 *}

  1183

  1184

  1185 section {* Definition by specification \label{sec:hol-specification} *}

  1186

  1187 text {*

  1188   \begin{matharray}{rcl}

  1189     @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\

  1190     @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\

  1191   \end{matharray}

  1192

  1193   \begin{rail}

  1194   ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)

  1195   ;

  1196   decl: ((name ':')? term '(' 'overloaded' ')'?)

  1197   \end{rail}

  1198

  1199   \begin{descr}

  1200

  1201   \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a

  1202   goal stating the existence of terms with the properties specified to

  1203   hold for the constants given in @{text decls}.  After finishing the

  1204   proof, the theory will be augmented with definitions for the given

  1205   constants, as well as with theorems stating the properties for these

  1206   constants.

  1207

  1208   \item [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets

  1209   up a goal stating the existence of terms with the properties

  1210   specified to hold for the constants given in @{text decls}.  After

  1211   finishing the proof, the theory will be augmented with axioms

  1212   expressing the properties given in the first place.

  1213

  1214   \item [@{text decl}] declares a constant to be defined by the

  1215   specification given.  The definition for the constant @{text c} is

  1216   bound to the name @{text c_def} unless a theorem name is given in

  1217   the declaration.  Overloaded constants should be declared as such.

  1218

  1219   \end{descr}

  1220

  1221   Whether to use @{command (HOL) "specification"} or @{command (HOL)

  1222   "ax_specification"} is to some extent a matter of style.  @{command

  1223   (HOL) "specification"} introduces no new axioms, and so by

  1224   construction cannot introduce inconsistencies, whereas @{command

  1225   (HOL) "ax_specification"} does introduce axioms, but only after the

  1226   user has explicitly proven it to be safe.  A practical issue must be

  1227   considered, though: After introducing two constants with the same

  1228   properties using @{command (HOL) "specification"}, one can prove

  1229   that the two constants are, in fact, equal.  If this might be a

  1230   problem, one should use @{command (HOL) "ax_specification"}.

  1231 *}

  1232

  1233 end