13 Isabelle/FOL.\footnote{See also |
13 Isabelle/FOL.\footnote{See also |
14 \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}} |
14 \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}} |
15 *} |
15 *} |
16 |
16 |
17 consts |
17 consts |
18 zero :: 'a ("0") |
18 zero :: 'a ("\<zero>") |
19 Suc :: "'a \\<Rightarrow> 'a" |
19 Suc :: "'a \<Rightarrow> 'a" |
20 rec :: "'a \\<Rightarrow> 'a \\<Rightarrow> ('a \\<Rightarrow> 'a \\<Rightarrow> 'a) \\<Rightarrow> 'a" |
20 rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a" |
21 |
21 |
22 axclass |
22 axclass nat < "term" |
23 nat < "term" |
23 induct: "P(\<zero>) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)" |
24 induct: "P(0) \\<Longrightarrow> (\\<And>x. P(x) \\<Longrightarrow> P(Suc(x))) \\<Longrightarrow> P(n)" |
24 Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n" |
25 Suc_inject: "Suc(m) = Suc(n) \\<Longrightarrow> m = n" |
25 Suc_neq_0: "Suc(m) = \<zero> \<Longrightarrow> R" |
26 Suc_neq_0: "Suc(m) = 0 \\<Longrightarrow> R" |
26 rec_0: "rec(\<zero>, a, f) = a" |
27 rec_0: "rec(0, a, f) = a" |
27 rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" |
28 rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" |
|
29 |
28 |
30 constdefs |
29 constdefs |
31 add :: "'a::nat \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "+" 60) |
30 add :: "'a::nat \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 60) |
32 "m + n \\<equiv> rec(m, n, \\<lambda>x y. Suc(y))" |
31 "m + n \<equiv> rec(m, n, \<lambda>x y. Suc(y))" |
33 |
32 |
34 text {* |
33 text {* |
35 This is an abstract version of the plain $Nat$ theory in |
34 This is an abstract version of the plain @{text Nat} theory in |
36 FOL.\footnote{See |
35 FOL.\footnote{See |
37 \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically, |
36 \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 |
37 we have just replaced all occurrences of type @{text nat} by @{typ |
39 used the natural number axioms to define class $nat$. There is only |
38 'a} and used the natural number axioms to define class @{text nat}. |
40 a minor snag, that the original recursion operator $rec$ had to be |
39 There is only a minor snag, that the original recursion operator |
41 made monomorphic. |
40 @{term rec} had to be made monomorphic. |
42 |
41 |
43 Thus class $nat$ contains exactly those types $\tau$ that are |
42 Thus class @{text nat} contains exactly those types @{text \<tau>} that |
44 isomorphic to ``the'' natural numbers (with signature $0$, $Suc$, |
43 are isomorphic to ``the'' natural numbers (with signature @{term |
45 $rec$). |
44 \<zero>}, @{term Suc}, @{term rec}). |
46 |
45 |
47 \medskip What we have done here can be also viewed as \emph{type |
46 \medskip What we have done here can be also viewed as \emph{type |
48 specification}. Of course, it still remains open if there is some |
47 specification}. Of course, it still remains open if there is some |
49 type at all that meets the class axioms. Now a very nice property of |
48 type at all that meets the class axioms. Now a very nice property of |
50 axiomatic type classes is that abstract reasoning is always possible |
49 axiomatic type classes is that abstract reasoning is always possible |