1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Jun 08 08:47:43 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Jun 08 10:24:07 2011 +0200
1.3 @@ -22,131 +22,1160 @@
1.4 }
1.5 \isamarkuptrue%
1.6 %
1.7 -\isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}%
1.8 +\isamarkupsection{Higher-Order Logic%
1.9 +}
1.10 +\isamarkuptrue%
1.11 +%
1.12 +\begin{isamarkuptext}%
1.13 +Isabelle/HOL is based on Higher-Order Logic, a polymorphic
1.14 + version of Church's Simple Theory of Types. HOL can be best
1.15 + understood as a simply-typed version of classical set theory. The
1.16 + logic was first implemented in Gordon's HOL system
1.17 + \cite{mgordon-hol}. It extends Church's original logic
1.18 + \cite{church40} by explicit type variables (naive polymorphism) and
1.19 + a sound axiomatization scheme for new types based on subsets of
1.20 + existing types.
1.21 +
1.22 + Andrews's book \cite{andrews86} is a full description of the
1.23 + original Church-style higher-order logic, with proofs of correctness
1.24 + and completeness wrt.\ certain set-theoretic interpretations. The
1.25 + particular extensions of Gordon-style HOL are explained semantically
1.26 + in two chapters of the 1993 HOL book \cite{pitts93}.
1.27 +
1.28 + Experience with HOL over decades has demonstrated that higher-order
1.29 + logic is widely applicable in many areas of mathematics and computer
1.30 + science. In a sense, Higher-Order Logic is simpler than First-Order
1.31 + Logic, because there are fewer restrictions and special cases. Note
1.32 + that HOL is \emph{weaker} than FOL with axioms for ZF set theory,
1.33 + which is traditionally considered the standard foundation of regular
1.34 + mathematics, but for most applications this does not matter. If you
1.35 + prefer ML to Lisp, you will probably prefer HOL to ZF.
1.36 +
1.37 + \medskip The syntax of HOL follows \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-calculus and
1.38 + functional programming. Function application is curried. To apply
1.39 + 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
1.40 + 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
1.41 + existing application of the Pure \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-calculus is re-used.
1.42 + 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
1.43 + 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
1.44 + be avoided by currying functions by default. Explicit tuples are as
1.45 + infrequent in HOL formalizations as in good ML or Haskell programs.
1.46 +
1.47 + \medskip Isabelle/HOL has a distinct feel, compared to other
1.48 + object-logics like Isabelle/ZF. It identifies object-level types
1.49 + with meta-level types, taking advantage of the default
1.50 + type-inference mechanism of Isabelle/Pure. HOL fully identifies
1.51 + object-level functions with meta-level functions, with native
1.52 + abstraction and application.
1.53 +
1.54 + These identifications allow Isabelle to support HOL particularly
1.55 + nicely, but they also mean that HOL requires some sophistication
1.56 + from the user. In particular, an understanding of Hindley-Milner
1.57 + type-inference with type-classes, which are both used extensively in
1.58 + the standard libraries and applications. Beginners can set
1.59 + \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
1.60 + explicit information about the result of type-inference.%
1.61 +\end{isamarkuptext}%
1.62 +\isamarkuptrue%
1.63 +%
1.64 +\isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
1.65 +}
1.66 +\isamarkuptrue%
1.67 +%
1.68 +\begin{isamarkuptext}%
1.69 +An \emph{inductive definition} specifies the least predicate
1.70 + or set \isa{R} closed under given rules: applying a rule to
1.71 + elements of \isa{R} yields a result within \isa{R}. For
1.72 + example, a structural operational semantics is an inductive
1.73 + definition of an evaluation relation.
1.74 +
1.75 + Dually, a \emph{coinductive definition} specifies the greatest
1.76 + predicate or set \isa{R} that is consistent with given rules:
1.77 + every element of \isa{R} can be seen as arising by applying a rule
1.78 + to elements of \isa{R}. An important example is using
1.79 + bisimulation relations to formalise equivalence of processes and
1.80 + infinite data structures.
1.81 +
1.82 + Both inductive and coinductive definitions are based on the
1.83 + Knaster-Tarski fixed-point theorem for complete lattices. The
1.84 + collection of introduction rules given by the user determines a
1.85 + functor on subsets of set-theoretic relations. The required
1.86 + monotonicity of the recursion scheme is proven as a prerequisite to
1.87 + the fixed-point definition and the resulting consequences. This
1.88 + works by pushing inclusion through logical connectives and any other
1.89 + operator that might be wrapped around recursive occurrences of the
1.90 + defined relation: there must be a monotonicity theorem of the form
1.91 + \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
1.92 + introduction rule. The default rule declarations of Isabelle/HOL
1.93 + already take care of most common situations.
1.94 +
1.95 + \begin{matharray}{rcl}
1.96 + \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}}} \\
1.97 + \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}}} \\
1.98 + \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}}} \\
1.99 + \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}}} \\
1.100 + \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
1.101 + \end{matharray}
1.102 +
1.103 + \begin{railoutput}
1.104 +\rail@begin{10}{}
1.105 +\rail@bar
1.106 +\rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
1.107 +\rail@nextbar{1}
1.108 +\rail@term{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1.109 +\rail@nextbar{2}
1.110 +\rail@term{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]
1.111 +\rail@nextbar{3}
1.112 +\rail@term{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1.113 +\rail@endbar
1.114 +\rail@bar
1.115 +\rail@nextbar{1}
1.116 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.117 +\rail@endbar
1.118 +\rail@cr{5}
1.119 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.120 +\rail@bar
1.121 +\rail@nextbar{6}
1.122 +\rail@term{\isa{\isakeyword{for}}}[]
1.123 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.124 +\rail@endbar
1.125 +\rail@bar
1.126 +\rail@nextbar{6}
1.127 +\rail@term{\isa{\isakeyword{where}}}[]
1.128 +\rail@nont{\isa{clauses}}[]
1.129 +\rail@endbar
1.130 +\rail@cr{8}
1.131 +\rail@bar
1.132 +\rail@nextbar{9}
1.133 +\rail@term{\isa{\isakeyword{monos}}}[]
1.134 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.135 +\rail@endbar
1.136 +\rail@end
1.137 +\rail@begin{3}{\isa{clauses}}
1.138 +\rail@plus
1.139 +\rail@bar
1.140 +\rail@nextbar{1}
1.141 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.142 +\rail@endbar
1.143 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.144 +\rail@nextplus{2}
1.145 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.146 +\rail@endplus
1.147 +\rail@end
1.148 +\rail@begin{3}{}
1.149 +\rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
1.150 +\rail@bar
1.151 +\rail@nextbar{1}
1.152 +\rail@term{\isa{add}}[]
1.153 +\rail@nextbar{2}
1.154 +\rail@term{\isa{del}}[]
1.155 +\rail@endbar
1.156 +\rail@end
1.157 +\end{railoutput}
1.158 +
1.159 +
1.160 + \begin{description}
1.161 +
1.162 + \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
1.163 + rules.
1.164 +
1.165 + 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
1.166 + (with arbitrary nesting), or equalities using \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}}. The
1.167 + latter specifies extra-logical abbreviations in the sense of
1.168 + \indexref{}{command}{abbreviation}\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}. Introducing abstract syntax
1.169 + simultaneously with the actual introduction rules is occasionally
1.170 + useful for complex specifications.
1.171 +
1.172 + The optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of
1.173 + the (co)inductive predicates that remain fixed throughout the
1.174 + definition, in contrast to arguments of the relation that may vary
1.175 + in each occurrence within the given \isa{{\isaliteral{22}{\isachardoublequote}}clauses{\isaliteral{22}{\isachardoublequote}}}.
1.176 +
1.177 + The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} declaration contains additional
1.178 + \emph{monotonicity theorems}, which are required for each operator
1.179 + applied to a recursive set in the introduction rules.
1.180 +
1.181 + \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
1.182 + native HOL predicates. This allows to define (co)inductive sets,
1.183 + where multiple arguments are simulated via tuples.
1.184 +
1.185 + \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules in the
1.186 + context. These rule are involved in the automated monotonicity
1.187 + proof of the above inductive and coinductive definitions.
1.188 +
1.189 + \end{description}%
1.190 +\end{isamarkuptext}%
1.191 +\isamarkuptrue%
1.192 +%
1.193 +\isamarkupsubsection{Derived rules%
1.194 +}
1.195 +\isamarkuptrue%
1.196 +%
1.197 +\begin{isamarkuptext}%
1.198 +A (co)inductive definition of \isa{R} provides the following
1.199 + main theorems:
1.200 +
1.201 + \begin{description}
1.202 +
1.203 + \item \isa{R{\isaliteral{2E}{\isachardot}}intros} is the list of introduction rules as proven
1.204 + theorems, for the recursive predicates (or sets). The rules are
1.205 + also available individually, using the names given them in the
1.206 + theory file;
1.207 +
1.208 + \item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
1.209 +
1.210 + \item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
1.211 + rule.
1.212 +
1.213 + \end{description}
1.214 +
1.215 + 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
1.216 + defined simultaneously, the list of introduction rules is called
1.217 + \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
1.218 + 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
1.219 + 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}}}.%
1.220 +\end{isamarkuptext}%
1.221 +\isamarkuptrue%
1.222 +%
1.223 +\isamarkupsubsection{Monotonicity theorems%
1.224 +}
1.225 +\isamarkuptrue%
1.226 +%
1.227 +\begin{isamarkuptext}%
1.228 +The context maintains a default set of theorems that are used
1.229 + in monotonicity proofs. New rules can be declared via the
1.230 + \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute. See the main Isabelle/HOL
1.231 + sources for some examples. The general format of such monotonicity
1.232 + theorems is as follows:
1.233 +
1.234 + \begin{itemize}
1.235 +
1.236 + \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
1.237 + monotonicity of inductive definitions whose introduction rules have
1.238 + premises involving terms such as \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4D3E}{\isasymM}}\ R\ t{\isaliteral{22}{\isachardoublequote}}}.
1.239 +
1.240 + \item Monotonicity theorems for logical operators, which are of the
1.241 + 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
1.242 + the case of the operator \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, the corresponding theorem is
1.243 + \[
1.244 + \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}}}}
1.245 + \]
1.246 +
1.247 + \item De Morgan style equations for reasoning about the ``polarity''
1.248 + of expressions, e.g.
1.249 + \[
1.250 + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ P{\isaliteral{22}{\isachardoublequote}}} \qquad\qquad
1.251 + \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}}}
1.252 + \]
1.253 +
1.254 + \item Equations for reducing complex operators to more primitive
1.255 + ones whose monotonicity can easily be proved, e.g.
1.256 + \[
1.257 + \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
1.258 + \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}}}
1.259 + \]
1.260 +
1.261 + \end{itemize}%
1.262 +\end{isamarkuptext}%
1.263 +\isamarkuptrue%
1.264 +%
1.265 +\isamarkupsubsubsection{Examples%
1.266 +}
1.267 +\isamarkuptrue%
1.268 +%
1.269 +\begin{isamarkuptext}%
1.270 +The finite powerset operator can be defined inductively like this:%
1.271 +\end{isamarkuptext}%
1.272 +\isamarkuptrue%
1.273 +\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
1.274 +\ 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
1.275 +\isakeyword{where}\isanewline
1.276 +\ \ empty{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Fin\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.277 +{\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}}%
1.278 +\begin{isamarkuptext}%
1.279 +The accessible part of a relation is defined as follows:%
1.280 +\end{isamarkuptext}%
1.281 +\isamarkuptrue%
1.282 +\isacommand{inductive}\isamarkupfalse%
1.283 +\ 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
1.284 +\ \ \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
1.285 +\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}}%
1.286 +\begin{isamarkuptext}%
1.287 +Common logical connectives can be easily characterized as
1.288 +non-recursive inductive definitions with parameters, but without
1.289 +arguments.%
1.290 +\end{isamarkuptext}%
1.291 +\isamarkuptrue%
1.292 +\isacommand{inductive}\isamarkupfalse%
1.293 +\ AND\ \isakeyword{for}\ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\isanewline
1.294 +\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ AND\ A\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.295 +\isanewline
1.296 +\isacommand{inductive}\isamarkupfalse%
1.297 +\ OR\ \isakeyword{for}\ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\isanewline
1.298 +\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ OR\ A\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.299 +\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ OR\ A\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.300 +\isanewline
1.301 +\isacommand{inductive}\isamarkupfalse%
1.302 +\ 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
1.303 +\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ EXISTS\ B{\isaliteral{22}{\isachardoublequoteclose}}%
1.304 +\begin{isamarkuptext}%
1.305 +Here the \isa{{\isaliteral{22}{\isachardoublequote}}cases{\isaliteral{22}{\isachardoublequote}}} or \isa{{\isaliteral{22}{\isachardoublequote}}induct{\isaliteral{22}{\isachardoublequote}}} rules produced by
1.306 + the \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} package coincide with the expected
1.307 + elimination rules for Natural Deduction. Already in the original
1.308 + article by Gerhard Gentzen \cite{Gentzen:1935} there is a hint that
1.309 + each connective can be characterized by its introductions, and the
1.310 + elimination can be constructed systematically.%
1.311 +\end{isamarkuptext}%
1.312 +\isamarkuptrue%
1.313 +%
1.314 +\isamarkupsection{Recursive functions \label{sec:recursion}%
1.315 }
1.316 \isamarkuptrue%
1.317 %
1.318 \begin{isamarkuptext}%
1.319 \begin{matharray}{rcl}
1.320 - \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}}} \\
1.321 + \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}}} \\
1.322 + \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}}} \\
1.323 + \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}}} \\
1.324 + \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}}} \\
1.325 \end{matharray}
1.326
1.327 \begin{railoutput}
1.328 \rail@begin{2}{}
1.329 -\rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
1.330 +\rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
1.331 \rail@bar
1.332 \rail@nextbar{1}
1.333 -\rail@nont{\isa{altname}}[]
1.334 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.335 \rail@endbar
1.336 -\rail@nont{\isa{abstype}}[]
1.337 -\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.338 -\rail@nont{\isa{repset}}[]
1.339 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.340 +\rail@term{\isa{\isakeyword{where}}}[]
1.341 +\rail@nont{\isa{equations}}[]
1.342 \rail@end
1.343 -\rail@begin{3}{\isa{altname}}
1.344 +\rail@begin{4}{}
1.345 +\rail@bar
1.346 +\rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
1.347 +\rail@nextbar{1}
1.348 +\rail@term{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}}[]
1.349 +\rail@endbar
1.350 +\rail@bar
1.351 +\rail@nextbar{1}
1.352 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.353 +\rail@endbar
1.354 +\rail@bar
1.355 +\rail@nextbar{1}
1.356 +\rail@nont{\isa{functionopts}}[]
1.357 +\rail@endbar
1.358 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.359 +\rail@cr{3}
1.360 +\rail@term{\isa{\isakeyword{where}}}[]
1.361 +\rail@nont{\isa{equations}}[]
1.362 +\rail@end
1.363 +\rail@begin{3}{\isa{equations}}
1.364 +\rail@plus
1.365 +\rail@bar
1.366 +\rail@nextbar{1}
1.367 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.368 +\rail@endbar
1.369 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.370 +\rail@nextplus{2}
1.371 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.372 +\rail@endplus
1.373 +\rail@end
1.374 +\rail@begin{3}{\isa{functionopts}}
1.375 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.376 +\rail@plus
1.377 \rail@bar
1.378 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.379 +\rail@term{\isa{sequential}}[]
1.380 \rail@nextbar{1}
1.381 -\rail@term{\isa{\isakeyword{open}}}[]
1.382 -\rail@nextbar{2}
1.383 -\rail@term{\isa{\isakeyword{open}}}[]
1.384 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.385 +\rail@term{\isa{domintros}}[]
1.386 \rail@endbar
1.387 +\rail@nextplus{2}
1.388 +\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
1.389 +\rail@endplus
1.390 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.391 \rail@end
1.392 -\rail@begin{2}{\isa{abstype}}
1.393 -\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
1.394 +\rail@begin{2}{}
1.395 +\rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
1.396 +\rail@bar
1.397 +\rail@nextbar{1}
1.398 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.399 +\rail@endbar
1.400 +\rail@end
1.401 +\end{railoutput}
1.402 +
1.403 +
1.404 + \begin{description}
1.405 +
1.406 + \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
1.407 + functions over datatypes (see also \indexref{HOL}{command}{datatype}\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} and
1.408 + \indexref{HOL}{command}{rep\_datatype}\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}). The given \isa{equations}
1.409 + specify reduction rules that are produced by instantiating the
1.410 + generic combinator for primitive recursion that is available for
1.411 + each datatype.
1.412 +
1.413 + Each equation needs to be of the form:
1.414 +
1.415 + \begin{isabelle}%
1.416 +{\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}}%
1.417 +\end{isabelle}
1.418 +
1.419 + such that \isa{C} is a datatype constructor, \isa{rhs} contains
1.420 + only the free variables on the left-hand side (or from the context),
1.421 + and all recursive occurrences of \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} in \isa{{\isaliteral{22}{\isachardoublequote}}rhs{\isaliteral{22}{\isachardoublequote}}} are of
1.422 + 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
1.423 + reduction rule for each constructor can be given. The order does
1.424 + not matter. For missing constructors, the function is defined to
1.425 + return a default value, but this equation is made difficult to
1.426 + access for users.
1.427 +
1.428 + The reduction rules are declared as \hyperlink{attribute.simp}{\mbox{\isa{simp}}} by default,
1.429 + which enables standard proof methods like \hyperlink{method.simp}{\mbox{\isa{simp}}} and
1.430 + \hyperlink{method.auto}{\mbox{\isa{auto}}} to normalize expressions of \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} applied to
1.431 + datatype constructions, by simulating symbolic computation via
1.432 + rewriting.
1.433 +
1.434 + \item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
1.435 + wellfounded recursion. A detailed description with examples can be
1.436 + found in \cite{isabelle-function}. The function is specified by a
1.437 + set of (possibly conditional) recursive equations with arbitrary
1.438 + pattern matching. The command generates proof obligations for the
1.439 + completeness and the compatibility of patterns.
1.440 +
1.441 + The defined function is considered partial, and the resulting
1.442 + simplification rules (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}psimps{\isaliteral{22}{\isachardoublequote}}}) and induction rule
1.443 + (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}pinduct{\isaliteral{22}{\isachardoublequote}}}) are guarded by a generated domain
1.444 + predicate \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5F}{\isacharunderscore}}dom{\isaliteral{22}{\isachardoublequote}}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}
1.445 + command can then be used to establish that the function is total.
1.446 +
1.447 + \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
1.448 + proof attempts regarding pattern matching and termination. See
1.449 + \cite{isabelle-function} for further details.
1.450 +
1.451 + \item \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f} commences a
1.452 + termination proof for the previously defined function \isa{f}. If
1.453 + this is omitted, the command refers to the most recent function
1.454 + definition. After the proof is closed, the recursive equations and
1.455 + the induction principle is established.
1.456 +
1.457 + \end{description}
1.458 +
1.459 + Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
1.460 + command accommodate reasoning by induction (cf.\ \hyperlink{method.induct}{\mbox{\isa{induct}}}):
1.461 + rule \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}induct{\isaliteral{22}{\isachardoublequote}}} refers to a specific induction rule, with
1.462 + parameters named according to the user-specified equations. Cases
1.463 + are numbered starting from 1. For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the
1.464 + induction principle coincides with structural recursion on the
1.465 + datatype where the recursion is carried out.
1.466 +
1.467 + The equations provided by these packages may be referred later as
1.468 + theorem list \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, where \isa{f} is the (collective)
1.469 + name of the functions defined. Individual equations may be named
1.470 + explicitly as well.
1.471 +
1.472 + The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following
1.473 + options.
1.474 +
1.475 + \begin{description}
1.476 +
1.477 + \item \isa{sequential} enables a preprocessor which disambiguates
1.478 + overlapping patterns by making them mutually disjoint. Earlier
1.479 + equations take precedence over later ones. This allows to give the
1.480 + specification in a format very similar to functional programming.
1.481 + Note that the resulting simplification and induction rules
1.482 + correspond to the transformed specification, not the one given
1.483 + originally. This usually means that each equation given by the user
1.484 + may result in several theorems. Also note that this automatic
1.485 + transformation only works for ML-style datatype patterns.
1.486 +
1.487 + \item \isa{domintros} enables the automated generation of
1.488 + introduction rules for the domain predicate. While mostly not
1.489 + needed, they can be helpful in some proofs about partial functions.
1.490 +
1.491 + \end{description}%
1.492 +\end{isamarkuptext}%
1.493 +\isamarkuptrue%
1.494 +%
1.495 +\isamarkupsubsubsection{Example: evaluation of expressions%
1.496 +}
1.497 +\isamarkuptrue%
1.498 +%
1.499 +\begin{isamarkuptext}%
1.500 +Subsequently, we define mutual datatypes for arithmetic and
1.501 + boolean expressions, and use \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} for evaluation
1.502 + functions that follow the same recursive structure.%
1.503 +\end{isamarkuptext}%
1.504 +\isamarkuptrue%
1.505 +\isacommand{datatype}\isamarkupfalse%
1.506 +\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.507 +\ \ \ \ 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
1.508 +\ \ {\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
1.509 +\ \ {\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
1.510 +\ \ {\isaliteral{7C}{\isacharbar}}\ Var\ {\isaliteral{27}{\isacharprime}}a\isanewline
1.511 +\ \ {\isaliteral{7C}{\isacharbar}}\ Num\ nat\isanewline
1.512 +\isakeyword{and}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.513 +\ \ \ \ Less\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.514 +\ \ {\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
1.515 +\ \ {\isaliteral{7C}{\isacharbar}}\ Neg\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}%
1.516 +\begin{isamarkuptext}%
1.517 +\medskip Evaluation of arithmetic and boolean expressions%
1.518 +\end{isamarkuptext}%
1.519 +\isamarkuptrue%
1.520 +\isacommand{primrec}\isamarkupfalse%
1.521 +\ 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
1.522 +\ \ \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
1.523 +\isakeyword{where}\isanewline
1.524 +\ \ {\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
1.525 +{\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
1.526 +{\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
1.527 +{\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
1.528 +{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.529 +{\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
1.530 +{\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
1.531 +{\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}}%
1.532 +\begin{isamarkuptext}%
1.533 +Since the value of an expression depends on the value of its
1.534 + variables, the functions \isa{evala} and \isa{evalb} take an
1.535 + additional parameter, an \emph{environment} that maps variables to
1.536 + their values.
1.537 +
1.538 + \medskip Substitution on expressions can be defined similarly. The
1.539 + 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
1.540 + parameter is lifted canonically on the types \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequote}}} and
1.541 + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequote}}}, respectively.%
1.542 +\end{isamarkuptext}%
1.543 +\isamarkuptrue%
1.544 +\isacommand{primrec}\isamarkupfalse%
1.545 +\ 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
1.546 +\ \ \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
1.547 +\isakeyword{where}\isanewline
1.548 +\ \ {\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
1.549 +{\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
1.550 +{\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
1.551 +{\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
1.552 +{\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
1.553 +{\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
1.554 +{\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
1.555 +{\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}}%
1.556 +\begin{isamarkuptext}%
1.557 +In textbooks about semantics one often finds substitution
1.558 + theorems, which express the relationship between substitution and
1.559 + 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
1.560 + such a theorem by mutual induction, followed by simplification.%
1.561 +\end{isamarkuptext}%
1.562 +\isamarkuptrue%
1.563 +\isacommand{lemma}\isamarkupfalse%
1.564 +\ subst{\isaliteral{5F}{\isacharunderscore}}one{\isaliteral{3A}{\isacharcolon}}\isanewline
1.565 +\ \ {\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
1.566 +\ \ {\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
1.567 +%
1.568 +\isadelimproof
1.569 +\ \ %
1.570 +\endisadelimproof
1.571 +%
1.572 +\isatagproof
1.573 +\isacommand{by}\isamarkupfalse%
1.574 +\ {\isaliteral{28}{\isacharparenleft}}induct\ a\ \isakeyword{and}\ b{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
1.575 +\endisatagproof
1.576 +{\isafoldproof}%
1.577 +%
1.578 +\isadelimproof
1.579 +\isanewline
1.580 +%
1.581 +\endisadelimproof
1.582 +\isanewline
1.583 +\isacommand{lemma}\isamarkupfalse%
1.584 +\ subst{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{3A}{\isacharcolon}}\isanewline
1.585 +\ \ {\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
1.586 +\ \ {\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
1.587 +%
1.588 +\isadelimproof
1.589 +\ \ %
1.590 +\endisadelimproof
1.591 +%
1.592 +\isatagproof
1.593 +\isacommand{by}\isamarkupfalse%
1.594 +\ {\isaliteral{28}{\isacharparenleft}}induct\ a\ \isakeyword{and}\ b{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
1.595 +\endisatagproof
1.596 +{\isafoldproof}%
1.597 +%
1.598 +\isadelimproof
1.599 +%
1.600 +\endisadelimproof
1.601 +%
1.602 +\isamarkupsubsubsection{Example: a substitution function for terms%
1.603 +}
1.604 +\isamarkuptrue%
1.605 +%
1.606 +\begin{isamarkuptext}%
1.607 +Functions on datatypes with nested recursion are also defined
1.608 + by mutual primitive recursion.%
1.609 +\end{isamarkuptext}%
1.610 +\isamarkuptrue%
1.611 +\isacommand{datatype}\isamarkupfalse%
1.612 +\ {\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}}%
1.613 +\begin{isamarkuptext}%
1.614 +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
1.615 + 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}}}:%
1.616 +\end{isamarkuptext}%
1.617 +\isamarkuptrue%
1.618 +\isacommand{primrec}\isamarkupfalse%
1.619 +\ 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
1.620 +\ \ 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
1.621 +\isakeyword{where}\isanewline
1.622 +\ \ {\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
1.623 +{\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
1.624 +{\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
1.625 +{\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}}%
1.626 +\begin{isamarkuptext}%
1.627 +The recursion scheme follows the structure of the unfolded
1.628 + 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
1.629 + substitution function, mutual induction is needed:%
1.630 +\end{isamarkuptext}%
1.631 +\isamarkuptrue%
1.632 +\isacommand{lemma}\isamarkupfalse%
1.633 +\ {\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
1.634 +\ \ {\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
1.635 +%
1.636 +\isadelimproof
1.637 +\ \ %
1.638 +\endisadelimproof
1.639 +%
1.640 +\isatagproof
1.641 +\isacommand{by}\isamarkupfalse%
1.642 +\ {\isaliteral{28}{\isacharparenleft}}induct\ t\ \isakeyword{and}\ ts{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
1.643 +\endisatagproof
1.644 +{\isafoldproof}%
1.645 +%
1.646 +\isadelimproof
1.647 +%
1.648 +\endisadelimproof
1.649 +%
1.650 +\isamarkupsubsubsection{Example: a map function for infinitely branching trees%
1.651 +}
1.652 +\isamarkuptrue%
1.653 +%
1.654 +\begin{isamarkuptext}%
1.655 +Defining functions on infinitely branching datatypes by
1.656 + primitive recursion is just as easy.%
1.657 +\end{isamarkuptext}%
1.658 +\isamarkuptrue%
1.659 +\isacommand{datatype}\isamarkupfalse%
1.660 +\ {\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
1.661 +\isanewline
1.662 +\isacommand{primrec}\isamarkupfalse%
1.663 +\ 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
1.664 +\isakeyword{where}\isanewline
1.665 +\ \ {\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
1.666 +{\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}}%
1.667 +\begin{isamarkuptext}%
1.668 +Note that all occurrences of functions such as \isa{ts}
1.669 + 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.%
1.670 +\end{isamarkuptext}%
1.671 +\isamarkuptrue%
1.672 +%
1.673 +\begin{isamarkuptext}%
1.674 +Here is a simple composition lemma for \isa{map{\isaliteral{5F}{\isacharunderscore}}tree}:%
1.675 +\end{isamarkuptext}%
1.676 +\isamarkuptrue%
1.677 +\isacommand{lemma}\isamarkupfalse%
1.678 +\ {\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
1.679 +%
1.680 +\isadelimproof
1.681 +\ \ %
1.682 +\endisadelimproof
1.683 +%
1.684 +\isatagproof
1.685 +\isacommand{by}\isamarkupfalse%
1.686 +\ {\isaliteral{28}{\isacharparenleft}}induct\ t{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
1.687 +\endisatagproof
1.688 +{\isafoldproof}%
1.689 +%
1.690 +\isadelimproof
1.691 +%
1.692 +\endisadelimproof
1.693 +%
1.694 +\isamarkupsubsection{Proof methods related to recursive definitions%
1.695 +}
1.696 +\isamarkuptrue%
1.697 +%
1.698 +\begin{isamarkuptext}%
1.699 +\begin{matharray}{rcl}
1.700 + \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}}} & : & \isa{method} \\
1.701 + \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
1.702 + \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}} & : & \isa{method} \\
1.703 + \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}} & : & \isa{method} \\
1.704 + \end{matharray}
1.705 +
1.706 + \begin{railoutput}
1.707 +\rail@begin{1}{}
1.708 +\rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
1.709 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.710 +\rail@end
1.711 +\rail@begin{2}{}
1.712 +\rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
1.713 +\rail@plus
1.714 +\rail@nextplus{1}
1.715 +\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.716 +\rail@endplus
1.717 +\rail@end
1.718 +\rail@begin{2}{}
1.719 +\rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
1.720 +\rail@nont{\isa{orders}}[]
1.721 +\rail@plus
1.722 +\rail@nextplus{1}
1.723 +\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.724 +\rail@endplus
1.725 +\rail@end
1.726 +\rail@begin{4}{\isa{orders}}
1.727 +\rail@plus
1.728 +\rail@nextplus{1}
1.729 +\rail@bar
1.730 +\rail@term{\isa{max}}[]
1.731 +\rail@nextbar{2}
1.732 +\rail@term{\isa{min}}[]
1.733 +\rail@nextbar{3}
1.734 +\rail@term{\isa{ms}}[]
1.735 +\rail@endbar
1.736 +\rail@endplus
1.737 +\rail@end
1.738 +\end{railoutput}
1.739 +
1.740 +
1.741 + \begin{description}
1.742 +
1.743 + \item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}} is a specialized method to
1.744 + solve goals regarding the completeness of pattern matching, as
1.745 + required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
1.746 + \cite{isabelle-function}).
1.747 +
1.748 + \item \hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R} introduces a termination
1.749 + proof using the relation \isa{R}. The resulting proof state will
1.750 + contain goals expressing that \isa{R} is wellfounded, and that the
1.751 + arguments of recursive calls decrease with respect to \isa{R}.
1.752 + Usually, this method is used as the initial proof step of manual
1.753 + termination proofs.
1.754 +
1.755 + \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}} attempts a fully
1.756 + automated termination proof by searching for a lexicographic
1.757 + combination of size measures on the arguments of the function. The
1.758 + method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
1.759 + 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}}}).
1.760 +
1.761 + In case of failure, extensive information is printed, which can help
1.762 + to analyse the situation (cf.\ \cite{isabelle-function}).
1.763 +
1.764 + \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}} also works on termination goals,
1.765 + using a variation of the size-change principle, together with a
1.766 + graph decomposition technique (see \cite{krauss_phd} for details).
1.767 + Three kinds of orders are used internally: \isa{max}, \isa{min},
1.768 + and \isa{ms} (multiset), which is only available when the theory
1.769 + \isa{Multiset} is loaded. When no order kinds are given, they are
1.770 + tried in order. The search for a termination proof uses SAT solving
1.771 + internally.
1.772 +
1.773 + For local descent proofs, the \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} modifiers are
1.774 + accepted (as for \hyperlink{method.auto}{\mbox{\isa{auto}}}).
1.775 +
1.776 + \end{description}%
1.777 +\end{isamarkuptext}%
1.778 +\isamarkuptrue%
1.779 +%
1.780 +\isamarkupsubsection{Functions with explicit partiality%
1.781 +}
1.782 +\isamarkuptrue%
1.783 +%
1.784 +\begin{isamarkuptext}%
1.785 +\begin{matharray}{rcl}
1.786 + \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}}} \\
1.787 + \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} \\
1.788 + \end{matharray}
1.789 +
1.790 + \begin{railoutput}
1.791 +\rail@begin{5}{}
1.792 +\rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
1.793 +\rail@bar
1.794 +\rail@nextbar{1}
1.795 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.796 +\rail@endbar
1.797 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.798 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.799 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.800 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.801 +\rail@cr{3}
1.802 +\rail@term{\isa{\isakeyword{where}}}[]
1.803 +\rail@bar
1.804 +\rail@nextbar{4}
1.805 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.806 +\rail@endbar
1.807 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.808 +\rail@end
1.809 +\end{railoutput}
1.810 +
1.811 +
1.812 + \begin{description}
1.813 +
1.814 + \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
1.815 + recursive functions based on fixpoints in complete partial
1.816 + orders. No termination proof is required from the user or
1.817 + constructed internally. Instead, the possibility of non-termination
1.818 + is modelled explicitly in the result type, which contains an
1.819 + explicit bottom element.
1.820 +
1.821 + Pattern matching and mutual recursion are currently not supported.
1.822 + Thus, the specification consists of a single function described by a
1.823 + single recursive equation.
1.824 +
1.825 + There are no fixed syntactic restrictions on the body of the
1.826 + function, but the induced functional must be provably monotonic
1.827 + wrt.\ the underlying order. The monotonicitity proof is performed
1.828 + internally, and the definition is rejected when it fails. The proof
1.829 + can be influenced by declaring hints using the
1.830 + \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} attribute.
1.831 +
1.832 + The mandatory \isa{mode} argument specifies the mode of operation
1.833 + of the command, which directly corresponds to a complete partial
1.834 + order on the result type. By default, the following modes are
1.835 + defined:
1.836 +
1.837 + \begin{description}
1.838 + \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
1.839 + non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
1.840 + must also be \isa{None}. This is best achieved through the use of
1.841 + the monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}.
1.842 +
1.843 + \item \isa{tailrec} defines functions with an arbitrary result
1.844 + 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
1.845 + if \isa{undefined} is returned by a recursive call, then the
1.846 + overall result must also be \isa{undefined}. In practice, this is
1.847 + only satisfied when each recursive call is a tail call, whose result
1.848 + is directly returned. Thus, this mode of operation allows the
1.849 + definition of arbitrary tail-recursive functions.
1.850 + \end{description}
1.851 +
1.852 + Experienced users may define new modes by instantiating the locale
1.853 + \isa{{\isaliteral{22}{\isachardoublequote}}partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}definitions{\isaliteral{22}{\isachardoublequote}}} appropriately.
1.854 +
1.855 + \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} declares rules for
1.856 + use in the internal monononicity proofs of partial function
1.857 + definitions.
1.858 +
1.859 + \end{description}%
1.860 +\end{isamarkuptext}%
1.861 +\isamarkuptrue%
1.862 +%
1.863 +\isamarkupsubsection{Old-style recursive function definitions (TFL)%
1.864 +}
1.865 +\isamarkuptrue%
1.866 +%
1.867 +\begin{isamarkuptext}%
1.868 +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.
1.869 +
1.870 + \begin{matharray}{rcl}
1.871 + \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}}} \\
1.872 + \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}}} \\
1.873 + \end{matharray}
1.874 +
1.875 + \begin{railoutput}
1.876 +\rail@begin{5}{}
1.877 +\rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
1.878 +\rail@bar
1.879 +\rail@nextbar{1}
1.880 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.881 +\rail@term{\isa{\isakeyword{permissive}}}[]
1.882 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.883 +\rail@endbar
1.884 +\rail@cr{3}
1.885 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.886 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.887 +\rail@plus
1.888 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.889 +\rail@nextplus{4}
1.890 +\rail@endplus
1.891 +\rail@bar
1.892 +\rail@nextbar{4}
1.893 +\rail@nont{\isa{hints}}[]
1.894 +\rail@endbar
1.895 +\rail@end
1.896 +\rail@begin{2}{}
1.897 +\rail@nont{\isa{recdeftc}}[]
1.898 +\rail@bar
1.899 +\rail@nextbar{1}
1.900 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.901 +\rail@endbar
1.902 +\rail@nont{\isa{tc}}[]
1.903 +\rail@end
1.904 +\rail@begin{2}{\isa{hints}}
1.905 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.906 +\rail@term{\isa{\isakeyword{hints}}}[]
1.907 +\rail@plus
1.908 +\rail@nextplus{1}
1.909 +\rail@cnont{\isa{recdefmod}}[]
1.910 +\rail@endplus
1.911 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.912 +\rail@end
1.913 +\rail@begin{4}{\isa{recdefmod}}
1.914 +\rail@bar
1.915 +\rail@bar
1.916 +\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}[]
1.917 +\rail@nextbar{1}
1.918 +\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}[]
1.919 +\rail@nextbar{2}
1.920 +\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}[]
1.921 +\rail@endbar
1.922 +\rail@bar
1.923 +\rail@nextbar{1}
1.924 +\rail@term{\isa{add}}[]
1.925 +\rail@nextbar{2}
1.926 +\rail@term{\isa{del}}[]
1.927 +\rail@endbar
1.928 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.929 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.930 +\rail@nextbar{3}
1.931 +\rail@nont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.932 +\rail@endbar
1.933 +\rail@end
1.934 +\rail@begin{2}{\isa{tc}}
1.935 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.936 +\rail@bar
1.937 +\rail@nextbar{1}
1.938 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.939 +\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.940 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.941 +\rail@endbar
1.942 +\rail@end
1.943 +\end{railoutput}
1.944 +
1.945 +
1.946 + \begin{description}
1.947 +
1.948 + \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
1.949 + recursive functions (using the TFL package), see also
1.950 + \cite{isabelle-HOL}. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells
1.951 + TFL to recover from failed proof attempts, returning unfinished
1.952 + 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
1.953 + automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}
1.954 + declarations may be given to tune the context of the Simplifier
1.955 + (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\
1.956 + \secref{sec:classical}).
1.957 +
1.958 + \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
1.959 + proof for leftover termination condition number \isa{i} (default
1.960 + 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
1.961 + constant \isa{c}.
1.962 +
1.963 + Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
1.964 + its internal proofs without manual intervention.
1.965 +
1.966 + \end{description}
1.967 +
1.968 + \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared
1.969 + globally, using the following attributes.
1.970 +
1.971 + \begin{matharray}{rcl}
1.972 + \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}} & : & \isa{attribute} \\
1.973 + \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}} & : & \isa{attribute} \\
1.974 + \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}} & : & \isa{attribute} \\
1.975 + \end{matharray}
1.976 +
1.977 + \begin{railoutput}
1.978 +\rail@begin{3}{}
1.979 +\rail@bar
1.980 +\rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
1.981 +\rail@nextbar{1}
1.982 +\rail@term{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}}[]
1.983 +\rail@nextbar{2}
1.984 +\rail@term{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}}[]
1.985 +\rail@endbar
1.986 +\rail@bar
1.987 +\rail@nextbar{1}
1.988 +\rail@term{\isa{add}}[]
1.989 +\rail@nextbar{2}
1.990 +\rail@term{\isa{del}}[]
1.991 +\rail@endbar
1.992 +\rail@end
1.993 +\end{railoutput}%
1.994 +\end{isamarkuptext}%
1.995 +\isamarkuptrue%
1.996 +%
1.997 +\isamarkupsection{Datatypes \label{sec:hol-datatype}%
1.998 +}
1.999 +\isamarkuptrue%
1.1000 +%
1.1001 +\begin{isamarkuptext}%
1.1002 +\begin{matharray}{rcl}
1.1003 + \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}}} \\
1.1004 + \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}}} \\
1.1005 + \end{matharray}
1.1006 +
1.1007 + \begin{railoutput}
1.1008 +\rail@begin{2}{}
1.1009 +\rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
1.1010 +\rail@plus
1.1011 +\rail@nont{\isa{spec}}[]
1.1012 +\rail@nextplus{1}
1.1013 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.1014 +\rail@endplus
1.1015 +\rail@end
1.1016 +\rail@begin{3}{}
1.1017 +\rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
1.1018 +\rail@bar
1.1019 +\rail@nextbar{1}
1.1020 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1021 +\rail@plus
1.1022 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1023 +\rail@nextplus{2}
1.1024 +\rail@endplus
1.1025 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1026 +\rail@endbar
1.1027 +\rail@plus
1.1028 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1029 +\rail@nextplus{1}
1.1030 +\rail@endplus
1.1031 +\rail@end
1.1032 +\rail@begin{2}{\isa{spec}}
1.1033 +\rail@bar
1.1034 +\rail@nextbar{1}
1.1035 +\rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
1.1036 +\rail@endbar
1.1037 +\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
1.1038 +\rail@bar
1.1039 +\rail@nextbar{1}
1.1040 +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.1041 +\rail@endbar
1.1042 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.1043 +\rail@plus
1.1044 +\rail@nont{\isa{cons}}[]
1.1045 +\rail@nextplus{1}
1.1046 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.1047 +\rail@endplus
1.1048 +\rail@end
1.1049 +\rail@begin{2}{\isa{cons}}
1.1050 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1051 +\rail@plus
1.1052 +\rail@nextplus{1}
1.1053 +\rail@cnont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
1.1054 +\rail@endplus
1.1055 \rail@bar
1.1056 \rail@nextbar{1}
1.1057 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.1058 \rail@endbar
1.1059 \rail@end
1.1060 -\rail@begin{2}{\isa{repset}}
1.1061 -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1062 -\rail@bar
1.1063 -\rail@nextbar{1}
1.1064 -\rail@term{\isa{\isakeyword{morphisms}}}[]
1.1065 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1066 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1067 -\rail@endbar
1.1068 -\rail@end
1.1069 \end{railoutput}
1.1070
1.1071
1.1072 \begin{description}
1.1073
1.1074 - \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}}}
1.1075 - axiomatizes a Gordon/HOL-style type definition in the background
1.1076 - theory of the current context, depending on a non-emptiness result
1.1077 - of the set \isa{A} (which needs to be proven interactively).
1.1078 + \item \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} defines inductive datatypes in
1.1079 + HOL.
1.1080
1.1081 - The raw type may not depend on parameters or assumptions of the
1.1082 - context --- this is logically impossible in Isabelle/HOL --- but the
1.1083 - non-emptiness property can be local, potentially resulting in
1.1084 - multiple interpretations in target contexts. Thus the established
1.1085 - bijection between the representing set \isa{A} and the new type
1.1086 - \isa{t} may semantically depend on local assumptions.
1.1087 + \item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}} represents existing types as
1.1088 + datatypes.
1.1089
1.1090 - By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t}
1.1091 - and a set (term constant) of the same name, unless an alternative
1.1092 - base name is given in parentheses, or the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}''
1.1093 - declaration is used to suppress a separate constant definition
1.1094 - altogether. The injection from type to set is called \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t},
1.1095 - its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t} --- this may be changed via an explicit
1.1096 - \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration.
1.1097 + 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
1.1098 + introduced by more primitive means using \indexref{}{command}{typedef}\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}. To
1.1099 + recover the rich infrastructure of \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} (e.g.\ rules
1.1100 + for \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} and the primitive recursion
1.1101 + combinators), such types may be represented as actual datatypes
1.1102 + later. This is done by specifying the constructors of the desired
1.1103 + type, and giving a proof of the induction rule, distinctness and
1.1104 + injectivity of constructors.
1.1105
1.1106 - Theorems \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t}, \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse}, and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse} provide the most basic characterization as a
1.1107 - corresponding injection/surjection pair (in both directions). Rules
1.1108 - \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} provide a slightly
1.1109 - more convenient view on the injectivity part, suitable for automated
1.1110 - proof tools (e.g.\ in \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}
1.1111 - declarations). Rules \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}cases}/\isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}induct}, and
1.1112 - \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}cases}/\isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views
1.1113 - on surjectivity; these are already declared as set or type rules for
1.1114 - the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.
1.1115 + For example, see \verb|~~/src/HOL/Sum_Type.thy| for the
1.1116 + representation of the primitive sum type as fully-featured datatype.
1.1117
1.1118 - An alternative name for the set definition (and other derived
1.1119 - entities) may be specified in parentheses; the default is to use
1.1120 - \isa{t} as indicated before.
1.1121 + \end{description}
1.1122
1.1123 - \end{description}%
1.1124 + The generated rules for \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.cases}{\mbox{\isa{cases}}} provide
1.1125 + case names according to the given constructors, while parameters are
1.1126 + named after the types (see also \secref{sec:cases-induct}).
1.1127 +
1.1128 + See \cite{isabelle-HOL} for more details on datatypes, but beware of
1.1129 + the old-style theory syntax being used there! Apart from proper
1.1130 + proof methods for case-analysis and induction, there are also
1.1131 + 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
1.1132 + to refer directly to the internal structure of subgoals (including
1.1133 + internally bound parameters).%
1.1134 \end{isamarkuptext}%
1.1135 \isamarkuptrue%
1.1136 %
1.1137 -\isamarkupsection{Adhoc tuples%
1.1138 +\isamarkupsubsubsection{Examples%
1.1139 }
1.1140 \isamarkuptrue%
1.1141 %
1.1142 \begin{isamarkuptext}%
1.1143 -\begin{matharray}{rcl}
1.1144 - \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} \\
1.1145 - \end{matharray}
1.1146 -
1.1147 - \begin{railoutput}
1.1148 -\rail@begin{2}{}
1.1149 -\rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
1.1150 -\rail@bar
1.1151 -\rail@nextbar{1}
1.1152 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1153 -\rail@term{\isa{complete}}[]
1.1154 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1155 -\rail@endbar
1.1156 -\rail@end
1.1157 -\end{railoutput}
1.1158 -
1.1159 -
1.1160 - \begin{description}
1.1161 -
1.1162 - \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
1.1163 - arguments in function applications to be represented canonically
1.1164 - according to their tuple type structure.
1.1165 -
1.1166 - Note that this operation tends to invent funny names for new local
1.1167 - parameters introduced.
1.1168 -
1.1169 - \end{description}%
1.1170 +We define a type of finite sequences, with slightly different
1.1171 + 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}}}:%
1.1172 \end{isamarkuptext}%
1.1173 \isamarkuptrue%
1.1174 +\isacommand{datatype}\isamarkupfalse%
1.1175 +\ {\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}}%
1.1176 +\begin{isamarkuptext}%
1.1177 +We can now prove some simple lemma by structural induction:%
1.1178 +\end{isamarkuptext}%
1.1179 +\isamarkuptrue%
1.1180 +\isacommand{lemma}\isamarkupfalse%
1.1181 +\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.1182 +%
1.1183 +\isadelimproof
1.1184 +%
1.1185 +\endisadelimproof
1.1186 +%
1.1187 +\isatagproof
1.1188 +\isacommand{proof}\isamarkupfalse%
1.1189 +\ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline
1.1190 +\ \ \isacommand{case}\isamarkupfalse%
1.1191 +\ Empty%
1.1192 +\begin{isamarkuptxt}%
1.1193 +This case can be proved using the simplifier: the freeness
1.1194 + properties of the datatype are already declared as \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rules.%
1.1195 +\end{isamarkuptxt}%
1.1196 +\isamarkuptrue%
1.1197 +\ \ \isacommand{show}\isamarkupfalse%
1.1198 +\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ Empty\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Empty{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.1199 +\ \ \ \ \isacommand{by}\isamarkupfalse%
1.1200 +\ simp\isanewline
1.1201 +\isacommand{next}\isamarkupfalse%
1.1202 +\isanewline
1.1203 +\ \ \isacommand{case}\isamarkupfalse%
1.1204 +\ {\isaliteral{28}{\isacharparenleft}}Seq\ y\ ys{\isaliteral{29}{\isacharparenright}}%
1.1205 +\begin{isamarkuptxt}%
1.1206 +The step case is proved similarly.%
1.1207 +\end{isamarkuptxt}%
1.1208 +\isamarkuptrue%
1.1209 +\ \ \isacommand{show}\isamarkupfalse%
1.1210 +\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ {\isaliteral{28}{\isacharparenleft}}Seq\ y\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Seq\ y\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.1211 +\ \ \ \ \isacommand{using}\isamarkupfalse%
1.1212 +\ {\isaliteral{60}{\isacharbackquoteopen}}Seq\ y\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ ys{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{by}\isamarkupfalse%
1.1213 +\ simp\isanewline
1.1214 +\isacommand{qed}\isamarkupfalse%
1.1215 +%
1.1216 +\endisatagproof
1.1217 +{\isafoldproof}%
1.1218 +%
1.1219 +\isadelimproof
1.1220 +%
1.1221 +\endisadelimproof
1.1222 +%
1.1223 +\begin{isamarkuptext}%
1.1224 +Here is a more succinct version of the same proof:%
1.1225 +\end{isamarkuptext}%
1.1226 +\isamarkuptrue%
1.1227 +\isacommand{lemma}\isamarkupfalse%
1.1228 +\ {\isaliteral{22}{\isachardoublequoteopen}}Seq\ x\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.1229 +%
1.1230 +\isadelimproof
1.1231 +\ \ %
1.1232 +\endisadelimproof
1.1233 +%
1.1234 +\isatagproof
1.1235 +\isacommand{by}\isamarkupfalse%
1.1236 +\ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
1.1237 +\endisatagproof
1.1238 +{\isafoldproof}%
1.1239 +%
1.1240 +\isadelimproof
1.1241 +%
1.1242 +\endisadelimproof
1.1243 %
1.1244 \isamarkupsection{Records \label{sec:hol-record}%
1.1245 }
1.1246 @@ -400,93 +1429,278 @@
1.1247 \end{isamarkuptext}%
1.1248 \isamarkuptrue%
1.1249 %
1.1250 -\isamarkupsection{Datatypes \label{sec:hol-datatype}%
1.1251 +\isamarkupsubsubsection{Examples%
1.1252 +}
1.1253 +\isamarkuptrue%
1.1254 +%
1.1255 +\begin{isamarkuptext}%
1.1256 +See \verb|~~/src/HOL/ex/Records.thy|, for example.%
1.1257 +\end{isamarkuptext}%
1.1258 +\isamarkuptrue%
1.1259 +%
1.1260 +\isamarkupsection{Adhoc tuples%
1.1261 }
1.1262 \isamarkuptrue%
1.1263 %
1.1264 \begin{isamarkuptext}%
1.1265 \begin{matharray}{rcl}
1.1266 - \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}}} \\
1.1267 - \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}}} \\
1.1268 + \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} \\
1.1269 \end{matharray}
1.1270
1.1271 \begin{railoutput}
1.1272 \rail@begin{2}{}
1.1273 -\rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
1.1274 -\rail@plus
1.1275 -\rail@nont{\isa{spec}}[]
1.1276 -\rail@nextplus{1}
1.1277 -\rail@cterm{\isa{\isakeyword{and}}}[]
1.1278 -\rail@endplus
1.1279 -\rail@end
1.1280 -\rail@begin{3}{}
1.1281 -\rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
1.1282 +\rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
1.1283 \rail@bar
1.1284 \rail@nextbar{1}
1.1285 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1286 -\rail@plus
1.1287 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1288 -\rail@nextplus{2}
1.1289 -\rail@endplus
1.1290 +\rail@term{\isa{complete}}[]
1.1291 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1292 \rail@endbar
1.1293 -\rail@plus
1.1294 -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1295 -\rail@nextplus{1}
1.1296 -\rail@endplus
1.1297 \rail@end
1.1298 -\rail@begin{2}{\isa{spec}}
1.1299 +\end{railoutput}
1.1300 +
1.1301 +
1.1302 + \begin{description}
1.1303 +
1.1304 + \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
1.1305 + arguments in function applications to be represented canonically
1.1306 + according to their tuple type structure.
1.1307 +
1.1308 + Note that this operation tends to invent funny names for new local
1.1309 + parameters introduced.
1.1310 +
1.1311 + \end{description}%
1.1312 +\end{isamarkuptext}%
1.1313 +\isamarkuptrue%
1.1314 +%
1.1315 +\isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}%
1.1316 +}
1.1317 +\isamarkuptrue%
1.1318 +%
1.1319 +\begin{isamarkuptext}%
1.1320 +A Gordon/HOL-style type definition is a certain axiom scheme
1.1321 + that identifies a new type with a subset of an existing type. More
1.1322 + precisely, the new type is defined by exhibiting an existing type
1.1323 + \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
1.1324 + \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
1.1325 + postulated that establish an isomorphism between the new type and
1.1326 + the subset. In general, the type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} may involve type
1.1327 + 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
1.1328 + 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
1.1329 + those type arguments.
1.1330 +
1.1331 + The axiomatization can be considered a ``definition'' in the sense
1.1332 + of the particular set-theoretic interpretation of HOL
1.1333 + \cite{pitts93}, where the universe of types is required to be
1.1334 + downwards-closed wrt.\ arbitrary non-empty subsets. Thus genuinely
1.1335 + new types introduced by \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} stay within the range
1.1336 + 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
1.1337 + abbreviations, without any logical significance.
1.1338 +
1.1339 + \begin{matharray}{rcl}
1.1340 + \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}}} \\
1.1341 + \end{matharray}
1.1342 +
1.1343 + \begin{railoutput}
1.1344 +\rail@begin{2}{}
1.1345 +\rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
1.1346 \rail@bar
1.1347 \rail@nextbar{1}
1.1348 -\rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
1.1349 +\rail@nont{\isa{alt{\isaliteral{5F}{\isacharunderscore}}name}}[]
1.1350 \rail@endbar
1.1351 -\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
1.1352 +\rail@nont{\isa{abs{\isaliteral{5F}{\isacharunderscore}}type}}[]
1.1353 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.1354 +\rail@nont{\isa{rep{\isaliteral{5F}{\isacharunderscore}}set}}[]
1.1355 +\rail@end
1.1356 +\rail@begin{3}{\isa{alt{\isaliteral{5F}{\isacharunderscore}}name}}
1.1357 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1358 \rail@bar
1.1359 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1360 \rail@nextbar{1}
1.1361 -\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.1362 +\rail@term{\isa{\isakeyword{open}}}[]
1.1363 +\rail@nextbar{2}
1.1364 +\rail@term{\isa{\isakeyword{open}}}[]
1.1365 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1366 \rail@endbar
1.1367 -\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.1368 -\rail@plus
1.1369 -\rail@nont{\isa{cons}}[]
1.1370 -\rail@nextplus{1}
1.1371 -\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.1372 -\rail@endplus
1.1373 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1374 \rail@end
1.1375 -\rail@begin{2}{\isa{cons}}
1.1376 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1377 -\rail@plus
1.1378 -\rail@nextplus{1}
1.1379 -\rail@cnont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
1.1380 -\rail@endplus
1.1381 +\rail@begin{2}{\isa{abs{\isaliteral{5F}{\isacharunderscore}}type}}
1.1382 +\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
1.1383 \rail@bar
1.1384 \rail@nextbar{1}
1.1385 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.1386 \rail@endbar
1.1387 \rail@end
1.1388 +\rail@begin{2}{\isa{rep{\isaliteral{5F}{\isacharunderscore}}set}}
1.1389 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1390 +\rail@bar
1.1391 +\rail@nextbar{1}
1.1392 +\rail@term{\isa{\isakeyword{morphisms}}}[]
1.1393 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1394 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1395 +\rail@endbar
1.1396 +\rail@end
1.1397 \end{railoutput}
1.1398
1.1399
1.1400 \begin{description}
1.1401
1.1402 - \item \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} defines inductive datatypes in
1.1403 - HOL.
1.1404 + \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}}}
1.1405 + axiomatizes a type definition in the background theory of the
1.1406 + current context, depending on a non-emptiness result of the set
1.1407 + \isa{A} that needs to be proven here. The set \isa{A} may
1.1408 + 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,
1.1409 + but no term variables.
1.1410
1.1411 - \item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}} represents existing types as
1.1412 - inductive ones, generating the standard infrastructure of derived
1.1413 - concepts (primitive recursion etc.).
1.1414 + Even though a local theory specification, the newly introduced type
1.1415 + constructor cannot depend on parameters or assumptions of the
1.1416 + context: this is structurally impossible in HOL. In contrast, the
1.1417 + non-emptiness proof may use local assumptions in unusual situations,
1.1418 + which could result in different interpretations in target contexts:
1.1419 + the meaning of the bijection between the representing set \isa{A}
1.1420 + and the new type \isa{t} may then change in different application
1.1421 + contexts.
1.1422 +
1.1423 + By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type
1.1424 + 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
1.1425 + altogether. The injection from type to set is called \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t},
1.1426 + its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t}, unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.
1.1427 +
1.1428 + The core axiomatization uses the locale predicate \isa{type{\isaliteral{5F}{\isacharunderscore}}definition} as defined in Isabelle/HOL. Various basic
1.1429 + consequences of that are instantiated accordingly, re-using the
1.1430 + locale facts with names derived from the new type constructor. Thus
1.1431 + the generic \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep} is turned into the specific
1.1432 + \isa{{\isaliteral{22}{\isachardoublequote}}Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{22}{\isachardoublequote}}}, for example.
1.1433 +
1.1434 + 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}
1.1435 + provide the most basic characterization as a corresponding
1.1436 + injection/surjection pair (in both directions). The derived rules
1.1437 + \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
1.1438 + injectivity, suitable for automated proof tools (e.g.\ in
1.1439 + declarations involving \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}).
1.1440 + 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}~/
1.1441 + \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views on
1.1442 + surjectivity. These rules are already declared as set or type rules
1.1443 + for the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods,
1.1444 + respectively.
1.1445 +
1.1446 + An alternative name for the set definition (and other derived
1.1447 + entities) may be specified in parentheses; the default is to use
1.1448 + \isa{t} directly.
1.1449
1.1450 \end{description}
1.1451
1.1452 - The induction and exhaustion theorems generated provide case names
1.1453 - according to the constructors involved, while parameters are named
1.1454 - after the types (see also \secref{sec:cases-induct}).
1.1455 + \begin{warn}
1.1456 + 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
1.1457 + is that it has a non-empty model, to avoid immediate collapse of the
1.1458 + HOL logic. Moreover, one needs to demonstrate that the
1.1459 + interpretation of such free-form axiomatizations can coexist with
1.1460 + that of the regular \indexdef{}{command}{typedef}\hypertarget{command.typedef}{\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}} scheme, and any extension
1.1461 + that other people might have introduced elsewhere (e.g.\ in HOLCF
1.1462 + \cite{MuellerNvOS99}).
1.1463 + \end{warn}%
1.1464 +\end{isamarkuptext}%
1.1465 +\isamarkuptrue%
1.1466 +%
1.1467 +\isamarkupsubsubsection{Examples%
1.1468 +}
1.1469 +\isamarkuptrue%
1.1470 +%
1.1471 +\begin{isamarkuptext}%
1.1472 +Type definitions permit the introduction of abstract data
1.1473 + types in a safe way, namely by providing models based on already
1.1474 + existing types. Given some abstract axiomatic description \isa{P}
1.1475 + of a type, this involves two steps:
1.1476
1.1477 - See \cite{isabelle-HOL} for more details on datatypes, but beware of
1.1478 - the old-style theory syntax being used there! Apart from proper
1.1479 - proof methods for case-analysis and induction, there are also
1.1480 - 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
1.1481 - to refer directly to the internal structure of subgoals (including
1.1482 - internally bound parameters).%
1.1483 + \begin{enumerate}
1.1484 +
1.1485 + \item Find an appropriate type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} and subset \isa{A} which
1.1486 + has the desired properties \isa{P}, and make a type definition
1.1487 + based on this representation.
1.1488 +
1.1489 + \item Prove that \isa{P} holds for \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} by lifting \isa{P}
1.1490 + from the representation.
1.1491 +
1.1492 + \end{enumerate}
1.1493 +
1.1494 + You can later forget about the representation and work solely in
1.1495 + terms of the abstract properties \isa{P}.
1.1496 +
1.1497 + \medskip The following trivial example pulls a three-element type
1.1498 + into existence within the formal logical environment of HOL.%
1.1499 +\end{isamarkuptext}%
1.1500 +\isamarkuptrue%
1.1501 +\isacommand{typedef}\isamarkupfalse%
1.1502 +\ 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
1.1503 +%
1.1504 +\isadelimproof
1.1505 +\ \ %
1.1506 +\endisadelimproof
1.1507 +%
1.1508 +\isatagproof
1.1509 +\isacommand{by}\isamarkupfalse%
1.1510 +\ blast%
1.1511 +\endisatagproof
1.1512 +{\isafoldproof}%
1.1513 +%
1.1514 +\isadelimproof
1.1515 +\isanewline
1.1516 +%
1.1517 +\endisadelimproof
1.1518 +\isanewline
1.1519 +\isacommand{definition}\isamarkupfalse%
1.1520 +\ {\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
1.1521 +\isacommand{definition}\isamarkupfalse%
1.1522 +\ {\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
1.1523 +\isacommand{definition}\isamarkupfalse%
1.1524 +\ {\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
1.1525 +\isanewline
1.1526 +\isacommand{lemma}\isamarkupfalse%
1.1527 +\ 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
1.1528 +%
1.1529 +\isadelimproof
1.1530 +\ \ %
1.1531 +\endisadelimproof
1.1532 +%
1.1533 +\isatagproof
1.1534 +\isacommand{by}\isamarkupfalse%
1.1535 +\ {\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}}%
1.1536 +\endisatagproof
1.1537 +{\isafoldproof}%
1.1538 +%
1.1539 +\isadelimproof
1.1540 +\isanewline
1.1541 +%
1.1542 +\endisadelimproof
1.1543 +\isanewline
1.1544 +\isacommand{lemma}\isamarkupfalse%
1.1545 +\ three{\isaliteral{5F}{\isacharunderscore}}cases{\isaliteral{3A}{\isacharcolon}}\isanewline
1.1546 +\ \ \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
1.1547 +%
1.1548 +\isadelimproof
1.1549 +\ \ %
1.1550 +\endisadelimproof
1.1551 +%
1.1552 +\isatagproof
1.1553 +\isacommand{by}\isamarkupfalse%
1.1554 +\ {\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}}%
1.1555 +\endisatagproof
1.1556 +{\isafoldproof}%
1.1557 +%
1.1558 +\isadelimproof
1.1559 +%
1.1560 +\endisadelimproof
1.1561 +%
1.1562 +\begin{isamarkuptext}%
1.1563 +Note that such trivial constructions are better done with
1.1564 + derived specification mechanisms such as \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}:%
1.1565 +\end{isamarkuptext}%
1.1566 +\isamarkuptrue%
1.1567 +\isacommand{datatype}\isamarkupfalse%
1.1568 +\ 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}}%
1.1569 +\begin{isamarkuptext}%
1.1570 +This avoids re-doing basic definitions and proofs from the
1.1571 + primitive \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} above.%
1.1572 \end{isamarkuptext}%
1.1573 \isamarkuptrue%
1.1574 %
1.1575 @@ -540,641 +1754,6 @@
1.1576 \end{isamarkuptext}%
1.1577 \isamarkuptrue%
1.1578 %
1.1579 -\isamarkupsection{Recursive functions \label{sec:recursion}%
1.1580 -}
1.1581 -\isamarkuptrue%
1.1582 -%
1.1583 -\begin{isamarkuptext}%
1.1584 -\begin{matharray}{rcl}
1.1585 - \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}}} \\
1.1586 - \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}}} \\
1.1587 - \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}}} \\
1.1588 - \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}}} \\
1.1589 - \end{matharray}
1.1590 -
1.1591 - \begin{railoutput}
1.1592 -\rail@begin{2}{}
1.1593 -\rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
1.1594 -\rail@bar
1.1595 -\rail@nextbar{1}
1.1596 -\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.1597 -\rail@endbar
1.1598 -\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.1599 -\rail@term{\isa{\isakeyword{where}}}[]
1.1600 -\rail@nont{\isa{equations}}[]
1.1601 -\rail@end
1.1602 -\rail@begin{4}{}
1.1603 -\rail@bar
1.1604 -\rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
1.1605 -\rail@nextbar{1}
1.1606 -\rail@term{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}}[]
1.1607 -\rail@endbar
1.1608 -\rail@bar
1.1609 -\rail@nextbar{1}
1.1610 -\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.1611 -\rail@endbar
1.1612 -\rail@bar
1.1613 -\rail@nextbar{1}
1.1614 -\rail@nont{\isa{functionopts}}[]
1.1615 -\rail@endbar
1.1616 -\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.1617 -\rail@cr{3}
1.1618 -\rail@term{\isa{\isakeyword{where}}}[]
1.1619 -\rail@nont{\isa{equations}}[]
1.1620 -\rail@end
1.1621 -\rail@begin{3}{\isa{equations}}
1.1622 -\rail@plus
1.1623 -\rail@bar
1.1624 -\rail@nextbar{1}
1.1625 -\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.1626 -\rail@endbar
1.1627 -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.1628 -\rail@nextplus{2}
1.1629 -\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.1630 -\rail@endplus
1.1631 -\rail@end
1.1632 -\rail@begin{3}{\isa{functionopts}}
1.1633 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1634 -\rail@plus
1.1635 -\rail@bar
1.1636 -\rail@term{\isa{sequential}}[]
1.1637 -\rail@nextbar{1}
1.1638 -\rail@term{\isa{domintros}}[]
1.1639 -\rail@endbar
1.1640 -\rail@nextplus{2}
1.1641 -\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
1.1642 -\rail@endplus
1.1643 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1644 -\rail@end
1.1645 -\rail@begin{2}{}
1.1646 -\rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
1.1647 -\rail@bar
1.1648 -\rail@nextbar{1}
1.1649 -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1650 -\rail@endbar
1.1651 -\rail@end
1.1652 -\end{railoutput}
1.1653 -
1.1654 -
1.1655 - \begin{description}
1.1656 -
1.1657 - \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
1.1658 - functions over datatypes, see also \cite{isabelle-HOL}.
1.1659 -
1.1660 - \item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
1.1661 - wellfounded recursion. A detailed description with examples can be
1.1662 - found in \cite{isabelle-function}. The function is specified by a
1.1663 - set of (possibly conditional) recursive equations with arbitrary
1.1664 - pattern matching. The command generates proof obligations for the
1.1665 - completeness and the compatibility of patterns.
1.1666 -
1.1667 - The defined function is considered partial, and the resulting
1.1668 - simplification rules (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}psimps{\isaliteral{22}{\isachardoublequote}}}) and induction rule
1.1669 - (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}pinduct{\isaliteral{22}{\isachardoublequote}}}) are guarded by a generated domain
1.1670 - predicate \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5F}{\isacharunderscore}}dom{\isaliteral{22}{\isachardoublequote}}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}
1.1671 - command can then be used to establish that the function is total.
1.1672 -
1.1673 - \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
1.1674 - proof attempts regarding pattern matching and termination. See
1.1675 - \cite{isabelle-function} for further details.
1.1676 -
1.1677 - \item \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f} commences a
1.1678 - termination proof for the previously defined function \isa{f}. If
1.1679 - this is omitted, the command refers to the most recent function
1.1680 - definition. After the proof is closed, the recursive equations and
1.1681 - the induction principle is established.
1.1682 -
1.1683 - \end{description}
1.1684 -
1.1685 - Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
1.1686 - command accommodate
1.1687 - reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2E}{\isachardot}}induct{\isaliteral{22}{\isachardoublequote}}} (where \isa{c} is the name of the function definition)
1.1688 - refers to a specific induction rule, with parameters named according
1.1689 - to the user-specified equations. Cases are numbered (starting from 1).
1.1690 -
1.1691 - For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
1.1692 - with structural recursion on the datatype the recursion is carried
1.1693 - out.
1.1694 -
1.1695 - The equations provided by these packages may be referred later as
1.1696 - theorem list \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, where \isa{f} is the (collective)
1.1697 - name of the functions defined. Individual equations may be named
1.1698 - explicitly as well.
1.1699 -
1.1700 - The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following
1.1701 - options.
1.1702 -
1.1703 - \begin{description}
1.1704 -
1.1705 - \item \isa{sequential} enables a preprocessor which disambiguates
1.1706 - overlapping patterns by making them mutually disjoint. Earlier
1.1707 - equations take precedence over later ones. This allows to give the
1.1708 - specification in a format very similar to functional programming.
1.1709 - Note that the resulting simplification and induction rules
1.1710 - correspond to the transformed specification, not the one given
1.1711 - originally. This usually means that each equation given by the user
1.1712 - may result in several theorems. Also note that this automatic
1.1713 - transformation only works for ML-style datatype patterns.
1.1714 -
1.1715 - \item \isa{domintros} enables the automated generation of
1.1716 - introduction rules for the domain predicate. While mostly not
1.1717 - needed, they can be helpful in some proofs about partial functions.
1.1718 -
1.1719 - \end{description}%
1.1720 -\end{isamarkuptext}%
1.1721 -\isamarkuptrue%
1.1722 -%
1.1723 -\isamarkupsubsection{Proof methods related to recursive definitions%
1.1724 -}
1.1725 -\isamarkuptrue%
1.1726 -%
1.1727 -\begin{isamarkuptext}%
1.1728 -\begin{matharray}{rcl}
1.1729 - \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}}} & : & \isa{method} \\
1.1730 - \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
1.1731 - \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}} & : & \isa{method} \\
1.1732 - \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}} & : & \isa{method} \\
1.1733 - \end{matharray}
1.1734 -
1.1735 - \begin{railoutput}
1.1736 -\rail@begin{1}{}
1.1737 -\rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
1.1738 -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1739 -\rail@end
1.1740 -\rail@begin{2}{}
1.1741 -\rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
1.1742 -\rail@plus
1.1743 -\rail@nextplus{1}
1.1744 -\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.1745 -\rail@endplus
1.1746 -\rail@end
1.1747 -\rail@begin{2}{}
1.1748 -\rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
1.1749 -\rail@nont{\isa{orders}}[]
1.1750 -\rail@plus
1.1751 -\rail@nextplus{1}
1.1752 -\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.1753 -\rail@endplus
1.1754 -\rail@end
1.1755 -\rail@begin{4}{\isa{orders}}
1.1756 -\rail@plus
1.1757 -\rail@nextplus{1}
1.1758 -\rail@bar
1.1759 -\rail@term{\isa{max}}[]
1.1760 -\rail@nextbar{2}
1.1761 -\rail@term{\isa{min}}[]
1.1762 -\rail@nextbar{3}
1.1763 -\rail@term{\isa{ms}}[]
1.1764 -\rail@endbar
1.1765 -\rail@endplus
1.1766 -\rail@end
1.1767 -\end{railoutput}
1.1768 -
1.1769 -
1.1770 - \begin{description}
1.1771 -
1.1772 - \item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}} is a specialized method to
1.1773 - solve goals regarding the completeness of pattern matching, as
1.1774 - required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
1.1775 - \cite{isabelle-function}).
1.1776 -
1.1777 - \item \hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R} introduces a termination
1.1778 - proof using the relation \isa{R}. The resulting proof state will
1.1779 - contain goals expressing that \isa{R} is wellfounded, and that the
1.1780 - arguments of recursive calls decrease with respect to \isa{R}.
1.1781 - Usually, this method is used as the initial proof step of manual
1.1782 - termination proofs.
1.1783 -
1.1784 - \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}} attempts a fully
1.1785 - automated termination proof by searching for a lexicographic
1.1786 - combination of size measures on the arguments of the function. The
1.1787 - method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
1.1788 - which it uses internally to prove local descents. The same context
1.1789 - modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see
1.1790 - \secref{sec:clasimp}.
1.1791 -
1.1792 - In case of failure, extensive information is printed, which can help
1.1793 - to analyse the situation (cf.\ \cite{isabelle-function}).
1.1794 -
1.1795 - \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}} also works on termination goals,
1.1796 - using a variation of the size-change principle, together with a
1.1797 - graph decomposition technique (see \cite{krauss_phd} for details).
1.1798 - Three kinds of orders are used internally: \isa{max}, \isa{min},
1.1799 - and \isa{ms} (multiset), which is only available when the theory
1.1800 - \isa{Multiset} is loaded. When no order kinds are given, they are
1.1801 - tried in order. The search for a termination proof uses SAT solving
1.1802 - internally.
1.1803 -
1.1804 - For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
1.1805 -
1.1806 - \end{description}%
1.1807 -\end{isamarkuptext}%
1.1808 -\isamarkuptrue%
1.1809 -%
1.1810 -\isamarkupsubsection{Functions with explicit partiality%
1.1811 -}
1.1812 -\isamarkuptrue%
1.1813 -%
1.1814 -\begin{isamarkuptext}%
1.1815 -\begin{matharray}{rcl}
1.1816 - \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}}} \\
1.1817 - \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} \\
1.1818 - \end{matharray}
1.1819 -
1.1820 - \begin{railoutput}
1.1821 -\rail@begin{5}{}
1.1822 -\rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
1.1823 -\rail@bar
1.1824 -\rail@nextbar{1}
1.1825 -\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.1826 -\rail@endbar
1.1827 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1828 -\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.1829 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1830 -\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.1831 -\rail@cr{3}
1.1832 -\rail@term{\isa{\isakeyword{where}}}[]
1.1833 -\rail@bar
1.1834 -\rail@nextbar{4}
1.1835 -\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.1836 -\rail@endbar
1.1837 -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.1838 -\rail@end
1.1839 -\end{railoutput}
1.1840 -
1.1841 -
1.1842 - \begin{description}
1.1843 -
1.1844 - \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
1.1845 - recursive functions based on fixpoints in complete partial
1.1846 - orders. No termination proof is required from the user or
1.1847 - constructed internally. Instead, the possibility of non-termination
1.1848 - is modelled explicitly in the result type, which contains an
1.1849 - explicit bottom element.
1.1850 -
1.1851 - Pattern matching and mutual recursion are currently not supported.
1.1852 - Thus, the specification consists of a single function described by a
1.1853 - single recursive equation.
1.1854 -
1.1855 - There are no fixed syntactic restrictions on the body of the
1.1856 - function, but the induced functional must be provably monotonic
1.1857 - wrt.\ the underlying order. The monotonicitity proof is performed
1.1858 - internally, and the definition is rejected when it fails. The proof
1.1859 - can be influenced by declaring hints using the
1.1860 - \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} attribute.
1.1861 -
1.1862 - The mandatory \isa{mode} argument specifies the mode of operation
1.1863 - of the command, which directly corresponds to a complete partial
1.1864 - order on the result type. By default, the following modes are
1.1865 - defined:
1.1866 -
1.1867 - \begin{description}
1.1868 - \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
1.1869 - non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
1.1870 - must also be \isa{None}. This is best achieved through the use of
1.1871 - the monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}.
1.1872 -
1.1873 - \item \isa{tailrec} defines functions with an arbitrary result
1.1874 - 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
1.1875 - if \isa{undefined} is returned by a recursive call, then the
1.1876 - overall result must also be \isa{undefined}. In practice, this is
1.1877 - only satisfied when each recursive call is a tail call, whose result
1.1878 - is directly returned. Thus, this mode of operation allows the
1.1879 - definition of arbitrary tail-recursive functions.
1.1880 - \end{description}
1.1881 -
1.1882 - Experienced users may define new modes by instantiating the locale
1.1883 - \isa{{\isaliteral{22}{\isachardoublequote}}partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}definitions{\isaliteral{22}{\isachardoublequote}}} appropriately.
1.1884 -
1.1885 - \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} declares rules for
1.1886 - use in the internal monononicity proofs of partial function
1.1887 - definitions.
1.1888 -
1.1889 - \end{description}%
1.1890 -\end{isamarkuptext}%
1.1891 -\isamarkuptrue%
1.1892 -%
1.1893 -\isamarkupsubsection{Old-style recursive function definitions (TFL)%
1.1894 -}
1.1895 -\isamarkuptrue%
1.1896 -%
1.1897 -\begin{isamarkuptext}%
1.1898 -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.
1.1899 -
1.1900 - \begin{matharray}{rcl}
1.1901 - \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}}} \\
1.1902 - \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}}} \\
1.1903 - \end{matharray}
1.1904 -
1.1905 - \begin{railoutput}
1.1906 -\rail@begin{5}{}
1.1907 -\rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
1.1908 -\rail@bar
1.1909 -\rail@nextbar{1}
1.1910 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1911 -\rail@term{\isa{\isakeyword{permissive}}}[]
1.1912 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1913 -\rail@endbar
1.1914 -\rail@cr{3}
1.1915 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1916 -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1917 -\rail@plus
1.1918 -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.1919 -\rail@nextplus{4}
1.1920 -\rail@endplus
1.1921 -\rail@bar
1.1922 -\rail@nextbar{4}
1.1923 -\rail@nont{\isa{hints}}[]
1.1924 -\rail@endbar
1.1925 -\rail@end
1.1926 -\rail@begin{2}{}
1.1927 -\rail@nont{\isa{recdeftc}}[]
1.1928 -\rail@bar
1.1929 -\rail@nextbar{1}
1.1930 -\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.1931 -\rail@endbar
1.1932 -\rail@nont{\isa{tc}}[]
1.1933 -\rail@end
1.1934 -\rail@begin{2}{\isa{hints}}
1.1935 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1936 -\rail@term{\isa{\isakeyword{hints}}}[]
1.1937 -\rail@plus
1.1938 -\rail@nextplus{1}
1.1939 -\rail@cnont{\isa{recdefmod}}[]
1.1940 -\rail@endplus
1.1941 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1942 -\rail@end
1.1943 -\rail@begin{4}{\isa{recdefmod}}
1.1944 -\rail@bar
1.1945 -\rail@bar
1.1946 -\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}[]
1.1947 -\rail@nextbar{1}
1.1948 -\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}[]
1.1949 -\rail@nextbar{2}
1.1950 -\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}[]
1.1951 -\rail@endbar
1.1952 -\rail@bar
1.1953 -\rail@nextbar{1}
1.1954 -\rail@term{\isa{add}}[]
1.1955 -\rail@nextbar{2}
1.1956 -\rail@term{\isa{del}}[]
1.1957 -\rail@endbar
1.1958 -\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.1959 -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.1960 -\rail@nextbar{3}
1.1961 -\rail@nont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.1962 -\rail@endbar
1.1963 -\rail@end
1.1964 -\rail@begin{2}{\isa{tc}}
1.1965 -\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.1966 -\rail@bar
1.1967 -\rail@nextbar{1}
1.1968 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1969 -\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.1970 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1971 -\rail@endbar
1.1972 -\rail@end
1.1973 -\end{railoutput}
1.1974 -
1.1975 -
1.1976 - \begin{description}
1.1977 -
1.1978 - \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
1.1979 - recursive functions (using the TFL package), see also
1.1980 - \cite{isabelle-HOL}. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells
1.1981 - TFL to recover from failed proof attempts, returning unfinished
1.1982 - 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
1.1983 - automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}
1.1984 - declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
1.1985 - context of the Simplifier (cf.\ \secref{sec:simplifier}) and
1.1986 - Classical reasoner (cf.\ \secref{sec:classical}).
1.1987 -
1.1988 - \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
1.1989 - proof for leftover termination condition number \isa{i} (default
1.1990 - 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
1.1991 - constant \isa{c}.
1.1992 -
1.1993 - Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
1.1994 - its internal proofs without manual intervention.
1.1995 -
1.1996 - \end{description}
1.1997 -
1.1998 - \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared
1.1999 - globally, using the following attributes.
1.2000 -
1.2001 - \begin{matharray}{rcl}
1.2002 - \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}} & : & \isa{attribute} \\
1.2003 - \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}} & : & \isa{attribute} \\
1.2004 - \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}} & : & \isa{attribute} \\
1.2005 - \end{matharray}
1.2006 -
1.2007 - \begin{railoutput}
1.2008 -\rail@begin{3}{}
1.2009 -\rail@bar
1.2010 -\rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
1.2011 -\rail@nextbar{1}
1.2012 -\rail@term{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}}[]
1.2013 -\rail@nextbar{2}
1.2014 -\rail@term{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}}[]
1.2015 -\rail@endbar
1.2016 -\rail@bar
1.2017 -\rail@nextbar{1}
1.2018 -\rail@term{\isa{add}}[]
1.2019 -\rail@nextbar{2}
1.2020 -\rail@term{\isa{del}}[]
1.2021 -\rail@endbar
1.2022 -\rail@end
1.2023 -\end{railoutput}%
1.2024 -\end{isamarkuptext}%
1.2025 -\isamarkuptrue%
1.2026 -%
1.2027 -\isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
1.2028 -}
1.2029 -\isamarkuptrue%
1.2030 -%
1.2031 -\begin{isamarkuptext}%
1.2032 -An \textbf{inductive definition} specifies the least predicate (or
1.2033 - set) \isa{R} closed under given rules: applying a rule to elements
1.2034 - of \isa{R} yields a result within \isa{R}. For example, a
1.2035 - structural operational semantics is an inductive definition of an
1.2036 - evaluation relation.
1.2037 -
1.2038 - Dually, a \textbf{coinductive definition} specifies the greatest
1.2039 - predicate~/ set \isa{R} that is consistent with given rules: every
1.2040 - element of \isa{R} can be seen as arising by applying a rule to
1.2041 - elements of \isa{R}. An important example is using bisimulation
1.2042 - relations to formalise equivalence of processes and infinite data
1.2043 - structures.
1.2044 -
1.2045 - \medskip The HOL package is related to the ZF one, which is
1.2046 - described in a separate paper,\footnote{It appeared in CADE
1.2047 - \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
1.2048 - which you should refer to in case of difficulties. The package is
1.2049 - simpler than that of ZF thanks to implicit type-checking in HOL.
1.2050 - The types of the (co)inductive predicates (or sets) determine the
1.2051 - domain of the fixedpoint definition, and the package does not have
1.2052 - to use inference rules for type-checking.
1.2053 -
1.2054 - \begin{matharray}{rcl}
1.2055 - \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}}} \\
1.2056 - \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}}} \\
1.2057 - \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}}} \\
1.2058 - \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}}} \\
1.2059 - \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
1.2060 - \end{matharray}
1.2061 -
1.2062 - \begin{railoutput}
1.2063 -\rail@begin{7}{}
1.2064 -\rail@bar
1.2065 -\rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
1.2066 -\rail@nextbar{1}
1.2067 -\rail@term{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1.2068 -\rail@nextbar{2}
1.2069 -\rail@term{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]
1.2070 -\rail@nextbar{3}
1.2071 -\rail@term{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1.2072 -\rail@endbar
1.2073 -\rail@bar
1.2074 -\rail@nextbar{1}
1.2075 -\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.2076 -\rail@endbar
1.2077 -\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.2078 -\rail@bar
1.2079 -\rail@nextbar{1}
1.2080 -\rail@term{\isa{\isakeyword{for}}}[]
1.2081 -\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.2082 -\rail@endbar
1.2083 -\rail@cr{5}
1.2084 -\rail@bar
1.2085 -\rail@nextbar{6}
1.2086 -\rail@term{\isa{\isakeyword{where}}}[]
1.2087 -\rail@nont{\isa{clauses}}[]
1.2088 -\rail@endbar
1.2089 -\rail@bar
1.2090 -\rail@nextbar{6}
1.2091 -\rail@term{\isa{\isakeyword{monos}}}[]
1.2092 -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.2093 -\rail@endbar
1.2094 -\rail@end
1.2095 -\rail@begin{3}{\isa{clauses}}
1.2096 -\rail@plus
1.2097 -\rail@bar
1.2098 -\rail@nextbar{1}
1.2099 -\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.2100 -\rail@endbar
1.2101 -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.2102 -\rail@nextplus{2}
1.2103 -\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.2104 -\rail@endplus
1.2105 -\rail@end
1.2106 -\rail@begin{3}{}
1.2107 -\rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
1.2108 -\rail@bar
1.2109 -\rail@nextbar{1}
1.2110 -\rail@term{\isa{add}}[]
1.2111 -\rail@nextbar{2}
1.2112 -\rail@term{\isa{del}}[]
1.2113 -\rail@endbar
1.2114 -\rail@end
1.2115 -\end{railoutput}
1.2116 -
1.2117 -
1.2118 - \begin{description}
1.2119 -
1.2120 - \item \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}} define (co)inductive predicates from the
1.2121 - introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part. The
1.2122 - optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the
1.2123 - (co)inductive predicates that remain fixed throughout the
1.2124 - definition. The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains
1.2125 - \emph{monotonicity theorems}, which are required for each operator
1.2126 - applied to a recursive set in the introduction rules. There
1.2127 - \emph{must} be a theorem of the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ M\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ M\ B{\isaliteral{22}{\isachardoublequote}}},
1.2128 - for each premise \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}} in an introduction rule!
1.2129 -
1.2130 - \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,
1.2131 - allowing the definition of (co)inductive sets.
1.2132 -
1.2133 - \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules. These
1.2134 - rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}.
1.2135 -
1.2136 - \end{description}%
1.2137 -\end{isamarkuptext}%
1.2138 -\isamarkuptrue%
1.2139 -%
1.2140 -\isamarkupsubsection{Derived rules%
1.2141 -}
1.2142 -\isamarkuptrue%
1.2143 -%
1.2144 -\begin{isamarkuptext}%
1.2145 -Each (co)inductive definition \isa{R} adds definitions to the
1.2146 - theory and also proves some theorems:
1.2147 -
1.2148 - \begin{description}
1.2149 -
1.2150 - \item \isa{R{\isaliteral{2E}{\isachardot}}intros} is the list of introduction rules as proven
1.2151 - theorems, for the recursive predicates (or sets). The rules are
1.2152 - also available individually, using the names given them in the
1.2153 - theory file;
1.2154 -
1.2155 - \item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
1.2156 -
1.2157 - \item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
1.2158 - rule.
1.2159 -
1.2160 - \end{description}
1.2161 -
1.2162 - 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
1.2163 - defined simultaneously, the list of introduction rules is called
1.2164 - \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
1.2165 - 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
1.2166 - 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}}}.%
1.2167 -\end{isamarkuptext}%
1.2168 -\isamarkuptrue%
1.2169 -%
1.2170 -\isamarkupsubsection{Monotonicity theorems%
1.2171 -}
1.2172 -\isamarkuptrue%
1.2173 -%
1.2174 -\begin{isamarkuptext}%
1.2175 -Each theory contains a default set of theorems that are used in
1.2176 - monotonicity proofs. New rules can be added to this set via the
1.2177 - \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute. The HOL theory \isa{Inductive}
1.2178 - shows how this is done. In general, the following monotonicity
1.2179 - theorems may be added:
1.2180 -
1.2181 - \begin{itemize}
1.2182 -
1.2183 - \item Theorems of the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ M\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ M\ B{\isaliteral{22}{\isachardoublequote}}}, for proving
1.2184 - monotonicity of inductive definitions whose introduction rules have
1.2185 - premises involving terms such as \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}}.
1.2186 -
1.2187 - \item Monotonicity theorems for logical operators, which are of the
1.2188 - 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
1.2189 - the case of the operator \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, the corresponding theorem is
1.2190 - \[
1.2191 - \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}}}}
1.2192 - \]
1.2193 -
1.2194 - \item De Morgan style equations for reasoning about the ``polarity''
1.2195 - of expressions, e.g.
1.2196 - \[
1.2197 - \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ P{\isaliteral{22}{\isachardoublequote}}} \qquad\qquad
1.2198 - \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}}}
1.2199 - \]
1.2200 -
1.2201 - \item Equations for reducing complex operators to more primitive
1.2202 - ones whose monotonicity can easily be proved, e.g.
1.2203 - \[
1.2204 - \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
1.2205 - \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}}}
1.2206 - \]
1.2207 -
1.2208 - \end{itemize}
1.2209 -
1.2210 - %FIXME: Example of an inductive definition%
1.2211 -\end{isamarkuptext}%
1.2212 -\isamarkuptrue%
1.2213 -%
1.2214 \isamarkupsection{Arithmetic proof support%
1.2215 }
1.2216 \isamarkuptrue%
1.2217 @@ -1483,14 +2062,15 @@
1.2218
1.2219 \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a
1.2220 term; optionally \isa{modes} can be specified, which are
1.2221 - appended to the current print mode (see also \cite{isabelle-ref}).
1.2222 + appended to the current print mode; see \secref{sec:print-modes}.
1.2223 Internally, the evaluation is performed by registered evaluators,
1.2224 which are invoked sequentially until a result is returned.
1.2225 Alternatively a specific evaluator can be selected using square
1.2226 brackets; typical evaluators use the current set of code equations
1.2227 - to normalize and include \isa{simp} for fully symbolic evaluation
1.2228 - using the simplifier, \isa{nbe} for \emph{normalization by evaluation}
1.2229 - and \emph{code} for code generation in SML.
1.2230 + to normalize and include \isa{simp} for fully symbolic
1.2231 + evaluation using the simplifier, \isa{nbe} for
1.2232 + \emph{normalization by evaluation} and \emph{code} for code
1.2233 + generation in SML.
1.2234
1.2235 \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
1.2236 counterexamples using a series of assignments for its