doc-src/IsarRef/Thy/HOL_Specific.thy
 author krauss Tue Oct 26 12:19:01 2010 +0200 (2010-10-26) changeset 40170 751121d5ca35 parent 39608 76bc7e4999f8 child 40171 1fa547166a1d permissions -rw-r--r--
remove outdated "(otherwise)" syntax from manual
     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

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

   553

   554 text {*

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

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

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

   558

   559   \begin{matharray}{rcl}

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

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

   562   \end{matharray}

   563

   564   \begin{rail}

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

   566     ;

   567     recdeftc thmdecl? tc

   568     ;

   569     hints: '(' 'hints' ( recdefmod * ) ')'

   570     ;

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

   572     ;

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

   574     ;

   575   \end{rail}

   576

   577   \begin{description}

   578

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

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

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

   582   TFL to recover from failed proof attempts, returning unfinished

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

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

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

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

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

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

   589

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

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

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

   593   constant @{text c}.

   594

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

   596   its internal proofs without manual intervention.

   597

   598   \end{description}

   599

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

   601   globally, using the following attributes.

   602

   603   \begin{matharray}{rcl}

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

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

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

   607   \end{matharray}

   608

   609   \begin{rail}

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

   611     ;

   612   \end{rail}

   613 *}

   614

   615

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

   617

   618 text {*

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

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

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

   622   structural operational semantics is an inductive definition of an

   623   evaluation relation.

   624

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

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

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

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

   629   relations to formalise equivalence of processes and infinite data

   630   structures.

   631

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

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

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

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

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

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

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

   639   to use inference rules for type-checking.

   640

   641   \begin{matharray}{rcl}

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

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

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

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

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

   647   \end{matharray}

   648

   649   \begin{rail}

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

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

   652     ;

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

   654     ;

   655     'mono' (() | 'add' | 'del')

   656     ;

   657   \end{rail}

   658

   659   \begin{description}

   660

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

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

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

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

   665   (co)inductive predicates that remain fixed throughout the

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

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

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

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

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

   671

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

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

   674   allowing the definition of (co)inductive sets.

   675

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

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

   678   (HOL) "inductive"}.

   679

   680   \end{description}

   681 *}

   682

   683

   684 subsection {* Derived rules *}

   685

   686 text {*

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

   688   theory and also proves some theorems:

   689

   690   \begin{description}

   691

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

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

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

   695   theory file;

   696

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

   698

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

   700   rule.

   701

   702   \end{description}

   703

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

   705   defined simultaneously, the list of introduction rules is called

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

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

   708   of mutual induction rules is called @{text

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

   710 *}

   711

   712

   713 subsection {* Monotonicity theorems *}

   714

   715 text {*

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

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

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

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

   720   theorems may be added:

   721

   722   \begin{itemize}

   723

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

   725   monotonicity of inductive definitions whose introduction rules have

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

   727

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

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

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

   731   $  732 \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"}}   733$

   734

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

   736   of expressions, e.g.

   737   $  738 @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad   739 @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}   740$

   741

   742   \item Equations for reducing complex operators to more primitive

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

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

   748

   749   \end{itemize}

   750

   751   %FIXME: Example of an inductive definition

   752 *}

   753

   754

   755 section {* Arithmetic proof support *}

   756

   757 text {*

   758   \begin{matharray}{rcl}

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

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

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

   762   \end{matharray}

   763

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

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

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

   767

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

   769   always supplied to the arithmetic provers implicitly.

   770

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

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

   773

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

   775   already invoked by the Simplifier.

   776 *}

   777

   778

   779 section {* Intuitionistic proof search *}

   780

   781 text {*

   782   \begin{matharray}{rcl}

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

   784   \end{matharray}

   785

   786   \begin{rail}

   787     'iprover' ( rulemod * )

   788     ;

   789   \end{rail}

   790

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

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

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

   794   goal before commencing proof search.

   795

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

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

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

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

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

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

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

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

   804 *}

   805

   806

   807 section {* Coherent Logic *}

   808

   809 text {*

   810   \begin{matharray}{rcl}

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

   812   \end{matharray}

   813

   814   \begin{rail}

   815     'coherent' thmrefs?

   816     ;

   817   \end{rail}

   818

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

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

   821   applications in confluence theory, lattice theory and projective

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

   823   examples.

   824 *}

   825

   826

   827 section {* Checking and refuting propositions *}

   828

   829 text {*

   830   Identifying incorrect propositions usually involves evaluation of

   831   particular assignments and systematic counter example search.  This

   832   is supported by the following commands.

   833

   834   \begin{matharray}{rcl}

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

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

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

   838   \end{matharray}

   839

   840   \begin{rail}

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

   842     ;

   843

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

   845     ;

   846

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

   848     ;

   849

   850     modes: '(' (name + ) ')'

   851     ;

   852

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

   854     ;

   855   \end{rail}

   856

   857   \begin{description}

   858

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

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

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

   862     Internally, the evaluation is performed by registered evaluators,

   863     which are invoked sequentially until a result is returned.

   864     Alternatively a specific evaluator can be selected using square

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

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

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

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

   869

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

   871     counter examples using a series of arbitrary assignments for its

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

   873     can be selected explicitly using an optional goal index.

   874     A number of configuration options are supported for

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

   876

   877     \begin{description}

   878

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

   880         assignment values.

   881

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

   883         generated for each particular size.

   884

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

   886         structured proofs should be ignored.

   887

   888     \end{description}

   889

   890     These option can be given within square brackets.

   891

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

   893     configuration options persitently.

   894

   895   \end{description}

   896 *}

   897

   898

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

   900

   901 text {*

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

   903   induction in unstructured tactic scripts; see also

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

   905

   906   \begin{matharray}{rcl}

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

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

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

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

   911   \end{matharray}

   912

   913   \begin{rail}

   914     'case\_tac' goalspec? term rule?

   915     ;

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

   917     ;

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

   919     ;

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

   921     ;

   922

   923     rule: ('rule' ':' thmref)

   924     ;

   925   \end{rail}

   926

   927   \begin{description}

   928

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

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

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

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

   933   datatype} package already takes care of this.

   934

   935   These unstructured tactics feature both goal addressing and dynamic

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

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

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

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

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

   941   being addressed.

   942

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

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

   945   mk_cases} operation.  Rules are simplified in an unrestricted

   946   forward manner.

   947

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

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

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

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

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

   953   be generalized before applying the resulting rule.

   954

   955   \end{description}

   956 *}

   957

   958

   959 section {* Executable code *}

   960

   961 text {*

   962   Isabelle/Pure provides two generic frameworks to support code

   963   generation from executable specifications.  Isabelle/HOL

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

   965   applications.

   966

   967   \medskip One framework generates code from functional programs

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

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

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

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

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

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

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

   975   using the predicate compiler which operates within HOL.

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

   977

   978   \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   998   \end{matharray}

   999

  1000   \begin{rail}

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

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

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

  1004     ;

  1005

  1006     const: term

  1007     ;

  1008

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

  1010     ;

  1011

  1012     typeconstructor: nameref

  1013     ;

  1014

  1015     class: nameref

  1016     ;

  1017

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

  1019     ;

  1020

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

  1022     ;

  1023

  1024     'code\_abort' ( const + )

  1025     ;

  1026

  1027     'code\_datatype' ( const + )

  1028     ;

  1029

  1030     'code_inline' ( 'del' ) ?

  1031     ;

  1032

  1033     'code_post' ( 'del' ) ?

  1034     ;

  1035

  1036     'code\_thms' ( constexpr + ) ?

  1037     ;

  1038

  1039     'code\_deps' ( constexpr + ) ?

  1040     ;

  1041

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

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

  1044     ;

  1045

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

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

  1048     ;

  1049

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

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

  1052     ;

  1053

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

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

  1056     ;

  1057

  1058     'code\_reserved' target ( string + )

  1059     ;

  1060

  1061     'code\_monad' const const target

  1062     ;

  1063

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

  1065     ;

  1066

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

  1068     ;

  1069

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

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

  1072     ;

  1073

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

  1075     ;

  1076

  1077   \end{rail}

  1078

  1079   \begin{description}

  1080

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

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

  1083   serialization instruction is given, only abstract code is generated

  1084   internally.

  1085

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

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

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

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

  1090

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

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

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

  1094   placed in this module.

  1095

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

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

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

  1099   module hierarchy.  Omitting the file specification denotes standard

  1100   output.

  1101

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

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

  1104   explicit module signatures.

  1105

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

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

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

  1109   datatype declaration.

  1110

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

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

  1113   Usually packages introducing code equations provide a reasonable

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

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

  1116   code equations on abstract datatype representations respectively.

  1117

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

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

  1120   these are implemented by program abort instead.

  1121

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

  1123   for a logical type.

  1124

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

  1126   selected code equations and code generator datatypes.

  1127

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

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

  1130   rewrite rules to any code equation during preprocessing.

  1131

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

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

  1134   result of an evaluation.

  1135

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

  1137   generator preprocessor.

  1138

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

  1140   representing the corresponding program containing all given

  1141   constants after preprocessing.

  1142

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

  1144   theorems representing the corresponding program containing all given

  1145   constants after preprocessing.

  1146

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

  1148   with target-specific serializations; omitting a serialization

  1149   deletes an existing serialization.

  1150

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

  1152   constructors with target-specific serializations; omitting a

  1153   serialization deletes an existing serialization.

  1154

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

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

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

  1158

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

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

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

  1162   already present'' declaration.  This applies only to

  1163   \emph{Haskell}.

  1164

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

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

  1167   generated code.

  1168

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

  1170   to generate monadic code for Haskell.

  1171

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

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

  1174   will remove an already added include''.

  1175

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

  1177   module name onto another.

  1178

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

  1180   argument compiles code into the system runtime environment and

  1181   modifies the code generator setup that future invocations of system

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

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

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

  1185   is generated into that specified file without modifying the code

  1186   generator setup.

  1187

  1188   \end{description}

  1189

  1190   The other framework generates code from both functional and

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

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

  1193   well).

  1194

  1195   \begin{matharray}{rcl}

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

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

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

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

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

  1201   \end{matharray}

  1202

  1203   \begin{rail}

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

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

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

  1207   ;

  1208

  1209   modespec: '(' ( name * ) ')'

  1210   ;

  1211

  1212   'consts\_code' (codespec +)

  1213   ;

  1214

  1215   codespec: const template attachment ?

  1216   ;

  1217

  1218   'types\_code' (tycodespec +)

  1219   ;

  1220

  1221   tycodespec: name template attachment ?

  1222   ;

  1223

  1224   const: term

  1225   ;

  1226

  1227   template: '(' string ')'

  1228   ;

  1229

  1230   attachment: 'attach' modespec ? verblbrace text verbrbrace

  1231   ;

  1232

  1233   'code' (name)?

  1234   ;

  1235   \end{rail}

  1236

  1237 *}

  1238

  1239

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

  1241

  1242 text {*

  1243   \begin{matharray}{rcl}

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

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

  1246   \end{matharray}

  1247

  1248   \begin{rail}

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

  1250   ;

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

  1252   \end{rail}

  1253

  1254   \begin{description}

  1255

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

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

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

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

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

  1261   constants.

  1262

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

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

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

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

  1267   properties given in the first place.

  1268

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

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

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

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

  1273

  1274   \end{description}

  1275

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

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

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

  1279   construction cannot introduce inconsistencies, whereas @{command

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

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

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

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

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

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

  1286 *}

  1287

  1288 end