1 |
|
2 header {* Defining natural numbers in FOL \label{sec:ex-natclass} *} |
|
3 |
|
4 theory NatClass imports FOL begin |
|
5 |
|
6 text {* |
|
7 \medskip\noindent Axiomatic type classes abstract over exactly one |
|
8 type argument. Thus, any \emph{axiomatic} theory extension where each |
|
9 axiom refers to at most one type variable, may be trivially turned |
|
10 into a \emph{definitional} one. |
|
11 |
|
12 We illustrate this with the natural numbers in |
|
13 Isabelle/FOL.\footnote{See also |
|
14 \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}} |
|
15 *} |
|
16 |
|
17 consts |
|
18 zero :: 'a ("\<zero>") |
|
19 Suc :: "'a \<Rightarrow> 'a" |
|
20 rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a" |
|
21 |
|
22 axclass nat \<subseteq> "term" |
|
23 induct: "P(\<zero>) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)" |
|
24 Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n" |
|
25 Suc_neq_0: "Suc(m) = \<zero> \<Longrightarrow> R" |
|
26 rec_0: "rec(\<zero>, a, f) = a" |
|
27 rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" |
|
28 |
|
29 constdefs |
|
30 add :: "'a::nat \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 60) |
|
31 "m + n \<equiv> rec(m, n, \<lambda>x y. Suc(y))" |
|
32 |
|
33 text {* |
|
34 This is an abstract version of the plain @{text Nat} theory in |
|
35 FOL.\footnote{See |
|
36 \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically, |
|
37 we have just replaced all occurrences of type @{text nat} by @{typ |
|
38 'a} and used the natural number axioms to define class @{text nat}. |
|
39 There is only a minor snag, that the original recursion operator |
|
40 @{term rec} had to be made monomorphic. |
|
41 |
|
42 Thus class @{text nat} contains exactly those types @{text \<tau>} that |
|
43 are isomorphic to ``the'' natural numbers (with signature @{term |
|
44 \<zero>}, @{term Suc}, @{term rec}). |
|
45 |
|
46 \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 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 --- independent of satisfiability. The meta-logic won't break, even |
|
51 if some classes (or general sorts) turns out to be empty later --- |
|
52 ``inconsistent'' class definitions may be useless, but do not cause |
|
53 any harm. |
|
54 |
|
55 Theorems of the abstract natural numbers may be derived in the same |
|
56 way as for the concrete version. The original proof scripts may be |
|
57 re-used with some trivial changes only (mostly adding some type |
|
58 constraints). |
|
59 *} |
|
60 |
|
61 (*<*) |
|
62 lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)" |
|
63 apply (rule_tac n = k in induct) |
|
64 apply (rule notI) |
|
65 apply (erule Suc_neq_0) |
|
66 apply (rule notI) |
|
67 apply (erule notE) |
|
68 apply (erule Suc_inject) |
|
69 done |
|
70 |
|
71 lemma "(k+m)+n = k+(m+n)" |
|
72 apply (rule induct) |
|
73 back |
|
74 back |
|
75 back |
|
76 back |
|
77 back |
|
78 back |
|
79 oops |
|
80 |
|
81 lemma add_0 [simp]: "\<zero>+n = n" |
|
82 apply (unfold add_def) |
|
83 apply (rule rec_0) |
|
84 done |
|
85 |
|
86 lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)" |
|
87 apply (unfold add_def) |
|
88 apply (rule rec_Suc) |
|
89 done |
|
90 |
|
91 lemma add_assoc: "(k+m)+n = k+(m+n)" |
|
92 apply (rule_tac n = k in induct) |
|
93 apply simp |
|
94 apply simp |
|
95 done |
|
96 |
|
97 lemma add_0_right: "m+\<zero> = m" |
|
98 apply (rule_tac n = m in induct) |
|
99 apply simp |
|
100 apply simp |
|
101 done |
|
102 |
|
103 lemma add_Suc_right: "m+Suc(n) = Suc(m+n)" |
|
104 apply (rule_tac n = m in induct) |
|
105 apply simp_all |
|
106 done |
|
107 |
|
108 lemma |
|
109 assumes prem: "!!n. f(Suc(n)) = Suc(f(n))" |
|
110 shows "f(i+j) = i+f(j)" |
|
111 apply (rule_tac n = i in induct) |
|
112 apply simp |
|
113 apply (simp add: prem) |
|
114 done |
|
115 (*>*) |
|
116 |
|
117 end |
|