1.1 --- a/doc-src/IsarRef/IsaMakefile	Thu May 08 12:27:19 2008 +0200
     1.2 +++ b/doc-src/IsarRef/IsaMakefile	Thu May 08 12:29:18 2008 +0200
     1.3 @@ -22,8 +22,8 @@
     1.4  HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
     1.5  
     1.6  $(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
     1.7 -  Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/Quick_Reference.thy \
     1.8 -  Thy/ML_Tactic.thy
     1.9 +  Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/HOL_Specific.thy \
    1.10 +  Thy/Quick_Reference.thy Thy/ML_Tactic.thy
    1.11  	@$(USEDIR) -s IsarRef HOL Thy
    1.12  
    1.13  

     2.1 --- a/doc-src/IsarRef/Makefile	Thu May 08 12:27:19 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Makefile	Thu May 08 12:29:18 2008 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4    Thy/document/ML_Tactic.tex Thy/document/Quick_Reference.tex \
     2.5    Thy/document/ZF_Specific.tex Thy/document/intro.tex \
     2.6    Thy/document/pure.tex Thy/document/syntax.tex \
     2.7 -  logics.tex ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
     2.8 +  ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
     2.9    ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    2.10  
    2.11  dvi: $(NAME).dvi

     3.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 08 12:27:19 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 08 12:29:18 2008 +0200
     3.3 @@ -1,7 +1,1146 @@
     3.4  (* $Id$ *)
     3.5  
     3.6  theory HOL_Specific
     3.7 -imports HOL
     3.8 +imports Main
     3.9  begin
    3.10  
    3.11 +chapter {* HOL specific elements \label{ch:logics} *}
    3.12 +
    3.13 +section {* Primitive types \label{sec:hol-typedef} *}
    3.14 +
    3.15 +text {*
    3.16 +  \begin{matharray}{rcl}
    3.17 +    @{command_def (HOL) "typedecl"} & : & \isartrans{theory}{theory} \\
    3.18 +    @{command_def (HOL) "typedef"} & : & \isartrans{theory}{proof(prove)} \\
    3.19 +  \end{matharray}
    3.20 +
    3.21 +  \begin{rail}
    3.22 +    'typedecl' typespec infix?
    3.23 +    ;
    3.24 +    'typedef' altname? abstype '=' repset
    3.25 +    ;
    3.26 +
    3.27 +    altname: '(' (name | 'open' | 'open' name) ')'
    3.28 +    ;
    3.29 +    abstype: typespec infix?
    3.30 +    ;
    3.31 +    repset: term ('morphisms' name name)?
    3.32 +    ;
    3.33 +  \end{rail}
    3.34 +
    3.35 +  \begin{descr}
    3.36 +  
    3.37 +  \item [@{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n)
    3.38 +  t"}] is similar to the original @{command "typedecl"} of
    3.39 +  Isabelle/Pure (see \secref{sec:types-pure}), but also declares type
    3.40 +  arity @{text "t :: (type, \<dots>, type) type"}, making @{text t} an
    3.41 +  actual HOL type constructor.   %FIXME check, update
    3.42 +  
    3.43 +  \item [@{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n)
    3.44 +  t = A"}] sets up a goal stating non-emptiness of the set @{text A}.
    3.45 +  After finishing the proof, the theory will be augmented by a
    3.46 +  Gordon/HOL-style type definition, which establishes a bijection
    3.47 +  between the representing set @{text A} and the new type @{text t}.
    3.48 +  
    3.49 +  Technically, @{command (HOL) "typedef"} defines both a type @{text
    3.50 +  t} and a set (term constant) of the same name (an alternative base
    3.51 +  name may be given in parentheses).  The injection from type to set
    3.52 +  is called @{text Rep_t}, its inverse @{text Abs_t} (this may be
    3.53 +  changed via an explicit @{keyword (HOL) "morphisms"} declaration).
    3.54 +  
    3.55 +  Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text
    3.56 +  Abs_t_inverse} provide the most basic characterization as a
    3.57 +  corresponding injection/surjection pair (in both directions).  Rules
    3.58 +  @{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly
    3.59 +  more convenient view on the injectivity part, suitable for automated
    3.60 +  proof tools (e.g.\ in @{method simp} or @{method iff} declarations).
    3.61 +  Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and @{text
    3.62 +  Abs_t_cases}/@{text Abs_t_induct} provide alternative views on
    3.63 +  surjectivity; these are already declared as set or type rules for
    3.64 +  the generic @{method cases} and @{method induct} methods.
    3.65 +  
    3.66 +  An alternative name may be specified in parentheses; the default is
    3.67 +  to use @{text t} as indicated before.  The ``@{text "(open)"}''
    3.68 +  declaration suppresses a separate constant definition for the
    3.69 +  representing set.
    3.70 +
    3.71 +  \end{descr}
    3.72 +
    3.73 +  Note that raw type declarations are rarely used in practice; the
    3.74 +  main application is with experimental (or even axiomatic!) theory
    3.75 +  fragments.  Instead of primitive HOL type definitions, user-level
    3.76 +  theories usually refer to higher-level packages such as @{command
    3.77 +  (HOL) "record"} (see \secref{sec:hol-record}) or @{command (HOL)
    3.78 +  "datatype"} (see \secref{sec:hol-datatype}).
    3.79 +*}
    3.80 +
    3.81 +
    3.82 +section {* Adhoc tuples *}
    3.83 +
    3.84 +text {*
    3.85 +  \begin{matharray}{rcl}
    3.86 +    @{attribute (HOL) split_format}@{text "\<^sup>*"} & : & \isaratt \\
    3.87 +  \end{matharray}
    3.88 +
    3.89 +  \begin{rail}
    3.90 +    'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))
    3.91 +    ;
    3.92 +  \end{rail}
    3.93 +
    3.94 +  \begin{descr}
    3.95 +  
    3.96 +  \item [@{method (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m
    3.97 +  \<AND> \<dots> \<AND> q\<^sub>1 \<dots> q\<^sub>n"}] puts expressions of
    3.98 +  low-level tuple types into canonical form as specified by the
    3.99 +  arguments given; the @{text i}-th collection of arguments refers to
   3.100 +  occurrences in premise @{text i} of the rule.  The ``@{text
   3.101 +  "(complete)"}'' option causes \emph{all} arguments in function
   3.102 +  applications to be represented canonically according to their tuple
   3.103 +  type structure.
   3.104 +
   3.105 +  Note that these operations tend to invent funny names for new local
   3.106 +  parameters to be introduced.
   3.107 +
   3.108 +  \end{descr}
   3.109 +*}
   3.110 +
   3.111 +
   3.112 +section {* Records \label{sec:hol-record} *}
   3.113 +
   3.114 +text {*
   3.115 +  In principle, records merely generalize the concept of tuples, where
   3.116 +  components may be addressed by labels instead of just position.  The
   3.117 +  logical infrastructure of records in Isabelle/HOL is slightly more
   3.118 +  advanced, though, supporting truly extensible record schemes.  This
   3.119 +  admits operations that are polymorphic with respect to record
   3.120 +  extension, yielding ``object-oriented'' effects like (single)
   3.121 +  inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for more
   3.122 +  details on object-oriented verification and record subtyping in HOL.
   3.123 +*}
   3.124 +
   3.125 +
   3.126 +subsection {* Basic concepts *}
   3.127 +
   3.128 +text {*
   3.129 +  Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
   3.130 +  at the level of terms and types.  The notation is as follows:
   3.131 +
   3.132 +  \begin{center}
   3.133 +  \begin{tabular}{l|l|l}
   3.134 +    & record terms & record types \\ \hline
   3.135 +    fixed & @{text "\<lparr>x = a, y = b\<rparr>"} & @{text "\<lparr>x :: A, y :: B\<rparr>"} \\
   3.136 +    schematic & @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} &
   3.137 +      @{text "\<lparr>x :: A, y :: B, \<dots> :: M\<rparr>"} \\
   3.138 +  \end{tabular}
   3.139 +  \end{center}
   3.140 +
   3.141 +  \noindent The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text
   3.142 +  "(| x = a |)"}.
   3.143 +
   3.144 +  A fixed record @{text "\<lparr>x = a, y = b\<rparr>"} has field @{text x} of value
   3.145 +  @{text a} and field @{text y} of value @{text b}.  The corresponding
   3.146 +  type is @{text "\<lparr>x :: A, y :: B\<rparr>"}, assuming that @{text "a :: A"}
   3.147 +  and @{text "b :: B"}.
   3.148 +
   3.149 +  A record scheme like @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} contains fields
   3.150 +  @{text x} and @{text y} as before, but also possibly further fields
   3.151 +  as indicated by the ``@{text "\<dots>"}'' notation (which is actually part
   3.152 +  of the syntax).  The improper field ``@{text "\<dots>"}'' of a record
   3.153 +  scheme is called the \emph{more part}.  Logically it is just a free
   3.154 +  variable, which is occasionally referred to as ``row variable'' in
   3.155 +  the literature.  The more part of a record scheme may be
   3.156 +  instantiated by zero or more further components.  For example, the
   3.157 +  previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z =
   3.158 +  c, \<dots> = m'"}, where @{text m'} refers to a different more part.
   3.159 +  Fixed records are special instances of record schemes, where
   3.160 +  ``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}
   3.161 +  element.  In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation
   3.162 +  for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}.
   3.163 +  
   3.164 +  \medskip Two key observations make extensible records in a simply
   3.165 +  typed language like HOL work out:
   3.166 +
   3.167 +  \begin{enumerate}
   3.168 +
   3.169 +  \item the more part is internalized, as a free term or type
   3.170 +  variable,
   3.171 +
   3.172 +  \item field names are externalized, they cannot be accessed within the logic
   3.173 +  as first-class values.
   3.174 +
   3.175 +  \end{enumerate}
   3.176 +
   3.177 +  \medskip In Isabelle/HOL record types have to be defined explicitly,
   3.178 +  fixing their field names and types, and their (optional) parent
   3.179 +  record.  Afterwards, records may be formed using above syntax, while
   3.180 +  obeying the canonical order of fields as given by their declaration.
   3.181 +  The record package provides several standard operations like
   3.182 +  selectors and updates.  The common setup for various generic proof
   3.183 +  tools enable succinct reasoning patterns.  See also the Isabelle/HOL
   3.184 +  tutorial \cite{isabelle-hol-book} for further instructions on using
   3.185 +  records in practice.
   3.186 +*}
   3.187 +
   3.188 +
   3.189 +subsection {* Record specifications *}
   3.190 +
   3.191 +text {*
   3.192 +  \begin{matharray}{rcl}
   3.193 +    @{command_def (HOL) "record"} & : & \isartrans{theory}{theory} \\
   3.194 +  \end{matharray}
   3.195 +
   3.196 +  \begin{rail}
   3.197 +    'record' typespec '=' (type '+')? (constdecl +)
   3.198 +    ;
   3.199 +  \end{rail}
   3.200 +
   3.201 +  \begin{descr}
   3.202 +
   3.203 +  \item [@{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t
   3.204 +  = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1 \<dots> c\<^sub>n :: \<sigma>\<^sub>n"}] defines
   3.205 +  extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},
   3.206 +  derived from the optional parent record @{text "\<tau>"} by adding new
   3.207 +  field components @{text "c\<^sub>i :: \<sigma>\<^sub>i"} etc.
   3.208 +
   3.209 +  The type variables of @{text "\<tau>"} and @{text "\<sigma>\<^sub>i"} need to be
   3.210 +  covered by the (distinct) parameters @{text "\<alpha>\<^sub>1, \<dots>,
   3.211 +  \<alpha>\<^sub>m"}.  Type constructor @{text t} has to be new, while @{text
   3.212 +  \<tau>} needs to specify an instance of an existing record type.  At
   3.213 +  least one new field @{text "c\<^sub>i"} has to be specified.
   3.214 +  Basically, field names need to belong to a unique record.  This is
   3.215 +  not a real restriction in practice, since fields are qualified by
   3.216 +  the record name internally.
   3.217 +
   3.218 +  The parent record specification @{text \<tau>} is optional; if omitted
   3.219 +  @{text t} becomes a root record.  The hierarchy of all records
   3.220 +  declared within a theory context forms a forest structure, i.e.\ a
   3.221 +  set of trees starting with a root record each.  There is no way to
   3.222 +  merge multiple parent records!
   3.223 +
   3.224 +  For convenience, @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} is made a
   3.225 +  type abbreviation for the fixed record type @{text "\<lparr>c\<^sub>1 ::
   3.226 +  \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"}, likewise is @{text
   3.227 +  "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme"} made an abbreviation for
   3.228 +  @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::
   3.229 +  \<zeta>\<rparr>"}.
   3.230 +
   3.231 +  \end{descr}
   3.232 +*}
   3.233 +
   3.234 +
   3.235 +subsection {* Record operations *}
   3.236 +
   3.237 +text {*
   3.238 +  Any record definition of the form presented above produces certain
   3.239 +  standard operations.  Selectors and updates are provided for any
   3.240 +  field, including the improper one ``@{text more}''.  There are also
   3.241 +  cumulative record constructor functions.  To simplify the
   3.242 +  presentation below, we assume for now that @{text "(\<alpha>\<^sub>1, \<dots>,
   3.243 +  \<alpha>\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 ::
   3.244 +  \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"}.
   3.245 +
   3.246 +  \medskip \textbf{Selectors} and \textbf{updates} are available for
   3.247 +  any field (including ``@{text more}''):
   3.248 +
   3.249 +  \begin{matharray}{lll}
   3.250 +    @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
   3.251 +    @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\
   3.252 +  \end{matharray}
   3.253 +
   3.254 +  There is special syntax for application of updates: @{text "r\<lparr>x :=
   3.255 +  a\<rparr>"} abbreviates term @{text "x_update a r"}.  Further notation for
   3.256 +  repeated updates is also available: @{text "r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z :=
   3.257 +  c\<rparr>"} may be written @{text "r\<lparr>x := a, y := b, z := c\<rparr>"}.  Note that
   3.258 +  because of postfix notation the order of fields shown here is
   3.259 +  reverse than in the actual term.  Since repeated updates are just
   3.260 +  function applications, fields may be freely permuted in @{text "\<lparr>x
   3.261 +  := a, y := b, z := c\<rparr>"}, as far as logical equality is concerned.
   3.262 +  Thus commutativity of independent updates can be proven within the
   3.263 +  logic for any two fields, but not as a general theorem.
   3.264 +
   3.265 +  \medskip The \textbf{make} operation provides a cumulative record
   3.266 +  constructor function:
   3.267 +
   3.268 +  \begin{matharray}{lll}
   3.269 +    @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"} \\
   3.270 +  \end{matharray}
   3.271 +
   3.272 +  \medskip We now reconsider the case of non-root records, which are
   3.273 +  derived of some parent.  In general, the latter may depend on
   3.274 +  another parent as well, resulting in a list of \emph{ancestor
   3.275 +  records}.  Appending the lists of fields of all ancestors results in
   3.276 +  a certain field prefix.  The record package automatically takes care
   3.277 +  of this by lifting operations over this context of ancestor fields.
   3.278 +  Assuming that @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} has ancestor
   3.279 +  fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"},
   3.280 +  the above record operations will get the following types:
   3.281 +
   3.282 +  \begin{matharray}{lll}
   3.283 +    @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
   3.284 +    @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> 
   3.285 +      \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
   3.286 +      \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\
   3.287 +    @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> 
   3.288 +      \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"} \\
   3.289 +  \end{matharray}
   3.290 +  \noindent
   3.291 +
   3.292 +  \medskip Some further operations address the extension aspect of a
   3.293 +  derived record scheme specifically: @{text "t.fields"} produces a
   3.294 +  record fragment consisting of exactly the new fields introduced here
   3.295 +  (the result may serve as a more part elsewhere); @{text "t.extend"}
   3.296 +  takes a fixed record and adds a given more part; @{text
   3.297 +  "t.truncate"} restricts a record scheme to a fixed record.
   3.298 +
   3.299 +  \begin{matharray}{lll}
   3.300 +    @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"} \\
   3.301 +    @{text "t.extend"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr> \<Rightarrow>
   3.302 +      \<zeta> \<Rightarrow> \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\
   3.303 +    @{text "t.truncate"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"} \\
   3.304 +  \end{matharray}
   3.305 +
   3.306 +  \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide
   3.307 +  for root records.
   3.308 +*}
   3.309 +
   3.310 +
   3.311 +subsection {* Derived rules and proof tools *}
   3.312 +
   3.313 +text {*
   3.314 +  The record package proves several results internally, declaring
   3.315 +  these facts to appropriate proof tools.  This enables users to
   3.316 +  reason about record structures quite conveniently.  Assume that
   3.317 +  @{text t} is a record type as specified above.
   3.318 +
   3.319 +  \begin{enumerate}
   3.320 +  
   3.321 +  \item Standard conversions for selectors or updates applied to
   3.322 +  record constructor terms are made part of the default Simplifier
   3.323 +  context; thus proofs by reduction of basic operations merely require
   3.324 +  the @{method simp} method without further arguments.  These rules
   3.325 +  are available as @{text "t.simps"}, too.
   3.326 +  
   3.327 +  \item Selectors applied to updated records are automatically reduced
   3.328 +  by an internal simplification procedure, which is also part of the
   3.329 +  standard Simplifier setup.
   3.330 +
   3.331 +  \item Inject equations of a form analogous to @{prop "(x, y) = (x',
   3.332 +  y') \<equiv> x = x' \<and> y = y'"} are declared to the Simplifier and Classical
   3.333 +  Reasoner as @{attribute iff} rules.  These rules are available as
   3.334 +  @{text "t.iffs"}.
   3.335 +
   3.336 +  \item The introduction rule for record equality analogous to @{text
   3.337 +  "x r = x r' \<Longrightarrow> y r = y r' \<dots> \<Longrightarrow> r = r'"} is declared to the Simplifier,
   3.338 +  and as the basic rule context as ``@{attribute intro}@{text "?"}''.
   3.339 +  The rule is called @{text "t.equality"}.
   3.340 +
   3.341 +  \item Representations of arbitrary record expressions as canonical
   3.342 +  constructor terms are provided both in @{method cases} and @{method
   3.343 +  induct} format (cf.\ the generic proof methods of the same name,
   3.344 +  \secref{sec:cases-induct}).  Several variations are available, for
   3.345 +  fixed records, record schemes, more parts etc.
   3.346 +  
   3.347 +  The generic proof methods are sufficiently smart to pick the most
   3.348 +  sensible rule according to the type of the indicated record
   3.349 +  expression: users just need to apply something like ``@{text "(cases
   3.350 +  r)"}'' to a certain proof problem.
   3.351 +
   3.352 +  \item The derived record operations @{text "t.make"}, @{text
   3.353 +  "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not}
   3.354 +  treated automatically, but usually need to be expanded by hand,
   3.355 +  using the collective fact @{text "t.defs"}.
   3.356 +
   3.357 +  \end{enumerate}
   3.358 +*}
   3.359 +
   3.360 +
   3.361 +section {* Datatypes \label{sec:hol-datatype} *}
   3.362 +
   3.363 +text {*
   3.364 +  \begin{matharray}{rcl}
   3.365 +    @{command_def (HOL) "datatype"} & : & \isartrans{theory}{theory} \\
   3.366 +    @{command_def (HOL) "rep_datatype"} & : & \isartrans{theory}{theory} \\
   3.367 +  \end{matharray}
   3.368 +
   3.369 +  \begin{rail}
   3.370 +    'datatype' (dtspec + 'and')
   3.371 +    ;
   3.372 +    'rep\_datatype' (name *) dtrules
   3.373 +    ;
   3.374 +
   3.375 +    dtspec: parname? typespec infix? '=' (cons + '|')
   3.376 +    ;
   3.377 +    cons: name (type *) mixfix?
   3.378 +    ;
   3.379 +    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
   3.380 +  \end{rail}
   3.381 +
   3.382 +  \begin{descr}
   3.383 +
   3.384 +  \item [@{command (HOL) "datatype"}] defines inductive datatypes in
   3.385 +  HOL.
   3.386 +
   3.387 +  \item [@{command (HOL) "rep_datatype"}] represents existing types as
   3.388 +  inductive ones, generating the standard infrastructure of derived
   3.389 +  concepts (primitive recursion etc.).
   3.390 +
   3.391 +  \end{descr}
   3.392 +
   3.393 +  The induction and exhaustion theorems generated provide case names
   3.394 +  according to the constructors involved, while parameters are named
   3.395 +  after the types (see also \secref{sec:cases-induct}).
   3.396 +
   3.397 +  See \cite{isabelle-HOL} for more details on datatypes, but beware of
   3.398 +  the old-style theory syntax being used there!  Apart from proper
   3.399 +  proof methods for case-analysis and induction, there are also
   3.400 +  emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
   3.401 +  induct_tac} available, see \secref{sec:hol-induct-tac}; these admit
   3.402 +  to refer directly to the internal structure of subgoals (including
   3.403 +  internally bound parameters).
   3.404 +*}
   3.405 +
   3.406 +
   3.407 +section {* Recursive functions \label{sec:recursion} *}
   3.408 +
   3.409 +text {*
   3.410 +  \begin{matharray}{rcl}
   3.411 +    @{command_def (HOL) "primrec"} & : & \isarkeep{local{\dsh}theory} \\
   3.412 +    @{command_def (HOL) "fun"} & : & \isarkeep{local{\dsh}theory} \\
   3.413 +    @{command_def (HOL) "function"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
   3.414 +    @{command_def (HOL) "termination"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
   3.415 +  \end{matharray}
   3.416 +
   3.417 +  \railalias{funopts}{function\_opts}  %FIXME ??
   3.418 +
   3.419 +  \begin{rail}
   3.420 +    'primrec' target? fixes 'where' equations
   3.421 +    ;
   3.422 +    equations: (thmdecl? prop + '|')
   3.423 +    ;
   3.424 +    ('fun' | 'function') (funopts)? fixes 'where' clauses
   3.425 +    ;
   3.426 +    clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
   3.427 +    ;
   3.428 +    funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' |
   3.429 +    'default' term) + ',') ')'
   3.430 +    ;
   3.431 +    'termination' ( term )?
   3.432 +  \end{rail}
   3.433 +
   3.434 +  \begin{descr}
   3.435 +
   3.436 +  \item [@{command (HOL) "primrec"}] defines primitive recursive
   3.437 +  functions over datatypes, see also \cite{isabelle-HOL}.
   3.438 +
   3.439 +  \item [@{command (HOL) "function"}] defines functions by general
   3.440 +  wellfounded recursion. A detailed description with examples can be
   3.441 +  found in \cite{isabelle-function}. The function is specified by a
   3.442 +  set of (possibly conditional) recursive equations with arbitrary
   3.443 +  pattern matching. The command generates proof obligations for the
   3.444 +  completeness and the compatibility of patterns.
   3.445 +
   3.446 +  The defined function is considered partial, and the resulting
   3.447 +  simplification rules (named @{text "f.psimps"}) and induction rule
   3.448 +  (named @{text "f.pinduct"}) are guarded by a generated domain
   3.449 +  predicate @{text "f_dom"}. The @{command (HOL) "termination"}
   3.450 +  command can then be used to establish that the function is total.
   3.451 +
   3.452 +  \item [@{command (HOL) "fun"}] is a shorthand notation for
   3.453 +  ``@{command (HOL) "function"}~@{text "(sequential)"}, followed by
   3.454 +  automated proof attempts regarding pattern matching and termination.
   3.455 +  See \cite{isabelle-function} for further details.
   3.456 +
   3.457 +  \item [@{command (HOL) "termination"}~@{text f}] commences a
   3.458 +  termination proof for the previously defined function @{text f}.  If
   3.459 +  this is omitted, the command refers to the most recent function
   3.460 +  definition.  After the proof is closed, the recursive equations and
   3.461 +  the induction principle is established.
   3.462 +
   3.463 +  \end{descr}
   3.464 +
   3.465 +  %FIXME check
   3.466 +
   3.467 +  Recursive definitions introduced by both the @{command (HOL)
   3.468 +  "primrec"} and the @{command (HOL) "function"} command accommodate
   3.469 +  reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
   3.470 +  "c.induct"} (where @{text c} is the name of the function definition)
   3.471 +  refers to a specific induction rule, with parameters named according
   3.472 +  to the user-specified equations.  Case names of @{command (HOL)
   3.473 +  "primrec"} are that of the datatypes involved, while those of
   3.474 +  @{command (HOL) "function"} are numbered (starting from 1).
   3.475 +
   3.476 +  The equations provided by these packages may be referred later as
   3.477 +  theorem list @{text "f.simps"}, where @{text f} is the (collective)
   3.478 +  name of the functions defined.  Individual equations may be named
   3.479 +  explicitly as well.
   3.480 +
   3.481 +  The @{command (HOL) "function"} command accepts the following
   3.482 +  options.
   3.483 +
   3.484 +  \begin{descr}
   3.485 +
   3.486 +  \item [@{text sequential}] enables a preprocessor which
   3.487 +  disambiguates overlapping patterns by making them mutually disjoint.
   3.488 +  Earlier equations take precedence over later ones.  This allows to
   3.489 +  give the specification in a format very similar to functional
   3.490 +  programming.  Note that the resulting simplification and induction
   3.491 +  rules correspond to the transformed specification, not the one given
   3.492 +  originally. This usually means that each equation given by the user
   3.493 +  may result in several theroems.  Also note that this automatic
   3.494 +  transformation only works for ML-style datatype patterns.
   3.495 +
   3.496 +  \item [@{text "\<IN> name"}] gives the target for the definition.
   3.497 +  %FIXME ?!?
   3.498 +
   3.499 +  \item [@{text domintros}] enables the automated generation of
   3.500 +  introduction rules for the domain predicate. While mostly not
   3.501 +  needed, they can be helpful in some proofs about partial functions.
   3.502 +
   3.503 +  \item [@{text tailrec}] generates the unconstrained recursive
   3.504 +  equations even without a termination proof, provided that the
   3.505 +  function is tail-recursive. This currently only works
   3.506 +
   3.507 +  \item [@{text "default d"}] allows to specify a default value for a
   3.508 +  (partial) function, which will ensure that @{text "f x = d x"}
   3.509 +  whenever @{text "x \<notin> f_dom"}.
   3.510 +
   3.511 +  \end{descr}
   3.512 +*}
   3.513 +
   3.514 +
   3.515 +subsection {* Proof methods related to recursive definitions *}
   3.516 +
   3.517 +text {*
   3.518 +  \begin{matharray}{rcl}
   3.519 +    @{method_def (HOL) pat_completeness} & : & \isarmeth \\
   3.520 +    @{method_def (HOL) relation} & : & \isarmeth \\
   3.521 +    @{method_def (HOL) lexicographic_order} & : & \isarmeth \\
   3.522 +  \end{matharray}
   3.523 +
   3.524 +  \begin{rail}
   3.525 +    'relation' term
   3.526 +    ;
   3.527 +    'lexicographic\_order' (clasimpmod *)
   3.528 +    ;
   3.529 +  \end{rail}
   3.530 +
   3.531 +  \begin{descr}
   3.532 +
   3.533 +  \item [@{method (HOL) pat_completeness}] is a specialized method to
   3.534 +  solve goals regarding the completeness of pattern matching, as
   3.535 +  required by the @{command (HOL) "function"} package (cf.\
   3.536 +  \cite{isabelle-function}).
   3.537 +
   3.538 +  \item [@{method (HOL) relation}~@{text R}] introduces a termination
   3.539 +  proof using the relation @{text R}.  The resulting proof state will
   3.540 +  contain goals expressing that @{text R} is wellfounded, and that the
   3.541 +  arguments of recursive calls decrease with respect to @{text R}.
   3.542 +  Usually, this method is used as the initial proof step of manual
   3.543 +  termination proofs.
   3.544 +
   3.545 +  \item [@{method (HOL) "lexicographic_order"}] attempts a fully
   3.546 +  automated termination proof by searching for a lexicographic
   3.547 +  combination of size measures on the arguments of the function. The
   3.548 +  method accepts the same arguments as the @{method auto} method,
   3.549 +  which it uses internally to prove local descents.  The same context
   3.550 +  modifiers as for @{method auto} are accepted, see
   3.551 +  \secref{sec:clasimp}.
   3.552 +
   3.553 +  In case of failure, extensive information is printed, which can help
   3.554 +  to analyse the situation (cf.\ \cite{isabelle-function}).
   3.555 +
   3.556 +  \end{descr}
   3.557 +*}
   3.558 +
   3.559 +
   3.560 +subsection {* Old-style recursive function definitions (TFL) *}
   3.561 +
   3.562 +text {*
   3.563 +  The old TFL commands @{command (HOL) "recdef"} and @{command (HOL)
   3.564 +  "recdef_tc"} for defining recursive are mostly obsolete; @{command
   3.565 +  (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
   3.566 +
   3.567 +  \begin{matharray}{rcl}
   3.568 +    @{command_def (HOL) "recdef"} & : & \isartrans{theory}{theory} \\
   3.569 +    @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & \isartrans{theory}{proof(prove)} \\
   3.570 +  \end{matharray}
   3.571 +
   3.572 +  \begin{rail}
   3.573 +    'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
   3.574 +    ;
   3.575 +    recdeftc thmdecl? tc
   3.576 +    ;
   3.577 +    hints: '(' 'hints' (recdefmod *) ')'
   3.578 +    ;
   3.579 +    recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
   3.580 +    ;
   3.581 +    tc: nameref ('(' nat ')')?
   3.582 +    ;
   3.583 +  \end{rail}
   3.584 +
   3.585 +  \begin{descr}
   3.586 +  
   3.587 +  \item [@{command (HOL) "recdef"}] defines general well-founded
   3.588 +  recursive functions (using the TFL package), see also
   3.589 +  \cite{isabelle-HOL}.  The ``@{text "(permissive)"}'' option tells
   3.590 +  TFL to recover from failed proof attempts, returning unfinished
   3.591 +  results.  The @{text recdef_simp}, @{text recdef_cong}, and @{text
   3.592 +  recdef_wf} hints refer to auxiliary rules to be used in the internal
   3.593 +  automated proof process of TFL.  Additional @{syntax clasimpmod}
   3.594 +  declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
   3.595 +  context of the Simplifier (cf.\ \secref{sec:simplifier}) and
   3.596 +  Classical reasoner (cf.\ \secref{sec:classical}).
   3.597 +  
   3.598 +  \item [@{command (HOL) "recdef_tc"}~@{text "c (i)"}] recommences the
   3.599 +  proof for leftover termination condition number @{text i} (default
   3.600 +  1) as generated by a @{command (HOL) "recdef"} definition of
   3.601 +  constant @{text c}.
   3.602 +  
   3.603 +  Note that in most cases, @{command (HOL) "recdef"} is able to finish
   3.604 +  its internal proofs without manual intervention.
   3.605 +
   3.606 +  \end{descr}
   3.607 +
   3.608 +  \medskip Hints for @{command (HOL) "recdef"} may be also declared
   3.609 +  globally, using the following attributes.
   3.610 +
   3.611 +  \begin{matharray}{rcl}
   3.612 +    @{attribute_def (HOL) recdef_simp} & : & \isaratt \\
   3.613 +    @{attribute_def (HOL) recdef_cong} & : & \isaratt \\
   3.614 +    @{attribute_def (HOL) recdef_wf} & : & \isaratt \\
   3.615 +  \end{matharray}
   3.616 +
   3.617 +  \begin{rail}
   3.618 +    ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
   3.619 +    ;
   3.620 +  \end{rail}
   3.621 +*}
   3.622 +
   3.623 +
   3.624 +section {* Definition by specification \label{sec:hol-specification} *}
   3.625 +
   3.626 +text {*
   3.627 +  \begin{matharray}{rcl}
   3.628 +    @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\
   3.629 +    @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\
   3.630 +  \end{matharray}
   3.631 +
   3.632 +  \begin{rail}
   3.633 +  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
   3.634 +  ;
   3.635 +  decl: ((name ':')? term '(' 'overloaded' ')'?)
   3.636 +  \end{rail}
   3.637 +
   3.638 +  \begin{descr}
   3.639 +
   3.640 +  \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a
   3.641 +  goal stating the existence of terms with the properties specified to
   3.642 +  hold for the constants given in @{text decls}.  After finishing the
   3.643 +  proof, the theory will be augmented with definitions for the given
   3.644 +  constants, as well as with theorems stating the properties for these
   3.645 +  constants.
   3.646 +
   3.647 +  \item [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets
   3.648 +  up a goal stating the existence of terms with the properties
   3.649 +  specified to hold for the constants given in @{text decls}.  After
   3.650 +  finishing the proof, the theory will be augmented with axioms
   3.651 +  expressing the properties given in the first place.
   3.652 +
   3.653 +  \item [@{text decl}] declares a constant to be defined by the
   3.654 +  specification given.  The definition for the constant @{text c} is
   3.655 +  bound to the name @{text c_def} unless a theorem name is given in
   3.656 +  the declaration.  Overloaded constants should be declared as such.
   3.657 +
   3.658 +  \end{descr}
   3.659 +
   3.660 +  Whether to use @{command (HOL) "specification"} or @{command (HOL)
   3.661 +  "ax_specification"} is to some extent a matter of style.  @{command
   3.662 +  (HOL) "specification"} introduces no new axioms, and so by
   3.663 +  construction cannot introduce inconsistencies, whereas @{command
   3.664 +  (HOL) "ax_specification"} does introduce axioms, but only after the
   3.665 +  user has explicitly proven it to be safe.  A practical issue must be
   3.666 +  considered, though: After introducing two constants with the same
   3.667 +  properties using @{command (HOL) "specification"}, one can prove
   3.668 +  that the two constants are, in fact, equal.  If this might be a
   3.669 +  problem, one should use @{command (HOL) "ax_specification"}.
   3.670 +*}
   3.671 +
   3.672 +
   3.673 +section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}
   3.674 +
   3.675 +text {*
   3.676 +  An \textbf{inductive definition} specifies the least predicate (or
   3.677 +  set) @{text R} closed under given rules: applying a rule to elements
   3.678 +  of @{text R} yields a result within @{text R}.  For example, a
   3.679 +  structural operational semantics is an inductive definition of an
   3.680 +  evaluation relation.
   3.681 +
   3.682 +  Dually, a \textbf{coinductive definition} specifies the greatest
   3.683 +  predicate~/ set @{text R} that is consistent with given rules: every
   3.684 +  element of @{text R} can be seen as arising by applying a rule to
   3.685 +  elements of @{text R}.  An important example is using bisimulation
   3.686 +  relations to formalise equivalence of processes and infinite data
   3.687 +  structures.
   3.688 +
   3.689 +  \medskip The HOL package is related to the ZF one, which is
   3.690 +  described in a separate paper,\footnote{It appeared in CADE
   3.691 +  \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
   3.692 +  which you should refer to in case of difficulties.  The package is
   3.693 +  simpler than that of ZF thanks to implicit type-checking in HOL.
   3.694 +  The types of the (co)inductive predicates (or sets) determine the
   3.695 +  domain of the fixedpoint definition, and the package does not have
   3.696 +  to use inference rules for type-checking.
   3.697 +
   3.698 +  \begin{matharray}{rcl}
   3.699 +    @{command_def (HOL) "inductive"} & : & \isarkeep{local{\dsh}theory} \\
   3.700 +    @{command_def (HOL) "inductive_set"} & : & \isarkeep{local{\dsh}theory} \\
   3.701 +    @{command_def (HOL) "coinductive"} & : & \isarkeep{local{\dsh}theory} \\
   3.702 +    @{command_def (HOL) "coinductive_set"} & : & \isarkeep{local{\dsh}theory} \\
   3.703 +    @{attribute_def (HOL) mono} & : & \isaratt \\
   3.704 +  \end{matharray}
   3.705 +
   3.706 +  \begin{rail}
   3.707 +    ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
   3.708 +    ('where' clauses)? ('monos' thmrefs)?
   3.709 +    ;
   3.710 +    clauses: (thmdecl? prop + '|')
   3.711 +    ;
   3.712 +    'mono' (() | 'add' | 'del')
   3.713 +    ;
   3.714 +  \end{rail}
   3.715 +
   3.716 +  \begin{descr}
   3.717 +
   3.718 +  \item [@{command (HOL) "inductive"} and @{command (HOL)
   3.719 +  "coinductive"}] define (co)inductive predicates from the
   3.720 +  introduction rules given in the @{keyword "where"} part.  The
   3.721 +  optional @{keyword "for"} part contains a list of parameters of the
   3.722 +  (co)inductive predicates that remain fixed throughout the
   3.723 +  definition.  The optional @{keyword "monos"} section contains
   3.724 +  \emph{monotonicity theorems}, which are required for each operator
   3.725 +  applied to a recursive set in the introduction rules.  There
   3.726 +  \emph{must} be a theorem of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"},
   3.727 +  for each premise @{text "M R\<^sub>i t"} in an introduction rule!
   3.728 +
   3.729 +  \item [@{command (HOL) "inductive_set"} and @{command (HOL)
   3.730 +  "coinductive_set"}] are wrappers for to the previous commands,
   3.731 +  allowing the definition of (co)inductive sets.
   3.732 +
   3.733 +  \item [@{attribute (HOL) mono}] declares monotonicity rules.  These
   3.734 +  rule are involved in the automated monotonicity proof of @{command
   3.735 +  (HOL) "inductive"}.
   3.736 +
   3.737 +  \end{descr}
   3.738 +*}
   3.739 +
   3.740 +
   3.741 +subsection {* Derived rules *}
   3.742 +
   3.743 +text {*
   3.744 +  Each (co)inductive definition @{text R} adds definitions to the
   3.745 +  theory and also proves some theorems:
   3.746 +
   3.747 +  \begin{description}
   3.748 +
   3.749 +  \item [@{text R.intros}] is the list of introduction rules as proven
   3.750 +  theorems, for the recursive predicates (or sets).  The rules are
   3.751 +  also available individually, using the names given them in the
   3.752 +  theory file;
   3.753 +
   3.754 +  \item [@{text R.cases}] is the case analysis (or elimination) rule;
   3.755 +
   3.756 +  \item [@{text R.induct} or @{text R.coinduct}] is the (co)induction
   3.757 +  rule.
   3.758 +
   3.759 +  \end{description}
   3.760 +
   3.761 +  When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are
   3.762 +  defined simultaneously, the list of introduction rules is called
   3.763 +  @{text "R\<^sub>1_\<dots>_R\<^sub>n.intros"}, the case analysis rules are
   3.764 +  called @{text "R\<^sub>1.cases, \<dots>, R\<^sub>n.cases"}, and the list
   3.765 +  of mutual induction rules is called @{text
   3.766 +  "R\<^sub>1_\<dots>_R\<^sub>n.inducts"}.
   3.767 +*}
   3.768 +
   3.769 +
   3.770 +subsection {* Monotonicity theorems *}
   3.771 +
   3.772 +text {*
   3.773 +  Each theory contains a default set of theorems that are used in
   3.774 +  monotonicity proofs.  New rules can be added to this set via the
   3.775 +  @{attribute (HOL) mono} attribute.  The HOL theory @{text Inductive}
   3.776 +  shows how this is done.  In general, the following monotonicity
   3.777 +  theorems may be added:
   3.778 +
   3.779 +  \begin{itemize}
   3.780 +
   3.781 +  \item Theorems of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"}, for proving
   3.782 +  monotonicity of inductive definitions whose introduction rules have
   3.783 +  premises involving terms such as @{text "M R\<^sub>i t"}.
   3.784 +
   3.785 +  \item Monotonicity theorems for logical operators, which are of the
   3.786 +  general form @{text "(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>"}.  For example, in
   3.787 +  the case of the operator @{text "\<or>"}, the corresponding theorem is
   3.788 +  \[
   3.789 +  \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"}}
   3.790 +  \]
   3.791 +
   3.792 +  \item De Morgan style equations for reasoning about the ``polarity''
   3.793 +  of expressions, e.g.
   3.794 +  \[
   3.795 +  @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad
   3.796 +  @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}
   3.797 +  \]
   3.798 +
   3.799 +  \item Equations for reducing complex operators to more primitive
   3.800 +  ones whose monotonicity can easily be proved, e.g.
   3.801 +  \[
   3.802 +  @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad
   3.803 +  @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}
   3.804 +  \]
   3.805 +
   3.806 +  \end{itemize}
   3.807 +
   3.808 +  %FIXME: Example of an inductive definition
   3.809 +*}
   3.810 +
   3.811 +
   3.812 +section {* Arithmetic proof support *}
   3.813 +
   3.814 +text {*
   3.815 +  \begin{matharray}{rcl}
   3.816 +    @{method_def (HOL) arith} & : & \isarmeth \\
   3.817 +    @{method_def (HOL) arith_split} & : & \isaratt \\
   3.818 +  \end{matharray}
   3.819 +
   3.820 +  The @{method (HOL) arith} method decides linear arithmetic problems
   3.821 +  (on types @{text nat}, @{text int}, @{text real}).  Any current
   3.822 +  facts are inserted into the goal before running the procedure.
   3.823 +
   3.824 +  The @{method (HOL) arith_split} attribute declares case split rules
   3.825 +  to be expanded before the arithmetic procedure is invoked.
   3.826 +
   3.827 +  Note that a simpler (but faster) version of arithmetic reasoning is
   3.828 +  already performed by the Simplifier.
   3.829 +*}
   3.830 +
   3.831 +
   3.832 +section {* Cases and induction: emulating tactic scripts \label{sec:hol-induct-tac} *}
   3.833 +
   3.834 +text {*
   3.835 +  The following important tactical tools of Isabelle/HOL have been
   3.836 +  ported to Isar.  These should be never used in proper proof texts!
   3.837 +
   3.838 +  \begin{matharray}{rcl}
   3.839 +    @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\
   3.840 +    @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\
   3.841 +    @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\
   3.842 +    @{command_def (HOL) "inductive_cases"} & : & \isartrans{theory}{theory} \\
   3.843 +  \end{matharray}
   3.844 +
   3.845 +  \begin{rail}
   3.846 +    'case\_tac' goalspec? term rule?
   3.847 +    ;
   3.848 +    'induct\_tac' goalspec? (insts * 'and') rule?
   3.849 +    ;
   3.850 +    'ind\_cases' (prop +) ('for' (name +)) ?
   3.851 +    ;
   3.852 +    'inductive\_cases' (thmdecl? (prop +) + 'and')
   3.853 +    ;
   3.854 +
   3.855 +    rule: ('rule' ':' thmref)
   3.856 +    ;
   3.857 +  \end{rail}
   3.858 +
   3.859 +  \begin{descr}
   3.860 +
   3.861 +  \item [@{method (HOL) case_tac} and @{method (HOL) induct_tac}]
   3.862 +  admit to reason about inductive datatypes only (unless an
   3.863 +  alternative rule is given explicitly).  Furthermore, @{method (HOL)
   3.864 +  case_tac} does a classical case split on booleans; @{method (HOL)
   3.865 +  induct_tac} allows only variables to be given as instantiation.
   3.866 +  These tactic emulations feature both goal addressing and dynamic
   3.867 +  instantiation.  Note that named rule cases are \emph{not} provided
   3.868 +  as would be by the proper @{method induct} and @{method cases} proof
   3.869 +  methods (see \secref{sec:cases-induct}).
   3.870 +  
   3.871 +  \item [@{method (HOL) ind_cases} and @{command (HOL)
   3.872 +  "inductive_cases"}] provide an interface to the internal
   3.873 +  \texttt{mk_cases} operation.  Rules are simplified in an
   3.874 +  unrestricted forward manner.
   3.875 +
   3.876 +  While @{method (HOL) ind_cases} is a proof method to apply the
   3.877 +  result immediately as elimination rules, @{command (HOL)
   3.878 +  "inductive_cases"} provides case split theorems at the theory level
   3.879 +  for later use.  The @{keyword "for"} argument of the @{method (HOL)
   3.880 +  ind_cases} method allows to specify a list of variables that should
   3.881 +  be generalized before applying the resulting rule.
   3.882 +
   3.883 +  \end{descr}
   3.884 +*}
   3.885 +
   3.886 +
   3.887 +section {* Executable code *}
   3.888 +
   3.889 +text {*
   3.890 +  Isabelle/Pure provides two generic frameworks to support code
   3.891 +  generation from executable specifications.  Isabelle/HOL
   3.892 +  instantiates these mechanisms in a way that is amenable to end-user
   3.893 +  applications.
   3.894 +
   3.895 +  One framework generates code from both functional and relational
   3.896 +  programs to SML.  See \cite{isabelle-HOL} for further information
   3.897 +  (this actually covers the new-style theory format as well).
   3.898 +
   3.899 +  \begin{matharray}{rcl}
   3.900 +    @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
   3.901 +    @{command_def (HOL) "code_module"} & : & \isartrans{theory}{theory} \\
   3.902 +    @{command_def (HOL) "code_library"} & : & \isartrans{theory}{theory} \\
   3.903 +    @{command_def (HOL) "consts_code"} & : & \isartrans{theory}{theory} \\
   3.904 +    @{command_def (HOL) "types_code"} & : & \isartrans{theory}{theory} \\  
   3.905 +    @{attribute_def (HOL) code} & : & \isaratt \\
   3.906 +  \end{matharray}
   3.907 +
   3.908 +  \begin{rail}
   3.909 +  'value' term
   3.910 +  ;
   3.911 +
   3.912 +  ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
   3.913 +    ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
   3.914 +    'contains' ( ( name '=' term ) + | term + )
   3.915 +  ;
   3.916 +
   3.917 +  modespec: '(' ( name * ) ')'
   3.918 +  ;
   3.919 +
   3.920 +  'consts\_code' (codespec +)
   3.921 +  ;
   3.922 +
   3.923 +  codespec: const template attachment ?
   3.924 +  ;
   3.925 +
   3.926 +  'types\_code' (tycodespec +)
   3.927 +  ;
   3.928 +
   3.929 +  tycodespec: name template attachment ?
   3.930 +  ;
   3.931 +
   3.932 +  const: term
   3.933 +  ;
   3.934 +
   3.935 +  template: '(' string ')'
   3.936 +  ;
   3.937 +
   3.938 +  attachment: 'attach' modespec ? verblbrace text verbrbrace
   3.939 +  ;
   3.940 +
   3.941 +  'code' (name)?
   3.942 +  ;
   3.943 +  \end{rail}
   3.944 +
   3.945 +  \begin{descr}
   3.946 +
   3.947 +  \item [@{command (HOL) "value"}~@{text t}] evaluates and prints a
   3.948 +  term using the code generator.
   3.949 +
   3.950 +  \end{descr}
   3.951 +
   3.952 +  \medskip The other framework generates code from functional programs
   3.953 +  (including overloading using type classes) to SML \cite{SML}, OCaml
   3.954 +  \cite{OCaml} and Haskell \cite{haskell-revised-report}.
   3.955 +  Conceptually, code generation is split up in three steps:
   3.956 +  \emph{selection} of code theorems, \emph{translation} into an
   3.957 +  abstract executable view and \emph{serialization} to a specific
   3.958 +  \emph{target language}.  See \cite{isabelle-codegen} for an
   3.959 +  introduction on how to use it.
   3.960 +
   3.961 +  \begin{matharray}{rcl}
   3.962 +    @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
   3.963 +    @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
   3.964 +    @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
   3.965 +    @{command_def (HOL) "code_datatype"} & : & \isartrans{theory}{theory} \\
   3.966 +    @{command_def (HOL) "code_const"} & : & \isartrans{theory}{theory} \\
   3.967 +    @{command_def (HOL) "code_type"} & : & \isartrans{theory}{theory} \\
   3.968 +    @{command_def (HOL) "code_class"} & : & \isartrans{theory}{theory} \\
   3.969 +    @{command_def (HOL) "code_instance"} & : & \isartrans{theory}{theory} \\
   3.970 +    @{command_def (HOL) "code_monad"} & : & \isartrans{theory}{theory} \\
   3.971 +    @{command_def (HOL) "code_reserved"} & : & \isartrans{theory}{theory} \\
   3.972 +    @{command_def (HOL) "code_include"} & : & \isartrans{theory}{theory} \\
   3.973 +    @{command_def (HOL) "code_modulename"} & : & \isartrans{theory}{theory} \\
   3.974 +    @{command_def (HOL) "code_exception"} & : & \isartrans{theory}{theory} \\
   3.975 +    @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
   3.976 +    @{attribute_def (HOL) code} & : & \isaratt \\
   3.977 +  \end{matharray}
   3.978 +
   3.979 +  \begin{rail}
   3.980 +    'export\_code' ( constexpr + ) ? \\
   3.981 +      ( ( 'in' target ( 'module\_name' string ) ? \\
   3.982 +        ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
   3.983 +    ;
   3.984 +
   3.985 +    'code\_thms' ( constexpr + ) ?
   3.986 +    ;
   3.987 +
   3.988 +    'code\_deps' ( constexpr + ) ?
   3.989 +    ;
   3.990 +
   3.991 +    const: term
   3.992 +    ;
   3.993 +
   3.994 +    constexpr: ( const | 'name.*' | '*' )
   3.995 +    ;
   3.996 +
   3.997 +    typeconstructor: nameref
   3.998 +    ;
   3.999 +
  3.1000 +    class: nameref
  3.1001 +    ;
  3.1002 +
  3.1003 +    target: 'OCaml' | 'SML' | 'Haskell'
  3.1004 +    ;
  3.1005 +
  3.1006 +    'code\_datatype' const +
  3.1007 +    ;
  3.1008 +
  3.1009 +    'code\_const' (const + 'and') \\
  3.1010 +      ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  3.1011 +    ;
  3.1012 +
  3.1013 +    'code\_type' (typeconstructor + 'and') \\
  3.1014 +      ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  3.1015 +    ;
  3.1016 +
  3.1017 +    'code\_class' (class + 'and') \\
  3.1018 +      ( ( '(' target \\
  3.1019 +        ( ( string ('where' \\
  3.1020 +          ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
  3.1021 +    ;
  3.1022 +
  3.1023 +    'code\_instance' (( typeconstructor '::' class ) + 'and') \\
  3.1024 +      ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
  3.1025 +    ;
  3.1026 +
  3.1027 +    'code\_monad' const const target
  3.1028 +    ;
  3.1029 +
  3.1030 +    'code\_reserved' target ( string + )
  3.1031 +    ;
  3.1032 +
  3.1033 +    'code\_include' target ( string ( string | '-') )
  3.1034 +    ;
  3.1035 +
  3.1036 +    'code\_modulename' target ( ( string string ) + )
  3.1037 +    ;
  3.1038 +
  3.1039 +    'code\_exception' ( const + )
  3.1040 +    ;
  3.1041 +
  3.1042 +    syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
  3.1043 +    ;
  3.1044 +
  3.1045 +    'code' ('func' | 'inline') ( 'del' )?
  3.1046 +    ;
  3.1047 +  \end{rail}
  3.1048 +
  3.1049 +  \begin{descr}
  3.1050 +
  3.1051 +  \item [@{command (HOL) "export_code"}] is the canonical interface
  3.1052 +  for generating and serializing code: for a given list of constants,
  3.1053 +  code is generated for the specified target languages.  Abstract code
  3.1054 +  is cached incrementally.  If no constant is given, the currently
  3.1055 +  cached code is serialized.  If no serialization instruction is
  3.1056 +  given, only abstract code is cached.
  3.1057 +
  3.1058 +  Constants may be specified by giving them literally, referring to
  3.1059 +  all executable contants within a certain theory by giving @{text
  3.1060 +  "name.*"}, or referring to \emph{all} executable constants currently
  3.1061 +  available by giving @{text "*"}.
  3.1062 +
  3.1063 +  By default, for each involved theory one corresponding name space
  3.1064 +  module is generated.  Alternativly, a module name may be specified
  3.1065 +  after the @{keyword "module_name"} keyword; then \emph{all} code is
  3.1066 +  placed in this module.
  3.1067 +
  3.1068 +  For \emph{SML} and \emph{OCaml}, the file specification refers to a
  3.1069 +  single file; for \emph{Haskell}, it refers to a whole directory,
  3.1070 +  where code is generated in multiple files reflecting the module
  3.1071 +  hierarchy.  The file specification ``@{text "-"}'' denotes standard
  3.1072 +  output.  For \emph{SML}, omitting the file specification compiles
  3.1073 +  code internally in the context of the current ML session.
  3.1074 +
  3.1075 +  Serializers take an optional list of arguments in parentheses.  For
  3.1076 +  \emph{Haskell} a module name prefix may be given using the ``@{text
  3.1077 +  "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
  3.1078 +  "deriving (Read, Show)"}'' clause to each appropriate datatype
  3.1079 +  declaration.
  3.1080 +
  3.1081 +  \item [@{command (HOL) "code_thms"}] prints a list of theorems
  3.1082 +  representing the corresponding program containing all given
  3.1083 +  constants; if no constants are given, the currently cached code
  3.1084 +  theorems are printed.
  3.1085 +
  3.1086 +  \item [@{command (HOL) "code_deps"}] visualizes dependencies of
  3.1087 +  theorems representing the corresponding program containing all given
  3.1088 +  constants; if no constants are given, the currently cached code
  3.1089 +  theorems are visualized.
  3.1090 +
  3.1091 +  \item [@{command (HOL) "code_datatype"}] specifies a constructor set
  3.1092 +  for a logical type.
  3.1093 +
  3.1094 +  \item [@{command (HOL) "code_const"}] associates a list of constants
  3.1095 +  with target-specific serializations; omitting a serialization
  3.1096 +  deletes an existing serialization.
  3.1097 +
  3.1098 +  \item [@{command (HOL) "code_type"}] associates a list of type
  3.1099 +  constructors with target-specific serializations; omitting a
  3.1100 +  serialization deletes an existing serialization.
  3.1101 +
  3.1102 +  \item [@{command (HOL) "code_class"}] associates a list of classes
  3.1103 +  with target-specific class names; in addition, constants associated
  3.1104 +  with this class may be given target-specific names used for instance
  3.1105 +  declarations; omitting a serialization deletes an existing
  3.1106 +  serialization.  This applies only to \emph{Haskell}.
  3.1107 +
  3.1108 +  \item [@{command (HOL) "code_instance"}] declares a list of type
  3.1109 +  constructor / class instance relations as ``already present'' for a
  3.1110 +  given target.  Omitting a ``@{text "-"}'' deletes an existing
  3.1111 +  ``already present'' declaration.  This applies only to
  3.1112 +  \emph{Haskell}.
  3.1113 +
  3.1114 +  \item [@{command (HOL) "code_monad"}] provides an auxiliary
  3.1115 +  mechanism to generate monadic code.
  3.1116 +
  3.1117 +  \item [@{command (HOL) "code_reserved"}] declares a list of names as
  3.1118 +  reserved for a given target, preventing it to be shadowed by any
  3.1119 +  generated code.
  3.1120 +
  3.1121 +  \item [@{command (HOL) "code_include"}] adds arbitrary named content
  3.1122 +  (``include'') to generated code.  A as last argument ``@{text "-"}''
  3.1123 +  will remove an already added ``include''.
  3.1124 +
  3.1125 +  \item [@{command (HOL) "code_modulename"}] declares aliasings from
  3.1126 +  one module name onto another.
  3.1127 +
  3.1128 +  \item [@{command (HOL) "code_exception"}] declares constants which
  3.1129 +  are not required to have a definition by a defining equations; these
  3.1130 +  are mapped on exceptions instead.
  3.1131 +
  3.1132 +  \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
  3.1133 +  with option ``@{text "del:"}'' deselects) a defining equation for
  3.1134 +  code generation.  Usually packages introducing defining equations
  3.1135 +  provide a resonable default setup for selection.
  3.1136 +
  3.1137 +  \item [@{attribute (HOL) code}@{text inline}] declares (or with
  3.1138 +  option ``@{text "del:"}'' removes) inlining theorems which are
  3.1139 +  applied as rewrite rules to any defining equation during
  3.1140 +  preprocessing.
  3.1141 +
  3.1142 +  \item [@{command (HOL) "print_codesetup"}] gives an overview on
  3.1143 +  selected defining equations, code generator datatypes and
  3.1144 +  preprocessor setup.
  3.1145 +
  3.1146 +  \end{descr}
  3.1147 +*}
  3.1148 +
  3.1149  end
  3.1150 +

     4.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 12:27:19 2008 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 12:29:18 2008 +0200
     4.3 @@ -11,18 +11,1153 @@
     4.4  \isatagtheory
     4.5  \isacommand{theory}\isamarkupfalse%
     4.6  \ HOL{\isacharunderscore}Specific\isanewline
     4.7 -\isakeyword{imports}\ HOL\isanewline
     4.8 -\isakeyword{begin}\isanewline
     4.9 -\isanewline
    4.10 +\isakeyword{imports}\ Main\isanewline
    4.11 +\isakeyword{begin}%
    4.12 +\endisatagtheory
    4.13 +{\isafoldtheory}%
    4.14 +%
    4.15 +\isadelimtheory
    4.16 +%
    4.17 +\endisadelimtheory
    4.18 +%
    4.19 +\isamarkupchapter{HOL specific elements \label{ch:logics}%
    4.20 +}
    4.21 +\isamarkuptrue%
    4.22 +%
    4.23 +\isamarkupsection{Primitive types \label{sec:hol-typedef}%
    4.24 +}
    4.25 +\isamarkuptrue%
    4.26 +%
    4.27 +\begin{isamarkuptext}%
    4.28 +\begin{matharray}{rcl}
    4.29 +    \indexdef{HOL}{command}{typedecl}\mbox{\isa{\isacommand{typedecl}}} & : & \isartrans{theory}{theory} \\
    4.30 +    \indexdef{HOL}{command}{typedef}\mbox{\isa{\isacommand{typedef}}} & : & \isartrans{theory}{proof(prove)} \\
    4.31 +  \end{matharray}
    4.32 +
    4.33 +  \begin{rail}
    4.34 +    'typedecl' typespec infix?
    4.35 +    ;
    4.36 +    'typedef' altname? abstype '=' repset
    4.37 +    ;
    4.38 +
    4.39 +    altname: '(' (name | 'open' | 'open' name) ')'
    4.40 +    ;
    4.41 +    abstype: typespec infix?
    4.42 +    ;
    4.43 +    repset: term ('morphisms' name name)?
    4.44 +    ;
    4.45 +  \end{rail}
    4.46 +
    4.47 +  \begin{descr}
    4.48 +  
    4.49 +  \item [\mbox{\isa{\isacommand{typedecl}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}] is similar to the original \mbox{\isa{\isacommand{typedecl}}} of
    4.50 +  Isabelle/Pure (see \secref{sec:types-pure}), but also declares type
    4.51 +  arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an
    4.52 +  actual HOL type constructor.   %FIXME check, update
    4.53 +  
    4.54 +  \item [\mbox{\isa{\isacommand{typedef}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}}] sets up a goal stating non-emptiness of the set \isa{A}.
    4.55 +  After finishing the proof, the theory will be augmented by a
    4.56 +  Gordon/HOL-style type definition, which establishes a bijection
    4.57 +  between the representing set \isa{A} and the new type \isa{t}.
    4.58 +  
    4.59 +  Technically, \mbox{\isa{\isacommand{typedef}}} defines both a type \isa{t} and a set (term constant) of the same name (an alternative base
    4.60 +  name may be given in parentheses).  The injection from type to set
    4.61 +  is called \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be
    4.62 +  changed via an explicit \mbox{\isa{\isakeyword{morphisms}}} declaration).
    4.63 +  
    4.64 +  Theorems \isa{Rep{\isacharunderscore}t}, \isa{Rep{\isacharunderscore}t{\isacharunderscore}inverse}, and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inverse} provide the most basic characterization as a
    4.65 +  corresponding injection/surjection pair (in both directions).  Rules
    4.66 +  \isa{Rep{\isacharunderscore}t{\isacharunderscore}inject} and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inject} provide a slightly
    4.67 +  more convenient view on the injectivity part, suitable for automated
    4.68 +  proof tools (e.g.\ in \mbox{\isa{simp}} or \mbox{\isa{iff}} declarations).
    4.69 +  Rules \isa{Rep{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Rep{\isacharunderscore}t{\isacharunderscore}induct}, and \isa{Abs{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Abs{\isacharunderscore}t{\isacharunderscore}induct} provide alternative views on
    4.70 +  surjectivity; these are already declared as set or type rules for
    4.71 +  the generic \mbox{\isa{cases}} and \mbox{\isa{induct}} methods.
    4.72 +  
    4.73 +  An alternative name may be specified in parentheses; the default is
    4.74 +  to use \isa{t} as indicated before.  The ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''
    4.75 +  declaration suppresses a separate constant definition for the
    4.76 +  representing set.
    4.77 +
    4.78 +  \end{descr}
    4.79 +
    4.80 +  Note that raw type declarations are rarely used in practice; the
    4.81 +  main application is with experimental (or even axiomatic!) theory
    4.82 +  fragments.  Instead of primitive HOL type definitions, user-level
    4.83 +  theories usually refer to higher-level packages such as \mbox{\isa{\isacommand{record}}} (see \secref{sec:hol-record}) or \mbox{\isa{\isacommand{datatype}}} (see \secref{sec:hol-datatype}).%
    4.84 +\end{isamarkuptext}%
    4.85 +\isamarkuptrue%
    4.86 +%
    4.87 +\isamarkupsection{Adhoc tuples%
    4.88 +}
    4.89 +\isamarkuptrue%
    4.90 +%
    4.91 +\begin{isamarkuptext}%
    4.92 +\begin{matharray}{rcl}
    4.93 +    \mbox{\isa{split{\isacharunderscore}format}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
    4.94 +  \end{matharray}
    4.95 +
    4.96 +  \begin{rail}
    4.97 +    'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))
    4.98 +    ;
    4.99 +  \end{rail}
   4.100 +
   4.101 +  \begin{descr}
   4.102 +  
   4.103 +  \item [\mbox{\isa{split{\isacharunderscore}format}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] puts expressions of
   4.104 +  low-level tuple types into canonical form as specified by the
   4.105 +  arguments given; the \isa{i}-th collection of arguments refers to
   4.106 +  occurrences in premise \isa{i} of the rule.  The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all} arguments in function
   4.107 +  applications to be represented canonically according to their tuple
   4.108 +  type structure.
   4.109 +
   4.110 +  Note that these operations tend to invent funny names for new local
   4.111 +  parameters to be introduced.
   4.112 +
   4.113 +  \end{descr}%
   4.114 +\end{isamarkuptext}%
   4.115 +\isamarkuptrue%
   4.116 +%
   4.117 +\isamarkupsection{Records \label{sec:hol-record}%
   4.118 +}
   4.119 +\isamarkuptrue%
   4.120 +%
   4.121 +\begin{isamarkuptext}%
   4.122 +In principle, records merely generalize the concept of tuples, where
   4.123 +  components may be addressed by labels instead of just position.  The
   4.124 +  logical infrastructure of records in Isabelle/HOL is slightly more
   4.125 +  advanced, though, supporting truly extensible record schemes.  This
   4.126 +  admits operations that are polymorphic with respect to record
   4.127 +  extension, yielding ``object-oriented'' effects like (single)
   4.128 +  inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for more
   4.129 +  details on object-oriented verification and record subtyping in HOL.%
   4.130 +\end{isamarkuptext}%
   4.131 +\isamarkuptrue%
   4.132 +%
   4.133 +\isamarkupsubsection{Basic concepts%
   4.134 +}
   4.135 +\isamarkuptrue%
   4.136 +%
   4.137 +\begin{isamarkuptext}%
   4.138 +Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
   4.139 +  at the level of terms and types.  The notation is as follows:
   4.140 +
   4.141 +  \begin{center}
   4.142 +  \begin{tabular}{l|l|l}
   4.143 +    & record terms & record types \\ \hline
   4.144 +    fixed & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isasymrparr}{\isachardoublequote}} \\
   4.145 +    schematic & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isasymrparr}{\isachardoublequote}} &
   4.146 +      \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ M{\isasymrparr}{\isachardoublequote}} \\
   4.147 +  \end{tabular}
   4.148 +  \end{center}
   4.149 +
   4.150 +  \noindent The ASCII representation of \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} is \isa{{\isachardoublequote}{\isacharparenleft}{\isacharbar}\ x\ {\isacharequal}\ a\ {\isacharbar}{\isacharparenright}{\isachardoublequote}}.
   4.151 +
   4.152 +  A fixed record \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} has field \isa{x} of value
   4.153 +  \isa{a} and field \isa{y} of value \isa{b}.  The corresponding
   4.154 +  type is \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isasymrparr}{\isachardoublequote}}, assuming that \isa{{\isachardoublequote}a\ {\isacharcolon}{\isacharcolon}\ A{\isachardoublequote}}
   4.155 +  and \isa{{\isachardoublequote}b\ {\isacharcolon}{\isacharcolon}\ B{\isachardoublequote}}.
   4.156 +
   4.157 +  A record scheme like \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isasymrparr}{\isachardoublequote}} contains fields
   4.158 +  \isa{x} and \isa{y} as before, but also possibly further fields
   4.159 +  as indicated by the ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' notation (which is actually part
   4.160 +  of the syntax).  The improper field ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' of a record
   4.161 +  scheme is called the \emph{more part}.  Logically it is just a free
   4.162 +  variable, which is occasionally referred to as ``row variable'' in
   4.163 +  the literature.  The more part of a record scheme may be
   4.164 +  instantiated by zero or more further components.  For example, the
   4.165 +  previous scheme may get instantiated to \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ z\ {\isacharequal}\ c{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isacharprime}{\isachardoublequote}}, where \isa{m{\isacharprime}} refers to a different more part.
   4.166 +  Fixed records are special instances of record schemes, where
   4.167 +  ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' is properly terminated by the \isa{{\isachardoublequote}{\isacharparenleft}{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ unit{\isachardoublequote}}
   4.168 +  element.  In fact, \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} is just an abbreviation
   4.169 +  for \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}{\isachardoublequote}}.
   4.170 +  
   4.171 +  \medskip Two key observations make extensible records in a simply
   4.172 +  typed language like HOL work out:
   4.173 +
   4.174 +  \begin{enumerate}
   4.175 +
   4.176 +  \item the more part is internalized, as a free term or type
   4.177 +  variable,
   4.178 +
   4.179 +  \item field names are externalized, they cannot be accessed within the logic
   4.180 +  as first-class values.
   4.181 +
   4.182 +  \end{enumerate}
   4.183 +
   4.184 +  \medskip In Isabelle/HOL record types have to be defined explicitly,
   4.185 +  fixing their field names and types, and their (optional) parent
   4.186 +  record.  Afterwards, records may be formed using above syntax, while
   4.187 +  obeying the canonical order of fields as given by their declaration.
   4.188 +  The record package provides several standard operations like
   4.189 +  selectors and updates.  The common setup for various generic proof
   4.190 +  tools enable succinct reasoning patterns.  See also the Isabelle/HOL
   4.191 +  tutorial \cite{isabelle-hol-book} for further instructions on using
   4.192 +  records in practice.%
   4.193 +\end{isamarkuptext}%
   4.194 +\isamarkuptrue%
   4.195 +%
   4.196 +\isamarkupsubsection{Record specifications%
   4.197 +}
   4.198 +\isamarkuptrue%
   4.199 +%
   4.200 +\begin{isamarkuptext}%
   4.201 +\begin{matharray}{rcl}
   4.202 +    \indexdef{HOL}{command}{record}\mbox{\isa{\isacommand{record}}} & : & \isartrans{theory}{theory} \\
   4.203 +  \end{matharray}
   4.204 +
   4.205 +  \begin{rail}
   4.206 +    'record' typespec '=' (type '+')? (constdecl +)
   4.207 +    ;
   4.208 +  \end{rail}
   4.209 +
   4.210 +  \begin{descr}
   4.211 +
   4.212 +  \item [\mbox{\isa{\isacommand{record}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}\ {\isacharplus}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}}] defines
   4.213 +  extensible record type \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}},
   4.214 +  derived from the optional parent record \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} by adding new
   4.215 +  field components \isa{{\isachardoublequote}c\isactrlsub i\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} etc.
   4.216 +
   4.217 +  The type variables of \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i{\isachardoublequote}} need to be
   4.218 +  covered by the (distinct) parameters \isa{{\isachardoublequote}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isachardoublequote}}.  Type constructor \isa{t} has to be new, while \isa{{\isasymtau}} needs to specify an instance of an existing record type.  At
   4.219 +  least one new field \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} has to be specified.
   4.220 +  Basically, field names need to belong to a unique record.  This is
   4.221 +  not a real restriction in practice, since fields are qualified by
   4.222 +  the record name internally.
   4.223 +
   4.224 +  The parent record specification \isa{{\isasymtau}} is optional; if omitted
   4.225 +  \isa{t} becomes a root record.  The hierarchy of all records
   4.226 +  declared within a theory context forms a forest structure, i.e.\ a
   4.227 +  set of trees starting with a root record each.  There is no way to
   4.228 +  merge multiple parent records!
   4.229 +
   4.230 +  For convenience, \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} is made a
   4.231 +  type abbreviation for the fixed record type \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}}, likewise is \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharcomma}\ {\isasymzeta}{\isacharparenright}\ t{\isacharunderscore}scheme{\isachardoublequote}} made an abbreviation for
   4.232 +  \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}}.
   4.233 +
   4.234 +  \end{descr}%
   4.235 +\end{isamarkuptext}%
   4.236 +\isamarkuptrue%
   4.237 +%
   4.238 +\isamarkupsubsection{Record operations%
   4.239 +}
   4.240 +\isamarkuptrue%
   4.241 +%
   4.242 +\begin{isamarkuptext}%
   4.243 +Any record definition of the form presented above produces certain
   4.244 +  standard operations.  Selectors and updates are provided for any
   4.245 +  field, including the improper one ``\isa{more}''.  There are also
   4.246 +  cumulative record constructor functions.  To simplify the
   4.247 +  presentation below, we assume for now that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} is a root record with fields \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}}.
   4.248 +
   4.249 +  \medskip \textbf{Selectors} and \textbf{updates} are available for
   4.250 +  any field (including ``\isa{more}''):
   4.251 +
   4.252 +  \begin{matharray}{lll}
   4.253 +    \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
   4.254 +    \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
   4.255 +  \end{matharray}
   4.256 +
   4.257 +  There is special syntax for application of updates: \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} abbreviates term \isa{{\isachardoublequote}x{\isacharunderscore}update\ a\ r{\isachardoublequote}}.  Further notation for
   4.258 +  repeated updates is also available: \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}y\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}{\isasymlparr}z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}} may be written \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ y\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}}.  Note that
   4.259 +  because of postfix notation the order of fields shown here is
   4.260 +  reverse than in the actual term.  Since repeated updates are just
   4.261 +  function applications, fields may be freely permuted in \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ y\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}}, as far as logical equality is concerned.
   4.262 +  Thus commutativity of independent updates can be proven within the
   4.263 +  logic for any two fields, but not as a general theorem.
   4.264 +
   4.265 +  \medskip The \textbf{make} operation provides a cumulative record
   4.266 +  constructor function:
   4.267 +
   4.268 +  \begin{matharray}{lll}
   4.269 +    \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}} \\
   4.270 +  \end{matharray}
   4.271 +
   4.272 +  \medskip We now reconsider the case of non-root records, which are
   4.273 +  derived of some parent.  In general, the latter may depend on
   4.274 +  another parent as well, resulting in a list of \emph{ancestor
   4.275 +  records}.  Appending the lists of fields of all ancestors results in
   4.276 +  a certain field prefix.  The record package automatically takes care
   4.277 +  of this by lifting operations over this context of ancestor fields.
   4.278 +  Assuming that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} has ancestor
   4.279 +  fields \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isachardoublequote}},
   4.280 +  the above record operations will get the following types:
   4.281 +
   4.282 +  \begin{matharray}{lll}
   4.283 +    \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
   4.284 +    \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
   4.285 +    \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymrho}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymrho}\isactrlsub k\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}} \\
   4.286 +  \end{matharray}
   4.287 +  \noindent
   4.288 +
   4.289 +  \medskip Some further operations address the extension aspect of a
   4.290 +  derived record scheme specifically: \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} produces a
   4.291 +  record fragment consisting of exactly the new fields introduced here
   4.292 +  (the result may serve as a more part elsewhere); \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}}
   4.293 +  takes a fixed record and adds a given more part; \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} restricts a record scheme to a fixed record.
   4.294 +
   4.295 +  \begin{matharray}{lll}
   4.296 +    \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}} \\
   4.297 +    \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}\ {\isasymRightarrow}\ {\isasymzeta}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
   4.298 +    \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}} \\
   4.299 +  \end{matharray}
   4.300 +
   4.301 +  \noindent Note that \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} and \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} coincide
   4.302 +  for root records.%
   4.303 +\end{isamarkuptext}%
   4.304 +\isamarkuptrue%
   4.305 +%
   4.306 +\isamarkupsubsection{Derived rules and proof tools%
   4.307 +}
   4.308 +\isamarkuptrue%
   4.309 +%
   4.310 +\begin{isamarkuptext}%
   4.311 +The record package proves several results internally, declaring
   4.312 +  these facts to appropriate proof tools.  This enables users to
   4.313 +  reason about record structures quite conveniently.  Assume that
   4.314 +  \isa{t} is a record type as specified above.
   4.315 +
   4.316 +  \begin{enumerate}
   4.317 +  
   4.318 +  \item Standard conversions for selectors or updates applied to
   4.319 +  record constructor terms are made part of the default Simplifier
   4.320 +  context; thus proofs by reduction of basic operations merely require
   4.321 +  the \mbox{\isa{simp}} method without further arguments.  These rules
   4.322 +  are available as \isa{{\isachardoublequote}t{\isachardot}simps{\isachardoublequote}}, too.
   4.323 +  
   4.324 +  \item Selectors applied to updated records are automatically reduced
   4.325 +  by an internal simplification procedure, which is also part of the
   4.326 +  standard Simplifier setup.
   4.327 +
   4.328 +  \item Inject equations of a form analogous to \isa{{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}\ y{\isacharprime}{\isacharparenright}\ {\isasymequiv}\ x\ {\isacharequal}\ x{\isacharprime}\ {\isasymand}\ y\ {\isacharequal}\ y{\isacharprime}{\isachardoublequote}} are declared to the Simplifier and Classical
   4.329 +  Reasoner as \mbox{\isa{iff}} rules.  These rules are available as
   4.330 +  \isa{{\isachardoublequote}t{\isachardot}iffs{\isachardoublequote}}.
   4.331 +
   4.332 +  \item The introduction rule for record equality analogous to \isa{{\isachardoublequote}x\ r\ {\isacharequal}\ x\ r{\isacharprime}\ {\isasymLongrightarrow}\ y\ r\ {\isacharequal}\ y\ r{\isacharprime}\ {\isasymdots}\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ r{\isacharprime}{\isachardoublequote}} is declared to the Simplifier,
   4.333 +  and as the basic rule context as ``\mbox{\isa{intro}}\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}''.
   4.334 +  The rule is called \isa{{\isachardoublequote}t{\isachardot}equality{\isachardoublequote}}.
   4.335 +
   4.336 +  \item Representations of arbitrary record expressions as canonical
   4.337 +  constructor terms are provided both in \mbox{\isa{cases}} and \mbox{\isa{induct}} format (cf.\ the generic proof methods of the same name,
   4.338 +  \secref{sec:cases-induct}).  Several variations are available, for
   4.339 +  fixed records, record schemes, more parts etc.
   4.340 +  
   4.341 +  The generic proof methods are sufficiently smart to pick the most
   4.342 +  sensible rule according to the type of the indicated record
   4.343 +  expression: users just need to apply something like ``\isa{{\isachardoublequote}{\isacharparenleft}cases\ r{\isacharparenright}{\isachardoublequote}}'' to a certain proof problem.
   4.344 +
   4.345 +  \item The derived record operations \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} are \emph{not}
   4.346 +  treated automatically, but usually need to be expanded by hand,
   4.347 +  using the collective fact \isa{{\isachardoublequote}t{\isachardot}defs{\isachardoublequote}}.
   4.348 +
   4.349 +  \end{enumerate}%
   4.350 +\end{isamarkuptext}%
   4.351 +\isamarkuptrue%
   4.352 +%
   4.353 +\isamarkupsection{Datatypes \label{sec:hol-datatype}%
   4.354 +}
   4.355 +\isamarkuptrue%
   4.356 +%
   4.357 +\begin{isamarkuptext}%
   4.358 +\begin{matharray}{rcl}
   4.359 +    \indexdef{HOL}{command}{datatype}\mbox{\isa{\isacommand{datatype}}} & : & \isartrans{theory}{theory} \\
   4.360 +    \indexdef{HOL}{command}{rep-datatype}\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
   4.361 +  \end{matharray}
   4.362 +
   4.363 +  \begin{rail}
   4.364 +    'datatype' (dtspec + 'and')
   4.365 +    ;
   4.366 +    'rep\_datatype' (name *) dtrules
   4.367 +    ;
   4.368 +
   4.369 +    dtspec: parname? typespec infix? '=' (cons + '|')
   4.370 +    ;
   4.371 +    cons: name (type *) mixfix?
   4.372 +    ;
   4.373 +    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
   4.374 +  \end{rail}
   4.375 +
   4.376 +  \begin{descr}
   4.377 +
   4.378 +  \item [\mbox{\isa{\isacommand{datatype}}}] defines inductive datatypes in
   4.379 +  HOL.
   4.380 +
   4.381 +  \item [\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}] represents existing types as
   4.382 +  inductive ones, generating the standard infrastructure of derived
   4.383 +  concepts (primitive recursion etc.).
   4.384 +
   4.385 +  \end{descr}
   4.386 +
   4.387 +  The induction and exhaustion theorems generated provide case names
   4.388 +  according to the constructors involved, while parameters are named
   4.389 +  after the types (see also \secref{sec:cases-induct}).
   4.390 +
   4.391 +  See \cite{isabelle-HOL} for more details on datatypes, but beware of
   4.392 +  the old-style theory syntax being used there!  Apart from proper
   4.393 +  proof methods for case-analysis and induction, there are also
   4.394 +  emulations of ML tactics \mbox{\isa{case{\isacharunderscore}tac}} and \mbox{\isa{induct{\isacharunderscore}tac}} available, see \secref{sec:hol-induct-tac}; these admit
   4.395 +  to refer directly to the internal structure of subgoals (including
   4.396 +  internally bound parameters).%
   4.397 +\end{isamarkuptext}%
   4.398 +\isamarkuptrue%
   4.399 +%
   4.400 +\isamarkupsection{Recursive functions \label{sec:recursion}%
   4.401 +}
   4.402 +\isamarkuptrue%
   4.403 +%
   4.404 +\begin{isamarkuptext}%
   4.405 +\begin{matharray}{rcl}
   4.406 +    \indexdef{HOL}{command}{primrec}\mbox{\isa{\isacommand{primrec}}} & : & \isarkeep{local{\dsh}theory} \\
   4.407 +    \indexdef{HOL}{command}{fun}\mbox{\isa{\isacommand{fun}}} & : & \isarkeep{local{\dsh}theory} \\
   4.408 +    \indexdef{HOL}{command}{function}\mbox{\isa{\isacommand{function}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
   4.409 +    \indexdef{HOL}{command}{termination}\mbox{\isa{\isacommand{termination}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
   4.410 +  \end{matharray}
   4.411 +
   4.412 +  \railalias{funopts}{function\_opts}  %FIXME ??
   4.413 +
   4.414 +  \begin{rail}
   4.415 +    'primrec' target? fixes 'where' equations
   4.416 +    ;
   4.417 +    equations: (thmdecl? prop + '|')
   4.418 +    ;
   4.419 +    ('fun' | 'function') (funopts)? fixes 'where' clauses
   4.420 +    ;
   4.421 +    clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
   4.422 +    ;
   4.423 +    funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' |
   4.424 +    'default' term) + ',') ')'
   4.425 +    ;
   4.426 +    'termination' ( term )?
   4.427 +  \end{rail}
   4.428 +
   4.429 +  \begin{descr}
   4.430 +
   4.431 +  \item [\mbox{\isa{\isacommand{primrec}}}] defines primitive recursive
   4.432 +  functions over datatypes, see also \cite{isabelle-HOL}.
   4.433 +
   4.434 +  \item [\mbox{\isa{\isacommand{function}}}] defines functions by general
   4.435 +  wellfounded recursion. A detailed description with examples can be
   4.436 +  found in \cite{isabelle-function}. The function is specified by a
   4.437 +  set of (possibly conditional) recursive equations with arbitrary
   4.438 +  pattern matching. The command generates proof obligations for the
   4.439 +  completeness and the compatibility of patterns.
   4.440 +
   4.441 +  The defined function is considered partial, and the resulting
   4.442 +  simplification rules (named \isa{{\isachardoublequote}f{\isachardot}psimps{\isachardoublequote}}) and induction rule
   4.443 +  (named \isa{{\isachardoublequote}f{\isachardot}pinduct{\isachardoublequote}}) are guarded by a generated domain
   4.444 +  predicate \isa{{\isachardoublequote}f{\isacharunderscore}dom{\isachardoublequote}}. The \mbox{\isa{\isacommand{termination}}}
   4.445 +  command can then be used to establish that the function is total.
   4.446 +
   4.447 +  \item [\mbox{\isa{\isacommand{fun}}}] is a shorthand notation for
   4.448 +  ``\mbox{\isa{\isacommand{function}}}~\isa{{\isachardoublequote}{\isacharparenleft}sequential{\isacharparenright}{\isachardoublequote}}, followed by
   4.449 +  automated proof attempts regarding pattern matching and termination.
   4.450 +  See \cite{isabelle-function} for further details.
   4.451 +
   4.452 +  \item [\mbox{\isa{\isacommand{termination}}}~\isa{f}] commences a
   4.453 +  termination proof for the previously defined function \isa{f}.  If
   4.454 +  this is omitted, the command refers to the most recent function
   4.455 +  definition.  After the proof is closed, the recursive equations and
   4.456 +  the induction principle is established.
   4.457 +
   4.458 +  \end{descr}
   4.459 +
   4.460 +  %FIXME check
   4.461 +
   4.462 +  Recursive definitions introduced by both the \mbox{\isa{\isacommand{primrec}}} and the \mbox{\isa{\isacommand{function}}} command accommodate
   4.463 +  reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isachardoublequote}c{\isachardot}induct{\isachardoublequote}} (where \isa{c} is the name of the function definition)
   4.464 +  refers to a specific induction rule, with parameters named according
   4.465 +  to the user-specified equations.  Case names of \mbox{\isa{\isacommand{primrec}}} are that of the datatypes involved, while those of
   4.466 +  \mbox{\isa{\isacommand{function}}} are numbered (starting from 1).
   4.467 +
   4.468 +  The equations provided by these packages may be referred later as
   4.469 +  theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective)
   4.470 +  name of the functions defined.  Individual equations may be named
   4.471 +  explicitly as well.
   4.472 +
   4.473 +  The \mbox{\isa{\isacommand{function}}} command accepts the following
   4.474 +  options.
   4.475 +
   4.476 +  \begin{descr}
   4.477 +
   4.478 +  \item [\isa{sequential}] enables a preprocessor which
   4.479 +  disambiguates overlapping patterns by making them mutually disjoint.
   4.480 +  Earlier equations take precedence over later ones.  This allows to
   4.481 +  give the specification in a format very similar to functional
   4.482 +  programming.  Note that the resulting simplification and induction
   4.483 +  rules correspond to the transformed specification, not the one given
   4.484 +  originally. This usually means that each equation given by the user
   4.485 +  may result in several theroems.  Also note that this automatic
   4.486 +  transformation only works for ML-style datatype patterns.
   4.487 +
   4.488 +  \item [\isa{{\isachardoublequote}{\isasymIN}\ name{\isachardoublequote}}] gives the target for the definition.
   4.489 +  %FIXME ?!?
   4.490 +
   4.491 +  \item [\isa{domintros}] enables the automated generation of
   4.492 +  introduction rules for the domain predicate. While mostly not
   4.493 +  needed, they can be helpful in some proofs about partial functions.
   4.494 +
   4.495 +  \item [\isa{tailrec}] generates the unconstrained recursive
   4.496 +  equations even without a termination proof, provided that the
   4.497 +  function is tail-recursive. This currently only works
   4.498 +
   4.499 +  \item [\isa{{\isachardoublequote}default\ d{\isachardoublequote}}] allows to specify a default value for a
   4.500 +  (partial) function, which will ensure that \isa{{\isachardoublequote}f\ x\ {\isacharequal}\ d\ x{\isachardoublequote}}
   4.501 +  whenever \isa{{\isachardoublequote}x\ {\isasymnotin}\ f{\isacharunderscore}dom{\isachardoublequote}}.
   4.502 +
   4.503 +  \end{descr}%
   4.504 +\end{isamarkuptext}%
   4.505 +\isamarkuptrue%
   4.506 +%
   4.507 +\isamarkupsubsection{Proof methods related to recursive definitions%
   4.508 +}
   4.509 +\isamarkuptrue%
   4.510 +%
   4.511 +\begin{isamarkuptext}%
   4.512 +\begin{matharray}{rcl}
   4.513 +    \indexdef{HOL}{method}{pat-completeness}\mbox{\isa{pat{\isacharunderscore}completeness}} & : & \isarmeth \\
   4.514 +    \indexdef{HOL}{method}{relation}\mbox{\isa{relation}} & : & \isarmeth \\
   4.515 +    \indexdef{HOL}{method}{lexicographic-order}\mbox{\isa{lexicographic{\isacharunderscore}order}} & : & \isarmeth \\
   4.516 +  \end{matharray}
   4.517 +
   4.518 +  \begin{rail}
   4.519 +    'relation' term
   4.520 +    ;
   4.521 +    'lexicographic\_order' (clasimpmod *)
   4.522 +    ;
   4.523 +  \end{rail}
   4.524 +
   4.525 +  \begin{descr}
   4.526 +
   4.527 +  \item [\mbox{\isa{pat{\isacharunderscore}completeness}}] is a specialized method to
   4.528 +  solve goals regarding the completeness of pattern matching, as
   4.529 +  required by the \mbox{\isa{\isacommand{function}}} package (cf.\
   4.530 +  \cite{isabelle-function}).
   4.531 +
   4.532 +  \item [\mbox{\isa{relation}}~\isa{R}] introduces a termination
   4.533 +  proof using the relation \isa{R}.  The resulting proof state will
   4.534 +  contain goals expressing that \isa{R} is wellfounded, and that the
   4.535 +  arguments of recursive calls decrease with respect to \isa{R}.
   4.536 +  Usually, this method is used as the initial proof step of manual
   4.537 +  termination proofs.
   4.538 +
   4.539 +  \item [\mbox{\isa{lexicographic{\isacharunderscore}order}}] attempts a fully
   4.540 +  automated termination proof by searching for a lexicographic
   4.541 +  combination of size measures on the arguments of the function. The
   4.542 +  method accepts the same arguments as the \mbox{\isa{auto}} method,
   4.543 +  which it uses internally to prove local descents.  The same context
   4.544 +  modifiers as for \mbox{\isa{auto}} are accepted, see
   4.545 +  \secref{sec:clasimp}.
   4.546 +
   4.547 +  In case of failure, extensive information is printed, which can help
   4.548 +  to analyse the situation (cf.\ \cite{isabelle-function}).
   4.549 +
   4.550 +  \end{descr}%
   4.551 +\end{isamarkuptext}%
   4.552 +\isamarkuptrue%
   4.553 +%
   4.554 +\isamarkupsubsection{Old-style recursive function definitions (TFL)%
   4.555 +}
   4.556 +\isamarkuptrue%
   4.557 +%
   4.558 +\begin{isamarkuptext}%
   4.559 +The old TFL commands \mbox{\isa{\isacommand{recdef}}} and \mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}} for defining recursive are mostly obsolete; \mbox{\isa{\isacommand{function}}} or \mbox{\isa{\isacommand{fun}}} should be used instead.
   4.560 +
   4.561 +  \begin{matharray}{rcl}
   4.562 +    \indexdef{HOL}{command}{recdef}\mbox{\isa{\isacommand{recdef}}} & : & \isartrans{theory}{theory} \\
   4.563 +    \indexdef{HOL}{command}{recdef-tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
   4.564 +  \end{matharray}
   4.565 +
   4.566 +  \begin{rail}
   4.567 +    'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
   4.568 +    ;
   4.569 +    recdeftc thmdecl? tc
   4.570 +    ;
   4.571 +    hints: '(' 'hints' (recdefmod *) ')'
   4.572 +    ;
   4.573 +    recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
   4.574 +    ;
   4.575 +    tc: nameref ('(' nat ')')?
   4.576 +    ;
   4.577 +  \end{rail}
   4.578 +
   4.579 +  \begin{descr}
   4.580 +  
   4.581 +  \item [\mbox{\isa{\isacommand{recdef}}}] defines general well-founded
   4.582 +  recursive functions (using the TFL package), see also
   4.583 +  \cite{isabelle-HOL}.  The ``\isa{{\isachardoublequote}{\isacharparenleft}permissive{\isacharparenright}{\isachardoublequote}}'' option tells
   4.584 +  TFL to recover from failed proof attempts, returning unfinished
   4.585 +  results.  The \isa{recdef{\isacharunderscore}simp}, \isa{recdef{\isacharunderscore}cong}, and \isa{recdef{\isacharunderscore}wf} hints refer to auxiliary rules to be used in the internal
   4.586 +  automated proof process of TFL.  Additional \mbox{\isa{clasimpmod}}
   4.587 +  declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
   4.588 +  context of the Simplifier (cf.\ \secref{sec:simplifier}) and
   4.589 +  Classical reasoner (cf.\ \secref{sec:classical}).
   4.590 +  
   4.591 +  \item [\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the
   4.592 +  proof for leftover termination condition number \isa{i} (default
   4.593 +  1) as generated by a \mbox{\isa{\isacommand{recdef}}} definition of
   4.594 +  constant \isa{c}.
   4.595 +  
   4.596 +  Note that in most cases, \mbox{\isa{\isacommand{recdef}}} is able to finish
   4.597 +  its internal proofs without manual intervention.
   4.598 +
   4.599 +  \end{descr}
   4.600 +
   4.601 +  \medskip Hints for \mbox{\isa{\isacommand{recdef}}} may be also declared
   4.602 +  globally, using the following attributes.
   4.603 +
   4.604 +  \begin{matharray}{rcl}
   4.605 +    \indexdef{HOL}{attribute}{recdef-simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\
   4.606 +    \indexdef{HOL}{attribute}{recdef-cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\
   4.607 +    \indexdef{HOL}{attribute}{recdef-wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\
   4.608 +  \end{matharray}
   4.609 +
   4.610 +  \begin{rail}
   4.611 +    ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
   4.612 +    ;
   4.613 +  \end{rail}%
   4.614 +\end{isamarkuptext}%
   4.615 +\isamarkuptrue%
   4.616 +%
   4.617 +\isamarkupsection{Definition by specification \label{sec:hol-specification}%
   4.618 +}
   4.619 +\isamarkuptrue%
   4.620 +%
   4.621 +\begin{isamarkuptext}%
   4.622 +\begin{matharray}{rcl}
   4.623 +    \indexdef{HOL}{command}{specification}\mbox{\isa{\isacommand{specification}}} & : & \isartrans{theory}{proof(prove)} \\
   4.624 +    \indexdef{HOL}{command}{ax-specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\
   4.625 +  \end{matharray}
   4.626 +
   4.627 +  \begin{rail}
   4.628 +  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
   4.629 +  ;
   4.630 +  decl: ((name ':')? term '(' 'overloaded' ')'?)
   4.631 +  \end{rail}
   4.632 +
   4.633 +  \begin{descr}
   4.634 +
   4.635 +  \item [\mbox{\isa{\isacommand{specification}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
   4.636 +  goal stating the existence of terms with the properties specified to
   4.637 +  hold for the constants given in \isa{decls}.  After finishing the
   4.638 +  proof, the theory will be augmented with definitions for the given
   4.639 +  constants, as well as with theorems stating the properties for these
   4.640 +  constants.
   4.641 +
   4.642 +  \item [\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
   4.643 +  up a goal stating the existence of terms with the properties
   4.644 +  specified to hold for the constants given in \isa{decls}.  After
   4.645 +  finishing the proof, the theory will be augmented with axioms
   4.646 +  expressing the properties given in the first place.
   4.647 +
   4.648 +  \item [\isa{decl}] declares a constant to be defined by the
   4.649 +  specification given.  The definition for the constant \isa{c} is
   4.650 +  bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
   4.651 +  the declaration.  Overloaded constants should be declared as such.
   4.652 +
   4.653 +  \end{descr}
   4.654 +
   4.655 +  Whether to use \mbox{\isa{\isacommand{specification}}} or \mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} is to some extent a matter of style.  \mbox{\isa{\isacommand{specification}}} introduces no new axioms, and so by
   4.656 +  construction cannot introduce inconsistencies, whereas \mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} does introduce axioms, but only after the
   4.657 +  user has explicitly proven it to be safe.  A practical issue must be
   4.658 +  considered, though: After introducing two constants with the same
   4.659 +  properties using \mbox{\isa{\isacommand{specification}}}, one can prove
   4.660 +  that the two constants are, in fact, equal.  If this might be a
   4.661 +  problem, one should use \mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}.%
   4.662 +\end{isamarkuptext}%
   4.663 +\isamarkuptrue%
   4.664 +%
   4.665 +\isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
   4.666 +}
   4.667 +\isamarkuptrue%
   4.668 +%
   4.669 +\begin{isamarkuptext}%
   4.670 +An \textbf{inductive definition} specifies the least predicate (or
   4.671 +  set) \isa{R} closed under given rules: applying a rule to elements
   4.672 +  of \isa{R} yields a result within \isa{R}.  For example, a
   4.673 +  structural operational semantics is an inductive definition of an
   4.674 +  evaluation relation.
   4.675 +
   4.676 +  Dually, a \textbf{coinductive definition} specifies the greatest
   4.677 +  predicate~/ set \isa{R} that is consistent with given rules: every
   4.678 +  element of \isa{R} can be seen as arising by applying a rule to
   4.679 +  elements of \isa{R}.  An important example is using bisimulation
   4.680 +  relations to formalise equivalence of processes and infinite data
   4.681 +  structures.
   4.682 +
   4.683 +  \medskip The HOL package is related to the ZF one, which is
   4.684 +  described in a separate paper,\footnote{It appeared in CADE
   4.685 +  \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
   4.686 +  which you should refer to in case of difficulties.  The package is
   4.687 +  simpler than that of ZF thanks to implicit type-checking in HOL.
   4.688 +  The types of the (co)inductive predicates (or sets) determine the
   4.689 +  domain of the fixedpoint definition, and the package does not have
   4.690 +  to use inference rules for type-checking.
   4.691 +
   4.692 +  \begin{matharray}{rcl}
   4.693 +    \indexdef{HOL}{command}{inductive}\mbox{\isa{\isacommand{inductive}}} & : & \isarkeep{local{\dsh}theory} \\
   4.694 +    \indexdef{HOL}{command}{inductive-set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
   4.695 +    \indexdef{HOL}{command}{coinductive}\mbox{\isa{\isacommand{coinductive}}} & : & \isarkeep{local{\dsh}theory} \\
   4.696 +    \indexdef{HOL}{command}{coinductive-set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
   4.697 +    \indexdef{HOL}{attribute}{mono}\mbox{\isa{mono}} & : & \isaratt \\
   4.698 +  \end{matharray}
   4.699 +
   4.700 +  \begin{rail}
   4.701 +    ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
   4.702 +    ('where' clauses)? ('monos' thmrefs)?
   4.703 +    ;
   4.704 +    clauses: (thmdecl? prop + '|')
   4.705 +    ;
   4.706 +    'mono' (() | 'add' | 'del')
   4.707 +    ;
   4.708 +  \end{rail}
   4.709 +
   4.710 +  \begin{descr}
   4.711 +
   4.712 +  \item [\mbox{\isa{\isacommand{inductive}}} and \mbox{\isa{\isacommand{coinductive}}}] define (co)inductive predicates from the
   4.713 +  introduction rules given in the \mbox{\isa{\isakeyword{where}}} part.  The
   4.714 +  optional \mbox{\isa{\isakeyword{for}}} part contains a list of parameters of the
   4.715 +  (co)inductive predicates that remain fixed throughout the
   4.716 +  definition.  The optional \mbox{\isa{\isakeyword{monos}}} section contains
   4.717 +  \emph{monotonicity theorems}, which are required for each operator
   4.718 +  applied to a recursive set in the introduction rules.  There
   4.719 +  \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}},
   4.720 +  for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule!
   4.721 +
   4.722 +  \item [\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} and \mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}] are wrappers for to the previous commands,
   4.723 +  allowing the definition of (co)inductive sets.
   4.724 +
   4.725 +  \item [\mbox{\isa{mono}}] declares monotonicity rules.  These
   4.726 +  rule are involved in the automated monotonicity proof of \mbox{\isa{\isacommand{inductive}}}.
   4.727 +
   4.728 +  \end{descr}%
   4.729 +\end{isamarkuptext}%
   4.730 +\isamarkuptrue%
   4.731 +%
   4.732 +\isamarkupsubsection{Derived rules%
   4.733 +}
   4.734 +\isamarkuptrue%
   4.735 +%
   4.736 +\begin{isamarkuptext}%
   4.737 +Each (co)inductive definition \isa{R} adds definitions to the
   4.738 +  theory and also proves some theorems:
   4.739 +
   4.740 +  \begin{description}
   4.741 +
   4.742 +  \item [\isa{R{\isachardot}intros}] is the list of introduction rules as proven
   4.743 +  theorems, for the recursive predicates (or sets).  The rules are
   4.744 +  also available individually, using the names given them in the
   4.745 +  theory file;
   4.746 +
   4.747 +  \item [\isa{R{\isachardot}cases}] is the case analysis (or elimination) rule;
   4.748 +
   4.749 +  \item [\isa{R{\isachardot}induct} or \isa{R{\isachardot}coinduct}] is the (co)induction
   4.750 +  rule.
   4.751 +
   4.752 +  \end{description}
   4.753 +
   4.754 +  When several predicates \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardoublequote}} are
   4.755 +  defined simultaneously, the list of introduction rules is called
   4.756 +  \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}intros{\isachardoublequote}}, the case analysis rules are
   4.757 +  called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isachardot}cases{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardot}cases{\isachardoublequote}}, and the list
   4.758 +  of mutual induction rules is called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}inducts{\isachardoublequote}}.%
   4.759 +\end{isamarkuptext}%
   4.760 +\isamarkuptrue%
   4.761 +%
   4.762 +\isamarkupsubsection{Monotonicity theorems%
   4.763 +}
   4.764 +\isamarkuptrue%
   4.765 +%
   4.766 +\begin{isamarkuptext}%
   4.767 +Each theory contains a default set of theorems that are used in
   4.768 +  monotonicity proofs.  New rules can be added to this set via the
   4.769 +  \mbox{\isa{mono}} attribute.  The HOL theory \isa{Inductive}
   4.770 +  shows how this is done.  In general, the following monotonicity
   4.771 +  theorems may be added:
   4.772 +
   4.773 +  \begin{itemize}
   4.774 +
   4.775 +  \item Theorems of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}}, for proving
   4.776 +  monotonicity of inductive definitions whose introduction rules have
   4.777 +  premises involving terms such as \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}}.
   4.778 +
   4.779 +  \item Monotonicity theorems for logical operators, which are of the
   4.780 +  general form \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isachardoublequote}}.  For example, in
   4.781 +  the case of the operator \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}, the corresponding theorem is
   4.782 +  \[
   4.783 +  \infer{\isa{{\isachardoublequote}P\isactrlsub {\isadigit{1}}\ {\isasymor}\ P\isactrlsub {\isadigit{2}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{1}}\ {\isasymor}\ Q\isactrlsub {\isadigit{2}}{\isachardoublequote}}}{\isa{{\isachardoublequote}P\isactrlsub {\isadigit{1}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \isa{{\isachardoublequote}P\isactrlsub {\isadigit{2}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{2}}{\isachardoublequote}}}
   4.784 +  \]
   4.785 +
   4.786 +  \item De Morgan style equations for reasoning about the ``polarity''
   4.787 +  of expressions, e.g.
   4.788 +  \[
   4.789 +  \isa{{\isachardoublequote}{\isasymnot}\ {\isasymnot}\ P\ {\isasymlongleftrightarrow}\ P{\isachardoublequote}} \qquad\qquad
   4.790 +  \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ {\isasymnot}\ Q{\isachardoublequote}}
   4.791 +  \]
   4.792 +
   4.793 +  \item Equations for reducing complex operators to more primitive
   4.794 +  ones whose monotonicity can easily be proved, e.g.
   4.795 +  \[
   4.796 +  \isa{{\isachardoublequote}{\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ Q{\isachardoublequote}} \qquad\qquad
   4.797 +  \isa{{\isachardoublequote}Ball\ A\ P\ {\isasymequiv}\ {\isasymforall}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}}
   4.798 +  \]
   4.799 +
   4.800 +  \end{itemize}
   4.801 +
   4.802 +  %FIXME: Example of an inductive definition%
   4.803 +\end{isamarkuptext}%
   4.804 +\isamarkuptrue%
   4.805 +%
   4.806 +\isamarkupsection{Arithmetic proof support%
   4.807 +}
   4.808 +\isamarkuptrue%
   4.809 +%
   4.810 +\begin{isamarkuptext}%
   4.811 +\begin{matharray}{rcl}
   4.812 +    \indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\
   4.813 +    \indexdef{HOL}{method}{arith-split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
   4.814 +  \end{matharray}
   4.815 +
   4.816 +  The \mbox{\isa{arith}} method decides linear arithmetic problems
   4.817 +  (on types \isa{nat}, \isa{int}, \isa{real}).  Any current
   4.818 +  facts are inserted into the goal before running the procedure.
   4.819 +
   4.820 +  The \mbox{\isa{arith{\isacharunderscore}split}} attribute declares case split rules
   4.821 +  to be expanded before the arithmetic procedure is invoked.
   4.822 +
   4.823 +  Note that a simpler (but faster) version of arithmetic reasoning is
   4.824 +  already performed by the Simplifier.%
   4.825 +\end{isamarkuptext}%
   4.826 +\isamarkuptrue%
   4.827 +%
   4.828 +\isamarkupsection{Cases and induction: emulating tactic scripts \label{sec:hol-induct-tac}%
   4.829 +}
   4.830 +\isamarkuptrue%
   4.831 +%
   4.832 +\begin{isamarkuptext}%
   4.833 +The following important tactical tools of Isabelle/HOL have been
   4.834 +  ported to Isar.  These should be never used in proper proof texts!
   4.835 +
   4.836 +  \begin{matharray}{rcl}
   4.837 +    \indexdef{HOL}{method}{case-tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   4.838 +    \indexdef{HOL}{method}{induct-tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   4.839 +    \indexdef{HOL}{method}{ind-cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   4.840 +    \indexdef{HOL}{command}{inductive-cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
   4.841 +  \end{matharray}
   4.842 +
   4.843 +  \begin{rail}
   4.844 +    'case\_tac' goalspec? term rule?
   4.845 +    ;
   4.846 +    'induct\_tac' goalspec? (insts * 'and') rule?
   4.847 +    ;
   4.848 +    'ind\_cases' (prop +) ('for' (name +)) ?
   4.849 +    ;
   4.850 +    'inductive\_cases' (thmdecl? (prop +) + 'and')
   4.851 +    ;
   4.852 +
   4.853 +    rule: ('rule' ':' thmref)
   4.854 +    ;
   4.855 +  \end{rail}
   4.856 +
   4.857 +  \begin{descr}
   4.858 +
   4.859 +  \item [\mbox{\isa{case{\isacharunderscore}tac}} and \mbox{\isa{induct{\isacharunderscore}tac}}]
   4.860 +  admit to reason about inductive datatypes only (unless an
   4.861 +  alternative rule is given explicitly).  Furthermore, \mbox{\isa{case{\isacharunderscore}tac}} does a classical case split on booleans; \mbox{\isa{induct{\isacharunderscore}tac}} allows only variables to be given as instantiation.
   4.862 +  These tactic emulations feature both goal addressing and dynamic
   4.863 +  instantiation.  Note that named rule cases are \emph{not} provided
   4.864 +  as would be by the proper \mbox{\isa{induct}} and \mbox{\isa{cases}} proof
   4.865 +  methods (see \secref{sec:cases-induct}).
   4.866 +  
   4.867 +  \item [\mbox{\isa{ind{\isacharunderscore}cases}} and \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}] provide an interface to the internal
   4.868 +  \texttt{mk_cases} operation.  Rules are simplified in an
   4.869 +  unrestricted forward manner.
   4.870 +
   4.871 +  While \mbox{\isa{ind{\isacharunderscore}cases}} is a proof method to apply the
   4.872 +  result immediately as elimination rules, \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} provides case split theorems at the theory level
   4.873 +  for later use.  The \mbox{\isa{\isakeyword{for}}} argument of the \mbox{\isa{ind{\isacharunderscore}cases}} method allows to specify a list of variables that should
   4.874 +  be generalized before applying the resulting rule.
   4.875 +
   4.876 +  \end{descr}%
   4.877 +\end{isamarkuptext}%
   4.878 +\isamarkuptrue%
   4.879 +%
   4.880 +\isamarkupsection{Executable code%
   4.881 +}
   4.882 +\isamarkuptrue%
   4.883 +%
   4.884 +\begin{isamarkuptext}%
   4.885 +Isabelle/Pure provides two generic frameworks to support code
   4.886 +  generation from executable specifications.  Isabelle/HOL
   4.887 +  instantiates these mechanisms in a way that is amenable to end-user
   4.888 +  applications.
   4.889 +
   4.890 +  One framework generates code from both functional and relational
   4.891 +  programs to SML.  See \cite{isabelle-HOL} for further information
   4.892 +  (this actually covers the new-style theory format as well).
   4.893 +
   4.894 +  \begin{matharray}{rcl}
   4.895 +    \indexdef{HOL}{command}{value}\mbox{\isa{\isacommand{value}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   4.896 +    \indexdef{HOL}{command}{code-module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\
   4.897 +    \indexdef{HOL}{command}{code-library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\
   4.898 +    \indexdef{HOL}{command}{consts-code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
   4.899 +    \indexdef{HOL}{command}{types-code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\  
   4.900 +    \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\
   4.901 +  \end{matharray}
   4.902 +
   4.903 +  \begin{rail}
   4.904 +  'value' term
   4.905 +  ;
   4.906 +
   4.907 +  ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
   4.908 +    ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
   4.909 +    'contains' ( ( name '=' term ) + | term + )
   4.910 +  ;
   4.911 +
   4.912 +  modespec: '(' ( name * ) ')'
   4.913 +  ;
   4.914 +
   4.915 +  'consts\_code' (codespec +)
   4.916 +  ;
   4.917 +
   4.918 +  codespec: const template attachment ?
   4.919 +  ;
   4.920 +
   4.921 +  'types\_code' (tycodespec +)
   4.922 +  ;
   4.923 +
   4.924 +  tycodespec: name template attachment ?
   4.925 +  ;
   4.926 +
   4.927 +  const: term
   4.928 +  ;
   4.929 +
   4.930 +  template: '(' string ')'
   4.931 +  ;
   4.932 +
   4.933 +  attachment: 'attach' modespec ? verblbrace text verbrbrace
   4.934 +  ;
   4.935 +
   4.936 +  'code' (name)?
   4.937 +  ;
   4.938 +  \end{rail}
   4.939 +
   4.940 +  \begin{descr}
   4.941 +
   4.942 +  \item [\mbox{\isa{\isacommand{value}}}~\isa{t}] evaluates and prints a
   4.943 +  term using the code generator.
   4.944 +
   4.945 +  \end{descr}
   4.946 +
   4.947 +  \medskip The other framework generates code from functional programs
   4.948 +  (including overloading using type classes) to SML \cite{SML}, OCaml
   4.949 +  \cite{OCaml} and Haskell \cite{haskell-revised-report}.
   4.950 +  Conceptually, code generation is split up in three steps:
   4.951 +  \emph{selection} of code theorems, \emph{translation} into an
   4.952 +  abstract executable view and \emph{serialization} to a specific
   4.953 +  \emph{target language}.  See \cite{isabelle-codegen} for an
   4.954 +  introduction on how to use it.
   4.955 +
   4.956 +  \begin{matharray}{rcl}
   4.957 +    \indexdef{HOL}{command}{export-code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   4.958 +    \indexdef{HOL}{command}{code-thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   4.959 +    \indexdef{HOL}{command}{code-deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   4.960 +    \indexdef{HOL}{command}{code-datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
   4.961 +    \indexdef{HOL}{command}{code-const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\
   4.962 +    \indexdef{HOL}{command}{code-type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\
   4.963 +    \indexdef{HOL}{command}{code-class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\
   4.964 +    \indexdef{HOL}{command}{code-instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\
   4.965 +    \indexdef{HOL}{command}{code-monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\
   4.966 +    \indexdef{HOL}{command}{code-reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\
   4.967 +    \indexdef{HOL}{command}{code-include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\
   4.968 +    \indexdef{HOL}{command}{code-modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\
   4.969 +    \indexdef{HOL}{command}{code-exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\
   4.970 +    \indexdef{HOL}{command}{print-codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   4.971 +    \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\
   4.972 +  \end{matharray}
   4.973 +
   4.974 +  \begin{rail}
   4.975 +    'export\_code' ( constexpr + ) ? \\
   4.976 +      ( ( 'in' target ( 'module\_name' string ) ? \\
   4.977 +        ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
   4.978 +    ;
   4.979 +
   4.980 +    'code\_thms' ( constexpr + ) ?
   4.981 +    ;
   4.982 +
   4.983 +    'code\_deps' ( constexpr + ) ?
   4.984 +    ;
   4.985 +
   4.986 +    const: term
   4.987 +    ;
   4.988 +
   4.989 +    constexpr: ( const | 'name.*' | '*' )
   4.990 +    ;
   4.991 +
   4.992 +    typeconstructor: nameref
   4.993 +    ;
   4.994 +
   4.995 +    class: nameref
   4.996 +    ;
   4.997 +
   4.998 +    target: 'OCaml' | 'SML' | 'Haskell'
   4.999 +    ;
  4.1000 +
  4.1001 +    'code\_datatype' const +
  4.1002 +    ;
  4.1003 +
  4.1004 +    'code\_const' (const + 'and') \\
  4.1005 +      ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  4.1006 +    ;
  4.1007 +
  4.1008 +    'code\_type' (typeconstructor + 'and') \\
  4.1009 +      ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  4.1010 +    ;
  4.1011 +
  4.1012 +    'code\_class' (class + 'and') \\
  4.1013 +      ( ( '(' target \\
  4.1014 +        ( ( string ('where' \\
  4.1015 +          ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
  4.1016 +    ;
  4.1017 +
  4.1018 +    'code\_instance' (( typeconstructor '::' class ) + 'and') \\
  4.1019 +      ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
  4.1020 +    ;
  4.1021 +
  4.1022 +    'code\_monad' const const target
  4.1023 +    ;
  4.1024 +
  4.1025 +    'code\_reserved' target ( string + )
  4.1026 +    ;
  4.1027 +
  4.1028 +    'code\_include' target ( string ( string | '-') )
  4.1029 +    ;
  4.1030 +
  4.1031 +    'code\_modulename' target ( ( string string ) + )
  4.1032 +    ;
  4.1033 +
  4.1034 +    'code\_exception' ( const + )
  4.1035 +    ;
  4.1036 +
  4.1037 +    syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
  4.1038 +    ;
  4.1039 +
  4.1040 +    'code' ('func' | 'inline') ( 'del' )?
  4.1041 +    ;
  4.1042 +  \end{rail}
  4.1043 +
  4.1044 +  \begin{descr}
  4.1045 +
  4.1046 +  \item [\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}] is the canonical interface
  4.1047 +  for generating and serializing code: for a given list of constants,
  4.1048 +  code is generated for the specified target languages.  Abstract code
  4.1049 +  is cached incrementally.  If no constant is given, the currently
  4.1050 +  cached code is serialized.  If no serialization instruction is
  4.1051 +  given, only abstract code is cached.
  4.1052 +
  4.1053 +  Constants may be specified by giving them literally, referring to
  4.1054 +  all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
  4.1055 +  available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.
  4.1056 +
  4.1057 +  By default, for each involved theory one corresponding name space
  4.1058 +  module is generated.  Alternativly, a module name may be specified
  4.1059 +  after the \mbox{\isa{\isakeyword{module{\isacharunderscore}name}}} keyword; then \emph{all} code is
  4.1060 +  placed in this module.
  4.1061 +
  4.1062 +  For \emph{SML} and \emph{OCaml}, the file specification refers to a
  4.1063 +  single file; for \emph{Haskell}, it refers to a whole directory,
  4.1064 +  where code is generated in multiple files reflecting the module
  4.1065 +  hierarchy.  The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard
  4.1066 +  output.  For \emph{SML}, omitting the file specification compiles
  4.1067 +  code internally in the context of the current ML session.
  4.1068 +
  4.1069 +  Serializers take an optional list of arguments in parentheses.  For
  4.1070 +  \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
  4.1071 +  declaration.
  4.1072 +
  4.1073 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}] prints a list of theorems
  4.1074 +  representing the corresponding program containing all given
  4.1075 +  constants; if no constants are given, the currently cached code
  4.1076 +  theorems are printed.
  4.1077 +
  4.1078 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}] visualizes dependencies of
  4.1079 +  theorems representing the corresponding program containing all given
  4.1080 +  constants; if no constants are given, the currently cached code
  4.1081 +  theorems are visualized.
  4.1082 +
  4.1083 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}] specifies a constructor set
  4.1084 +  for a logical type.
  4.1085 +
  4.1086 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}] associates a list of constants
  4.1087 +  with target-specific serializations; omitting a serialization
  4.1088 +  deletes an existing serialization.
  4.1089 +
  4.1090 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}] associates a list of type
  4.1091 +  constructors with target-specific serializations; omitting a
  4.1092 +  serialization deletes an existing serialization.
  4.1093 +
  4.1094 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}] associates a list of classes
  4.1095 +  with target-specific class names; in addition, constants associated
  4.1096 +  with this class may be given target-specific names used for instance
  4.1097 +  declarations; omitting a serialization deletes an existing
  4.1098 +  serialization.  This applies only to \emph{Haskell}.
  4.1099 +
  4.1100 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}] declares a list of type
  4.1101 +  constructor / class instance relations as ``already present'' for a
  4.1102 +  given target.  Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
  4.1103 +  ``already present'' declaration.  This applies only to
  4.1104 +  \emph{Haskell}.
  4.1105 +
  4.1106 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}] provides an auxiliary
  4.1107 +  mechanism to generate monadic code.
  4.1108 +
  4.1109 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}] declares a list of names as
  4.1110 +  reserved for a given target, preventing it to be shadowed by any
  4.1111 +  generated code.
  4.1112 +
  4.1113 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}] adds arbitrary named content
  4.1114 +  (``include'') to generated code.  A as last argument ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}''
  4.1115 +  will remove an already added ``include''.
  4.1116 +
  4.1117 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}] declares aliasings from
  4.1118 +  one module name onto another.
  4.1119 +
  4.1120 +  \item [\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}] declares constants which
  4.1121 +  are not required to have a definition by a defining equations; these
  4.1122 +  are mapped on exceptions instead.
  4.1123 +
  4.1124 +  \item [\mbox{\isa{code}}~\isa{func}] explicitly selects (or
  4.1125 +  with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
  4.1126 +  code generation.  Usually packages introducing defining equations
  4.1127 +  provide a resonable default setup for selection.
  4.1128 +
  4.1129 +  \item [\mbox{\isa{code}}\isa{inline}] declares (or with
  4.1130 +  option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are
  4.1131 +  applied as rewrite rules to any defining equation during
  4.1132 +  preprocessing.
  4.1133 +
  4.1134 +  \item [\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}] gives an overview on
  4.1135 +  selected defining equations, code generator datatypes and
  4.1136 +  preprocessor setup.
  4.1137 +
  4.1138 +  \end{descr}%
  4.1139 +\end{isamarkuptext}%
  4.1140 +\isamarkuptrue%
  4.1141 +%
  4.1142 +\isadelimtheory
  4.1143 +%
  4.1144 +\endisadelimtheory
  4.1145 +%
  4.1146 +\isatagtheory
  4.1147  \isacommand{end}\isamarkupfalse%
  4.1148  %
  4.1149  \endisatagtheory
  4.1150  {\isafoldtheory}%
  4.1151  %
  4.1152  \isadelimtheory
  4.1153 -\isanewline
  4.1154  %
  4.1155  \endisadelimtheory
  4.1156 +\isanewline
  4.1157 +\isanewline
  4.1158  \end{isabellebody}%
  4.1159  %%% Local Variables:
  4.1160  %%% mode: latex

     5.1 --- a/doc-src/IsarRef/Thy/document/session.tex	Thu May 08 12:27:19 2008 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/document/session.tex	Thu May 08 12:29:18 2008 +0200
     5.3 @@ -1,4 +1,16 @@
     5.4 -\input{ZF_Specific.tex}
     5.5 +\input{intro.tex}
     5.6 +
     5.7 +\input{syntax.tex}
     5.8 +
     5.9 +\input{pure.tex}
    5.10 +
    5.11 +\input{Generic.tex}
    5.12 +
    5.13 +\input{HOL_Specific.tex}
    5.14 +
    5.15 +\input{Quick_Reference.tex}
    5.16 +
    5.17 +\input{ML_Tactic.tex}
    5.18  
    5.19  %%% Local Variables:
    5.20  %%% mode: latex

     6.1 --- a/doc-src/IsarRef/isar-ref.tex	Thu May 08 12:27:19 2008 +0200
     6.2 +++ b/doc-src/IsarRef/isar-ref.tex	Thu May 08 12:29:18 2008 +0200
     6.3 @@ -85,7 +85,6 @@
     6.4  \input{Thy/document/HOL_Specific.tex}
     6.5  \input{Thy/document/HOLCF_Specific.tex}
     6.6  \input{Thy/document/ZF_Specific.tex}
     6.7 -\input{logics.tex}
     6.8  
     6.9  \appendix
    6.10  \input{Thy/document/Quick_Reference.tex}

     7.1 --- a/doc-src/IsarRef/logics.tex	Thu May 08 12:27:19 2008 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,1055 +0,0 @@
     7.4 -
     7.5 -\chapter{Object-logic specific elements}\label{ch:logics}
     7.6 -
     7.7 -\section{HOL}
     7.8 -
     7.9 -\subsection{Primitive types}\label{sec:hol-typedef}
    7.10 -
    7.11 -\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
    7.12 -\begin{matharray}{rcl}
    7.13 -  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
    7.14 -  \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
    7.15 -\end{matharray}
    7.16 -
    7.17 -\begin{rail}
    7.18 -  'typedecl' typespec infix?
    7.19 -  ;
    7.20 -  'typedef' altname? abstype '=' repset
    7.21 -  ;
    7.22 -
    7.23 -  altname: '(' (name | 'open' | 'open' name) ')'
    7.24 -  ;
    7.25 -  abstype: typespec infix?
    7.26 -  ;
    7.27 -  repset: term ('morphisms' name name)?
    7.28 -  ;
    7.29 -\end{rail}
    7.30 -
    7.31 -\begin{descr}
    7.32 -  
    7.33 -\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
    7.34 -  $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
    7.35 -  also declares type arity $t :: (type, \dots, type) type$, making $t$ an
    7.36 -  actual HOL type constructor.
    7.37 -  
    7.38 -\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
    7.39 -  non-emptiness of the set $A$.  After finishing the proof, the theory will be
    7.40 -  augmented by a Gordon/HOL-style type definition, which establishes a
    7.41 -  bijection between the representing set $A$ and the new type $t$.
    7.42 -  
    7.43 -  Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term
    7.44 -  constant) of the same name (an alternative base name may be given in
    7.45 -  parentheses).  The injection from type to set is called $Rep_t$, its inverse
    7.46 -  $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$
    7.47 -  declaration).
    7.48 -  
    7.49 -  Theorems $Rep_t$, $Rep_t_inverse$, and $Abs_t_inverse$ provide the most
    7.50 -  basic characterization as a corresponding injection/surjection pair (in both
    7.51 -  directions).  Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly
    7.52 -  more convenient view on the injectivity part, suitable for automated proof
    7.53 -  tools (e.g.\ in $simp$ or $iff$ declarations).  Rules
    7.54 -  $Rep_t_cases/Rep_t_induct$, and $Abs_t_cases/Abs_t_induct$ provide
    7.55 -  alternative views on surjectivity; these are already declared as set or type
    7.56 -  rules for the generic $cases$ and $induct$ methods.
    7.57 -  
    7.58 -  An alternative name may be specified in parentheses; the default is to use
    7.59 -  $t$ as indicated before.  The $open$ declaration suppresses a separate
    7.60 -  constant definition for the representing set.
    7.61 -\end{descr}
    7.62 -
    7.63 -Note that raw type declarations are rarely used in practice; the main
    7.64 -application is with experimental (or even axiomatic!) theory fragments.
    7.65 -Instead of primitive HOL type definitions, user-level theories usually refer
    7.66 -to higher-level packages such as $\isarkeyword{record}$ (see
    7.67 -\S\ref{sec:hol-record}) or $\isarkeyword{datatype}$ (see
    7.68 -\S\ref{sec:hol-datatype}).
    7.69 -
    7.70 -
    7.71 -\subsection{Adhoc tuples}
    7.72 -
    7.73 -\indexisarattof{HOL}{split-format}
    7.74 -\begin{matharray}{rcl}
    7.75 -  split_format^* & : & \isaratt \\
    7.76 -\end{matharray}
    7.77 -
    7.78 -\railalias{splitformat}{split\_format}
    7.79 -\railterm{splitformat}
    7.80 -
    7.81 -\begin{rail}
    7.82 -  splitformat (((name *) + 'and') | ('(' 'complete' ')'))
    7.83 -  ;
    7.84 -\end{rail}
    7.85 -
    7.86 -\begin{descr}
    7.87 -  
    7.88 -\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
    7.89 -  tuple types into canonical form as specified by the arguments given; $\vec
    7.90 -  p@i$ refers to occurrences in premise $i$ of the rule.  The ``$(complete)$''
    7.91 -  option causes \emph{all} arguments in function applications to be
    7.92 -  represented canonically according to their tuple type structure.
    7.93 -
    7.94 -  Note that these operations tend to invent funny names for new local
    7.95 -  parameters to be introduced.
    7.96 -
    7.97 -\end{descr}
    7.98 -
    7.99 -
   7.100 -\subsection{Records}\label{sec:hol-record}
   7.101 -
   7.102 -In principle, records merely generalize the concept of tuples, where
   7.103 -components may be addressed by labels instead of just position.  The logical
   7.104 -infrastructure of records in Isabelle/HOL is slightly more advanced, though,
   7.105 -supporting truly extensible record schemes.  This admits operations that are
   7.106 -polymorphic with respect to record extension, yielding ``object-oriented''
   7.107 -effects like (single) inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for
   7.108 -more details on object-oriented verification and record subtyping in HOL.
   7.109 -
   7.110 -
   7.111 -\subsubsection{Basic concepts}
   7.112 -
   7.113 -Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the
   7.114 -level of terms and types.  The notation is as follows:
   7.115 -
   7.116 -\begin{center}
   7.117 -\begin{tabular}{l|l|l}
   7.118 -  & record terms & record types \\ \hline
   7.119 -  fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
   7.120 -  schematic & $\record{x = a\fs y = b\fs \more = m}$ &
   7.121 -    $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
   7.122 -\end{tabular}
   7.123 -\end{center}
   7.124 -
   7.125 -\noindent The ASCII representation of $\record{x = a}$ is \texttt{(| x = a |)}.
   7.126 -
   7.127 -A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
   7.128 -$y$ of value $b$.  The corresponding type is $\record{x \ty A\fs y \ty B}$,
   7.129 -assuming that $a \ty A$ and $b \ty B$.
   7.130 -
   7.131 -A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
   7.132 -$x$ and $y$ as before, but also possibly further fields as indicated by the
   7.133 -``$\more$'' notation (which is actually part of the syntax).  The improper
   7.134 -field ``$\more$'' of a record scheme is called the \emph{more part}.
   7.135 -Logically it is just a free variable, which is occasionally referred to as
   7.136 -``row variable'' in the literature.  The more part of a record scheme may be
   7.137 -instantiated by zero or more further components.  For example, the previous
   7.138 -scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more =
   7.139 -  m'}$, where $m'$ refers to a different more part.  Fixed records are special
   7.140 -instances of record schemes, where ``$\more$'' is properly terminated by the
   7.141 -$() :: unit$ element.  Actually, $\record{x = a\fs y = b}$ is just an
   7.142 -abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
   7.143 -
   7.144 -\medskip
   7.145 -
   7.146 -Two key observations make extensible records in a simply typed language like
   7.147 -HOL feasible:
   7.148 -\begin{enumerate}
   7.149 -\item the more part is internalized, as a free term or type variable,
   7.150 -\item field names are externalized, they cannot be accessed within the logic
   7.151 -  as first-class values.
   7.152 -\end{enumerate}
   7.153 -
   7.154 -\medskip
   7.155 -
   7.156 -In Isabelle/HOL record types have to be defined explicitly, fixing their field
   7.157 -names and types, and their (optional) parent record.  Afterwards, records may
   7.158 -be formed using above syntax, while obeying the canonical order of fields as
   7.159 -given by their declaration.  The record package provides several standard
   7.160 -operations like selectors and updates.  The common setup for various generic
   7.161 -proof tools enable succinct reasoning patterns.  See also the Isabelle/HOL
   7.162 -tutorial \cite{isabelle-hol-book} for further instructions on using records in
   7.163 -practice.
   7.164 -
   7.165 -
   7.166 -\subsubsection{Record specifications}
   7.167 -
   7.168 -\indexisarcmdof{HOL}{record}
   7.169 -\begin{matharray}{rcl}
   7.170 -  \isarcmd{record} & : & \isartrans{theory}{theory} \\
   7.171 -\end{matharray}
   7.172 -
   7.173 -\begin{rail}
   7.174 -  'record' typespec '=' (type '+')? (constdecl +)
   7.175 -  ;
   7.176 -\end{rail}
   7.177 -
   7.178 -\begin{descr}
   7.179 -\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
   7.180 -  defines extensible record type $(\vec\alpha)t$, derived from the optional
   7.181 -  parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
   7.182 -
   7.183 -  The type variables of $\tau$ and $\vec\sigma$ need to be covered by the
   7.184 -  (distinct) parameters $\vec\alpha$.  Type constructor $t$ has to be new,
   7.185 -  while $\tau$ needs to specify an instance of an existing record type.  At
   7.186 -  least one new field $\vec c$ has to be specified.  Basically, field names
   7.187 -  need to belong to a unique record.  This is not a real restriction in
   7.188 -  practice, since fields are qualified by the record name internally.
   7.189 -
   7.190 -  The parent record specification $\tau$ is optional; if omitted $t$ becomes a
   7.191 -  root record.  The hierarchy of all records declared within a theory context
   7.192 -  forms a forest structure, i.e.\ a set of trees starting with a root record
   7.193 -  each.  There is no way to merge multiple parent records!
   7.194 -
   7.195 -  For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the
   7.196 -  fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is
   7.197 -  $(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c
   7.198 -    \ty \vec\sigma\fs \more \ty \zeta}$.
   7.199 -
   7.200 -\end{descr}
   7.201 -
   7.202 -\subsubsection{Record operations}
   7.203 -
   7.204 -Any record definition of the form presented above produces certain standard
   7.205 -operations.  Selectors and updates are provided for any field, including the
   7.206 -improper one ``$more$''.  There are also cumulative record constructor
   7.207 -functions.  To simplify the presentation below, we assume for now that
   7.208 -$(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$.
   7.209 -
   7.210 -\medskip \textbf{Selectors} and \textbf{updates} are available for any field
   7.211 -(including ``$more$''):
   7.212 -\begin{matharray}{lll}
   7.213 -  c@i & \ty & \record{\vec c \ty \vec \sigma, \more \ty \zeta} \To \sigma@i \\
   7.214 -  c@i_update & \ty & \sigma@i \To \record{\vec c \ty \vec\sigma, \more \ty \zeta} \To
   7.215 -    \record{\vec c \ty \vec\sigma, \more \ty \zeta}
   7.216 -\end{matharray}
   7.217 -
   7.218 -There is special syntax for application of updates: $r \, \record{x \asn a}$
   7.219 -abbreviates term $x_update \, a \, r$.  Further notation for repeated updates
   7.220 -is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z
   7.221 -  \asn c}$ may be written $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$.
   7.222 -Note that because of postfix notation the order of fields shown here is
   7.223 -reverse than in the actual term.  Since repeated updates are just function
   7.224 -applications, fields may be freely permuted in $\record{x \asn a\fs y \asn
   7.225 -  b\fs z \asn c}$, as far as logical equality is concerned.  Thus
   7.226 -commutativity of independent updates can be proven within the logic for any
   7.227 -two fields, but not as a general theorem.
   7.228 -
   7.229 -\medskip The \textbf{make} operation provides a cumulative record constructor
   7.230 -function:
   7.231 -\begin{matharray}{lll}
   7.232 -  t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
   7.233 -\end{matharray}
   7.234 -
   7.235 -\medskip We now reconsider the case of non-root records, which are derived of
   7.236 -some parent.  In general, the latter may depend on another parent as well,
   7.237 -resulting in a list of \emph{ancestor records}.  Appending the lists of fields
   7.238 -of all ancestors results in a certain field prefix.  The record package
   7.239 -automatically takes care of this by lifting operations over this context of
   7.240 -ancestor fields.  Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec
   7.241 -b \ty \vec\rho$, the above record operations will get the following types:
   7.242 -\begin{matharray}{lll}
   7.243 -  c@i & \ty & \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty
   7.244 -    \zeta} \To \sigma@i \\
   7.245 -  c@i_update & \ty & \sigma@i \To
   7.246 -    \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To
   7.247 -    \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
   7.248 -  t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To
   7.249 -    \record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\
   7.250 -\end{matharray}
   7.251 -\noindent
   7.252 -
   7.253 -\medskip Some further operations address the extension aspect of a derived
   7.254 -record scheme specifically: $fields$ produces a record fragment consisting of
   7.255 -exactly the new fields introduced here (the result may serve as a more part
   7.256 -elsewhere); $extend$ takes a fixed record and adds a given more part;
   7.257 -$truncate$ restricts a record scheme to a fixed record.
   7.258 -
   7.259 -\begin{matharray}{lll}
   7.260 -  t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
   7.261 -  t{\dtt}extend & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \To
   7.262 -    \zeta \To \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
   7.263 -  t{\dtt}truncate & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To
   7.264 -    \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\
   7.265 -\end{matharray}
   7.266 -
   7.267 -\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records.
   7.268 -
   7.269 -
   7.270 -\subsubsection{Derived rules and proof tools}
   7.271 -
   7.272 -The record package proves several results internally, declaring these facts to
   7.273 -appropriate proof tools.  This enables users to reason about record structures
   7.274 -quite conveniently.  Assume that $t$ is a record type as specified above.
   7.275 -
   7.276 -\begin{enumerate}
   7.277 -  
   7.278 -\item Standard conversions for selectors or updates applied to record
   7.279 -  constructor terms are made part of the default Simplifier context; thus
   7.280 -  proofs by reduction of basic operations merely require the $simp$ method
   7.281 -  without further arguments.  These rules are available as $t{\dtt}simps$,
   7.282 -  too.
   7.283 -  
   7.284 -\item Selectors applied to updated records are automatically reduced by an
   7.285 -  internal simplification procedure, which is also part of the standard
   7.286 -  Simplifier setup.
   7.287 -
   7.288 -\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
   7.289 -  \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$
   7.290 -  rules.  These rules are available as $t{\dtt}iffs$.
   7.291 -
   7.292 -\item The introduction rule for record equality analogous to $x~r = x~r' \Imp
   7.293 -  y~r = y~r' \Imp \dots \Imp r = r'$ is declared to the Simplifier, and as the
   7.294 -  basic rule context as ``$intro?$''.  The rule is called $t{\dtt}equality$.
   7.295 -
   7.296 -\item Representations of arbitrary record expressions as canonical constructor
   7.297 -  terms are provided both in $cases$ and $induct$ format (cf.\ the generic
   7.298 -  proof methods of the same name, \S\ref{sec:cases-induct}).  Several
   7.299 -  variations are available, for fixed records, record schemes, more parts etc.
   7.300 -  
   7.301 -  The generic proof methods are sufficiently smart to pick the most sensible
   7.302 -  rule according to the type of the indicated record expression: users just
   7.303 -  need to apply something like ``$(cases~r)$'' to a certain proof problem.
   7.304 -
   7.305 -\item The derived record operations $t{\dtt}make$, $t{\dtt}fields$,
   7.306 -  $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but
   7.307 -  usually need to be expanded by hand, using the collective fact
   7.308 -  $t{\dtt}defs$.
   7.309 -
   7.310 -\end{enumerate}
   7.311 -
   7.312 -
   7.313 -\subsection{Datatypes}\label{sec:hol-datatype}
   7.314 -
   7.315 -\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
   7.316 -\begin{matharray}{rcl}
   7.317 -  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
   7.318 -  \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
   7.319 -\end{matharray}
   7.320 -
   7.321 -\railalias{repdatatype}{rep\_datatype}
   7.322 -\railterm{repdatatype}
   7.323 -
   7.324 -\begin{rail}
   7.325 -  'datatype' (dtspec + 'and')
   7.326 -  ;
   7.327 -  repdatatype (name *) dtrules
   7.328 -  ;
   7.329 -
   7.330 -  dtspec: parname? typespec infix? '=' (cons + '|')
   7.331 -  ;
   7.332 -  cons: name (type *) mixfix?
   7.333 -  ;
   7.334 -  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
   7.335 -\end{rail}
   7.336 -
   7.337 -\begin{descr}
   7.338 -\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
   7.339 -\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
   7.340 -  ones, generating the standard infrastructure of derived concepts (primitive
   7.341 -  recursion etc.).
   7.342 -\end{descr}
   7.343 -
   7.344 -The induction and exhaustion theorems generated provide case names according
   7.345 -to the constructors involved, while parameters are named after the types (see
   7.346 -also \S\ref{sec:cases-induct}).
   7.347 -
   7.348 -See \cite{isabelle-HOL} for more details on datatypes, but beware of the
   7.349 -old-style theory syntax being used there!  Apart from proper proof methods for
   7.350 -case-analysis and induction, there are also emulations of ML tactics
   7.351 -\texttt{case_tac} and \texttt{induct_tac} available, see
   7.352 -\S\ref{sec:hol-induct-tac}; these admit to refer directly to the internal
   7.353 -structure of subgoals (including internally bound parameters).
   7.354 -
   7.355 -
   7.356 -\subsection{Recursive functions}\label{sec:recursion}
   7.357 -
   7.358 -\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{fun}\indexisarcmdof{HOL}{function}\indexisarcmdof{HOL}{termination}
   7.359 -
   7.360 -\begin{matharray}{rcl}
   7.361 -  \isarcmd{primrec} & : & \isarkeep{local{\dsh}theory} \\
   7.362 -  \isarcmd{fun} & : & \isarkeep{local{\dsh}theory} \\
   7.363 -  \isarcmd{function} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
   7.364 -  \isarcmd{termination} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
   7.365 -\end{matharray}
   7.366 -
   7.367 -\railalias{funopts}{function\_opts}
   7.368 -
   7.369 -\begin{rail}
   7.370 -  'primrec' target? fixes 'where' equations
   7.371 -  ;
   7.372 -  equations: (thmdecl? prop + '|')
   7.373 -  ;
   7.374 -  ('fun' | 'function') (funopts)? fixes 'where' clauses
   7.375 -  ;
   7.376 -  clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
   7.377 -  ;
   7.378 -  funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' |
   7.379 -  'default' term) + ',') ')'
   7.380 -  ;
   7.381 -  'termination' ( term )?
   7.382 -\end{rail}
   7.383 -
   7.384 -\begin{descr}
   7.385 -
   7.386 -\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
   7.387 -  datatypes, see also \cite{isabelle-HOL}.
   7.388 -
   7.389 -\item [$\isarkeyword{function}$] defines functions by general
   7.390 -  wellfounded recursion. A detailed description with examples can be
   7.391 -  found in \cite{isabelle-function}. The function is specified by a
   7.392 -  set of (possibly conditional) recursive equations with arbitrary
   7.393 -  pattern matching. The command generates proof obligations for the
   7.394 -  completeness and the compatibility of patterns.
   7.395 -
   7.396 -  The defined function is considered partial, and the resulting
   7.397 -  simplification rules (named $f.psimps$) and induction rule (named
   7.398 -  $f.pinduct$) are guarded by a generated domain predicate $f_dom$. 
   7.399 -  The $\isarkeyword{termination}$ command can then be used to establish
   7.400 -  that the function is total.
   7.401 -
   7.402 -\item [$\isarkeyword{fun}$] is a shorthand notation for
   7.403 -  $\isarkeyword{function}~(\textit{sequential})$, followed by automated
   7.404 -  proof attemts regarding pattern matching and termination. For
   7.405 -  details, see \cite{isabelle-function}.
   7.406 -
   7.407 -\item [$\isarkeyword{termination}$~f] commences a termination proof
   7.408 -  for the previously defined function $f$. If no name is given, it
   7.409 -  refers to the most recent function definition. After the proof is
   7.410 -  closed, the recursive equations and the induction principle is established.
   7.411 -\end{descr}
   7.412 -
   7.413 -Recursive definitions introduced by both the $\isarkeyword{primrec}$
   7.414 -and the $\isarkeyword{function}$ command accommodate reasoning by
   7.415 -induction (cf.\ \S\ref{sec:cases-induct}): rule $c\mathord{.}induct$
   7.416 -(where $c$ is the name of the function definition) refers to a
   7.417 -specific induction rule, with parameters named according to the
   7.418 -user-specified equations.  Case names of $\isarkeyword{primrec}$ are
   7.419 -that of the datatypes involved, while those of
   7.420 -$\isarkeyword{function}$ are numbered (starting from $1$).
   7.421 -
   7.422 -The equations provided by these packages may be referred later as theorem list
   7.423 -$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined.
   7.424 -Individual equations may be named explicitly as well.
   7.425 -
   7.426 -The $\isarkeyword{function}$ command accepts the following options:
   7.427 -
   7.428 -\begin{descr}
   7.429 -\item [\emph{sequential}] enables a preprocessor which disambiguates
   7.430 -  overlapping patterns by making them mutually disjoint. Earlier
   7.431 -  equations take precedence over later ones. This allows to give the
   7.432 -  specification in a format very similar to functional programming.
   7.433 -  Note that the resulting simplification and induction rules
   7.434 -  correspond to the transformed specification, not the one given
   7.435 -  originally. This usually means that each equation given by the user
   7.436 -  may result in several theroems.
   7.437 -  Also note that this automatic transformation only works
   7.438 -  for ML-style datatype patterns.
   7.439 -
   7.440 -
   7.441 -\item [\emph{in name}] gives the target for the definition.
   7.442 -
   7.443 -\item [\emph{domintros}] enables the automated generation of
   7.444 -  introduction rules for the domain predicate. While mostly not
   7.445 -  needed, they can be helpful in some proofs about partial functions.
   7.446 -
   7.447 -\item [\emph{tailrec}] generates the unconstrained recursive equations
   7.448 -  even without a termination proof, provided that the function is
   7.449 -  tail-recursive. This currently only works 
   7.450 -
   7.451 -\item [\emph{default d}] allows to specify a default value for a
   7.452 -  (partial) function, which will ensure that $f(x)=d(x)$ whenever $x
   7.453 -  \notin \textit{f\_dom}$. This feature is experimental.
   7.454 -\end{descr}
   7.455 -
   7.456 -\subsubsection{Proof methods related to recursive definitions}
   7.457 -
   7.458 -\indexisarmethof{HOL}{pat-completeness}
   7.459 -\indexisarmethof{HOL}{relation}
   7.460 -\indexisarmethof{HOL}{lexicographic-order}
   7.461 -
   7.462 -\begin{matharray}{rcl}
   7.463 -  pat\_completeness & : & \isarmeth \\
   7.464 -  relation & : & \isarmeth \\
   7.465 -  lexicographic\_order & : & \isarmeth \\
   7.466 -\end{matharray}
   7.467 -
   7.468 -\begin{rail}
   7.469 -  'pat\_completeness'
   7.470 -  ;
   7.471 -  'relation' term
   7.472 -  ;
   7.473 -  'lexicographic\_order' clasimpmod
   7.474 -\end{rail}
   7.475 -
   7.476 -\begin{descr}
   7.477 -\item [\emph{pat\_completeness}] Specialized method to solve goals
   7.478 -  regarding the completeness of pattern matching, as required by the
   7.479 -  $\isarkeyword{function}$ package (cf.~\cite{isabelle-function}).
   7.480 -
   7.481 -\item [\emph{relation R}] Introduces a termination proof using the
   7.482 -  relation $R$. The resulting proof state will contain goals
   7.483 -  expressing that $R$ is wellfounded, and that the arguments
   7.484 -  of recursive calls decrease with respect to $R$. Usually, this
   7.485 -  method is used as the initial proof step of manual termination
   7.486 -  proofs.
   7.487 -
   7.488 -\item [\emph{lexicographic\_order}] Attempts a fully automated
   7.489 -  termination proof by searching for a lexicographic combination of
   7.490 -  size measures on the arguments of the function. The method
   7.491 -  accepts the same arguments as the \emph{auto} method, which it uses
   7.492 -  internally to prove local descents. Hence, modifiers like
   7.493 -  \emph{simp}, \emph{intro} etc.\ can be used to add ``hints'' for the
   7.494 -  automated proofs. In case of failure, extensive information is
   7.495 -  printed, which can help to analyse the failure (cf.~\cite{isabelle-function}).
   7.496 -\end{descr}
   7.497 -
   7.498 -\subsubsection{Legacy recursion package}
   7.499 -\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
   7.500 -
   7.501 -The use of the legacy $\isarkeyword{recdef}$ command is now deprecated
   7.502 -in favour of $\isarkeyword{function}$ and $\isarkeyword{fun}$.
   7.503 -
   7.504 -\begin{matharray}{rcl}
   7.505 -  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
   7.506 -  \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
   7.507 -\end{matharray}
   7.508 -
   7.509 -\railalias{recdefsimp}{recdef\_simp}
   7.510 -\railterm{recdefsimp}
   7.511 -
   7.512 -\railalias{recdefcong}{recdef\_cong}
   7.513 -\railterm{recdefcong}
   7.514 -
   7.515 -\railalias{recdefwf}{recdef\_wf}
   7.516 -\railterm{recdefwf}
   7.517 -
   7.518 -\railalias{recdeftc}{recdef\_tc}
   7.519 -\railterm{recdeftc}
   7.520 -
   7.521 -\begin{rail}
   7.522 -  'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
   7.523 -  ;
   7.524 -  recdeftc thmdecl? tc
   7.525 -  ;
   7.526 -  hints: '(' 'hints' (recdefmod *) ')'
   7.527 -  ;
   7.528 -  recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
   7.529 -  ;
   7.530 -  tc: nameref ('(' nat ')')?
   7.531 -  ;
   7.532 -\end{rail}
   7.533 -
   7.534 -\begin{descr}
   7.535 -  
   7.536 -\item [$\isarkeyword{recdef}$] defines general well-founded recursive
   7.537 -  functions (using the TFL package), see also \cite{isabelle-HOL}.  The
   7.538 -  ``$(permissive)$'' option tells TFL to recover from failed proof attempts,
   7.539 -  returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
   7.540 -  $recdef_wf$ hints refer to auxiliary rules to be used in the internal
   7.541 -  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\ 
   7.542 -  \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
   7.543 -  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ 
   7.544 -  \S\ref{sec:classical}).
   7.545 -  
   7.546 -\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
   7.547 -  termination condition number $i$ (default $1$) as generated by a
   7.548 -  $\isarkeyword{recdef}$ definition of constant $c$.
   7.549 -  
   7.550 -  Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
   7.551 -  internal proofs without manual intervention.
   7.552 -
   7.553 -\end{descr}
   7.554 -
   7.555 -\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
   7.556 -the following attributes.
   7.557 -
   7.558 -\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
   7.559 -\begin{matharray}{rcl}
   7.560 -  recdef_simp & : & \isaratt \\
   7.561 -  recdef_cong & : & \isaratt \\
   7.562 -  recdef_wf & : & \isaratt \\
   7.563 -\end{matharray}
   7.564 -
   7.565 -\railalias{recdefsimp}{recdef\_simp}
   7.566 -\railterm{recdefsimp}
   7.567 -
   7.568 -\railalias{recdefcong}{recdef\_cong}
   7.569 -\railterm{recdefcong}
   7.570 -
   7.571 -\railalias{recdefwf}{recdef\_wf}
   7.572 -\railterm{recdefwf}
   7.573 -
   7.574 -\begin{rail}
   7.575 -  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
   7.576 -  ;
   7.577 -\end{rail}
   7.578 -
   7.579 -\subsection{Definition by specification}\label{sec:hol-specification}
   7.580 -
   7.581 -\indexisarcmdof{HOL}{specification}
   7.582 -\begin{matharray}{rcl}
   7.583 -  \isarcmd{specification} & : & \isartrans{theory}{proof(prove)} \\
   7.584 -  \isarcmd{ax_specification} & : & \isartrans{theory}{proof(prove)} \\
   7.585 -\end{matharray}
   7.586 -
   7.587 -\begin{rail}
   7.588 -('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
   7.589 -;
   7.590 -decl: ((name ':')? term '(' 'overloaded' ')'?)
   7.591 -\end{rail}
   7.592 -
   7.593 -\begin{descr}
   7.594 -\item [$\isarkeyword{specification}~decls~\phi$] sets up a goal stating
   7.595 -  the existence of terms with the properties specified to hold for the
   7.596 -  constants given in $\mathit{decls}$.  After finishing the proof, the
   7.597 -  theory will be augmented with definitions for the given constants,
   7.598 -  as well as with theorems stating the properties for these constants.
   7.599 -\item [$\isarkeyword{ax_specification}~decls~\phi$] sets up a goal stating
   7.600 -  the existence of terms with the properties specified to hold for the
   7.601 -  constants given in $\mathit{decls}$.  After finishing the proof, the
   7.602 -  theory will be augmented with axioms expressing the properties given
   7.603 -  in the first place.
   7.604 -\item[$decl$] declares a constant to be defined by the specification
   7.605 -  given.  The definition for the constant $c$ is bound to the name
   7.606 -  $c$\_def unless a theorem name is given in the declaration.
   7.607 -  Overloaded constants should be declared as such.
   7.608 -\end{descr}
   7.609 -
   7.610 -Whether to use $\isarkeyword{specification}$ or $\isarkeyword{ax_specification}$
   7.611 -is to some extent a matter of style.  $\isarkeyword{specification}$ introduces no new axioms,
   7.612 -and so by construction cannot introduce inconsistencies, whereas $\isarkeyword{ax_specification}$
   7.613 -does introduce axioms, but only after the user has explicitly proven it to be
   7.614 -safe.  A practical issue must be considered, though: After introducing two constants
   7.615 -with the same properties using $\isarkeyword{specification}$, one can prove
   7.616 -that the two constants are, in fact, equal.  If this might be a problem,
   7.617 -one should use $\isarkeyword{ax_specification}$.
   7.618 -
   7.619 -\subsection{Inductive and coinductive definitions}\label{sec:hol-inductive}
   7.620 -
   7.621 -An {\bf inductive definition} specifies the least predicate (or set) $R$ closed under given
   7.622 -rules.  (Applying a rule to elements of~$R$ yields a result within~$R$.)  For
   7.623 -example, a structural operational semantics is an inductive definition of an
   7.624 -evaluation relation.  Dually, a {\bf coinductive definition} specifies the
   7.625 -greatest predicate (or set) $R$ consistent with given rules.  (Every element of~$R$ can be
   7.626 -seen as arising by applying a rule to elements of~$R$.)  An important example
   7.627 -is using bisimulation relations to formalise equivalence of processes and
   7.628 -infinite data structures.
   7.629 -
   7.630 -This package is related to the ZF one, described in a separate
   7.631 -paper,%
   7.632 -\footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
   7.633 -  distributed with Isabelle.}  %
   7.634 -which you should refer to in case of difficulties.  The package is simpler
   7.635 -than ZF's thanks to HOL's extra-logical automatic type-checking.  The types of
   7.636 -the (co)inductive predicates (or sets) determine the domain of the fixedpoint definition, and
   7.637 -the package does not have to use inference rules for type-checking.
   7.638 -
   7.639 -\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{inductive-set}\indexisarcmdof{HOL}{coinductive}\indexisarcmdof{HOL}{coinductive-set}\indexisarattof{HOL}{mono}
   7.640 -\begin{matharray}{rcl}
   7.641 -  \isarcmd{inductive} & : & \isarkeep{local{\dsh}theory} \\
   7.642 -  \isarcmd{inductive_set} & : & \isarkeep{local{\dsh}theory} \\
   7.643 -  \isarcmd{coinductive} & : & \isarkeep{local{\dsh}theory} \\
   7.644 -  \isarcmd{coinductive_set} & : & \isarkeep{local{\dsh}theory} \\
   7.645 -  mono & : & \isaratt \\
   7.646 -\end{matharray}
   7.647 -
   7.648 -\begin{rail}
   7.649 -  ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
   7.650 -  ('where' clauses)? ('monos' thmrefs)?
   7.651 -  ;
   7.652 -  clauses: (thmdecl? prop + '|')
   7.653 -  ;
   7.654 -  'mono' (() | 'add' | 'del')
   7.655 -  ;
   7.656 -\end{rail}
   7.657 -
   7.658 -\begin{descr}
   7.659 -\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
   7.660 -  (co)inductive predicates from the introduction rules given in the \texttt{where} section.
   7.661 -  The optional \texttt{for} section contains a list of parameters of the (co)inductive
   7.662 -  predicates that remain fixed throughout the definition.
   7.663 -  The optional \texttt{monos} section contains \textit{monotonicity theorems},
   7.664 -  which are required for each operator applied to a recursive set in the introduction rules.
   7.665 -  There {\bf must} be a theorem of the form $A \leq B \Imp M~A \leq M~B$, for each
   7.666 -  premise $M~R@i~t$ in an introduction rule!
   7.667 -\item [$\isarkeyword{inductive_set}$ and $\isarkeyword{coinductive_set}$] are wrappers
   7.668 -  for to the previous commands, allowing the definition of (co)inductive sets.
   7.669 -\item [$mono$] declares monotonicity rules.  These rule are involved in the
   7.670 -  automated monotonicity proof of $\isarkeyword{inductive}$.
   7.671 -\end{descr}
   7.672 -
   7.673 -\subsubsection{Derived rules}
   7.674 -
   7.675 -Each (co)inductive definition $R$ adds definitions to the theory and also
   7.676 -proves some theorems:
   7.677 -\begin{description}
   7.678 -\item[$R{\dtt}intros$] is the list of introduction rules, now proved as theorems, for
   7.679 -the recursive predicates (or sets).  The rules are also available individually,
   7.680 -using the names given them in the theory file.
   7.681 -\item[$R{\dtt}cases$] is the case analysis (or elimination) rule.
   7.682 -\item[$R{\dtt}(co)induct$] is the (co)induction rule.
   7.683 -\end{description}
   7.684 -When several predicates $R@1$, $\ldots$, $R@n$ are defined simultaneously,
   7.685 -the list of introduction rules is called $R@1_\ldots_R@n{\dtt}intros$, the
   7.686 -case analysis rules are called $R@1{\dtt}cases$, $\ldots$, $R@n{\dtt}cases$, and
   7.687 -the list of mutual induction rules is called $R@1_\ldots_R@n{\dtt}inducts$.
   7.688 -
   7.689 -\subsubsection{Monotonicity theorems}
   7.690 -
   7.691 -Each theory contains a default set of theorems that are used in monotonicity
   7.692 -proofs. New rules can be added to this set via the $mono$ attribute.
   7.693 -Theory \texttt{Inductive} shows how this is done. In general, the following
   7.694 -monotonicity theorems may be added:
   7.695 -\begin{itemize}
   7.696 -\item Theorems of the form $A \leq B \Imp M~A \leq M~B$, for proving
   7.697 -  monotonicity of inductive definitions whose introduction rules have premises
   7.698 -  involving terms such as $M~R@i~t$.
   7.699 -\item Monotonicity theorems for logical operators, which are of the general form
   7.700 -  $\List{\cdots \to \cdots;~\ldots;~\cdots \to \cdots} \Imp
   7.701 -    \cdots \to \cdots$.
   7.702 -  For example, in the case of the operator $\lor$, the corresponding theorem is
   7.703 -  \[
   7.704 -  \infer{P@1 \lor P@2 \to Q@1 \lor Q@2}
   7.705 -    {P@1 \to Q@1 & P@2 \to Q@2}
   7.706 -  \]
   7.707 -\item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g.
   7.708 -  \[
   7.709 -  (\lnot \lnot P) ~=~ P \qquad\qquad
   7.710 -  (\lnot (P \land Q)) ~=~ (\lnot P \lor \lnot Q)
   7.711 -  \]
   7.712 -\item Equations for reducing complex operators to more primitive ones whose
   7.713 -  monotonicity can easily be proved, e.g.
   7.714 -  \[
   7.715 -  (P \to Q) ~=~ (\lnot P \lor Q) \qquad\qquad
   7.716 -  \mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \to P~x
   7.717 -  \]
   7.718 -\end{itemize}
   7.719 -
   7.720 -%FIXME: Example of an inductive definition
   7.721 -
   7.722 -
   7.723 -\subsection{Arithmetic proof support}
   7.724 -
   7.725 -\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
   7.726 -\begin{matharray}{rcl}
   7.727 -  arith & : & \isarmeth \\
   7.728 -  arith_split & : & \isaratt \\
   7.729 -\end{matharray}
   7.730 -
   7.731 -\begin{rail}
   7.732 -  'arith' '!'?
   7.733 -  ;
   7.734 -\end{rail}
   7.735 -
   7.736 -The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
   7.737 -$real$).  Any current facts are inserted into the goal before running the
   7.738 -procedure.  The ``!''~argument causes the full context of assumptions to be
   7.739 -included.  The $arith_split$ attribute declares case split rules to be
   7.740 -expanded before the arithmetic procedure is invoked.
   7.741 -
   7.742 -Note that a simpler (but faster) version of arithmetic reasoning is already
   7.743 -performed by the Simplifier.
   7.744 -
   7.745 -
   7.746 -\subsection{Cases and induction: emulating tactic scripts}\label{sec:hol-induct-tac}
   7.747 -
   7.748 -The following important tactical tools of Isabelle/HOL have been ported to
   7.749 -Isar.  These should be never used in proper proof texts!
   7.750 -
   7.751 -\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
   7.752 -\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
   7.753 -\begin{matharray}{rcl}
   7.754 -  case_tac^* & : & \isarmeth \\
   7.755 -  induct_tac^* & : & \isarmeth \\
   7.756 -  ind_cases^* & : & \isarmeth \\
   7.757 -  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
   7.758 -\end{matharray}
   7.759 -
   7.760 -\railalias{casetac}{case\_tac}
   7.761 -\railterm{casetac}
   7.762 -
   7.763 -\railalias{inducttac}{induct\_tac}
   7.764 -\railterm{inducttac}
   7.765 -
   7.766 -\railalias{indcases}{ind\_cases}
   7.767 -\railterm{indcases}
   7.768 -
   7.769 -\railalias{inductivecases}{inductive\_cases}
   7.770 -\railterm{inductivecases}
   7.771 -
   7.772 -\begin{rail}
   7.773 -  casetac goalspec? term rule?
   7.774 -  ;
   7.775 -  inducttac goalspec? (insts * 'and') rule?
   7.776 -  ;
   7.777 -  indcases (prop +) ('for' (name +)) ?
   7.778 -  ;
   7.779 -  inductivecases (thmdecl? (prop +) + 'and')
   7.780 -  ;
   7.781 -
   7.782 -  rule: ('rule' ':' thmref)
   7.783 -  ;
   7.784 -\end{rail}
   7.785 -
   7.786 -\begin{descr}
   7.787 -\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
   7.788 -  only (unless an alternative rule is given explicitly).  Furthermore,
   7.789 -  $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
   7.790 -  variables to be given as instantiation.  These tactic emulations feature
   7.791 -  both goal addressing and dynamic instantiation.  Note that named rule cases
   7.792 -  are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
   7.793 -  methods (see \S\ref{sec:cases-induct}).
   7.794 -  
   7.795 -\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
   7.796 -  to the internal \texttt{mk_cases} operation.  Rules are simplified in an
   7.797 -  unrestricted forward manner.
   7.798 -
   7.799 -  While $ind_cases$ is a proof method to apply the result immediately as
   7.800 -  elimination rules, $\isarkeyword{inductive_cases}$ provides case split
   7.801 -  theorems at the theory level for later use.
   7.802 -  The \texttt{for} option of the $ind_cases$ method allows to specify a list
   7.803 -  of variables that should be generalized before applying the resulting rule.
   7.804 -\end{descr}
   7.805 -
   7.806 -
   7.807 -\subsection{Executable code}
   7.808 -
   7.809 -Isabelle/Pure provides two generic frameworks to support code
   7.810 -generation from executable specifications. Isabelle/HOL
   7.811 -instantiates these mechanisms in a
   7.812 -way that is amenable to end-user applications.
   7.813 -
   7.814 -One framework generates code from both functional and
   7.815 -relational programs to SML.  See
   7.816 -\cite{isabelle-HOL} for further information (this actually covers the
   7.817 -new-style theory format as well).
   7.818 -
   7.819 -\indexisarcmd{value}\indexisarcmd{code-module}\indexisarcmd{code-library}
   7.820 -\indexisarcmd{consts-code}\indexisarcmd{types-code}
   7.821 -\indexisaratt{code}
   7.822 -
   7.823 -\begin{matharray}{rcl}
   7.824 -  \isarcmd{value}^* & : & \isarkeep{theory~|~proof} \\
   7.825 -  \isarcmd{code_module} & : & \isartrans{theory}{theory} \\
   7.826 -  \isarcmd{code_library} & : & \isartrans{theory}{theory} \\
   7.827 -  \isarcmd{consts_code} & : & \isartrans{theory}{theory} \\
   7.828 -  \isarcmd{types_code} & : & \isartrans{theory}{theory} \\  
   7.829 -  code & : & \isaratt \\
   7.830 -\end{matharray}
   7.831 -
   7.832 -\railalias{verblbrace}{\texttt{\ttlbrace*}}
   7.833 -\railalias{verbrbrace}{\texttt{*\ttrbrace}}
   7.834 -\railterm{verblbrace}
   7.835 -\railterm{verbrbrace}
   7.836 -
   7.837 -\begin{rail}
   7.838 -'value' term;
   7.839 -
   7.840 -( 'code\_module' | 'code\_library' ) modespec ? name ? \\
   7.841 -  ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
   7.842 -  'contains' ( ( name '=' term ) + | term + );
   7.843 -
   7.844 -modespec : '(' ( name * ) ')';
   7.845 -
   7.846 -'consts\_code' (codespec +);
   7.847 -
   7.848 -codespec : const template attachment ?;
   7.849 -
   7.850 -'types\_code' (tycodespec +);
   7.851 -
   7.852 -tycodespec : name template attachment ?;
   7.853 -
   7.854 -const: term;
   7.855 -
   7.856 -template: '(' string ')';
   7.857 -
   7.858 -attachment: 'attach' modespec ? verblbrace text verbrbrace;
   7.859 -
   7.860 -'code' (name)?;
   7.861 -\end{rail}
   7.862 -
   7.863 -\begin{descr}
   7.864 -\item [$\isarkeyword{value}~t$] reads, evaluates and prints a term
   7.865 -  using the code generator.
   7.866 -\end{descr}
   7.867 -
   7.868 -The other framework generates code from functional programs
   7.869 -(including overloading using type classes) to SML \cite{SML},
   7.870 -OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}.
   7.871 -Conceptually, code generation is split up in three steps: \emph{selection}
   7.872 -of code theorems, \emph{translation} into an abstract executable view
   7.873 -and \emph{serialization} to a specific \emph{target language}.
   7.874 -See \cite{isabelle-codegen} for an introduction on how to use it.
   7.875 -
   7.876 -\indexisarcmd{export-code}
   7.877 -\indexisarcmd{code-thms}
   7.878 -\indexisarcmd{code-deps}
   7.879 -\indexisarcmd{code-datatype}
   7.880 -\indexisarcmd{code-const}
   7.881 -\indexisarcmd{code-type}
   7.882 -\indexisarcmd{code-class}
   7.883 -\indexisarcmd{code-instance}
   7.884 -\indexisarcmd{code-monad}
   7.885 -\indexisarcmd{code-reserved}
   7.886 -\indexisarcmd{code-include}
   7.887 -\indexisarcmd{code-modulename}
   7.888 -\indexisarcmd{code-exception}
   7.889 -\indexisarcmd{print-codesetup}
   7.890 -\indexisaratt{code func}
   7.891 -\indexisaratt{code inline}
   7.892 -
   7.893 -\begin{matharray}{rcl}
   7.894 -  \isarcmd{export_code}^* & : & \isarkeep{theory~|~proof} \\
   7.895 -  \isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\
   7.896 -  \isarcmd{code_deps}^* & : & \isarkeep{theory~|~proof} \\
   7.897 -  \isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\
   7.898 -  \isarcmd{code_const} & : & \isartrans{theory}{theory} \\
   7.899 -  \isarcmd{code_type} & : & \isartrans{theory}{theory} \\
   7.900 -  \isarcmd{code_class} & : & \isartrans{theory}{theory} \\
   7.901 -  \isarcmd{code_instance} & : & \isartrans{theory}{theory} \\
   7.902 -  \isarcmd{code_monad} & : & \isartrans{theory}{theory} \\
   7.903 -  \isarcmd{code_reserved} & : & \isartrans{theory}{theory} \\
   7.904 -  \isarcmd{code_include} & : & \isartrans{theory}{theory} \\
   7.905 -  \isarcmd{code_modulename} & : & \isartrans{theory}{theory} \\
   7.906 -  \isarcmd{code_exception} & : & \isartrans{theory}{theory} \\
   7.907 -  \isarcmd{print_codesetup}^* & : & \isarkeep{theory~|~proof} \\
   7.908 -  code\ func & : & \isaratt \\
   7.909 -  code\ inline & : & \isaratt \\
   7.910 -\end{matharray}
   7.911 -
   7.912 -\begin{rail}
   7.913 -'export\_code' ( constexpr + ) ? \\
   7.914 -  ( ( 'in' target ( 'module\_name' string ) ? \\
   7.915 -      ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
   7.916 -
   7.917 -'code\_thms' ( constexpr + ) ?;
   7.918 -
   7.919 -'code\_deps' ( constexpr + ) ?;
   7.920 -
   7.921 -const : term;
   7.922 -
   7.923 -constexpr : ( const | 'name.*' | '*' );
   7.924 -
   7.925 -typeconstructor : nameref;
   7.926 -
   7.927 -class : nameref;
   7.928 -
   7.929 -target : 'OCaml' | 'SML' | 'Haskell';
   7.930 -
   7.931 -'code\_datatype' const +;
   7.932 -
   7.933 -'code\_const' (const + 'and') \\
   7.934 -  ( ( '(' target ( syntax ? + 'and' ) ')' ) + );
   7.935 -
   7.936 -'code\_type' (typeconstructor + 'and') \\
   7.937 -  ( ( '(' target ( syntax ? + 'and' ) ')' ) + );
   7.938 -
   7.939 -'code\_class' (class + 'and') \\
   7.940 -  ( ( '(' target \\
   7.941 -    ( ( string ('where' \\
   7.942 -      ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + );
   7.943 -
   7.944 -'code\_instance' (( typeconstructor '::' class ) + 'and') \\
   7.945 -  ( ( '(' target ( '-' ? + 'and' ) ')' ) + );
   7.946 -
   7.947 -'code\_monad' const const target;
   7.948 -
   7.949 -'code\_reserved' target ( string + );
   7.950 -
   7.951 -'code\_include' target ( string ( string | '-') );
   7.952 -
   7.953 -'code\_modulename' target ( ( string string ) + );
   7.954 -
   7.955 -'code\_exception' ( const + );
   7.956 -
   7.957 -syntax : string | ( 'infix' | 'infixl' | 'infixr' ) nat string;
   7.958 -
   7.959 -'print\_codesetup';
   7.960 -
   7.961 -'code\ func' ( 'del' ) ?;
   7.962 -
   7.963 -'code\ inline' ( 'del' ) ?;
   7.964 -\end{rail}
   7.965 -
   7.966 -\begin{descr}
   7.967 -
   7.968 -\item [$\isarcmd{export_code}$] is the canonical interface for generating and
   7.969 -  serializing code: for a given list of constants, code is generated for the specified
   7.970 -  target language(s).  Abstract code is cached incrementally.  If no constant is given,
   7.971 -  the currently cached code is serialized.  If no serialization instruction
   7.972 -  is given, only abstract code is cached.
   7.973 -
   7.974 -  Constants may be specified by giving them literally, referring
   7.975 -  to all exeuctable contants within a certain theory named ``name''
   7.976 -  by giving (``name.*''), or referring to \emph{all} executable
   7.977 -  constants currently available (``*'').
   7.978 -
   7.979 -  By default, for each involved theory one corresponding name space module
   7.980 -  is generated.  Alternativly, a module name may be specified after the
   7.981 -  (``module_name'') keyword; then \emph{all} code is placed in this module.
   7.982 -
   7.983 -  For \emph{SML} and \emph{OCaml}, the file specification refers to
   7.984 -  a single file;  for \emph{Haskell}, it refers to a whole directory,
   7.985 -  where code is generated in multiple files reflecting the module hierarchy.
   7.986 -  The file specification ``-'' denotes standard output.  For \emph{SML},
   7.987 -  omitting the file specification compiles code internally
   7.988 -  in the context of the current ML session.
   7.989 -
   7.990 -  Serializers take an optional list of arguments in parentheses. 
   7.991 -  For \emph{Haskell} a module name prefix may be given using the ``root:''
   7.992 -  argument;  ``string\_classes'' adds a ``deriving (Read, Show)'' clause
   7.993 -  to each appropriate datatype declaration.
   7.994 -
   7.995 -\item [$\isarcmd{code_thms}$] prints a list of theorems representing the
   7.996 -  corresponding program containing all given constants; if no constants are
   7.997 -  given, the currently cached code theorems are printed.
   7.998 -
   7.999 -\item [$\isarcmd{code_deps}$] visualizes dependencies of theorems representing the
  7.1000 -  corresponding program containing all given constants; if no constants are
  7.1001 -  given, the currently cached code theorems are visualized.
  7.1002 -
  7.1003 -\item [$\isarcmd{code_datatype}$] specifies a constructor set for a logical type.
  7.1004 -
  7.1005 -\item [$\isarcmd{code_const}$] associates a list of constants
  7.1006 -  with target-specific serializations; omitting a serialization
  7.1007 -  deletes an existing serialization.
  7.1008 -
  7.1009 -\item [$\isarcmd{code_type}$] associates a list of type constructors
  7.1010 -  with target-specific serializations; omitting a serialization
  7.1011 -  deletes an existing serialization.
  7.1012 -
  7.1013 -\item [$\isarcmd{code_class}$] associates a list of classes
  7.1014 -  with target-specific class names; in addition, constants associated
  7.1015 -  with this class may be given target-specific names used for instance
  7.1016 -  declarations; omitting a serialization
  7.1017 -  deletes an existing serialization.  Applies only to \emph{Haskell}.
  7.1018 -
  7.1019 -\item [$\isarcmd{code_instance}$] declares a list of type constructor / class
  7.1020 -  instance relations as ``already present'' for a given target.
  7.1021 -  Omitting a ``-'' deletes an existing ``already present'' declaration.
  7.1022 -  Applies only to \emph{Haskell}.
  7.1023 -
  7.1024 -\item [$\isarcmd{code_monad}$] provides an auxiliary mechanism
  7.1025 -  to generate monadic code.
  7.1026 -
  7.1027 -\item [$\isarcmd{code_reserved}$] declares a list of names
  7.1028 -  as reserved for a given target, preventing it to be shadowed
  7.1029 -  by any generated code.
  7.1030 -
  7.1031 -\item [$\isarcmd{code_include}$] adds arbitrary named content (''include``)
  7.1032 -  to generated code. A as last argument ``-'' will remove an already added ''include``.
  7.1033 -
  7.1034 -\item [$\isarcmd{code_modulename}$] declares aliasings from one module name
  7.1035 -  onto another.
  7.1036 -
  7.1037 -\item [$\isarcmd{code_exception}$] declares constants which are not required
  7.1038 -  to have a definition by a defining equations; these are mapped on exceptions
  7.1039 -  instead.
  7.1040 -
  7.1041 -\item [$code\ func$] selects (or with option ''del``, deselects) explicitly
  7.1042 -  a defining equation for code generation.  Usually packages introducing
  7.1043 -  defining equations provide a resonable default setup for selection.
  7.1044 -
  7.1045 -\item [$code\ inline$] declares (or with option ''del``, removes)
  7.1046 -  inlining theorems which are applied as rewrite rules to any defining equation
  7.1047 -  during preprocessing.
  7.1048 -
  7.1049 -\item [$\isarcmd{print_codesetup}$] gives an overview on selected
  7.1050 -  defining equations, code generator datatypes and preprocessor setup.
  7.1051 -
  7.1052 -\end{descr}
  7.1053 -
  7.1054 -
  7.1055 -%%% Local Variables:
  7.1056 -%%% mode: latex
  7.1057 -%%% TeX-master: "isar-ref"
  7.1058 -%%% End: