17128
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{NatClass}%
|
17181
|
4 |
\isamarkupfalse%
|
17128
|
5 |
%
|
|
6 |
\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}%
|
|
7 |
}
|
17175
|
8 |
\isamarkuptrue%
|
17128
|
9 |
%
|
|
10 |
\isadelimtheory
|
|
11 |
%
|
|
12 |
\endisadelimtheory
|
|
13 |
%
|
|
14 |
\isatagtheory
|
17175
|
15 |
\isacommand{theory}\isamarkupfalse%
|
|
16 |
\ NatClass\ \isakeyword{imports}\ FOL\ \isakeyword{begin}%
|
17128
|
17 |
\endisatagtheory
|
|
18 |
{\isafoldtheory}%
|
|
19 |
%
|
|
20 |
\isadelimtheory
|
|
21 |
%
|
|
22 |
\endisadelimtheory
|
|
23 |
%
|
|
24 |
\begin{isamarkuptext}%
|
|
25 |
\medskip\noindent Axiomatic type classes abstract over exactly one
|
|
26 |
type argument. Thus, any \emph{axiomatic} theory extension where each
|
|
27 |
axiom refers to at most one type variable, may be trivially turned
|
|
28 |
into a \emph{definitional} one.
|
|
29 |
|
|
30 |
We illustrate this with the natural numbers in
|
|
31 |
Isabelle/FOL.\footnote{See also
|
|
32 |
\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
|
|
33 |
\end{isamarkuptext}%
|
17175
|
34 |
\isamarkuptrue%
|
|
35 |
\isacommand{consts}\isamarkupfalse%
|
|
36 |
\isanewline
|
|
37 |
\ \ zero\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymzero}{\isachardoublequoteclose}{\isacharparenright}\isanewline
|
|
38 |
\ \ Suc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
|
|
39 |
\ \ rec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
|
17128
|
40 |
\isanewline
|
17175
|
41 |
\isacommand{axclass}\isamarkupfalse%
|
|
42 |
\ nat\ {\isasymsubseteq}\ {\isachardoublequoteopen}term{\isachardoublequoteclose}\isanewline
|
|
43 |
\ \ induct{\isacharcolon}\ {\isachardoublequoteopen}P{\isacharparenleft}{\isasymzero}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}Suc{\isacharparenleft}x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}n{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
|
44 |
\ \ Suc{\isacharunderscore}inject{\isacharcolon}\ {\isachardoublequoteopen}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
|
|
45 |
\ \ Suc{\isacharunderscore}neq{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequoteopen}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ {\isasymzero}\ {\isasymLongrightarrow}\ R{\isachardoublequoteclose}\isanewline
|
|
46 |
\ \ rec{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequoteopen}rec{\isacharparenleft}{\isasymzero}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ a{\isachardoublequoteclose}\isanewline
|
|
47 |
\ \ rec{\isacharunderscore}Suc{\isacharcolon}\ {\isachardoublequoteopen}rec{\isacharparenleft}Suc{\isacharparenleft}m{\isacharparenright}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}m{\isacharcomma}\ rec{\isacharparenleft}m{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
17128
|
48 |
\isanewline
|
17175
|
49 |
\isacommand{constdefs}\isamarkupfalse%
|
|
50 |
\isanewline
|
|
51 |
\ \ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
|
|
52 |
\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ n\ {\isasymequiv}\ rec{\isacharparenleft}m{\isacharcomma}\ n{\isacharcomma}\ {\isasymlambda}x\ y{\isachardot}\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
|
17128
|
53 |
\begin{isamarkuptext}%
|
|
54 |
This is an abstract version of the plain \isa{Nat} theory in
|
|
55 |
FOL.\footnote{See
|
|
56 |
\url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
|
|
57 |
we have just replaced all occurrences of type \isa{nat} by \isa{{\isacharprime}a} and used the natural number axioms to define class \isa{nat}.
|
|
58 |
There is only a minor snag, that the original recursion operator
|
|
59 |
\isa{rec} had to be made monomorphic.
|
|
60 |
|
|
61 |
Thus class \isa{nat} contains exactly those types \isa{{\isasymtau}} that
|
|
62 |
are isomorphic to ``the'' natural numbers (with signature \isa{{\isasymzero}}, \isa{Suc}, \isa{rec}).
|
|
63 |
|
|
64 |
\medskip What we have done here can be also viewed as \emph{type
|
|
65 |
specification}. Of course, it still remains open if there is some
|
|
66 |
type at all that meets the class axioms. Now a very nice property of
|
|
67 |
axiomatic type classes is that abstract reasoning is always possible
|
|
68 |
--- independent of satisfiability. The meta-logic won't break, even
|
|
69 |
if some classes (or general sorts) turns out to be empty later ---
|
|
70 |
``inconsistent'' class definitions may be useless, but do not cause
|
|
71 |
any harm.
|
|
72 |
|
|
73 |
Theorems of the abstract natural numbers may be derived in the same
|
|
74 |
way as for the concrete version. The original proof scripts may be
|
|
75 |
re-used with some trivial changes only (mostly adding some type
|
|
76 |
constraints).%
|
|
77 |
\end{isamarkuptext}%
|
17175
|
78 |
\isamarkuptrue%
|
17128
|
79 |
%
|
|
80 |
\isadelimtheory
|
|
81 |
%
|
|
82 |
\endisadelimtheory
|
|
83 |
%
|
|
84 |
\isatagtheory
|
17175
|
85 |
\isacommand{end}\isamarkupfalse%
|
|
86 |
%
|
17128
|
87 |
\endisatagtheory
|
|
88 |
{\isafoldtheory}%
|
|
89 |
%
|
|
90 |
\isadelimtheory
|
|
91 |
%
|
|
92 |
\endisadelimtheory
|
|
93 |
\end{isabellebody}%
|
|
94 |
%%% Local Variables:
|
|
95 |
%%% mode: latex
|
|
96 |
%%% TeX-master: "root"
|
|
97 |
%%% End:
|