3 \index{higher-order logic|(} |
3 \index{higher-order logic|(} |
4 \index{HOL system@{\sc hol} system} |
4 \index{HOL system@{\sc hol} system} |
5 |
5 |
6 The theory~\thydx{HOL} implements higher-order logic. It is based on |
6 The theory~\thydx{HOL} implements higher-order logic. It is based on |
7 Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on |
7 Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on |
8 Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is |
8 Church's original paper~\cite{church40}. Andrews's |
9 a full description of higher-order logic. Experience with the {\sc hol} |
9 book~\cite{andrews86} is a full description of the original |
10 system has demonstrated that higher-order logic is widely applicable in many |
10 Church-style higher-order logic. Experience with the {\sc hol} system |
11 areas of mathematics and computer science, not just hardware verification, |
11 has demonstrated that higher-order logic is widely applicable in many |
12 {\sc hol}'s original {\it raison d'\^etre\/}. It is weaker than {\ZF} set |
12 areas of mathematics and computer science, not just hardware |
13 theory but for most applications this does not matter. If you prefer {\ML} |
13 verification, {\sc hol}'s original {\it raison d'\^etre\/}. It is |
14 to Lisp, you will probably prefer \HOL\ to~{\ZF}. |
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\ |
|
16 to~{\ZF}. |
15 |
17 |
16 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 |
17 different syntax. Ancient releases of Isabelle included still another version |
19 different syntax. Ancient releases of Isabelle included still another version |
18 of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This |
20 of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This |
19 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 |
138 When using $=$ to mean logical equivalence, enclose both operands in |
141 When using $=$ to mean logical equivalence, enclose both operands in |
139 parentheses. |
142 parentheses. |
140 \end{warn} |
143 \end{warn} |
141 |
144 |
142 \subsection{Types and classes} |
145 \subsection{Types and classes} |
143 The type class of higher-order terms is called~\cldx{term}. By default, |
146 The universal type class of higher-order terms is called~\cldx{term}. |
144 explicit type variables have class \cldx{term}. In particular the equality |
147 By default, explicit type variables have class \cldx{term}. In |
145 symbol and quantifiers are polymorphic over class {\tt term}. |
148 particular the equality symbol and quantifiers are polymorphic over |
|
149 class {\tt term}. |
146 |
150 |
147 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, |
151 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, |
148 formulae are terms. The built-in type~\tydx{fun}, which constructs function |
152 formulae are terms. The built-in type~\tydx{fun}, which constructs |
149 types, is overloaded with arity {\tt(term,term)term}. Thus, $\sigma\To\tau$ |
153 function types, is overloaded with arity {\tt(term,\thinspace |
150 belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification |
154 term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt |
151 over functions. |
155 term} if $\sigma$ and~$\tau$ do, allowing quantification over |
152 |
156 functions. |
153 HOL offers various methods for introducing new |
157 |
154 types. See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}. |
158 \HOL\ offers various methods for introducing new types. |
155 |
159 See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}. |
156 Theory \thydx{Ord} defines the class \cldx{ord} of all ordered types; the |
160 |
157 relations $<$ and $\leq$ are polymorphic over this class, as are the functions |
161 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order |
158 \cdx{mono}, \cdx{min} and \cdx{max}, and the least element operator |
162 signatures; the relations $<$ and $\leq$ are polymorphic over this |
159 \cdx{LEAST}. \thydx{Ord} also defines the subclass \cldx{order} of \cldx{ord} |
163 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and |
160 which axiomatizes partially ordered types (w.r.t.\ $\le$). |
164 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass |
161 |
165 \cldx{order} of \cldx{ord} which axiomatizes partially ordered types |
162 Three other type classes --- \cldx{plus}, \cldx{minus} and \cldx{times} --- |
166 (w.r.t.\ $\le$). |
163 permit overloading of the operators {\tt+},\index{*"+ symbol} |
167 |
164 {\tt-}\index{*"- symbol} and {\tt*}.\index{*"* symbol} In particular, {\tt-} |
168 Three other syntactic type classes --- \cldx{plus}, \cldx{minus} and |
165 is overloaded for set difference and subtraction. |
169 \cldx{times} --- permit overloading of the operators {\tt+},\index{*"+ |
|
170 symbol} {\tt-}\index{*"- symbol} and {\tt*}.\index{*"* symbol} In |
|
171 particular, {\tt-} is instantiated for set difference and subtraction |
|
172 on natural numbers. |
166 |
173 |
167 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 |
168 type constraints. Type inference may otherwise make the goal more |
175 type constraints. Type inference may otherwise make the goal more |
169 polymorphic than you intended, with confusing results. For example, the |
176 polymorphic than you intended, with confusing results. For example, the |
170 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 |
239 \[\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\] |
240 as a uniform means of expressing {\tt case} constructs. Therefore {\tt case} |
253 as a uniform means of expressing {\tt case} constructs. Therefore {\tt case} |
241 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 |
242 logical meaning. By declaring translations, you can cause instances of the |
255 logical meaning. By declaring translations, you can cause instances of the |
243 {\tt case} construct to denote applications of particular case operators. |
256 {\tt case} construct to denote applications of particular case operators. |
244 This is what happens automatically for each {\tt datatype} declaration |
257 This is what happens automatically for each {\tt datatype} definition |
245 (see~\S\ref{sec:HOL:datatype}). |
258 (see~\S\ref{sec:HOL:datatype}). |
246 |
259 |
247 \begin{warn} |
260 \begin{warn} |
248 Both {\tt if} and {\tt case} constructs have as low a priority as |
261 Both {\tt if} and {\tt case} constructs have as low a priority as |
249 quantifiers, which requires additional enclosing parenthesis in the context |
262 quantifiers, which requires additional enclosing parentheses in the context |
250 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 |
251 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 |
252 \dots)$. |
265 \dots)$. |
253 \end{warn} |
266 \end{warn} |
254 |
267 |
255 \section{Rules of inference} |
268 \section{Rules of inference} |
256 |
269 |
257 \begin{figure} |
270 \begin{figure} |
258 \begin{ttbox}\makeatother |
271 \begin{ttbox}\makeatother |
259 \tdx{refl} t = t |
272 \tdx{refl} t = (t::'a) |
260 \tdx{subst} [| s=t; P s |] ==> P t |
273 \tdx{subst} [| s = t; P s |] ==> P (t::'a) |
261 \tdx{ext} (!!x. f x = g x) ==> (\%x.f x) = (\%x.g x) |
274 \tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x.f x) = (\%x.g x) |
262 \tdx{impI} (P ==> Q) ==> P-->Q |
275 \tdx{impI} (P ==> Q) ==> P-->Q |
263 \tdx{mp} [| P-->Q; P |] ==> Q |
276 \tdx{mp} [| P-->Q; P |] ==> Q |
264 \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q) |
277 \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q) |
265 \tdx{selectI} P(x) ==> P(@x.P x) |
278 \tdx{selectI} P(x::'a) ==> P(@x.P x) |
266 \tdx{True_or_False} (P=True) | (P=False) |
279 \tdx{True_or_False} (P=True) | (P=False) |
267 \end{ttbox} |
280 \end{ttbox} |
268 \caption{The {\tt HOL} rules} \label{hol-rules} |
281 \caption{The {\tt HOL} rules} \label{hol-rules} |
269 \end{figure} |
282 \end{figure} |
270 |
283 |
567 very natural: {\tt Collect} maps $\alpha\To bool$ to $\alpha\,set$, while |
581 very natural: {\tt Collect} maps $\alpha\To bool$ to $\alpha\,set$, while |
568 \hbox{\tt op :} maps in the other direction (ignoring argument order). |
582 \hbox{\tt op :} maps in the other direction (ignoring argument order). |
569 |
583 |
570 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax |
584 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax |
571 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new |
585 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new |
572 constructs. Infix operators include union and intersection ($A\union B$ |
586 constructs. Infix operators include union and intersection ($A\un B$ |
573 and $A\inter B$), the subset and membership relations, and the image |
587 and $A\int B$), the subset and membership relations, and the image |
574 operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to |
588 operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to |
575 $\neg(a\in b)$. |
589 $\neg(a\in b)$. |
576 |
590 |
577 The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the |
591 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in |
578 obvious manner using~{\tt insert} and~$\{\}$: |
592 the obvious manner using~{\tt insert} and~$\{\}$: |
579 \begin{eqnarray*} |
593 \begin{eqnarray*} |
580 \{a@1, \ldots, a@n\} & \equiv & |
594 \{a, b, c\} & \equiv & |
581 {\tt insert}~a@1~({\tt insert}\ldots({\tt insert}~a@n~\{\})\ldots) |
595 {\tt insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\})) |
582 \end{eqnarray*} |
596 \end{eqnarray*} |
583 |
597 |
584 The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type) |
598 The set \hbox{\tt{\ttlbrace}$x$.$P[x]${\ttrbrace}} consists of all $x$ (of suitable type) |
585 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free |
599 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free |
586 occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda |
600 occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda |
587 x.P[x])$. It defines sets by absolute comprehension, which is impossible |
601 x.P[x])$. It defines sets by absolute comprehension, which is impossible |
588 in~{\ZF}; the type of~$x$ implicitly restricts the comprehension. |
602 in~{\ZF}; the type of~$x$ implicitly restricts the comprehension. |
589 |
603 |
618 |
632 |
619 |
633 |
620 |
634 |
621 \begin{figure} \underscoreon |
635 \begin{figure} \underscoreon |
622 \begin{ttbox} |
636 \begin{ttbox} |
623 \tdx{mem_Collect_eq} (a : \{x.P x\}) = P a |
637 \tdx{mem_Collect_eq} (a : {\ttlbrace}x.P x{\ttrbrace}) = P a |
624 \tdx{Collect_mem_eq} \{x.x:A\} = A |
638 \tdx{Collect_mem_eq} {\ttlbrace}x.x:A{\ttrbrace} = A |
625 |
639 |
626 \tdx{empty_def} \{\} == \{x.False\} |
640 \tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x.False{\ttrbrace} |
627 \tdx{insert_def} insert a B == \{x.x=a\} Un B |
641 \tdx{insert_def} insert a B == {\ttlbrace}x.x=a{\ttrbrace} Un B |
628 \tdx{Ball_def} Ball A P == ! x. x:A --> P x |
642 \tdx{Ball_def} Ball A P == ! x. x:A --> P x |
629 \tdx{Bex_def} Bex A P == ? x. x:A & P x |
643 \tdx{Bex_def} Bex A P == ? x. x:A & P x |
630 \tdx{subset_def} A <= B == ! x:A. x:B |
644 \tdx{subset_def} A <= B == ! x:A. x:B |
631 \tdx{Un_def} A Un B == \{x.x:A | x:B\} |
645 \tdx{Un_def} A Un B == {\ttlbrace}x.x:A | x:B{\ttrbrace} |
632 \tdx{Int_def} A Int B == \{x.x:A & x:B\} |
646 \tdx{Int_def} A Int B == {\ttlbrace}x.x:A & x:B{\ttrbrace} |
633 \tdx{set_diff_def} A - B == \{x.x:A & x~:B\} |
647 \tdx{set_diff_def} A - B == {\ttlbrace}x.x:A & x~:B{\ttrbrace} |
634 \tdx{Compl_def} Compl A == \{x. ~ x:A\} |
648 \tdx{Compl_def} Compl A == {\ttlbrace}x. ~ x:A{\ttrbrace} |
635 \tdx{INTER_def} INTER A B == \{y. ! x:A. y: B x\} |
649 \tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace} |
636 \tdx{UNION_def} UNION A B == \{y. ? x:A. y: B x\} |
650 \tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace} |
637 \tdx{INTER1_def} INTER1 B == INTER \{x.True\} B |
651 \tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x.True{\ttrbrace} B |
638 \tdx{UNION1_def} UNION1 B == UNION \{x.True\} B |
652 \tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x.True{\ttrbrace} B |
639 \tdx{Inter_def} Inter S == (INT x:S. x) |
653 \tdx{Inter_def} Inter S == (INT x:S. x) |
640 \tdx{Union_def} Union S == (UN x:S. x) |
654 \tdx{Union_def} Union S == (UN x:S. x) |
641 \tdx{Pow_def} Pow A == \{B. B <= A\} |
655 \tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace} |
642 \tdx{image_def} f``A == \{y. ? x:A. y=f x\} |
656 \tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace} |
643 \tdx{range_def} range f == \{y. ? x. y=f x\} |
657 \tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace} |
644 \end{ttbox} |
658 \end{ttbox} |
645 \caption{Rules of the theory {\tt Set}} \label{hol-set-rules} |
659 \caption{Rules of the theory {\tt Set}} \label{hol-set-rules} |
646 \end{figure} |
660 \end{figure} |
647 |
661 |
648 |
662 |
649 \begin{figure} \underscoreon |
663 \begin{figure} \underscoreon |
650 \begin{ttbox} |
664 \begin{ttbox} |
651 \tdx{CollectI} [| P a |] ==> a : \{x.P x\} |
665 \tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x.P x{\ttrbrace} |
652 \tdx{CollectD} [| a : \{x.P x\} |] ==> P a |
666 \tdx{CollectD} [| a : {\ttlbrace}x.P x{\ttrbrace} |] ==> P a |
653 \tdx{CollectE} [| a : \{x.P x\}; P a ==> W |] ==> W |
667 \tdx{CollectE} [| a : {\ttlbrace}x.P x{\ttrbrace}; P a ==> W |] ==> W |
654 |
668 |
655 \tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x |
669 \tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x |
656 \tdx{bspec} [| ! x:A. P x; x:A |] ==> P x |
670 \tdx{bspec} [| ! x:A. P x; x:A |] ==> P x |
657 \tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q |
671 \tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q |
658 |
672 |
986 \end{ttbox} |
1003 \end{ttbox} |
987 \caption{Type $\alpha\times\beta$}\label{hol-prod} |
1004 \caption{Type $\alpha\times\beta$}\label{hol-prod} |
988 \end{figure} |
1005 \end{figure} |
989 |
1006 |
990 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type |
1007 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type |
991 $\alpha\times\beta$, with the ordered pair syntax {\tt($a$,$b$)}. Tuples are |
1008 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General |
992 simulated by pairs nested to the right: |
1009 tuples are simulated by pairs nested to the right: |
993 \begin{center} |
1010 \begin{center} |
994 \begin{tabular}{|c|c|} |
1011 \begin{tabular}{|c|c|} |
995 \hline |
1012 \hline |
996 external & internal \\ |
1013 external & internal \\ |
997 \hline |
1014 \hline |
998 $\tau@1 * \dots * \tau@n$ & $\tau@1 * (\dots (\tau@{n-1} * \tau@n)\dots)$ \\ |
1015 $\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\ |
999 \hline |
1016 \hline |
1000 $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\ |
1017 $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\ |
1001 \hline |
1018 \hline |
1002 \end{tabular} |
1019 \end{tabular} |
1003 \end{center} |
1020 \end{center} |
1004 In addition, it is possible to use tuples |
1021 In addition, it is possible to use tuples |
1005 as patterns in abstractions: |
1022 as patterns in abstractions: |
1006 \begin{center} |
1023 \begin{center} |
1007 {\tt\%($x$,$y$).$t$} \quad stands for\quad {\tt split(\%$x$ $y$.$t$)} |
1024 {\tt\%($x$,$y$).$t$} \quad stands for\quad {\tt split(\%$x$\thinspace$y$.$t$)} |
1008 \end{center} |
1025 \end{center} |
1009 Nested patterns are also supported. They are translated stepwise: |
1026 Nested patterns are also supported. They are translated stepwise: |
1010 {\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$ |
1027 {\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$ |
1011 {\tt split(\%$x$.\%($y$,$z$).$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$ |
1028 {\tt split(\%$x$.\%($y$,$z$).$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$ |
1012 $z$.$t$))}. The reverse translation is performed upon printing. |
1029 $z$.$t$))}. The reverse translation is performed upon printing. |
1177 |
1194 |
1178 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the |
1195 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the |
1179 overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also |
1196 overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also |
1180 \cdx{min}, \cdx{max} and \cdx{LEAST}) available on {\tt nat}. Theory |
1197 \cdx{min}, \cdx{max} and \cdx{LEAST}) available on {\tt nat}. Theory |
1181 \thydx{Nat} builds on {\tt NatDef} and shows that {\tt<=} is a partial order, |
1198 \thydx{Nat} builds on {\tt NatDef} and shows that {\tt<=} is a partial order, |
1182 i.e.\ {\tt nat} is an instance of class {\tt order}. |
1199 i.e.\ {\tt nat} is even an instance of class {\tt order}. |
1183 |
1200 |
1184 Theory \thydx{Arith} develops arithmetic on the natural numbers. It |
1201 Theory \thydx{Arith} develops arithmetic on the natural numbers. It |
1185 defines addition, multiplication, subtraction, division, and remainder. |
1202 defines addition, multiplication, subtraction, division, and remainder. |
1186 Many of their properties are proved: commutative, associative and |
1203 Many of their properties are proved: commutative, associative and |
1187 distributive laws, identity and cancellation laws, etc. |
1204 distributive laws, identity and cancellation laws, etc. |
1188 % The most |
1205 % The most |
1189 %interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$. |
1206 %interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$. |
1190 Division and remainder are defined by repeated subtraction, which requires |
1207 Division and remainder are defined by repeated subtraction, which |
1191 well-founded rather than primitive recursion. See Figs.\ts\ref{hol-nat1} |
1208 requires well-founded rather than primitive recursion. See |
1192 and~\ref{hol-nat2}. The recursion equations for the operators {\tt +}, {\tt |
1209 Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The recursion equations for |
1193 -} and {\tt *} are part of the default simpset. |
1210 the operators {\tt +}, {\tt -} and {\tt *} on \texttt{nat} are part of |
|
1211 the default simpset. |
1194 |
1212 |
1195 Functions on {\tt nat} can be defined by primitive recursion, for example |
1213 Functions on {\tt nat} can be defined by primitive recursion, for example |
1196 addition: |
1214 addition: |
1197 \begin{ttbox} |
1215 \begin{ttbox} |
1198 \sdx{primrec} "op +" nat |
1216 \sdx{primrec} "op +" nat |
1199 "0 + n = n" |
1217 "0 + n = n" |
1200 "Suc m + n = Suc(m + n)" |
1218 "Suc m + n = Suc(m + n)" |
1201 \end{ttbox} |
1219 \end{ttbox} |
1202 (Remember that the name of an infix operator $\oplus$ is {\tt op}~$\oplus$.) |
1220 Remember that the name of infix operators usually has an {\tt op} |
1203 The general format for defining primitive recursive functions on {\tt nat} |
1221 prefixed. The general format for defining primitive recursive |
1204 follows the rules for primitive recursive functions on datatypes |
1222 functions on {\tt nat} follows the rules for primitive recursive |
1205 (see~\S\ref{sec:HOL:primrec}). |
1223 functions on datatypes (see~\S\ref{sec:HOL:primrec}). There is also a |
1206 There is also a \sdx{case}-construct of the form |
1224 \sdx{case}-construct of the form |
1207 \begin{ttbox} |
1225 \begin{ttbox} |
1208 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\) |
1226 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\) |
1209 \end{ttbox} |
1227 \end{ttbox} |
1210 Note that Isabelle insists on precisely this format; you may not even change |
1228 Note that Isabelle insists on precisely this format; you may not even change |
1211 the order of the two cases. |
1229 the order of the two cases. |
1356 |
1372 |
1357 \subsection{The type constructor for lists, {\tt list}} |
1373 \subsection{The type constructor for lists, {\tt list}} |
1358 \index{*list type} |
1374 \index{*list type} |
1359 |
1375 |
1360 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list |
1376 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list |
1361 operations with their types and syntax. The type constructor {\tt list} is |
1377 operations with their types and syntax. Type $\alpha \; list$ is |
1362 defined as a {\tt datatype} with the constructors {\tt[]} and {\tt\#}. As a |
1378 defined as a {\tt datatype} with the constructors {\tt[]} and {\tt\#}. |
1363 result the generic induction tactic \ttindex{induct_tac} also performs |
1379 As a result the generic induction tactic \ttindex{induct_tac} also |
1364 structural induction over lists. A \sdx{case} construct of the form |
1380 performs structural induction over lists. A \sdx{case} construct of |
|
1381 the form |
1365 \begin{center}\tt |
1382 \begin{center}\tt |
1366 case $e$ of [] => $a$ | \(x\)\#\(xs\) => b |
1383 case $e$ of [] => $a$ | \(x\)\#\(xs\) => b |
1367 \end{center} |
1384 \end{center} |
1368 is defined by translation. For details see~\S\ref{sec:HOL:datatype}. |
1385 is defined by translation. For details see~\S\ref{sec:HOL:datatype}. |
1369 |
1386 |
1370 {\tt List} provides a basic library of list processing functions defined by |
1387 {\tt List} provides a basic library of list processing functions defined by |
1371 primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations |
1388 primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations |
1372 are shown in Fig.\ts\ref{fig:HOL:list-simps}. |
1389 are shown in Fig.\ts\ref{fig:HOL:list-simps}. |
1373 |
1390 |
1374 |
1391 |
1375 \subsection{Introducing new types} |
1392 \subsection{Introducing new types} \label{sec:typedef} |
1376 |
1393 |
1377 The \HOL-methodology dictates that all extension to a theory should be |
1394 The \HOL-methodology dictates that all extensions to a theory should |
1378 conservative and thus preserve consistency. There are two basic type |
1395 be \textbf{definitional}. The basic type definition mechanism which |
1379 extension mechanisms which meet this criterion: {\em type synonyms\/} and |
1396 meets this criterion --- w.r.t.\ the standard model theory of |
1380 {\em type definitions\/}. The former are inherited from {\tt Pure} and are |
1397 \textsc{hol} --- is \ttindex{typedef}. Note that \emph{type synonyms}, |
1381 described elsewhere. |
1398 which are inherited from {\Pure} and described elsewhere, are just |
|
1399 syntactic abbreviations that have no logical meaning. |
|
1400 |
1382 \begin{warn} |
1401 \begin{warn} |
1383 Types in \HOL\ must be non-empty; otherwise the quantifier rules would be |
1402 Types in \HOL\ must be non-empty; otherwise the quantifier rules would be |
1384 unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}. |
1403 unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}. |
1385 \end{warn} |
1404 \end{warn} |
1386 A \bfindex{type definition} identifies the new type with a subset of an |
1405 A \bfindex{type definition} identifies the new type with a subset of an |
1392 \ldots, $\alpha@n$, then the type definition creates a type constructor |
1411 \ldots, $\alpha@n$, then the type definition creates a type constructor |
1393 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type. |
1412 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type. |
1394 |
1413 |
1395 \begin{figure}[htbp] |
1414 \begin{figure}[htbp] |
1396 \begin{rail} |
1415 \begin{rail} |
1397 typedef : 'typedef' ( () | '(' tname ')') type '=' set witness; |
1416 typedef : 'typedef' ( () | '(' name ')') type '=' set witness; |
1398 type : typevarlist name ( () | '(' infix ')' ); |
1417 type : typevarlist name ( () | '(' infix ')' ); |
1399 tname : name; |
|
1400 set : string; |
1418 set : string; |
1401 witness : () | '(' id ')'; |
1419 witness : () | '(' id ')'; |
1402 \end{rail} |
1420 \end{rail} |
1403 \caption{Syntax of type definition} |
1421 \caption{Syntax of type definitions} |
1404 \label{fig:HOL:typedef} |
1422 \label{fig:HOL:typedef} |
1405 \end{figure} |
1423 \end{figure} |
1406 |
1424 |
1407 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For |
1425 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For |
1408 the definition of `typevarlist' and `infix' see |
1426 the definition of `typevarlist' and `infix' see |
1409 \iflabelundefined{chap:classical} |
1427 \iflabelundefined{chap:classical} |
1410 {the appendix of the {\em Reference Manual\/}}% |
1428 {the appendix of the {\em Reference Manual\/}}% |
1411 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the |
1429 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the |
1412 following meaning: |
1430 following meaning: |
1413 \begin{description} |
1431 \begin{description} |
1414 \item[\it type]: the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with |
1432 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with |
1415 optional infix annotation. |
1433 optional infix annotation. |
1416 \item[\it tname]: an alphanumeric name $T$ for the type constructor $ty$, in |
1434 \item[\it name:] an alphanumeric name $T$ for the type constructor |
1417 case $ty$ is a symbolic name. Default: $ty$. |
1435 $ty$, in case $ty$ is a symbolic name. Defaults to $ty$. |
1418 \item[\it set]: the representing subset $A$. |
1436 \item[\it set:] the representing subset $A$. |
1419 \item[\it witness]: name of a theorem of the form $a:A$ proving |
1437 \item[\it witness:] name of a theorem of the form $a:A$ proving |
1420 non-emptiness. Can be omitted in case Isabelle manages to prove |
1438 non-emptiness. It can be omitted in case Isabelle manages to prove |
1421 non-emptiness automatically. |
1439 non-emptiness automatically. |
1422 \end{description} |
1440 \end{description} |
1423 If all context conditions are met (no duplicate type variables in |
1441 If all context conditions are met (no duplicate type variables in |
1424 `typevarlist', no extra type variables in `set', and no free term variables |
1442 `typevarlist', no extra type variables in `set', and no free term variables |
1425 in `set'), the following components are added to the theory: |
1443 in `set'), the following components are added to the theory: |
1426 \begin{itemize} |
1444 \begin{itemize} |
1427 \item a type $ty :: (term,\dots)term$; |
1445 \item a type $ty :: (term,\dots)term$; |
1428 \item constants |
1446 \item constants |
1429 \begin{eqnarray*} |
1447 \begin{eqnarray*} |
1430 T &::& (\tau)set \\ |
1448 T &::& \tau\;set \\ |
1431 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\ |
1449 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\ |
1432 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty |
1450 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty |
1433 \end{eqnarray*} |
1451 \end{eqnarray*} |
1434 \item a definition and three axioms |
1452 \item a definition and three axioms |
1435 \[ |
1453 \[ |
1436 \begin{array}{ll} |
1454 \begin{array}{ll} |
1437 T{\tt_def} & T \equiv A \\ |
1455 T{\tt_def} & T \equiv A \\ |
1438 {\tt Rep_}T & Rep_T(x) : T \\ |
1456 {\tt Rep_}T & Rep_T\,x \in T \\ |
1439 {\tt Rep_}T{\tt_inverse} & Abs_T(Rep_T(x)) = x \\ |
1457 {\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\ |
1440 {\tt Abs_}T{\tt_inverse} & y:T \Imp Rep_T(Abs_T(y)) = y |
1458 {\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y |
1441 \end{array} |
1459 \end{array} |
1442 \] |
1460 \] |
1443 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$ |
1461 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$ |
1444 and its inverse $Abs_T$. |
1462 and its inverse $Abs_T$. |
1445 \end{itemize} |
1463 \end{itemize} |
1446 Here are two simple examples where emptiness is proved automatically: |
1464 Below are two simple examples of \HOL\ type definitions. Emptiness is |
1447 \begin{ttbox} |
1465 proved automatically here. |
1448 typedef unit = "\{True\}" |
1466 \begin{ttbox} |
|
1467 typedef unit = "{\ttlbrace}True{\ttrbrace}" |
1449 |
1468 |
1450 typedef (prod) |
1469 typedef (prod) |
1451 ('a, 'b) "*" (infixr 20) |
1470 ('a, 'b) "*" (infixr 20) |
1452 = "\{f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b)\}" |
1471 = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}" |
1453 \end{ttbox} |
1472 \end{ttbox} |
1454 |
1473 |
1455 Type definitions permit the introduction of abstract data types in a safe |
1474 Type definitions permit the introduction of abstract data types in a safe |
1456 way, namely by providing models based on already existing types. Given some |
1475 way, namely by providing models based on already existing types. Given some |
1457 abstract axiomatic description $P$ of a type, this involves two steps: |
1476 abstract axiomatic description $P$ of a type, this involves two steps: |
1467 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by |
1486 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by |
1468 declaring the type and its operations and by stating the desired axioms, you |
1487 declaring the type and its operations and by stating the desired axioms, you |
1469 should make sure the type has a non-empty model. You must also have a clause |
1488 should make sure the type has a non-empty model. You must also have a clause |
1470 \par |
1489 \par |
1471 \begin{ttbox} |
1490 \begin{ttbox} |
1472 arities \(ty\): (term,\(\dots\),term)term |
1491 arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term |
1473 \end{ttbox} |
1492 \end{ttbox} |
1474 in your theory file to tell Isabelle that $ty$ is in class {\tt term}, the |
1493 in your theory file to tell Isabelle that $ty$ is in class {\tt term}, the |
1475 class of all HOL types. |
1494 class of all \HOL\ types. |
1476 \end{warn} |
1495 \end{warn} |
1477 |
1496 |
1478 \section{Datatype declarations} |
1497 \section{Datatype declarations} |
1479 \label{sec:HOL:datatype} |
1498 \label{sec:HOL:datatype} |
1480 \index{*datatype|(} |
1499 \index{*datatype|(} |
1481 |
1500 |
1482 It is often necessary to extend a theory with \ML-like datatypes. This |
1501 Inductive datatypes similar to those of \ML{} frequently appear in |
1483 extension consists of the new type, declarations of its constructors and |
1502 non-trivial applications of \HOL. In principle, such types could be |
1484 rules that describe the new type. The theory definition section {\tt |
1503 defined by hand via \texttt{typedef} (see \S\ref{sec:typedef}), but |
1485 datatype} automates this. |
1504 this would be far too tedious. The \ttindex{datatype} definition |
1486 |
1505 package of \HOL\ automates such chores. It generates freeness and |
1487 |
1506 induction rules from a very simple description provided by the user. |
1488 \subsection{Foundations} |
1507 |
1489 |
1508 |
1490 \underscoreon |
1509 \subsection{Basics} |
1491 |
1510 |
1492 A datatype declaration has the following general structure: |
1511 The general \HOL\ \texttt{datatype} definition is of the following form: |
1493 \[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~ |
1512 \[ |
1494 C_1~\tau_{11}~\dots~\tau_{1k_1} ~\mid~ \dots ~\mid~ |
1513 \mathtt{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~ |
1495 C_m~\tau_{m1}~\dots~\tau_{mk_m} |
1514 C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~ |
|
1515 C@m~\tau@{m1}~\dots~\tau@{mk@m} |
1496 \] |
1516 \] |
1497 where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and |
1517 where $\alpha@i$ are type variables, $C@i$ are distinct constructor |
1498 $\tau_{ij}$ are one of the following: |
1518 names and $\tau@{ij}$ are types. The latter may be one of the |
|
1519 following: |
1499 \begin{itemize} |
1520 \begin{itemize} |
1500 \item type variables $\alpha_1,\dots,\alpha_n$, |
1521 \item type variables $\alpha@1, \dots, \alpha@n$, |
1501 \item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared |
1522 |
1502 type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq |
1523 \item types $(\beta@1, \dots, \beta@l) \, t'$ where $t'$ is a |
1503 \{\alpha_1,\dots,\alpha_n\}$, |
1524 previously declared type constructor or type synonym and $\{\beta@1, |
1504 \item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This |
1525 \dots, \beta@l\} \subseteq \{\alpha@1, \dots, \alpha@n\}$, |
1505 makes it a recursive type. To ensure that the new type is not empty at |
1526 |
1506 least one constructor must consist of only non-recursive type |
1527 \item the newly defined type $(\alpha@1, \dots, \alpha@n) \, t$. |
1507 components.} |
|
1508 \end{itemize} |
1528 \end{itemize} |
1509 If you would like one of the $\tau_{ij}$ to be a complex type expression |
1529 Recursive occurences of $(\alpha@1, \dots, \alpha@n) \, t$ are quite |
1510 $\tau$ you need to declare a new type synonym $syn = \tau$ first and use |
1530 restricted. To ensure that the new type is not empty, at least one |
1511 $syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the |
1531 constructor must consist of only non-recursive type components. If |
1512 recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt |
1532 you would like one of the $\tau@{ij}$ to be a complex type expression |
1513 datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[ |
1533 $\tau$ you need to declare a new type synonym $syn = \tau$ first and |
1514 \mbox{\tt datatype}~ t ~=~ C(t~list). \] |
1534 use $syn$ in place of $\tau$. Of course this does not work if $\tau$ |
|
1535 mentions the recursive type itself, thus ruling out problematic cases |
|
1536 like $\mathtt{datatype}~ t ~=~ C \, (t \To t)$, but also unproblematic |
|
1537 ones like $\mathtt{datatype}~ t ~=~ C \, (t~list)$. |
1515 |
1538 |
1516 The constructors are automatically defined as functions of their respective |
1539 The constructors are automatically defined as functions of their respective |
1517 type: |
1540 type: |
1518 \[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \] |
1541 \[ C@j : [\tau@{j1},\dots,\tau@{jk@j}] \To (\alpha@1,\dots,\alpha@n)t \] |
1519 These functions have certain {\em freeness} properties: |
1542 These functions have certain {\em freeness} properties: |
1520 \begin{description} |
1543 \begin{itemize} |
1521 \item[\tt distinct] They are distinct: |
1544 |
1522 \[ C_i~x_1~\dots~x_{k_i} \neq C_j~y_1~\dots~y_{k_j} \qquad |
1545 \item They are distinct: |
1523 \mbox{for all}~ i \neq j. |
1546 \[ |
|
1547 C@i~x@1~\dots~x@{k@i} \neq C@j~y@1~\dots~y@{k@j} \qquad |
|
1548 \mbox{for all}~ i \neq j. |
|
1549 \] |
|
1550 |
|
1551 \item They are injective: |
|
1552 \[ |
|
1553 (C@j~x@1~\dots~x@{k@j} = C@j~y@1~\dots~y@{k@j}) = |
|
1554 (x@1 = y@1 \land \dots \land x@{k@j} = y@{k@j}) |
|
1555 \] |
|
1556 \end{itemize} |
|
1557 Because the number of inequalities is quadratic in the number of |
|
1558 constructors, a different representation is used if there are $7$ or |
|
1559 more of them. In that case every constructor term is mapped to a |
|
1560 natural number: |
|
1561 \[ |
|
1562 t_ord \, (C@i \, x@1 \, \dots \, x@{k@1}) = i - 1 |
1524 \] |
1563 \] |
1525 \item[\tt inject] They are injective: |
1564 Then distinctness of constructor terms is expressed by: |
1526 \[ (C_j~x_1~\dots~x_{k_j} = C_j~y_1~\dots~y_{k_j}) = |
1565 \[ |
1527 (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j}) |
1566 t_ord \, x \neq t_ord \, y \Imp x \neq y. |
1528 \] |
1567 \] |
1529 \end{description} |
1568 |
1530 Because the number of inequalities is quadratic in the number of |
1569 \medskip Furthermore, the following structural induction rule is |
1531 constructors, a different method is used if their number exceeds |
1570 provided: |
1532 a certain value, currently 6. In that case every constructor is mapped to a |
|
1533 natural number |
|
1534 \[ |
1571 \[ |
1535 \begin{array}{lcl} |
1572 \infer{P \, x} |
1536 \mbox{\it t\_ord}(C_1~x_1~\dots~x_{k_1}) & = & 0 \\ |
|
1537 & \vdots & \\ |
|
1538 \mbox{\it t\_ord}(C_m x_1~\dots~x_{k_m}) & = & m-1 |
|
1539 \end{array} |
|
1540 \] |
|
1541 and distinctness of constructors is expressed by: |
|
1542 \[ |
|
1543 \mbox{\it t\_ord}~x \neq \mbox{\it t\_ord}~y \Imp x \neq y. |
|
1544 \] |
|
1545 In addition a structural induction axiom {\tt induct} is provided: |
|
1546 \[ |
|
1547 \infer{P x} |
|
1548 {\begin{array}{lcl} |
1573 {\begin{array}{lcl} |
1549 \Forall x_1\dots x_{k_1}. |
1574 \Forall x@1\dots x@{k@1}. |
1550 \List{P~x_{r_{11}}; \dots; P~x_{r_{1l_1}}} & |
1575 \List{P~x@{r@{11}}; \dots; P~x@{r@{1l@1}}} & |
1551 \Imp & P(C_1~x_1~\dots~x_{k_1}) \\ |
1576 \Imp & P \, (C@1~x@1~\dots~x@{k@1}) \\ |
1552 & \vdots & \\ |
1577 & \vdots & \\ |
1553 \Forall x_1\dots x_{k_m}. |
1578 \Forall x@1\dots x@{k@m}. |
1554 \List{P~x_{r_{m1}}; \dots; P~x_{r_{ml_m}}} & |
1579 \List{P~x@{r@{m1}}; \dots; P~x@{r@{ml@m}}} & |
1555 \Imp & P(C_m~x_1~\dots~x_{k_m}) |
1580 \Imp & P \, (C@m~x@1~\dots~x@{k@m}) |
1556 \end{array}} |
1581 \end{array}} |
1557 \] |
1582 \] |
1558 where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji} |
1583 where $\{r@{j1},\dots,r@{jl@j}\} = \{i \in \{1,\dots k@j\} ~\mid~ \tau@{ji} |
1559 = (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for |
1584 = (\alpha@1,\dots,\alpha@n)t \}$, i.e.\ the property $P$ can be assumed for |
1560 all arguments of the recursive type. |
1585 all arguments of the recursive type. |
1561 |
1586 |
1562 The type also comes with an \ML-like \sdx{case}-construct: |
1587 The type also comes with an \ML-like \sdx{case}-construct: |
1563 \[ |
1588 \[ |
1564 \begin{array}{rrcl} |
1589 \begin{array}{rrcl} |
1565 \mbox{\tt case}~e~\mbox{\tt of} & C_1~x_{11}~\dots~x_{1k_1} & \To & e_1 \\ |
1590 \mbox{\tt case}~e~\mbox{\tt of} & C@1~x@{11}~\dots~x@{1k@1} & \To & e@1 \\ |
1566 \vdots \\ |
1591 \vdots \\ |
1567 \mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m |
1592 \mid & C@m~x@{m1}~\dots~x@{mk@m} & \To & e@m |
1568 \end{array} |
1593 \end{array} |
1569 \] |
1594 \] |
1570 where the $x_{ij}$ are either identifiers or nested tuple patterns as in |
1595 where the $x@{ij}$ are either identifiers or nested tuple patterns as in |
1571 \S\ref{subsec:prod-sum}. |
1596 \S\ref{subsec:prod-sum}. |
1572 \begin{warn} |
1597 \begin{warn} |
1573 In contrast to \ML, {\em all} constructors must be present, their order is |
1598 In contrast to \ML, {\em all} constructors must be present, their order is |
1574 fixed, and nested patterns are not supported (with the exception of tuples). |
1599 fixed, and nested patterns are not supported (with the exception of tuples). |
1575 Violating this restriction results in strange error messages. |
1600 Violating this restriction results in strange error messages. |
1576 \end{warn} |
1601 \end{warn} |
1577 |
1602 |
1578 \underscoreoff |
|
1579 |
1603 |
1580 \subsection{Defining datatypes} |
1604 \subsection{Defining datatypes} |
1581 |
1605 |
1582 A datatype is defined in a theory definition file using the keyword {\tt |
1606 A datatype is defined in a theory definition file using the keyword |
1583 datatype}. The definition following {\tt datatype} must conform to the |
1607 {\tt datatype}. The definition following this must conform to the |
1584 syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and must |
1608 syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and |
1585 obey the rules in the previous section. As a result the theory is extended |
1609 must obey the rules in the previous section. As a result the theory is |
1586 with the new type, the constructors, and the theorems listed in the previous |
1610 extended with the new type, the constructors, and the theorems listed |
1587 section. |
1611 in the previous section. |
1588 |
1612 |
1589 \begin{figure} |
1613 \begin{figure} |
1590 \begin{rail} |
1614 \begin{rail} |
1591 typedecl : typevarlist id '=' (cons + '|') |
1615 typedecl : typevarlist id '=' (cons + '|') |
1592 ; |
1616 ; |
1613 applies structural induction on variable $x$ to subgoal $i$, provided the |
1638 applies structural induction on variable $x$ to subgoal $i$, provided the |
1614 type of $x$ is a datatype or type {\tt nat}. |
1639 type of $x$ is a datatype or type {\tt nat}. |
1615 \end{ttdescription} |
1640 \end{ttdescription} |
1616 |
1641 |
1617 For the technically minded, we give a more detailed description. |
1642 For the technically minded, we give a more detailed description. |
1618 Reading the theory file produces a structure which, in addition to the usual |
1643 Reading the theory file produces a structure which, in addition to the |
1619 components, contains a structure named $t$ for each datatype $t$ defined in |
1644 usual components, contains a structure named $t$ for each datatype $t$ |
1620 the file.\footnote{Otherwise multiple datatypes in the same theory file would |
1645 defined in the file. Each structure $t$ contains the following |
1621 lead to name clashes.} Each structure $t$ contains the following elements: |
1646 elements: |
1622 \begin{ttbox} |
1647 \begin{ttbox} |
1623 val distinct : thm list |
1648 val distinct : thm list |
1624 val inject : thm list |
1649 val inject : thm list |
1625 val induct : thm |
1650 val induct : thm |
1626 val cases : thm list |
1651 val cases : thm list |
1627 val simps : thm list |
1652 val simps : thm list |
1628 val induct_tac : string -> int -> tactic |
1653 val induct_tac : string -> int -> tactic |
1629 \end{ttbox} |
1654 \end{ttbox} |
1630 {\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described |
1655 {\tt distinct}, {\tt inject} and {\tt induct} contain the theorems |
1631 above. For convenience {\tt distinct} contains inequalities in both |
1656 described above. For user convenience, {\tt distinct} contains |
1632 directions. The reduction rules of the {\tt case}-construct are in {\tt |
1657 inequalities in both directions. The reduction rules of the {\tt |
1633 cases}. All theorems from {\tt distinct}, {\tt inject} and {\tt cases} are |
1658 case}-construct are in {\tt cases}. All theorems from {\tt |
1634 combined in {\tt simps}. |
1659 distinct}, {\tt inject} and {\tt cases} are combined in {\tt simps}. |
1635 |
1660 |
1636 \subsection{Examples} |
1661 \subsection{Examples} |
1637 |
1662 |
1638 \subsubsection{The datatype $\alpha~list$} |
1663 \subsubsection{The datatype $\alpha~list$} |
1639 |
1664 |
1640 We want to define the type $\alpha~list$.\footnote{Of course there is a list |
1665 We want to define the type $\alpha~list$.\footnote{This is just an |
1641 type in HOL already. This is only an example.} To do this we have to build |
1666 example. There is already a list type in \HOL, of course.} To do |
1642 a new theory that contains the type definition. We start from {\tt HOL}. |
1667 this we have to build a new theory that contains the type definition. |
|
1668 We start from the basic {\tt HOL} theory. |
1643 \begin{ttbox} |
1669 \begin{ttbox} |
1644 MyList = HOL + |
1670 MyList = HOL + |
1645 datatype 'a list = Nil | Cons 'a ('a list) |
1671 datatype 'a list = Nil | Cons 'a ('a list) |
1646 end |
1672 end |
1647 \end{ttbox} |
1673 \end{ttbox} |
1757 example |
1787 example |
1758 \begin{ttbox} |
1788 \begin{ttbox} |
1759 primrec app MyList.list |
1789 primrec app MyList.list |
1760 "app [] ys = us" |
1790 "app [] ys = us" |
1761 \end{ttbox} |
1791 \end{ttbox} |
1762 is rejected: |
1792 is rejected with an error message \texttt{Extra variables on rhs}. |
1763 \begin{ttbox} |
1793 |
1764 Extra variables on rhs |
|
1765 \end{ttbox} |
|
1766 \bigskip |
1794 \bigskip |
1767 |
1795 |
1768 The general form of a primitive recursive definition is |
1796 The general form of a primitive recursive definition is |
1769 \begin{ttbox} |
1797 \begin{ttbox} |
1770 primrec {\it function} {\it type} |
1798 primrec {\it function} {\it type} |
1771 {\it reduction rules} |
1799 {\it reduction rules} |
1772 \end{ttbox} |
1800 \end{ttbox} |
1773 where |
1801 where |
1774 \begin{itemize} |
1802 \begin{itemize} |
1775 \item {\it function} is the name of the function, either as an {\it id} or a |
1803 \item {\it function} is the name of the function, either as an {\it id} or a |
1776 {\it string}. The function must already have been declared. |
1804 {\it string}. The function must already have been declared as a constant. |
1777 \item {\it type} is the name of the datatype, either as an {\it id} or in the |
1805 \item {\it type} is the name of the datatype, either as an {\it id} or |
1778 long form {\it Thy.t}, where {\it Thy} is the name of the parent theory the |
1806 in the long form \texttt{$T$.$t$} ($T$ is the name of the theory |
1779 datatype was declared in, and $t$ the name of the datatype. The long form |
1807 where the datatype has been declared, $t$ the name of the datatype). |
1780 is required if the {\tt datatype} and the {\tt primrec} sections are in |
1808 The long form is required if the {\tt datatype} and the {\tt |
1781 different theories. |
1809 primrec} sections are in different theories. |
1782 \item {\it reduction rules} specify one or more equations of the form \[ |
1810 \item {\it reduction rules} specify one or more equations of the form |
1783 f~x@1~\dots~x@m~(C~y@1~\dots~y@k)~z@1~\dots~z@n = r \] such that $C$ is a |
1811 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \, |
1784 constructor of the datatype, $r$ contains only the free variables on the |
1812 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, |
1785 left-hand side, and all recursive calls in $r$ are of the form |
1813 $r$ contains only the free variables on the left-hand side, and all |
1786 $f~\dots~y@i~\dots$ for some $i$. There must be exactly one reduction rule |
1814 recursive calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ |
1787 for each constructor. The order is immaterial. {\em All reduction rules are |
1815 for some $i$. There must be exactly one reduction rule for each |
1788 added to the default {\tt simpset}.} |
1816 constructor. The order is immaterial. Also note that all reduction |
1789 |
1817 rules are added to the default simpset! |
1790 If you would like to refer to some rule explicitly, you have to prefix each |
1818 |
1791 rule with an identifier (like in the {\tt rules} section of the first {\tt |
1819 If you would like to refer to some rule explicitly, you have to prefix |
1792 Append} theory above) that will serve as the name of the corresponding |
1820 each rule with an identifier (like in the {\tt rules} section of the |
1793 theorem at the \ML\ level. |
1821 axiomatic {\tt Append} theory above) that will serve as the name of |
|
1822 the corresponding theorem at the \ML\ level. |
1794 \end{itemize} |
1823 \end{itemize} |
1795 A theory file may contain any number of {\tt primrec} sections which may be |
1824 A theory file may contain any number of {\tt primrec} sections which may be |
1796 intermixed with other declarations. |
1825 intermixed with other declarations. |
1797 |
|
1798 For the consistency-conscious user it may be reassuring to know that {\tt |
|
1799 primrec} does not assert the reduction rules as new axioms but derives them |
|
1800 as theorems from an explicit definition of the recursive function in terms of |
|
1801 a recursion operator on the datatype. |
|
1802 |
1826 |
1803 The primitive recursive function can have infix or mixfix syntax: |
1827 The primitive recursive function can have infix or mixfix syntax: |
1804 \begin{ttbox}\underscoreon |
1828 \begin{ttbox}\underscoreon |
1805 Append = MyList + |
1829 Append = MyList + |
1806 consts "@" :: ['a list,'a list] => 'a list (infixr 60) |
1830 consts "@" :: ['a list,'a list] => 'a list (infixr 60) |
1972 inductively, with two introduction rules: |
2002 inductively, with two introduction rules: |
1973 \begin{ttbox} |
2003 \begin{ttbox} |
1974 consts Fin :: 'a set => 'a set set |
2004 consts Fin :: 'a set => 'a set set |
1975 inductive "Fin A" |
2005 inductive "Fin A" |
1976 intrs |
2006 intrs |
1977 emptyI "\{\} : Fin A" |
2007 emptyI "{\ttlbrace}{\ttrbrace} : Fin A" |
1978 insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A" |
2008 insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A" |
1979 \end{ttbox} |
2009 \end{ttbox} |
1980 The resulting theory structure contains a substructure, called~{\tt Fin}. |
2010 The resulting theory structure contains a substructure, called~{\tt Fin}. |
1981 It contains the {\tt Fin}$~A$ introduction rules as the list {\tt Fin.intrs}, |
2011 It contains the {\tt Fin}$~A$ introduction rules as the list {\tt Fin.intrs}, |
1982 and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction |
2012 and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction |
1983 rule is {\tt Fin.induct}. |
2013 rule is {\tt Fin.induct}. |
1984 |
2014 |
1985 For another example, here is a theory file defining the accessible part of a |
2015 For another example, here is a theory file defining the accessible |
1986 relation. The main thing to note is the use of~{\tt Pow} in the sole |
2016 part of a relation. The main thing to note is the use of~{\tt Pow} in |
1987 introduction rule, and the corresponding mention of the rule |
2017 the sole introduction rule, and the corresponding mention of the rule |
1988 \verb|Pow_mono| in the {\tt monos} list. The paper discusses a ZF version |
2018 \verb|Pow_mono| in the {\tt monos} list. The paper |
1989 of this example in more detail. |
2019 \cite{paulson-CADE} discusses a \ZF\ version of this example in more |
|
2020 detail. |
1990 \begin{ttbox} |
2021 \begin{ttbox} |
1991 Acc = WF + |
2022 Acc = WF + |
1992 consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) |
2023 consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) |
1993 acc :: "('a * 'a)set => 'a set" (*Accessible part*) |
2024 acc :: "('a * 'a)set => 'a set" (*Accessible part*) |
1994 defs pred_def "pred x r == {y. (y,x):r}" |
2025 defs pred_def "pred x r == {y. (y,x):r}" |
2118 |
2149 |
2119 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and |
2150 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and |
2120 the operator \cdx{range}. The set~$S$ is given as an unknown instead of a |
2151 the operator \cdx{range}. The set~$S$ is given as an unknown instead of a |
2121 quantified variable so that we may inspect the subset found by the proof. |
2152 quantified variable so that we may inspect the subset found by the proof. |
2122 \begin{ttbox} |
2153 \begin{ttbox} |
2123 goal Set.thy "~ ?S : range(f :: 'a=>'a set)"; |
2154 goal Set.thy "?S ~: range\thinspace(f :: 'a=>'a set)"; |
2124 {\out Level 0} |
2155 {\out Level 0} |
2125 {\out ~ ?S : range f} |
2156 {\out ?S ~: range f} |
2126 {\out 1. ~ ?S : range f} |
2157 {\out 1. ?S ~: range f} |
2127 \end{ttbox} |
2158 \end{ttbox} |
2128 The first two steps are routine. The rule \tdx{rangeE} replaces |
2159 The first two steps are routine. The rule \tdx{rangeE} replaces |
2129 $\Var{S}\in {\tt range} f$ by $\Var{S}=f~x$ for some~$x$. |
2160 $\Var{S}\in {\tt range} \, f$ by $\Var{S}=f~x$ for some~$x$. |
2130 \begin{ttbox} |
2161 \begin{ttbox} |
2131 by (resolve_tac [notI] 1); |
2162 by (resolve_tac [notI] 1); |
2132 {\out Level 1} |
2163 {\out Level 1} |
2133 {\out ~ ?S : range f} |
2164 {\out ?S ~: range f} |
2134 {\out 1. ?S : range f ==> False} |
2165 {\out 1. ?S : range f ==> False} |
2135 \ttbreak |
2166 \ttbreak |
2136 by (eresolve_tac [rangeE] 1); |
2167 by (eresolve_tac [rangeE] 1); |
2137 {\out Level 2} |
2168 {\out Level 2} |
2138 {\out ~ ?S : range f} |
2169 {\out ?S ~: range f} |
2139 {\out 1. !!x. ?S = f x ==> False} |
2170 {\out 1. !!x. ?S = f x ==> False} |
2140 \end{ttbox} |
2171 \end{ttbox} |
2141 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$, |
2172 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$, |
2142 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for |
2173 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for |
2143 any~$\Var{c}$. |
2174 any~$\Var{c}$. |
2144 \begin{ttbox} |
2175 \begin{ttbox} |
2145 by (eresolve_tac [equalityCE] 1); |
2176 by (eresolve_tac [equalityCE] 1); |
2146 {\out Level 3} |
2177 {\out Level 3} |
2147 {\out ~ ?S : range f} |
2178 {\out ?S ~: range f} |
2148 {\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False} |
2179 {\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False} |
2149 {\out 2. !!x. [| ~ ?c3 x : ?S; ~ ?c3 x : f x |] ==> False} |
2180 {\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False} |
2150 \end{ttbox} |
2181 \end{ttbox} |
2151 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a |
2182 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a |
2152 comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies |
2183 comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies |
2153 $\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD} |
2184 $\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD} |
2154 instantiates~$\Var{S}$ and creates the new assumption. |
2185 instantiates~$\Var{S}$ and creates the new assumption. |
2155 \begin{ttbox} |
2186 \begin{ttbox} |
2156 by (dresolve_tac [CollectD] 1); |
2187 by (dresolve_tac [CollectD] 1); |
2157 {\out Level 4} |
2188 {\out Level 4} |
2158 {\out ~ \{x. ?P7 x\} : range f} |
2189 {\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f} |
2159 {\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False} |
2190 {\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False} |
2160 {\out 2. !!x. [| ~ ?c3 x : \{x. ?P7 x\}; ~ ?c3 x : f x |] ==> False} |
2191 {\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False} |
2161 \end{ttbox} |
2192 \end{ttbox} |
2162 Forcing a contradiction between the two assumptions of subgoal~1 completes |
2193 Forcing a contradiction between the two assumptions of subgoal~1 |
2163 the instantiation of~$S$. It is now the set $\{x. x\not\in f~x\}$, which |
2194 completes the instantiation of~$S$. It is now the set $\{x. x\not\in |
2164 is the standard diagonal construction. |
2195 f~x\}$, which is the standard diagonal construction. |
2165 \begin{ttbox} |
2196 \begin{ttbox} |
2166 by (contr_tac 1); |
2197 by (contr_tac 1); |
2167 {\out Level 5} |
2198 {\out Level 5} |
2168 {\out ~ \{x. ~ x : f x\} : range f} |
2199 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} |
2169 {\out 1. !!x. [| ~ x : \{x. ~ x : f x\}; ~ x : f x |] ==> False} |
2200 {\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False} |
2170 \end{ttbox} |
2201 \end{ttbox} |
2171 The rest should be easy. To apply \tdx{CollectI} to the negated |
2202 The rest should be easy. To apply \tdx{CollectI} to the negated |
2172 assumption, we employ \ttindex{swap_res_tac}: |
2203 assumption, we employ \ttindex{swap_res_tac}: |
2173 \begin{ttbox} |
2204 \begin{ttbox} |
2174 by (swap_res_tac [CollectI] 1); |
2205 by (swap_res_tac [CollectI] 1); |
2175 {\out Level 6} |
2206 {\out Level 6} |
2176 {\out ~ \{x. ~ x : f x\} : range f} |
2207 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} |
2177 {\out 1. !!x. [| ~ x : f x; ~ False |] ==> ~ x : f x} |
2208 {\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x} |
2178 \ttbreak |
2209 \ttbreak |
2179 by (assume_tac 1); |
2210 by (assume_tac 1); |
2180 {\out Level 7} |
2211 {\out Level 7} |
2181 {\out ~ \{x. ~ x : f x\} : range f} |
2212 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} |
2182 {\out No subgoals!} |
2213 {\out No subgoals!} |
2183 \end{ttbox} |
2214 \end{ttbox} |
2184 How much creativity is required? As it happens, Isabelle can prove this |
2215 How much creativity is required? As it happens, Isabelle can prove this |
2185 theorem automatically. The default classical set {\tt!claset} contains rules |
2216 theorem automatically. The default classical set {\tt!claset} contains rules |
2186 for most of the constructs of \HOL's set theory. We must augment it with |
2217 for most of the constructs of \HOL's set theory. We must augment it with |