doc-src/IsarRef/Thy/document/HOL_Specific.tex
author Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Fri Feb 10 09:47:59 2012 +0100 (2012-02-10)
changeset 46448 f1201fac7398
parent 46447 f37da60a8cc6
child 46457 915af80f74b3
permissions -rw-r--r--
more specification of the quotient package in IsarRef
wenzelm@26840
     1
%
wenzelm@26840
     2
\begin{isabellebody}%
wenzelm@40406
     3
\def\isabellecontext{HOL{\isaliteral{5F}{\isacharunderscore}}Specific}%
wenzelm@26840
     4
%
wenzelm@26840
     5
\isadelimtheory
wenzelm@26840
     6
%
wenzelm@26840
     7
\endisadelimtheory
wenzelm@26840
     8
%
wenzelm@26840
     9
\isatagtheory
wenzelm@26840
    10
\isacommand{theory}\isamarkupfalse%
wenzelm@40406
    11
\ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
wenzelm@44055
    12
\isakeyword{imports}\ Base\ Main\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}Library{\isaliteral{2F}{\isacharslash}}Old{\isaliteral{5F}{\isacharunderscore}}Recdef{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@26849
    13
\isakeyword{begin}%
wenzelm@26849
    14
\endisatagtheory
wenzelm@26849
    15
{\isafoldtheory}%
wenzelm@26849
    16
%
wenzelm@26849
    17
\isadelimtheory
wenzelm@26849
    18
%
wenzelm@26849
    19
\endisadelimtheory
wenzelm@26849
    20
%
wenzelm@26852
    21
\isamarkupchapter{Isabelle/HOL \label{ch:hol}%
wenzelm@26849
    22
}
wenzelm@26849
    23
\isamarkuptrue%
wenzelm@26849
    24
%
wenzelm@42914
    25
\isamarkupsection{Higher-Order Logic%
wenzelm@42914
    26
}
wenzelm@42914
    27
\isamarkuptrue%
wenzelm@42914
    28
%
wenzelm@42914
    29
\begin{isamarkuptext}%
wenzelm@42914
    30
Isabelle/HOL is based on Higher-Order Logic, a polymorphic
wenzelm@42914
    31
  version of Church's Simple Theory of Types.  HOL can be best
wenzelm@42914
    32
  understood as a simply-typed version of classical set theory.  The
wenzelm@42914
    33
  logic was first implemented in Gordon's HOL system
wenzelm@42914
    34
  \cite{mgordon-hol}.  It extends Church's original logic
wenzelm@42914
    35
  \cite{church40} by explicit type variables (naive polymorphism) and
wenzelm@42914
    36
  a sound axiomatization scheme for new types based on subsets of
wenzelm@42914
    37
  existing types.
wenzelm@42914
    38
wenzelm@42914
    39
  Andrews's book \cite{andrews86} is a full description of the
wenzelm@42914
    40
  original Church-style higher-order logic, with proofs of correctness
wenzelm@42914
    41
  and completeness wrt.\ certain set-theoretic interpretations.  The
wenzelm@42914
    42
  particular extensions of Gordon-style HOL are explained semantically
wenzelm@42914
    43
  in two chapters of the 1993 HOL book \cite{pitts93}.
wenzelm@42914
    44
wenzelm@42914
    45
  Experience with HOL over decades has demonstrated that higher-order
wenzelm@42914
    46
  logic is widely applicable in many areas of mathematics and computer
wenzelm@42914
    47
  science.  In a sense, Higher-Order Logic is simpler than First-Order
wenzelm@42914
    48
  Logic, because there are fewer restrictions and special cases.  Note
wenzelm@42914
    49
  that HOL is \emph{weaker} than FOL with axioms for ZF set theory,
wenzelm@42914
    50
  which is traditionally considered the standard foundation of regular
wenzelm@42914
    51
  mathematics, but for most applications this does not matter.  If you
wenzelm@42914
    52
  prefer ML to Lisp, you will probably prefer HOL to ZF.
wenzelm@42914
    53
wenzelm@42914
    54
  \medskip The syntax of HOL follows \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-calculus and
wenzelm@42914
    55
  functional programming.  Function application is curried.  To apply
wenzelm@42914
    56
  the function \isa{f} of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}} to the
wenzelm@42914
    57
  arguments \isa{a} and \isa{b} in HOL, you simply write \isa{{\isaliteral{22}{\isachardoublequote}}f\ a\ b{\isaliteral{22}{\isachardoublequote}}} (as in ML or Haskell).  There is no ``apply'' operator; the
wenzelm@42914
    58
  existing application of the Pure \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-calculus is re-used.
wenzelm@42914
    59
  Note that in HOL \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} means ``\isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} applied to
wenzelm@42914
    60
  the pair \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} (which is notation for \isa{{\isaliteral{22}{\isachardoublequote}}Pair\ a\ b{\isaliteral{22}{\isachardoublequote}}}).  The latter typically introduces extra formal efforts that can
wenzelm@42914
    61
  be avoided by currying functions by default.  Explicit tuples are as
wenzelm@42914
    62
  infrequent in HOL formalizations as in good ML or Haskell programs.
wenzelm@42914
    63
wenzelm@42914
    64
  \medskip Isabelle/HOL has a distinct feel, compared to other
wenzelm@42914
    65
  object-logics like Isabelle/ZF.  It identifies object-level types
wenzelm@42914
    66
  with meta-level types, taking advantage of the default
wenzelm@42914
    67
  type-inference mechanism of Isabelle/Pure.  HOL fully identifies
wenzelm@42914
    68
  object-level functions with meta-level functions, with native
wenzelm@42914
    69
  abstraction and application.
wenzelm@42914
    70
wenzelm@42914
    71
  These identifications allow Isabelle to support HOL particularly
wenzelm@42914
    72
  nicely, but they also mean that HOL requires some sophistication
wenzelm@42914
    73
  from the user.  In particular, an understanding of Hindley-Milner
wenzelm@42914
    74
  type-inference with type-classes, which are both used extensively in
wenzelm@42914
    75
  the standard libraries and applications.  Beginners can set
wenzelm@42914
    76
  \hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}} or even \hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}} to get more
wenzelm@42914
    77
  explicit information about the result of type-inference.%
wenzelm@42914
    78
\end{isamarkuptext}%
wenzelm@42914
    79
\isamarkuptrue%
wenzelm@42914
    80
%
wenzelm@42908
    81
\isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
wenzelm@26849
    82
}
wenzelm@26849
    83
\isamarkuptrue%
wenzelm@26849
    84
%
wenzelm@26849
    85
\begin{isamarkuptext}%
wenzelm@42913
    86
An \emph{inductive definition} specifies the least predicate
wenzelm@42913
    87
  or set \isa{R} closed under given rules: applying a rule to
wenzelm@42913
    88
  elements of \isa{R} yields a result within \isa{R}.  For
wenzelm@42913
    89
  example, a structural operational semantics is an inductive
wenzelm@42913
    90
  definition of an evaluation relation.
wenzelm@42908
    91
wenzelm@42913
    92
  Dually, a \emph{coinductive definition} specifies the greatest
wenzelm@42913
    93
  predicate or set \isa{R} that is consistent with given rules:
wenzelm@42913
    94
  every element of \isa{R} can be seen as arising by applying a rule
wenzelm@42913
    95
  to elements of \isa{R}.  An important example is using
wenzelm@42913
    96
  bisimulation relations to formalise equivalence of processes and
wenzelm@42913
    97
  infinite data structures.
wenzelm@42913
    98
  
wenzelm@42913
    99
  Both inductive and coinductive definitions are based on the
wenzelm@42913
   100
  Knaster-Tarski fixed-point theorem for complete lattices.  The
wenzelm@42913
   101
  collection of introduction rules given by the user determines a
wenzelm@42913
   102
  functor on subsets of set-theoretic relations.  The required
wenzelm@42913
   103
  monotonicity of the recursion scheme is proven as a prerequisite to
wenzelm@42913
   104
  the fixed-point definition and the resulting consequences.  This
wenzelm@42913
   105
  works by pushing inclusion through logical connectives and any other
wenzelm@42913
   106
  operator that might be wrapped around recursive occurrences of the
wenzelm@42913
   107
  defined relation: there must be a monotonicity theorem of the form
wenzelm@42913
   108
  \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ B{\isaliteral{22}{\isachardoublequote}}}, for each premise \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4D3E}{\isasymM}}\ R\ t{\isaliteral{22}{\isachardoublequote}}} in an
wenzelm@42913
   109
  introduction rule.  The default rule declarations of Isabelle/HOL
wenzelm@42913
   110
  already take care of most common situations.
wenzelm@42908
   111
wenzelm@42907
   112
  \begin{matharray}{rcl}
wenzelm@42908
   113
    \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
   114
    \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
   115
    \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
   116
    \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
   117
    \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
wenzelm@26849
   118
  \end{matharray}
wenzelm@26849
   119
wenzelm@42596
   120
  \begin{railoutput}
wenzelm@42913
   121
\rail@begin{10}{}
wenzelm@42908
   122
\rail@bar
wenzelm@42908
   123
\rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
wenzelm@42908
   124
\rail@nextbar{1}
wenzelm@42908
   125
\rail@term{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
wenzelm@42908
   126
\rail@nextbar{2}
wenzelm@42908
   127
\rail@term{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]
wenzelm@42908
   128
\rail@nextbar{3}
wenzelm@42908
   129
\rail@term{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
wenzelm@42908
   130
\rail@endbar
wenzelm@42596
   131
\rail@bar
wenzelm@42596
   132
\rail@nextbar{1}
wenzelm@42908
   133
\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
wenzelm@42596
   134
\rail@endbar
wenzelm@42913
   135
\rail@cr{5}
wenzelm@42908
   136
\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
wenzelm@42596
   137
\rail@bar
wenzelm@42913
   138
\rail@nextbar{6}
wenzelm@42908
   139
\rail@term{\isa{\isakeyword{for}}}[]
wenzelm@42908
   140
\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
wenzelm@42596
   141
\rail@endbar
wenzelm@42596
   142
\rail@bar
wenzelm@42908
   143
\rail@nextbar{6}
wenzelm@42908
   144
\rail@term{\isa{\isakeyword{where}}}[]
wenzelm@42908
   145
\rail@nont{\isa{clauses}}[]
wenzelm@42908
   146
\rail@endbar
wenzelm@42913
   147
\rail@cr{8}
wenzelm@42908
   148
\rail@bar
wenzelm@42913
   149
\rail@nextbar{9}
wenzelm@42908
   150
\rail@term{\isa{\isakeyword{monos}}}[]
wenzelm@42908
   151
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
wenzelm@42596
   152
\rail@endbar
wenzelm@42596
   153
\rail@end
wenzelm@42908
   154
\rail@begin{3}{\isa{clauses}}
wenzelm@42908
   155
\rail@plus
wenzelm@42596
   156
\rail@bar
wenzelm@42596
   157
\rail@nextbar{1}
wenzelm@42908
   158
\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
wenzelm@42908
   159
\rail@endbar
wenzelm@42908
   160
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
wenzelm@42908
   161
\rail@nextplus{2}
wenzelm@42908
   162
\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
wenzelm@42908
   163
\rail@endplus
wenzelm@42908
   164
\rail@end
wenzelm@42908
   165
\rail@begin{3}{}
wenzelm@42908
   166
\rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
wenzelm@42908
   167
\rail@bar
wenzelm@42908
   168
\rail@nextbar{1}
wenzelm@42908
   169
\rail@term{\isa{add}}[]
wenzelm@42908
   170
\rail@nextbar{2}
wenzelm@42908
   171
\rail@term{\isa{del}}[]
wenzelm@42596
   172
\rail@endbar
wenzelm@42596
   173
\rail@end
wenzelm@42596
   174
\end{railoutput}
wenzelm@42596
   175
wenzelm@26849
   176
wenzelm@28788
   177
  \begin{description}
wenzelm@42123
   178
wenzelm@42913
   179
  \item \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}} define (co)inductive predicates from the introduction
wenzelm@42913
   180
  rules.
wenzelm@42913
   181
wenzelm@42913
   182
  The propositions given as \isa{{\isaliteral{22}{\isachardoublequote}}clauses{\isaliteral{22}{\isachardoublequote}}} in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part are either rules of the usual \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} format
wenzelm@42913
   183
  (with arbitrary nesting), or equalities using \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}}.  The
wenzelm@42913
   184
  latter specifies extra-logical abbreviations in the sense of
wenzelm@42913
   185
  \indexref{}{command}{abbreviation}\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}.  Introducing abstract syntax
wenzelm@42913
   186
  simultaneously with the actual introduction rules is occasionally
wenzelm@42913
   187
  useful for complex specifications.
wenzelm@42913
   188
wenzelm@42913
   189
  The optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of
wenzelm@42913
   190
  the (co)inductive predicates that remain fixed throughout the
wenzelm@42913
   191
  definition, in contrast to arguments of the relation that may vary
wenzelm@42913
   192
  in each occurrence within the given \isa{{\isaliteral{22}{\isachardoublequote}}clauses{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@42913
   193
wenzelm@42913
   194
  The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} declaration contains additional
wenzelm@42908
   195
  \emph{monotonicity theorems}, which are required for each operator
wenzelm@42913
   196
  applied to a recursive set in the introduction rules.
wenzelm@26849
   197
wenzelm@42913
   198
  \item \hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}} are wrappers for to the previous commands for
wenzelm@42913
   199
  native HOL predicates.  This allows to define (co)inductive sets,
wenzelm@42913
   200
  where multiple arguments are simulated via tuples.
wenzelm@26849
   201
wenzelm@42913
   202
  \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules in the
wenzelm@42913
   203
  context.  These rule are involved in the automated monotonicity
wenzelm@42913
   204
  proof of the above inductive and coinductive definitions.
wenzelm@26849
   205
wenzelm@28788
   206
  \end{description}%
wenzelm@26849
   207
\end{isamarkuptext}%
wenzelm@26849
   208
\isamarkuptrue%
wenzelm@26849
   209
%
wenzelm@42908
   210
\isamarkupsubsection{Derived rules%
wenzelm@26849
   211
}
wenzelm@26849
   212
\isamarkuptrue%
wenzelm@26849
   213
%
wenzelm@26849
   214
\begin{isamarkuptext}%
wenzelm@42913
   215
A (co)inductive definition of \isa{R} provides the following
wenzelm@42913
   216
  main theorems:
wenzelm@26849
   217
wenzelm@42908
   218
  \begin{description}
wenzelm@26849
   219
wenzelm@42908
   220
  \item \isa{R{\isaliteral{2E}{\isachardot}}intros} is the list of introduction rules as proven
wenzelm@42908
   221
  theorems, for the recursive predicates (or sets).  The rules are
wenzelm@42908
   222
  also available individually, using the names given them in the
wenzelm@42908
   223
  theory file;
wenzelm@26849
   224
wenzelm@42908
   225
  \item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
wenzelm@42908
   226
wenzelm@42908
   227
  \item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
bulwahn@44273
   228
  rule;
bulwahn@44273
   229
bulwahn@44273
   230
  \item \isa{R{\isaliteral{2E}{\isachardot}}simps} is the equation unrolling the fixpoint of the
bulwahn@44273
   231
  predicate one step.
bulwahn@44273
   232
 
wenzelm@42908
   233
  \end{description}
wenzelm@26849
   234
wenzelm@42908
   235
  When several predicates \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are
wenzelm@42908
   236
  defined simultaneously, the list of introduction rules is called
wenzelm@42908
   237
  \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5F}{\isacharunderscore}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}intros{\isaliteral{22}{\isachardoublequote}}}, the case analysis rules are
wenzelm@42908
   238
  called \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}cases{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}cases{\isaliteral{22}{\isachardoublequote}}}, and the list
wenzelm@42908
   239
  of mutual induction rules is called \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5F}{\isacharunderscore}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}inducts{\isaliteral{22}{\isachardoublequote}}}.%
wenzelm@26849
   240
\end{isamarkuptext}%
wenzelm@26849
   241
\isamarkuptrue%
wenzelm@26849
   242
%
wenzelm@42908
   243
\isamarkupsubsection{Monotonicity theorems%
wenzelm@26849
   244
}
wenzelm@26849
   245
\isamarkuptrue%
wenzelm@26849
   246
%
wenzelm@26849
   247
\begin{isamarkuptext}%
wenzelm@42913
   248
The context maintains a default set of theorems that are used
wenzelm@42913
   249
  in monotonicity proofs.  New rules can be declared via the
wenzelm@42913
   250
  \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute.  See the main Isabelle/HOL
wenzelm@42913
   251
  sources for some examples.  The general format of such monotonicity
wenzelm@42913
   252
  theorems is as follows:
wenzelm@26849
   253
wenzelm@42908
   254
  \begin{itemize}
wenzelm@26849
   255
wenzelm@42913
   256
  \item Theorems of the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ B{\isaliteral{22}{\isachardoublequote}}}, for proving
wenzelm@42908
   257
  monotonicity of inductive definitions whose introduction rules have
wenzelm@42913
   258
  premises involving terms such as \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4D3E}{\isasymM}}\ R\ t{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@26849
   259
wenzelm@42908
   260
  \item Monotonicity theorems for logical operators, which are of the
wenzelm@42908
   261
  general form \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}.  For example, in
wenzelm@42908
   262
  the case of the operator \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, the corresponding theorem is
wenzelm@42908
   263
  \[
wenzelm@42908
   264
  \infer{\isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}}
wenzelm@42908
   265
  \]
haftmann@41396
   266
wenzelm@42908
   267
  \item De Morgan style equations for reasoning about the ``polarity''
