|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{NatClass}% |
|
4 \isamarkuptrue% |
|
5 % |
|
6 \isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}% |
|
7 } |
|
8 % |
|
9 \isadelimtheory |
|
10 % |
|
11 \endisadelimtheory |
|
12 % |
|
13 \isatagtheory |
|
14 \isamarkupfalse% |
|
15 \isacommand{theory}\ NatClass\ \isakeyword{imports}\ FOL\ \isakeyword{begin}% |
|
16 \endisatagtheory |
|
17 {\isafoldtheory}% |
|
18 % |
|
19 \isadelimtheory |
|
20 % |
|
21 \endisadelimtheory |
|
22 \isamarkuptrue% |
|
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}% |
|
34 \isamarkupfalse% |
|
35 \isacommand{consts}\isanewline |
|
36 \ \ zero\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymzero}{\isachardoublequote}{\isacharparenright}\isanewline |
|
37 \ \ Suc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline |
|
38 \ \ rec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline |
|
39 \isanewline |
|
40 \isamarkupfalse% |
|
41 \isacommand{axclass}\ nat\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
|
42 \ \ induct{\isacharcolon}\ {\isachardoublequote}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}{\isachardoublequote}\isanewline |
|
43 \ \ Suc{\isacharunderscore}inject{\isacharcolon}\ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline |
|
44 \ \ Suc{\isacharunderscore}neq{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ {\isasymzero}\ {\isasymLongrightarrow}\ R{\isachardoublequote}\isanewline |
|
45 \ \ rec{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequote}rec{\isacharparenleft}{\isasymzero}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ a{\isachardoublequote}\isanewline |
|
46 \ \ rec{\isacharunderscore}Suc{\isacharcolon}\ {\isachardoublequote}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}{\isachardoublequote}\isanewline |
|
47 \isanewline |
|
48 \isamarkupfalse% |
|
49 \isacommand{constdefs}\isanewline |
|
50 \ \ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline |
|
51 \ \ {\isachardoublequote}m\ {\isacharplus}\ n\ {\isasymequiv}\ rec{\isacharparenleft}m{\isacharcomma}\ n{\isacharcomma}\ {\isasymlambda}x\ y{\isachardot}\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
|
52 % |
|
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}% |
|
78 % |
|
79 \isadelimtheory |
|
80 % |
|
81 \endisadelimtheory |
|
82 % |
|
83 \isatagtheory |
|
84 \isamarkupfalse% |
|
85 \isacommand{end}% |
|
86 \endisatagtheory |
|
87 {\isafoldtheory}% |
|
88 % |
|
89 \isadelimtheory |
|
90 % |
|
91 \endisadelimtheory |
|
92 \end{isabellebody}% |
|
93 %%% Local Variables: |
|
94 %%% mode: latex |
|
95 %%% TeX-master: "root" |
|
96 %%% End: |