1 (* Title: FOL/ex/NatClass.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 *) |
|
5 |
|
6 theory NatClass |
|
7 imports FOL |
|
8 begin |
|
9 |
|
10 text {* |
|
11 This is an abstract version of theory @{text "Nat"}. Instead of |
|
12 axiomatizing a single type @{text nat} we define the class of all |
|
13 these types (up to isomorphism). |
|
14 |
|
15 Note: The @{text rec} operator had to be made \emph{monomorphic}, |
|
16 because class axioms may not contain more than one type variable. |
|
17 *} |
|
18 |
|
19 consts |
|
20 0 :: 'a ("0") |
|
21 Suc :: "'a => 'a" |
|
22 rec :: "['a, 'a, ['a, 'a] => 'a] => 'a" |
|
23 |
|
24 axclass |
|
25 nat < "term" |
|
26 induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" |
|
27 Suc_inject: "Suc(m) = Suc(n) ==> m = n" |
|
28 Suc_neq_0: "Suc(m) = 0 ==> R" |
|
29 rec_0: "rec(0, a, f) = a" |
|
30 rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" |
|
31 |
|
32 definition |
|
33 add :: "['a::nat, 'a] => 'a" (infixl "+" 60) where |
|
34 "m + n = rec(m, n, %x y. Suc(y))" |
|
35 |
|
36 lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)" |
|
37 apply (rule_tac n = k in induct) |
|
38 apply (rule notI) |
|
39 apply (erule Suc_neq_0) |
|
40 apply (rule notI) |
|
41 apply (erule notE) |
|
42 apply (erule Suc_inject) |
|
43 done |
|
44 |
|
45 lemma "(k+m)+n = k+(m+n)" |
|
46 apply (rule induct) |
|
47 back |
|
48 back |
|
49 back |
|
50 back |
|
51 back |
|
52 back |
|
53 oops |
|
54 |
|
55 lemma add_0 [simp]: "0+n = n" |
|
56 apply (unfold add_def) |
|
57 apply (rule rec_0) |
|
58 done |
|
59 |
|
60 lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)" |
|
61 apply (unfold add_def) |
|
62 apply (rule rec_Suc) |
|
63 done |
|
64 |
|
65 lemma add_assoc: "(k+m)+n = k+(m+n)" |
|
66 apply (rule_tac n = k in induct) |
|
67 apply simp |
|
68 apply simp |
|
69 done |
|
70 |
|
71 lemma add_0_right: "m+0 = m" |
|
72 apply (rule_tac n = m in induct) |
|
73 apply simp |
|
74 apply simp |
|
75 done |
|
76 |
|
77 lemma add_Suc_right: "m+Suc(n) = Suc(m+n)" |
|
78 apply (rule_tac n = m in induct) |
|
79 apply simp_all |
|
80 done |
|
81 |
|
82 lemma |
|
83 assumes prem: "!!n. f(Suc(n)) = Suc(f(n))" |
|
84 shows "f(i+j) = i+f(j)" |
|
85 apply (rule_tac n = i in induct) |
|
86 apply simp |
|
87 apply (simp add: prem) |
|
88 done |
|
89 |
|
90 end |
|