wenzelm@42908
   268
  of expressions, e.g.
wenzelm@42908
   269
  \[
wenzelm@42908
   270
  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ P{\isaliteral{22}{\isachardoublequote}}} \qquad\qquad
wenzelm@42908
   271
  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ Q{\isaliteral{22}{\isachardoublequote}}}
wenzelm@42908
   272
  \]
haftmann@41396
   273
wenzelm@42908
   274
  \item Equations for reducing complex operators to more primitive
wenzelm@42908
   275
  ones whose monotonicity can easily be proved, e.g.
wenzelm@42908
   276
  \[
wenzelm@42908
   277
  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}} \qquad\qquad
wenzelm@42908
   278
  \isa{{\isaliteral{22}{\isachardoublequote}}Ball\ A\ P\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequote}}}
wenzelm@42908
   279
  \]
haftmann@41396
   280
wenzelm@42913
   281
  \end{itemize}%
wenzelm@42913
   282
\end{isamarkuptext}%
wenzelm@42913
   283
\isamarkuptrue%
wenzelm@42913
   284
%
wenzelm@42913
   285
\isamarkupsubsubsection{Examples%
wenzelm@42913
   286
}
wenzelm@42913
   287
\isamarkuptrue%
wenzelm@42913
   288
%
wenzelm@42913
   289
\begin{isamarkuptext}%
wenzelm@42913
   290
The finite powerset operator can be defined inductively like this:%
wenzelm@42913
   291
\end{isamarkuptext}%
wenzelm@42913
   292
\isamarkuptrue%
wenzelm@42913
   293
\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
wenzelm@42913
   294
\ Fin\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{for}\ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42913
   295
\isakeyword{where}\isanewline
wenzelm@42913
   296
\ \ empty{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Fin\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42913
   297
{\isaliteral{7C}{\isacharbar}}\ insert{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Fin\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ insert\ a\ B\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Fin\ A{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@42913
   298
\begin{isamarkuptext}%
wenzelm@42913
   299
The accessible part of a relation is defined as follows:%
wenzelm@42913
   300
\end{isamarkuptext}%
wenzelm@42913
   301
\isamarkuptrue%
wenzelm@42913
   302
\isacommand{inductive}\isamarkupfalse%
wenzelm@42913
   303
\ acc\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42913
   304
\ \ \isakeyword{for}\ r\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C707265633E}{\isasymprec}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@42913
   305
\isakeyword{where}\ acc{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}y{\isaliteral{2E}{\isachardot}}\ y\ {\isaliteral{5C3C707265633E}{\isasymprec}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ acc\ r\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ acc\ r\ x{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@42913
   306
\begin{isamarkuptext}%
wenzelm@42913
   307
Common logical connectives can be easily characterized as
wenzelm@42913
   308
non-recursive inductive definitions with parameters, but without
wenzelm@42913
   309
arguments.%
wenzelm@42913
   310
\end{isamarkuptext}%
wenzelm@42913
   311
\isamarkuptrue%
wenzelm@42913
   312
\isacommand{inductive}\isamarkupfalse%
wenzelm@42913
   313
\ AND\ \isakeyword{for}\ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\isanewline
wenzelm@42913
   314
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ AND\ A\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42913
   315
\isanewline
wenzelm@42913
   316
\isacommand{inductive}\isamarkupfalse%
wenzelm@42913
   317
\ OR\ \isakeyword{for}\ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\isanewline
wenzelm@42913
   318
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ OR\ A\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42913
   319
\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ OR\ A\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42913
   320
\isanewline
wenzelm@42913
   321
\isacommand{inductive}\isamarkupfalse%
wenzelm@42913
   322
\ EXISTS\ \isakeyword{for}\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42913
   323
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ EXISTS\ B{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@42913
   324
\begin{isamarkuptext}%
wenzelm@42913
   325
Here the \isa{{\isaliteral{22}{\isachardoublequote}}cases{\isaliteral{22}{\isachardoublequote}}} or \isa{{\isaliteral{22}{\isachardoublequote}}induct{\isaliteral{22}{\isachardoublequote}}} rules produced by
wenzelm@42913
   326
  the \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} package coincide with the expected
wenzelm@42913
   327
  elimination rules for Natural Deduction.  Already in the original
wenzelm@42913
   328
  article by Gerhard Gentzen \cite{Gentzen:1935} there is a hint that
wenzelm@42913
   329
  each connective can be characterized by its introductions, and the
wenzelm@42913
   330
  elimination can be constructed systematically.%
haftmann@41396
   331
\end{isamarkuptext}%
haftmann@41396
   332
\isamarkuptrue%
haftmann@41396
   333
%
wenzelm@26849
   334
\isamarkupsection{Recursive functions \label{sec:recursion}%
wenzelm@26849
   335
}
wenzelm@26849
   336
\isamarkuptrue%
wenzelm@26849
   337
%
wenzelm@26849
   338
\begin{isamarkuptext}%
wenzelm@26849
   339
\begin{matharray}{rcl}
wenzelm@40406
   340
    \indexdef{HOL}{command}{primrec}\hypertarget{command.HOL.primrec}{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40406
   341
    \indexdef{HOL}{command}{fun}\hypertarget{command.HOL.fun}{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40406
   342
    \indexdef{HOL}{command}{function}\hypertarget{command.HOL.function}{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40406
   343
    \indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@26849
   344
  \end{matharray}
wenzelm@26849
   345
wenzelm@42596
   346
  \begin{railoutput}
wenzelm@42662
   347
\rail@begin{2}{}
wenzelm@42596
   348
\rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
wenzelm@42596
   349
\rail@bar
wenzelm@42596
   350
\rail@nextbar{1}
wenzelm@42596
   351
\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
wenzelm@42596
   352
\rail@endbar
wenzelm@42596
   353
\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
wenzelm@42596
   354
\rail@term{\isa{\isakeyword{where}}}[]
wenzelm@42596
   355
\rail@nont{\isa{equations}}[]
wenzelm@42596
   356
\rail@end
wenzelm@42662
   357
\rail@begin{4}{}
wenzelm@42596
   358
\rail@bar
wenzelm@42596
   359
\rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
wenzelm@42596
   360
\rail@nextbar{1}
wenzelm@42596
   361
\rail@term{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}}[]
wenzelm@42596
   362
\rail@endbar
wenzelm@42596
   363
\rail@bar
wenzelm@42596
   364
\rail@nextbar{1}
wenzelm@42596
   365
\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
wenzelm@42596
   366
\rail@endbar
wenzelm@42596
   367
\rail@bar
wenzelm@42596
   368
\rail@nextbar{1}
wenzelm@42596
   369
\rail@nont{\isa{functionopts}}[]
wenzelm@42596
   370
\rail@endbar
wenzelm@42596
   371
\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
wenzelm@42596
   372
\rail@cr{3}
wenzelm@42596
   373
\rail@term{\isa{\isakeyword{where}}}[]
wenzelm@42596
   374
\rail@nont{\isa{equations}}[]
wenzelm@42596
   375
\rail@end
wenzelm@42596
   376
\rail@begin{3}{\isa{equations}}
wenzelm@42596
   377
\rail@plus
wenzelm@42596
   378
\rail@bar
wenzelm@42596
   379
\rail@nextbar{1}
wenzelm@42596
   380
\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
wenzelm@42596
   381
\rail@endbar
wenzelm@42596
   382
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
wenzelm@42596
   383
\rail@nextplus{2}
wenzelm@42596
   384
\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
wenzelm@42596
   385
\rail@endplus
wenzelm@42596
   386
\rail@end
wenzelm@42596
   387
\rail@begin{3}{\isa{functionopts}}
wenzelm@42596
   388
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@42596
   389
\rail@plus
wenzelm@42596
   390
\rail@bar
wenzelm@42596
   391
\rail@term{\isa{sequential}}[]
wenzelm@42596
   392
\rail@nextbar{1}
wenzelm@42596
   393
\rail@term{\isa{domintros}}[]
wenzelm@42596
   394
\rail@endbar
wenzelm@42596
   395
\rail@nextplus{2}
wenzelm@42596
   396
\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
wenzelm@42596
   397
\rail@endplus
wenzelm@42596
   398
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@42596
   399
\rail@end
wenzelm@42662
   400
\rail@begin{2}{}
wenzelm@42596
   401
\rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
wenzelm@42596
   402
\rail@bar
wenzelm@42596
   403
\rail@nextbar{1}
wenzelm@42596
   404
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
wenzelm@42596
   405
\rail@endbar
wenzelm@42596
   406
\rail@end
wenzelm@42596
   407
\end{railoutput}
wenzelm@42596
   408
wenzelm@26849
   409
wenzelm@28788
   410
  \begin{description}
wenzelm@26849
   411
wenzelm@28788
   412
  \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
wenzelm@42912
   413
  functions over datatypes (see also \indexref{HOL}{command}{datatype}\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} and
wenzelm@42912
   414
  \indexref{HOL}{command}{rep\_datatype}\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}).  The given \isa{equations}
wenzelm@42912
   415
  specify reduction rules that are produced by instantiating the
wenzelm@42912
   416
  generic combinator for primitive recursion that is available for
wenzelm@42912
   417
  each datatype.
wenzelm@42912
   418
wenzelm@42912
   419
  Each equation needs to be of the form:
wenzelm@42912
   420
wenzelm@42912
   421
  \begin{isabelle}%
wenzelm@42912
   422
{\isaliteral{22}{\isachardoublequote}}f\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{28}{\isacharparenleft}}C\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{29}{\isacharparenright}}\ z\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ z\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3D}{\isacharequal}}\ rhs{\isaliteral{22}{\isachardoublequote}}%
wenzelm@42912
   423
\end{isabelle}
wenzelm@42912
   424
wenzelm@42912
   425
  such that \isa{C} is a datatype constructor, \isa{rhs} contains
wenzelm@42912
   426
  only the free variables on the left-hand side (or from the context),
wenzelm@42912
   427
  and all recursive occurrences of \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} in \isa{{\isaliteral{22}{\isachardoublequote}}rhs{\isaliteral{22}{\isachardoublequote}}} are of
wenzelm@42912
   428
  the form \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} for some \isa{i}.  At most one
wenzelm@42912
   429
  reduction rule for each constructor can be given.  The order does
wenzelm@42912
   430
  not matter.  For missing constructors, the function is defined to
wenzelm@42912
   431
  return a default value, but this equation is made difficult to
wenzelm@42912
   432
  access for users.
wenzelm@42912
   433
wenzelm@42912
   434
  The reduction rules are declared as \hyperlink{attribute.simp}{\mbox{\isa{simp}}} by default,
wenzelm@42912
   435
  which enables standard proof methods like \hyperlink{method.simp}{\mbox{\isa{simp}}} and
wenzelm@42912
   436
  \hyperlink{method.auto}{\mbox{\isa{auto}}} to normalize expressions of \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} applied to
wenzelm@42912
   437
  datatype constructions, by simulating symbolic computation via
wenzelm@42912
   438
  rewriting.
wenzelm@26849
   439
wenzelm@28788
   440
  \item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
wenzelm@26849
   441
  wellfounded recursion. A detailed description with examples can be
wenzelm@26849
   442
  found in \cite{isabelle-function}. The function is specified by a
wenzelm@26849
   443
  set of (possibly conditional) recursive equations with arbitrary
wenzelm@26849
   444
  pattern matching. The command generates proof obligations for the
wenzelm@26849
   445
  completeness and the compatibility of patterns.
wenzelm@26849
   446
wenzelm@26849
   447
  The defined function is considered partial, and the resulting
wenzelm@40406
   448
  simplification rules (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}psimps{\isaliteral{22}{\isachardoublequote}}}) and induction rule
wenzelm@40406
   449
  (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}pinduct{\isaliteral{22}{\isachardoublequote}}}) are guarded by a generated domain
wenzelm@40406
   450
  predicate \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5F}{\isacharunderscore}}dom{\isaliteral{22}{\isachardoublequote}}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}
wenzelm@26849
   451
  command can then be used to establish that the function is total.
wenzelm@26849
   452
wenzelm@40406
   453
  \item \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} is a shorthand notation for ``\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}sequential{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, followed by automated
wenzelm@28788
   454
  proof attempts regarding pattern matching and termination.  See
wenzelm@28788
   455
  \cite{isabelle-function} for further details.
wenzelm@26849
   456
wenzelm@28788
   457
  \item \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f} commences a
wenzelm@26849
   458
  termination proof for the previously defined function \isa{f}.  If
wenzelm@26849
   459
  this is omitted, the command refers to the most recent function
wenzelm@26849
   460
  definition.  After the proof is closed, the recursive equations and
wenzelm@26849
   461
  the induction principle is established.
wenzelm@26849
   462
wenzelm@28788
   463
  \end{description}
wenzelm@26849
   464
haftmann@27452
   465
  Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
wenzelm@42912
   466
  command accommodate reasoning by induction (cf.\ \hyperlink{method.induct}{\mbox{\isa{induct}}}):
wenzelm@42912
   467
  rule \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}induct{\isaliteral{22}{\isachardoublequote}}} refers to a specific induction rule, with
wenzelm@42912
   468
  parameters named according to the user-specified equations. Cases
wenzelm@42912
   469
  are numbered starting from 1.  For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the
wenzelm@42912
   470
  induction principle coincides with structural recursion on the
wenzelm@42912
   471
  datatype where the recursion is carried out.
wenzelm@26849
   472
wenzelm@26849
   473
  The equations provided by these packages may be referred later as
wenzelm@40406
   474
  theorem list \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, where \isa{f} is the (collective)
wenzelm@26849
   475
  name of the functions defined.  Individual equations may be named
wenzelm@26849
   476
  explicitly as well.
wenzelm@26849
   477
wenzelm@26902
   478
  The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following
wenzelm@26849
   479
  options.
wenzelm@26849
   480
wenzelm@28788
   481
  \begin{description}
wenzelm@26849
   482
wenzelm@28788
   483
  \item \isa{sequential} enables a preprocessor which disambiguates
wenzelm@28788
   484
  overlapping patterns by making them mutually disjoint.  Earlier
wenzelm@28788
   485
  equations take precedence over later ones.  This allows to give the
wenzelm@28788
   486
  specification in a format very similar to functional programming.
wenzelm@28788
   487
  Note that the resulting simplification and induction rules
wenzelm@28788
   488
  correspond to the transformed specification, not the one given
wenzelm@26849
   489
  originally. This usually means that each equation given by the user
hoelzl@36139
   490
  may result in several theorems.  Also note that this automatic
wenzelm@26849
   491
  transformation only works for ML-style datatype patterns.
wenzelm@26849
   492
wenzelm@28788
   493
  \item \isa{domintros} enables the automated generation of
wenzelm@26849
   494
  introduction rules for the domain predicate. While mostly not
wenzelm@26849
   495
  needed, they can be helpful in some proofs about partial functions.
wenzelm@26849
   496
wenzelm@28788
   497
  \end{description}%
wenzelm@26849
   498
\end{isamarkuptext}%
wenzelm@26849
   499
\isamarkuptrue%
wenzelm@26849
   500
%
wenzelm@42912
   501
\isamarkupsubsubsection{Example: evaluation of expressions%
wenzelm@42912
   502
}
wenzelm@42912
   503
\isamarkuptrue%
wenzelm@42912
   504
%
wenzelm@42912
   505
\begin{isamarkuptext}%
wenzelm@42912
   506
Subsequently, we define mutual datatypes for arithmetic and
wenzelm@42912
   507
  boolean expressions, and use \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} for evaluation
wenzelm@42912
   508
  functions that follow the same recursive structure.%
wenzelm@42912
   509
\end{isamarkuptext}%
wenzelm@42912
   510
\isamarkuptrue%
wenzelm@42912
   511
\isacommand{datatype}\isamarkupfalse%
wenzelm@42912
   512
\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{3D}{\isacharequal}}\isanewline
wenzelm@42912
   513
\ \ \ \ IF\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   514
\ \ {\isaliteral{7C}{\isacharbar}}\ Sum\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   515
\ \ {\isaliteral{7C}{\isacharbar}}\ Diff\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   516
\ \ {\isaliteral{7C}{\isacharbar}}\ Var\ {\isaliteral{27}{\isacharprime}}a\isanewline
wenzelm@42912
   517
\ \ {\isaliteral{7C}{\isacharbar}}\ Num\ nat\isanewline
wenzelm@42912
   518
\isakeyword{and}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{3D}{\isacharequal}}\isanewline
wenzelm@42912
   519
\ \ \ \ Less\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   520
\ \ {\isaliteral{7C}{\isacharbar}}\ And\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   521
\ \ {\isaliteral{7C}{\isacharbar}}\ Neg\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@42912
   522
\begin{isamarkuptext}%
wenzelm@42912
   523
\medskip Evaluation of arithmetic and boolean expressions%
wenzelm@42912
   524
\end{isamarkuptext}%
wenzelm@42912
   525
\isamarkuptrue%
wenzelm@42912
   526
\isacommand{primrec}\isamarkupfalse%
wenzelm@42912
   527
\ evala\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   528
\ \ \isakeyword{and}\ evalb\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   529
\isakeyword{where}\isanewline
wenzelm@42912
   530
