8 Church's original paper~\cite{church40}. Andrews's |
8 Church's original paper~\cite{church40}. Andrews's |
9 book~\cite{andrews86} is a full description of the original |
9 book~\cite{andrews86} is a full description of the original |
10 Church-style higher-order logic. Experience with the {\sc hol} system |
10 Church-style higher-order logic. Experience with the {\sc hol} system |
11 has demonstrated that higher-order logic is widely applicable in many |
11 has demonstrated that higher-order logic is widely applicable in many |
12 areas of mathematics and computer science, not just hardware |
12 areas of mathematics and computer science, not just hardware |
13 verification, {\sc hol}'s original {\it raison d'\^etre\/}. It is |
13 verification, {\sc hol}'s original \textit{raison d'\^etre\/}. It is |
14 weaker than {\ZF} set theory but for most applications this does not |
14 weaker than {\ZF} set theory but for most applications this does not |
15 matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\ |
15 matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\ |
16 to~{\ZF}. |
16 to~{\ZF}. |
17 |
17 |
18 The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a |
18 The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a |
19 different syntax. Ancient releases of Isabelle included still another version |
19 different syntax. Ancient releases of Isabelle included still another version |
20 of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This |
20 of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This |
21 version no longer exists, but \thydx{ZF} supports a similar style of |
21 version no longer exists, but \thydx{ZF} supports a similar style of |
22 reasoning.} follows $\lambda$-calculus and functional programming. Function |
22 reasoning.} follows $\lambda$-calculus and functional programming. Function |
23 application is curried. To apply the function~$f$ of type |
23 application is curried. To apply the function~$f$ of type |
24 $\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply |
24 $\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply |
25 write $f\,a\,b$. There is no `apply' operator as in \thydx{ZF}. Note that |
25 write $f\,a\,b$. There is no `apply' operator as in \thydx{ZF}. Note that |
26 $f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL. We write ordered |
26 $f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL. We write ordered |
27 pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}. |
27 pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}. |
28 |
28 |
29 \HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It |
29 \HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It |
30 identifies object-level types with meta-level types, taking advantage of |
30 identifies object-level types with meta-level types, taking advantage of |
171 particular, {\tt-} is instantiated for set difference and subtraction |
171 particular, {\tt-} is instantiated for set difference and subtraction |
172 on natural numbers. |
172 on natural numbers. |
173 |
173 |
174 If you state a goal containing overloaded functions, you may need to include |
174 If you state a goal containing overloaded functions, you may need to include |
175 type constraints. Type inference may otherwise make the goal more |
175 type constraints. Type inference may otherwise make the goal more |
176 polymorphic than you intended, with confusing results. For example, the |
176 polymorphic than you intended, with confusing results. For example, the |
177 variables $i$, $j$ and $k$ in the goal $i \le j \Imp i \le j+k$ have type |
177 variables $i$, $j$ and $k$ in the goal $i \le j \Imp i \le j+k$ have type |
178 $\alpha::\{ord,plus\}$, although you may have expected them to have some |
178 $\alpha::\{ord,plus\}$, although you may have expected them to have some |
179 numeric type, e.g. $nat$. Instead you should have stated the goal as |
179 numeric type, e.g. $nat$. Instead you should have stated the goal as |
180 $(i::nat) \le j \Imp i \le j+k$, which causes all three variables to have |
180 $(i::nat) \le j \Imp i \le j+k$, which causes all three variables to have |
181 type $nat$. |
181 type $nat$. |
182 |
182 |
183 \begin{warn} |
183 \begin{warn} |
184 If resolution fails for no obvious reason, try setting |
184 If resolution fails for no obvious reason, try setting |
185 \ttindex{show_types} to {\tt true}, causing Isabelle to display |
185 \ttindex{show_types} to \texttt{true}, causing Isabelle to display |
186 types of terms. Possibly set \ttindex{show_sorts} to {\tt true} as |
186 types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as |
187 well, causing Isabelle to display type classes and sorts. |
187 well, causing Isabelle to display type classes and sorts. |
188 |
188 |
189 \index{unification!incompleteness of} |
189 \index{unification!incompleteness of} |
190 Where function types are involved, Isabelle's unification code does not |
190 Where function types are involved, Isabelle's unification code does not |
191 guarantee to find instantiations for type variables automatically. Be |
191 guarantee to find instantiations for type variables automatically. Be |
192 prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac}, |
192 prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac}, |
193 possibly instantiating type variables. Setting |
193 possibly instantiating type variables. Setting |
194 \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to report |
194 \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report |
195 omitted search paths during unification.\index{tracing!of unification} |
195 omitted search paths during unification.\index{tracing!of unification} |
196 \end{warn} |
196 \end{warn} |
197 |
197 |
198 |
198 |
199 \subsection{Binders} |
199 \subsection{Binders} |
220 unknown, while \verb'? x.f x=y' is a quantification. Isabelle's usual |
220 unknown, while \verb'? x.f x=y' is a quantification. Isabelle's usual |
221 notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also |
221 notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also |
222 available. Both notations are accepted for input. The {\ML} reference |
222 available. Both notations are accepted for input. The {\ML} reference |
223 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt |
223 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt |
224 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set |
224 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set |
225 to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed. |
225 to \texttt{false}, then~{\tt ALL} and~{\tt EX} are displayed. |
226 |
226 |
227 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a |
227 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a |
228 variable of type $\tau$, then the term \cdx{LEAST}~$x.P[x]$ is defined |
228 variable of type $\tau$, then the term \cdx{LEAST}~$x.P[x]$ is defined |
229 to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see |
229 to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see |
230 Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$ |
230 Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$ |
231 choice operator, so \texttt{Least} is always meaningful, but may yield |
231 choice operator, so \texttt{Least} is always meaningful, but may yield |
232 nothing useful in case there is not a unique least element satisfying |
232 nothing useful in case there is not a unique least element satisfying |
233 $P$.\footnote{Class $ord$ does not require much of its instances, so |
233 $P$.\footnote{Class $ord$ does not require much of its instances, so |
234 $\le$ need not be a well-ordering, not even an order at all!} |
234 $\le$ need not be a well-ordering, not even an order at all!} |
235 |
235 |
236 \medskip All these binders have priority 10. |
236 \medskip All these binders have priority 10. |
237 |
237 |
238 \begin{warn} |
238 \begin{warn} |
239 The low priority of binders means that they need to be enclosed in |
239 The low priority of binders means that they need to be enclosed in |
240 parenthesis when they occur in the context of other operations. For example, |
240 parenthesis when they occur in the context of other operations. For example, |
241 instead of $P \land \forall x.Q$ you need to write $P \land (\forall x.Q)$. |
241 instead of $P \land \forall x.Q$ you need to write $P \land (\forall x.Q)$. |
242 \end{warn} |
242 \end{warn} |
243 |
243 |
244 |
244 |
245 \subsection{The \sdx{let} and \sdx{case} constructions} |
245 \subsection{The \sdx{let} and \sdx{case} constructions} |
246 Local abbreviations can be introduced by a {\tt let} construct whose |
246 Local abbreviations can be introduced by a \texttt{let} construct whose |
247 syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into |
247 syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into |
248 the constant~\cdx{Let}. It can be expanded by rewriting with its |
248 the constant~\cdx{Let}. It can be expanded by rewriting with its |
249 definition, \tdx{Let_def}. |
249 definition, \tdx{Let_def}. |
250 |
250 |
251 \HOL\ also defines the basic syntax |
251 \HOL\ also defines the basic syntax |
252 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] |
252 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] |
253 as a uniform means of expressing {\tt case} constructs. Therefore {\tt case} |
253 as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case} |
254 and \sdx{of} are reserved words. Initially, this is mere syntax and has no |
254 and \sdx{of} are reserved words. Initially, this is mere syntax and has no |
255 logical meaning. By declaring translations, you can cause instances of the |
255 logical meaning. By declaring translations, you can cause instances of the |
256 {\tt case} construct to denote applications of particular case operators. |
256 {\tt case} construct to denote applications of particular case operators. |
257 This is what happens automatically for each {\tt datatype} definition |
257 This is what happens automatically for each \texttt{datatype} definition |
258 (see~\S\ref{sec:HOL:datatype}). |
258 (see~\S\ref{sec:HOL:datatype}). |
259 |
259 |
260 \begin{warn} |
260 \begin{warn} |
261 Both {\tt if} and {\tt case} constructs have as low a priority as |
261 Both \texttt{if} and \texttt{case} constructs have as low a priority as |
262 quantifiers, which requires additional enclosing parentheses in the context |
262 quantifiers, which requires additional enclosing parentheses in the context |
263 of most other operations. For example, instead of $f~x = if \dots then \dots |
263 of most other operations. For example, instead of $f~x = if \dots then \dots |
264 else \dots$ you need to write $f~x = (if \dots then \dots else |
264 else \dots$ you need to write $f~x = (if \dots then \dots else |
265 \dots)$. |
265 \dots)$. |
266 \end{warn} |
266 \end{warn} |
267 |
267 |
268 \section{Rules of inference} |
268 \section{Rules of inference} |
888 \end{figure} |
888 \end{figure} |
889 |
889 |
890 \subsection{Properties of functions}\nopagebreak |
890 \subsection{Properties of functions}\nopagebreak |
891 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions. |
891 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions. |
892 Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse |
892 Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse |
893 of~$f$. See the file {\tt HOL/Fun.ML} for a complete listing of the derived |
893 of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived |
894 rules. Reasoning about function composition (the operator~\sdx{o}) and the |
894 rules. Reasoning about function composition (the operator~\sdx{o}) and the |
895 predicate~\cdx{surj} is done simply by expanding the definitions. |
895 predicate~\cdx{surj} is done simply by expanding the definitions. |
896 |
896 |
897 There is also a large collection of monotonicity theorems for constructions |
897 There is also a large collection of monotonicity theorems for constructions |
898 on sets in the file {\tt HOL/mono.ML}. |
898 on sets in the file \texttt{HOL/mono.ML}. |
899 |
899 |
900 \section{Generic packages} |
900 \section{Generic packages} |
901 \label{sec:HOL:generic-packages} |
901 \label{sec:HOL:generic-packages} |
902 |
902 |
903 \HOL\ instantiates most of Isabelle's generic packages, making available the |
903 \HOL\ instantiates most of Isabelle's generic packages, making available the |
904 simplifier and the classical reasoner. |
904 simplifier and the classical reasoner. |
905 |
905 |
906 \subsection{Simplification and substitution} |
906 \subsection{Simplification and substitution} |
907 |
907 |
908 The simplifier is available in \HOL. Tactics such as {\tt |
908 The simplifier is available in \HOL. Tactics such as {\tt |
909 Asm_simp_tac} and {\tt Full_simp_tac} use the default simpset |
909 Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset |
910 ({\tt!simpset}), which works for most purposes. A quite minimal |
910 ({\tt!simpset}), which works for most purposes. A quite minimal |
911 simplification set for higher-order logic is~\ttindexbold{HOL_ss}, |
911 simplification set for higher-order logic is~\ttindexbold{HOL_ss}, |
912 even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which |
912 even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which |
913 also expresses logical equivalence, may be used for rewriting. See |
913 also expresses logical equivalence, may be used for rewriting. See |
914 the file {\tt HOL/simpdata.ML} for a complete listing of the basic |
914 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic |
915 simplification rules. |
915 simplification rules. |
916 |
916 |
917 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% |
917 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% |
918 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution |
918 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution |
919 and simplification. |
919 and simplification. |
947 |
947 |
948 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as |
948 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as |
949 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap |
949 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap |
950 rule; recall Fig.\ts\ref{hol-lemmas2} above. |
950 rule; recall Fig.\ts\ref{hol-lemmas2} above. |
951 |
951 |
952 The classical reasoner is installed. Tactics such as {\tt Blast_tac} and {\tt |
952 The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt |
953 Best_tac} use the default claset ({\tt!claset}), which works for most |
953 Best_tac} use the default claset ({\tt!claset}), which works for most |
954 purposes. Named clasets include \ttindexbold{prop_cs}, which includes the |
954 purposes. Named clasets include \ttindexbold{prop_cs}, which includes the |
955 propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier |
955 propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier |
956 rules. See the file {\tt HOL/cladata.ML} for lists of the classical rules, |
956 rules. See the file \texttt{HOL/cladata.ML} for lists of the classical rules, |
957 and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% |
957 and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% |
958 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods. |
958 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods. |
959 |
959 |
960 |
960 |
961 \section{Types}\label{sec:HOL:Types} |
961 \section{Types}\label{sec:HOL:Types} |
962 This section describes \HOL's basic predefined types ($\alpha \times |
962 This section describes \HOL's basic predefined types ($\alpha \times |
963 \beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for |
963 \beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for |
964 introducing new types in general. The most important type |
964 introducing new types in general. The most important type |
965 construction, the {\tt datatype}, is treated separately in |
965 construction, the \texttt{datatype}, is treated separately in |
966 \S\ref{sec:HOL:datatype}. |
966 \S\ref{sec:HOL:datatype}. |
967 |
967 |
968 |
968 |
969 \subsection{Product and sum types}\index{*"* type}\index{*"+ type} |
969 \subsection{Product and sum types}\index{*"* type}\index{*"+ type} |
970 \label{subsec:prod-sum} |
970 \label{subsec:prod-sum} |
1020 \end{tabular} |
1020 \end{tabular} |
1021 \end{center} |
1021 \end{center} |
1022 In addition, it is possible to use tuples |
1022 In addition, it is possible to use tuples |
1023 as patterns in abstractions: |
1023 as patterns in abstractions: |
1024 \begin{center} |
1024 \begin{center} |
1025 {\tt\%($x$,$y$).$t$} \quad stands for\quad {\tt split(\%$x$\thinspace$y$.$t$)} |
1025 {\tt\%($x$,$y$).$t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.$t$)} |
1026 \end{center} |
1026 \end{center} |
1027 Nested patterns are also supported. They are translated stepwise: |
1027 Nested patterns are also supported. They are translated stepwise: |
1028 {\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$ |
1028 {\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$ |
1029 {\tt split(\%$x$.\%($y$,$z$).$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$ |
1029 {\tt split(\%$x$.\%($y$,$z$).$t$)} $\leadsto$ \texttt{split(\%$x$.split(\%$y$ |
1030 $z$.$t$))}. The reverse translation is performed upon printing. |
1030 $z$.$t$))}. The reverse translation is performed upon printing. |
1031 \begin{warn} |
1031 \begin{warn} |
1032 The translation between patterns and {\tt split} is performed automatically |
1032 The translation between patterns and \texttt{split} is performed automatically |
1033 by the parser and printer. Thus the internal and external form of a term |
1033 by the parser and printer. Thus the internal and external form of a term |
1034 may differ, which can affects proofs. For example the term {\tt |
1034 may differ, which can affects proofs. For example the term {\tt |
1035 (\%(x,y).(y,x))(a,b)} requires the theorem {\tt split} (which is in the |
1035 (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the |
1036 default simpset) to rewrite to {\tt(b,a)}. |
1036 default simpset) to rewrite to {\tt(b,a)}. |
1037 \end{warn} |
1037 \end{warn} |
1038 In addition to explicit $\lambda$-abstractions, patterns can be used in any |
1038 In addition to explicit $\lambda$-abstractions, patterns can be used in any |
1039 variable binding construct which is internally described by a |
1039 variable binding construct which is internally described by a |
1040 $\lambda$-abstraction. Some important examples are |
1040 $\lambda$-abstraction. Some important examples are |
1041 \begin{description} |
1041 \begin{description} |
1042 \item[Let:] {\tt let {\it pattern} = $t$ in $u$} |
1042 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$} |
1043 \item[Quantifiers:] {\tt !~{\it pattern}:$A$.~$P$} |
1043 \item[Quantifiers:] \texttt{!~{\it pattern}:$A$.~$P$} |
1044 \item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$} |
1044 \item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$} |
1045 \item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$} |
1045 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} |
1046 \item[Sets:] {\tt {\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}} |
1046 \item[Sets:] \texttt{{\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}} |
1047 \end{description} |
1047 \end{description} |
1048 |
1048 |
1049 There is a simple tactic which supports reasoning about patterns: |
1049 There is a simple tactic which supports reasoning about patterns: |
1050 \begin{ttdescription} |
1050 \begin{ttdescription} |
1051 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all |
1051 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all |
1052 {\tt!!}-quantified variables of product type by individual variables for |
1052 {\tt!!}-quantified variables of product type by individual variables for |
1053 each component. A simple example: |
1053 each component. A simple example: |
1054 \begin{ttbox} |
1054 \begin{ttbox} |
1055 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p} |
1055 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p} |
1056 by(split_all_tac 1); |
1056 by(split_all_tac 1); |
1057 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)} |
1057 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)} |
1058 \end{ttbox} |
1058 \end{ttbox} |
1059 \end{ttdescription} |
1059 \end{ttdescription} |
1060 |
1060 |
1061 Theory {\tt Prod} also introduces the degenerate product type {\tt unit} |
1061 Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit} |
1062 which contains only a single element named {\tt()} with the property |
1062 which contains only a single element named {\tt()} with the property |
1063 \begin{ttbox} |
1063 \begin{ttbox} |
1064 \tdx{unit_eq} u = () |
1064 \tdx{unit_eq} u = () |
1065 \end{ttbox} |
1065 \end{ttbox} |
1066 \bigskip |
1066 \bigskip |
1130 \tdx{Suc_not_Zero} Suc m ~= 0 |
1130 \tdx{Suc_not_Zero} Suc m ~= 0 |
1131 \tdx{inj_Suc} inj Suc |
1131 \tdx{inj_Suc} inj Suc |
1132 \tdx{n_not_Suc_n} n~=Suc n |
1132 \tdx{n_not_Suc_n} n~=Suc n |
1133 \subcaption{Basic properties} |
1133 \subcaption{Basic properties} |
1134 \end{ttbox} |
1134 \end{ttbox} |
1135 \caption{The type of natural numbers, {\tt nat}} \label{hol-nat1} |
1135 \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1} |
1136 \end{figure} |
1136 \end{figure} |
1137 |
1137 |
1138 |
1138 |
1139 \begin{figure} |
1139 \begin{figure} |
1140 \begin{ttbox}\makeatother |
1140 \begin{ttbox}\makeatother |
1141 %\tdx{nat_case_0} nat_case a f 0 = a |
|
1142 %\tdx{nat_case_Suc} nat_case a f (Suc k) = f k |
|
1143 % |
|
1144 %\tdx{nat_rec_0} nat_rec 0 c h = c |
|
1145 %\tdx{nat_rec_Suc} nat_rec (Suc n) c h = h n (nat_rec n c h) |
|
1146 % |
|
1147 0+n = n |
1141 0+n = n |
1148 (Suc m)+n = Suc(m+n) |
1142 (Suc m)+n = Suc(m+n) |
|
1143 |
1149 m-0 = m |
1144 m-0 = m |
1150 0-n = n |
1145 0-n = n |
1151 Suc(m)-Suc(n) = m-n |
1146 Suc(m)-Suc(n) = m-n |
|
1147 |
1152 0*n = 0 |
1148 0*n = 0 |
1153 Suc(m)*n = n + m*n |
1149 Suc(m)*n = n + m*n |
1154 |
1150 |
1155 \tdx{mod_less} m<n ==> m mod n = m |
1151 \tdx{mod_less} m<n ==> m mod n = m |
1156 \tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n |
1152 \tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n |
|
1153 |
1157 \tdx{div_less} m<n ==> m div n = 0 |
1154 \tdx{div_less} m<n ==> m div n = 0 |
1158 \tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n) |
1155 \tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n) |
1159 %\subcaption{Recursion equations} |
1156 \end{ttbox} |
1160 % |
1157 \caption{Recursion equations for the arithmetic operators} \label{hol-nat2} |
1161 %\tdx{less_trans} [| i<j; j<k |] ==> i<k |
|
1162 %\tdx{lessI} n < Suc n |
|
1163 %\tdx{zero_less_Suc} 0 < Suc n |
|
1164 % |
|
1165 %\tdx{less_not_sym} n<m --> ~ m<n |
|
1166 %\tdx{less_not_refl} ~ n<n |
|
1167 %\tdx{not_less0} ~ n<0 |
|
1168 % |
|
1169 %\tdx{Suc_less_eq} (Suc m < Suc n) = (m<n) |
|
1170 %\tdx{less_induct} [| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n |
|
1171 % |
|
1172 %\tdx{less_linear} m<n | m=n | n<m |
|
1173 %\subcaption{The less-than relation} |
|
1174 \end{ttbox} |
|
1175 \caption{Recursion equations for {\tt nat}} \label{hol-nat2} |
|
1176 \end{figure} |
1158 \end{figure} |
1177 |
1159 |
1178 \subsection{The type of natural numbers, {\tt nat}} |
1160 \subsection{The type of natural numbers, \textit{nat}} |
1179 |
1161 \index{nat@{\textit{nat}} type|(} |
1180 The theory \thydx{NatDef} defines the natural numbers in a roundabout |
1162 |
1181 but traditional way. The axiom of infinity postulates a |
1163 The theory \thydx{NatDef} defines the natural numbers in a roundabout but |
1182 type~\tydx{ind} of individuals, which is non-empty and closed under an |
1164 traditional way. The axiom of infinity postulates a type~\tydx{ind} of |
1183 injective operation. The natural numbers are inductively generated by |
1165 individuals, which is non-empty and closed under an injective operation. The |
1184 choosing an arbitrary individual for~0 and using the injective |
1166 natural numbers are inductively generated by choosing an arbitrary individual |
1185 operation to take successors. For details see the file |
1167 for~0 and using the injective operation to take successors. This is a least |
1186 \texttt{NatDef.thy}. |
1168 fixedpoint construction. For details see the file \texttt{NatDef.thy}. |
1187 |
|
1188 %The definition makes use of a least fixed point operator \cdx{lfp}, |
|
1189 %defined using the Knaster-Tarski theorem. This is used to define the |
|
1190 %operator \cdx{trancl}, for taking the transitive closure of a relation. |
|
1191 %Primitive recursion makes use of \cdx{wfrec}, an operator for recursion |
|
1192 %along arbitrary well-founded relations. The corresponding theories are |
|
1193 %called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described |
|
1194 %similar constructions in the context of set theory~\cite{paulson-set-II}. |
|
1195 |
1169 |
1196 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the |
1170 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the |
1197 overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also |
1171 overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also |
1198 \cdx{min}, \cdx{max} and \cdx{LEAST}) available on {\tt nat}. Theory |
1172 \cdx{min}, \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory |
1199 \thydx{Nat} builds on {\tt NatDef} and shows that {\tt<=} is a partial order, |
1173 \thydx{Nat} builds on \texttt{NatDef} and shows that {\tt<=} is a partial order, |
1200 i.e.\ {\tt nat} is even an instance of class {\tt order}. |
1174 so \tydx{nat} is also an instance of class \cldx{order}. |
1201 |
1175 |
1202 Theory \thydx{Arith} develops arithmetic on the natural numbers. It |
1176 Theory \thydx{Arith} develops arithmetic on the natural numbers. It defines |
1203 defines addition, multiplication, subtraction, division, and remainder. |
1177 addition, multiplication and subtraction. Theory \thydx{Divides} defines |
1204 Many of their properties are proved: commutative, associative and |
1178 division, remainder and the ``divides'' relation. The numerous theorems |
1205 distributive laws, identity and cancellation laws, etc. |
1179 proved include commutative, associative, distributive, identity and |
1206 % The most |
1180 cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The |
1207 %interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$. |
1181 recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on |
1208 Division and remainder are defined by repeated subtraction, which |
1182 \texttt{nat} are part of the default simpset. |
1209 requires well-founded rather than primitive recursion. See |
1183 |
1210 Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The recursion equations for |
1184 Functions on \tydx{nat} can be defined by primitive or well-founded recursion; |
1211 the operators {\tt +}, {\tt -} and {\tt *} on \texttt{nat} are part of |
1185 see \S\ref{sec:HOL:recursive}. A simple example is addition. |
1212 the default simpset. |
1186 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following |
1213 |
1187 the standard convention. |
1214 Functions on {\tt nat} can be defined by primitive recursion, for example |
|
1215 addition: |
|
1216 \begin{ttbox} |
1188 \begin{ttbox} |
1217 \sdx{primrec} "op +" nat |
1189 \sdx{primrec} "op +" nat |
1218 "0 + n = n" |
1190 " 0 + n = n" |
1219 "Suc m + n = Suc(m + n)" |
1191 "Suc m + n = Suc(m + n)" |
1220 \end{ttbox} |
1192 \end{ttbox} |
1221 Remember that the name of infix operators usually has an {\tt op} |
1193 There is also a \sdx{case}-construct |
1222 prefixed. The general format for defining primitive recursive |
1194 of the form |
1223 functions on {\tt nat} follows the rules for primitive recursive |
|
1224 functions on datatypes (see~\S\ref{sec:HOL:primrec}). There is also a |
|
1225 \sdx{case}-construct of the form |
|
1226 \begin{ttbox} |
1195 \begin{ttbox} |
1227 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\) |
1196 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\) |
1228 \end{ttbox} |
1197 \end{ttbox} |
1229 Note that Isabelle insists on precisely this format; you may not even change |
1198 Note that Isabelle insists on precisely this format; you may not even change |
1230 the order of the two cases. |
1199 the order of the two cases. |
1231 Both {\tt primrec} and {\tt case} are realized by a recursion operator |
1200 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator |
1232 \cdx{nat_rec}, the details of which can be found in theory {\tt NatDef}. |
1201 \cdx{nat_rec}, the details of which can be found in theory \texttt{NatDef}. |
1233 |
1202 |
1234 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded. |
1203 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded. |
1235 %Recursion along this relation resembles primitive recursion, but is |
1204 %Recursion along this relation resembles primitive recursion, but is |
1236 %stronger because we are in higher-order logic; using primitive recursion to |
1205 %stronger because we are in higher-order logic; using primitive recursion to |
1237 %define a higher-order function, we can easily Ackermann's function, which |
1206 %define a higher-order function, we can easily Ackermann's function, which |
1238 %is not primitive recursive \cite[page~104]{thompson91}. |
1207 %is not primitive recursive \cite[page~104]{thompson91}. |
1239 %The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the |
1208 %The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the |
1240 %natural numbers are most easily expressed using recursion along~$<$. |
1209 %natural numbers are most easily expressed using recursion along~$<$. |
1241 |
1210 |
1242 Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$ |
1211 Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$ |
1243 in subgoal~$i$ using theorem {\tt nat_induct}. There is also the derived |
1212 in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived |
1244 theorem \tdx{less_induct}: |
1213 theorem \tdx{less_induct}: |
1245 \begin{ttbox} |
1214 \begin{ttbox} |
1246 [| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n |
1215 [| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n |
1247 \end{ttbox} |
1216 \end{ttbox} |
1248 |
1217 |
1249 |
1218 |
1250 Reasoning about arithmetic inequalities can be tedious. A minimal amount of |
1219 Reasoning about arithmetic inequalities can be tedious. A minimal amount of |
1251 automation is provided by the tactic \ttindex{trans_tac} of type {\tt int -> |
1220 automation is provided by the tactic \ttindex{trans_tac} of type \texttt{int -> |
1252 tactic} that deals with simple inequalities. Note that it only knows about |
1221 tactic} that deals with simple inequalities. Note that it only knows about |
1253 {\tt 0}, {\tt Suc}, {\tt<} and {\tt<=}. The following goals are all solved by |
1222 {\tt 0}, \texttt{Suc}, {\tt<} and {\tt<=}. The following goals are all solved by |
1254 {\tt trans_tac 1}: |
1223 {\tt trans_tac 1}: |
1255 \begin{ttbox} |
1224 \begin{ttbox} |
1256 {\out 1. \dots ==> m <= Suc(Suc m)} |
1225 {\out 1. \dots ==> m <= Suc(Suc m)} |
1257 {\out 1. [| \dots i <= j \dots Suc j <= k \dots |] ==> i < k} |
1226 {\out 1. [| \dots i <= j \dots Suc j <= k \dots |] ==> i < k} |
1258 {\out 1. [| \dots Suc m <= n \dots ~ m < n \dots |] ==> \dots} |
1227 {\out 1. [| \dots Suc m <= n \dots ~ m < n \dots |] ==> \dots} |
1259 \end{ttbox} |
1228 \end{ttbox} |
1260 For a complete description of the limitations of the tactic and how to avoid |
1229 For a complete description of the limitations of the tactic and how to avoid |
1261 some of them, see the comments at the start of the file {\tt |
1230 some of them, see the comments at the start of the file {\tt |
1262 Provers/nat_transitive.ML}. |
1231 Provers/nat_transitive.ML}. |
1263 |
1232 |
1264 If {\tt trans_tac} fails you, try to find relevant arithmetic results in the |
1233 If \texttt{trans_tac} fails you, try to find relevant arithmetic results in |
1265 library. The theory {\tt NatDef} contains theorems about {\tt<} and {\tt<=}, |
1234 the library. The theory \texttt{NatDef} contains theorems about {\tt<} and |
1266 the theory {\tt Arith} contains theorems about {\tt +}, {\tt -}, {\tt *}, |
1235 {\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+}, |
1267 {\tt div} and {\tt mod}. Since specific results may be hard to find, we |
1236 \texttt{-} and \texttt{*}, and theory \texttt{Divides} contains theorems about |
1268 recommend the {\tt find}-functions (see the {\em Reference Manual\/}). |
1237 \texttt{div} and \texttt{mod}. Use the \texttt{find}-functions to locate them |
|
1238 (see the {\em Reference Manual\/}). |
1269 |
1239 |
1270 \begin{figure} |
1240 \begin{figure} |
1271 \index{#@{\tt[]} symbol} |
1241 \index{#@{\tt[]} symbol} |
1272 \index{#@{\tt\#} symbol} |
1242 \index{#@{\tt\#} symbol} |
1273 \index{"@@{\tt\at} symbol} |
1243 \index{"@@{\tt\at} symbol} |
1367 dropWhile P (x#xs) = (if P x then dropWhile P xs else xs) |
1337 dropWhile P (x#xs) = (if P x then dropWhile P xs else xs) |
1368 \end{ttbox} |
1338 \end{ttbox} |
1369 \caption{Recursions equations for list processing functions} |
1339 \caption{Recursions equations for list processing functions} |
1370 \label{fig:HOL:list-simps} |
1340 \label{fig:HOL:list-simps} |
1371 \end{figure} |
1341 \end{figure} |
1372 |
1342 \index{nat@{\textit{nat}} type|)} |
1373 |
1343 |
1374 \subsection{The type constructor for lists, {\tt list}} |
1344 |
1375 \index{*list type} |
1345 \subsection{The type constructor for lists, \textit{list}} |
|
1346 \index{list@{\textit{list}} type|(} |
1376 |
1347 |
1377 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list |
1348 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list |
1378 operations with their types and syntax. Type $\alpha \; list$ is |
1349 operations with their types and syntax. Type $\alpha \; list$ is |
1379 defined as a {\tt datatype} with the constructors {\tt[]} and {\tt\#}. |
1350 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}. |
1380 As a result the generic structural induction and case analysis tactics |
1351 As a result the generic structural induction and case analysis tactics |
1381 \texttt{induct\_tac} and \texttt{exhaust\_tac} also become available for |
1352 \texttt{induct\_tac} and \texttt{exhaust\_tac} also become available for |
1382 lists. A \sdx{case} construct of the form |
1353 lists. A \sdx{case} construct of the form |
1383 \begin{center}\tt |
1354 \begin{center}\tt |
1384 case $e$ of [] => $a$ | \(x\)\#\(xs\) => b |
1355 case $e$ of [] => $a$ | \(x\)\#\(xs\) => b |
1385 \end{center} |
1356 \end{center} |
1386 is defined by translation. For details see~\S\ref{sec:HOL:datatype}. |
1357 is defined by translation. For details see~\S\ref{sec:HOL:datatype}. |
1387 |
1358 |
1388 {\tt List} provides a basic library of list processing functions defined by |
1359 {\tt List} provides a basic library of list processing functions defined by |
1389 primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations |
1360 primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations |
1390 are shown in Fig.\ts\ref{fig:HOL:list-simps}. |
1361 are shown in Fig.\ts\ref{fig:HOL:list-simps}. |
1391 |
1362 |
|
1363 \index{list@{\textit{list}} type|)} |
|
1364 |
1392 |
1365 |
1393 \subsection{Introducing new types} \label{sec:typedef} |
1366 \subsection{Introducing new types} \label{sec:typedef} |
1394 |
1367 |
1395 The \HOL-methodology dictates that all extensions to a theory should |
1368 The \HOL-methodology dictates that all extensions to a theory should |
1396 be \textbf{definitional}. The basic type definition mechanism which |
1369 be \textbf{definitional}. The type definition mechanism that |
1397 meets this criterion --- w.r.t.\ the standard model theory of |
1370 meets this criterion is \ttindex{typedef}. Note that \emph{type synonyms}, |
1398 \textsc{hol} --- is \ttindex{typedef}. Note that \emph{type synonyms}, |
|
1399 which are inherited from {\Pure} and described elsewhere, are just |
1371 which are inherited from {\Pure} and described elsewhere, are just |
1400 syntactic abbreviations that have no logical meaning. |
1372 syntactic abbreviations that have no logical meaning. |
1401 |
1373 |
1402 \begin{warn} |
1374 \begin{warn} |
1403 Types in \HOL\ must be non-empty; otherwise the quantifier rules would be |
1375 Types in \HOL\ must be non-empty; otherwise the quantifier rules would be |
1404 unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}. |
1376 unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}. |
1405 \end{warn} |
1377 \end{warn} |
1406 A \bfindex{type definition} identifies the new type with a subset of |
1378 A \bfindex{type definition} identifies the new type with a subset of |
1407 an existing type. More precisely, the new type is defined by |
1379 an existing type. More precisely, the new type is defined by |
1408 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a |
1380 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a |
1409 theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$, |
1381 theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$, |
1410 and the new type denotes this subset. New functions are defined that |
1382 and the new type denotes this subset. New functions are defined that |
1411 establish an isomorphism between the new type and the subset. If |
1383 establish an isomorphism between the new type and the subset. If |
1412 type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$, |
1384 type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$, |
1422 \end{rail} |
1394 \end{rail} |
1423 \caption{Syntax of type definitions} |
1395 \caption{Syntax of type definitions} |
1424 \label{fig:HOL:typedef} |
1396 \label{fig:HOL:typedef} |
1425 \end{figure} |
1397 \end{figure} |
1426 |
1398 |
1427 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For |
1399 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For |
1428 the definition of `typevarlist' and `infix' see |
1400 the definition of `typevarlist' and `infix' see |
1429 \iflabelundefined{chap:classical} |
1401 \iflabelundefined{chap:classical} |
1430 {the appendix of the {\em Reference Manual\/}}% |
1402 {the appendix of the {\em Reference Manual\/}}% |
1431 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the |
1403 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the |
1432 following meaning: |
1404 following meaning: |
1433 \begin{description} |
1405 \begin{description} |
1434 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with |
1406 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with |
1435 optional infix annotation. |
1407 optional infix annotation. |
1436 \item[\it name:] an alphanumeric name $T$ for the type constructor |
1408 \item[\it name:] an alphanumeric name $T$ for the type constructor |
1437 $ty$, in case $ty$ is a symbolic name. Defaults to $ty$. |
1409 $ty$, in case $ty$ is a symbolic name. Defaults to $ty$. |
1438 \item[\it set:] the representing subset $A$. |
1410 \item[\it set:] the representing subset $A$. |
1439 \item[\it witness:] name of a theorem of the form $a:A$ proving |
1411 \item[\it witness:] name of a theorem of the form $a:A$ proving |
1440 non-emptiness. It can be omitted in case Isabelle manages to prove |
1412 non-emptiness. It can be omitted in case Isabelle manages to prove |
1441 non-emptiness automatically. |
1413 non-emptiness automatically. |
1442 \end{description} |
1414 \end{description} |
1443 If all context conditions are met (no duplicate type variables in |
1415 If all context conditions are met (no duplicate type variables in |
1444 `typevarlist', no extra type variables in `set', and no free term variables |
1416 `typevarlist', no extra type variables in `set', and no free term variables |
1445 in `set'), the following components are added to the theory: |
1417 in `set'), the following components are added to the theory: |
1645 \label{datatype-grammar} |
1617 \label{datatype-grammar} |
1646 \end{figure} |
1618 \end{figure} |
1647 |
1619 |
1648 \begin{warn} |
1620 \begin{warn} |
1649 Every theory containing a datatype declaration must be based, directly or |
1621 Every theory containing a datatype declaration must be based, directly or |
1650 indirectly, on the theory {\tt Arith}, if necessary by including it |
1622 indirectly, on the theory \texttt{Arith}, if necessary by including it |
1651 explicitly as a parent. |
1623 explicitly as a parent. |
1652 \end{warn} |
1624 \end{warn} |
1653 |
1625 |
1654 Most of the theorems about the datatype become part of the default simpset |
1626 Most of the theorems about the datatype become part of the default simpset |
1655 and you never need to see them again because the simplifier applies them |
1627 and you never need to see them again because the simplifier applies them |
1656 automatically. Only induction is invoked by hand: |
1628 automatically. Only induction is invoked by hand: |
1657 \begin{ttdescription} |
1629 \begin{ttdescription} |
1658 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] |
1630 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] |
1659 applies structural induction on variable $x$ to subgoal $i$, provided the |
1631 applies structural induction on variable $x$ to subgoal $i$, provided the |
1660 type of $x$ is a datatype or type {\tt nat}. |
1632 type of $x$ is a datatype or type \tydx{nat}. |
1661 \end{ttdescription} |
1633 \end{ttdescription} |
1662 In some cases, induction is overkill and a case distinction over all |
1634 In some cases, induction is overkill and a case distinction over all |
1663 constructors of the datatype suffices: |
1635 constructors of the datatype suffices: |
1664 \begin{ttdescription} |
1636 \begin{ttdescription} |
1665 \item[\ttindexbold{exhaust_tac} {\tt"}$u${\tt"} $i$] |
1637 \item[\ttindexbold{exhaust_tac} {\tt"}$u${\tt"} $i$] |
1666 performs an exhaustive case analysis for the term $u$ whose type |
1638 performs an exhaustive case analysis for the term $u$ whose type |
1667 must be a datatyp or type {\tt nat}. If the datatype has $n$ constructors |
1639 must be a datatype or type \tydx{nat}. If the datatype has $n$ constructors |
1668 $C@1$, \dots $C@n$, subgoal $i$ is replaced by $n$ new subgoals which |
1640 $C@1$, \dots $C@n$, subgoal $i$ is replaced by $n$ new subgoals which |
1669 contain the additional assumption $u = C@j~x@1~\dots~x@{k@j}$ for |
1641 contain the additional assumption $u = C@j~x@1~\dots~x@{k@j}$ for |
1670 $j=1,\dots,n$. |
1642 $j=1$, $\dots$,~$n$. |
1671 \end{ttdescription} |
1643 \end{ttdescription} |
1672 \begin{warn} |
1644 \begin{warn} |
1673 Induction is only allowed on a free variable that should not occur among |
1645 Induction is only allowed on a free variable that should not occur among |
1674 the premises of the subgoal. Exhaustion is works for arbitrary terms. |
1646 the premises of the subgoal. Exhaustion is works for arbitrary terms. |
1675 \end{warn} |
1647 \end{warn} |
1676 \bigskip |
1648 \bigskip |
1677 |
1649 |
1678 |
1650 |
1679 For the technically minded, we give a more detailed description. |
1651 For the technically minded, we give a more detailed description. |
1680 Reading the theory file produces an \ML\ structure which, in addition to the |
1652 Reading the theory file produces an \ML\ structure which, in addition to the |
1681 usual components, contains a structure named $t$ for each datatype $t$ |
1653 usual components, contains a structure named $t$ for each datatype $t$ |
1682 defined in the file. Each structure $t$ contains the following |
1654 defined in the file. Each structure $t$ contains the following |
1683 elements: |
1655 elements: |
1684 \begin{ttbox} |
1656 \begin{ttbox} |
1685 val distinct : thm list |
1657 val distinct : thm list |
1686 val inject : thm list |
1658 val inject : thm list |
1687 val induct : thm |
1659 val induct : thm |
1688 val cases : thm list |
1660 val cases : thm list |
1689 val simps : thm list |
1661 val simps : thm list |
1690 val induct_tac : string -> int -> tactic |
1662 val induct_tac : string -> int -> tactic |
1691 \end{ttbox} |
1663 \end{ttbox} |
1692 {\tt distinct}, {\tt inject} and {\tt induct} contain the theorems |
1664 {\tt distinct}, \texttt{inject} and \texttt{induct} contain the theorems |
1693 described above. For user convenience, {\tt distinct} contains |
1665 described above. For user convenience, \texttt{distinct} contains |
1694 inequalities in both directions. The reduction rules of the {\tt |
1666 inequalities in both directions. The reduction rules of the {\tt |
1695 case}-construct are in {\tt cases}. All theorems from {\tt |
1667 case}-construct are in \texttt{cases}. All theorems from {\tt |
1696 distinct}, {\tt inject} and {\tt cases} are combined in {\tt simps}. |
1668 distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}. |
1697 |
1669 |
1698 \subsection{Examples} |
1670 \subsection{Examples} |
1699 |
1671 |
1700 \subsubsection{The datatype $\alpha~mylist$} |
1672 \subsubsection{The datatype $\alpha~mylist$} |
1701 |
1673 |
1702 We want to define the type $\alpha~mylist$.\footnote{This is just an |
1674 We want to define the type $\alpha~mylist$.\footnote{This is just an |
1703 example, there is already a list type in \HOL, of course.} To do |
1675 example, there is already a list type in \HOL, of course.} To do |
1704 this we have to build a new theory that contains the type definition. |
1676 this we have to build a new theory that contains the type definition. |
1705 We start from the basic {\tt HOL} theory. |
1677 We start from the basic \texttt{HOL} theory. |
1706 \begin{ttbox} |
1678 \begin{ttbox} |
1707 MyList = HOL + |
1679 MyList = HOL + |
1708 datatype 'a mylist = Nil | Cons 'a ('a mylist) |
1680 datatype 'a mylist = Nil | Cons 'a ('a mylist) |
1709 end |
1681 end |
1710 \end{ttbox} |
1682 \end{ttbox} |
1711 After loading the theory (with \verb$use_thy "MyList"$), we can prove |
1683 After loading the theory (with \verb$use_thy "MyList"$), we can prove |
1712 $Cons~x~xs\neq xs$. To ease the induction applied below, we state the |
1684 $Cons~x~xs\neq xs$. To ease the induction applied below, we state the |
1713 goal with $x$ quantified at the object-level. This will be stripped |
1685 goal with $x$ quantified at the object-level. This will be stripped |
1714 later using \ttindex{qed_spec_mp}. |
1686 later using \ttindex{qed_spec_mp}. |
1715 \begin{ttbox} |
1687 \begin{ttbox} |
1716 goal MyList.thy "!x. Cons x xs ~= xs"; |
1688 goal MyList.thy "!x. Cons x xs ~= xs"; |
1717 {\out Level 0} |
1689 {\out Level 0} |
1718 {\out ! x. Cons x xs ~= xs} |
1690 {\out ! x. Cons x xs ~= xs} |
1780 Days = Arith + |
1752 Days = Arith + |
1781 datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun |
1753 datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun |
1782 end |
1754 end |
1783 \end{ttbox} |
1755 \end{ttbox} |
1784 Because there are more than 6 constructors, the theory must be based |
1756 Because there are more than 6 constructors, the theory must be based |
1785 on {\tt Arith}. Inequality is expressed via a function |
1757 on \texttt{Arith}. Inequality is expressed via a function |
1786 \verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly |
1758 \verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly |
1787 contained among the distinctness theorems, but the simplifier can |
1759 contained among the distinctness theorems, but the simplifier can |
1788 prove it thanks to rewrite rules inherited from theory {\tt Arith}: |
1760 prove it thanks to rewrite rules inherited from theory \texttt{Arith}: |
1789 \begin{ttbox} |
1761 \begin{ttbox} |
1790 goal Days.thy "Mon ~= Tue"; |
1762 goal Days.thy "Mon ~= Tue"; |
1791 by (Simp_tac 1); |
1763 by (Simp_tac 1); |
1792 \end{ttbox} |
1764 \end{ttbox} |
1793 You need not derive such inequalities explicitly: the simplifier will dispose |
1765 You need not derive such inequalities explicitly: the simplifier will dispose |
1794 of them automatically. |
1766 of them automatically. |
|
1767 \index{*datatype|)} |
|
1768 |
|
1769 |
|
1770 \section{Recursive function definitions}\label{sec:HOL:recursive} |
|
1771 \index{recursive functions|see{recursion}} |
|
1772 |
|
1773 Isabelle/HOL provides two means of declaring recursive functions. |
|
1774 \begin{itemize} |
|
1775 \item \textbf{Primitive recursion} is available only for datatypes, and it is |
|
1776 highly restrictive. Recursive calls are only allowed on the argument's |
|
1777 immediate constituents. On the other hand, it is the form of recursion most |
|
1778 often wanted, and it is easy to use. |
|
1779 |
|
1780 \item \textbf{Well-founded recursion} requires that you supply a well-founded |
|
1781 relation that governs the recursion. Recursive calls are only allowed if |
|
1782 they make the argument decrease under the relation. Complicated recursion |
|
1783 forms, such as nested recursion, can be dealt with. Termination can even be |
|
1784 proved at a later time, though having unsolved termination conditions around |
|
1785 can make work difficult.% |
|
1786 \footnote{This facility is based on Konrad Slind's TFL |
|
1787 package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL |
|
1788 and assisting with its installation.} |
|
1789 \end{itemize} |
|
1790 |
|
1791 |
|
1792 A theory file may contain any number of recursive function definitions, which |
|
1793 may be intermixed with other declarations. Every recursive function must |
|
1794 already have been declared as a constant. |
|
1795 |
|
1796 These declarations do not assert new axioms. Instead, they define the |
|
1797 function using a recursion operator. Both HOL and ZF derive the theory of |
|
1798 well-founded recursion from first principles~\cite{paulson-set-II}. Primitive |
|
1799 recursion over some datatype relies on the recursion operator provided by the |
|
1800 datatype package. With either form of function definition, Isabelle proves |
|
1801 the desired recursion equations as theorems. |
1795 |
1802 |
1796 |
1803 |
1797 \subsection{Primitive recursive functions} |
1804 \subsection{Primitive recursive functions} |
1798 \label{sec:HOL:primrec} |
1805 \label{sec:HOL:primrec} |
1799 \index{primitive recursion|(} |
1806 \index{recursion!primitive|(} |
1800 \index{*primrec|(} |
1807 \index{*primrec|(} |
1801 |
1808 |
1802 Datatypes come with a uniform way of defining functions, {\bf |
1809 Datatypes come with a uniform way of defining functions, {\bf |
1803 primitive recursion}. In principle it would be possible to define |
1810 primitive recursion}. In principle, one can define |
1804 primitive recursive functions by asserting their reduction rules as |
1811 primitive recursive functions by asserting their reduction rules as |
1805 new axioms, e.g.\ |
1812 new axioms. Here is an example: |
1806 \begin{ttbox} |
1813 \begin{ttbox} |
1807 Append = MyList + |
1814 Append = MyList + |
1808 consts app :: ['a mylist, 'a mylist] => 'a mylist |
1815 consts app :: ['a mylist, 'a mylist] => 'a mylist |
1809 rules |
1816 rules |
1810 app_Nil "app [] ys = ys" |
1817 app_Nil "app [] ys = ys" |
1811 app_Cons "app (x#xs) ys = x#app xs ys" |
1818 app_Cons "app (x#xs) ys = x#app xs ys" |
1812 end |
1819 end |
1813 \end{ttbox} |
1820 \end{ttbox} |
1814 This carries with it the danger of accidentally asserting an |
1821 But asserting axioms brings the danger of accidentally asserting an |
1815 inconsistency, as in \verb$app [] ys = us$, though. |
1822 inconsistency, as in \verb$app [] ys = us$. |
1816 |
1823 |
1817 \HOL\ provides a save mechanism to define primitive recursive |
1824 The \ttindex{primrec} declaration is a safe means of defining primitive |
1818 functions on datatypes --- \ttindex{primrec}: |
1825 recursive functions on datatypes: |
1819 \begin{ttbox} |
1826 \begin{ttbox} |
1820 Append = MyList + |
1827 Append = MyList + |
1821 consts app :: ['a mylist, 'a mylist] => 'a mylist |
1828 consts app :: ['a mylist, 'a mylist] => 'a mylist |
1822 primrec app MyList.mylist |
1829 primrec app MyList.mylist |
1823 "app [] ys = ys" |
1830 "app [] ys = ys" |
1824 "app (x#xs) ys = x#app xs ys" |
1831 "app (x#xs) ys = x#app xs ys" |
1825 end |
1832 end |
1826 \end{ttbox} |
1833 \end{ttbox} |
1827 Isabelle will now check that the two rules do indeed form a primitive |
1834 Isabelle will now check that the two rules do indeed form a primitive |
1828 recursive definition, thus ensuring that consistency is maintained. For |
1835 recursive definition, preserving consistency. For example |
1829 example |
|
1830 \begin{ttbox} |
1836 \begin{ttbox} |
1831 primrec app MyList.mylist |
1837 primrec app MyList.mylist |
1832 "app [] ys = us" |
1838 "app [] ys = us" |
1833 \end{ttbox} |
1839 \end{ttbox} |
1834 is rejected with an error message \texttt{Extra variables on rhs}. |
1840 is rejected with an error message \texttt{Extra variables on rhs}. |
1840 primrec {\it function} {\it type} |
1846 primrec {\it function} {\it type} |
1841 {\it reduction rules} |
1847 {\it reduction rules} |
1842 \end{ttbox} |
1848 \end{ttbox} |
1843 where |
1849 where |
1844 \begin{itemize} |
1850 \begin{itemize} |
1845 \item {\it function} is the name of the function, either as an {\it id} or a |
1851 \item \textit{function} is the name of the function, either as an \textit{id} |
1846 {\it string}. The function must already have been declared as a constant. |
1852 or a \textit{string}. |
1847 \item {\it type} is the name of the datatype, either as an {\it id} or |
1853 \item \textit{type} is the name of the datatype, either as an \textit{id} or |
1848 in the long form \texttt{$T$.$t$} ($T$ is the name of the theory |
1854 in the long form \texttt{$T$.$t$} ($T$ is the name of the theory |
1849 where the datatype has been declared, $t$ the name of the datatype). |
1855 where the datatype has been declared, $t$ the name of the datatype). |
1850 The long form is required if the {\tt datatype} and the {\tt |
1856 The long form is required if the \texttt{datatype} and the {\tt |
1851 primrec} sections are in different theories. |
1857 primrec} sections are in different theories. |
1852 \item {\it reduction rules} specify one or more equations of the form |
1858 \item \textit{reduction rules} specify one or more equations of the form |
1853 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \, |
1859 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \, |
1854 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, |
1860 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, |
1855 $r$ contains only the free variables on the left-hand side, and all |
1861 $r$ contains only the free variables on the left-hand side, and all |
1856 recursive calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ |
1862 recursive calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ |
1857 for some $i$. There must be exactly one reduction rule for each |
1863 for some $i$. There must be exactly one reduction rule for each |
1858 constructor. The order is immaterial. Also note that all reduction |
1864 constructor. The order is immaterial. Also note that all reduction |
1859 rules are added to the default simpset! |
1865 rules are added to the default simpset! |
1860 |
1866 |
1861 If you would like to refer to some rule explicitly, you have to prefix |
1867 If you would like to refer to some rule by name, then you must prefix |
1862 each rule with an identifier (like in the {\tt rules} section of the |
1868 \emph{each} rule with an identifier. These identifiers, like those in the |
1863 axiomatic {\tt Append} theory above) that will serve as the name of |
1869 \texttt{rules} section of a theory, will be visible at the \ML\ level. |
1864 the corresponding theorem at the \ML\ level. |
|
1865 \end{itemize} |
1870 \end{itemize} |
1866 A theory file may contain any number of {\tt primrec} sections which may be |
|
1867 intermixed with other declarations. |
|
1868 |
1871 |
1869 The primitive recursive function can have infix or mixfix syntax: |
1872 The primitive recursive function can have infix or mixfix syntax: |
1870 \begin{ttbox}\underscoreon |
1873 \begin{ttbox}\underscoreon |
1871 Append = MyList + |
1874 Append = MyList + |
1872 consts "@" :: ['a mylist, 'a mylist] => 'a mylist (infixr 60) |
1875 consts "@" :: ['a mylist, 'a mylist] => 'a mylist (infixr 60) |
1882 goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)"; |
1885 goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)"; |
1883 by (induct\_tac "xs" 1); |
1886 by (induct\_tac "xs" 1); |
1884 by (ALLGOALS Asm\_simp\_tac); |
1887 by (ALLGOALS Asm\_simp\_tac); |
1885 \end{ttbox} |
1888 \end{ttbox} |
1886 |
1889 |
1887 %Note that underdefined primitive recursive functions are allowed: |
1890 \index{recursion!primitive|)} |
1888 %\begin{ttbox} |
|
1889 %Tl = MyList + |
|
1890 %consts tl :: 'a mylist => 'a mylist |
|
1891 %primrec tl MyList.mylist |
|
1892 % tl_Cons "tl(x#xs) = xs" |
|
1893 %end |
|
1894 %\end{ttbox} |
|
1895 %Nevertheless {\tt tl} is total, although we do not know what the result of |
|
1896 %\verb$tl([])$ is. |
|
1897 |
|
1898 \medskip For the definitionally-minded user it may be reassuring to |
|
1899 know that {\tt primrec} does not assert the reduction rules as new |
|
1900 axioms but derives them as theorems from an explicit definition of the |
|
1901 recursive function in terms of a recursion operator on the datatype. |
|
1902 |
|
1903 \index{primitive recursion|)} |
|
1904 \index{*primrec|)} |
1891 \index{*primrec|)} |
1905 \index{*datatype|)} |
1892 |
|
1893 |
|
1894 \subsection{Well-founded recursive functions} |
|
1895 \label{sec:HOL:recdef} |
|
1896 \index{primitive recursion|(} |
|
1897 \index{*recdef|(} |
|
1898 |
|
1899 Well-founded recursion can express any function whose termination can be |
|
1900 proved by showing that each recursive call makes the argument smaller in a |
|
1901 suitable sense. The recursion need not involve datatypes and there are few |
|
1902 syntactic restrictions. Nested recursion and pattern-matching are allowed. |
|
1903 |
|
1904 Here is a simple example, the Fibonacci function. The first line declares |
|
1905 \texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on |
|
1906 the natural numbers). Pattern-matching is used here: \texttt{1} is a |
|
1907 macro for \texttt{Suc~0}. |
|
1908 \begin{ttbox} |
|
1909 consts fib :: "nat => nat" |
|
1910 recdef fib "less_than" |
|
1911 "fib 0 = 0" |
|
1912 "fib 1 = 1" |
|
1913 "fib (Suc(Suc x)) = (fib x + fib (Suc x))" |
|
1914 \end{ttbox} |
|
1915 |
|
1916 The well-founded relation defines a notion of ``smaller'' for the function's |
|
1917 argument type. The relation $\prec$ is \textbf{well-founded} provided it |
|
1918 admits no infinitely decreasing chains |
|
1919 \[ \cdots\prec x@n\prec\cdots\prec x@1. \] |
|
1920 If the function's argument has type~$\tau$, then $\prec$ should be a relation |
|
1921 over~$\tau$: it must have type $(\tau\times\tau)set$. |
|
1922 |
|
1923 Proving well-foundedness can be tricky, so {\HOL} provides a collection of |
|
1924 operators for building well-founded relations. The package recognizes these |
|
1925 operators and automatically proves that the constructed relation is |
|
1926 well-founded. Here are those operators, in order of importance: |
|
1927 \begin{itemize} |
|
1928 \item \texttt{less_than} is ``less than'' on the natural numbers. |
|
1929 (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$. |
|
1930 |
|
1931 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the |
|
1932 relation~$\prec$ on type~$\tau$ such that $x\prec y$ iff $f(x)<f(y)$. |
|
1933 Typically, $f$ takes the recursive function's arguments (as a tuple) and |
|
1934 returns a result expressed in terms of the function \texttt{size}. It is |
|
1935 called a \textbf{measure function}. Recall that \texttt{size} is overloaded |
|
1936 and is defined on all datatypes (see \S\ref{sec:HOL:size}). |
|
1937 |
|
1938 \item $\mathop{\mathtt{inv_image}} f\;R$ is a generalization of |
|
1939 \texttt{measure}. It specifies a relation such that $x\prec y$ iff $f(x)$ |
|
1940 is less than $f(y)$ according to~$R$, which must itself be a well-founded |
|
1941 relation. |
|
1942 |
|
1943 \item $R@1\texttt{**}R@2$ is the lexicographic product of two relations. It |
|
1944 is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ iff $x@1$ |
|
1945 is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$ |
|
1946 is less than $y@2$ according to~$R@2$. |
|
1947 |
|
1948 \item \texttt{finite_psubset} is the proper subset relation on finite sets. |
|
1949 \end{itemize} |
|
1950 |
|
1951 We can use \texttt{measure} to declare Euclid's algorithm for the greatest |
|
1952 common divisor. The measure function, $\lambda(m,n).n$, specifies that the |
|
1953 recursion terminates because argument~$n$ decreases. |
|
1954 \begin{ttbox} |
|
1955 recdef gcd "measure ((\%(m,n).n) ::nat*nat=>nat)" |
|
1956 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" |
|
1957 \end{ttbox} |
|
1958 |
|
1959 The general form of a primitive recursive definition is |
|
1960 \begin{ttbox} |
|
1961 recdef {\it function} {\it rel} |
|
1962 congs {\it congruence rules} {\bf(optional)} |
|
1963 simpset {\it simplification set} {\bf(optional)} |
|
1964 {\it reduction rules} |
|
1965 \end{ttbox} |
|
1966 where |
|
1967 \begin{itemize} |
|
1968 \item \textit{function} is the name of the function, either as an \textit{id} |
|
1969 or a \textit{string}. |
|
1970 |
|
1971 \item \textit{rel} is a {\HOL} expression for the well-founded termination |
|
1972 relation. |
|
1973 |
|
1974 \item \textit{congruence rules} are required only in highly exceptional |
|
1975 circumstances. |
|
1976 |
|
1977 \item the \textit{simplification set} is used to prove that the supplied |
|
1978 relation is well-founded. It is also used to prove the \textbf{termination |
|
1979 conditions}: assertions that arguments of recursive calls decrease under |
|
1980 \textit{rel}. By default, simplification uses \texttt{!simpset}, which |
|
1981 is sufficient to prove well-foundedness for the built-in relations listed |
|
1982 above. |
|
1983 |
|
1984 \item \textit{reduction rules} specify one or more recursion equations. Each |
|
1985 left-hand side must have the form $f\,t$, where $f$ is the function and $t$ |
|
1986 is a tuple of distinct variables. If more than one equation is present then |
|
1987 $f$ is defined by pattern-matching on components of its argument whose type |
|
1988 is a \texttt{datatype}. The patterns must be exhaustive and |
|
1989 non-overlapping. |
|
1990 |
|
1991 Unlike with \texttt{primrec}, the reduction rules are not added to the |
|
1992 default simpset, and individual rules may not be labelled with identifiers. |
|
1993 However, the identifier $f$\texttt{.rules} is visible at the \ML\ level |
|
1994 as a list of theorems. |
|
1995 \end{itemize} |
|
1996 |
|
1997 With the definition of \texttt{gcd} shown above, Isabelle is unable to prove |
|
1998 one termination condition. It remains as a precondition of the recursion |
|
1999 theorems. |
|
2000 \begin{ttbox} |
|
2001 gcd.rules; |
|
2002 {\out ["! m n. n ~= 0 --> m mod n < n} |
|
2003 {\out ==> gcd (?m, ?n) = (if ?n = 0 then ?m else gcd (?n, ?m mod ?n))"] } |
|
2004 {\out : thm list} |
|
2005 \end{ttbox} |
|
2006 The theory \texttt{Primes} (on the examples directory \texttt{HOL/ex}) |
|
2007 illustrates how to prove termination conditions afterwards. The function |
|
2008 \texttt{Tfl.tgoalw} is like the standard function \texttt{goalw}, which sets |
|
2009 up a goal to prove, but its argument should be the identifier |
|
2010 $f$\texttt{.rules} and its effect is to set up a proof of the termination |
|
2011 conditions: |
|
2012 \begin{ttbox} |
|
2013 Tfl.tgoalw thy [] gcd.rules; |
|
2014 {\out Level 0} |
|
2015 {\out ! m n. n ~= 0 --> m mod n < n} |
|
2016 {\out 1. ! m n. n ~= 0 --> m mod n < n} |
|
2017 \end{ttbox} |
|
2018 This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem |
|
2019 is proved, it can be used to eliminate the termination conditions from |
|
2020 elements of \texttt{gcd.rules}. Theory \texttt{Unify} on directory |
|
2021 \texttt{HOL/Subst} is a much more complicated example of this process, where |
|
2022 the termination conditions can only be proved by complicated reasoning |
|
2023 involving the recursive function itself. |
|
2024 |
|
2025 Isabelle can prove the \texttt{gcd} function's termination condition |
|
2026 automatically if supplied with the right simpset. |
|
2027 \begin{ttbox} |
|
2028 recdef gcd "measure ((\%(m,n).n) ::nat*nat=>nat)" |
|
2029 simpset "!simpset addsimps [mod_less_divisor, zero_less_eq]" |
|
2030 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" |
|
2031 \end{ttbox} |
|
2032 |
|
2033 A \texttt{recdef} definition also returns an induction rule specialized for |
|
2034 the recursive function. For the \texttt{gcd} function above, the induction |
|
2035 rule is |
|
2036 \begin{ttbox} |
|
2037 gcd.induct; |
|
2038 {\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm} |
|
2039 \end{ttbox} |
|
2040 This rule should be used to reason inductively about the \texttt{gcd} |
|
2041 function. It usually makes the induction hypothesis available at all |
|
2042 recursive calls, leading to very direct proofs. If any termination |
|
2043 conditions remain unproved, they will be additional premises of this rule. |
|
2044 |
|
2045 \index{recursion!general|)} |
|
2046 \index{*recdef|)} |
1906 |
2047 |
1907 |
2048 |
1908 \section{Inductive and coinductive definitions} |
2049 \section{Inductive and coinductive definitions} |
1909 \index{*inductive|(} |
2050 \index{*inductive|(} |
1910 \index{*coinductive|(} |
2051 \index{*coinductive|(} |
1989 \end{figure} |
2131 \end{figure} |
1990 |
2132 |
1991 \subsection{The syntax of a (co)inductive definition} |
2133 \subsection{The syntax of a (co)inductive definition} |
1992 An inductive definition has the form |
2134 An inductive definition has the form |
1993 \begin{ttbox} |
2135 \begin{ttbox} |
1994 inductive {\it inductive sets} |
2136 inductive \textit{inductive sets} |
1995 intrs {\it introduction rules} |
2137 intrs \textit{introduction rules} |
1996 monos {\it monotonicity theorems} |
2138 monos \textit{monotonicity theorems} |
1997 con_defs {\it constructor definitions} |
2139 con_defs \textit{constructor definitions} |
1998 \end{ttbox} |
2140 \end{ttbox} |
1999 A coinductive definition is identical, except that it starts with the keyword |
2141 A coinductive definition is identical, except that it starts with the keyword |
2000 {\tt coinductive}. |
2142 {\tt coinductive}. |
2001 |
2143 |
2002 The {\tt monos} and {\tt con_defs} sections are optional. If present, |
2144 The \texttt{monos} and \texttt{con_defs} sections are optional. If present, |
2003 each is specified as a string, which must be a valid \ML{} expression |
2145 each is specified as a string, which must be a valid \ML{} expression |
2004 of type {\tt thm list}. It is simply inserted into the generated |
2146 of type \texttt{thm list}. It is simply inserted into the generated |
2005 \ML{} file that is generated from the theory definition; if it is |
2147 \ML{} file that is generated from the theory definition; if it is |
2006 ill-formed, it will trigger ML error messages. You can then inspect |
2148 ill-formed, it will trigger ML error messages. You can then inspect |
2007 the file on your directory. |
2149 the file on your directory. |
2008 |
2150 |
2009 \begin{itemize} |
2151 \begin{itemize} |
2010 \item The {\it inductive sets} are specified by one or more strings. |
2152 \item The \textit{inductive sets} are specified by one or more strings. |
2011 |
2153 |
2012 \item The {\it introduction rules} specify one or more introduction rules in |
2154 \item The \textit{introduction rules} specify one or more introduction rules in |
2013 the form {\it ident\/}~{\it string}, where the identifier gives the name of |
2155 the form \textit{ident\/}~\textit{string}, where the identifier gives the name of |
2014 the rule in the result structure. |
2156 the rule in the result structure. |
2015 |
2157 |
2016 \item The {\it monotonicity theorems} are required for each operator |
2158 \item The \textit{monotonicity theorems} are required for each operator |
2017 applied to a recursive set in the introduction rules. There {\bf must} |
2159 applied to a recursive set in the introduction rules. There {\bf must} |
2018 be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each |
2160 be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each |
2019 premise $t\in M(R@i)$ in an introduction rule! |
2161 premise $t\in M(R@i)$ in an introduction rule! |
2020 |
2162 |
2021 \item The {\it constructor definitions} contain definitions of constants |
2163 \item The \textit{constructor definitions} contain definitions of constants |
2022 appearing in the introduction rules. In most cases it can be omitted. |
2164 appearing in the introduction rules. In most cases it can be omitted. |
2023 \end{itemize} |
2165 \end{itemize} |
2024 |
2166 |
2025 The package has a few notable restrictions: |
2167 The package has a few notable restrictions: |
2026 \begin{itemize} |
2168 \begin{itemize} |
2071 monos "[Pow_mono]" |
2213 monos "[Pow_mono]" |
2072 end |
2214 end |
2073 \end{ttbox} |
2215 \end{ttbox} |
2074 The \HOL{} distribution contains many other inductive definitions. |
2216 The \HOL{} distribution contains many other inductive definitions. |
2075 Simple examples are collected on subdirectory \texttt{Induct}. The |
2217 Simple examples are collected on subdirectory \texttt{Induct}. The |
2076 theory {\tt HOL/Induct/LList.thy} contains coinductive definitions. |
2218 theory \texttt{HOL/Induct/LList.thy} contains coinductive definitions. |
2077 Larger examples may be found on other subdirectories, such as {\tt |
2219 Larger examples may be found on other subdirectories, such as {\tt |
2078 IMP}, {\tt Lambda} and {\tt Auth}. |
2220 IMP}, \texttt{Lambda} and \texttt{Auth}. |
2079 |
2221 |
2080 \index{*coinductive|)} \index{*inductive|)} |
2222 \index{*coinductive|)} \index{*inductive|)} |
2081 |
2223 |
2082 |
2224 |
2083 \section{The examples directories} |
2225 \section{The examples directories} |
2084 |
2226 |
2085 Directory {\tt HOL/Auth} contains theories for proving the correctness of |
2227 Directory \texttt{HOL/Auth} contains theories for proving the correctness of |
2086 cryptographic protocols. The approach is based upon operational |
2228 cryptographic protocols. The approach is based upon operational |
2087 semantics~\cite{paulson-security} rather than the more usual belief logics. |
2229 semantics~\cite{paulson-security} rather than the more usual belief logics. |
2088 On the same directory are proofs for some standard examples, such as the |
2230 On the same directory are proofs for some standard examples, such as the |
2089 Needham-Schroeder public-key authentication protocol~\cite{paulson-ns} |
2231 Needham-Schroeder public-key authentication protocol~\cite{paulson-ns} |
2090 and the Otway-Rees protocol. |
2232 and the Otway-Rees protocol. |
2091 |
2233 |
2092 Directory {\tt HOL/IMP} contains a formalization of various denotational, |
2234 Directory \texttt{HOL/IMP} contains a formalization of various denotational, |
2093 operational and axiomatic semantics of a simple while-language, the necessary |
2235 operational and axiomatic semantics of a simple while-language, the necessary |
2094 equivalence proofs, soundness and completeness of the Hoare rules with respect |
2236 equivalence proofs, soundness and completeness of the Hoare rules with respect |
2095 to the |
2237 to the |
2096 denotational semantics, and soundness and completeness of a verification |
2238 denotational semantics, and soundness and completeness of a verification |
2097 condition generator. Much of development is taken from |
2239 condition generator. Much of development is taken from |
2098 Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}. |
2240 Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}. |
2099 |
2241 |
2100 Directory {\tt HOL/Hoare} contains a user friendly surface syntax for Hoare |
2242 Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare |
2101 logic, including a tactic for generating verification-conditions. |
2243 logic, including a tactic for generating verification-conditions. |
2102 |
2244 |
2103 Directory {\tt HOL/MiniML} contains a formalization of the type system of the |
2245 Directory \texttt{HOL/MiniML} contains a formalization of the type system of the |
2104 core functional language Mini-ML and a correctness proof for its type |
2246 core functional language Mini-ML and a correctness proof for its type |
2105 inference algorithm $\cal W$~\cite{milner78,nazareth-nipkow}. |
2247 inference algorithm $\cal W$~\cite{milner78,nazareth-nipkow}. |
2106 |
2248 |
2107 Directory {\tt HOL/Lambda} contains a formalization of untyped |
2249 Directory \texttt{HOL/Lambda} contains a formalization of untyped |
2108 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$ |
2250 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$ |
2109 and $\eta$ reduction~\cite{Nipkow-CR}. |
2251 and $\eta$ reduction~\cite{Nipkow-CR}. |
2110 |
2252 |
2111 Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of |
2253 Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory of |
2112 substitutions and unifiers. It is based on Paulson's previous |
2254 substitutions and unifiers. It is based on Paulson's previous |
2113 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's |
2255 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's |
2114 theory~\cite{mw81}. |
2256 theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef}, |
2115 |
2257 with nested recursion. |
2116 Directory {\tt HOL/Induct} presents simple examples of (co)inductive |
2258 |
|
2259 Directory \texttt{HOL/Induct} presents simple examples of (co)inductive |
2117 definitions. |
2260 definitions. |
2118 \begin{itemize} |
2261 \begin{itemize} |
2119 \item Theory {\tt PropLog} proves the soundness and completeness of |
2262 \item Theory \texttt{PropLog} proves the soundness and completeness of |
2120 classical propositional logic, given a truth table semantics. The only |
2263 classical propositional logic, given a truth table semantics. The only |
2121 connective is $\imp$. A Hilbert-style axiom system is specified, and its |
2264 connective is $\imp$. A Hilbert-style axiom system is specified, and its |
2122 set of theorems defined inductively. A similar proof in \ZF{} is |
2265 set of theorems defined inductively. A similar proof in \ZF{} is |
2123 described elsewhere~\cite{paulson-set-II}. |
2266 described elsewhere~\cite{paulson-set-II}. |
2124 |
2267 |
2125 \item Theory {\tt Term} develops an experimental recursive type definition; |
2268 \item Theory \texttt{Term} develops an experimental recursive type definition; |
2126 the recursion goes through the type constructor~\tydx{list}. |
2269 the recursion goes through the type constructor~\tydx{list}. |
2127 |
2270 |
2128 \item Theory {\tt Simult} constructs mutually recursive sets of trees and |
2271 \item Theory \texttt{Simult} constructs mutually recursive sets of trees and |
2129 forests, including induction and recursion rules. |
2272 forests, including induction and recursion rules. |
2130 |
2273 |
2131 \item The definition of lazy lists demonstrates methods for handling |
2274 \item The definition of lazy lists demonstrates methods for handling |
2132 infinite data structures and coinduction in higher-order |
2275 infinite data structures and coinduction in higher-order |
2133 logic~\cite{paulson-coind}.% |
2276 logic~\cite{paulson-coind}.% |
2147 \item Theory \thydx{Exp} illustrates the use of iterated inductive definitions |
2290 \item Theory \thydx{Exp} illustrates the use of iterated inductive definitions |
2148 to express a programming language semantics that appears to require mutual |
2291 to express a programming language semantics that appears to require mutual |
2149 induction. Iterated induction allows greater modularity. |
2292 induction. Iterated induction allows greater modularity. |
2150 \end{itemize} |
2293 \end{itemize} |
2151 |
2294 |
2152 Directory {\tt HOL/ex} contains other examples and experimental proofs in |
2295 Directory \texttt{HOL/ex} contains other examples and experimental proofs in |
2153 {\HOL}. |
2296 {\HOL}. |
2154 \begin{itemize} |
2297 \begin{itemize} |
2155 \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty |
2298 \item Theory \texttt{Recdef} presents many examples of using \texttt{recdef} |
|
2299 to define recursive functions. Another example is \texttt{Fib}, which |
|
2300 defines the Fibonacci function. |
|
2301 |
|
2302 \item Theory \texttt{Primes} defines the Greatest Common Divisor of two |
|
2303 natural numbers and proves a key lemma of the Fundamental Theorem of |
|
2304 Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$ |
|
2305 or $p$ divides~$n$. |
|
2306 |
|
2307 \item Theory \texttt{Primrec} develops some computation theory. It |
|
2308 inductively defines the set of primitive recursive functions and presents a |
|
2309 proof that Ackermann's function is not primitive recursive. |
|
2310 |
|
2311 \item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty |
2156 predicate calculus theorems, ranging from simple tautologies to |
2312 predicate calculus theorems, ranging from simple tautologies to |
2157 moderately difficult problems involving equality and quantifiers. |
2313 moderately difficult problems involving equality and quantifiers. |
2158 |
2314 |
2159 \item File {\tt meson.ML} contains an experimental implementation of the {\sc |
2315 \item File \texttt{meson.ML} contains an experimental implementation of the {\sc |
2160 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is |
2316 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is |
2161 much more powerful than Isabelle's classical reasoner. But it is less |
2317 much more powerful than Isabelle's classical reasoner. But it is less |
2162 useful in practice because it works only for pure logic; it does not |
2318 useful in practice because it works only for pure logic; it does not |
2163 accept derived rules for the set theory primitives, for example. |
2319 accept derived rules for the set theory primitives, for example. |
2164 |
2320 |
2165 \item File {\tt mesontest.ML} contains test data for the {\sc meson} proof |
2321 \item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof |
2166 procedure. These are mostly taken from Pelletier \cite{pelletier86}. |
2322 procedure. These are mostly taken from Pelletier \cite{pelletier86}. |
2167 |
2323 |
2168 \item File {\tt set.ML} proves Cantor's Theorem, which is presented in |
2324 \item File \texttt{set.ML} proves Cantor's Theorem, which is presented in |
2169 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem. |
2325 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem. |
2170 |
2326 |
2171 \item Theory {\tt MT} contains Jacob Frost's formalization~\cite{frost93} of |
2327 \item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of |
2172 Milner and Tofte's coinduction example~\cite{milner-coind}. This |
2328 Milner and Tofte's coinduction example~\cite{milner-coind}. This |
2173 substantial proof concerns the soundness of a type system for a simple |
2329 substantial proof concerns the soundness of a type system for a simple |
2174 functional language. The semantics of recursion is given by a cyclic |
2330 functional language. The semantics of recursion is given by a cyclic |
2175 environment, which makes a coinductive argument appropriate. |
2331 environment, which makes a coinductive argument appropriate. |
2176 \end{itemize} |
2332 \end{itemize} |