32 "m + n \\<equiv> rec(m, n, \\<lambda>x y. Suc(y))"; |
32 "m + n \\<equiv> rec(m, n, \\<lambda>x y. Suc(y))"; |
33 |
33 |
34 text {* |
34 text {* |
35 This is an abstract version of the plain $Nat$ theory in |
35 This is an abstract version of the plain $Nat$ theory in |
36 FOL.\footnote{See |
36 FOL.\footnote{See |
37 \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} |
37 \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically, |
|
38 we have just replaced all occurrences of type $nat$ by $\alpha$ and |
|
39 used the natural number axioms to define class $nat$. There is only |
|
40 a minor snag, that the original recursion operator $rec$ had to be |
|
41 made monomorphic. |
38 |
42 |
39 Basically, we have just replaced all occurrences of type $nat$ by |
43 Thus class $nat$ contains exactly those types $\tau$ that are |
40 $\alpha$ and used the natural number axioms to define class $nat$. |
44 isomorphic to ``the'' natural numbers (with signature $0$, $Suc$, |
41 There is only a minor snag, that the original recursion operator |
45 $rec$). |
42 $rec$ had to be made monomorphic, in a sense. Thus class $nat$ |
|
43 contains exactly those types $\tau$ that are isomorphic to ``the'' |
|
44 natural numbers (with signature $0$, $Suc$, $rec$). |
|
45 |
46 |
46 \medskip What we have done here can be also viewed as \emph{type |
47 \medskip What we have done here can be also viewed as \emph{type |
47 specification}. Of course, it still remains open if there is some |
48 specification}. Of course, it still remains open if there is some |
48 type at all that meets the class axioms. Now a very nice property of |
49 type at all that meets the class axioms. Now a very nice property of |
49 axiomatic type classes is, that abstract reasoning is always possible |
50 axiomatic type classes is that abstract reasoning is always possible |
50 --- independent of satisfiability. The meta-logic won't break, even |
51 --- independent of satisfiability. The meta-logic won't break, even |
51 if some classes (or general sorts) turns out to be empty |
52 if some classes (or general sorts) turns out to be empty later --- |
52 (``inconsistent'') later. |
53 ``inconsistent'' class definitions may be useless, but do not cause |
|
54 any harm. |
53 |
55 |
54 Theorems of the abstract natural numbers may be derived in the same |
56 Theorems of the abstract natural numbers may be derived in the same |
55 way as for the concrete version. The original proof scripts may be |
57 way as for the concrete version. The original proof scripts may be |
56 used with some trivial changes only (mostly adding some type |
58 re-used with some trivial changes only (mostly adding some type |
57 constraints). |
59 constraints). |
58 *}; |
60 *}; |
59 |
61 |
60 end; |
62 end; |