\ \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ evalb\ env\ b\ then\ evala\ env\ a{\isadigit{1}}\ else\ evala\ env\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   531
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ evala\ env\ a{\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   532
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isadigit{1}}\ {\isaliteral{2D}{\isacharminus}}\ evala\ env\ a{\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   533
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Var\ v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ env\ v{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   534
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   535
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}evala\ env\ a{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ evala\ env\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   536
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}evalb\ env\ b{\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ evalb\ env\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   537
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ evalb\ env\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@42912
   538
\begin{isamarkuptext}%
wenzelm@42912
   539
Since the value of an expression depends on the value of its
wenzelm@42912
   540
  variables, the functions \isa{evala} and \isa{evalb} take an
wenzelm@42912
   541
  additional parameter, an \emph{environment} that maps variables to
wenzelm@42912
   542
  their values.
wenzelm@42912
   543
wenzelm@42912
   544
  \medskip Substitution on expressions can be defined similarly.  The
wenzelm@42912
   545
  mapping \isa{f} of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequote}}} given as a
wenzelm@42912
   546
  parameter is lifted canonically on the types \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequote}}} and
wenzelm@42912
   547
  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequote}}}, respectively.%
wenzelm@42912
   548
\end{isamarkuptext}%
wenzelm@42912
   549
\isamarkuptrue%
wenzelm@42912
   550
\isacommand{primrec}\isamarkupfalse%
wenzelm@42912
   551
\ substa\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   552
\ \ \isakeyword{and}\ substb\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   553
\isakeyword{where}\isanewline
wenzelm@42912
   554
\ \ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   555
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Sum\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   556
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Diff\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   557
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Var\ v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ v{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   558
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Num\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   559
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substb\ f\ {\isaliteral{28}{\isacharparenleft}}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Less\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   560
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substb\ f\ {\isaliteral{28}{\isacharparenleft}}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ And\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   561
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substb\ f\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Neg\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@42912
   562
\begin{isamarkuptext}%
wenzelm@42912
   563
In textbooks about semantics one often finds substitution
wenzelm@42912
   564
  theorems, which express the relationship between substitution and
wenzelm@42912
   565
  evaluation.  For \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequote}}}, we can prove
wenzelm@42912
   566
  such a theorem by mutual induction, followed by simplification.%
wenzelm@42912
   567
\end{isamarkuptext}%
wenzelm@42912
   568
\isamarkuptrue%
wenzelm@42912
   569
\isacommand{lemma}\isamarkupfalse%
wenzelm@42912
   570
\ subst{\isaliteral{5F}{\isacharunderscore}}one{\isaliteral{3A}{\isacharcolon}}\isanewline
wenzelm@42912
   571
\ \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}substa\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ {\isaliteral{28}{\isacharparenleft}}env\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   572
\ \ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}substb\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evalb\ {\isaliteral{28}{\isacharparenleft}}env\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   573
%
wenzelm@42912
   574
\isadelimproof
wenzelm@42912
   575
\ \ %
wenzelm@42912
   576
\endisadelimproof
wenzelm@42912
   577
%
wenzelm@42912
   578
\isatagproof
wenzelm@42912
   579
\isacommand{by}\isamarkupfalse%
wenzelm@42912
   580
\ {\isaliteral{28}{\isacharparenleft}}induct\ a\ \isakeyword{and}\ b{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
wenzelm@42912
   581
\endisatagproof
wenzelm@42912
   582
{\isafoldproof}%
wenzelm@42912
   583
%
wenzelm@42912
   584
\isadelimproof
wenzelm@42912
   585
\isanewline
wenzelm@42912
   586
%
wenzelm@42912
   587
\endisadelimproof
wenzelm@42912
   588
\isanewline
wenzelm@42912
   589
\isacommand{lemma}\isamarkupfalse%
wenzelm@42912
   590
\ subst{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{3A}{\isacharcolon}}\isanewline
wenzelm@42912
   591
\ \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ evala\ env\ {\isaliteral{28}{\isacharparenleft}}s\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   592
\ \ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evalb\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ evala\ env\ {\isaliteral{28}{\isacharparenleft}}s\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   593
%
wenzelm@42912
   594
\isadelimproof
wenzelm@42912
   595
\ \ %
wenzelm@42912
   596
\endisadelimproof
wenzelm@42912
   597
%
wenzelm@42912
   598
\isatagproof
wenzelm@42912
   599
\isacommand{by}\isamarkupfalse%
wenzelm@42912
   600
\ {\isaliteral{28}{\isacharparenleft}}induct\ a\ \isakeyword{and}\ b{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
wenzelm@42912
   601
\endisatagproof
wenzelm@42912
   602
{\isafoldproof}%
wenzelm@42912
   603
%
wenzelm@42912
   604
\isadelimproof
wenzelm@42912
   605
%
wenzelm@42912
   606
\endisadelimproof
wenzelm@42912
   607
%
wenzelm@42912
   608
\isamarkupsubsubsection{Example: a substitution function for terms%
wenzelm@42912
   609
}
wenzelm@42912
   610
\isamarkuptrue%
wenzelm@42912
   611
%
wenzelm@42912
   612
\begin{isamarkuptext}%
wenzelm@42912
   613
Functions on datatypes with nested recursion are also defined
wenzelm@42912
   614
  by mutual primitive recursion.%
wenzelm@42912
   615
\end{isamarkuptext}%
wenzelm@42912
   616
\isamarkuptrue%
wenzelm@42912
   617
\isacommand{datatype}\isamarkupfalse%
wenzelm@42912
   618
\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequoteopen}}term{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{7C}{\isacharbar}}\ App\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@42912
   619
\begin{isamarkuptext}%
wenzelm@42912
   620
A substitution function on type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{22}{\isachardoublequote}}} can be
wenzelm@42912
   621
  defined as follows, by working simultaneously on \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list{\isaliteral{22}{\isachardoublequote}}}:%
wenzelm@42912
   622
\end{isamarkuptext}%
wenzelm@42912
   623
\isamarkuptrue%
wenzelm@42912
   624
\isacommand{primrec}\isamarkupfalse%
wenzelm@42912
   625
\ subst{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
wenzelm@42912
   626
\ \ subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   627
\isakeyword{where}\isanewline
wenzelm@42912
   628
\ \ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f\ {\isaliteral{28}{\isacharparenleft}}Var\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   629
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f\ {\isaliteral{28}{\isacharparenleft}}App\ b\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ b\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   630
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   631
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{23}{\isacharhash}}\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ subst{\isaliteral{5F}{\isacharunderscore}}term\ f\ t\ {\isaliteral{23}{\isacharhash}}\ subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ ts{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@42912
   632
\begin{isamarkuptext}%
wenzelm@42912
   633
The recursion scheme follows the structure of the unfolded
wenzelm@42912
   634
  definition of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{22}{\isachardoublequote}}}.  To prove properties of this
wenzelm@42912
   635
  substitution function, mutual induction is needed:%
wenzelm@42912
   636
\end{isamarkuptext}%
wenzelm@42912
   637
\isamarkuptrue%
wenzelm@42912
   638
\isacommand{lemma}\isamarkupfalse%
wenzelm@42912
   639
\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{2}}\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
wenzelm@42912
   640
\ \ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ ts\ {\isaliteral{3D}{\isacharequal}}\ subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f{\isadigit{2}}\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   641
%
wenzelm@42912
   642
\isadelimproof
wenzelm@42912
   643
\ \ %
wenzelm@42912
   644
\endisadelimproof
wenzelm@42912
   645
%
wenzelm@42912
   646
\isatagproof
wenzelm@42912
   647
\isacommand{by}\isamarkupfalse%
wenzelm@42912
   648
\ {\isaliteral{28}{\isacharparenleft}}induct\ t\ \isakeyword{and}\ ts{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
wenzelm@42912
   649
\endisatagproof
wenzelm@42912
   650
{\isafoldproof}%
wenzelm@42912
   651
%
wenzelm@42912
   652
\isadelimproof
wenzelm@42912
   653
%
wenzelm@42912
   654
\endisadelimproof
wenzelm@42912
   655
%
wenzelm@42912
   656
\isamarkupsubsubsection{Example: a map function for infinitely branching trees%
wenzelm@42912
   657
}
wenzelm@42912
   658
\isamarkuptrue%
wenzelm@42912
   659
%
wenzelm@42912
   660
\begin{isamarkuptext}%
wenzelm@42912
   661
Defining functions on infinitely branching datatypes by
wenzelm@42912
   662
  primitive recursion is just as easy.%
wenzelm@42912
   663
\end{isamarkuptext}%
wenzelm@42912
   664
\isamarkuptrue%
wenzelm@42912
   665
\isacommand{datatype}\isamarkupfalse%
wenzelm@42912
   666
\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Atom\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{7C}{\isacharbar}}\ Branch\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   667
\isanewline
wenzelm@42912
   668
\isacommand{primrec}\isamarkupfalse%
wenzelm@42912
   669
\ map{\isaliteral{5F}{\isacharunderscore}}tree\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ tree{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   670
\isakeyword{where}\isanewline
wenzelm@42912
   671
\ \ {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{28}{\isacharparenleft}}Atom\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Atom\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   672
{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{28}{\isacharparenleft}}Branch\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Branch\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{28}{\isacharparenleft}}ts\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@42912
   673
\begin{isamarkuptext}%
wenzelm@42912
   674
Note that all occurrences of functions such as \isa{ts}
wenzelm@42912
   675
  above must be applied to an argument.  In particular, \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ ts{\isaliteral{22}{\isachardoublequote}}} is not allowed here.%
wenzelm@42912
   676
\end{isamarkuptext}%
wenzelm@42912
   677
\isamarkuptrue%
wenzelm@42912
   678
%
wenzelm@42912
   679
\begin{isamarkuptext}%
wenzelm@42912
   680
Here is a simple composition lemma for \isa{map{\isaliteral{5F}{\isacharunderscore}}tree}:%
wenzelm@42912
   681
\end{isamarkuptext}%
wenzelm@42912
   682
\isamarkuptrue%
wenzelm@42912
   683
\isacommand{lemma}\isamarkupfalse%
wenzelm@42912
   684
\ {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}tree\ g\ {\isaliteral{28}{\isacharparenleft}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ map{\isaliteral{5F}{\isacharunderscore}}tree\ {\isaliteral{28}{\isacharparenleft}}g\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42912
   685
%
wenzelm@42912
   686
\isadelimproof
wenzelm@42912
   687
\ \ %
wenzelm@42912
   688
\endisadelimproof
wenzelm@42912
   689
%
wenzelm@42912
   690
\isatagproof
wenzelm@42912
   691
\isacommand{by}\isamarkupfalse%
wenzelm@42912
   692
\ {\isaliteral{28}{\isacharparenleft}}induct\ t{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
wenzelm@42912
   693
\endisatagproof
wenzelm@42912
   694
{\isafoldproof}%
wenzelm@42912
   695
%
wenzelm@42912
   696
\isadelimproof
wenzelm@42912
   697
%
wenzelm@42912
   698
\endisadelimproof
wenzelm@42912
   699
%
wenzelm@26849
   700
\isamarkupsubsection{Proof methods related to recursive definitions%
wenzelm@26849
   701
}
wenzelm@26849
   702
\isamarkuptrue%
wenzelm@26849
   703
%
wenzelm@26849
   704
\begin{isamarkuptext}%
wenzelm@26849
   705
\begin{matharray}{rcl}
wenzelm@40406
   706
    \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}}} & : & \isa{method} \\
wenzelm@28788
   707
    \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
wenzelm@40406
   708
    \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}} & : & \isa{method} \\
wenzelm@40406
   709
    \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}} & : & \isa{method} \\
bulwahn@45944
   710
    \indexdef{HOL}{method}{induction\_schema}\hypertarget{method.HOL.induction-schema}{\hyperlink{method.HOL.induction-schema}{\mbox{\isa{induction{\isaliteral{5F}{\isacharunderscore}}schema}}}} & : & \isa{method} \\
wenzelm@26849
   711
  \end{matharray}
wenzelm@26849
   712
wenzelm@42596
   713
  \begin{railoutput}
wenzelm@42662
   714
\rail@begin{1}{}
wenzelm@42596
   715
\rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
wenzelm@42596
   716
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
wenzelm@42596
   717
\rail@end
wenzelm@42662
   718
\rail@begin{2}{}
wenzelm@42596
   719
\rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
wenzelm@42596
   720
\rail@plus
wenzelm@42596
   721
\rail@nextplus{1}
wenzelm@42596
   722
\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
wenzelm@42596
   723
\rail@endplus
wenzelm@42596
   724
\rail@end
wenzelm@42662
   725
\rail@begin{2}{}
wenzelm@42596
   726
\rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
wenzelm@42596
   727
\rail@nont{\isa{orders}}[]
wenzelm@42596
   728
\rail@plus
wenzelm@42596
   729
\rail@nextplus{1}
wenzelm@42596
   730
\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
wenzelm@42596
   731
\rail@endplus
wenzelm@42596
   732
\rail@end
bulwahn@45944
   733
\rail@begin{1}{}
bulwahn@45944
   734
\rail@term{\hyperlink{method.HOL.induction-schema}{\mbox{\isa{induction{\isaliteral{5F}{\isacharunderscore}}schema}}}}[]
bulwahn@45944
   735
\rail@end
wenzelm@42596
   736
\rail@begin{4}{\isa{orders}}
wenzelm@42596
   737
\rail@plus
wenzelm@42596
   738
\rail@nextplus{1}
wenzelm@42596
   739
\rail@bar
wenzelm@42596
   740
\rail@term{\isa{max}}[]
wenzelm@42596
   741
\rail@nextbar{2}
wenzelm@42596
   742
\rail@term{\isa{min}}[]
wenzelm@42596
   743
\rail@nextbar{3}
wenzelm@42596
   744
\rail@term{\isa{ms}}[]
wenzelm@42596
   745
\rail@endbar
wenzelm@42596
   746
\rail@endplus
wenzelm@42596
   747
\rail@end
wenzelm@42596
   748
\end{railoutput}
wenzelm@42596
   749
wenzelm@26849
   750
wenzelm@28788
   751
  \begin{description}
wenzelm@26849
   752
wenzelm@40406
   753
  \item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}} is a specialized method to
wenzelm@26849
   754
  solve goals regarding the completeness of pattern matching, as
wenzelm@26902
   755
  required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
wenzelm@26849
   756
  \cite{isabelle-function}).
wenzelm@26849
   757
wenzelm@28788
   758
  \item \hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R} introduces a termination
wenzelm@26849
   759
  proof using the relation \isa{R}.  The resulting proof state will
wenzelm@26849
   760
  contain goals expressing that \isa{R} is wellfounded, and that the
wenzelm@26849
   761
  arguments of recursive calls decrease with respect to \isa{R}.
wenzelm@26849
   762
  Usually, this method is used as the initial proof step of manual
wenzelm@26849
   763
  termination proofs.
wenzelm@26849
   764
wenzelm@40406
   765
  \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}} attempts a fully
wenzelm@26849
   766
  automated termination proof by searching for a lexicographic
wenzelm@26849
   767
  combination of size measures on the arguments of the function. The
wenzelm@26902
   768
  method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
wenzelm@42930
   769
  which it uses internally to prove local descents.  The \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} modifiers are accepted (as for \hyperlink{method.auto}{\mbox{\isa{auto}}}).
wenzelm@26849
   770
wenzelm@26849
   771
  In case of failure, extensive information is printed, which can help
wenzelm@26849
   772
  to analyse the situation (cf.\ \cite{isabelle-function}).
wenzelm@26849
   773
wenzelm@40406
   774
  \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}} also works on termination goals,
krauss@33858
   775
  using a variation of the size-change principle, together with a
krauss@33858
   776
  graph decomposition technique (see \cite{krauss_phd} for details).
krauss@33858
   777
  Three kinds of orders are used internally: \isa{max}, \isa{min},
krauss@33858
   778
  and \isa{ms} (multiset), which is only available when the theory
krauss@33858
   779
  \isa{Multiset} is loaded. When no order kinds are given, they are
krauss@33858
   780
  tried in order. The search for a termination proof uses SAT solving
krauss@33858
   781
  internally.
krauss@33858
   782
wenzelm@42930
   783
  For local descent proofs, the \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} modifiers are
wenzelm@42930
   784
  accepted (as for \hyperlink{method.auto}{\mbox{\isa{auto}}}).
krauss@33858
   785
bulwahn@45944
   786
  \item \hyperlink{method.HOL.induction-schema}{\mbox{\isa{induction{\isaliteral{5F}{\isacharunderscore}}schema}}} derives user-specified
bulwahn@45944
   787
   induction rules from well-founded induction and completeness of
bulwahn@45944
   788
   patterns. This factors out some operations that are done internally
bulwahn@45944
   789
   by the function package and makes them available separately. See
bulwahn@45944
   790
   \verb|~~/src/HOL/ex/Induction_Schema.thy| for examples.
bulwahn@45944
   791
wenzelm@28788
   792
  \end{description}%
wenzelm@26849
   793
\end{isamarkuptext}%
wenzelm@26849
   794
\isamarkuptrue%
wenzelm@26849
   795
%
krauss@40171
   796
\isamarkupsubsection{Functions with explicit partiality%
krauss@40171
   797
}
krauss@40171
   798
\isamarkuptrue%
krauss@40171
   799
%
krauss@40171
   800
\begin{isamarkuptext}%
krauss@40171
   801
\begin{matharray}{rcl}
wenzelm@40406
   802
    \indexdef{HOL}{command}{partial\_function}\hypertarget{command.HOL.partial-function}{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40406
   803
    \indexdef{HOL}{attribute}{partial\_function\_mono}\hypertarget{attribute.HOL.partial-function-mono}{\hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}}} & : & \isa{attribute} \\
krauss@40171
   804
  \end{matharray}
krauss@40171
   805
wenzelm@42596
   806
  \begin{railoutput}
wenzelm@42662
   807
\rail@begin{5}{}
wenzelm@42596
   808
\rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
wenzelm@42596
   809
\rail@bar
wenzelm@42596
   810
\rail@nextbar{1}
wenzelm@42596
   811
