8890
|
1 |
\begin{isabelle}%
|
8906
|
2 |
%
|
|
3 |
\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}}
|
|
4 |
\isacommand{theory}~NatClass~=~FOL:%
|
|
5 |
\begin{isamarkuptext}%
|
|
6 |
\medskip\noindent Axiomatic type classes abstract over exactly one
|
|
7 |
type argument. Thus, any \emph{axiomatic} theory extension where each
|
|
8 |
axiom refers to at most one type variable, may be trivially turned
|
|
9 |
into a \emph{definitional} one.
|
|
10 |
|
|
11 |
We illustrate this with the natural numbers in
|
|
12 |
Isabelle/FOL.\footnote{See also
|
|
13 |
\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
|
|
14 |
\end{isamarkuptext}%
|
8890
|
15 |
\isacommand{consts}\isanewline
|
|
16 |
~~zero~::~'a~~~~({"}0{"})\isanewline
|
|
17 |
~~Suc~::~{"}'a~{\isasymRightarrow}~'a{"}\isanewline
|
|
18 |
~~rec~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~'a{"}\isanewline
|
|
19 |
\isanewline
|
|
20 |
\isacommand{axclass}\isanewline
|
|
21 |
~~nat~<~{"}term{"}\isanewline
|
|
22 |
~~induct:~~~~~{"}P(0)~{\isasymLongrightarrow}~({\isasymAnd}x.~P(x)~{\isasymLongrightarrow}~P(Suc(x)))~{\isasymLongrightarrow}~P(n){"}\isanewline
|
|
23 |
~~Suc\_inject:~{"}Suc(m)~=~Suc(n)~{\isasymLongrightarrow}~m~=~n{"}\isanewline
|
|
24 |
~~Suc\_neq\_0:~~{"}Suc(m)~=~0~{\isasymLongrightarrow}~R{"}\isanewline
|
|
25 |
~~rec\_0:~~~~~~{"}rec(0,~a,~f)~=~a{"}\isanewline
|
|
26 |
~~rec\_Suc:~~~~{"}rec(Suc(m),~a,~f)~=~f(m,~rec(m,~a,~f)){"}\isanewline
|
|
27 |
\isanewline
|
|
28 |
\isacommand{constdefs}\isanewline
|
|
29 |
~~add~::~{"}'a::nat~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}+{"}~60)\isanewline
|
8906
|
30 |
~~{"}m~+~n~{\isasymequiv}~rec(m,~n,~{\isasymlambda}x~y.~Suc(y)){"}%
|
|
31 |
\begin{isamarkuptext}%
|
|
32 |
This is an abstract version of the plain $Nat$ theory in
|
|
33 |
FOL.\footnote{See
|
|
34 |
\url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
|
|
35 |
|
|
36 |
Basically, we have just replaced all occurrences of type $nat$ by
|
|
37 |
$\alpha$ and used the natural number axioms to define class $nat$.
|
|
38 |
There is only a minor snag, that the original recursion operator
|
|
39 |
$rec$ had to be made monomorphic, in a sense. Thus class $nat$
|
|
40 |
contains exactly those types $\tau$ that are isomorphic to ``the''
|
|
41 |
natural numbers (with signature $0$, $Suc$, $rec$).
|
|
42 |
|
|
43 |
\medskip What we have done here can be also viewed as \emph{type
|
|
44 |
specification}. Of course, it still remains open if there is some
|
|
45 |
type at all that meets the class axioms. Now a very nice property of
|
|
46 |
axiomatic type classes is, that abstract reasoning is always possible
|
|
47 |
--- independent of satisfiability. The meta-logic won't break, even
|
|
48 |
if some classes (or general sorts) turns out to be empty
|
|
49 |
(``inconsistent'') later.
|
|
50 |
|
|
51 |
Theorems of the abstract natural numbers may be derived in the same
|
|
52 |
way as for the concrete version. The original proof scripts may be
|
|
53 |
used with some trivial changes only (mostly adding some type
|
|
54 |
constraints).%
|
|
55 |
\end{isamarkuptext}%
|
8890
|
56 |
\isacommand{end}\end{isabelle}%
|