8 theory Nat |
8 theory Nat |
9 imports FOL |
9 imports FOL |
10 begin |
10 begin |
11 |
11 |
12 typedecl nat |
12 typedecl nat |
13 instance nat :: "term" .. |
13 instance nat :: \<open>term\<close> .. |
14 |
14 |
15 axiomatization |
15 axiomatization |
16 Zero :: nat (\<open>0\<close>) and |
16 Zero :: \<open>nat\<close> (\<open>0\<close>) and |
17 Suc :: "nat => nat" and |
17 Suc :: \<open>nat => nat\<close> and |
18 rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" |
18 rec :: \<open>[nat, 'a, [nat, 'a] => 'a] => 'a\<close> |
19 where |
19 where |
20 induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" and |
20 induct: \<open>[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)\<close> and |
21 Suc_inject: "Suc(m)=Suc(n) ==> m=n" and |
21 Suc_inject: \<open>Suc(m)=Suc(n) ==> m=n\<close> and |
22 Suc_neq_0: "Suc(m)=0 ==> R" and |
22 Suc_neq_0: \<open>Suc(m)=0 ==> R\<close> and |
23 rec_0: "rec(0,a,f) = a" and |
23 rec_0: \<open>rec(0,a,f) = a\<close> and |
24 rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))" |
24 rec_Suc: \<open>rec(Suc(m), a, f) = f(m, rec(m,a,f))\<close> |
25 |
25 |
26 definition add :: "[nat, nat] => nat" (infixl \<open>+\<close> 60) |
26 definition add :: \<open>[nat, nat] => nat\<close> (infixl \<open>+\<close> 60) |
27 where "m + n == rec(m, n, %x y. Suc(y))" |
27 where \<open>m + n == rec(m, n, %x y. Suc(y))\<close> |
28 |
28 |
29 |
29 |
30 subsection \<open>Proofs about the natural numbers\<close> |
30 subsection \<open>Proofs about the natural numbers\<close> |
31 |
31 |
32 lemma Suc_n_not_n: "Suc(k) \<noteq> k" |
32 lemma Suc_n_not_n: \<open>Suc(k) \<noteq> k\<close> |
33 apply (rule_tac n = k in induct) |
33 apply (rule_tac n = \<open>k\<close> in induct) |
34 apply (rule notI) |
34 apply (rule notI) |
35 apply (erule Suc_neq_0) |
35 apply (erule Suc_neq_0) |
36 apply (rule notI) |
36 apply (rule notI) |
37 apply (erule notE) |
37 apply (erule notE) |
38 apply (erule Suc_inject) |
38 apply (erule Suc_inject) |
39 done |
39 done |
40 |
40 |
41 lemma "(k+m)+n = k+(m+n)" |
41 lemma \<open>(k+m)+n = k+(m+n)\<close> |
42 apply (rule induct) |
42 apply (rule induct) |
43 back |
43 back |
44 back |
44 back |
45 back |
45 back |
46 back |
46 back |
47 back |
47 back |
48 back |
48 back |
49 oops |
49 oops |
50 |
50 |
51 lemma add_0 [simp]: "0+n = n" |
51 lemma add_0 [simp]: \<open>0+n = n\<close> |
52 apply (unfold add_def) |
52 apply (unfold add_def) |
53 apply (rule rec_0) |
53 apply (rule rec_0) |
54 done |
54 done |
55 |
55 |
56 lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)" |
56 lemma add_Suc [simp]: \<open>Suc(m)+n = Suc(m+n)\<close> |
57 apply (unfold add_def) |
57 apply (unfold add_def) |
58 apply (rule rec_Suc) |
58 apply (rule rec_Suc) |
59 done |
59 done |
60 |
60 |
61 lemma add_assoc: "(k+m)+n = k+(m+n)" |
61 lemma add_assoc: \<open>(k+m)+n = k+(m+n)\<close> |
62 apply (rule_tac n = k in induct) |
62 apply (rule_tac n = \<open>k\<close> in induct) |
63 apply simp |
63 apply simp |
64 apply simp |
64 apply simp |
65 done |
65 done |
66 |
66 |
67 lemma add_0_right: "m+0 = m" |
67 lemma add_0_right: \<open>m+0 = m\<close> |
68 apply (rule_tac n = m in induct) |
68 apply (rule_tac n = \<open>m\<close> in induct) |
69 apply simp |
69 apply simp |
70 apply simp |
70 apply simp |
71 done |
71 done |
72 |
72 |
73 lemma add_Suc_right: "m+Suc(n) = Suc(m+n)" |
73 lemma add_Suc_right: \<open>m+Suc(n) = Suc(m+n)\<close> |
74 apply (rule_tac n = m in induct) |
74 apply (rule_tac n = \<open>m\<close> in induct) |
75 apply simp_all |
75 apply simp_all |
76 done |
76 done |
77 |
77 |
78 lemma |
78 lemma |
79 assumes prem: "!!n. f(Suc(n)) = Suc(f(n))" |
79 assumes prem: \<open>!!n. f(Suc(n)) = Suc(f(n))\<close> |
80 shows "f(i+j) = i+f(j)" |
80 shows \<open>f(i+j) = i+f(j)\<close> |
81 apply (rule_tac n = i in induct) |
81 apply (rule_tac n = \<open>i\<close> in induct) |
82 apply simp |
82 apply simp |
83 apply (simp add: prem) |
83 apply (simp add: prem) |
84 done |
84 done |
85 |
85 |
86 end |
86 end |