\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
wenzelm@42596
   812
\rail@endbar
wenzelm@42596
   813
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@42617
   814
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@42596
   815
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@42596
   816
\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
wenzelm@42596
   817
\rail@cr{3}
wenzelm@42596
   818
\rail@term{\isa{\isakeyword{where}}}[]
wenzelm@42596
   819
\rail@bar
wenzelm@42596
   820
\rail@nextbar{4}
wenzelm@42596
   821
\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
wenzelm@42596
   822
\rail@endbar
wenzelm@42596
   823
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
wenzelm@42596
   824
\rail@end
wenzelm@42596
   825
\end{railoutput}
wenzelm@42617
   826
krauss@40171
   827
krauss@40171
   828
  \begin{description}
krauss@40171
   829
wenzelm@42617
   830
  \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} defines
wenzelm@42617
   831
  recursive functions based on fixpoints in complete partial
wenzelm@42617
   832
  orders. No termination proof is required from the user or
wenzelm@42617
   833
  constructed internally. Instead, the possibility of non-termination
wenzelm@42617
   834
  is modelled explicitly in the result type, which contains an
wenzelm@42617
   835
  explicit bottom element.
krauss@40171
   836
krauss@40171
   837
  Pattern matching and mutual recursion are currently not supported.
krauss@40171
   838
  Thus, the specification consists of a single function described by a
krauss@40171
   839
  single recursive equation.
krauss@40171
   840
krauss@40171
   841
  There are no fixed syntactic restrictions on the body of the
krauss@40171
   842
  function, but the induced functional must be provably monotonic
krauss@40171
   843
  wrt.\ the underlying order.  The monotonicitity proof is performed
krauss@40171
   844
  internally, and the definition is rejected when it fails. The proof
krauss@40171
   845
  can be influenced by declaring hints using the
wenzelm@40406
   846
  \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} attribute.
krauss@40171
   847
krauss@40171
   848
  The mandatory \isa{mode} argument specifies the mode of operation
krauss@40171
   849
  of the command, which directly corresponds to a complete partial
krauss@40171
   850
  order on the result type. By default, the following modes are
wenzelm@42123
   851
  defined:
krauss@40171
   852
krauss@40171
   853
  \begin{description}
krauss@40171
   854
  \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
krauss@40171
   855
  non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
krauss@40171
   856
  must also be \isa{None}. This is best achieved through the use of
wenzelm@40406
   857
  the monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@42123
   858
krauss@40171
   859
  \item \isa{tailrec} defines functions with an arbitrary result
wenzelm@40406
   860
  type and uses the slightly degenerated partial order where \isa{{\isaliteral{22}{\isachardoublequote}}undefined{\isaliteral{22}{\isachardoublequote}}} is the bottom element.  Now, monotonicity requires that
krauss@40171
   861
  if \isa{undefined} is returned by a recursive call, then the
krauss@40171
   862
  overall result must also be \isa{undefined}. In practice, this is
krauss@40171
   863
  only satisfied when each recursive call is a tail call, whose result
krauss@40171
   864
  is directly returned. Thus, this mode of operation allows the
krauss@40171
   865
  definition of arbitrary tail-recursive functions.
krauss@40171
   866
  \end{description}
krauss@40171
   867
krauss@40171
   868
  Experienced users may define new modes by instantiating the locale
wenzelm@40406
   869
  \isa{{\isaliteral{22}{\isachardoublequote}}partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}definitions{\isaliteral{22}{\isachardoublequote}}} appropriately.
krauss@40171
   870
wenzelm@40406
   871
  \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} declares rules for
krauss@40171
   872
  use in the internal monononicity proofs of partial function
krauss@40171
   873
  definitions.
krauss@40171
   874
krauss@40171
   875
  \end{description}%
krauss@40171
   876
\end{isamarkuptext}%
krauss@40171
   877
\isamarkuptrue%
krauss@40171
   878
%
wenzelm@26849
   879
\isamarkupsubsection{Old-style recursive function definitions (TFL)%
wenzelm@26849
   880
}
wenzelm@26849
   881
\isamarkuptrue%
wenzelm@26849
   882
%
wenzelm@26849
   883
\begin{isamarkuptext}%
wenzelm@40406
   884
The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}} for defining recursive are mostly obsolete; \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} or \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} should be used instead.
wenzelm@26849
   885
wenzelm@26849
   886
  \begin{matharray}{rcl}
wenzelm@40406
   887
    \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40406
   888
    \indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@26849
   889
  \end{matharray}
wenzelm@26849
   890
wenzelm@42596
   891
  \begin{railoutput}
wenzelm@42662
   892
\rail@begin{5}{}
wenzelm@42596
   893
\rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
wenzelm@42596
   894
\rail@bar
wenzelm@42596
   895
\rail@nextbar{1}
wenzelm@42596
   896
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@42596
   897
\rail@term{\isa{\isakeyword{permissive}}}[]
wenzelm@42596
   898
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@42596
   899
\rail@endbar
wenzelm@42596
   900
\rail@cr{3}
wenzelm@42596
   901
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@42596
   902
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
wenzelm@42596
   903
\rail@plus
wenzelm@42596
   904
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
wenzelm@42596
   905
\rail@nextplus{4}
wenzelm@42596
   906
\rail@endplus
wenzelm@42596
   907
\rail@bar
wenzelm@42596
   908
\rail@nextbar{4}
wenzelm@42596
   909
\rail@nont{\isa{hints}}[]
wenzelm@42596
   910
\rail@endbar
wenzelm@42596
   911
\rail@end
wenzelm@42662
   912
\rail@begin{2}{}
wenzelm@42596
   913
\rail@nont{\isa{recdeftc}}[]
wenzelm@42596
   914
\rail@bar
wenzelm@42596
   915
\rail@nextbar{1}
wenzelm@42596
   916
\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
wenzelm@42596
   917
\rail@endbar
wenzelm@42596
   918
\rail@nont{\isa{tc}}[]
wenzelm@42596
   919
\rail@end
wenzelm@42596
   920
\rail@begin{2}{\isa{hints}}
wenzelm@42596
   921
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@42596
   922
\rail@term{\isa{\isakeyword{hints}}}[]
wenzelm@42596
   923
\rail@plus
wenzelm@42596
   924
\rail@nextplus{1}
wenzelm@42596
   925
\rail@cnont{\isa{recdefmod}}[]
wenzelm@42596
   926
\rail@endplus
wenzelm@42596
   927
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@42596
   928
\rail@end
wenzelm@42596
   929
\rail@begin{4}{\isa{recdefmod}}
wenzelm@42596
   930
\rail@bar
wenzelm@42596
   931
\rail@bar
wenzelm@42596
   932
\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}[]
wenzelm@42596
   933
\rail@nextbar{1}
wenzelm@42596
   934
\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}[]
wenzelm@42596
   935
\rail@nextbar{2}
wenzelm@42596
   936
\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}[]
wenzelm@42596
   937
\rail@endbar
wenzelm@42596
   938
\rail@bar
wenzelm@42596
   939
\rail@nextbar{1}
wenzelm@42596
   940
\rail@term{\isa{add}}[]
wenzelm@42596
   941
\rail@nextbar{2}
wenzelm@42596
   942
\rail@term{\isa{del}}[]
wenzelm@42596
   943
\rail@endbar
wenzelm@42596
   944
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
wenzelm@42596
   945
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
wenzelm@42596
   946
\rail@nextbar{3}
wenzelm@42596
   947
\rail@nont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
wenzelm@42596
   948
\rail@endbar
wenzelm@42596
   949
\rail@end
wenzelm@42596
   950
\rail@begin{2}{\isa{tc}}
wenzelm@42596
   951
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@42596
   952
\rail@bar
wenzelm@42596
   953
\rail@nextbar{1}
wenzelm@42596
   954
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@42596
   955
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
wenzelm@42596
   956
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@42596
   957
\rail@endbar
wenzelm@42596
   958
\rail@end
wenzelm@42596
   959
\end{railoutput}
wenzelm@42596
   960
wenzelm@26849
   961
wenzelm@28788
   962
  \begin{description}
wenzelm@42123
   963
wenzelm@28788
   964
  \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
wenzelm@26849
   965
  recursive functions (using the TFL package), see also
wenzelm@40406
   966
  \cite{isabelle-HOL}.  The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells
wenzelm@26849
   967
  TFL to recover from failed proof attempts, returning unfinished
wenzelm@40406
   968
  results.  The \isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}, \isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}, and \isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf} hints refer to auxiliary rules to be used in the internal
wenzelm@26902
   969
  automated proof process of TFL.  Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}
wenzelm@42930
   970
  declarations may be given to tune the context of the Simplifier
wenzelm@42930
   971
  (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\
wenzelm@42930
   972
  \secref{sec:classical}).
wenzelm@42123
   973
wenzelm@40406
   974
  \item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} recommences the
wenzelm@26849
   975
  proof for leftover termination condition number \isa{i} (default
wenzelm@26902
   976
  1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
wenzelm@26849
   977
  constant \isa{c}.
wenzelm@42123
   978
wenzelm@26902
   979
  Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
wenzelm@26849
   980
  its internal proofs without manual intervention.
wenzelm@26849
   981
wenzelm@28788
   982
  \end{description}
wenzelm@26849
   983
wenzelm@26902
   984
  \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared
wenzelm@26849
   985
  globally, using the following attributes.
wenzelm@26849
   986
wenzelm@26849
   987
  \begin{matharray}{rcl}
wenzelm@40406
   988
    \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}} & : & \isa{attribute} \\
wenzelm@40406
   989
    \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}} & : & \isa{attribute} \\
wenzelm@40406
   990
    \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}} & : & \isa{attribute} \\
wenzelm@26849
   991
  \end{matharray}
wenzelm@26849
   992
wenzelm@42596
   993
  \begin{railoutput}
wenzelm@42662
   994
\rail@begin{3}{}
wenzelm@42596
   995
\rail@bar
wenzelm@42596
   996
\rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
wenzelm@42596
   997
\rail@nextbar{1}
wenzelm@42596
   998
\rail@term{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}}[]
wenzelm@42596
   999
\rail@nextbar{2}
wenzelm@42596
  1000
\rail@term{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}}[]
wenzelm@42596
  1001
\rail@endbar
wenzelm@42596
  1002
\rail@bar
wenzelm@42596
  1003
\rail@nextbar{1}
wenzelm@42596
  1004
\rail@term{\isa{add}}[]
wenzelm@42596
  1005
\rail@nextbar{2}
wenzelm@42596
  1006
\rail@term{\isa{del}}[]
wenzelm@42596
  1007
\rail@endbar
wenzelm@42596
  1008
\rail@end
wenzelm@42596
  1009
\end{railoutput}%
wenzelm@26849
  1010
\end{isamarkuptext}%
wenzelm@26849
  1011
\isamarkuptrue%
wenzelm@26849
  1012
%
wenzelm@42908
  1013
\isamarkupsection{Datatypes \label{sec:hol-datatype}%
wenzelm@26849
  1014
}
wenzelm@26849
  1015
\isamarkuptrue%
wenzelm@26849
  1016
%
wenzelm@26849
  1017
\begin{isamarkuptext}%
wenzelm@42908
  1018
\begin{matharray}{rcl}
wenzelm@42908
  1019
    \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1020
    \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@26849
  1021
  \end{matharray}
wenzelm@26849
  1022
wenzelm@42596
  1023
  \begin{railoutput}
wenzelm@42908
  1024
\rail@begin{2}{}
wenzelm@42908
  1025
\rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
wenzelm@42908
  1026
\rail@plus
wenzelm@42908
  1027
\rail@nont{\isa{spec}}[]
wenzelm@42908
  1028
\rail@nextplus{1}
wenzelm@42908
  1029
\rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@42908
  1030
\rail@endplus
wenzelm@42908
  1031
\rail@end
wenzelm@42908
  1032
\rail@begin{3}{}
wenzelm@42908
  1033
\rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
wenzelm@42596
  1034
\rail@bar
wenzelm@42596
  1035
\rail@nextbar{1}
wenzelm@42908
  1036
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@42908
  1037
\rail@plus
wenzelm@42908
  1038
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@42908
  1039
\rail@nextplus{2}
wenzelm@42908
  1040
\rail@endplus
wenzelm@42908
  1041
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@42596
  1042
\rail@endbar
wenzelm@42908
  1043
\rail@plus
wenzelm@42908
  1044
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
wenzelm@42908
  1045
\rail@nextplus{1}
wenzelm@42908
  1046
\rail@endplus
wenzelm@42596
  1047
\rail@end
wenzelm@42908
  1048
\rail@begin{2}{\isa{spec}}
wenzelm@45839
  1049
\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
wenzelm@42908
  1050
\rail@bar
wenzelm@42908
  1051
\rail@nextbar{1}
wenzelm@42908
  1052
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
wenzelm@42908
  1053
\rail@endbar
wenzelm@42908
  1054
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
wenzelm@42908
  1055
\rail@plus
wenzelm@42908
  1056
\rail@nont{\isa{cons}}[]
wenzelm@42908
  1057
\rail@nextplus{1}
wenzelm@42596
  1058
\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
wenzelm@42596
  1059
\rail@endplus
wenzelm@42596
  1060
\rail@end
wenzelm@42908
  1061
\rail@begin{2}{\isa{cons}}
wenzelm@42908
  1062
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@42908
  1063
\rail@plus
wenzelm@42908
  1064
\rail@nextplus{1}
wenzelm@42908
  1065
\rail@cnont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
wenzelm@42908
  1066
\rail@endplus
wenzelm@42596
  1067
\rail@bar
wenzelm@42596
  1068
\rail@nextbar{1}
wenzelm@42908
  1069
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
wenzelm@42596
  1070
\rail@endbar
wenzelm@42596
  1071
\rail@end
wenzelm@42596
  1072
\end{railoutput}
wenzelm@42596
  1073
wenzelm@26849
  1074
wenzelm@28788
  1075
  \begin{description}
wenzelm@26849
  1076
wenzelm@42908
  1077
  \item \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} defines inductive datatypes in
wenzelm@42908
  1078
  HOL.
wenzelm@42908
  1079
wenzelm@42908
  1080
  \item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}} represents existing types as
wenzelm@42909
  1081
  datatypes.
wenzelm@42909
  1082
wenzelm@42909
  1083
  For foundational reasons, some basic types such as \isa{nat}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}, \isa{bool} and \isa{unit} are
wenzelm@42909
  1084
  introduced by more primitive means using \indexref{}{command}{typedef}\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}.  To
wenzelm@42909
  1085
  recover the rich infrastructure of \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} (e.g.\ rules
wenzelm@42909
  1086
  for \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} and the primitive recursion
wenzelm@42909
  1087
  combinators), such types may be represented as actual datatypes
wenzelm@42909
  1088
  later.  This is done by specifying the constructors of the desired
wenzelm@42909
  1089
  type, and giving a proof of the induction rule, distinctness and
wenzelm@42909
  1090
  injectivity of constructors.
wenzelm@42909
  1091
wenzelm@42909
  1092
  For example, see \verb|~~/src/HOL/Sum_Type.thy| for the
wenzelm@42909
  1093
  representation of the primitive sum type as fully-featured datatype.
wenzelm@42908
  1094
wenzelm@42908
  1095
  \end{description}
wenzelm@42908
  1096
wenzelm@42909
  1097
  The generated rules for \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.cases}{\mbox{\isa{cases}}} provide
wenzelm@42909
  1098
  case names according to the given constructors, while parameters are
wenzelm@42909
  1099
  named after the types (see also \secref{sec:cases-induct}).
wenzelm@42908
  1100
wenzelm@42908
  1101
  See \cite{isabelle-HOL} for more details on datatypes, but beware of
wenzelm@42908
  1102
  the old-style theory syntax being used there!  Apart from proper
wenzelm@42908
  1103
  proof methods for case-analysis and induction, there are also
wenzelm@42908
  1104
  emulations of ML tactics \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}} available, see \secref{sec:hol-induct-tac}; these admit
wenzelm@42908
  1105
  to refer directly to the internal structure of subgoals (including
wenzelm@42908
  1106
  internally bound parameters).%
wenzelm@42908
  1107
\end{isamarkuptext}%
wenzelm@42908
  1108
\isamarkuptrue%
wenzelm@42908
  1109
%
wenzelm@42910
  1110
\isamarkupsubsubsection{Examples%
wenzelm@42910
  1111
}
wenzelm@42910
  1112
\isamarkuptrue%
wenzelm@42910
  1113
%
wenzelm@42910
  1114
\begin{isamarkuptext}%
wenzelm@42910
  1115
We define a type of finite sequences, with slightly different
wenzelm@42910
  1116
  names than the existing \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequote}}} that is already in \hyperlink{theory.Main}{\mbox{\isa{Main}}}:%
wenzelm@42910
  1117
\end{isamarkuptext}%
wenzelm@42910
  1118
\isamarkuptrue%
wenzelm@42910
  1119
\isacommand{datatype}\isamarkupfalse%
wenzelm@42910
  1120
