doc-src/IsarRef/Thy/HOL_Specific.thy
 author haftmann Wed Jul 14 14:53:44 2010 +0200 (2010-07-14) changeset 37820 ffaca9167c16 parent 37749 c7e15d59c58d child 38462 34d3de1254cd permissions -rw-r--r--
export_code without file prints to standard output
     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     equations: (thmdecl? prop + '|')

   405     ;

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

   407     ;

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

   409     ;

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

   411     ;

   412     'termination' ( term )?

   413   \end{rail}

   414

   415   \begin{description}

   416

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

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

   419

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

   421   wellfounded recursion. A detailed description with examples can be

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

   423   set of (possibly conditional) recursive equations with arbitrary

   424   pattern matching. The command generates proof obligations for the

   425   completeness and the compatibility of patterns.

   426

   427   The defined function is considered partial, and the resulting

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

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

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

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

   432

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

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

   435   proof attempts regarding pattern matching and termination.  See

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

   437

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

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

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

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

   442   the induction principle is established.

   443

   444   \end{description}

   445

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

   447   command accommodate

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

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

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

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

   452

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

   454   with structural recursion on the datatype the recursion is carried

   455   out.

   456

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

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

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

   460   explicitly as well.

   461

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

   463   options.

   464

   465   \begin{description}

   466

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

   468   overlapping patterns by making them mutually disjoint.  Earlier

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

   470   specification in a format very similar to functional programming.

   471   Note that the resulting simplification and induction rules

   472   correspond to the transformed specification, not the one given

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

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

   475   transformation only works for ML-style datatype patterns.

   476

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

   478   introduction rules for the domain predicate. While mostly not

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

   480

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

   482   equations even without a termination proof, provided that the

   483   function is tail-recursive. This currently only works

   484

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

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

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

   488

   489   \end{description}

   490 *}

   491

   492

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

   494

   495 text {*

   496   \begin{matharray}{rcl}

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

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

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

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

   501   \end{matharray}

   502

   503   \begin{rail}

   504     'relation' term

   505     ;

   506     'lexicographic\_order' ( clasimpmod * )

   507     ;

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

   509     ;

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

   511   \end{rail}

   512

   513   \begin{description}

   514

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

   516   solve goals regarding the completeness of pattern matching, as

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

   518   \cite{isabelle-function}).

   519

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

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

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

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

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

   525   termination proofs.

   526

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

   528   automated termination proof by searching for a lexicographic

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

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

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

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

   533   \secref{sec:clasimp}.

   534

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

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

   537

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

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

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

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

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

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

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

   545   internally.

   546

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

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

   549

   550   \end{description}

   551 *}

   552

   553

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

   555

   556 text {*

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

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

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

   560

   561   \begin{matharray}{rcl}

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

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

   564   \end{matharray}

   565

   566   \begin{rail}

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

   568     ;

   569     recdeftc thmdecl? tc

   570     ;

   571     hints: '(' 'hints' ( recdefmod * ) ')'

   572     ;

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

   574     ;

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

   576     ;

   577   \end{rail}

   578

   579   \begin{description}

   580

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

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

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

   584   TFL to recover from failed proof attempts, returning unfinished

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

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

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

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

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

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

   591

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

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

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

   595   constant @{text c}.

   596

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

   598   its internal proofs without manual intervention.

   599

   600   \end{description}

   601

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

   603   globally, using the following attributes.

   604

   605   \begin{matharray}{rcl}

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

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

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

   609   \end{matharray}

   610

   611   \begin{rail}

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

   613     ;

   614   \end{rail}

   615 *}

   616

   617

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

   619

   620 text {*

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

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

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

   624   structural operational semantics is an inductive definition of an

   625   evaluation relation.

   626

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

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

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

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

   631   relations to formalise equivalence of processes and infinite data

   632   structures.

   633

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

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

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

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

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

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

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

   641   to use inference rules for type-checking.

   642

   643   \begin{matharray}{rcl}

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

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

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

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

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

   649   \end{matharray}

   650

   651   \begin{rail}

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

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

   654     ;

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

   656     ;

   657     'mono' (() | 'add' | 'del')

   658     ;

   659   \end{rail}

   660

   661   \begin{description}

   662

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

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

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

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

   667   (co)inductive predicates that remain fixed throughout the

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

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

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

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

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

   673

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

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

   676   allowing the definition of (co)inductive sets.

   677

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

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

   680   (HOL) "inductive"}.

   681

   682   \end{description}

   683 *}

   684

   685

   686 subsection {* Derived rules *}

   687

   688 text {*

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

   690   theory and also proves some theorems:

   691

   692   \begin{description}

   693

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

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

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

   697   theory file;

   698

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

   700

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

   702   rule.

   703

   704   \end{description}

   705

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

   707   defined simultaneously, the list of introduction rules is called

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

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

   710   of mutual induction rules is called @{text

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

   712 *}

   713

   714

   715 subsection {* Monotonicity theorems *}

   716

   717 text {*

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

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

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

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

   722   theorems may be added:

   723

   724   \begin{itemize}

   725

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

   727   monotonicity of inductive definitions whose introduction rules have

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

   729

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

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

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

   733   $  734 \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"}}   735$

   736

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

   738   of expressions, e.g.

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

   743

   744   \item Equations for reducing complex operators to more primitive

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

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

   750

   751   \end{itemize}

   752

   753   %FIXME: Example of an inductive definition

   754 *}

   755

   756

   757 section {* Arithmetic proof support *}

   758

   759 text {*

   760   \begin{matharray}{rcl}

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

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

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

   764   \end{matharray}

   765

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

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

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

   769

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

   771   always supplied to the arithmetic provers implicitly.

   772

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

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

   775

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

   777   already invoked by the Simplifier.

   778 *}

   779

   780

   781 section {* Intuitionistic proof search *}

   782

   783 text {*

   784   \begin{matharray}{rcl}

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

   786   \end{matharray}

   787

   788   \begin{rail}

   789     'iprover' ( rulemod * )

   790     ;

   791   \end{rail}

   792

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

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

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

   796   goal before commencing proof search.

   797

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

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

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

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

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

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

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

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

   806 *}

   807

   808

   809 section {* Coherent Logic *}

   810

   811 text {*

   812   \begin{matharray}{rcl}

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

   814   \end{matharray}

   815

   816   \begin{rail}

   817     'coherent' thmrefs?

   818     ;

   819   \end{rail}

   820

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

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

   823   applications in confluence theory, lattice theory and projective

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

   825   examples.

   826 *}

   827

   828

   829 section {* Checking and refuting propositions *}

   830

   831 text {*

   832   Identifying incorrect propositions usually involves evaluation of

   833   particular assignments and systematic counter example search.  This

   834   is supported by the following commands.

   835

   836   \begin{matharray}{rcl}

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

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

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

   840   \end{matharray}

   841

   842   \begin{rail}

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

   844     ;

   845

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

   847     ;

   848

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

   850     ;

   851

   852     modes: '(' (name + ) ')'

   853     ;

   854

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

   856     ;

   857   \end{rail}

   858

   859   \begin{description}

   860

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

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

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

   864     Internally, the evaluation is performed by registered evaluators,

   865     which are invoked sequentially until a result is returned.

   866     Alternatively a specific evaluator can be selected using square

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

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

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

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

   871

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

   873     counter examples using a series of arbitrary assignments for its

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

   875     can be selected explicitly using an optional goal index.

   876     A number of configuration options are supported for

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

   878

   879     \begin{description}

   880

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

   882         assignment values.

   883

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

   885         generated for each particular size.

   886

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

   888         structured proofs should be ignored.

   889

   890     \end{description}

   891

   892     These option can be given within square brackets.

   893

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

   895     configuration options persitently.

   896

   897   \end{description}

   898 *}

   899

   900

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

   902

   903 text {*

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

   905   induction in unstructured tactic scripts; see also

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

   907

   908   \begin{matharray}{rcl}

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

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

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

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

   913   \end{matharray}

   914

   915   \begin{rail}

   916     'case\_tac' goalspec? term rule?

   917     ;

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

   919     ;

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

   921     ;

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

   923     ;

   924

   925     rule: ('rule' ':' thmref)

   926     ;

   927   \end{rail}

   928

   929   \begin{description}

   930

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

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

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

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

   935   datatype} package already takes care of this.

   936

   937   These unstructured tactics feature both goal addressing and dynamic

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

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

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

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

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

   943   being addressed.

   944

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

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

   947   mk_cases} operation.  Rules are simplified in an unrestricted

   948   forward manner.

   949

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

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

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

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

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

   955   be generalized before applying the resulting rule.

   956

   957   \end{description}

   958 *}

   959

   960

   961 section {* Executable code *}

   962

   963 text {*

   964   Isabelle/Pure provides two generic frameworks to support code

   965   generation from executable specifications.  Isabelle/HOL

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

   967   applications.

   968

   969   \medskip One framework generates code from functional programs

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

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

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

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

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

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

   976   using the predicate compiler which operates within HOL.

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

   978

   979   \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   997     @{command_def (HOL) "code_modulename"} & : & @{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: 'OCaml' | 'SML' | 'Haskell'

  1019     ;

  1020

  1021     'code' ( 'del' ) ?

  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     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string

  1071     ;

  1072

  1073   \end{rail}

  1074

  1075   \begin{description}

  1076

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

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

  1079   instruction is given, only abstract code is generated internally.

  1080

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

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

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

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

  1085

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

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

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

  1089   placed in this module.

  1090

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

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

  1093   where code is generated in multiple files reflecting the module

  1094   hierarchy.  Omitting the file specification denotes standard

  1095   output.

  1096

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

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

  1099   explicit module signatures.

  1100

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

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

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

  1104   declaration.

  1105

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

  1107   @{text "del"}'' deselects) a code equation for code

  1108   generation.  Usually packages introducing code equations provide

  1109   a reasonable default setup for selection.

  1110

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

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

  1113   needed these are implemented by program abort instead.

  1114

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

  1116   for a logical type.

  1117

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

  1119   selected code equations and code generator datatypes.

  1120

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

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

  1123   applied as rewrite rules to any code equation during

  1124   preprocessing.

  1125

  1126   \item @{attribute (HOL) code_post} declares (or with

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

  1128   applied as rewrite rules to any result of an evaluation.

  1129

  1130   \item @{command (HOL) "print_codeproc"} prints the setup

  1131   of the code generator preprocessor.

  1132

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

  1134   representing the corresponding program containing all given

  1135   constants after preprocessing.

  1136

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

  1138   theorems representing the corresponding program containing all given

  1139   constants after preprocessing.

  1140

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

  1142   with target-specific serializations; omitting a serialization

  1143   deletes an existing serialization.

  1144

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

  1146   constructors with target-specific serializations; omitting a

  1147   serialization deletes an existing serialization.

  1148

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

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

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

  1152

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

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

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

  1156   already present'' declaration.  This applies only to

  1157   \emph{Haskell}.

  1158

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

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

  1161   generated code.

  1162

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

  1164   to generate monadic code for Haskell.

  1165

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

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

  1168   will remove an already added include''.

  1169

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

  1171   module name onto another.

  1172

  1173   \end{description}

  1174

  1175   The other framework generates code from both functional and relational

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

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

  1178

  1179   \begin{matharray}{rcl}

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

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

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

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

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

  1185   \end{matharray}

  1186

  1187   \begin{rail}

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

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

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

  1191   ;

  1192

  1193   modespec: '(' ( name * ) ')'

  1194   ;

  1195

  1196   'consts\_code' (codespec +)

  1197   ;

  1198

  1199   codespec: const template attachment ?

  1200   ;

  1201

  1202   'types\_code' (tycodespec +)

  1203   ;

  1204

  1205   tycodespec: name template attachment ?

  1206   ;

  1207

  1208   const: term

  1209   ;

  1210

  1211   template: '(' string ')'

  1212   ;

  1213

  1214   attachment: 'attach' modespec ? verblbrace text verbrbrace

  1215   ;

  1216

  1217   'code' (name)?

  1218   ;

  1219   \end{rail}

  1220

  1221 *}

  1222

  1223

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

  1225

  1226 text {*

  1227   \begin{matharray}{rcl}

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

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

  1230   \end{matharray}

  1231

  1232   \begin{rail}

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

  1234   ;

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

  1236   \end{rail}

  1237

  1238   \begin{description}

  1239

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

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

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

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

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

  1245   constants.

  1246

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

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

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

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

  1251   properties given in the first place.

  1252

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

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

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

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

  1257

  1258   \end{description}

  1259

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

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

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

  1263   construction cannot introduce inconsistencies, whereas @{command

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

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

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

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

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

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

  1270 *}

  1271

  1272 end