doc-src/IsarRef/Thy/HOL_Specific.thy
 author bulwahn Fri Oct 29 08:44:43 2010 +0200 (2010-10-29) changeset 40245 59f011c1877a parent 40171 1fa547166a1d child 40254 6d1ebaa7a4ba permissions -rw-r--r--
updating documentation on quickcheck in the Isar reference
     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' ((( name * ) + 'and') | ('(' 'complete' ')'))

    76     ;

    77   \end{rail}

    78

    79   \begin{description}

    80

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

    82   \<AND> q\<^sub>1 \<dots> q\<^sub>n"} puts expressions of low-level tuple types into

    83   canonical form as specified by the arguments given; the @{text i}-th

    84   collection of arguments refers to occurrences in premise @{text i}

    85   of the rule.  The @{text "(complete)"}'' option causes \emph{all}

    86   arguments in function applications to be represented canonically

    87   according to their tuple type structure.

    88

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

    90   parameters to be introduced.

    91

    92   \end{description}

    93 *}

    94

    95

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

    97

    98 text {*

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

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

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

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

   103   admits operations that are polymorphic with respect to record

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

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

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

   107 *}

   108

   109

   110 subsection {* Basic concepts *}

   111

   112 text {*

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

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

   115

   116   \begin{center}

   117   \begin{tabular}{l|l|l}

   118     & record terms & record types \\ \hline

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

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

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

   122   \end{tabular}

   123   \end{center}

   124

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

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

   127

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

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

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

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

   132

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

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

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

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

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

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

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

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

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

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

   143   Fixed records are special instances of record schemes, where

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

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

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

   147

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

   149   typed language like HOL work out:

   150

   151   \begin{enumerate}

   152

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

   154   variable,

   155

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

   157   the logic as first-class values.

   158

   159   \end{enumerate}

   160

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

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

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

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

   165   The record package provides several standard operations like

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

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

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

   169   records in practice.

   170 *}

   171

   172

   173 subsection {* Record specifications *}

   174

   175 text {*

   176   \begin{matharray}{rcl}

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

   178   \end{matharray}

   179

   180   \begin{rail}

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

   182     ;

   183   \end{rail}

   184

   185   \begin{description}

   186

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

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

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

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

   191

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

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

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

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

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

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

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

   199   the record name internally.

   200

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

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

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

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

   205   merge multiple parent records!

   206

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

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

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

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

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

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

   213

   214   \end{description}

   215 *}

   216

   217

   218 subsection {* Record operations *}

   219

   220 text {*

   221   Any record definition of the form presented above produces certain

   222   standard operations.  Selectors and updates are provided for any

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

   224   cumulative record constructor functions.  To simplify the

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

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

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

   228

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

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

   231

   232   \begin{matharray}{lll}

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

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

   235   \end{matharray}

   236

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

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

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

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

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

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

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

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

   245   Thus commutativity of independent updates can be proven within the

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

   247

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

   249   constructor function:

   250

   251   \begin{matharray}{lll}

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

   253   \end{matharray}

   254

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

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

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

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

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

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

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

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

   263   the above record operations will get the following types:

   264

   265   \medskip

   266   \begin{tabular}{lll}

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

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

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

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

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

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

   273   \end{tabular}

   274   \medskip

   275

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

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

   278   record fragment consisting of exactly the new fields introduced here

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

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

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

   282

   283   \medskip

   284   \begin{tabular}{lll}

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

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

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

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

   289   \end{tabular}

   290   \medskip

   291

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

   293   for root records.

   294 *}

   295

   296

   297 subsection {* Derived rules and proof tools *}

   298

   299 text {*

   300   The record package proves several results internally, declaring

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

   302   reason about record structures quite conveniently.  Assume that

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

   304

   305   \begin{enumerate}

   306

   307   \item Standard conversions for selectors or updates applied to

   308   record constructor terms are made part of the default Simplifier

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

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

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

   312

   313   \item Selectors applied to updated records are automatically reduced

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

   315   standard Simplifier setup.

   316

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

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

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

   320   @{text "t.iffs"}.

   321

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

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

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

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

   326

   327   \item Representations of arbitrary record expressions as canonical

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

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

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

   331   fixed records, record schemes, more parts etc.

   332

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

   334   sensible rule according to the type of the indicated record

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

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

   337

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

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

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

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

   342

   343   \end{enumerate}

   344 *}

   345

   346

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

   348

   349 text {*

   350   \begin{matharray}{rcl}

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

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

   353   \end{matharray}

   354

   355   \begin{rail}

   356     'datatype' (dtspec + 'and')

   357     ;

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

   359     ;

   360

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

   362     ;

   363     cons: name ( type * ) mixfix?

   364   \end{rail}

   365

   366   \begin{description}

   367

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

   369   HOL.

   370

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

   372   inductive ones, generating the standard infrastructure of derived

   373   concepts (primitive recursion etc.).

   374

   375   \end{description}

   376

   377   The induction and exhaustion theorems generated provide case names

   378   according to the constructors involved, while parameters are named

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

   380

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

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

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

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

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

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

   387   internally bound parameters).

   388 *}

   389

   390

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

   392

   393 text {*

   394   \begin{matharray}{rcl}

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

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

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

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

   399   \end{matharray}

   400

   401   \begin{rail}

   402     'primrec' target? fixes 'where' equations

   403     ;

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

   405     ;

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

   407     ;

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

   409     ;

   410     'termination' ( term )?

   411   \end{rail}

   412

   413   \begin{description}

   414

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

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

   417

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

   419   wellfounded recursion. A detailed description with examples can be

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

   421   set of (possibly conditional) recursive equations with arbitrary

   422   pattern matching. The command generates proof obligations for the

   423   completeness and the compatibility of patterns.

   424

   425   The defined function is considered partial, and the resulting

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

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

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

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

   430

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

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

   433   proof attempts regarding pattern matching and termination.  See

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

   435

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

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

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

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

   440   the induction principle is established.

   441

   442   \end{description}

   443

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

   445   command accommodate

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

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

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

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

   450

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

   452   with structural recursion on the datatype the recursion is carried

   453   out.

   454

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

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

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

   458   explicitly as well.

   459

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

   461   options.

   462

   463   \begin{description}

   464

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

   466   overlapping patterns by making them mutually disjoint.  Earlier

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

   468   specification in a format very similar to functional programming.

   469   Note that the resulting simplification and induction rules

   470   correspond to the transformed specification, not the one given

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

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

   473   transformation only works for ML-style datatype patterns.

   474

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

   476   introduction rules for the domain predicate. While mostly not

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

   478

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

   480   equations even without a termination proof, provided that the

   481   function is tail-recursive. This currently only works

   482

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

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

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

   486

   487   \end{description}

   488 *}

   489

   490

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

   492

   493 text {*

   494   \begin{matharray}{rcl}

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

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

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

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

   499   \end{matharray}

   500

   501   \begin{rail}

   502     'relation' term

   503     ;

   504     'lexicographic\_order' ( clasimpmod * )

   505     ;

   506     'size\_change' ( orders ( clasimpmod * ) )

   507     ;

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

   509   \end{rail}

   510

   511   \begin{description}

   512

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

   514   solve goals regarding the completeness of pattern matching, as

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

   516   \cite{isabelle-function}).

   517

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

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

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

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

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

   523   termination proofs.

   524

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

   526   automated termination proof by searching for a lexicographic

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

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

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

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

   531   \secref{sec:clasimp}.

   532

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

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

   535

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

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

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

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

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

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

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

   543   internally.

   544

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

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

   547

   548   \end{description}

   549 *}

   550

   551 subsection {* Functions with explicit partiality *}

   552

   553 text {*

   554   \begin{matharray}{rcl}

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

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

   557   \end{matharray}

   558

   559   \begin{rail}

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

   561   \end{rail}

   562

   563   \begin{description}

   564

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

   566   functions based on fixpoints in complete partial orders. No

   567   termination proof is required from the user or constructed

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

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

   570   element.

   571

   572   Pattern matching and mutual recursion are currently not supported.

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

   574   single recursive equation.

   575

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

   577   function, but the induced functional must be provably monotonic

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

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

   580   can be influenced by declaring hints using the

   581   @{attribute (HOL) partial_function_mono} attribute.

   582

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

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

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

   586   defined:

   587

   588   \begin{description}

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

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

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

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

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

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

   595

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

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

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

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

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

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

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

   603   definition of arbitrary tail-recursive functions.

   604   \end{description}

   605

   606   Experienced users may define new modes by instantiating the locale

   607   @{const "partial_function_definitions"} appropriately.

   608

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

   610   use in the internal monononicity proofs of partial function

   611   definitions.

   612

   613   \end{description}

   614

   615 *}

   616

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

   618

   619 text {*

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

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

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

   623

   624   \begin{matharray}{rcl}

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

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

   627   \end{matharray}

   628

   629   \begin{rail}

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

   631     ;

   632     recdeftc thmdecl? tc

   633     ;

   634     hints: '(' 'hints' ( recdefmod * ) ')'

   635     ;

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

   637     ;

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

   639     ;

   640   \end{rail}

   641

   642   \begin{description}

   643

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

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

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

   647   TFL to recover from failed proof attempts, returning unfinished

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

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

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

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

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

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

   654

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

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

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

   658   constant @{text c}.

   659

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

   661   its internal proofs without manual intervention.

   662

   663   \end{description}

   664

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

   666   globally, using the following attributes.

   667

   668   \begin{matharray}{rcl}

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

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

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

   672   \end{matharray}

   673

   674   \begin{rail}

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

   676     ;

   677   \end{rail}

   678 *}

   679

   680

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

   682

   683 text {*

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

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

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

   687   structural operational semantics is an inductive definition of an

   688   evaluation relation.

   689

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

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

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

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

   694   relations to formalise equivalence of processes and infinite data

   695   structures.

   696

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

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

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

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

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

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

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

   704   to use inference rules for type-checking.

   705

   706   \begin{matharray}{rcl}

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

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

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

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

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

   712   \end{matharray}

   713

   714   \begin{rail}

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

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

   717     ;

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

   719     ;

   720     'mono' (() | 'add' | 'del')

   721     ;

   722   \end{rail}

   723

   724   \begin{description}

   725

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

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

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

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

   730   (co)inductive predicates that remain fixed throughout the

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

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

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

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

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

   736

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

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

   739   allowing the definition of (co)inductive sets.

   740

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

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

   743   (HOL) "inductive"}.

   744

   745   \end{description}

   746 *}

   747

   748

   749 subsection {* Derived rules *}

   750

   751 text {*

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

   753   theory and also proves some theorems:

   754

   755   \begin{description}

   756

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

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

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

   760   theory file;

   761

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

   763

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

   765   rule.

   766

   767   \end{description}

   768

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

   770   defined simultaneously, the list of introduction rules is called

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

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

   773   of mutual induction rules is called @{text

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

   775 *}

   776

   777

   778 subsection {* Monotonicity theorems *}

   779

   780 text {*

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

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

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

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

   785   theorems may be added:

   786

   787   \begin{itemize}

   788

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

   790   monotonicity of inductive definitions whose introduction rules have

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

   792

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

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

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

   796   $  797 \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"}}   798$

   799

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

   801   of expressions, e.g.

   802   $  803 @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad   804 @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}   805$

   806

   807   \item Equations for reducing complex operators to more primitive

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

   809   $  810 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad   811 @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}   812$

   813

   814   \end{itemize}

   815

   816   %FIXME: Example of an inductive definition

   817 *}

   818

   819

   820 section {* Arithmetic proof support *}

   821

   822 text {*

   823   \begin{matharray}{rcl}

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

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

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

   827   \end{matharray}

   828

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

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

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

   832

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

   834   always supplied to the arithmetic provers implicitly.

   835

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

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

   838

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

   840   already invoked by the Simplifier.

   841 *}

   842

   843

   844 section {* Intuitionistic proof search *}

   845

   846 text {*

   847   \begin{matharray}{rcl}

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

   849   \end{matharray}

   850

   851   \begin{rail}

   852     'iprover' ( rulemod * )

   853     ;

   854   \end{rail}

   855

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

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

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

   859   goal before commencing proof search.

   860

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

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

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

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

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

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

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

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

   869 *}

   870

   871

   872 section {* Coherent Logic *}

   873

   874 text {*

   875   \begin{matharray}{rcl}

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

   877   \end{matharray}

   878

   879   \begin{rail}

   880     'coherent' thmrefs?

   881     ;

   882   \end{rail}

   883

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

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

   886   applications in confluence theory, lattice theory and projective

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

   888   examples.

   889 *}

   890

   891

   892 section {* Checking and refuting propositions *}

   893

   894 text {*

   895   Identifying incorrect propositions usually involves evaluation of

   896   particular assignments and systematic counter example search.  This

   897   is supported by the following commands.

   898

   899   \begin{matharray}{rcl}

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

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

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

   903   \end{matharray}

   904

   905   \begin{rail}

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

   907     ;

   908

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

   910     ;

   911

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

   913     ;

   914

   915     modes: '(' (name + ) ')'

   916     ;

   917

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

   919     ;

   920   \end{rail}

   921

   922   \begin{description}

   923

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

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

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

   927     Internally, the evaluation is performed by registered evaluators,

   928     which are invoked sequentially until a result is returned.

   929     Alternatively a specific evaluator can be selected using square

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

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

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

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

   934

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

   936     counter examples using a series of arbitrary assignments for its

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

   938     can be selected explicitly using an optional goal index.

   939     A number of configuration options are supported for

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

   941

   942     \begin{description}

   943

   944       \item[size] specifies the maximum size of the search space for

   945         assignment values.

   946

   947       \item[iterations] sets how many sets of assignments are

   948         generated for each particular size.

   949

   950       \item[no\_assms] specifies whether assumptions in

   951         structured proofs should be ignored.

   952

   953       \item[timeout] sets the time limit in seconds.

   954

   955       \item[default\_type] sets the type(s) generally used to instantiate

   956         type variables.

   957

   958       \item[report] if set quickcheck reports how many tests fulfilled

   959         the preconditions.

   960

   961       \item[quiet] if not set quickcheck informs about the current size

   962         for assignment values.

   963

   964       \item[expect] can be used to check if the user's expectation was met

   965         (no\_expectation, no\_counterexample, or counterexample)

   966

   967     \end{description}

   968

   969     These option can be given within square brackets.

   970

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

   972     configuration options persitently.

   973

   974   \end{description}

   975 *}

   976

   977

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

   979

   980 text {*

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

   982   induction in unstructured tactic scripts; see also

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

   984

   985   \begin{matharray}{rcl}

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

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

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

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

   990   \end{matharray}

   991

   992   \begin{rail}

   993     'case\_tac' goalspec? term rule?

   994     ;

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

   996     ;

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

   998     ;

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

  1000     ;

  1001

  1002     rule: ('rule' ':' thmref)

  1003     ;

  1004   \end{rail}

  1005

  1006   \begin{description}

  1007

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

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

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

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

  1012   datatype} package already takes care of this.

  1013

  1014   These unstructured tactics feature both goal addressing and dynamic

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

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

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

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

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

  1020   being addressed.

  1021

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

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

  1024   mk_cases} operation.  Rules are simplified in an unrestricted

  1025   forward manner.

  1026

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

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

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

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

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

  1032   be generalized before applying the resulting rule.

  1033

  1034   \end{description}

  1035 *}

  1036

  1037

  1038 section {* Executable code *}

  1039

  1040 text {*

  1041   Isabelle/Pure provides two generic frameworks to support code

  1042   generation from executable specifications.  Isabelle/HOL

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

  1044   applications.

  1045

  1046   \medskip One framework generates code from functional programs

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

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

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

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

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

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

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

  1054   using the predicate compiler which operates within HOL.

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

  1056

  1057   \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1077   \end{matharray}

  1078

  1079   \begin{rail}

  1080      'export\_code' ( constexpr + ) \\

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

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

  1083     ;

  1084

  1085     const: term

  1086     ;

  1087

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

  1089     ;

  1090

  1091     typeconstructor: nameref

  1092     ;

  1093

  1094     class: nameref

  1095     ;

  1096

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

  1098     ;

  1099

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

  1101     ;

  1102

  1103     'code\_abort' ( const + )

  1104     ;

  1105

  1106     'code\_datatype' ( const + )

  1107     ;

  1108

  1109     'code_inline' ( 'del' ) ?

  1110     ;

  1111

  1112     'code_post' ( 'del' ) ?

  1113     ;

  1114

  1115     'code\_thms' ( constexpr + ) ?

  1116     ;

  1117

  1118     'code\_deps' ( constexpr + ) ?

  1119     ;

  1120

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

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

  1123     ;

  1124

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

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

  1127     ;

  1128

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

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

  1131     ;

  1132

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

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

  1135     ;

  1136

  1137     'code\_reserved' target ( string + )

  1138     ;

  1139

  1140     'code\_monad' const const target

  1141     ;

  1142

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

  1144     ;

  1145

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

  1147     ;

  1148

  1149     'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\

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

  1151     ;

  1152

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

  1154     ;

  1155

  1156   \end{rail}

  1157

  1158   \begin{description}

  1159

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

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

  1162   serialization instruction is given, only abstract code is generated

  1163   internally.

  1164

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

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

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

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

  1169

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

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

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

  1173   placed in this module.

  1174

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

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

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

  1178   module hierarchy.  Omitting the file specification denotes standard

  1179   output.

  1180

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

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

  1183   explicit module signatures.

  1184

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

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

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

  1188   datatype declaration.

  1189

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

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

  1192   Usually packages introducing code equations provide a reasonable

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

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

  1195   code equations on abstract datatype representations respectively.

  1196

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

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

  1199   these are implemented by program abort instead.

  1200

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

  1202   for a logical type.

  1203

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

  1205   selected code equations and code generator datatypes.

  1206

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

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

  1209   rewrite rules to any code equation during preprocessing.

  1210

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

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

  1213   result of an evaluation.

  1214

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

  1216   generator preprocessor.

  1217

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

  1219   representing the corresponding program containing all given

  1220   constants after preprocessing.

  1221

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

  1223   theorems representing the corresponding program containing all given

  1224   constants after preprocessing.

  1225

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

  1227   with target-specific serializations; omitting a serialization

  1228   deletes an existing serialization.

  1229

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

  1231   constructors with target-specific serializations; omitting a

  1232   serialization deletes an existing serialization.

  1233

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

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

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

  1237

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

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

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

  1241   already present'' declaration.  This applies only to

  1242   \emph{Haskell}.

  1243

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

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

  1246   generated code.

  1247

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

  1249   to generate monadic code for Haskell.

  1250

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

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

  1253   will remove an already added include''.

  1254

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

  1256   module name onto another.

  1257

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

  1259   argument compiles code into the system runtime environment and

  1260   modifies the code generator setup that future invocations of system

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

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

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

  1264   is generated into that specified file without modifying the code

  1265   generator setup.

  1266

  1267   \end{description}

  1268

  1269   The other framework generates code from both functional and

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

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

  1272   well).

  1273

  1274   \begin{matharray}{rcl}

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

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

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

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

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

  1280   \end{matharray}

  1281

  1282   \begin{rail}

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

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

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

  1286   ;

  1287

  1288   modespec: '(' ( name * ) ')'

  1289   ;

  1290

  1291   'consts\_code' (codespec +)

  1292   ;

  1293

  1294   codespec: const template attachment ?

  1295   ;

  1296

  1297   'types\_code' (tycodespec +)

  1298   ;

  1299

  1300   tycodespec: name template attachment ?

  1301   ;

  1302

  1303   const: term

  1304   ;

  1305

  1306   template: '(' string ')'

  1307   ;

  1308

  1309   attachment: 'attach' modespec ? verblbrace text verbrbrace

  1310   ;

  1311

  1312   'code' (name)?

  1313   ;

  1314   \end{rail}

  1315

  1316 *}

  1317

  1318

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

  1320

  1321 text {*

  1322   \begin{matharray}{rcl}

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

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

  1325   \end{matharray}

  1326

  1327   \begin{rail}

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

  1329   ;

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

  1331   \end{rail}

  1332

  1333   \begin{description}

  1334

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

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

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

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

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

  1340   constants.

  1341

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

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

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

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

  1346   properties given in the first place.

  1347

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

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

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

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

  1352

  1353   \end{description}

  1354

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

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

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

  1358   construction cannot introduce inconsistencies, whereas @{command

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

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

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

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

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

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

  1365 *}

  1366

  1367 end