\ {\isaliteral{27}{\isacharprime}}a\ seq\ {\isaliteral{3D}{\isacharequal}}\ Empty\ {\isaliteral{7C}{\isacharbar}}\ Seq\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ seq{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@42910
  1121
\begin{isamarkuptext}%
wenzelm@42910
  1122
We can now prove some simple lemma by structural induction:%
wenzelm@42910
  1123
\end{isamarkuptext}%
wenzelm@42910
  1124
\isamarkuptrue%
wenzelm@42910
  1125
\isacommand{lemma}\isamarkupfalse%
wenzelm@42910
  1126
\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42910
  1127
%
wenzelm@42910
  1128
\isadelimproof
wenzelm@42910
  1129
%
wenzelm@42910
  1130
\endisadelimproof
wenzelm@42910
  1131
%
wenzelm@42910
  1132
\isatagproof
wenzelm@42910
  1133
\isacommand{proof}\isamarkupfalse%
wenzelm@42910
  1134
\ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@42910
  1135
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@42910
  1136
\ Empty%
wenzelm@42910
  1137
\begin{isamarkuptxt}%
wenzelm@42910
  1138
This case can be proved using the simplifier: the freeness
wenzelm@42910
  1139
    properties of the datatype are already declared as \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rules.%
wenzelm@42910
  1140
\end{isamarkuptxt}%
wenzelm@42910
  1141
\isamarkuptrue%
wenzelm@42910
  1142
\ \ \isacommand{show}\isamarkupfalse%
wenzelm@42910
  1143
\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ Empty\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Empty{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42910
  1144
\ \ \ \ \isacommand{by}\isamarkupfalse%
wenzelm@42910
  1145
\ simp\isanewline
wenzelm@42910
  1146
\isacommand{next}\isamarkupfalse%
wenzelm@42910
  1147
\isanewline
wenzelm@42910
  1148
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@42910
  1149
\ {\isaliteral{28}{\isacharparenleft}}Seq\ y\ ys{\isaliteral{29}{\isacharparenright}}%
wenzelm@42910
  1150
\begin{isamarkuptxt}%
wenzelm@42910
  1151
The step case is proved similarly.%
wenzelm@42910
  1152
\end{isamarkuptxt}%
wenzelm@42910
  1153
\isamarkuptrue%
wenzelm@42910
  1154
\ \ \isacommand{show}\isamarkupfalse%
wenzelm@42910
  1155
\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ {\isaliteral{28}{\isacharparenleft}}Seq\ y\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Seq\ y\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42910
  1156
\ \ \ \ \isacommand{using}\isamarkupfalse%
wenzelm@42910
  1157
\ {\isaliteral{60}{\isacharbackquoteopen}}Seq\ y\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ ys{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@42910
  1158
\ simp\isanewline
wenzelm@42910
  1159
\isacommand{qed}\isamarkupfalse%
wenzelm@42910
  1160
%
wenzelm@42910
  1161
\endisatagproof
wenzelm@42910
  1162
{\isafoldproof}%
wenzelm@42910
  1163
%
wenzelm@42910
  1164
\isadelimproof
wenzelm@42910
  1165
%
wenzelm@42910
  1166
\endisadelimproof
wenzelm@42910
  1167
%
wenzelm@42910
  1168
\begin{isamarkuptext}%
wenzelm@42910
  1169
Here is a more succinct version of the same proof:%
wenzelm@42910
  1170
\end{isamarkuptext}%
wenzelm@42910
  1171
\isamarkuptrue%
wenzelm@42910
  1172
\isacommand{lemma}\isamarkupfalse%
wenzelm@42910
  1173
\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42910
  1174
%
wenzelm@42910
  1175
\isadelimproof
wenzelm@42910
  1176
\ \ %
wenzelm@42910
  1177
\endisadelimproof
wenzelm@42910
  1178
%
wenzelm@42910
  1179
\isatagproof
wenzelm@42910
  1180
\isacommand{by}\isamarkupfalse%
wenzelm@42910
  1181
\ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
wenzelm@42910
  1182
\endisatagproof
wenzelm@42910
  1183
{\isafoldproof}%
wenzelm@42910
  1184
%
wenzelm@42910
  1185
\isadelimproof
wenzelm@42910
  1186
%
wenzelm@42910
  1187
\endisadelimproof
wenzelm@42910
  1188
%
wenzelm@42908
  1189
\isamarkupsection{Records \label{sec:hol-record}%
wenzelm@42908
  1190
}
wenzelm@42908
  1191
\isamarkuptrue%
wenzelm@42908
  1192
%
wenzelm@42908
  1193
\begin{isamarkuptext}%
wenzelm@42908
  1194
In principle, records merely generalize the concept of tuples, where
wenzelm@42908
  1195
  components may be addressed by labels instead of just position.  The
wenzelm@42908
  1196
  logical infrastructure of records in Isabelle/HOL is slightly more
wenzelm@42908
  1197
  advanced, though, supporting truly extensible record schemes.  This
wenzelm@42908
  1198
  admits operations that are polymorphic with respect to record
wenzelm@42908
  1199
  extension, yielding ``object-oriented'' effects like (single)
wenzelm@42908
  1200
  inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for more
wenzelm@42908
  1201
  details on object-oriented verification and record subtyping in HOL.%
wenzelm@42908
  1202
\end{isamarkuptext}%
wenzelm@42908
  1203
\isamarkuptrue%
wenzelm@42908
  1204
%
wenzelm@42908
  1205
\isamarkupsubsection{Basic concepts%
wenzelm@42908
  1206
}
wenzelm@42908
  1207
\isamarkuptrue%
wenzelm@42908
  1208
%
wenzelm@42908
  1209
\begin{isamarkuptext}%
wenzelm@42908
  1210
Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
wenzelm@42908
  1211
  at the level of terms and types.  The notation is as follows:
wenzelm@42908
  1212
wenzelm@42908
  1213
  \begin{center}
wenzelm@42908
  1214
  \begin{tabular}{l|l|l}
wenzelm@42908
  1215
    & record terms & record types \\ \hline
wenzelm@42908
  1216
    fixed & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1217
    schematic & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} &
wenzelm@42908
  1218
      \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ M{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1219
  \end{tabular}
wenzelm@42908
  1220
  \end{center}
wenzelm@42908
  1221
wenzelm@42908
  1222
  \noindent The ASCII representation of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{7C}{\isacharbar}}\ x\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@42908
  1223
wenzelm@42908
  1224
  A fixed record \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} has field \isa{x} of value
wenzelm@42908
  1225
  \isa{a} and field \isa{y} of value \isa{b}.  The corresponding
wenzelm@42908
  1226
  type is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, assuming that \isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{22}{\isachardoublequote}}}
wenzelm@42908
  1227
  and \isa{{\isaliteral{22}{\isachardoublequote}}b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@42908
  1228
wenzelm@42908
  1229
  A record scheme like \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} contains fields
wenzelm@42908
  1230
  \isa{x} and \isa{y} as before, but also possibly further fields
wenzelm@42908
  1231
  as indicated by the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' notation (which is actually part
wenzelm@42908
  1232
  of the syntax).  The improper field ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' of a record
wenzelm@42908
  1233
  scheme is called the \emph{more part}.  Logically it is just a free
wenzelm@42908
  1234
  variable, which is occasionally referred to as ``row variable'' in
wenzelm@42908
  1235
  the literature.  The more part of a record scheme may be
wenzelm@42908
  1236
  instantiated by zero or more further components.  For example, the
wenzelm@42908
  1237
  previous scheme may get instantiated to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{m{\isaliteral{27}{\isacharprime}}} refers to a different more part.
wenzelm@42908
  1238
  Fixed records are special instances of record schemes, where
wenzelm@42908
  1239
  ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' is properly terminated by the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ unit{\isaliteral{22}{\isachardoublequote}}}
wenzelm@42908
  1240
  element.  In fact, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is just an abbreviation
wenzelm@42908
  1241
  for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@26849
  1242
wenzelm@42908
  1243
  \medskip Two key observations make extensible records in a simply
wenzelm@42908
  1244
  typed language like HOL work out:
wenzelm@42908
  1245
wenzelm@42908
  1246
  \begin{enumerate}
wenzelm@42908
  1247
wenzelm@42908
  1248
  \item the more part is internalized, as a free term or type
wenzelm@42908
  1249
  variable,
wenzelm@42908
  1250
wenzelm@42908
  1251
  \item field names are externalized, they cannot be accessed within
wenzelm@42908
  1252
  the logic as first-class values.
wenzelm@42908
  1253
wenzelm@42908
  1254
  \end{enumerate}
wenzelm@42908
  1255
wenzelm@42908
  1256
  \medskip In Isabelle/HOL record types have to be defined explicitly,
wenzelm@42908
  1257
  fixing their field names and types, and their (optional) parent
wenzelm@42908
  1258
  record.  Afterwards, records may be formed using above syntax, while
wenzelm@42908
  1259
  obeying the canonical order of fields as given by their declaration.
wenzelm@42908
  1260
  The record package provides several standard operations like
wenzelm@42908
  1261
  selectors and updates.  The common setup for various generic proof
wenzelm@42908
  1262
  tools enable succinct reasoning patterns.  See also the Isabelle/HOL
wenzelm@42908
  1263
  tutorial \cite{isabelle-hol-book} for further instructions on using
wenzelm@42908
  1264
  records in practice.%
wenzelm@42908
  1265
\end{isamarkuptext}%
wenzelm@42908
  1266
\isamarkuptrue%
wenzelm@42908
  1267
%
wenzelm@42908
  1268
\isamarkupsubsection{Record specifications%
wenzelm@42908
  1269
}
wenzelm@42908
  1270
\isamarkuptrue%
wenzelm@42908
  1271
%
wenzelm@42908
  1272
\begin{isamarkuptext}%
wenzelm@42908
  1273
\begin{matharray}{rcl}
wenzelm@42908
  1274
    \indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1275
  \end{matharray}
wenzelm@26849
  1276
wenzelm@42908
  1277
  \begin{railoutput}
wenzelm@42908
  1278
\rail@begin{4}{}
wenzelm@42908
  1279
\rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
wenzelm@42908
  1280
\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
wenzelm@42908
  1281
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
wenzelm@42908
  1282
\rail@cr{2}
wenzelm@42908
  1283
\rail@bar
wenzelm@42908
  1284
\rail@nextbar{3}
wenzelm@42908
  1285
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
wenzelm@42908
  1286
\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
wenzelm@42908
  1287
\rail@endbar
wenzelm@42908
  1288
\rail@plus
wenzelm@42908
  1289
\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
wenzelm@42908
  1290
\rail@nextplus{3}
wenzelm@42908
  1291
\rail@endplus
wenzelm@42908
  1292
\rail@end
wenzelm@42908
  1293
\end{railoutput}
wenzelm@42908
  1294
wenzelm@42908
  1295
wenzelm@42908
  1296
  \begin{description}
wenzelm@42908
  1297
wenzelm@42908
  1298
  \item \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{2B}{\isacharplus}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} defines extensible record type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}},
wenzelm@42908
  1299
  derived from the optional parent record \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} by adding new
wenzelm@42908
  1300
  field components \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} etc.
wenzelm@42908
  1301
wenzelm@42908
  1302
  The type variables of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} need to be
wenzelm@42908
  1303
  covered by the (distinct) parameters \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}.  Type constructor \isa{t} has to be new, while \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} needs to specify an instance of an existing record type.  At
wenzelm@42908
  1304
  least one new field \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} has to be specified.
wenzelm@42908
  1305
  Basically, field names need to belong to a unique record.  This is
wenzelm@42908
  1306
  not a real restriction in practice, since fields are qualified by
wenzelm@42908
  1307
  the record name internally.
wenzelm@42908
  1308
wenzelm@42908
  1309
  The parent record specification \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is optional; if omitted
wenzelm@42908
  1310
  \isa{t} becomes a root record.  The hierarchy of all records
wenzelm@42908
  1311
  declared within a theory context forms a forest structure, i.e.\ a
wenzelm@42908
  1312
  set of trees starting with a root record each.  There is no way to
wenzelm@42908
  1313
  merge multiple parent records!
wenzelm@42908
  1314
wenzelm@42908
  1315
  For convenience, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} is made a
wenzelm@42908
  1316
  type abbreviation for the fixed record type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, likewise is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{22}{\isachardoublequote}}} made an abbreviation for
wenzelm@42908
  1317
  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@26849
  1318
wenzelm@28788
  1319
  \end{description}%
wenzelm@26849
  1320
\end{isamarkuptext}%
wenzelm@26849
  1321
\isamarkuptrue%
wenzelm@26849
  1322
%
wenzelm@42908
  1323
\isamarkupsubsection{Record operations%
wenzelm@42908
  1324
}
wenzelm@42908
  1325
\isamarkuptrue%
wenzelm@42908
  1326
%
wenzelm@42908
  1327
\begin{isamarkuptext}%
wenzelm@42908
  1328
Any record definition of the form presented above produces certain
wenzelm@42908
  1329
  standard operations.  Selectors and updates are provided for any
wenzelm@42908
  1330
  field, including the improper one ``\isa{more}''.  There are also
wenzelm@42908
  1331
  cumulative record constructor functions.  To simplify the
wenzelm@42908
  1332
  presentation below, we assume for now that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} is a root record with fields \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@42908
  1333
wenzelm@42908
  1334
  \medskip \textbf{Selectors} and \textbf{updates} are available for
wenzelm@42908
  1335
  any field (including ``\isa{more}''):
wenzelm@42908
  1336
wenzelm@42908
  1337
  \begin{matharray}{lll}
wenzelm@42908
  1338
    \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1339
    \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5F}{\isacharunderscore}}update{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1340
  \end{matharray}
wenzelm@42908
  1341
wenzelm@42908
  1342
  There is special syntax for application of updates: \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} abbreviates term \isa{{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{5F}{\isacharunderscore}}update\ a\ r{\isaliteral{22}{\isachardoublequote}}}.  Further notation for
wenzelm@42908
  1343
  repeated updates is also available: \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} may be written \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.  Note that
wenzelm@42908
  1344
  because of postfix notation the order of fields shown here is
wenzelm@42908
  1345
  reverse than in the actual term.  Since repeated updates are just
wenzelm@42908
  1346
  function applications, fields may be freely permuted in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, as far as logical equality is concerned.
wenzelm@42908
  1347
  Thus commutativity of independent updates can be proven within the
wenzelm@42908
  1348
  logic for any two fields, but not as a general theorem.
wenzelm@42908
  1349
wenzelm@42908
  1350
  \medskip The \textbf{make} operation provides a cumulative record
wenzelm@42908
  1351
  constructor function:
wenzelm@42908
  1352
wenzelm@42908
  1353
  \begin{matharray}{lll}
wenzelm@42908
  1354
    \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1355
  \end{matharray}
wenzelm@42908
  1356
wenzelm@42908
  1357
  \medskip We now reconsider the case of non-root records, which are
wenzelm@42908
  1358
  derived of some parent.  In general, the latter may depend on
wenzelm@42908
  1359
  another parent as well, resulting in a list of \emph{ancestor
wenzelm@42908
  1360
  records}.  Appending the lists of fields of all ancestors results in
wenzelm@42908
  1361
  a certain field prefix.  The record package automatically takes care
wenzelm@42908
  1362
  of this by lifting operations over this context of ancestor fields.
wenzelm@42908
  1363
  Assuming that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} has ancestor
wenzelm@42908
  1364
  fields \isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}},
wenzelm@42908
  1365
  the above record operations will get the following types:
wenzelm@42908
  1366
wenzelm@42908
  1367
  \medskip
wenzelm@42908
  1368
  \begin{tabular}{lll}
wenzelm@42908
  1369
    \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1370
    \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5F}{\isacharunderscore}}update{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1371
    \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1372
  \end{tabular}
wenzelm@42908
  1373
  \medskip
wenzelm@42908
  1374
wenzelm@42908
  1375
  \noindent Some further operations address the extension aspect of a
wenzelm@42908
  1376
  derived record scheme specifically: \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} produces a
wenzelm@42908
  1377
  record fragment consisting of exactly the new fields introduced here
wenzelm@42908
  1378
  (the result may serve as a more part elsewhere); \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}
wenzelm@42908
  1379
  takes a fixed record and adds a given more part; \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} restricts a record scheme to a fixed record.
wenzelm@42908
  1380
wenzelm@42908
  1381
  \medskip
wenzelm@42908
  1382
  \begin{tabular}{lll}
wenzelm@42908
  1383
    \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1384
    \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1385
    \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1386
  \end{tabular}
wenzelm@42908
  1387
  \medskip
wenzelm@42908
  1388
wenzelm@42908
  1389
  \noindent Note that \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} coincide
wenzelm@42908
  1390
  for root records.%
wenzelm@42908
  1391
\end{isamarkuptext}%
wenzelm@42908
  1392
\isamarkuptrue%
wenzelm@42908
  1393
%
wenzelm@42908
  1394
\isamarkupsubsection{Derived rules and proof tools%
wenzelm@26849
  1395
}
wenzelm@26849
  1396
\isamarkuptrue%
wenzelm@26849
  1397
%
wenzelm@26849
  1398
\begin{isamarkuptext}%
wenzelm@42908
  1399
The record package proves several results internally, declaring
wenzelm@42908
  1400
  these facts to appropriate proof tools.  This enables users to
wenzelm@42908
  1401
  reason about record structures quite conveniently.  Assume that
wenzelm@42908
  1402
  \isa{t} is a record type as specified above.
wenzelm@42908
  1403
wenzelm@42908
  1404
  \begin{enumerate}
wenzelm@42908
  1405
wenzelm@42908
  1406
  \item Standard conversions for selectors or updates applied to
wenzelm@42908
  1407
  record constructor terms are made part of the default Simplifier
wenzelm@42908
  1408
  context; thus proofs by reduction of basic operations merely require
wenzelm@42908
  1409
  the \hyperlink{method.simp}{\mbox{\isa{simp}}} method without further arguments.  These rules
wenzelm@42908
  1410
  are available as \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, too.
wenzelm@42908
  1411
wenzelm@42908
  1412
  \item Selectors applied to updated records are automatically reduced
wenzelm@42908
  1413
  by an internal simplification procedure, which is also part of the
wenzelm@42908
  1414
  standard Simplifier setup.
