doc-src/IsarRef/Thy/HOL_Specific.thy
 author krauss Sat Nov 06 00:10:32 2010 +0100 (2010-11-06) changeset 40388 cb9fd7dd641c parent 40255 9ffbc25e1606 child 40709 b29c70cd5c93 permissions -rw-r--r--
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
     1 theory HOL_Specific

     2 imports Main

     3 begin

     4

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

     6

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

     8

     9 text {*

    10   \begin{matharray}{rcl}

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

    12   \end{matharray}

    13

    14   \begin{rail}

    15     'typedef' altname? abstype '=' repset

    16     ;

    17

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

    19     ;

    20     abstype: typespecsorts mixfix?

    21     ;

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

    23     ;

    24   \end{rail}

    25

    26   \begin{description}

    27

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

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

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

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

    32

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

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

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

    36   multiple interpretations in target contexts.  Thus the established

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

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

    39

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

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

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

    43   declaration is used to suppress a separate constant definition

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

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

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

    47

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

    49   Abs_t_inverse} provide the most basic characterization as a

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

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

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

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

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

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

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

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

    58

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

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

    61   @{text t} as indicated before.

    62

    63   \end{description}

    64 *}

    65

    66

    67 section {* Adhoc tuples *}

    68

    69 text {*

    70   \begin{matharray}{rcl}

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

    72   \end{matharray}

    73

    74   \begin{rail}

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

    76     ;

    77   \end{rail}

    78

    79   \begin{description}

    80

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

    82   arguments in function applications to be represented canonically

    83   according to their tuple type structure.

    84

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

    86   parameters introduced.

    87

    88   \end{description}

    89 *}

    90

    91

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

    93

    94 text {*

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

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

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

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

    99   admits operations that are polymorphic with respect to record

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

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

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

   103 *}

   104

   105

   106 subsection {* Basic concepts *}

   107

   108 text {*

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

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

   111

   112   \begin{center}

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

   114     & record terms & record types \\ \hline

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

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

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

   118   \end{tabular}

   119   \end{center}

   120

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

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

   123

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

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

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

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

   128

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

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

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

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

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

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

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

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

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

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

   139   Fixed records are special instances of record schemes, where

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

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

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

   143

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

   145   typed language like HOL work out:

   146

   147   \begin{enumerate}

   148

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

   150   variable,

   151

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

   153   the logic as first-class values.

   154

   155   \end{enumerate}

   156

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

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

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

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

   161   The record package provides several standard operations like

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

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

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

   165   records in practice.

   166 *}

   167

   168

   169 subsection {* Record specifications *}

   170

   171 text {*

   172   \begin{matharray}{rcl}

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

   174   \end{matharray}

   175

   176   \begin{rail}

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

   178     ;

   179   \end{rail}

   180

   181   \begin{description}

   182

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

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

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

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

   187

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

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

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

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

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

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

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

   195   the record name internally.

   196

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

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

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

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

   201   merge multiple parent records!

   202

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

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

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

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

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

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

   209

   210   \end{description}

   211 *}

   212

   213

   214 subsection {* Record operations *}

   215

   216 text {*

   217   Any record definition of the form presented above produces certain

   218   standard operations.  Selectors and updates are provided for any

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

   220   cumulative record constructor functions.  To simplify the

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

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

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

   224

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

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

   227

   228   \begin{matharray}{lll}

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

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

   231   \end{matharray}

   232

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

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

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

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

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

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

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

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

   241   Thus commutativity of independent updates can be proven within the

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

   243

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

   245   constructor function:

   246

   247   \begin{matharray}{lll}

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

   249   \end{matharray}

   250

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

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

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

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

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

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

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

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

   259   the above record operations will get the following types:

   260

   261   \medskip

   262   \begin{tabular}{lll}

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

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

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

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

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

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

   269   \end{tabular}

   270   \medskip

   271

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

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

   274   record fragment consisting of exactly the new fields introduced here

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

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

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

   278

   279   \medskip

   280   \begin{tabular}{lll}

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

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

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

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

   285   \end{tabular}

   286   \medskip

   287

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

   289   for root records.

   290 *}

   291

   292

   293 subsection {* Derived rules and proof tools *}

   294

   295 text {*

   296   The record package proves several results internally, declaring

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

   298   reason about record structures quite conveniently.  Assume that

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

   300

   301   \begin{enumerate}

   302

   303   \item Standard conversions for selectors or updates applied to

   304   record constructor terms are made part of the default Simplifier

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

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

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

   308

   309   \item Selectors applied to updated records are automatically reduced

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

   311   standard Simplifier setup.

   312

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

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

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

   316   @{text "t.iffs"}.

   317

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

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

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

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

   322

   323   \item Representations of arbitrary record expressions as canonical

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

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

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

   327   fixed records, record schemes, more parts etc.

   328

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

   330   sensible rule according to the type of the indicated record

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

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

   333

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

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

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

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

   338

   339   \end{enumerate}

   340 *}

   341

   342

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

   344

   345 text {*

   346   \begin{matharray}{rcl}

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

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

   349   \end{matharray}

   350

   351   \begin{rail}

   352     'datatype' (dtspec + 'and')

   353     ;

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

   355     ;

   356

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

   358     ;

   359     cons: name ( type * ) mixfix?

   360   \end{rail}

   361

   362   \begin{description}

   363

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

   365   HOL.

   366

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

   368   inductive ones, generating the standard infrastructure of derived

   369   concepts (primitive recursion etc.).

   370

   371   \end{description}

   372

   373   The induction and exhaustion theorems generated provide case names

   374   according to the constructors involved, while parameters are named

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

   376

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

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

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

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

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

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

   383   internally bound parameters).

   384 *}

   385

   386

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

   388

   389 text {*

   390   \begin{matharray}{rcl}

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

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

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

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

   395   \end{matharray}

   396

   397   \begin{rail}

   398     'primrec' target? fixes 'where' equations

   399     ;

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

   401     ;

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

   403     ;

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

   405     ;

   406     'termination' ( term )?

   407   \end{rail}

   408

   409   \begin{description}

   410

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

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

   413

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

   415   wellfounded recursion. A detailed description with examples can be

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

   417   set of (possibly conditional) recursive equations with arbitrary

   418   pattern matching. The command generates proof obligations for the

   419   completeness and the compatibility of patterns.

   420

   421   The defined function is considered partial, and the resulting

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

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

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

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

   426

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

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

   429   proof attempts regarding pattern matching and termination.  See

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

   431

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

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

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

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

   436   the induction principle is established.

   437

   438   \end{description}

   439

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

   441   command accommodate

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

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

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

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

   446

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

   448   with structural recursion on the datatype the recursion is carried

   449   out.

   450

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

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

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

   454   explicitly as well.

   455

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

   457   options.

   458

   459   \begin{description}

   460

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

   462   overlapping patterns by making them mutually disjoint.  Earlier

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

   464   specification in a format very similar to functional programming.

   465   Note that the resulting simplification and induction rules

   466   correspond to the transformed specification, not the one given

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

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

   469   transformation only works for ML-style datatype patterns.

   470

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

   472   introduction rules for the domain predicate. While mostly not

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

   474

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

   476   equations even without a termination proof, provided that the

   477   function is tail-recursive. This currently only works

   478

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

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

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

   482

   483   \end{description}

   484 *}

   485

   486

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

   488

   489 text {*

   490   \begin{matharray}{rcl}

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

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

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

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

   495   \end{matharray}

   496

   497   \begin{rail}

   498     'relation' term

   499     ;

   500     'lexicographic_order' ( clasimpmod * )

   501     ;

   502     'size_change' ( orders ( clasimpmod * ) )

   503     ;

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

   505   \end{rail}

   506

   507   \begin{description}

   508

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

   510   solve goals regarding the completeness of pattern matching, as

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

   512   \cite{isabelle-function}).

   513

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

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

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

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

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

   519   termination proofs.

   520

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

   522   automated termination proof by searching for a lexicographic

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

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

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

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

   527   \secref{sec:clasimp}.

   528

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

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

   531

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

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

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

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

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

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

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

   539   internally.

   540

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

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

   543

   544   \end{description}

   545 *}

   546

   547 subsection {* Functions with explicit partiality *}

   548

   549 text {*

   550   \begin{matharray}{rcl}

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

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

   553   \end{matharray}

   554

   555   \begin{rail}

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

   557   \end{rail}

   558

   559   \begin{description}

   560

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

   562   functions based on fixpoints in complete partial orders. No

   563   termination proof is required from the user or constructed

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

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

   566   element.

   567

   568   Pattern matching and mutual recursion are currently not supported.

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

   570   single recursive equation.

   571

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

   573   function, but the induced functional must be provably monotonic

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

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

   576   can be influenced by declaring hints using the

   577   @{attribute (HOL) partial_function_mono} attribute.

   578

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

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

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

   582   defined:

   583

   584   \begin{description}

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

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

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

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

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

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

   591

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

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

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

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

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

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

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

   599   definition of arbitrary tail-recursive functions.

   600   \end{description}

   601

   602   Experienced users may define new modes by instantiating the locale

   603   @{const "partial_function_definitions"} appropriately.

   604

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

   606   use in the internal monononicity proofs of partial function

   607   definitions.

   608

   609   \end{description}

   610

   611 *}

   612

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

   614

   615 text {*

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

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

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

   619

   620   \begin{matharray}{rcl}

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

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

   623   \end{matharray}

   624

   625   \begin{rail}

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

   627     ;

   628     recdeftc thmdecl? tc

   629     ;

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

   631     ;

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

   633     ;

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

   635     ;

   636   \end{rail}

   637

   638   \begin{description}

   639

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

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

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

   643   TFL to recover from failed proof attempts, returning unfinished

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

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

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

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

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

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

   650

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

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

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

   654   constant @{text c}.

   655

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

   657   its internal proofs without manual intervention.

   658

   659   \end{description}

   660

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

   662   globally, using the following attributes.

   663

   664   \begin{matharray}{rcl}

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

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

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

   668   \end{matharray}

   669

   670   \begin{rail}

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

   672     ;

   673   \end{rail}

   674 *}

   675

   676

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

   678

   679 text {*

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

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

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

   683   structural operational semantics is an inductive definition of an

   684   evaluation relation.

   685

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

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

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

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

   690   relations to formalise equivalence of processes and infinite data

   691   structures.

   692

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

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

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

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

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

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

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

   700   to use inference rules for type-checking.

   701

   702   \begin{matharray}{rcl}

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

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

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

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

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

   708   \end{matharray}

   709

   710   \begin{rail}

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

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

   713     ;

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

   715     ;

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

   717     ;

   718   \end{rail}

   719

   720   \begin{description}

   721

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

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

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

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

   726   (co)inductive predicates that remain fixed throughout the

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

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

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

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

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

   732

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

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

   735   allowing the definition of (co)inductive sets.

   736

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

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

   739   (HOL) "inductive"}.

   740

   741   \end{description}

   742 *}

   743

   744

   745 subsection {* Derived rules *}

   746

   747 text {*

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

   749   theory and also proves some theorems:

   750

   751   \begin{description}

   752

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

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

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

   756   theory file;

   757

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

   759

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

   761   rule.

   762

   763   \end{description}

   764

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

   766   defined simultaneously, the list of introduction rules is called

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

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

   769   of mutual induction rules is called @{text

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

   771 *}

   772

   773

   774 subsection {* Monotonicity theorems *}

   775

   776 text {*

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

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

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

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

   781   theorems may be added:

   782

   783   \begin{itemize}

   784

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

   786   monotonicity of inductive definitions whose introduction rules have

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

   788

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

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

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

   792   $  793 \infer{@{text "P\<^sub>1 \<or> P\<^sub>2 \<longrightarrow> Q\<^sub>1 \<or> Q\<^sub>2"}}{@{text "P\<^sub>1 \<longrightarrow> Q\<^sub>1"} & @{text "P\<^sub>2 \<longrightarrow> Q\<^sub>2"}}   794$

   795

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

   797   of expressions, e.g.

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

   802

   803   \item Equations for reducing complex operators to more primitive

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

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

   809

   810   \end{itemize}

   811

   812   %FIXME: Example of an inductive definition

   813 *}

   814

   815

   816 section {* Arithmetic proof support *}

   817

   818 text {*

   819   \begin{matharray}{rcl}

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

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

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

   823   \end{matharray}

   824

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

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

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

   828

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

   830   always supplied to the arithmetic provers implicitly.

   831

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

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

   834

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

   836   already invoked by the Simplifier.

   837 *}

   838

   839

   840 section {* Intuitionistic proof search *}

   841

   842 text {*

   843   \begin{matharray}{rcl}

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

   845   \end{matharray}

   846

   847   \begin{rail}

   848     'iprover' ( rulemod * )

   849     ;

   850   \end{rail}

   851

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

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

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

   855   goal before commencing proof search.

   856

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

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

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

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

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

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

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

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

   865 *}

   866

   867

   868 section {* Coherent Logic *}

   869

   870 text {*

   871   \begin{matharray}{rcl}

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

   873   \end{matharray}

   874

   875   \begin{rail}

   876     'coherent' thmrefs?

   877     ;

   878   \end{rail}

   879

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

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

   882   applications in confluence theory, lattice theory and projective

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

   884   examples.

   885 *}

   886

   887

   888 section {* Checking and refuting propositions *}

   889

   890 text {*

   891   Identifying incorrect propositions usually involves evaluation of

   892   particular assignments and systematic counter example search.  This

   893   is supported by the following commands.

   894

   895   \begin{matharray}{rcl}

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

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

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

   899   \end{matharray}

   900

   901   \begin{rail}

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

   903     ;

   904

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

   906     ;

   907

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

   909     ;

   910

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

   912     ;

   913

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

   915     ;

   916   \end{rail}

   917

   918   \begin{description}

   919

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

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

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

   923     Internally, the evaluation is performed by registered evaluators,

   924     which are invoked sequentially until a result is returned.

   925     Alternatively a specific evaluator can be selected using square

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

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

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

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

   930

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

   932     counter examples using a series of arbitrary assignments for its

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

   934     can be selected explicitly using an optional goal index.

   935     A number of configuration options are supported for

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

   937

   938     \begin{description}

   939

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

   941     for assignment values.

   942

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

   944     generated for each particular size.

   945

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

   947     structured proofs should be ignored.

   948

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

   950

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

   952     instantiate type variables.

   953

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

   955     fulfilled the preconditions.

   956

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

   958     current size for assignment values.

   959

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

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

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

   963

   964     \end{description}

   965

   966     These option can be given within square brackets.

   967

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

   969     configuration options persitently.

   970

   971   \end{description}

   972 *}

   973

   974

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

   976

   977 text {*

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

   979   induction in unstructured tactic scripts; see also

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

   981

   982   \begin{matharray}{rcl}

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

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

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

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

   987   \end{matharray}

   988

   989   \begin{rail}

   990     'case_tac' goalspec? term rule?

   991     ;

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

   993     ;

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

   995     ;

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

   997     ;

   998

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

  1000     ;

  1001   \end{rail}

  1002

  1003   \begin{description}

  1004

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

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

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

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

  1009   datatype} package already takes care of this.

  1010

  1011   These unstructured tactics feature both goal addressing and dynamic

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

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

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

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

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

  1017   being addressed.

  1018

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

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

  1021   mk_cases} operation.  Rules are simplified in an unrestricted

  1022   forward manner.

  1023

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

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

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

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

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

  1029   be generalized before applying the resulting rule.

  1030

  1031   \end{description}

  1032 *}

  1033

  1034

  1035 section {* Executable code *}

  1036

  1037 text {*

  1038   Isabelle/Pure provides two generic frameworks to support code

  1039   generation from executable specifications.  Isabelle/HOL

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

  1041   applications.

  1042

  1043   \medskip One framework generates code from functional programs

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

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

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

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

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

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

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

  1051   using the predicate compiler which operates within HOL.

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

  1053

  1054   \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1074   \end{matharray}

  1075

  1076   \begin{rail}

  1077      'export_code' ( constexpr + ) \\

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

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

  1080     ;

  1081

  1082     const: term

  1083     ;

  1084

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

  1086     ;

  1087

  1088     typeconstructor: nameref

  1089     ;

  1090

  1091     class: nameref

  1092     ;

  1093

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

  1095     ;

  1096

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

  1098     ;

  1099

  1100     'code_abort' ( const + )

  1101     ;

  1102

  1103     'code_datatype' ( const + )

  1104     ;

  1105

  1106     'code_inline' ( 'del' ) ?

  1107     ;

  1108

  1109     'code_post' ( 'del' ) ?

  1110     ;

  1111

  1112     'code_thms' ( constexpr + ) ?

  1113     ;

  1114

  1115     'code_deps' ( constexpr + ) ?

  1116     ;

  1117

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

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

  1120     ;

  1121

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

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

  1124     ;

  1125

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

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

  1128     ;

  1129

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

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

  1132     ;

  1133

  1134     'code_reserved' target ( string + )

  1135     ;

  1136

  1137     'code_monad' const const target

  1138     ;

  1139

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

  1141     ;

  1142

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

  1144     ;

  1145

  1146     'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\

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

  1148     ;

  1149

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

  1151     ;

  1152

  1153   \end{rail}

  1154

  1155   \begin{description}

  1156

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

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

  1159   serialization instruction is given, only abstract code is generated

  1160   internally.

  1161

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

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

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

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

  1166

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

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

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

  1170   placed in this module.

  1171

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

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

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

  1175   module hierarchy.  Omitting the file specification denotes standard

  1176   output.

  1177

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

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

  1180   explicit module signatures.

  1181

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

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

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

  1185   datatype declaration.

  1186

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

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

  1189   Usually packages introducing code equations provide a reasonable

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

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

  1192   code equations on abstract datatype representations respectively.

  1193

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

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

  1196   these are implemented by program abort instead.

  1197

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

  1199   for a logical type.

  1200

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

  1202   selected code equations and code generator datatypes.

  1203

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

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

  1206   rewrite rules to any code equation during preprocessing.

  1207

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

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

  1210   result of an evaluation.

  1211

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

  1213   generator preprocessor.

  1214

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

  1216   representing the corresponding program containing all given

  1217   constants after preprocessing.

  1218

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

  1220   theorems representing the corresponding program containing all given

  1221   constants after preprocessing.

  1222

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

  1224   with target-specific serializations; omitting a serialization

  1225   deletes an existing serialization.

  1226

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

  1228   constructors with target-specific serializations; omitting a

  1229   serialization deletes an existing serialization.

  1230

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

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

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

  1234

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

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

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

  1238   already present'' declaration.  This applies only to

  1239   \emph{Haskell}.

  1240

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

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

  1243   generated code.

  1244

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

  1246   to generate monadic code for Haskell.

  1247

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

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

  1250   will remove an already added include''.

  1251

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

  1253   module name onto another.

  1254

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

  1256   argument compiles code into the system runtime environment and

  1257   modifies the code generator setup that future invocations of system

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

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

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

  1261   is generated into that specified file without modifying the code

  1262   generator setup.

  1263

  1264   \end{description}

  1265

  1266   The other framework generates code from both functional and

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

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

  1269   well).

  1270

  1271   \begin{matharray}{rcl}

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

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

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

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

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

  1277   \end{matharray}

  1278

  1279   \begin{rail}

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

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

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

  1283   ;

  1284

  1285   modespec: '(' ( name * ) ')'

  1286   ;

  1287

  1288   'consts_code' (codespec +)

  1289   ;

  1290

  1291   codespec: const template attachment ?

  1292   ;

  1293

  1294   'types_code' (tycodespec +)

  1295   ;

  1296

  1297   tycodespec: name template attachment ?

  1298   ;

  1299

  1300   const: term

  1301   ;

  1302

  1303   template: '(' string ')'

  1304   ;

  1305

  1306   attachment: 'attach' modespec ? verblbrace text verbrbrace

  1307   ;

  1308

  1309   'code' (name)?

  1310   ;

  1311   \end{rail}

  1312

  1313 *}

  1314

  1315

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

  1317

  1318 text {*

  1319   \begin{matharray}{rcl}

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

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

  1322   \end{matharray}

  1323

  1324   \begin{rail}

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

  1326   ;

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

  1328   \end{rail}

  1329

  1330   \begin{description}

  1331

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

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

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

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

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

  1337   constants.

  1338

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

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

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

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

  1343   properties given in the first place.

  1344

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

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

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

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

  1349

  1350   \end{description}

  1351

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

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

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

  1355   construction cannot introduce inconsistencies, whereas @{command

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

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

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

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

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

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

  1362 *}

  1363

  1364 end