12 Theory of the natural numbers: Peano's axioms, primitive recursion. |
12 Theory of the natural numbers: Peano's axioms, primitive recursion. |
13 (Modernized version of Larry Paulson's theory "Nat".) \medskip |
13 (Modernized version of Larry Paulson's theory "Nat".) \medskip |
14 \<close> |
14 \<close> |
15 |
15 |
16 typedecl nat |
16 typedecl nat |
17 instance nat :: "term" .. |
17 instance nat :: \<open>term\<close> .. |
18 |
18 |
19 axiomatization |
19 axiomatization |
20 Zero :: nat (\<open>0\<close>) and |
20 Zero :: \<open>nat\<close> (\<open>0\<close>) and |
21 Suc :: "nat => nat" and |
21 Suc :: \<open>nat => nat\<close> and |
22 rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" |
22 rec :: \<open>[nat, 'a, [nat, 'a] => 'a] => 'a\<close> |
23 where |
23 where |
24 induct [case_names 0 Suc, induct type: nat]: |
24 induct [case_names 0 Suc, induct type: nat]: |
25 "P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)" and |
25 \<open>P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)\<close> and |
26 Suc_inject: "Suc(m) = Suc(n) ==> m = n" and |
26 Suc_inject: \<open>Suc(m) = Suc(n) ==> m = n\<close> and |
27 Suc_neq_0: "Suc(m) = 0 ==> R" and |
27 Suc_neq_0: \<open>Suc(m) = 0 ==> R\<close> and |
28 rec_0: "rec(0, a, f) = a" and |
28 rec_0: \<open>rec(0, a, f) = a\<close> and |
29 rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" |
29 rec_Suc: \<open>rec(Suc(m), a, f) = f(m, rec(m, a, f))\<close> |
30 |
30 |
31 lemma Suc_n_not_n: "Suc(k) \<noteq> k" |
31 lemma Suc_n_not_n: \<open>Suc(k) \<noteq> k\<close> |
32 proof (induct k) |
32 proof (induct \<open>k\<close>) |
33 show "Suc(0) \<noteq> 0" |
33 show \<open>Suc(0) \<noteq> 0\<close> |
34 proof |
34 proof |
35 assume "Suc(0) = 0" |
35 assume \<open>Suc(0) = 0\<close> |
36 then show False by (rule Suc_neq_0) |
36 then show \<open>False\<close> by (rule Suc_neq_0) |
37 qed |
37 qed |
38 next |
38 next |
39 fix n assume hyp: "Suc(n) \<noteq> n" |
39 fix n assume hyp: \<open>Suc(n) \<noteq> n\<close> |
40 show "Suc(Suc(n)) \<noteq> Suc(n)" |
40 show \<open>Suc(Suc(n)) \<noteq> Suc(n)\<close> |
41 proof |
41 proof |
42 assume "Suc(Suc(n)) = Suc(n)" |
42 assume \<open>Suc(Suc(n)) = Suc(n)\<close> |
43 then have "Suc(n) = n" by (rule Suc_inject) |
43 then have \<open>Suc(n) = n\<close> by (rule Suc_inject) |
44 with hyp show False by contradiction |
44 with hyp show \<open>False\<close> by contradiction |
45 qed |
45 qed |
46 qed |
46 qed |
47 |
47 |
48 |
48 |
49 definition add :: "nat => nat => nat" (infixl \<open>+\<close> 60) |
49 definition add :: \<open>nat => nat => nat\<close> (infixl \<open>+\<close> 60) |
50 where "m + n = rec(m, n, \<lambda>x y. Suc(y))" |
50 where \<open>m + n = rec(m, n, \<lambda>x y. Suc(y))\<close> |
51 |
51 |
52 lemma add_0 [simp]: "0 + n = n" |
52 lemma add_0 [simp]: \<open>0 + n = n\<close> |
53 unfolding add_def by (rule rec_0) |
53 unfolding add_def by (rule rec_0) |
54 |
54 |
55 lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)" |
55 lemma add_Suc [simp]: \<open>Suc(m) + n = Suc(m + n)\<close> |
56 unfolding add_def by (rule rec_Suc) |
56 unfolding add_def by (rule rec_Suc) |
57 |
57 |
58 lemma add_assoc: "(k + m) + n = k + (m + n)" |
58 lemma add_assoc: \<open>(k + m) + n = k + (m + n)\<close> |
59 by (induct k) simp_all |
59 by (induct \<open>k\<close>) simp_all |
60 |
60 |
61 lemma add_0_right: "m + 0 = m" |
61 lemma add_0_right: \<open>m + 0 = m\<close> |
62 by (induct m) simp_all |
62 by (induct \<open>m\<close>) simp_all |
63 |
63 |
64 lemma add_Suc_right: "m + Suc(n) = Suc(m + n)" |
64 lemma add_Suc_right: \<open>m + Suc(n) = Suc(m + n)\<close> |
65 by (induct m) simp_all |
65 by (induct \<open>m\<close>) simp_all |
66 |
66 |
67 lemma |
67 lemma |
68 assumes "!!n. f(Suc(n)) = Suc(f(n))" |
68 assumes \<open>!!n. f(Suc(n)) = Suc(f(n))\<close> |
69 shows "f(i + j) = i + f(j)" |
69 shows \<open>f(i + j) = i + f(j)\<close> |
70 using assms by (induct i) simp_all |
70 using assms by (induct \<open>i\<close>) simp_all |
71 |
71 |
72 end |
72 end |