wenzelm@42908
  1415
wenzelm@42908
  1416
  \item Inject equations of a form analogous to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} are declared to the Simplifier and Classical
wenzelm@42908
  1417
  Reasoner as \hyperlink{attribute.iff}{\mbox{\isa{iff}}} rules.  These rules are available as
wenzelm@42908
  1418
  \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}iffs{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@42908
  1419
wenzelm@42908
  1420
  \item The introduction rule for record equality analogous to \isa{{\isaliteral{22}{\isachardoublequote}}x\ r\ {\isaliteral{3D}{\isacharequal}}\ x\ r{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ y\ r\ {\isaliteral{3D}{\isacharequal}}\ y\ r{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} is declared to the Simplifier,
wenzelm@42908
  1421
  and as the basic rule context as ``\hyperlink{attribute.intro}{\mbox{\isa{intro}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}''.
wenzelm@42908
  1422
  The rule is called \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}equality{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@42908
  1423
wenzelm@42908
  1424
  \item Representations of arbitrary record expressions as canonical
wenzelm@42908
  1425
  constructor terms are provided both in \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} format (cf.\ the generic proof methods of the same name,
wenzelm@42908
  1426
  \secref{sec:cases-induct}).  Several variations are available, for
wenzelm@42908
  1427
  fixed records, record schemes, more parts etc.
wenzelm@42908
  1428
wenzelm@42908
  1429
  The generic proof methods are sufficiently smart to pick the most
wenzelm@42908
  1430
  sensible rule according to the type of the indicated record
wenzelm@42908
  1431
  expression: users just need to apply something like ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}cases\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' to a certain proof problem.
wenzelm@42908
  1432
wenzelm@42908
  1433
  \item The derived record operations \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} are \emph{not}
wenzelm@42908
  1434
  treated automatically, but usually need to be expanded by hand,
wenzelm@42908
  1435
  using the collective fact \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}defs{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@42908
  1436
wenzelm@42908
  1437
  \end{enumerate}%
wenzelm@42908
  1438
\end{isamarkuptext}%
wenzelm@42908
  1439
\isamarkuptrue%
wenzelm@42908
  1440
%
wenzelm@42911
  1441
\isamarkupsubsubsection{Examples%
wenzelm@42911
  1442
}
wenzelm@42911
  1443
\isamarkuptrue%
wenzelm@42911
  1444
%
wenzelm@42911
  1445
\begin{isamarkuptext}%
wenzelm@42911
  1446
See \verb|~~/src/HOL/ex/Records.thy|, for example.%
wenzelm@42911
  1447
\end{isamarkuptext}%
wenzelm@42911
  1448
\isamarkuptrue%
wenzelm@42911
  1449
%
wenzelm@42908
  1450
\isamarkupsection{Adhoc tuples%
wenzelm@42908
  1451
}
wenzelm@42908
  1452
\isamarkuptrue%
wenzelm@42908
  1453
%
wenzelm@42908
  1454
\begin{isamarkuptext}%
wenzelm@42908
  1455
\begin{matharray}{rcl}
wenzelm@42908
  1456
    \indexdef{HOL}{attribute}{split\_format}\hypertarget{attribute.HOL.split-format}{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{attribute} \\
wenzelm@42908
  1457
  \end{matharray}
wenzelm@42908
  1458
wenzelm@42908
  1459
  \begin{railoutput}
wenzelm@42908
  1460
\rail@begin{2}{}
wenzelm@42908
  1461
\rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
wenzelm@42908
  1462
\rail@bar
wenzelm@42908
  1463
\rail@nextbar{1}
wenzelm@42908
  1464
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@42908
  1465
\rail@term{\isa{complete}}[]
wenzelm@42908
  1466
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@42908
  1467
\rail@endbar
wenzelm@42908
  1468
\rail@end
wenzelm@42908
  1469
\end{railoutput}
wenzelm@42908
  1470
wenzelm@26849
  1471
wenzelm@26849
  1472
  \begin{description}
wenzelm@26849
  1473
wenzelm@42908
  1474
  \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}complete{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} causes
wenzelm@42908
  1475
  arguments in function applications to be represented canonically
wenzelm@42908
  1476
  according to their tuple type structure.
wenzelm@26849
  1477
wenzelm@42908
  1478
  Note that this operation tends to invent funny names for new local
wenzelm@42908
  1479
  parameters introduced.
wenzelm@26849
  1480
wenzelm@42908
  1481
  \end{description}%
wenzelm@26849
  1482
\end{isamarkuptext}%
wenzelm@26849
  1483
\isamarkuptrue%
wenzelm@26849
  1484
%
wenzelm@42908
  1485
\isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}%
wenzelm@26849
  1486
}
wenzelm@26849
  1487
\isamarkuptrue%
wenzelm@26849
  1488
%
wenzelm@26849
  1489
\begin{isamarkuptext}%
wenzelm@42908
  1490
A Gordon/HOL-style type definition is a certain axiom scheme
wenzelm@42908
  1491
  that identifies a new type with a subset of an existing type.  More
wenzelm@42908
  1492
  precisely, the new type is defined by exhibiting an existing type
wenzelm@42908
  1493
  \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, a set \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ set{\isaliteral{22}{\isachardoublequote}}}, and a theorem that proves
wenzelm@42908
  1494
  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequote}}}.  Thus \isa{A} is a non-empty subset of \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, and the new type denotes this subset.  New functions are
wenzelm@42908
  1495
  postulated that establish an isomorphism between the new type and
wenzelm@42908
  1496
  the subset.  In general, the type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} may involve type
wenzelm@42908
  1497
  variables \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} which means that the type definition
wenzelm@42908
  1498
  produces a type constructor \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} depending on
wenzelm@42908
  1499
  those type arguments.
wenzelm@42908
  1500
wenzelm@42908
  1501
  The axiomatization can be considered a ``definition'' in the sense
wenzelm@42908
  1502
  of the particular set-theoretic interpretation of HOL
wenzelm@42908
  1503
  \cite{pitts93}, where the universe of types is required to be
wenzelm@42908
  1504
  downwards-closed wrt.\ arbitrary non-empty subsets.  Thus genuinely
wenzelm@42908
  1505
  new types introduced by \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} stay within the range
wenzelm@42908
  1506
  of HOL models by construction.  Note that \indexref{}{command}{type\_synonym}\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}} from Isabelle/Pure merely introduces syntactic
wenzelm@42908
  1507
  abbreviations, without any logical significance.
wenzelm@42908
  1508
  
wenzelm@42908
  1509
  \begin{matharray}{rcl}
wenzelm@42908
  1510
    \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1511
  \end{matharray}
wenzelm@42908
  1512
wenzelm@42908
  1513
  \begin{railoutput}
wenzelm@42908
  1514
\rail@begin{2}{}
wenzelm@42908
  1515
\rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
wenzelm@42908
  1516
\rail@bar
wenzelm@42908
  1517
\rail@nextbar{1}
wenzelm@42908
  1518
\rail@nont{\isa{alt{\isaliteral{5F}{\isacharunderscore}}name}}[]
wenzelm@42908
  1519
\rail@endbar
wenzelm@42908
  1520
\rail@nont{\isa{abs{\isaliteral{5F}{\isacharunderscore}}type}}[]
wenzelm@42908
  1521
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
wenzelm@42908
  1522
\rail@nont{\isa{rep{\isaliteral{5F}{\isacharunderscore}}set}}[]
wenzelm@42908
  1523
\rail@end
wenzelm@42908
  1524
\rail@begin{3}{\isa{alt{\isaliteral{5F}{\isacharunderscore}}name}}
wenzelm@42908
  1525
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@42908
  1526
\rail@bar
wenzelm@42908
  1527
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@42908
  1528
\rail@nextbar{1}
wenzelm@42908
  1529
\rail@term{\isa{\isakeyword{open}}}[]
wenzelm@42908
  1530
\rail@nextbar{2}
wenzelm@42908
  1531
\rail@term{\isa{\isakeyword{open}}}[]
wenzelm@42908
  1532
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@42908
  1533
\rail@endbar
wenzelm@42908
  1534
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@42908
  1535
\rail@end
wenzelm@42908
  1536
\rail@begin{2}{\isa{abs{\isaliteral{5F}{\isacharunderscore}}type}}
wenzelm@42908
  1537
\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
wenzelm@42908
  1538
\rail@bar
wenzelm@42908
  1539
\rail@nextbar{1}
wenzelm@42908
  1540
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
wenzelm@42908
  1541
\rail@endbar
wenzelm@42908
  1542
\rail@end
wenzelm@42908
  1543
\rail@begin{2}{\isa{rep{\isaliteral{5F}{\isacharunderscore}}set}}
wenzelm@42908
  1544
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
wenzelm@42908
  1545
\rail@bar
wenzelm@42908
  1546
\rail@nextbar{1}
wenzelm@42908
  1547
\rail@term{\isa{\isakeyword{morphisms}}}[]
wenzelm@42908
  1548
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@42908
  1549
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@42908
  1550
\rail@endbar
wenzelm@42908
  1551
\rail@end
wenzelm@42908
  1552
\end{railoutput}
wenzelm@42908
  1553
wenzelm@42908
  1554
wenzelm@42908
  1555
  \begin{description}
wenzelm@26849
  1556
wenzelm@42908
  1557
  \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{22}{\isachardoublequote}}}
wenzelm@42908
  1558
  axiomatizes a type definition in the background theory of the
wenzelm@42908
  1559
  current context, depending on a non-emptiness result of the set
wenzelm@42908
  1560
  \isa{A} that needs to be proven here.  The set \isa{A} may
wenzelm@42908
  1561
  contain type variables \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} as specified on the LHS,
wenzelm@42908
  1562
  but no term variables.
wenzelm@42908
  1563
wenzelm@42908
  1564
  Even though a local theory specification, the newly introduced type
wenzelm@42908
  1565
  constructor cannot depend on parameters or assumptions of the
wenzelm@42908
  1566
  context: this is structurally impossible in HOL.  In contrast, the
wenzelm@42908
  1567
  non-emptiness proof may use local assumptions in unusual situations,
wenzelm@42908
  1568
  which could result in different interpretations in target contexts:
wenzelm@42908
  1569
  the meaning of the bijection between the representing set \isa{A}
wenzelm@42908
  1570
  and the new type \isa{t} may then change in different application
wenzelm@42908
  1571
  contexts.
wenzelm@42908
  1572
wenzelm@42908
  1573
  By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type
wenzelm@42908
  1574
  constructor \isa{t} for the new type, and a term constant \isa{t} for the representing set within the old type.  Use the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option to suppress a separate constant definition
wenzelm@42908
  1575
  altogether.  The injection from type to set is called \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t},
wenzelm@42908
  1576
  its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t}, unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.
wenzelm@42908
  1577
wenzelm@42908
  1578
  The core axiomatization uses the locale predicate \isa{type{\isaliteral{5F}{\isacharunderscore}}definition} as defined in Isabelle/HOL.  Various basic
wenzelm@42908
  1579
  consequences of that are instantiated accordingly, re-using the
wenzelm@42908
  1580
  locale facts with names derived from the new type constructor.  Thus
wenzelm@42908
  1581
  the generic \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep} is turned into the specific
wenzelm@42908
  1582
  \isa{{\isaliteral{22}{\isachardoublequote}}Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{22}{\isachardoublequote}}}, for example.
wenzelm@26849
  1583
wenzelm@42908
  1584
  Theorems \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep}, \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}inverse}, and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}inverse}
wenzelm@42908
  1585
  provide the most basic characterization as a corresponding
wenzelm@42908
  1586
  injection/surjection pair (in both directions).  The derived rules
wenzelm@42908
  1587
  \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}inject} and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}inject} provide a more convenient version of
wenzelm@42908
  1588
  injectivity, suitable for automated proof tools (e.g.\ in
wenzelm@42908
  1589
  declarations involving \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}).
wenzelm@42908
  1590
  Furthermore, the rules \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}cases}~/ \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}induct}, and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}cases}~/
wenzelm@42908
  1591
  \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views on
wenzelm@42908
  1592
  surjectivity.  These rules are already declared as set or type rules
wenzelm@42908
  1593
  for the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods,
wenzelm@42908
  1594
  respectively.
wenzelm@42908
  1595
wenzelm@42908
  1596
  An alternative name for the set definition (and other derived
wenzelm@42908
  1597
  entities) may be specified in parentheses; the default is to use
wenzelm@42908
  1598
  \isa{t} directly.
wenzelm@42908
  1599
wenzelm@42908
  1600
  \end{description}
wenzelm@42908
  1601
wenzelm@42908
  1602
  \begin{warn}
wenzelm@42908
  1603
  If you introduce a new type axiomatically, i.e.\ via \indexref{}{command}{typedecl}\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} and \indexref{}{command}{axiomatization}\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}, the minimum requirement
wenzelm@42908
  1604
  is that it has a non-empty model, to avoid immediate collapse of the
wenzelm@42908
  1605
  HOL logic.  Moreover, one needs to demonstrate that the
wenzelm@42908
  1606
  interpretation of such free-form axiomatizations can coexist with
wenzelm@42908
  1607
  that of the regular \indexdef{}{command}{typedef}\hypertarget{command.typedef}{\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}} scheme, and any extension
wenzelm@42908
  1608
  that other people might have introduced elsewhere (e.g.\ in HOLCF
wenzelm@42908
  1609
  \cite{MuellerNvOS99}).
wenzelm@42908
  1610
  \end{warn}%
wenzelm@42908
  1611
\end{isamarkuptext}%
wenzelm@42908
  1612
\isamarkuptrue%
wenzelm@42908
  1613
%
wenzelm@42908
  1614
\isamarkupsubsubsection{Examples%
wenzelm@42908
  1615
}
wenzelm@42908
  1616
\isamarkuptrue%
wenzelm@42908
  1617
%
wenzelm@42908
  1618
\begin{isamarkuptext}%
wenzelm@42908
  1619
Type definitions permit the introduction of abstract data
wenzelm@42908
  1620
  types in a safe way, namely by providing models based on already
wenzelm@42908
  1621
  existing types.  Given some abstract axiomatic description \isa{P}
wenzelm@42908
  1622
  of a type, this involves two steps:
wenzelm@42908
  1623
wenzelm@42908
  1624
  \begin{enumerate}
wenzelm@26849
  1625
wenzelm@42908
  1626
  \item Find an appropriate type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} and subset \isa{A} which
wenzelm@42908
  1627
  has the desired properties \isa{P}, and make a type definition
wenzelm@42908
  1628
  based on this representation.
wenzelm@42908
  1629
wenzelm@42908
  1630
  \item Prove that \isa{P} holds for \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} by lifting \isa{P}
wenzelm@42908
  1631
  from the representation.
wenzelm@42908
  1632
wenzelm@42908
  1633
  \end{enumerate}
wenzelm@42908
  1634
wenzelm@42908
  1635
  You can later forget about the representation and work solely in
wenzelm@42908
  1636
  terms of the abstract properties \isa{P}.
wenzelm@26849
  1637
wenzelm@42908
  1638
  \medskip The following trivial example pulls a three-element type
wenzelm@42908
  1639
  into existence within the formal logical environment of HOL.%
wenzelm@42908
  1640
\end{isamarkuptext}%
wenzelm@42908
  1641
\isamarkuptrue%
wenzelm@42908
  1642
\isacommand{typedef}\isamarkupfalse%
wenzelm@42908
  1643
