doc-src/IsarRef/Thy/HOL_Specific.thy
 author haftmann Fri Nov 26 12:03:18 2010 +0100 (2010-11-26) changeset 40711 81bc73585eec parent 40709 b29c70cd5c93 child 40800 330eb65c9469 permissions -rw-r--r--
globbing constant expressions use more idiomatic underscore rather than star
     1 theory HOL_Specific

     2 imports Main

     3 begin

     4

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

     6

     7 section {* Typedef axiomatization \label{sec:hol-typedef} *}

     8

     9 text {*

    10   \begin{matharray}{rcl}

    11     @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

    12   \end{matharray}

    13

    14   \begin{rail}

    15     'typedef' altname? abstype '=' repset

    16     ;

    17

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

    19     ;

    20     abstype: typespecsorts mixfix?

    21     ;

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

    23     ;

    24   \end{rail}

    25

    26   \begin{description}

    27

    28   \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}

    29   axiomatizes a Gordon/HOL-style type definition in the background

    30   theory of the current context, depending on a non-emptiness result

    31   of the set @{text A} (which needs to be proven interactively).

    32

    33   The raw type may not depend on parameters or assumptions of the

    34   context --- this is logically impossible in Isabelle/HOL --- but the

    35   non-emptiness property can be local, potentially resulting in

    36   multiple interpretations in target contexts.  Thus the established

    37   bijection between the representing set @{text A} and the new type

    38   @{text t} may semantically depend on local assumptions.

    39

    40   By default, @{command (HOL) "typedef"} defines both a type @{text t}

    41   and a set (term constant) of the same name, unless an alternative

    42   base name is given in parentheses, or the @{text "(open)"}''

    43   declaration is used to suppress a separate constant definition

    44   altogether.  The injection from type to set is called @{text Rep_t},

    45   its inverse @{text Abs_t} --- this may be changed via an explicit

    46   @{keyword (HOL) "morphisms"} declaration.

    47

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

    49   Abs_t_inverse} provide the most basic characterization as a

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

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

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

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

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

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

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

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

    58

    59   An alternative name for the set definition (and other derived

    60   entities) may be specified in parentheses; the default is to use

    61   @{text t} as indicated before.

    62

    63   \end{description}

    64 *}

    65

    66

    67 section {* Adhoc tuples *}

    68

    69 text {*

    70   \begin{matharray}{rcl}

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

    72   \end{matharray}

    73

    74   \begin{rail}

    75     'split_format' '(' 'complete' ')'

    76     ;

    77   \end{rail}

    78

    79   \begin{description}

    80

    81   \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes

    82   arguments in function applications to be represented canonically

    83   according to their tuple type structure.

    84

    85   Note that this operation tends to invent funny names for new local

    86   parameters introduced.

    87

    88   \end{description}

    89 *}

    90

    91

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

    93

    94 text {*

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

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

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

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

    99   admits operations that are polymorphic with respect to record

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

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

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

   103 *}

   104

   105

   106 subsection {* Basic concepts *}

   107

   108 text {*

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

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

   111

   112   \begin{center}

   113   \begin{tabular}{l|l|l}

   114     & record terms & record types \\ \hline

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

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

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

   118   \end{tabular}

   119   \end{center}

   120

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

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

   123

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

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

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

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

   128

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

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

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

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

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

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

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

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

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

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

   139   Fixed records are special instances of record schemes, where

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

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

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

   143

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

   145   typed language like HOL work out:

   146

   147   \begin{enumerate}

   148

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

   150   variable,

   151

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

   153   the logic as first-class values.

   154

   155   \end{enumerate}

   156

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

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

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

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

   161   The record package provides several standard operations like

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

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

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

   165   records in practice.

   166 *}

   167

   168

   169 subsection {* Record specifications *}

   170

   171 text {*

   172   \begin{matharray}{rcl}

   173     @{command_def (HOL) "record"} & : & @{text "theory \<rightarrow> theory"} \\

   174   \end{matharray}

   175

   176   \begin{rail}

   177     'record' typespecsorts '=' (type '+')? (constdecl +)

   178     ;

   179   \end{rail}

   180

   181   \begin{description}

   182

   183   \item @{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1

   184   \<dots> c\<^sub>n :: \<sigma>\<^sub>n"} defines extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},

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

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

   187

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

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

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

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

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

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

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

   195   the record name internally.

   196

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

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

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

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

   201   merge multiple parent records!

   202

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

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

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

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

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

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

   209

   210   \end{description}

   211 *}

   212

   213

   214 subsection {* Record operations *}

   215

   216 text {*

   217   Any record definition of the form presented above produces certain

   218   standard operations.  Selectors and updates are provided for any

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

   220   cumulative record constructor functions.  To simplify the

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

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

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

   224

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

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

   227

   228   \begin{matharray}{lll}

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

   230     @{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>"} \\

   231   \end{matharray}

   232

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

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

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

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

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

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

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

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

   241   Thus commutativity of independent updates can be proven within the

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

   243

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

   245   constructor function:

   246

   247   \begin{matharray}{lll}

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

   249   \end{matharray}

   250

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

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

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

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

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

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

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

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

   259   the above record operations will get the following types:

   260

   261   \medskip

   262   \begin{tabular}{lll}

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

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

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

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

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

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

   269   \end{tabular}

   270   \medskip

   271

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

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

   274   record fragment consisting of exactly the new fields introduced here

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

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

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

   278

   279   \medskip

   280   \begin{tabular}{lll}

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

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

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

   284     @{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>"} \\

   285   \end{tabular}

   286   \medskip

   287

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

   289   for root records.

   290 *}

   291

   292

   293 subsection {* Derived rules and proof tools *}

   294

   295 text {*

   296   The record package proves several results internally, declaring

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

   298   reason about record structures quite conveniently.  Assume that

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

   300

   301   \begin{enumerate}

   302

   303   \item Standard conversions for selectors or updates applied to

   304   record constructor terms are made part of the default Simplifier

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

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

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

   308

   309   \item Selectors applied to updated records are automatically reduced

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

   311   standard Simplifier setup.

   312

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

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

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

   316   @{text "t.iffs"}.

   317

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

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

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

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

   322

   323   \item Representations of arbitrary record expressions as canonical

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

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

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

   327   fixed records, record schemes, more parts etc.

   328

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

   330   sensible rule according to the type of the indicated record

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

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

   333

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

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

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

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

   338

   339   \end{enumerate}

   340 *}

   341

   342

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

   344

   345 text {*

   346   \begin{matharray}{rcl}

   347     @{command_def (HOL) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\

   348   @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\

   349   \end{matharray}

   350

   351   \begin{rail}

   352     'datatype' (dtspec + 'and')

   353     ;

   354     'rep_datatype' ('(' (name +) ')')? (term +)

   355     ;

   356

   357     dtspec: parname? typespec mixfix? '=' (cons + '|')

   358     ;

   359     cons: name ( type * ) mixfix?

   360   \end{rail}

   361

   362   \begin{description}

   363

   364   \item @{command (HOL) "datatype"} defines inductive datatypes in

   365   HOL.

   366

   367   \item @{command (HOL) "rep_datatype"} represents existing types as

   368   inductive ones, generating the standard infrastructure of derived

   369   concepts (primitive recursion etc.).

   370

   371   \end{description}

   372

   373   The induction and exhaustion theorems generated provide case names

   374   according to the constructors involved, while parameters are named

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

   376

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

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

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

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

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

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

   383   internally bound parameters).

   384 *}

   385

   386

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

   388

   389 text {*

   390   \begin{matharray}{rcl}

   391     @{command_def (HOL) "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   392     @{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   393     @{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   394     @{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   395   \end{matharray}

   396

   397   \begin{rail}

   398     'primrec' target? fixes 'where' equations

   399     ;

   400     ('fun' | 'function') target? functionopts? fixes \\ 'where' equations

   401     ;

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

   403     ;

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

   405     ;

   406     'termination' ( term )?

   407   \end{rail}

   408

   409   \begin{description}

   410

   411   \item @{command (HOL) "primrec"} defines primitive recursive

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

   413

   414   \item @{command (HOL) "function"} defines functions by general

   415   wellfounded recursion. A detailed description with examples can be

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

   417   set of (possibly conditional) recursive equations with arbitrary

   418   pattern matching. The command generates proof obligations for the

   419   completeness and the compatibility of patterns.

   420

   421   The defined function is considered partial, and the resulting

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

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

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

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

   426

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

   428   (HOL) "function"}~@{text "(sequential)"}, followed by automated

   429   proof attempts regarding pattern matching and termination.  See

   430   \cite{isabelle-function} for further details.

   431

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

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

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

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

   436   the induction principle is established.

   437

   438   \end{description}

   439

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

   441   command accommodate

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

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

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

   445   to the user-specified equations. Cases are numbered (starting from 1).

   446

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

   448   with structural recursion on the datatype the recursion is carried

   449   out.

   450

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

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

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

   454   explicitly as well.

   455

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

   457   options.

   458

   459   \begin{description}

   460

   461   \item @{text sequential} enables a preprocessor which disambiguates

   462   overlapping patterns by making them mutually disjoint.  Earlier

   463   equations take precedence over later ones.  This allows to give the

   464   specification in a format very similar to functional programming.

   465   Note that the resulting simplification and induction rules

   466   correspond to the transformed specification, not the one given

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

   468   may result in several theorems.  Also note that this automatic

   469   transformation only works for ML-style datatype patterns.

   470

   471   \item @{text domintros} enables the automated generation of

   472   introduction rules for the domain predicate. While mostly not

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

   474

   475   \item @{text tailrec} generates the unconstrained recursive

   476   equations even without a termination proof, provided that the

   477   function is tail-recursive. This currently only works

   478

   479   \item @{text "default d"} allows to specify a default value for a

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

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

   482

   483   \end{description}

   484 *}

   485

   486

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

   488

   489 text {*

   490   \begin{matharray}{rcl}

   491     @{method_def (HOL) pat_completeness} & : & @{text method} \\

   492     @{method_def (HOL) relation} & : & @{text method} \\

   493     @{method_def (HOL) lexicographic_order} & : & @{text method} \\

   494     @{method_def (HOL) size_change} & : & @{text method} \\

   495   \end{matharray}

   496

   497   \begin{rail}

   498     'relation' term

   499     ;

   500     'lexicographic_order' ( clasimpmod * )

   501     ;

   502     'size_change' ( orders ( clasimpmod * ) )

   503     ;

   504     orders: ( 'max' | 'min' | 'ms' ) *

   505   \end{rail}

   506

   507   \begin{description}

   508

   509   \item @{method (HOL) pat_completeness} is a specialized method to

   510   solve goals regarding the completeness of pattern matching, as

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

   512   \cite{isabelle-function}).

   513

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

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

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

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

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

   519   termination proofs.

   520

   521   \item @{method (HOL) "lexicographic_order"} attempts a fully

   522   automated termination proof by searching for a lexicographic

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

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

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

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

   527   \secref{sec:clasimp}.

   528

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

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

   531

   532   \item @{method (HOL) "size_change"} also works on termination goals,

   533   using a variation of the size-change principle, together with a

   534   graph decomposition technique (see \cite{krauss_phd} for details).

   535   Three kinds of orders are used internally: @{text max}, @{text min},

   536   and @{text ms} (multiset), which is only available when the theory

   537   @{text Multiset} is loaded. When no order kinds are given, they are

   538   tried in order. The search for a termination proof uses SAT solving

   539   internally.

   540

   541  For local descent proofs, the same context modifiers as for @{method

   542   auto} are accepted, see \secref{sec:clasimp}.

   543

   544   \end{description}

   545 *}

   546

   547 subsection {* Functions with explicit partiality *}

   548

   549 text {*

   550   \begin{matharray}{rcl}

   551     @{command_def (HOL) "partial_function"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   552     @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\

   553   \end{matharray}

   554

   555   \begin{rail}

   556     'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop

   557   \end{rail}

   558

   559   \begin{description}

   560

   561   \item @{command (HOL) "partial_function"} defines recursive

   562   functions based on fixpoints in complete partial orders. No

   563   termination proof is required from the user or constructed

   564   internally. Instead, the possibility of non-termination is modelled

   565   explicitly in the result type, which contains an explicit bottom

   566   element.

   567

   568   Pattern matching and mutual recursion are currently not supported.

   569   Thus, the specification consists of a single function described by a

   570   single recursive equation.

   571

   572   There are no fixed syntactic restrictions on the body of the

   573   function, but the induced functional must be provably monotonic

   574   wrt.\ the underlying order.  The monotonicitity proof is performed

   575   internally, and the definition is rejected when it fails. The proof

   576   can be influenced by declaring hints using the

   577   @{attribute (HOL) partial_function_mono} attribute.

   578

   579   The mandatory @{text mode} argument specifies the mode of operation

   580   of the command, which directly corresponds to a complete partial

   581   order on the result type. By default, the following modes are

   582   defined:

   583

   584   \begin{description}

   585   \item @{text option} defines functions that map into the @{type

   586   option} type. Here, the value @{term None} is used to model a

   587   non-terminating computation. Monotonicity requires that if @{term

   588   None} is returned by a recursive call, then the overall result

   589   must also be @{term None}. This is best achieved through the use of

   590   the monadic operator @{const "Option.bind"}.

   591

   592   \item @{text tailrec} defines functions with an arbitrary result

   593   type and uses the slightly degenerated partial order where @{term

   594   "undefined"} is the bottom element.  Now, monotonicity requires that

   595   if @{term undefined} is returned by a recursive call, then the

   596   overall result must also be @{term undefined}. In practice, this is

   597   only satisfied when each recursive call is a tail call, whose result

   598   is directly returned. Thus, this mode of operation allows the

   599   definition of arbitrary tail-recursive functions.

   600   \end{description}

   601

   602   Experienced users may define new modes by instantiating the locale

   603   @{const "partial_function_definitions"} appropriately.

   604

   605   \item @{attribute (HOL) partial_function_mono} declares rules for

   606   use in the internal monononicity proofs of partial function

   607   definitions.

   608

   609   \end{description}

   610

   611 *}

   612

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

   614

   615 text {*

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

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

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

   619

   620   \begin{matharray}{rcl}

   621     @{command_def (HOL) "recdef"} & : & @{text "theory \<rightarrow> theory)"} \\

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

   623   \end{matharray}

   624

   625   \begin{rail}

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

   627     ;

   628     recdeftc thmdecl? tc

   629     ;

   630     hints: '(' 'hints' ( recdefmod * ) ')'

   631     ;

   632     recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod

   633     ;

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

   635     ;

   636   \end{rail}

   637

   638   \begin{description}

   639

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

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

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

   643   TFL to recover from failed proof attempts, returning unfinished

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

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

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

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

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

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

   650

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

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

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

   654   constant @{text c}.

   655

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

   657   its internal proofs without manual intervention.

   658

   659   \end{description}

   660

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

   662   globally, using the following attributes.

   663

   664   \begin{matharray}{rcl}

   665     @{attribute_def (HOL) recdef_simp} & : & @{text attribute} \\

   666     @{attribute_def (HOL) recdef_cong} & : & @{text attribute} \\

   667     @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\

   668   \end{matharray}

   669

   670   \begin{rail}

   671     ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')

   672     ;

   673   \end{rail}

   674 *}

   675

   676

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

   678

   679 text {*

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

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

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

   683   structural operational semantics is an inductive definition of an

   684   evaluation relation.

   685

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

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

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

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

   690   relations to formalise equivalence of processes and infinite data

   691   structures.

   692

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

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

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

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

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

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

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

   700   to use inference rules for type-checking.

   701

   702   \begin{matharray}{rcl}

   703     @{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   704     @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   705     @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   706     @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   707     @{attribute_def (HOL) mono} & : & @{text attribute} \\

   708   \end{matharray}

   709

   710   \begin{rail}

   711     ('inductive' | 'inductive_set' | 'coinductive' | 'coinductive_set') target? fixes ('for' fixes)? \\

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

   713     ;

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

   715     ;

   716     'mono' (() | 'add' | 'del')

   717     ;

   718   \end{rail}

   719

   720   \begin{description}

   721

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

   723   "coinductive"} define (co)inductive predicates from the

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

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

   726   (co)inductive predicates that remain fixed throughout the

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

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

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

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

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

   732

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

   734   "coinductive_set"} are wrappers for to the previous commands,

   735   allowing the definition of (co)inductive sets.

   736

   737   \item @{attribute (HOL) mono} declares monotonicity rules.  These

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

   739   (HOL) "inductive"}.

   740

   741   \end{description}

   742 *}

   743

   744

   745 subsection {* Derived rules *}

   746

   747 text {*

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

   749   theory and also proves some theorems:

   750

   751   \begin{description}

   752

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

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

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

   756   theory file;

   757

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

   759

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

   761   rule.

   762

   763   \end{description}

   764

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

   766   defined simultaneously, the list of introduction rules is called

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

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

   769   of mutual induction rules is called @{text

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

   771 *}

   772

   773

   774 subsection {* Monotonicity theorems *}

   775

   776 text {*

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

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

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

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

   781   theorems may be added:

   782

   783   \begin{itemize}

   784

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

   786   monotonicity of inductive definitions whose introduction rules have

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

   788

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

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

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

   792   $  793 \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"}}   794$

   795

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

   797   of expressions, e.g.

   798   $  799 @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad   800 @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}   801$

   802

   803   \item Equations for reducing complex operators to more primitive

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

   805   $  806 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad   807 @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}   808$

   809

   810   \end{itemize}

   811

   812   %FIXME: Example of an inductive definition

   813 *}

   814

   815

   816 section {* Arithmetic proof support *}

   817

   818 text {*

   819   \begin{matharray}{rcl}

   820     @{method_def (HOL) arith} & : & @{text method} \\

   821     @{attribute_def (HOL) arith} & : & @{text attribute} \\

   822     @{attribute_def (HOL) arith_split} & : & @{text attribute} \\

   823   \end{matharray}

   824

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

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

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

   828

   829   The @{attribute (HOL) arith} attribute declares facts that are

   830   always supplied to the arithmetic provers implicitly.

   831

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

   833   rules to be expanded before @{method (HOL) arith} is invoked.

   834

   835   Note that a simpler (but faster) arithmetic prover is

   836   already invoked by the Simplifier.

   837 *}

   838

   839

   840 section {* Intuitionistic proof search *}

   841

   842 text {*

   843   \begin{matharray}{rcl}

   844     @{method_def (HOL) iprover} & : & @{text method} \\

   845   \end{matharray}

   846

   847   \begin{rail}

   848     'iprover' ( rulemod * )

   849     ;

   850   \end{rail}

   851

   852   The @{method (HOL) iprover} method performs intuitionistic proof

   853   search, depending on specifically declared rules from the context,

   854   or given as explicit arguments.  Chained facts are inserted into the

   855   goal before commencing proof search.

   856

   857   Rules need to be classified as @{attribute (Pure) intro},

   858   @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the

   859   @{text "!"}'' indicator refers to safe'' rules, which may be

   860   applied aggressively (without considering back-tracking later).

   861   Rules declared with @{text "?"}'' are ignored in proof search (the

   862   single-step @{method rule} method still observes these).  An

   863   explicit weight annotation may be given as well; otherwise the

   864   number of rule premises will be taken into account here.

   865 *}

   866

   867

   868 section {* Coherent Logic *}

   869

   870 text {*

   871   \begin{matharray}{rcl}

   872     @{method_def (HOL) "coherent"} & : & @{text method} \\

   873   \end{matharray}

   874

   875   \begin{rail}

   876     'coherent' thmrefs?

   877     ;

   878   \end{rail}

   879

   880   The @{method (HOL) coherent} method solves problems of

   881   \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers

   882   applications in confluence theory, lattice theory and projective

   883   geometry.  See @{"file" "~~/src/HOL/ex/Coherent.thy"} for some

   884   examples.

   885 *}

   886

   887

   888 section {* Checking and refuting propositions *}

   889

   890 text {*

   891   Identifying incorrect propositions usually involves evaluation of

   892   particular assignments and systematic counter example search.  This

   893   is supported by the following commands.

   894

   895   \begin{matharray}{rcl}

   896     @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

   897     @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\

   898     @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"}

   899   \end{matharray}

   900

   901   \begin{rail}

   902     'value' ( ( '[' name ']' ) ? ) modes? term

   903     ;

   904

   905     'quickcheck' ( ( '[' args ']' ) ? ) nat?

   906     ;

   907

   908     'quickcheck_params' ( ( '[' args ']' ) ? )

   909     ;

   910

   911     modes: '(' (name + ) ')'

   912     ;

   913

   914     args: ( name '=' value + ',' )

   915     ;

   916   \end{rail}

   917

   918   \begin{description}

   919

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

   921     term; optionally @{text modes} can be specified, which are

   922     appended to the current print mode (see also \cite{isabelle-ref}).

   923     Internally, the evaluation is performed by registered evaluators,

   924     which are invoked sequentially until a result is returned.

   925     Alternatively a specific evaluator can be selected using square

   926     brackets; typical evaluators use the current set of code equations

   927     to normalize and include @{text simp} for fully symbolic evaluation

   928     using the simplifier, @{text nbe} for \emph{normalization by evaluation}

   929     and \emph{code} for code generation in SML.

   930

   931   \item @{command (HOL) "quickcheck"} tests the current goal for

   932     counter examples using a series of arbitrary assignments for its

   933     free variables; by default the first subgoal is tested, an other

   934     can be selected explicitly using an optional goal index.

   935     A number of configuration options are supported for

   936     @{command (HOL) "quickcheck"}, notably:

   937

   938     \begin{description}

   939

   940     \item[@{text size}] specifies the maximum size of the search space

   941     for assignment values.

   942

   943     \item[@{text iterations}] sets how many sets of assignments are

   944     generated for each particular size.

   945

   946     \item[@{text no_assms}] specifies whether assumptions in

   947     structured proofs should be ignored.

   948

   949     \item[@{text timeout}] sets the time limit in seconds.

   950

   951     \item[@{text default_type}] sets the type(s) generally used to

   952     instantiate type variables.

   953

   954     \item[@{text report}] if set quickcheck reports how many tests

   955     fulfilled the preconditions.

   956

   957     \item[@{text quiet}] if not set quickcheck informs about the

   958     current size for assignment values.

   959

   960     \item[@{text expect}] can be used to check if the user's

   961     expectation was met (@{text no_expectation}, @{text

   962     no_counterexample}, or @{text counterexample}).

   963

   964     \end{description}

   965

   966     These option can be given within square brackets.

   967

   968   \item @{command (HOL) "quickcheck_params"} changes quickcheck

   969     configuration options persitently.

   970

   971   \end{description}

   972 *}

   973

   974

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

   976

   977 text {*

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

   979   induction in unstructured tactic scripts; see also

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

   981

   982   \begin{matharray}{rcl}

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

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

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

   986     @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   987   \end{matharray}

   988

   989   \begin{rail}

   990     'case_tac' goalspec? term rule?

   991     ;

   992     'induct_tac' goalspec? (insts * 'and') rule?

   993     ;

   994     'ind_cases' (prop +) ('for' (name +)) ?

   995     ;

   996     'inductive_cases' (thmdecl? (prop +) + 'and')

   997     ;

   998

   999     rule: ('rule' ':' thmref)

  1000     ;

  1001   \end{rail}

  1002

  1003   \begin{description}

  1004

  1005   \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit

  1006   to reason about inductive types.  Rules are selected according to

  1007   the declarations by the @{attribute cases} and @{attribute induct}

  1008   attributes, cf.\ \secref{sec:cases-induct}.  The @{command (HOL)

  1009   datatype} package already takes care of this.

  1010

  1011   These unstructured tactics feature both goal addressing and dynamic

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

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

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

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

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

  1017   being addressed.

  1018

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

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

  1021   mk_cases} operation.  Rules are simplified in an unrestricted

  1022   forward manner.

  1023

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

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

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

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

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

  1029   be generalized before applying the resulting rule.

  1030

  1031   \end{description}

  1032 *}

  1033

  1034

  1035 section {* Executable code *}

  1036

  1037 text {*

  1038   Isabelle/Pure provides two generic frameworks to support code

  1039   generation from executable specifications.  Isabelle/HOL

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

  1041   applications.

  1042

  1043   \medskip One framework generates code from functional programs

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

  1045   \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala

  1046   \cite{scala-overview-tech-report}.

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

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

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

  1050   \emph{target language}.  Inductive specifications can be executed

  1051   using the predicate compiler which operates within HOL.

  1052   See \cite{isabelle-codegen} for an introduction.

  1053

  1054   \begin{matharray}{rcl}

  1055     @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  1056     @{attribute_def (HOL) code} & : & @{text attribute} \\

  1057     @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\

  1058     @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\

  1059     @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  1060     @{attribute_def (HOL) code_inline} & : & @{text attribute} \\

  1061     @{attribute_def (HOL) code_post} & : & @{text attribute} \\

  1062     @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  1063     @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  1064     @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  1065     @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\

  1066     @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\

  1067     @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\

  1068     @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\

  1069     @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\

  1070     @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\

  1071     @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\

  1072     @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\

  1073     @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"}

  1074   \end{matharray}

  1075

  1076   \begin{rail}

  1077      'export_code' ( constexpr + ) \\

  1078        ( ( 'in' target ( 'module_name' string ) ? \\

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

  1080     ;

  1081

  1082     const: term

  1083     ;

  1084

  1085     constexpr: ( const | 'name._' | '_' )

  1086     ;

  1087

  1088     typeconstructor: nameref

  1089     ;

  1090

  1091     class: nameref

  1092     ;

  1093

  1094     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'

  1095     ;

  1096

  1097     'code' ( 'del' | 'abstype' | 'abstract' ) ?

  1098     ;

  1099

  1100     'code_abort' ( const + )

  1101     ;

  1102

  1103     'code_datatype' ( const + )

  1104     ;

  1105

  1106     'code_inline' ( 'del' ) ?

  1107     ;

  1108

  1109     'code_post' ( 'del' ) ?

  1110     ;

  1111

  1112     'code_thms' ( constexpr + ) ?

  1113     ;

  1114

  1115     'code_deps' ( constexpr + ) ?

  1116     ;

  1117

  1118     'code_const' (const + 'and') \\

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

  1120     ;

  1121

  1122     'code_type' (typeconstructor + 'and') \\

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

  1124     ;

  1125

  1126     'code_class' (class + 'and') \\

  1127       ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )

  1128     ;

  1129

  1130     'code_instance' (( typeconstructor '::' class ) + 'and') \\

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

  1132     ;

  1133

  1134     'code_reserved' target ( string + )

  1135     ;

  1136

  1137     'code_monad' const const target

  1138     ;

  1139

  1140     'code_include' target ( string ( string | '-') )

  1141     ;

  1142

  1143     'code_modulename' target ( ( string string ) + )

  1144     ;

  1145

  1146     'code_reflect' string \\

  1147       ( 'datatypes' ( string '=' ( '_' | ( string + '|' ) + 'and' ) ) ) ? \\

  1148       ( 'functions' ( string + ) ) ? ( 'file' string ) ?

  1149     ;

  1150

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

  1152     ;

  1153

  1154   \end{rail}

  1155

  1156   \begin{description}

  1157

  1158   \item @{command (HOL) "export_code"} generates code for a given list

  1159   of constants in the specified target language(s).  If no

  1160   serialization instruction is given, only abstract code is generated

  1161   internally.

  1162

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

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

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

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

  1167

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

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

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

  1171   placed in this module.

  1172

  1173   For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification

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

  1175   directory, where code is generated in multiple files reflecting the

  1176   module hierarchy.  Omitting the file specification denotes standard

  1177   output.

  1178

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

  1180   \emph{SML} and \emph{OCaml}, @{text no_signatures} omits

  1181   explicit module signatures.

  1182

  1183   For \emph{Haskell} a module name prefix may be given using the

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

  1185   @{verbatim "deriving (Read, Show)"}'' clause to each appropriate

  1186   datatype declaration.

  1187

  1188   \item @{attribute (HOL) code} explicitly selects (or with option

  1189   @{text "del"}'' deselects) a code equation for code generation.

  1190   Usually packages introducing code equations provide a reasonable

  1191   default setup for selection.  Variants @{text "code abstype"} and

  1192   @{text "code abstract"} declare abstract datatype certificates or

  1193   code equations on abstract datatype representations respectively.

  1194

  1195   \item @{command (HOL) "code_abort"} declares constants which are not

  1196   required to have a definition by means of code equations; if needed

  1197   these are implemented by program abort instead.

  1198

  1199   \item @{command (HOL) "code_datatype"} specifies a constructor set

  1200   for a logical type.

  1201

  1202   \item @{command (HOL) "print_codesetup"} gives an overview on

  1203   selected code equations and code generator datatypes.

  1204

  1205   \item @{attribute (HOL) code_inline} declares (or with option

  1206   @{text "del"}'' removes) inlining theorems which are applied as

  1207   rewrite rules to any code equation during preprocessing.

  1208

  1209   \item @{attribute (HOL) code_post} declares (or with option @{text

  1210   "del"}'' removes) theorems which are applied as rewrite rules to any

  1211   result of an evaluation.

  1212

  1213   \item @{command (HOL) "print_codeproc"} prints the setup of the code

  1214   generator preprocessor.

  1215

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

  1217   representing the corresponding program containing all given

  1218   constants after preprocessing.

  1219

  1220   \item @{command (HOL) "code_deps"} visualizes dependencies of

  1221   theorems representing the corresponding program containing all given

  1222   constants after preprocessing.

  1223

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

  1225   with target-specific serializations; omitting a serialization

  1226   deletes an existing serialization.

  1227

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

  1229   constructors with target-specific serializations; omitting a

  1230   serialization deletes an existing serialization.

  1231

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

  1233   with target-specific class names; omitting a serialization deletes

  1234   an existing serialization.  This applies only to \emph{Haskell}.

  1235

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

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

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

  1239   already present'' declaration.  This applies only to

  1240   \emph{Haskell}.

  1241

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

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

  1244   generated code.

  1245

  1246   \item @{command (HOL) "code_monad"} provides an auxiliary mechanism

  1247   to generate monadic code for Haskell.

  1248

  1249   \item @{command (HOL) "code_include"} adds arbitrary named content

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

  1251   will remove an already added include''.

  1252

  1253   \item @{command (HOL) "code_modulename"} declares aliasings from one

  1254   module name onto another.

  1255

  1256   \item @{command (HOL) "code_reflect"} without a @{text "file"}''

  1257   argument compiles code into the system runtime environment and

  1258   modifies the code generator setup that future invocations of system

  1259   runtime code generation referring to one of the @{text

  1260   "datatypes"}'' or @{text "functions"}'' entities use these precompiled

  1261   entities.  With a @{text "file"}'' argument, the corresponding code

  1262   is generated into that specified file without modifying the code

  1263   generator setup.

  1264

  1265   \end{description}

  1266

  1267   The other framework generates code from both functional and

  1268   relational programs to SML.  See \cite{isabelle-HOL} for further

  1269   information (this actually covers the new-style theory format as

  1270   well).

  1271

  1272   \begin{matharray}{rcl}

  1273     @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\

  1274     @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\

  1275     @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\

  1276     @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\

  1277     @{attribute_def (HOL) code} & : & @{text attribute} \\

  1278   \end{matharray}

  1279

  1280   \begin{rail}

  1281   ( 'code_module' | 'code_library' ) modespec ? name ? \\

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

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

  1284   ;

  1285

  1286   modespec: '(' ( name * ) ')'

  1287   ;

  1288

  1289   'consts_code' (codespec +)

  1290   ;

  1291

  1292   codespec: const template attachment ?

  1293   ;

  1294

  1295   'types_code' (tycodespec +)

  1296   ;

  1297

  1298   tycodespec: name template attachment ?

  1299   ;

  1300

  1301   const: term

  1302   ;

  1303

  1304   template: '(' string ')'

  1305   ;

  1306

  1307   attachment: 'attach' modespec ? verblbrace text verbrbrace

  1308   ;

  1309

  1310   'code' (name)?

  1311   ;

  1312   \end{rail}

  1313

  1314 *}

  1315

  1316

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

  1318

  1319 text {*

  1320   \begin{matharray}{rcl}

  1321     @{command_def (HOL) "specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\

  1322     @{command_def (HOL) "ax_specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\

  1323   \end{matharray}

  1324

  1325   \begin{rail}

  1326   ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)

  1327   ;

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

  1329   \end{rail}

  1330

  1331   \begin{description}

  1332

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

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

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

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

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

  1338   constants.

  1339

  1340   \item @{command (HOL) "ax_specification"}~@{text "decls \<phi>"} sets up

  1341   a goal stating the existence of terms with the properties specified

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

  1343   the proof, the theory will be augmented with axioms expressing the

  1344   properties given in the first place.

  1345

  1346   \item @{text decl} declares a constant to be defined by the

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

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

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

  1350

  1351   \end{description}

  1352

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

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

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

  1356   construction cannot introduce inconsistencies, whereas @{command

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

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

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

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

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

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

  1363 *}

  1364

  1365 end