1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed May 25 22:12:46 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed May 25 22:21:38 2011 +0200
1.3 @@ -22,6 +22,1018 @@
1.4 }
1.5 \isamarkuptrue%
1.6 %
1.7 +\isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
1.8 +}
1.9 +\isamarkuptrue%
1.10 +%
1.11 +\begin{isamarkuptext}%
1.12 +An \textbf{inductive definition} specifies the least predicate (or
1.13 + set) \isa{R} closed under given rules: applying a rule to elements
1.14 + of \isa{R} yields a result within \isa{R}. For example, a
1.15 + structural operational semantics is an inductive definition of an
1.16 + evaluation relation.
1.17 +
1.18 + Dually, a \textbf{coinductive definition} specifies the greatest
1.19 + predicate~/ set \isa{R} that is consistent with given rules: every
1.20 + element of \isa{R} can be seen as arising by applying a rule to
1.21 + elements of \isa{R}. An important example is using bisimulation
1.22 + relations to formalise equivalence of processes and infinite data
1.23 + structures.
1.24 +
1.25 + \medskip The HOL package is related to the ZF one, which is
1.26 + described in a separate paper,\footnote{It appeared in CADE
1.27 + \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
1.28 + which you should refer to in case of difficulties. The package is
1.29 + simpler than that of ZF thanks to implicit type-checking in HOL.
1.30 + The types of the (co)inductive predicates (or sets) determine the
1.31 + domain of the fixedpoint definition, and the package does not have
1.32 + to use inference rules for type-checking.
1.33 +
1.34 + \begin{matharray}{rcl}
1.35 + \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.36 + \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.37 + \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.38 + \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.39 + \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
1.40 + \end{matharray}
1.41 +
1.42 + \begin{railoutput}
1.43 +\rail@begin{7}{}
1.44 +\rail@bar
1.45 +\rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
1.46 +\rail@nextbar{1}
1.47 +\rail@term{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1.48 +\rail@nextbar{2}
1.49 +\rail@term{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]
1.50 +\rail@nextbar{3}
1.51 +\rail@term{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1.52 +\rail@endbar
1.53 +\rail@bar
1.54 +\rail@nextbar{1}
1.55 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.56 +\rail@endbar
1.57 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.58 +\rail@bar
1.59 +\rail@nextbar{1}
1.60 +\rail@term{\isa{\isakeyword{for}}}[]
1.61 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.62 +\rail@endbar
1.63 +\rail@cr{5}
1.64 +\rail@bar
1.65 +\rail@nextbar{6}
1.66 +\rail@term{\isa{\isakeyword{where}}}[]
1.67 +\rail@nont{\isa{clauses}}[]
1.68 +\rail@endbar
1.69 +\rail@bar
1.70 +\rail@nextbar{6}
1.71 +\rail@term{\isa{\isakeyword{monos}}}[]
1.72 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.73 +\rail@endbar
1.74 +\rail@end
1.75 +\rail@begin{3}{\isa{clauses}}
1.76 +\rail@plus
1.77 +\rail@bar
1.78 +\rail@nextbar{1}
1.79 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.80 +\rail@endbar
1.81 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.82 +\rail@nextplus{2}
1.83 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.84 +\rail@endplus
1.85 +\rail@end
1.86 +\rail@begin{3}{}
1.87 +\rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
1.88 +\rail@bar
1.89 +\rail@nextbar{1}
1.90 +\rail@term{\isa{add}}[]
1.91 +\rail@nextbar{2}
1.92 +\rail@term{\isa{del}}[]
1.93 +\rail@endbar
1.94 +\rail@end
1.95 +\end{railoutput}
1.96 +
1.97 +
1.98 + \begin{description}
1.99 +
1.100 + \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.101 + introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part. The
1.102 + optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the
1.103 + (co)inductive predicates that remain fixed throughout the
1.104 + definition. The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains
1.105 + \emph{monotonicity theorems}, which are required for each operator
1.106 + applied to a recursive set in the introduction rules. There
1.107 + \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.108 + for each premise \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}} in an introduction rule!
1.109 +
1.110 + \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.111 + allowing the definition of (co)inductive sets.
1.112 +
1.113 + \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules. These
1.114 + rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}.
1.115 +
1.116 + \end{description}%
1.117 +\end{isamarkuptext}%
1.118 +\isamarkuptrue%
1.119 +%
1.120 +\isamarkupsubsection{Derived rules%
1.121 +}
1.122 +\isamarkuptrue%
1.123 +%
1.124 +\begin{isamarkuptext}%
1.125 +Each (co)inductive definition \isa{R} adds definitions to the
1.126 + theory and also proves some theorems:
1.127 +
1.128 + \begin{description}
1.129 +
1.130 + \item \isa{R{\isaliteral{2E}{\isachardot}}intros} is the list of introduction rules as proven
1.131 + theorems, for the recursive predicates (or sets). The rules are
1.132 + also available individually, using the names given them in the
1.133 + theory file;
1.134 +
1.135 + \item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
1.136 +
1.137 + \item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
1.138 + rule.
1.139 +
1.140 + \end{description}
1.141 +
1.142 + 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.143 + defined simultaneously, the list of introduction rules is called
1.144 + \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.145 + 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.146 + 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.147 +\end{isamarkuptext}%
1.148 +\isamarkuptrue%
1.149 +%
1.150 +\isamarkupsubsection{Monotonicity theorems%
1.151 +}
1.152 +\isamarkuptrue%
1.153 +%
1.154 +\begin{isamarkuptext}%
1.155 +Each theory contains a default set of theorems that are used in
1.156 + monotonicity proofs. New rules can be added to this set via the
1.157 + \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute. The HOL theory \isa{Inductive}
1.158 + shows how this is done. In general, the following monotonicity
1.159 + theorems may be added:
1.160 +
1.161 + \begin{itemize}
1.162 +
1.163 + \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.164 + monotonicity of inductive definitions whose introduction rules have
1.165 + premises involving terms such as \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}}.
1.166 +
1.167 + \item Monotonicity theorems for logical operators, which are of the
1.168 + 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.169 + the case of the operator \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, the corresponding theorem is
1.170 + \[
1.171 + \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.172 + \]
1.173 +
1.174 + \item De Morgan style equations for reasoning about the ``polarity''
1.175 + of expressions, e.g.
1.176 + \[
1.177 + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ P{\isaliteral{22}{\isachardoublequote}}} \qquad\qquad
1.178 + \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.179 + \]
1.180 +
1.181 + \item Equations for reducing complex operators to more primitive
1.182 + ones whose monotonicity can easily be proved, e.g.
1.183 + \[
1.184 + \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.185 + \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.186 + \]
1.187 +
1.188 + \end{itemize}
1.189 +
1.190 + %FIXME: Example of an inductive definition%
1.191 +\end{isamarkuptext}%
1.192 +\isamarkuptrue%
1.193 +%
1.194 +\isamarkupsection{Recursive functions \label{sec:recursion}%
1.195 +}
1.196 +\isamarkuptrue%
1.197 +%
1.198 +\begin{isamarkuptext}%
1.199 +\begin{matharray}{rcl}
1.200 + \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.201 + \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.202 + \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.203 + \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.204 + \end{matharray}
1.205 +
1.206 + \begin{railoutput}
1.207 +\rail@begin{2}{}
1.208 +\rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
1.209 +\rail@bar
1.210 +\rail@nextbar{1}
1.211 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.212 +\rail@endbar
1.213 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.214 +\rail@term{\isa{\isakeyword{where}}}[]
1.215 +\rail@nont{\isa{equations}}[]
1.216 +\rail@end
1.217 +\rail@begin{4}{}
1.218 +\rail@bar
1.219 +\rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
1.220 +\rail@nextbar{1}
1.221 +\rail@term{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}}[]
1.222 +\rail@endbar
1.223 +\rail@bar
1.224 +\rail@nextbar{1}
1.225 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.226 +\rail@endbar
1.227 +\rail@bar
1.228 +\rail@nextbar{1}
1.229 +\rail@nont{\isa{functionopts}}[]
1.230 +\rail@endbar
1.231 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.232 +\rail@cr{3}
1.233 +\rail@term{\isa{\isakeyword{where}}}[]
1.234 +\rail@nont{\isa{equations}}[]
1.235 +\rail@end
1.236 +\rail@begin{3}{\isa{equations}}
1.237 +\rail@plus
1.238 +\rail@bar
1.239 +\rail@nextbar{1}
1.240 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.241 +\rail@endbar
1.242 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.243 +\rail@nextplus{2}
1.244 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.245 +\rail@endplus
1.246 +\rail@end
1.247 +\rail@begin{3}{\isa{functionopts}}
1.248 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.249 +\rail@plus
1.250 +\rail@bar
1.251 +\rail@term{\isa{sequential}}[]
1.252 +\rail@nextbar{1}
1.253 +\rail@term{\isa{domintros}}[]
1.254 +\rail@endbar
1.255 +\rail@nextplus{2}
1.256 +\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
1.257 +\rail@endplus
1.258 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.259 +\rail@end
1.260 +\rail@begin{2}{}
1.261 +\rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
1.262 +\rail@bar
1.263 +\rail@nextbar{1}
1.264 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.265 +\rail@endbar
1.266 +\rail@end
1.267 +\end{railoutput}
1.268 +
1.269 +
1.270 + \begin{description}
1.271 +
1.272 + \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
1.273 + functions over datatypes, see also \cite{isabelle-HOL}.
1.274 +
1.275 + \item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
1.276 + wellfounded recursion. A detailed description with examples can be
1.277 + found in \cite{isabelle-function}. The function is specified by a
1.278 + set of (possibly conditional) recursive equations with arbitrary
1.279 + pattern matching. The command generates proof obligations for the
1.280 + completeness and the compatibility of patterns.
1.281 +
1.282 + The defined function is considered partial, and the resulting
1.283 + simplification rules (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}psimps{\isaliteral{22}{\isachardoublequote}}}) and induction rule
1.284 + (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}pinduct{\isaliteral{22}{\isachardoublequote}}}) are guarded by a generated domain
1.285 + predicate \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5F}{\isacharunderscore}}dom{\isaliteral{22}{\isachardoublequote}}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}
1.286 + command can then be used to establish that the function is total.
1.287 +
1.288 + \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.289 + proof attempts regarding pattern matching and termination. See
1.290 + \cite{isabelle-function} for further details.
1.291 +
1.292 + \item \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f} commences a
1.293 + termination proof for the previously defined function \isa{f}. If
1.294 + this is omitted, the command refers to the most recent function
1.295 + definition. After the proof is closed, the recursive equations and
1.296 + the induction principle is established.
1.297 +
1.298 + \end{description}
1.299 +
1.300 + Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
1.301 + command accommodate
1.302 + 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.303 + refers to a specific induction rule, with parameters named according
1.304 + to the user-specified equations. Cases are numbered (starting from 1).
1.305 +
1.306 + For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
1.307 + with structural recursion on the datatype the recursion is carried
1.308 + out.
1.309 +
1.310 + The equations provided by these packages may be referred later as
1.311 + theorem list \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, where \isa{f} is the (collective)
1.312 + name of the functions defined. Individual equations may be named
1.313 + explicitly as well.
1.314 +
1.315 + The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following
1.316 + options.
1.317 +
1.318 + \begin{description}
1.319 +
1.320 + \item \isa{sequential} enables a preprocessor which disambiguates
1.321 + overlapping patterns by making them mutually disjoint. Earlier
1.322 + equations take precedence over later ones. This allows to give the
1.323 + specification in a format very similar to functional programming.
1.324 + Note that the resulting simplification and induction rules
1.325 + correspond to the transformed specification, not the one given
1.326 + originally. This usually means that each equation given by the user
1.327 + may result in several theorems. Also note that this automatic
1.328 + transformation only works for ML-style datatype patterns.
1.329 +
1.330 + \item \isa{domintros} enables the automated generation of
1.331 + introduction rules for the domain predicate. While mostly not
1.332 + needed, they can be helpful in some proofs about partial functions.
1.333 +
1.334 + \end{description}%
1.335 +\end{isamarkuptext}%
1.336 +\isamarkuptrue%
1.337 +%
1.338 +\isamarkupsubsection{Proof methods related to recursive definitions%
1.339 +}
1.340 +\isamarkuptrue%
1.341 +%
1.342 +\begin{isamarkuptext}%
1.343 +\begin{matharray}{rcl}
1.344 + \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.345 + \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
1.346 + \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.347 + \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.348 + \end{matharray}
1.349 +
1.350 + \begin{railoutput}
1.351 +\rail@begin{1}{}
1.352 +\rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
1.353 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.354 +\rail@end
1.355 +\rail@begin{2}{}
1.356 +\rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
1.357 +\rail@plus
1.358 +\rail@nextplus{1}
1.359 +\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.360 +\rail@endplus
1.361 +\rail@end
1.362 +\rail@begin{2}{}
1.363 +\rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
1.364 +\rail@nont{\isa{orders}}[]
1.365 +\rail@plus
1.366 +\rail@nextplus{1}
1.367 +\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.368 +\rail@endplus
1.369 +\rail@end
1.370 +\rail@begin{4}{\isa{orders}}
1.371 +\rail@plus
1.372 +\rail@nextplus{1}
1.373 +\rail@bar
1.374 +\rail@term{\isa{max}}[]
1.375 +\rail@nextbar{2}
1.376 +\rail@term{\isa{min}}[]
1.377 +\rail@nextbar{3}
1.378 +\rail@term{\isa{ms}}[]
1.379 +\rail@endbar
1.380 +\rail@endplus
1.381 +\rail@end
1.382 +\end{railoutput}
1.383 +
1.384 +
1.385 + \begin{description}
1.386 +
1.387 + \item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}} is a specialized method to
1.388 + solve goals regarding the completeness of pattern matching, as
1.389 + required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
1.390 + \cite{isabelle-function}).
1.391 +
1.392 + \item \hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R} introduces a termination
1.393 + proof using the relation \isa{R}. The resulting proof state will
1.394 + contain goals expressing that \isa{R} is wellfounded, and that the
1.395 + arguments of recursive calls decrease with respect to \isa{R}.
1.396 + Usually, this method is used as the initial proof step of manual
1.397 + termination proofs.
1.398 +
1.399 + \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}} attempts a fully
1.400 + automated termination proof by searching for a lexicographic
1.401 + combination of size measures on the arguments of the function. The
1.402 + method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
1.403 + which it uses internally to prove local descents. The same context
1.404 + modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see
1.405 + \secref{sec:clasimp}.
1.406 +
1.407 + In case of failure, extensive information is printed, which can help
1.408 + to analyse the situation (cf.\ \cite{isabelle-function}).
1.409 +
1.410 + \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}} also works on termination goals,
1.411 + using a variation of the size-change principle, together with a
1.412 + graph decomposition technique (see \cite{krauss_phd} for details).
1.413 + Three kinds of orders are used internally: \isa{max}, \isa{min},
1.414 + and \isa{ms} (multiset), which is only available when the theory
1.415 + \isa{Multiset} is loaded. When no order kinds are given, they are
1.416 + tried in order. The search for a termination proof uses SAT solving
1.417 + internally.
1.418 +
1.419 + For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
1.420 +
1.421 + \end{description}%
1.422 +\end{isamarkuptext}%
1.423 +\isamarkuptrue%
1.424 +%
1.425 +\isamarkupsubsection{Functions with explicit partiality%
1.426 +}
1.427 +\isamarkuptrue%
1.428 +%
1.429 +\begin{isamarkuptext}%
1.430 +\begin{matharray}{rcl}
1.431 + \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.432 + \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.433 + \end{matharray}
1.434 +
1.435 + \begin{railoutput}
1.436 +\rail@begin{5}{}
1.437 +\rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
1.438 +\rail@bar
1.439 +\rail@nextbar{1}
1.440 +\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.441 +\rail@endbar
1.442 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.443 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.444 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.445 +\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.446 +\rail@cr{3}
1.447 +\rail@term{\isa{\isakeyword{where}}}[]
1.448 +\rail@bar
1.449 +\rail@nextbar{4}
1.450 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.451 +\rail@endbar
1.452 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.453 +\rail@end
1.454 +\end{railoutput}
1.455 +
1.456 +
1.457 + \begin{description}
1.458 +
1.459 + \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.460 + recursive functions based on fixpoints in complete partial
1.461 + orders. No termination proof is required from the user or
1.462 + constructed internally. Instead, the possibility of non-termination
1.463 + is modelled explicitly in the result type, which contains an
1.464 + explicit bottom element.
1.465 +
1.466 + Pattern matching and mutual recursion are currently not supported.
1.467 + Thus, the specification consists of a single function described by a
1.468 + single recursive equation.
1.469 +
1.470 + There are no fixed syntactic restrictions on the body of the
1.471 + function, but the induced functional must be provably monotonic
1.472 + wrt.\ the underlying order. The monotonicitity proof is performed
1.473 + internally, and the definition is rejected when it fails. The proof
1.474 + can be influenced by declaring hints using the
1.475 + \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} attribute.
1.476 +
1.477 + The mandatory \isa{mode} argument specifies the mode of operation
1.478 + of the command, which directly corresponds to a complete partial
1.479 + order on the result type. By default, the following modes are
1.480 + defined:
1.481 +
1.482 + \begin{description}
1.483 + \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
1.484 + non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
1.485 + must also be \isa{None}. This is best achieved through the use of
1.486 + the monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}.
1.487 +
1.488 + \item \isa{tailrec} defines functions with an arbitrary result
1.489 + 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.490 + if \isa{undefined} is returned by a recursive call, then the
1.491 + overall result must also be \isa{undefined}. In practice, this is
1.492 + only satisfied when each recursive call is a tail call, whose result
1.493 + is directly returned. Thus, this mode of operation allows the
1.494 + definition of arbitrary tail-recursive functions.
1.495 + \end{description}
1.496 +
1.497 + Experienced users may define new modes by instantiating the locale
1.498 + \isa{{\isaliteral{22}{\isachardoublequote}}partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}definitions{\isaliteral{22}{\isachardoublequote}}} appropriately.
1.499 +
1.500 + \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} declares rules for
1.501 + use in the internal monononicity proofs of partial function
1.502 + definitions.
1.503 +
1.504 + \end{description}%
1.505 +\end{isamarkuptext}%
1.506 +\isamarkuptrue%
1.507 +%
1.508 +\isamarkupsubsection{Old-style recursive function definitions (TFL)%
1.509 +}
1.510 +\isamarkuptrue%
1.511 +%
1.512 +\begin{isamarkuptext}%
1.513 +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.514 +
1.515 + \begin{matharray}{rcl}
1.516 + \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.517 + \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.518 + \end{matharray}
1.519 +
1.520 + \begin{railoutput}
1.521 +\rail@begin{5}{}
1.522 +\rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
1.523 +\rail@bar
1.524 +\rail@nextbar{1}
1.525 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.526 +\rail@term{\isa{\isakeyword{permissive}}}[]
1.527 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.528 +\rail@endbar
1.529 +\rail@cr{3}
1.530 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.531 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.532 +\rail@plus
1.533 +\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.534 +\rail@nextplus{4}
1.535 +\rail@endplus
1.536 +\rail@bar
1.537 +\rail@nextbar{4}
1.538 +\rail@nont{\isa{hints}}[]
1.539 +\rail@endbar
1.540 +\rail@end
1.541 +\rail@begin{2}{}
1.542 +\rail@nont{\isa{recdeftc}}[]
1.543 +\rail@bar
1.544 +\rail@nextbar{1}
1.545 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.546 +\rail@endbar
1.547 +\rail@nont{\isa{tc}}[]
1.548 +\rail@end
1.549 +\rail@begin{2}{\isa{hints}}
1.550 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.551 +\rail@term{\isa{\isakeyword{hints}}}[]
1.552 +\rail@plus
1.553 +\rail@nextplus{1}
1.554 +\rail@cnont{\isa{recdefmod}}[]
1.555 +\rail@endplus
1.556 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.557 +\rail@end
1.558 +\rail@begin{4}{\isa{recdefmod}}
1.559 +\rail@bar
1.560 +\rail@bar
1.561 +\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}[]
1.562 +\rail@nextbar{1}
1.563 +\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}[]
1.564 +\rail@nextbar{2}
1.565 +\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}[]
1.566 +\rail@endbar
1.567 +\rail@bar
1.568 +\rail@nextbar{1}
1.569 +\rail@term{\isa{add}}[]
1.570 +\rail@nextbar{2}
1.571 +\rail@term{\isa{del}}[]
1.572 +\rail@endbar
1.573 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.574 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.575 +\rail@nextbar{3}
1.576 +\rail@nont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.577 +\rail@endbar
1.578 +\rail@end
1.579 +\rail@begin{2}{\isa{tc}}
1.580 +\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.581 +\rail@bar
1.582 +\rail@nextbar{1}
1.583 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.584 +\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.585 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.586 +\rail@endbar
1.587 +\rail@end
1.588 +\end{railoutput}
1.589 +
1.590 +
1.591 + \begin{description}
1.592 +
1.593 + \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
1.594 + recursive functions (using the TFL package), see also
1.595 + \cite{isabelle-HOL}. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells
1.596 + TFL to recover from failed proof attempts, returning unfinished
1.597 + 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.598 + automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}
1.599 + declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
1.600 + context of the Simplifier (cf.\ \secref{sec:simplifier}) and
1.601 + Classical reasoner (cf.\ \secref{sec:classical}).
1.602 +
1.603 + \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.604 + proof for leftover termination condition number \isa{i} (default
1.605 + 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
1.606 + constant \isa{c}.
1.607 +
1.608 + Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
1.609 + its internal proofs without manual intervention.
1.610 +
1.611 + \end{description}
1.612 +
1.613 + \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared
1.614 + globally, using the following attributes.
1.615 +
1.616 + \begin{matharray}{rcl}
1.617 + \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.618 + \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.619 + \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.620 + \end{matharray}
1.621 +
1.622 + \begin{railoutput}
1.623 +\rail@begin{3}{}
1.624 +\rail@bar
1.625 +\rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
1.626 +\rail@nextbar{1}
1.627 +\rail@term{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}}[]
1.628 +\rail@nextbar{2}
1.629 +\rail@term{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}}[]
1.630 +\rail@endbar
1.631 +\rail@bar
1.632 +\rail@nextbar{1}
1.633 +\rail@term{\isa{add}}[]
1.634 +\rail@nextbar{2}
1.635 +\rail@term{\isa{del}}[]
1.636 +\rail@endbar
1.637 +\rail@end
1.638 +\end{railoutput}%
1.639 +\end{isamarkuptext}%
1.640 +\isamarkuptrue%
1.641 +%
1.642 +\isamarkupsection{Datatypes \label{sec:hol-datatype}%
1.643 +}
1.644 +\isamarkuptrue%
1.645 +%
1.646 +\begin{isamarkuptext}%
1.647 +\begin{matharray}{rcl}
1.648 + \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.649 + \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.650 + \end{matharray}
1.651 +
1.652 + \begin{railoutput}
1.653 +\rail@begin{2}{}
1.654 +\rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
1.655 +\rail@plus
1.656 +\rail@nont{\isa{spec}}[]
1.657 +\rail@nextplus{1}
1.658 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.659 +\rail@endplus
1.660 +\rail@end
1.661 +\rail@begin{3}{}
1.662 +\rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
1.663 +\rail@bar
1.664 +\rail@nextbar{1}
1.665 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.666 +\rail@plus
1.667 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.668 +\rail@nextplus{2}
1.669 +\rail@endplus
1.670 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.671 +\rail@endbar
1.672 +\rail@plus
1.673 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.674 +\rail@nextplus{1}
1.675 +\rail@endplus
1.676 +\rail@end
1.677 +\rail@begin{2}{\isa{spec}}
1.678 +\rail@bar
1.679 +\rail@nextbar{1}
1.680 +\rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
1.681 +\rail@endbar
1.682 +\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
1.683 +\rail@bar
1.684 +\rail@nextbar{1}
1.685 +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.686 +\rail@endbar
1.687 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.688 +\rail@plus
1.689 +\rail@nont{\isa{cons}}[]
1.690 +\rail@nextplus{1}
1.691 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.692 +\rail@endplus
1.693 +\rail@end
1.694 +\rail@begin{2}{\isa{cons}}
1.695 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.696 +\rail@plus
1.697 +\rail@nextplus{1}
1.698 +\rail@cnont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
1.699 +\rail@endplus
1.700 +\rail@bar
1.701 +\rail@nextbar{1}
1.702 +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.703 +\rail@endbar
1.704 +\rail@end
1.705 +\end{railoutput}
1.706 +
1.707 +
1.708 + \begin{description}
1.709 +
1.710 + \item \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} defines inductive datatypes in
1.711 + HOL.
1.712 +
1.713 + \item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}} represents existing types as
1.714 + inductive ones, generating the standard infrastructure of derived
1.715 + concepts (primitive recursion etc.).
1.716 +
1.717 + \end{description}
1.718 +
1.719 + The induction and exhaustion theorems generated provide case names
1.720 + according to the constructors involved, while parameters are named
1.721 + after the types (see also \secref{sec:cases-induct}).
1.722 +
1.723 + See \cite{isabelle-HOL} for more details on datatypes, but beware of
1.724 + the old-style theory syntax being used there! Apart from proper
1.725 + proof methods for case-analysis and induction, there are also
1.726 + 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.727 + to refer directly to the internal structure of subgoals (including
1.728 + internally bound parameters).%
1.729 +\end{isamarkuptext}%
1.730 +\isamarkuptrue%
1.731 +%
1.732 +\isamarkupsection{Records \label{sec:hol-record}%
1.733 +}
1.734 +\isamarkuptrue%
1.735 +%
1.736 +\begin{isamarkuptext}%
1.737 +In principle, records merely generalize the concept of tuples, where
1.738 + components may be addressed by labels instead of just position. The
1.739 + logical infrastructure of records in Isabelle/HOL is slightly more
1.740 + advanced, though, supporting truly extensible record schemes. This
1.741 + admits operations that are polymorphic with respect to record
1.742 + extension, yielding ``object-oriented'' effects like (single)
1.743 + inheritance. See also \cite{NaraschewskiW-TPHOLs98} for more
1.744 + details on object-oriented verification and record subtyping in HOL.%
1.745 +\end{isamarkuptext}%
1.746 +\isamarkuptrue%
1.747 +%
1.748 +\isamarkupsubsection{Basic concepts%
1.749 +}
1.750 +\isamarkuptrue%
1.751 +%
1.752 +\begin{isamarkuptext}%
1.753 +Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
1.754 + at the level of terms and types. The notation is as follows:
1.755 +
1.756 + \begin{center}
1.757 + \begin{tabular}{l|l|l}
1.758 + & record terms & record types \\ \hline
1.759 + fixed & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.760 + schematic & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} &
1.761 + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ M{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.762 + \end{tabular}
1.763 + \end{center}
1.764 +
1.765 + \noindent The ASCII representation of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{7C}{\isacharbar}}\ x\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
1.766 +
1.767 + A fixed record \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} has field \isa{x} of value
1.768 + \isa{a} and field \isa{y} of value \isa{b}. The corresponding
1.769 + type is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, assuming that \isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{22}{\isachardoublequote}}}
1.770 + and \isa{{\isaliteral{22}{\isachardoublequote}}b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{22}{\isachardoublequote}}}.
1.771 +
1.772 + A record scheme like \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} contains fields
1.773 + \isa{x} and \isa{y} as before, but also possibly further fields
1.774 + as indicated by the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' notation (which is actually part
1.775 + of the syntax). The improper field ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' of a record
1.776 + scheme is called the \emph{more part}. Logically it is just a free
1.777 + variable, which is occasionally referred to as ``row variable'' in
1.778 + the literature. The more part of a record scheme may be
1.779 + instantiated by zero or more further components. For example, the
1.780 + previous scheme may get instantiated to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{m{\isaliteral{27}{\isacharprime}}} refers to a different more part.
1.781 + Fixed records are special instances of record schemes, where
1.782 + ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' is properly terminated by the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ unit{\isaliteral{22}{\isachardoublequote}}}
1.783 + element. In fact, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is just an abbreviation
1.784 + for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.
1.785 +
1.786 + \medskip Two key observations make extensible records in a simply
1.787 + typed language like HOL work out:
1.788 +
1.789 + \begin{enumerate}
1.790 +
1.791 + \item the more part is internalized, as a free term or type
1.792 + variable,
1.793 +
1.794 + \item field names are externalized, they cannot be accessed within
1.795 + the logic as first-class values.
1.796 +
1.797 + \end{enumerate}
1.798 +
1.799 + \medskip In Isabelle/HOL record types have to be defined explicitly,
1.800 + fixing their field names and types, and their (optional) parent
1.801 + record. Afterwards, records may be formed using above syntax, while
1.802 + obeying the canonical order of fields as given by their declaration.
1.803 + The record package provides several standard operations like
1.804 + selectors and updates. The common setup for various generic proof
1.805 + tools enable succinct reasoning patterns. See also the Isabelle/HOL
1.806 + tutorial \cite{isabelle-hol-book} for further instructions on using
1.807 + records in practice.%
1.808 +\end{isamarkuptext}%
1.809 +\isamarkuptrue%
1.810 +%
1.811 +\isamarkupsubsection{Record specifications%
1.812 +}
1.813 +\isamarkuptrue%
1.814 +%
1.815 +\begin{isamarkuptext}%
1.816 +\begin{matharray}{rcl}
1.817 + \indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1.818 + \end{matharray}
1.819 +
1.820 + \begin{railoutput}
1.821 +\rail@begin{4}{}
1.822 +\rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
1.823 +\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
1.824 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.825 +\rail@cr{2}
1.826 +\rail@bar
1.827 +\rail@nextbar{3}
1.828 +\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
1.829 +\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
1.830 +\rail@endbar
1.831 +\rail@plus
1.832 +\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
1.833 +\rail@nextplus{3}
1.834 +\rail@endplus
1.835 +\rail@end
1.836 +\end{railoutput}
1.837 +
1.838 +
1.839 + \begin{description}
1.840 +
1.841 + \item \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{2B}{\isacharplus}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} defines extensible record type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}},
1.842 + derived from the optional parent record \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} by adding new
1.843 + field components \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} etc.
1.844 +
1.845 + The type variables of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} need to be
1.846 + covered by the (distinct) parameters \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}. Type constructor \isa{t} has to be new, while \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} needs to specify an instance of an existing record type. At
1.847 + least one new field \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} has to be specified.
1.848 + Basically, field names need to belong to a unique record. This is
1.849 + not a real restriction in practice, since fields are qualified by
1.850 + the record name internally.
1.851 +
1.852 + The parent record specification \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is optional; if omitted
1.853 + \isa{t} becomes a root record. The hierarchy of all records
1.854 + declared within a theory context forms a forest structure, i.e.\ a
1.855 + set of trees starting with a root record each. There is no way to
1.856 + merge multiple parent records!
1.857 +
1.858 + For convenience, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} is made a
1.859 + type abbreviation for the fixed record type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, likewise is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{22}{\isachardoublequote}}} made an abbreviation for
1.860 + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.
1.861 +
1.862 + \end{description}%
1.863 +\end{isamarkuptext}%
1.864 +\isamarkuptrue%
1.865 +%
1.866 +\isamarkupsubsection{Record operations%
1.867 +}
1.868 +\isamarkuptrue%
1.869 +%
1.870 +\begin{isamarkuptext}%
1.871 +Any record definition of the form presented above produces certain
1.872 + standard operations. Selectors and updates are provided for any
1.873 + field, including the improper one ``\isa{more}''. There are also
1.874 + cumulative record constructor functions. To simplify the
1.875 + presentation below, we assume for now that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} is a root record with fields \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.
1.876 +
1.877 + \medskip \textbf{Selectors} and \textbf{updates} are available for
1.878 + any field (including ``\isa{more}''):
1.879 +
1.880 + \begin{matharray}{lll}
1.881 + \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} \\
1.882 + \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5F}{\isacharunderscore}}update{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.883 + \end{matharray}
1.884 +
1.885 + There is special syntax for application of updates: \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} abbreviates term \isa{{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{5F}{\isacharunderscore}}update\ a\ r{\isaliteral{22}{\isachardoublequote}}}. Further notation for
1.886 + repeated updates is also available: \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} may be written \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}. Note that
1.887 + because of postfix notation the order of fields shown here is
1.888 + reverse than in the actual term. Since repeated updates are just
1.889 + function applications, fields may be freely permuted in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, as far as logical equality is concerned.
1.890 + Thus commutativity of independent updates can be proven within the
1.891 + logic for any two fields, but not as a general theorem.
1.892 +
1.893 + \medskip The \textbf{make} operation provides a cumulative record
1.894 + constructor function:
1.895 +
1.896 + \begin{matharray}{lll}
1.897 + \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.898 + \end{matharray}
1.899 +
1.900 + \medskip We now reconsider the case of non-root records, which are
1.901 + derived of some parent. In general, the latter may depend on
1.902 + another parent as well, resulting in a list of \emph{ancestor
1.903 + records}. Appending the lists of fields of all ancestors results in
1.904 + a certain field prefix. The record package automatically takes care
1.905 + of this by lifting operations over this context of ancestor fields.
1.906 + Assuming that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} has ancestor
1.907 + fields \isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}},
1.908 + the above record operations will get the following types:
1.909 +
1.910 + \medskip
1.911 + \begin{tabular}{lll}
1.912 + \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} \\
1.913 + \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5F}{\isacharunderscore}}update{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.914 + \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.915 + \end{tabular}
1.916 + \medskip
1.917 +
1.918 + \noindent Some further operations address the extension aspect of a
1.919 + derived record scheme specifically: \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} produces a
1.920 + record fragment consisting of exactly the new fields introduced here
1.921 + (the result may serve as a more part elsewhere); \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}
1.922 + takes a fixed record and adds a given more part; \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} restricts a record scheme to a fixed record.
1.923 +
1.924 + \medskip
1.925 + \begin{tabular}{lll}
1.926 + \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.927 + \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.928 + \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.929 + \end{tabular}
1.930 + \medskip
1.931 +
1.932 + \noindent Note that \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} coincide
1.933 + for root records.%
1.934 +\end{isamarkuptext}%
1.935 +\isamarkuptrue%
1.936 +%
1.937 +\isamarkupsubsection{Derived rules and proof tools%
1.938 +}
1.939 +\isamarkuptrue%
1.940 +%
1.941 +\begin{isamarkuptext}%
1.942 +The record package proves several results internally, declaring
1.943 + these facts to appropriate proof tools. This enables users to
1.944 + reason about record structures quite conveniently. Assume that
1.945 + \isa{t} is a record type as specified above.
1.946 +
1.947 + \begin{enumerate}
1.948 +
1.949 + \item Standard conversions for selectors or updates applied to
1.950 + record constructor terms are made part of the default Simplifier
1.951 + context; thus proofs by reduction of basic operations merely require
1.952 + the \hyperlink{method.simp}{\mbox{\isa{simp}}} method without further arguments. These rules
1.953 + are available as \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, too.
1.954 +
1.955 + \item Selectors applied to updated records are automatically reduced
1.956 + by an internal simplification procedure, which is also part of the
1.957 + standard Simplifier setup.
1.958 +
1.959 + \item Inject equations of a form analogous to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} are declared to the Simplifier and Classical
1.960 + Reasoner as \hyperlink{attribute.iff}{\mbox{\isa{iff}}} rules. These rules are available as
1.961 + \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}iffs{\isaliteral{22}{\isachardoublequote}}}.
1.962 +
1.963 + \item The introduction rule for record equality analogous to \isa{{\isaliteral{22}{\isachardoublequote}}x\ r\ {\isaliteral{3D}{\isacharequal}}\ x\ r{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ y\ r\ {\isaliteral{3D}{\isacharequal}}\ y\ r{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} is declared to the Simplifier,
1.964 + and as the basic rule context as ``\hyperlink{attribute.intro}{\mbox{\isa{intro}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}''.
1.965 + The rule is called \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}equality{\isaliteral{22}{\isachardoublequote}}}.
1.966 +
1.967 + \item Representations of arbitrary record expressions as canonical
1.968 + constructor terms are provided both in \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} format (cf.\ the generic proof methods of the same name,
1.969 + \secref{sec:cases-induct}). Several variations are available, for
1.970 + fixed records, record schemes, more parts etc.
1.971 +
1.972 + The generic proof methods are sufficiently smart to pick the most
1.973 + sensible rule according to the type of the indicated record
1.974 + expression: users just need to apply something like ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}cases\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' to a certain proof problem.
1.975 +
1.976 + \item The derived record operations \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} are \emph{not}
1.977 + treated automatically, but usually need to be expanded by hand,
1.978 + using the collective fact \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}defs{\isaliteral{22}{\isachardoublequote}}}.
1.979 +
1.980 + \end{enumerate}%
1.981 +\end{isamarkuptext}%
1.982 +\isamarkuptrue%
1.983 +%
1.984 +\isamarkupsection{Adhoc tuples%
1.985 +}
1.986 +\isamarkuptrue%
1.987 +%
1.988 +\begin{isamarkuptext}%
1.989 +\begin{matharray}{rcl}
1.990 + \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.991 + \end{matharray}
1.992 +
1.993 + \begin{railoutput}
1.994 +\rail@begin{2}{}
1.995 +\rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
1.996 +\rail@bar
1.997 +\rail@nextbar{1}
1.998 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.999 +\rail@term{\isa{complete}}[]
1.1000 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1001 +\rail@endbar
1.1002 +\rail@end
1.1003 +\end{railoutput}
1.1004 +
1.1005 +
1.1006 + \begin{description}
1.1007 +
1.1008 + \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.1009 + arguments in function applications to be represented canonically
1.1010 + according to their tuple type structure.
1.1011 +
1.1012 + Note that this operation tends to invent funny names for new local
1.1013 + parameters introduced.
1.1014 +
1.1015 + \end{description}%
1.1016 +\end{isamarkuptext}%
1.1017 +\isamarkuptrue%
1.1018 +%
1.1019 \isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}%
1.1020 }
1.1021 \isamarkuptrue%
1.1022 @@ -253,383 +1265,6 @@
1.1023 \end{isamarkuptext}%
1.1024 \isamarkuptrue%
1.1025 %
1.1026 -\isamarkupsection{Adhoc tuples%
1.1027 -}
1.1028 -\isamarkuptrue%
1.1029 -%
1.1030 -\begin{isamarkuptext}%
1.1031 -\begin{matharray}{rcl}
1.1032 - \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.1033 - \end{matharray}
1.1034 -
1.1035 - \begin{railoutput}
1.1036 -\rail@begin{2}{}
1.1037 -\rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
1.1038 -\rail@bar
1.1039 -\rail@nextbar{1}
1.1040 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1041 -\rail@term{\isa{complete}}[]
1.1042 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1043 -\rail@endbar
1.1044 -\rail@end
1.1045 -\end{railoutput}
1.1046 -
1.1047 -
1.1048 - \begin{description}
1.1049 -
1.1050 - \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.1051 - arguments in function applications to be represented canonically
1.1052 - according to their tuple type structure.
1.1053 -
1.1054 - Note that this operation tends to invent funny names for new local
1.1055 - parameters introduced.
1.1056 -
1.1057 - \end{description}%
1.1058 -\end{isamarkuptext}%
1.1059 -\isamarkuptrue%
1.1060 -%
1.1061 -\isamarkupsection{Records \label{sec:hol-record}%
1.1062 -}
1.1063 -\isamarkuptrue%
1.1064 -%
1.1065 -\begin{isamarkuptext}%
1.1066 -In principle, records merely generalize the concept of tuples, where
1.1067 - components may be addressed by labels instead of just position. The
1.1068 - logical infrastructure of records in Isabelle/HOL is slightly more
1.1069 - advanced, though, supporting truly extensible record schemes. This
1.1070 - admits operations that are polymorphic with respect to record
1.1071 - extension, yielding ``object-oriented'' effects like (single)
1.1072 - inheritance. See also \cite{NaraschewskiW-TPHOLs98} for more
1.1073 - details on object-oriented verification and record subtyping in HOL.%
1.1074 -\end{isamarkuptext}%
1.1075 -\isamarkuptrue%
1.1076 -%
1.1077 -\isamarkupsubsection{Basic concepts%
1.1078 -}
1.1079 -\isamarkuptrue%
1.1080 -%
1.1081 -\begin{isamarkuptext}%
1.1082 -Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
1.1083 - at the level of terms and types. The notation is as follows:
1.1084 -
1.1085 - \begin{center}
1.1086 - \begin{tabular}{l|l|l}
1.1087 - & record terms & record types \\ \hline
1.1088 - fixed & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.1089 - schematic & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} &
1.1090 - \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ M{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.1091 - \end{tabular}
1.1092 - \end{center}
1.1093 -
1.1094 - \noindent The ASCII representation of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{7C}{\isacharbar}}\ x\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
1.1095 -
1.1096 - A fixed record \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} has field \isa{x} of value
1.1097 - \isa{a} and field \isa{y} of value \isa{b}. The corresponding
1.1098 - type is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, assuming that \isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{22}{\isachardoublequote}}}
1.1099 - and \isa{{\isaliteral{22}{\isachardoublequote}}b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{22}{\isachardoublequote}}}.
1.1100 -
1.1101 - A record scheme like \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} contains fields
1.1102 - \isa{x} and \isa{y} as before, but also possibly further fields
1.1103 - as indicated by the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' notation (which is actually part
1.1104 - of the syntax). The improper field ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' of a record
1.1105 - scheme is called the \emph{more part}. Logically it is just a free
1.1106 - variable, which is occasionally referred to as ``row variable'' in
1.1107 - the literature. The more part of a record scheme may be
1.1108 - instantiated by zero or more further components. For example, the
1.1109 - previous scheme may get instantiated to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{m{\isaliteral{27}{\isacharprime}}} refers to a different more part.
1.1110 - Fixed records are special instances of record schemes, where
1.1111 - ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' is properly terminated by the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ unit{\isaliteral{22}{\isachardoublequote}}}
1.1112 - element. In fact, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is just an abbreviation
1.1113 - for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.
1.1114 -
1.1115 - \medskip Two key observations make extensible records in a simply
1.1116 - typed language like HOL work out:
1.1117 -
1.1118 - \begin{enumerate}
1.1119 -
1.1120 - \item the more part is internalized, as a free term or type
1.1121 - variable,
1.1122 -
1.1123 - \item field names are externalized, they cannot be accessed within
1.1124 - the logic as first-class values.
1.1125 -
1.1126 - \end{enumerate}
1.1127 -
1.1128 - \medskip In Isabelle/HOL record types have to be defined explicitly,
1.1129 - fixing their field names and types, and their (optional) parent
1.1130 - record. Afterwards, records may be formed using above syntax, while
1.1131 - obeying the canonical order of fields as given by their declaration.
1.1132 - The record package provides several standard operations like
1.1133 - selectors and updates. The common setup for various generic proof
1.1134 - tools enable succinct reasoning patterns. See also the Isabelle/HOL
1.1135 - tutorial \cite{isabelle-hol-book} for further instructions on using
1.1136 - records in practice.%
1.1137 -\end{isamarkuptext}%
1.1138 -\isamarkuptrue%
1.1139 -%
1.1140 -\isamarkupsubsection{Record specifications%
1.1141 -}
1.1142 -\isamarkuptrue%
1.1143 -%
1.1144 -\begin{isamarkuptext}%
1.1145 -\begin{matharray}{rcl}
1.1146 - \indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1.1147 - \end{matharray}
1.1148 -
1.1149 - \begin{railoutput}
1.1150 -\rail@begin{4}{}
1.1151 -\rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
1.1152 -\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
1.1153 -\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.1154 -\rail@cr{2}
1.1155 -\rail@bar
1.1156 -\rail@nextbar{3}
1.1157 -\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
1.1158 -\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
1.1159 -\rail@endbar
1.1160 -\rail@plus
1.1161 -\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
1.1162 -\rail@nextplus{3}
1.1163 -\rail@endplus
1.1164 -\rail@end
1.1165 -\end{railoutput}
1.1166 -
1.1167 -
1.1168 - \begin{description}
1.1169 -
1.1170 - \item \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{2B}{\isacharplus}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} defines extensible record type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}},
1.1171 - derived from the optional parent record \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} by adding new
1.1172 - field components \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} etc.
1.1173 -
1.1174 - The type variables of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} need to be
1.1175 - covered by the (distinct) parameters \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}. Type constructor \isa{t} has to be new, while \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} needs to specify an instance of an existing record type. At
1.1176 - least one new field \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} has to be specified.
1.1177 - Basically, field names need to belong to a unique record. This is
1.1178 - not a real restriction in practice, since fields are qualified by
1.1179 - the record name internally.
1.1180 -
1.1181 - The parent record specification \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is optional; if omitted
1.1182 - \isa{t} becomes a root record. The hierarchy of all records
1.1183 - declared within a theory context forms a forest structure, i.e.\ a
1.1184 - set of trees starting with a root record each. There is no way to
1.1185 - merge multiple parent records!
1.1186 -
1.1187 - For convenience, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} is made a
1.1188 - type abbreviation for the fixed record type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, likewise is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{22}{\isachardoublequote}}} made an abbreviation for
1.1189 - \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.
1.1190 -
1.1191 - \end{description}%
1.1192 -\end{isamarkuptext}%
1.1193 -\isamarkuptrue%
1.1194 -%
1.1195 -\isamarkupsubsection{Record operations%
1.1196 -}
1.1197 -\isamarkuptrue%
1.1198 -%
1.1199 -\begin{isamarkuptext}%
1.1200 -Any record definition of the form presented above produces certain
1.1201 - standard operations. Selectors and updates are provided for any
1.1202 - field, including the improper one ``\isa{more}''. There are also
1.1203 - cumulative record constructor functions. To simplify the
1.1204 - presentation below, we assume for now that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} is a root record with fields \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.
1.1205 -
1.1206 - \medskip \textbf{Selectors} and \textbf{updates} are available for
1.1207 - any field (including ``\isa{more}''):
1.1208 -
1.1209 - \begin{matharray}{lll}
1.1210 - \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} \\
1.1211 - \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5F}{\isacharunderscore}}update{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.1212 - \end{matharray}
1.1213 -
1.1214 - There is special syntax for application of updates: \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} abbreviates term \isa{{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{5F}{\isacharunderscore}}update\ a\ r{\isaliteral{22}{\isachardoublequote}}}. Further notation for
1.1215 - repeated updates is also available: \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} may be written \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}. Note that
1.1216 - because of postfix notation the order of fields shown here is
1.1217 - reverse than in the actual term. Since repeated updates are just
1.1218 - function applications, fields may be freely permuted in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, as far as logical equality is concerned.
1.1219 - Thus commutativity of independent updates can be proven within the
1.1220 - logic for any two fields, but not as a general theorem.
1.1221 -
1.1222 - \medskip The \textbf{make} operation provides a cumulative record
1.1223 - constructor function:
1.1224 -
1.1225 - \begin{matharray}{lll}
1.1226 - \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.1227 - \end{matharray}
1.1228 -
1.1229 - \medskip We now reconsider the case of non-root records, which are
1.1230 - derived of some parent. In general, the latter may depend on
1.1231 - another parent as well, resulting in a list of \emph{ancestor
1.1232 - records}. Appending the lists of fields of all ancestors results in
1.1233 - a certain field prefix. The record package automatically takes care
1.1234 - of this by lifting operations over this context of ancestor fields.
1.1235 - Assuming that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} has ancestor
1.1236 - fields \isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}},
1.1237 - the above record operations will get the following types:
1.1238 -
1.1239 - \medskip
1.1240 - \begin{tabular}{lll}
1.1241 - \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} \\
1.1242 - \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5F}{\isacharunderscore}}update{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.1243 - \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.1244 - \end{tabular}
1.1245 - \medskip
1.1246 -
1.1247 - \noindent Some further operations address the extension aspect of a
1.1248 - derived record scheme specifically: \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} produces a
1.1249 - record fragment consisting of exactly the new fields introduced here
1.1250 - (the result may serve as a more part elsewhere); \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}
1.1251 - takes a fixed record and adds a given more part; \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} restricts a record scheme to a fixed record.
1.1252 -
1.1253 - \medskip
1.1254 - \begin{tabular}{lll}
1.1255 - \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.1256 - \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.1257 - \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
1.1258 - \end{tabular}
1.1259 - \medskip
1.1260 -
1.1261 - \noindent Note that \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} coincide
1.1262 - for root records.%
1.1263 -\end{isamarkuptext}%
1.1264 -\isamarkuptrue%
1.1265 -%
1.1266 -\isamarkupsubsection{Derived rules and proof tools%
1.1267 -}
1.1268 -\isamarkuptrue%
1.1269 -%
1.1270 -\begin{isamarkuptext}%
1.1271 -The record package proves several results internally, declaring
1.1272 - these facts to appropriate proof tools. This enables users to
1.1273 - reason about record structures quite conveniently. Assume that
1.1274 - \isa{t} is a record type as specified above.
1.1275 -
1.1276 - \begin{enumerate}
1.1277 -
1.1278 - \item Standard conversions for selectors or updates applied to
1.1279 - record constructor terms are made part of the default Simplifier
1.1280 - context; thus proofs by reduction of basic operations merely require
1.1281 - the \hyperlink{method.simp}{\mbox{\isa{simp}}} method without further arguments. These rules
1.1282 - are available as \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, too.
1.1283 -
1.1284 - \item Selectors applied to updated records are automatically reduced
1.1285 - by an internal simplification procedure, which is also part of the
1.1286 - standard Simplifier setup.
1.1287 -
1.1288 - \item Inject equations of a form analogous to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} are declared to the Simplifier and Classical
1.1289 - Reasoner as \hyperlink{attribute.iff}{\mbox{\isa{iff}}} rules. These rules are available as
1.1290 - \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}iffs{\isaliteral{22}{\isachardoublequote}}}.
1.1291 -
1.1292 - \item The introduction rule for record equality analogous to \isa{{\isaliteral{22}{\isachardoublequote}}x\ r\ {\isaliteral{3D}{\isacharequal}}\ x\ r{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ y\ r\ {\isaliteral{3D}{\isacharequal}}\ y\ r{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} is declared to the Simplifier,
1.1293 - and as the basic rule context as ``\hyperlink{attribute.intro}{\mbox{\isa{intro}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}''.
1.1294 - The rule is called \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}equality{\isaliteral{22}{\isachardoublequote}}}.
1.1295 -
1.1296 - \item Representations of arbitrary record expressions as canonical
1.1297 - constructor terms are provided both in \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} format (cf.\ the generic proof methods of the same name,
1.1298 - \secref{sec:cases-induct}). Several variations are available, for
1.1299 - fixed records, record schemes, more parts etc.
1.1300 -
1.1301 - The generic proof methods are sufficiently smart to pick the most
1.1302 - sensible rule according to the type of the indicated record
1.1303 - expression: users just need to apply something like ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}cases\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' to a certain proof problem.
1.1304 -
1.1305 - \item The derived record operations \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} are \emph{not}
1.1306 - treated automatically, but usually need to be expanded by hand,
1.1307 - using the collective fact \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}defs{\isaliteral{22}{\isachardoublequote}}}.
1.1308 -
1.1309 - \end{enumerate}%
1.1310 -\end{isamarkuptext}%
1.1311 -\isamarkuptrue%
1.1312 -%
1.1313 -\isamarkupsection{Datatypes \label{sec:hol-datatype}%
1.1314 -}
1.1315 -\isamarkuptrue%
1.1316 -%
1.1317 -\begin{isamarkuptext}%
1.1318 -\begin{matharray}{rcl}
1.1319 - \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.1320 - \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.1321 - \end{matharray}
1.1322 -
1.1323 - \begin{railoutput}
1.1324 -\rail@begin{2}{}
1.1325 -\rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
1.1326 -\rail@plus
1.1327 -\rail@nont{\isa{spec}}[]
1.1328 -\rail@nextplus{1}
1.1329 -\rail@cterm{\isa{\isakeyword{and}}}[]
1.1330 -\rail@endplus
1.1331 -\rail@end
1.1332 -\rail@begin{3}{}
1.1333 -\rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
1.1334 -\rail@bar
1.1335 -\rail@nextbar{1}
1.1336 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1337 -\rail@plus
1.1338 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1339 -\rail@nextplus{2}
1.1340 -\rail@endplus
1.1341 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1342 -\rail@endbar
1.1343 -\rail@plus
1.1344 -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1345 -\rail@nextplus{1}
1.1346 -\rail@endplus
1.1347 -\rail@end
1.1348 -\rail@begin{2}{\isa{spec}}
1.1349 -\rail@bar
1.1350 -\rail@nextbar{1}
1.1351 -\rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
1.1352 -\rail@endbar
1.1353 -\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
1.1354 -\rail@bar
1.1355 -\rail@nextbar{1}
1.1356 -\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.1357 -\rail@endbar
1.1358 -\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.1359 -\rail@plus
1.1360 -\rail@nont{\isa{cons}}[]
1.1361 -\rail@nextplus{1}
1.1362 -\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.1363 -\rail@endplus
1.1364 -\rail@end
1.1365 -\rail@begin{2}{\isa{cons}}
1.1366 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1367 -\rail@plus
1.1368 -\rail@nextplus{1}
1.1369 -\rail@cnont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
1.1370 -\rail@endplus
1.1371 -\rail@bar
1.1372 -\rail@nextbar{1}
1.1373 -\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.1374 -\rail@endbar
1.1375 -\rail@end
1.1376 -\end{railoutput}
1.1377 -
1.1378 -
1.1379 - \begin{description}
1.1380 -
1.1381 - \item \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} defines inductive datatypes in
1.1382 - HOL.
1.1383 -
1.1384 - \item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}} represents existing types as
1.1385 - inductive ones, generating the standard infrastructure of derived
1.1386 - concepts (primitive recursion etc.).
1.1387 -
1.1388 - \end{description}
1.1389 -
1.1390 - The induction and exhaustion theorems generated provide case names
1.1391 - according to the constructors involved, while parameters are named
1.1392 - after the types (see also \secref{sec:cases-induct}).
1.1393 -
1.1394 - See \cite{isabelle-HOL} for more details on datatypes, but beware of
1.1395 - the old-style theory syntax being used there! Apart from proper
1.1396 - proof methods for case-analysis and induction, there are also
1.1397 - 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.1398 - to refer directly to the internal structure of subgoals (including
1.1399 - internally bound parameters).%
1.1400 -\end{isamarkuptext}%
1.1401 -\isamarkuptrue%
1.1402 -%
1.1403 \isamarkupsection{Functorial structure of types%
1.1404 }
1.1405 \isamarkuptrue%
1.1406 @@ -680,641 +1315,6 @@
1.1407 \end{isamarkuptext}%
1.1408 \isamarkuptrue%
1.1409 %
1.1410 -\isamarkupsection{Recursive functions \label{sec:recursion}%
1.1411 -}
1.1412 -\isamarkuptrue%
1.1413 -%
1.1414 -\begin{isamarkuptext}%
1.1415 -\begin{matharray}{rcl}
1.1416 - \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.1417 - \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.1418 - \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.1419 - \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.1420 - \end{matharray}
1.1421 -
1.1422 - \begin{railoutput}
1.1423 -\rail@begin{2}{}
1.1424 -\rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
1.1425 -\rail@bar
1.1426 -\rail@nextbar{1}
1.1427 -\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.1428 -\rail@endbar
1.1429 -\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.1430 -\rail@term{\isa{\isakeyword{where}}}[]
1.1431 -\rail@nont{\isa{equations}}[]
1.1432 -\rail@end
1.1433 -\rail@begin{4}{}
1.1434 -\rail@bar
1.1435 -\rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
1.1436 -\rail@nextbar{1}
1.1437 -\rail@term{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}}[]
1.1438 -\rail@endbar
1.1439 -\rail@bar
1.1440 -\rail@nextbar{1}
1.1441 -\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.1442 -\rail@endbar
1.1443 -\rail@bar
1.1444 -\rail@nextbar{1}
1.1445 -\rail@nont{\isa{functionopts}}[]
1.1446 -\rail@endbar
1.1447 -\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.1448 -\rail@cr{3}
1.1449 -\rail@term{\isa{\isakeyword{where}}}[]
1.1450 -\rail@nont{\isa{equations}}[]
1.1451 -\rail@end
1.1452 -\rail@begin{3}{\isa{equations}}
1.1453 -\rail@plus
1.1454 -\rail@bar
1.1455 -\rail@nextbar{1}
1.1456 -\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.1457 -\rail@endbar
1.1458 -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.1459 -\rail@nextplus{2}
1.1460 -\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.1461 -\rail@endplus
1.1462 -\rail@end
1.1463 -\rail@begin{3}{\isa{functionopts}}
1.1464 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1465 -\rail@plus
1.1466 -\rail@bar
1.1467 -\rail@term{\isa{sequential}}[]
1.1468 -\rail@nextbar{1}
1.1469 -\rail@term{\isa{domintros}}[]
1.1470 -\rail@endbar
1.1471 -\rail@nextplus{2}
1.1472 -\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
1.1473 -\rail@endplus
1.1474 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1475 -\rail@end
1.1476 -\rail@begin{2}{}
1.1477 -\rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
1.1478 -\rail@bar
1.1479 -\rail@nextbar{1}
1.1480 -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1481 -\rail@endbar
1.1482 -\rail@end
1.1483 -\end{railoutput}
1.1484 -
1.1485 -
1.1486 - \begin{description}
1.1487 -
1.1488 - \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
1.1489 - functions over datatypes, see also \cite{isabelle-HOL}.
1.1490 -
1.1491 - \item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
1.1492 - wellfounded recursion. A detailed description with examples can be
1.1493 - found in \cite{isabelle-function}. The function is specified by a
1.1494 - set of (possibly conditional) recursive equations with arbitrary
1.1495 - pattern matching. The command generates proof obligations for the
1.1496 - completeness and the compatibility of patterns.
1.1497 -
1.1498 - The defined function is considered partial, and the resulting
1.1499 - simplification rules (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}psimps{\isaliteral{22}{\isachardoublequote}}}) and induction rule
1.1500 - (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}pinduct{\isaliteral{22}{\isachardoublequote}}}) are guarded by a generated domain
1.1501 - predicate \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5F}{\isacharunderscore}}dom{\isaliteral{22}{\isachardoublequote}}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}
1.1502 - command can then be used to establish that the function is total.
1.1503 -
1.1504 - \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.1505 - proof attempts regarding pattern matching and termination. See
1.1506 - \cite{isabelle-function} for further details.
1.1507 -
1.1508 - \item \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f} commences a
1.1509 - termination proof for the previously defined function \isa{f}. If
1.1510 - this is omitted, the command refers to the most recent function
1.1511 - definition. After the proof is closed, the recursive equations and
1.1512 - the induction principle is established.
1.1513 -
1.1514 - \end{description}
1.1515 -
1.1516 - Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
1.1517 - command accommodate
1.1518 - 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.1519 - refers to a specific induction rule, with parameters named according
1.1520 - to the user-specified equations. Cases are numbered (starting from 1).
1.1521 -
1.1522 - For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
1.1523 - with structural recursion on the datatype the recursion is carried
1.1524 - out.
1.1525 -
1.1526 - The equations provided by these packages may be referred later as
1.1527 - theorem list \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, where \isa{f} is the (collective)
1.1528 - name of the functions defined. Individual equations may be named
1.1529 - explicitly as well.
1.1530 -
1.1531 - The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following
1.1532 - options.
1.1533 -
1.1534 - \begin{description}
1.1535 -
1.1536 - \item \isa{sequential} enables a preprocessor which disambiguates
1.1537 - overlapping patterns by making them mutually disjoint. Earlier
1.1538 - equations take precedence over later ones. This allows to give the
1.1539 - specification in a format very similar to functional programming.
1.1540 - Note that the resulting simplification and induction rules
1.1541 - correspond to the transformed specification, not the one given
1.1542 - originally. This usually means that each equation given by the user
1.1543 - may result in several theorems. Also note that this automatic
1.1544 - transformation only works for ML-style datatype patterns.
1.1545 -
1.1546 - \item \isa{domintros} enables the automated generation of
1.1547 - introduction rules for the domain predicate. While mostly not
1.1548 - needed, they can be helpful in some proofs about partial functions.
1.1549 -
1.1550 - \end{description}%
1.1551 -\end{isamarkuptext}%
1.1552 -\isamarkuptrue%
1.1553 -%
1.1554 -\isamarkupsubsection{Proof methods related to recursive definitions%
1.1555 -}
1.1556 -\isamarkuptrue%
1.1557 -%
1.1558 -\begin{isamarkuptext}%
1.1559 -\begin{matharray}{rcl}
1.1560 - \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.1561 - \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
1.1562 - \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.1563 - \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.1564 - \end{matharray}
1.1565 -
1.1566 - \begin{railoutput}
1.1567 -\rail@begin{1}{}
1.1568 -\rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
1.1569 -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1570 -\rail@end
1.1571 -\rail@begin{2}{}
1.1572 -\rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
1.1573 -\rail@plus
1.1574 -\rail@nextplus{1}
1.1575 -\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.1576 -\rail@endplus
1.1577 -\rail@end
1.1578 -\rail@begin{2}{}
1.1579 -\rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
1.1580 -\rail@nont{\isa{orders}}[]
1.1581 -\rail@plus
1.1582 -\rail@nextplus{1}
1.1583 -\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.1584 -\rail@endplus
1.1585 -\rail@end
1.1586 -\rail@begin{4}{\isa{orders}}
1.1587 -\rail@plus
1.1588 -\rail@nextplus{1}
1.1589 -\rail@bar
1.1590 -\rail@term{\isa{max}}[]
1.1591 -\rail@nextbar{2}
1.1592 -\rail@term{\isa{min}}[]
1.1593 -\rail@nextbar{3}
1.1594 -\rail@term{\isa{ms}}[]
1.1595 -\rail@endbar
1.1596 -\rail@endplus
1.1597 -\rail@end
1.1598 -\end{railoutput}
1.1599 -
1.1600 -
1.1601 - \begin{description}
1.1602 -
1.1603 - \item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}} is a specialized method to
1.1604 - solve goals regarding the completeness of pattern matching, as
1.1605 - required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
1.1606 - \cite{isabelle-function}).
1.1607 -
1.1608 - \item \hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R} introduces a termination
1.1609 - proof using the relation \isa{R}. The resulting proof state will
1.1610 - contain goals expressing that \isa{R} is wellfounded, and that the
1.1611 - arguments of recursive calls decrease with respect to \isa{R}.
1.1612 - Usually, this method is used as the initial proof step of manual
1.1613 - termination proofs.
1.1614 -
1.1615 - \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}} attempts a fully
1.1616 - automated termination proof by searching for a lexicographic
1.1617 - combination of size measures on the arguments of the function. The
1.1618 - method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
1.1619 - which it uses internally to prove local descents. The same context
1.1620 - modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see
1.1621 - \secref{sec:clasimp}.
1.1622 -
1.1623 - In case of failure, extensive information is printed, which can help
1.1624 - to analyse the situation (cf.\ \cite{isabelle-function}).
1.1625 -
1.1626 - \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}} also works on termination goals,
1.1627 - using a variation of the size-change principle, together with a
1.1628 - graph decomposition technique (see \cite{krauss_phd} for details).
1.1629 - Three kinds of orders are used internally: \isa{max}, \isa{min},
1.1630 - and \isa{ms} (multiset), which is only available when the theory
1.1631 - \isa{Multiset} is loaded. When no order kinds are given, they are
1.1632 - tried in order. The search for a termination proof uses SAT solving
1.1633 - internally.
1.1634 -
1.1635 - For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
1.1636 -
1.1637 - \end{description}%
1.1638 -\end{isamarkuptext}%
1.1639 -\isamarkuptrue%
1.1640 -%
1.1641 -\isamarkupsubsection{Functions with explicit partiality%
1.1642 -}
1.1643 -\isamarkuptrue%
1.1644 -%
1.1645 -\begin{isamarkuptext}%
1.1646 -\begin{matharray}{rcl}
1.1647 - \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.1648 - \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.1649 - \end{matharray}
1.1650 -
1.1651 - \begin{railoutput}
1.1652 -\rail@begin{5}{}
1.1653 -\rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
1.1654 -\rail@bar
1.1655 -\rail@nextbar{1}
1.1656 -\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.1657 -\rail@endbar
1.1658 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1659 -\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.1660 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1661 -\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.1662 -\rail@cr{3}
1.1663 -\rail@term{\isa{\isakeyword{where}}}[]
1.1664 -\rail@bar
1.1665 -\rail@nextbar{4}
1.1666 -\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.1667 -\rail@endbar
1.1668 -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.1669 -\rail@end
1.1670 -\end{railoutput}
1.1671 -
1.1672 -
1.1673 - \begin{description}
1.1674 -
1.1675 - \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.1676 - recursive functions based on fixpoints in complete partial
1.1677 - orders. No termination proof is required from the user or
1.1678 - constructed internally. Instead, the possibility of non-termination
1.1679 - is modelled explicitly in the result type, which contains an
1.1680 - explicit bottom element.
1.1681 -
1.1682 - Pattern matching and mutual recursion are currently not supported.
1.1683 - Thus, the specification consists of a single function described by a
1.1684 - single recursive equation.
1.1685 -
1.1686 - There are no fixed syntactic restrictions on the body of the
1.1687 - function, but the induced functional must be provably monotonic
1.1688 - wrt.\ the underlying order. The monotonicitity proof is performed
1.1689 - internally, and the definition is rejected when it fails. The proof
1.1690 - can be influenced by declaring hints using the
1.1691 - \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} attribute.
1.1692 -
1.1693 - The mandatory \isa{mode} argument specifies the mode of operation
1.1694 - of the command, which directly corresponds to a complete partial
1.1695 - order on the result type. By default, the following modes are
1.1696 - defined:
1.1697 -
1.1698 - \begin{description}
1.1699 - \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
1.1700 - non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
1.1701 - must also be \isa{None}. This is best achieved through the use of
1.1702 - the monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}.
1.1703 -
1.1704 - \item \isa{tailrec} defines functions with an arbitrary result
1.1705 - 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.1706 - if \isa{undefined} is returned by a recursive call, then the
1.1707 - overall result must also be \isa{undefined}. In practice, this is
1.1708 - only satisfied when each recursive call is a tail call, whose result
1.1709 - is directly returned. Thus, this mode of operation allows the
1.1710 - definition of arbitrary tail-recursive functions.
1.1711 - \end{description}
1.1712 -
1.1713 - Experienced users may define new modes by instantiating the locale
1.1714 - \isa{{\isaliteral{22}{\isachardoublequote}}partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}definitions{\isaliteral{22}{\isachardoublequote}}} appropriately.
1.1715 -
1.1716 - \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} declares rules for
1.1717 - use in the internal monononicity proofs of partial function
1.1718 - definitions.
1.1719 -
1.1720 - \end{description}%
1.1721 -\end{isamarkuptext}%
1.1722 -\isamarkuptrue%
1.1723 -%
1.1724 -\isamarkupsubsection{Old-style recursive function definitions (TFL)%
1.1725 -}
1.1726 -\isamarkuptrue%
1.1727 -%
1.1728 -\begin{isamarkuptext}%
1.1729 -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.1730 -
1.1731 - \begin{matharray}{rcl}
1.1732 - \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.1733 - \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.1734 - \end{matharray}
1.1735 -
1.1736 - \begin{railoutput}
1.1737 -\rail@begin{5}{}
1.1738 -\rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
1.1739 -\rail@bar
1.1740 -\rail@nextbar{1}
1.1741 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1742 -\rail@term{\isa{\isakeyword{permissive}}}[]
1.1743 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1744 -\rail@endbar
1.1745 -\rail@cr{3}
1.1746 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.1747 -\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.1748 -\rail@plus
1.1749 -\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.1750 -\rail@nextplus{4}
1.1751 -\rail@endplus
1.1752 -\rail@bar
1.1753 -\rail@nextbar{4}
1.1754 -\rail@nont{\isa{hints}}[]
1.1755 -\rail@endbar
1.1756 -\rail@end
1.1757 -\rail@begin{2}{}
1.1758 -\rail@nont{\isa{recdeftc}}[]
1.1759 -\rail@bar
1.1760 -\rail@nextbar{1}
1.1761 -\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.1762 -\rail@endbar
1.1763 -\rail@nont{\isa{tc}}[]
1.1764 -\rail@end
1.1765 -\rail@begin{2}{\isa{hints}}
1.1766 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1767 -\rail@term{\isa{\isakeyword{hints}}}[]
1.1768 -\rail@plus
1.1769 -\rail@nextplus{1}
1.1770 -\rail@cnont{\isa{recdefmod}}[]
1.1771 -\rail@endplus
1.1772 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1773 -\rail@end
1.1774 -\rail@begin{4}{\isa{recdefmod}}
1.1775 -\rail@bar
1.1776 -\rail@bar
1.1777 -\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}[]
1.1778 -\rail@nextbar{1}
1.1779 -\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}[]
1.1780 -\rail@nextbar{2}
1.1781 -\rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}[]
1.1782 -\rail@endbar
1.1783 -\rail@bar
1.1784 -\rail@nextbar{1}
1.1785 -\rail@term{\isa{add}}[]
1.1786 -\rail@nextbar{2}
1.1787 -\rail@term{\isa{del}}[]
1.1788 -\rail@endbar
1.1789 -\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.1790 -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.1791 -\rail@nextbar{3}
1.1792 -\rail@nont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
1.1793 -\rail@endbar
1.1794 -\rail@end
1.1795 -\rail@begin{2}{\isa{tc}}
1.1796 -\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1.1797 -\rail@bar
1.1798 -\rail@nextbar{1}
1.1799 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.1800 -\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1.1801 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.1802 -\rail@endbar
1.1803 -\rail@end
1.1804 -\end{railoutput}
1.1805 -
1.1806 -
1.1807 - \begin{description}
1.1808 -
1.1809 - \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
1.1810 - recursive functions (using the TFL package), see also
1.1811 - \cite{isabelle-HOL}. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells
1.1812 - TFL to recover from failed proof attempts, returning unfinished
1.1813 - 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.1814 - automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}
1.1815 - declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
1.1816 - context of the Simplifier (cf.\ \secref{sec:simplifier}) and
1.1817 - Classical reasoner (cf.\ \secref{sec:classical}).
1.1818 -
1.1819 - \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.1820 - proof for leftover termination condition number \isa{i} (default
1.1821 - 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
1.1822 - constant \isa{c}.
1.1823 -
1.1824 - Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
1.1825 - its internal proofs without manual intervention.
1.1826 -
1.1827 - \end{description}
1.1828 -
1.1829 - \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared
1.1830 - globally, using the following attributes.
1.1831 -
1.1832 - \begin{matharray}{rcl}
1.1833 - \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.1834 - \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.1835 - \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.1836 - \end{matharray}
1.1837 -
1.1838 - \begin{railoutput}
1.1839 -\rail@begin{3}{}
1.1840 -\rail@bar
1.1841 -\rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
1.1842 -\rail@nextbar{1}
1.1843 -\rail@term{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}}[]
1.1844 -\rail@nextbar{2}
1.1845 -\rail@term{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}}[]
1.1846 -\rail@endbar
1.1847 -\rail@bar
1.1848 -\rail@nextbar{1}
1.1849 -\rail@term{\isa{add}}[]
1.1850 -\rail@nextbar{2}
1.1851 -\rail@term{\isa{del}}[]
1.1852 -\rail@endbar
1.1853 -\rail@end
1.1854 -\end{railoutput}%
1.1855 -\end{isamarkuptext}%
1.1856 -\isamarkuptrue%
1.1857 -%
1.1858 -\isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
1.1859 -}
1.1860 -\isamarkuptrue%
1.1861 -%
1.1862 -\begin{isamarkuptext}%
1.1863 -An \textbf{inductive definition} specifies the least predicate (or
1.1864 - set) \isa{R} closed under given rules: applying a rule to elements
1.1865 - of \isa{R} yields a result within \isa{R}. For example, a
1.1866 - structural operational semantics is an inductive definition of an
1.1867 - evaluation relation.
1.1868 -
1.1869 - Dually, a \textbf{coinductive definition} specifies the greatest
1.1870 - predicate~/ set \isa{R} that is consistent with given rules: every
1.1871 - element of \isa{R} can be seen as arising by applying a rule to
1.1872 - elements of \isa{R}. An important example is using bisimulation
1.1873 - relations to formalise equivalence of processes and infinite data
1.1874 - structures.
1.1875 -
1.1876 - \medskip The HOL package is related to the ZF one, which is
1.1877 - described in a separate paper,\footnote{It appeared in CADE
1.1878 - \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
1.1879 - which you should refer to in case of difficulties. The package is
1.1880 - simpler than that of ZF thanks to implicit type-checking in HOL.
1.1881 - The types of the (co)inductive predicates (or sets) determine the
1.1882 - domain of the fixedpoint definition, and the package does not have
1.1883 - to use inference rules for type-checking.
1.1884 -
1.1885 - \begin{matharray}{rcl}
1.1886 - \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.1887 - \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.1888 - \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.1889 - \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.1890 - \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
1.1891 - \end{matharray}
1.1892 -
1.1893 - \begin{railoutput}
1.1894 -\rail@begin{7}{}
1.1895 -\rail@bar
1.1896 -\rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
1.1897 -\rail@nextbar{1}
1.1898 -\rail@term{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1.1899 -\rail@nextbar{2}
1.1900 -\rail@term{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]
1.1901 -\rail@nextbar{3}
1.1902 -\rail@term{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1.1903 -\rail@endbar
1.1904 -\rail@bar
1.1905 -\rail@nextbar{1}
1.1906 -\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1.1907 -\rail@endbar
1.1908 -\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.1909 -\rail@bar
1.1910 -\rail@nextbar{1}
1.1911 -\rail@term{\isa{\isakeyword{for}}}[]
1.1912 -\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1.1913 -\rail@endbar
1.1914 -\rail@cr{5}
1.1915 -\rail@bar
1.1916 -\rail@nextbar{6}
1.1917 -\rail@term{\isa{\isakeyword{where}}}[]
1.1918 -\rail@nont{\isa{clauses}}[]
1.1919 -\rail@endbar
1.1920 -\rail@bar
1.1921 -\rail@nextbar{6}
1.1922 -\rail@term{\isa{\isakeyword{monos}}}[]
1.1923 -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.1924 -\rail@endbar
1.1925 -\rail@end
1.1926 -\rail@begin{3}{\isa{clauses}}
1.1927 -\rail@plus
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{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1.1933 -\rail@nextplus{2}
1.1934 -\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1.1935 -\rail@endplus
1.1936 -\rail@end
1.1937 -\rail@begin{3}{}
1.1938 -\rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
1.1939 -\rail@bar
1.1940 -\rail@nextbar{1}
1.1941 -\rail@term{\isa{add}}[]
1.1942 -\rail@nextbar{2}
1.1943 -\rail@term{\isa{del}}[]
1.1944 -\rail@endbar
1.1945 -\rail@end
1.1946 -\end{railoutput}
1.1947 -
1.1948 -
1.1949 - \begin{description}
1.1950 -
1.1951 - \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.1952 - introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part. The
1.1953 - optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the
1.1954 - (co)inductive predicates that remain fixed throughout the
1.1955 - definition. The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains
1.1956 - \emph{monotonicity theorems}, which are required for each operator
1.1957 - applied to a recursive set in the introduction rules. There
1.1958 - \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.1959 - for each premise \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}} in an introduction rule!
1.1960 -
1.1961 - \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.1962 - allowing the definition of (co)inductive sets.
1.1963 -
1.1964 - \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules. These
1.1965 - rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}.
1.1966 -
1.1967 - \end{description}%
1.1968 -\end{isamarkuptext}%
1.1969 -\isamarkuptrue%
1.1970 -%
1.1971 -\isamarkupsubsection{Derived rules%
1.1972 -}
1.1973 -\isamarkuptrue%
1.1974 -%
1.1975 -\begin{isamarkuptext}%
1.1976 -Each (co)inductive definition \isa{R} adds definitions to the
1.1977 - theory and also proves some theorems:
1.1978 -
1.1979 - \begin{description}
1.1980 -
1.1981 - \item \isa{R{\isaliteral{2E}{\isachardot}}intros} is the list of introduction rules as proven
1.1982 - theorems, for the recursive predicates (or sets). The rules are
1.1983 - also available individually, using the names given them in the
1.1984 - theory file;
1.1985 -
1.1986 - \item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
1.1987 -
1.1988 - \item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
1.1989 - rule.
1.1990 -
1.1991 - \end{description}
1.1992 -
1.1993 - 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.1994 - defined simultaneously, the list of introduction rules is called
1.1995 - \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.1996 - 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.1997 - 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.1998 -\end{isamarkuptext}%
1.1999 -\isamarkuptrue%
1.2000 -%
1.2001 -\isamarkupsubsection{Monotonicity theorems%
1.2002 -}
1.2003 -\isamarkuptrue%
1.2004 -%
1.2005 -\begin{isamarkuptext}%
1.2006 -Each theory contains a default set of theorems that are used in
1.2007 - monotonicity proofs. New rules can be added to this set via the
1.2008 - \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute. The HOL theory \isa{Inductive}
1.2009 - shows how this is done. In general, the following monotonicity
1.2010 - theorems may be added:
1.2011 -
1.2012 - \begin{itemize}
1.2013 -
1.2014 - \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.2015 - monotonicity of inductive definitions whose introduction rules have
1.2016 - premises involving terms such as \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}}.
1.2017 -
1.2018 - \item Monotonicity theorems for logical operators, which are of the
1.2019 - 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.2020 - the case of the operator \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, the corresponding theorem is
1.2021 - \[
1.2022 - \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.2023 - \]
1.2024 -
1.2025 - \item De Morgan style equations for reasoning about the ``polarity''
1.2026 - of expressions, e.g.
1.2027 - \[
1.2028 - \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ P{\isaliteral{22}{\isachardoublequote}}} \qquad\qquad
1.2029 - \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.2030 - \]
1.2031 -
1.2032 - \item Equations for reducing complex operators to more primitive
1.2033 - ones whose monotonicity can easily be proved, e.g.
1.2034 - \[
1.2035 - \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.2036 - \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.2037 - \]
1.2038 -
1.2039 - \end{itemize}
1.2040 -
1.2041 - %FIXME: Example of an inductive definition%
1.2042 -\end{isamarkuptext}%
1.2043 -\isamarkuptrue%
1.2044 -%
1.2045 \isamarkupsection{Arithmetic proof support%
1.2046 }
1.2047 \isamarkuptrue%