\ three\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}False{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42908
  1644
%
wenzelm@42908
  1645
\isadelimproof
wenzelm@42908
  1646
\ \ %
wenzelm@42908
  1647
\endisadelimproof
wenzelm@42908
  1648
%
wenzelm@42908
  1649
\isatagproof
wenzelm@42908
  1650
\isacommand{by}\isamarkupfalse%
wenzelm@42908
  1651
\ blast%
wenzelm@42908
  1652
\endisatagproof
wenzelm@42908
  1653
{\isafoldproof}%
wenzelm@42908
  1654
%
wenzelm@42908
  1655
\isadelimproof
wenzelm@42908
  1656
\isanewline
wenzelm@42908
  1657
%
wenzelm@42908
  1658
\endisadelimproof
wenzelm@42908
  1659
\isanewline
wenzelm@42908
  1660
\isacommand{definition}\isamarkupfalse%
wenzelm@42908
  1661
\ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42908
  1662
\isacommand{definition}\isamarkupfalse%
wenzelm@42908
  1663
\ {\isaliteral{22}{\isachardoublequoteopen}}Two\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42908
  1664
\isacommand{definition}\isamarkupfalse%
wenzelm@42908
  1665
\ {\isaliteral{22}{\isachardoublequoteopen}}Three\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}False{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42908
  1666
\isanewline
wenzelm@42908
  1667
\isacommand{lemma}\isamarkupfalse%
wenzelm@42908
  1668
\ three{\isaliteral{5F}{\isacharunderscore}}distinct{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Two{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}Two\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42908
  1669
%
wenzelm@42908
  1670
\isadelimproof
wenzelm@42908
  1671
\ \ %
wenzelm@42908
  1672
\endisadelimproof
wenzelm@42908
  1673
%
wenzelm@42908
  1674
\isatagproof
wenzelm@42908
  1675
\isacommand{by}\isamarkupfalse%
wenzelm@42908
  1676
\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ One{\isaliteral{5F}{\isacharunderscore}}def\ Two{\isaliteral{5F}{\isacharunderscore}}def\ Three{\isaliteral{5F}{\isacharunderscore}}def\ Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject\ three{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
wenzelm@42908
  1677
\endisatagproof
wenzelm@42908
  1678
{\isafoldproof}%
wenzelm@42908
  1679
%
wenzelm@42908
  1680
\isadelimproof
wenzelm@42908
  1681
\isanewline
wenzelm@42908
  1682
%
wenzelm@42908
  1683
\endisadelimproof
wenzelm@42908
  1684
\isanewline
wenzelm@42908
  1685
\isacommand{lemma}\isamarkupfalse%
wenzelm@42908
  1686
\ three{\isaliteral{5F}{\isacharunderscore}}cases{\isaliteral{3A}{\isacharcolon}}\isanewline
wenzelm@42908
  1687
\ \ \isakeyword{fixes}\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ three\ \isakeyword{obtains}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ One{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Two{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@42908
  1688
%
wenzelm@42908
  1689
\isadelimproof
wenzelm@42908
  1690
\ \ %
wenzelm@42908
  1691
\endisadelimproof
wenzelm@42908
  1692
%
wenzelm@42908
  1693
\isatagproof
wenzelm@42908
  1694
\isacommand{by}\isamarkupfalse%
wenzelm@42908
  1695
\ {\isaliteral{28}{\isacharparenleft}}cases\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}auto\ simp{\isaliteral{3A}{\isacharcolon}}\ One{\isaliteral{5F}{\isacharunderscore}}def\ Two{\isaliteral{5F}{\isacharunderscore}}def\ Three{\isaliteral{5F}{\isacharunderscore}}def\ Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject\ three{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
wenzelm@42908
  1696
\endisatagproof
wenzelm@42908
  1697
{\isafoldproof}%
wenzelm@42908
  1698
%
wenzelm@42908
  1699
\isadelimproof
wenzelm@42908
  1700
%
wenzelm@42908
  1701
\endisadelimproof
wenzelm@42908
  1702
%
wenzelm@42908
  1703
\begin{isamarkuptext}%
wenzelm@42908
  1704
Note that such trivial constructions are better done with
wenzelm@42908
  1705
  derived specification mechanisms such as \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}:%
wenzelm@42908
  1706
\end{isamarkuptext}%
wenzelm@42908
  1707
\isamarkuptrue%
wenzelm@42908
  1708
\isacommand{datatype}\isamarkupfalse%
wenzelm@42908
  1709
\ three{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ One{\isaliteral{27}{\isacharprime}}\ {\isaliteral{7C}{\isacharbar}}\ Two{\isaliteral{27}{\isacharprime}}\ {\isaliteral{7C}{\isacharbar}}\ Three{\isaliteral{27}{\isacharprime}}%
wenzelm@42908
  1710
\begin{isamarkuptext}%
wenzelm@42908
  1711
This avoids re-doing basic definitions and proofs from the
wenzelm@42908
  1712
  primitive \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} above.%
wenzelm@42908
  1713
\end{isamarkuptext}%
wenzelm@42908
  1714
\isamarkuptrue%
wenzelm@42908
  1715
%
wenzelm@42908
  1716
\isamarkupsection{Functorial structure of types%
wenzelm@42908
  1717
}
wenzelm@42908
  1718
\isamarkuptrue%
wenzelm@42908
  1719
%
wenzelm@42908
  1720
\begin{isamarkuptext}%
wenzelm@42908
  1721
\begin{matharray}{rcl}
wenzelm@42908
  1722
    \indexdef{HOL}{command}{enriched\_type}\hypertarget{command.HOL.enriched-type}{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
wenzelm@42908
  1723
  \end{matharray}
wenzelm@26849
  1724
wenzelm@42908
  1725
  \begin{railoutput}
wenzelm@42908
  1726
\rail@begin{2}{}
wenzelm@42908
  1727
\rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
wenzelm@42908
  1728
\rail@bar
wenzelm@42908
  1729
\rail@nextbar{1}
wenzelm@42908
  1730
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@42908
  1731
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
wenzelm@42908
  1732
\rail@endbar
wenzelm@42908
  1733
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
wenzelm@42908
  1734
\rail@end
wenzelm@42908
  1735
\end{railoutput}
wenzelm@42908
  1736
wenzelm@42908
  1737
wenzelm@42908
  1738
  \begin{description}
wenzelm@26849
  1739
wenzelm@42908
  1740
  \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}prefix{\isaliteral{3A}{\isacharcolon}}\ m{\isaliteral{22}{\isachardoublequote}}} allows to
wenzelm@42908
  1741
  prove and register properties about the functorial structure of type
wenzelm@42908
  1742
  constructors.  These properties then can be used by other packages
wenzelm@42908
  1743
  to deal with those type constructors in certain type constructions.
wenzelm@42908
  1744
  Characteristic theorems are noted in the current local theory.  By
wenzelm@42908
  1745
  default, they are prefixed with the base name of the type
wenzelm@42908
  1746
  constructor, an explicit prefix can be given alternatively.
wenzelm@42908
  1747
wenzelm@42908
  1748
  The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the
wenzelm@42908
  1749
  corresponding type constructor and must conform to the following
wenzelm@42908
  1750
  type pattern:
wenzelm@26849
  1751
wenzelm@42908
  1752
  \begin{matharray}{lll}
wenzelm@42908
  1753
    \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
wenzelm@42908
  1754
      \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@42908
  1755
  \end{matharray}
wenzelm@42908
  1756
wenzelm@42908
  1757
  \noindent where \isa{t} is the type constructor, \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are distinct
wenzelm@42908
  1758
  type variables free in the local theory and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}},
wenzelm@42908
  1759
  \ldots, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{22}{\isachardoublequote}}} is a subsequence of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \ldots,
wenzelm@42908
  1760
  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@42908
  1761
wenzelm@42908
  1762
  \end{description}%
wenzelm@26849
  1763
\end{isamarkuptext}%
wenzelm@26849
  1764
\isamarkuptrue%
wenzelm@26849
  1765
%
bulwahn@43993
  1766
\isamarkupsection{Quotient types%
bulwahn@43993
  1767
}
bulwahn@43993
  1768
\isamarkuptrue%
bulwahn@43993
  1769
%
bulwahn@43993
  1770
\begin{isamarkuptext}%
bulwahn@43993
  1771
The quotient package defines a new quotient type given a raw type
bulwahn@43993
  1772
  and a partial equivalence relation.
bulwahn@43993
  1773
  It also includes automation for transporting definitions and theorems.
bulwahn@43993
  1774
  It can automatically produce definitions and theorems on the quotient type,
bulwahn@43993
  1775
  given the corresponding constants and facts on the raw type.
bulwahn@43993
  1776
bulwahn@43993
  1777
  \begin{matharray}{rcl}
bulwahn@43993
  1778
    \indexdef{HOL}{command}{quotient\_type}\hypertarget{command.HOL.quotient-type}{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
bulwahn@43993
  1779
    \indexdef{HOL}{command}{quotient\_definition}\hypertarget{command.HOL.quotient-definition}{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
bulwahn@43993
  1780
    \indexdef{HOL}{command}{print\_quotmaps}\hypertarget{command.HOL.print-quotmaps}{\hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\
bulwahn@43993
  1781
    \indexdef{HOL}{command}{print\_quotients}\hypertarget{command.HOL.print-quotients}{\hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\
bulwahn@43993
  1782
    \indexdef{HOL}{command}{print\_quotconsts}\hypertarget{command.HOL.print-quotconsts}{\hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\
cezarykaliszyk@46447
  1783
    \indexdef{HOL}{method}{lifting}\hypertarget{method.HOL.lifting}{\hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}}} & : & \isa{method} \\
cezarykaliszyk@46447
  1784
    \indexdef{HOL}{method}{lifting\_setup}\hypertarget{method.HOL.lifting-setup}{\hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\
cezarykaliszyk@46447
  1785
    \indexdef{HOL}{method}{descending}\hypertarget{method.HOL.descending}{\hyperlink{method.HOL.descending}{\mbox{\isa{descending}}}} & : & \isa{method} \\
cezarykaliszyk@46447
  1786
    \indexdef{HOL}{method}{descending\_setup}\hypertarget{method.HOL.descending-setup}{\hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\
cezarykaliszyk@46447
  1787
    \indexdef{HOL}{method}{partiality\_descending}\hypertarget{method.HOL.partiality-descending}{\hyperlink{method.HOL.partiality-descending}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending}}}} & : & \isa{method} \\
cezarykaliszyk@46447
  1788
    \indexdef{HOL}{method}{partiality\_descending\_setup}\hypertarget{method.HOL.partiality-descending-setup}{\hyperlink{method.HOL.partiality-descending-setup}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\
cezarykaliszyk@46447
  1789
    \indexdef{HOL}{method}{regularize}\hypertarget{method.HOL.regularize}{\hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}}} & : & \isa{method} \\
cezarykaliszyk@46447
  1790
    \indexdef{HOL}{method}{injection}\hypertarget{method.HOL.injection}{\hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}} & : & \isa{method} \\
cezarykaliszyk@46447
  1791
    \indexdef{HOL}{method}{cleaning}\hypertarget{method.HOL.cleaning}{\hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}}} & : & \isa{method} \\
cezarykaliszyk@46448
  1792
    \indexdef{HOL}{attribute}{quot\_thm}\hypertarget{attribute.HOL.quot-thm}{\hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}}} & : & \isa{attribute} \\
cezarykaliszyk@46447
  1793
    \indexdef{HOL}{attribute}{quot\_lifted}\hypertarget{attribute.HOL.quot-lifted}{\hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}}} & : & \isa{attribute} \\
cezarykaliszyk@46447
  1794
    \indexdef{HOL}{attribute}{quot\_respect}\hypertarget{attribute.HOL.quot-respect}{\hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}}} & : & \isa{attribute} \\
cezarykaliszyk@46447
  1795
    \indexdef{HOL}{attribute}{quot\_preserve}\hypertarget{attribute.HOL.quot-preserve}{\hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}}} & : & \isa{attribute} \\
bulwahn@43993
  1796
  \end{matharray}
bulwahn@43993
  1797
bulwahn@43993
  1798
  \begin{railoutput}
bulwahn@43993
  1799
\rail@begin{2}{}
bulwahn@43993
  1800
\rail@term{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
bulwahn@43993
  1801
\rail@plus
bulwahn@43993
  1802
\rail@nont{\isa{spec}}[]
bulwahn@43993
  1803
\rail@nextplus{1}
bulwahn@43993
  1804
\rail@cterm{\isa{\isakeyword{and}}}[]
bulwahn@43993
  1805
\rail@endplus
bulwahn@43993
  1806
\rail@end
kuncar@45678
  1807
\rail@begin{8}{\isa{spec}}
bulwahn@43993
  1808
\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
bulwahn@43993
  1809
\rail@bar
bulwahn@43993
  1810
\rail@nextbar{1}
bulwahn@43993
  1811
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
bulwahn@43993
  1812
\rail@endbar
bulwahn@43993
  1813
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
bulwahn@43993
  1814
\rail@cr{3}
bulwahn@43993
  1815
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
bulwahn@43993
  1816
\rail@term{\isa{{\isaliteral{2F}{\isacharslash}}}}[]
bulwahn@43993
  1817
\rail@bar
bulwahn@43993
  1818
\rail@nextbar{4}
bulwahn@43993
  1819
\rail@term{\isa{partial}}[]
bulwahn@43993
  1820
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
bulwahn@43993
  1821
\rail@endbar
bulwahn@43993
  1822
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
kuncar@45678
  1823
\rail@cr{6}
kuncar@45678
  1824
\rail@bar
kuncar@45678
  1825
\rail@nextbar{7}
kuncar@45678
  1826
\rail@term{\isa{\isakeyword{morphisms}}}[]
kuncar@45678
  1827
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
kuncar@45678
  1828
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
kuncar@45678
  1829
\rail@endbar
bulwahn@43993
  1830
\rail@end
bulwahn@43993
  1831
\end{railoutput}
bulwahn@43993
  1832
bulwahn@43993
  1833
bulwahn@43993
  1834
  \begin{railoutput}
bulwahn@43993
  1835
\rail@begin{4}{}
bulwahn@43993
  1836
\rail@term{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}}[]
bulwahn@43993
  1837
\rail@bar
bulwahn@43993
  1838
\rail@nextbar{1}
bulwahn@43993
  1839
\rail@nont{\isa{constdecl}}[]
bulwahn@43993
  1840
\rail@endbar
bulwahn@43993
  1841
\rail@bar
bulwahn@43993
  1842
\rail@nextbar{1}
bulwahn@43993
  1843
\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
bulwahn@43993
  1844
\rail@endbar
bulwahn@43993
  1845
\rail@cr{3}
bulwahn@43993
  1846
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
bulwahn@43993
  1847
\rail@term{\isa{is}}[]
bulwahn@43993
  1848
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
bulwahn@43993
  1849
\rail@end
bulwahn@43993
  1850
\rail@begin{2}{\isa{constdecl}}
bulwahn@43993
  1851
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
bulwahn@43993
  1852
\rail@bar
bulwahn@43993
  1853
\rail@nextbar{1}
bulwahn@43993
  1854
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
bulwahn@43993
  1855
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
bulwahn@43993
  1856
\rail@endbar
bulwahn@43993
  1857
\rail@bar
bulwahn@43993
  1858
\rail@nextbar{1}
bulwahn@43993
  1859
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
bulwahn@43993
  1860
\rail@endbar
bulwahn@43993
  1861
\rail@end
bulwahn@43993
  1862
\end{railoutput}
bulwahn@43993
  1863
bulwahn@43993
  1864
cezarykaliszyk@46447
  1865
  \begin{railoutput}
cezarykaliszyk@46447
  1866
\rail@begin{2}{}
cezarykaliszyk@46447
  1867
\rail@term{\hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}}}[]
cezarykaliszyk@46447
  1868
\rail@bar
cezarykaliszyk@46447
  1869
\rail@nextbar{1}
cezarykaliszyk@46447
  1870
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
cezarykaliszyk@46447
  1871
\rail@endbar
cezarykaliszyk@46447
  1872
\rail@end
cezarykaliszyk@46447
  1873
\rail@begin{2}{}
cezarykaliszyk@46447
  1874
\rail@term{\hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}}[]
cezarykaliszyk@46447
  1875
\rail@bar
cezarykaliszyk@46447
  1876
\rail@nextbar{1}
cezarykaliszyk@46447
  1877
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
cezarykaliszyk@46447
  1878
\rail@endbar
cezarykaliszyk@46447
  1879
\rail@end
cezarykaliszyk@46447
  1880
\end{railoutput}
cezarykaliszyk@46447
  1881
cezarykaliszyk@46447
  1882
bulwahn@43993
  1883
  \begin{description}
cezarykaliszyk@46447
  1884
kuncar@45767
  1885
  \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. The injection from a quotient type 
cezarykaliszyk@46447
  1886
  to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names. \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} requires
cezarykaliszyk@46447
  1887
  the user to prove that the relation is an equivalence relation (predicate \isa{equivp}), unless
cezarykaliszyk@46447
  1888
  the user specifies explicitely \isa{partial} in which case the obligation is \isa{part{\isaliteral{5F}{\isacharunderscore}}equivp}.
cezarykaliszyk@46447
  1889
  A quotient defined with \isa{partial} is weaker in the sense that less things can be proved
cezarykaliszyk@46447
  1890
  automatically.
bulwahn@43993
  1891
bulwahn@43993
  1892
  \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type.
bulwahn@43993
  1893
bulwahn@43993
  1894
  \item \hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}} prints quotient map functions.
bulwahn@43993
  1895
bulwahn@43993
  1896
  \item \hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}} prints quotients.
bulwahn@43993
  1897
bulwahn@43993
  1898
  \item \hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}} prints quotient constants.
bulwahn@43993
  1899
cezarykaliszyk@46447
  1900
  \item \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} and \hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}
cezarykaliszyk@46447
  1901
    methods match the current goal with the given raw theorem to be
cezarykaliszyk@46447
  1902
    lifted producing three new subgoals: regularization, injection and
cezarykaliszyk@46447
  1903
    cleaning subgoals. \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} tries to apply the
cezarykaliszyk@46447
  1904
    heuristics for automatically solving these three subgoals and
cezarykaliszyk@46447
  1905
    leaves only the subgoals unsolved by the heuristics to the user as
cezarykaliszyk@46447
  1906
    opposed to \hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}} which leaves the three
cezarykaliszyk@46447
  1907
    subgoals unsolved.
cezarykaliszyk@46447
  1908
cezarykaliszyk@46447
  1909
  \item \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} and \hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}} try to guess a raw statement that would lift
cezarykaliszyk@46447
  1910
    to the current subgoal. Such statement is assumed as a new subgoal
cezarykaliszyk@46447
  1911
    and \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} continues in the same way as
cezarykaliszyk@46447
  1912
    \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} does. \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} tries
cezarykaliszyk@46447
  1913
    to solve the arising regularization, injection and cleaning
cezarykaliszyk@46447
  1914
    subgoals with the analoguous method \hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}} which leaves the four unsolved subgoals.
cezarykaliszyk@46447
  1915
cezarykaliszyk@46447
  1916
  \item \hyperlink{method.HOL.partiality-descending}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending}}} finds the regularized
cezarykaliszyk@46447
  1917
    theorem that would lift to the current subgoal, lifts it and
cezarykaliszyk@46447
  1918
    leaves as a subgoal. This method can be used with partial
cezarykaliszyk@46447
  1919
    equivalence quotients where the non regularized statements would
cezarykaliszyk@46447
  1920
    not be true. \hyperlink{method.HOL.partiality-descending-setup}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending{\isaliteral{5F}{\isacharunderscore}}setup}}} leaves
cezarykaliszyk@46447
  1921
    the injection and cleaning subgoals unchanged.
cezarykaliszyk@46447
  1922
cezarykaliszyk@46447
  1923
  \item \hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}} applies the regularization
cezarykaliszyk@46447
  1924
    heuristics to the current subgoal.
cezarykaliszyk@46447
  1925
cezarykaliszyk@46447
  1926
  \item \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}} applies the injection heuristics
cezarykaliszyk@46447
  1927
    to the current goal using the stored quotient respectfulness
cezarykaliszyk@46447
  1928
    theorems.
cezarykaliszyk@46447
  1929
cezarykaliszyk@46447
  1930
  \item \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} applies the injection cleaning
cezarykaliszyk@46447
  1931
    heuristics to the current subgoal using the stored quotient
cezarykaliszyk@46447
  1932
    preservation theorems.
cezarykaliszyk@46447
  1933
cezarykaliszyk@46447
  1934
  \item \hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}} attribute tries to
cezarykaliszyk@46447
  1935
    automatically transport the theorem to the quotient type.
cezarykaliszyk@46447
  1936
    The attribute uses all the defined quotients types and quotient
cezarykaliszyk@46447
  1937
    constants often producing undesired results or theorems that
cezarykaliszyk@46447
  1938
    cannot be lifted.
cezarykaliszyk@46447
  1939
cezarykaliszyk@46447
  1940
  \item \hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}} and \hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}} attributes declare a theorem as a respectfulness
cezarykaliszyk@46447
  1941
    and preservation theorem respectively.  These are stored in the
cezarykaliszyk@46447
  1942
    local theory store and used by the \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}
cezarykaliszyk@46447
  1943
    and \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} methods respectively.
cezarykaliszyk@46447
  1944
cezarykaliszyk@46448
  1945
  \item \hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}} declares that a certain theorem
cezarykaliszyk@46448
  1946
    is a quotient extension theorem. Quotient extension theorems
cezarykaliszyk@46448
  1947
    allow for quotienting inside container types. Given a polymorphic
cezarykaliszyk@46448
  1948
    type that serves as a container, a map function defined for this
cezarykaliszyk@46448
  1949
    container  using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation
cezarykaliszyk@46448
  1950
    map defined for for the container type, the quotient extension
cezarykaliszyk@46448
  1951
    theorem should be \isa{{\isaliteral{22}{\isachardoublequote}}Quotient\ R\ Abs\ Rep\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Quotient\ {\isaliteral{28}{\isacharparenleft}}rel{\isaliteral{5F}{\isacharunderscore}}map\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Abs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Rep{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Quotient extension theorems
cezarykaliszyk@46448
  1952
    are stored in a database and are used all the steps of lifting
cezarykaliszyk@46448
  1953
    theorems.
cezarykaliszyk@46448
  1954
bulwahn@43993
  1955
  \end{description}%
bulwahn@43993
  1956
\end{isamarkuptext}%
bulwahn@43993
  1957
\isamarkuptrue%
bulwahn@43993
  1958
%
noschinl@43994
  1959
\isamarkupsection{Coercive subtyping%
noschinl@43994
  1960
}
noschinl@43994
  1961
\isamarkuptrue%
noschinl@43994
  1962
%
noschinl@43994
  1963
\begin{isamarkuptext}%
noschinl@43994
  1964
\begin{matharray}{rcl}
noschinl@43994
  1965
    \indexdef{HOL}{attribute}{coercion}\hypertarget{attribute.HOL.coercion}{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}} & : & \isa{attribute} \\
noschinl@43994
  1966
    \indexdef{HOL}{attribute}{coercion\_enabled}\hypertarget{attribute.HOL.coercion-enabled}{\hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}}} & : & \isa{attribute} \\
noschinl@43994
  1967
    \indexdef{HOL}{attribute}{coercion\_map}\hypertarget{attribute.HOL.coercion-map}{\hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}} & : & \isa{attribute} \\
noschinl@43994
  1968
  \end{matharray}
noschinl@43994
  1969
noschinl@43994
  1970
  \begin{railoutput}
noschinl@43994
  1971
\rail@begin{2}{}
noschinl@43994
  1972
\rail@term{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}}[]
noschinl@43994
  1973
\rail@bar
noschinl@43994
  1974
\rail@nextbar{1}
noschinl@43994
  1975
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
noschinl@43994
  1976
\rail@endbar
noschinl@43994
  1977
\rail@end
noschinl@43994
  1978
\end{railoutput}
noschinl@43994
  1979
noschinl@43994
  1980
  \begin{railoutput}
noschinl@43994
  1981
\rail@begin{2}{}
noschinl@43994
  1982
\rail@term{\hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}}[]
noschinl@43994
  1983
\rail@bar
noschinl@43994
  1984
\rail@nextbar{1}
noschinl@43994
  1985
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
noschinl@43994
  1986
\rail@endbar
noschinl@43994
  1987
\rail@end
noschinl@43994
  1988
\end{railoutput}
noschinl@43994
  1989
noschinl@43994
  1990
noschinl@43994
  1991
  Coercive subtyping allows the user to omit explicit type conversions,
noschinl@43994
  1992
  also called \emph{coercions}.  Type inference will add them as
noschinl@43994
  1993
  necessary when parsing a term. See
noschinl@43994
  1994
  \cite{traytel-berghofer-nipkow-2011} for details.
noschinl@43994
  1995
noschinl@43994
  1996
  \begin{description}
noschinl@43994
  1997
noschinl@43994
  1998
  \item \hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} registers a new
noschinl@43994
  1999
  coercion function \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} where \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} are nullary type constructors. Coercions are
noschinl@43994
  2000
  composed by the inference algorithm if needed. Note that the type
noschinl@43994
  2001
  inference algorithm is complete only if the registered coercions form
noschinl@43994
  2002
  a lattice.
noschinl@43994
  2003
noschinl@43994
  2004
noschinl@43994
  2005
  \item \hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}~\isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} registers a new
noschinl@43994
  2006
  map function to lift coercions through type constructors. The function
noschinl@43994
  2007
  \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} must conform to the following type pattern
noschinl@43994
  2008
noschinl@43994
  2009
  \begin{matharray}{lll}
noschinl@43994
  2010
    \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
noschinl@43994
  2011
      \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ f\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} \\
noschinl@43994
  2012
  \end{matharray}
noschinl@43994
  2013
noschinl@43994
  2014
  where \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is a type constructor and \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} is of
noschinl@43994
  2015
  type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} or
noschinl@43994
  2016
  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}.
noschinl@43994
  2017
  Registering a map function overwrites any existing map function for
noschinl@43994
  2018
  this particular type constructor.
noschinl@43994
  2019
noschinl@43994
  2020
noschinl@43994
  2021
  \item \hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}} enables the coercion
noschinl@43994
  2022
  inference algorithm.
noschinl@43994
  2023
noschinl@43994
  2024
  \end{description}%
noschinl@43994
  2025
\end{isamarkuptext}%
noschinl@43994
  2026
\isamarkuptrue%
noschinl@43994
  2027
%
wenzelm@26849
  2028
\isamarkupsection{Arithmetic proof support%
wenzelm@26849
  2029
}
wenzelm@26849
  2030
\isamarkuptrue%
wenzelm@26849
  2031
%
wenzelm@26849
  2032
\begin{isamarkuptext}%
wenzelm@26849
  2033
\begin{matharray}{rcl}
wenzelm@28788
  2034
    \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{method} \\
nipkow@30863
  2035
    \indexdef{HOL}{attribute}{arith}\hypertarget{attribute.HOL.arith}{\hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{attribute} \\
wenzelm@40406
  2036
    \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}}} & : & \isa{attribute} \\
wenzelm@26849
  2037
  \end{matharray}
wenzelm@26849
  2038
wenzelm@26902
  2039
  The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems
wenzelm@26849
  2040
  (on types \isa{nat}, \isa{int}, \isa{real}).  Any current
wenzelm@26849
  2041
  facts are inserted into the goal before running the procedure.
wenzelm@26849
  2042
nipkow@30863
  2043
  The \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} attribute declares facts that are
nipkow@30863
  2044
  always supplied to the arithmetic provers implicitly.
wenzelm@26849
  2045
wenzelm@40406
  2046
  The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}} attribute declares case split
wenzelm@30865
  2047
  rules to be expanded before \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} is invoked.
nipkow@30863
  2048
nipkow@30863
  2049
  Note that a simpler (but faster) arithmetic prover is
nipkow@30863
  2050
  already invoked by the Simplifier.%
wenzelm@26849
  2051
\end{isamarkuptext}%
wenzelm@26849
  2052
\isamarkuptrue%
wenzelm@26849
  2053
%
wenzelm@30172
  2054
\isamarkupsection{Intuitionistic proof search%
wenzelm@30172
  2055
}
wenzelm@30172
  2056
\isamarkuptrue%
wenzelm@30172
  2057
%
wenzelm@30172
  2058
\begin{isamarkuptext}%
wenzelm@30172
  2059
\begin{matharray}{rcl}
wenzelm@30172
  2060
    \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\
wenzelm@30172
  2061
  \end{matharray}
wenzelm@30172
  2062
wenzelm@42596
  2063
  \begin{railoutput}
wenzelm@42662
  2064
\rail@begin{2}{}
wenzelm@42596
  2065
\rail@term{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}}[]
wenzelm@42596
  2066
\rail@plus
wenzelm@42596
  2067
\rail@nextplus{1}
wenzelm@42596
  2068
\rail@cnont{\hyperlink{syntax.rulemod}{\mbox{\isa{rulemod}}}}[]
wenzelm@42596
  2069
\rail@endplus
wenzelm@42596
  2070
\rail@end
wenzelm@42596
  2071
\end{railoutput}
wenzelm@42596
  2072
wenzelm@30172
  2073
wenzelm@30172
  2074
  The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
wenzelm@30172
  2075
  search, depending on specifically declared rules from the context,
wenzelm@30172
  2076
  or given as explicit arguments.  Chained facts are inserted into the
wenzelm@35613
  2077
  goal before commencing proof search.
wenzelm@35613
  2078
wenzelm@30172
  2079
  Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
wenzelm@30172
  2080
  \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
wenzelm@40406
  2081
  ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' indicator refers to ``safe'' rules, which may be
wenzelm@30172
  2082
  applied aggressively (without considering back-tracking later).
wenzelm@40406
  2083
  Rules declared with ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' are ignored in proof search (the
wenzelm@42626
  2084
  single-step \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method still observes these).  An
wenzelm@30172
  2085
  explicit weight annotation may be given as well; otherwise the
wenzelm@30172
  2086
  number of rule premises will be taken into account here.%
wenzelm@30172
  2087
\end{isamarkuptext}%
wenzelm@30172
  2088
\isamarkuptrue%
wenzelm@30172
  2089
%
blanchet@43578
  2090
\isamarkupsection{Model Elimination and Resolution%
blanchet@43578
  2091
}
blanchet@43578
  2092
\isamarkuptrue%
blanchet@43578
  2093
%
blanchet@43578
  2094
\begin{isamarkuptext}%
blanchet@43578
  2095
\begin{matharray}{rcl}
blanchet@43578
  2096
    \indexdef{HOL}{method}{meson}\hypertarget{method.HOL.meson}{\hyperlink{method.HOL.meson}{\mbox{\isa{meson}}}} & : & \isa{method} \\
blanchet@43578
  2097
    \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
blanchet@43578
  2098
  \end{matharray}
blanchet@43578
  2099
blanchet@43578
  2100
  \begin{railoutput}
blanchet@43578
  2101
\rail@begin{2}{}
blanchet@43578
  2102
\rail@term{\hyperlink{method.HOL.meson}{\mbox{\isa{meson}}}}[]
blanchet@43578
  2103
\rail@bar
blanchet@43578
  2104
\rail@nextbar{1}
blanchet@43578
  2105
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
blanchet@43578
  2106
\rail@endbar
blanchet@43578
  2107
\rail@end
blanchet@43578
  2108
\rail@begin{5}{}
blanchet@43578
  2109
\rail@term{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}}[]
blanchet@43578
  2110
\rail@bar
blanchet@43578
  2111
\rail@nextbar{1}
blanchet@43578
  2112
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
blanchet@43578
  2113
\rail@bar
blanchet@43578
  2114
\rail@term{\isa{partial{\isaliteral{5F}{\isacharunderscore}}types}}[]
blanchet@43578
  2115
\rail@nextbar{2}
blanchet@43578
  2116
\rail@term{\isa{full{\isaliteral{5F}{\isacharunderscore}}types}}[]
blanchet@43578
  2117
\rail@nextbar{3}
blanchet@43578
  2118
\rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}types}}[]
blanchet@43578
  2119
\rail@nextbar{4}
blanchet@43578
  2120
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
blanchet@43578
  2121
\rail@endbar
blanchet@43578
  2122
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
blanchet@43578
  2123
\rail@endbar
blanchet@43578
  2124
\rail@bar
blanchet@43578
  2125
\rail@nextbar{1}
blanchet@43578
  2126
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
blanchet@43578
  2127
\rail@endbar
blanchet@43578
  2128
\rail@end
blanchet@43578
  2129
\end{railoutput}
blanchet@43578
  2130
blanchet@43578
  2131
blanchet@43578
  2132
  The \hyperlink{method.HOL.meson}{\mbox{\isa{meson}}} method implements Loveland's model elimination
blanchet@43578
  2133
  procedure \cite{loveland-78}. See \verb|~~/src/HOL/ex/Meson_Test.thy| for
blanchet@43578
  2134
  examples.
blanchet@43578
  2135
blanchet@43578
  2136
  The \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}} method combines ordered resolution and ordered
blanchet@43578
  2137
  paramodulation to find first-order (or mildly higher-order) proofs. The first
blanchet@43578
  2138
  optional argument specifies a type encoding; see the Sledgehammer manual
blanchet@43578
  2139
  \cite{isabelle-sledgehammer} for details. The \verb|~~/src/HOL/Metis_Examples| directory contains several small theories
blanchet@43578
  2140
  developed to a large extent using Metis.%
blanchet@43578
  2141
\end{isamarkuptext}%
blanchet@43578
  2142
\isamarkuptrue%
blanchet@43578
  2143
%
wenzelm@30172
  2144
\isamarkupsection{Coherent Logic%
wenzelm@30172
  2145
}
wenzelm@30172
  2146
\isamarkuptrue%
wenzelm@30172
  2147
%
wenzelm@30172
  2148
\begin{isamarkuptext}%
wenzelm@30172
  2149
\begin{matharray}{rcl}
wenzelm@30172
  2150
    \indexdef{HOL}{method}{coherent}\hypertarget{method.HOL.coherent}{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}} & : & \isa{method} \\
wenzelm@30172
  2151
  \end{matharray}
wenzelm@30172
  2152
wenzelm@42596
  2153
  \begin{railoutput}
wenzelm@42662
  2154
\rail@begin{2}{}
wenzelm@42596
  2155
\rail@term{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}}[]
wenzelm@42596
  2156
\rail@bar
wenzelm@42596
  2157
\rail@nextbar{1}
wenzelm@42596
  2158
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
wenzelm@42596
  2159
\rail@endbar
wenzelm@42596
  2160
\rail@end
wenzelm@42596
  2161
\end{railoutput}
wenzelm@42596
  2162
wenzelm@30172
  2163
wenzelm@30172
  2164
  The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
wenzelm@30172
  2165
  \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
wenzelm@30172
  2166
  applications in confluence theory, lattice theory and projective
wenzelm@40802
  2167
  geometry.  See \verb|~~/src/HOL/ex/Coherent.thy| for some
wenzelm@30172
  2168
  examples.%
wenzelm@30172
  2169
\end{isamarkuptext}%
wenzelm@30172
  2170
\isamarkuptrue%
wenzelm@30172
  2171
%
blanchet@42215
  2172
\isamarkupsection{Proving propositions%
blanchet@42215
  2173
}
blanchet@42215
  2174
\isamarkuptrue%
blanchet@42215
  2175
%
blanchet@42215
  2176
\begin{isamarkuptext}%
blanchet@42215
  2177
In addition to the standard proof methods, a number of diagnosis
blanchet@42215
  2178
  tools search for proofs and provide an Isar proof snippet on success.
blanchet@42215
  2179
  These tools are available via the following commands.
blanchet@42215
  2180
blanchet@42215
  2181
  \begin{matharray}{rcl}
blanchet@42215
  2182
    \indexdef{HOL}{command}{solve\_direct}\hypertarget{command.HOL.solve-direct}{\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
blanchet@42215
  2183
    \indexdef{HOL}{command}{try}\hypertarget{command.HOL.try}{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
blanchet@43040
  2184
    \indexdef{HOL}{command}{try\_methods}\hypertarget{command.HOL.try-methods}{\hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
blanchet@42215
  2185
    \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
blanchet@42215
  2186
    \indexdef{HOL}{command}{sledgehammer\_params}\hypertarget{command.HOL.sledgehammer-params}{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
blanchet@42215
  2187
  \end{matharray}
blanchet@42215
  2188
wenzelm@42596
  2189
  \begin{railoutput}
blanchet@43040
  2190
\rail@begin{1}{}
blanchet@43040
  2191
\rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
blanchet@43040
  2192
\rail@end
wenzelm@42662
  2193
\rail@begin{6}{}
blanchet@43040
  2194
\rail@term{\hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}}[]
wenzelm@42596
  2195
\rail@bar
wenzelm@42596
  2196
\rail@nextbar{1}
wenzelm@42596
  2197
\rail@plus
wenzelm@42596
  2198
\rail@bar
wenzelm@42596
  2199
\rail@term{\isa{simp}}[]
wenzelm@42596
  2200
\rail@nextbar{2}
wenzelm@42596
  2201
\rail@term{\isa{intro}