author | wenzelm |
Sun, 26 Nov 2006 23:43:53 +0100 | |
changeset 21539 | c5cf9243ad62 |
parent 16417 | 9bc16273c2d4 |
child 25989 | 3267d0694d93 |
permissions | -rw-r--r-- |
11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: FOL/ex/Natural_Numbers.thy |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Munich |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
4 |
*) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
5 |
|
12371 | 6 |
header {* Natural numbers *} |
7 |
||
16417 | 8 |
theory Natural_Numbers imports FOL begin |
11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
9 |
|
12371 | 10 |
text {* |
11 |
Theory of the natural numbers: Peano's axioms, primitive recursion. |
|
12 |
(Modernized version of Larry Paulson's theory "Nat".) \medskip |
|
13 |
*} |
|
14 |
||
11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
15 |
typedecl nat |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
16 |
arities nat :: "term" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
17 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
18 |
consts |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
19 |
Zero :: nat ("0") |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
20 |
Suc :: "nat => nat" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
21 |
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
22 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
23 |
axioms |
11789 | 24 |
induct [case_names 0 Suc, induct type: nat]: |
11679 | 25 |
"P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)" |
11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
26 |
Suc_inject: "Suc(m) = Suc(n) ==> m = n" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
27 |
Suc_neq_0: "Suc(m) = 0 ==> R" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
28 |
rec_0: "rec(0, a, f) = a" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
29 |
rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
30 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
31 |
lemma Suc_n_not_n: "Suc(k) \<noteq> k" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
32 |
proof (induct k) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
33 |
show "Suc(0) \<noteq> 0" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
34 |
proof |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
35 |
assume "Suc(0) = 0" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
36 |
thus False by (rule Suc_neq_0) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
37 |
qed |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
38 |
fix n assume hyp: "Suc(n) \<noteq> n" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
39 |
show "Suc(Suc(n)) \<noteq> Suc(n)" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
40 |
proof |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
41 |
assume "Suc(Suc(n)) = Suc(n)" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
42 |
hence "Suc(n) = n" by (rule Suc_inject) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
43 |
with hyp show False by contradiction |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
44 |
qed |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
45 |
qed |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
46 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
47 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
48 |
constdefs |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
49 |
add :: "[nat, nat] => nat" (infixl "+" 60) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
50 |
"m + n == rec(m, n, \<lambda>x y. Suc(y))" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
51 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
52 |
lemma add_0 [simp]: "0 + n = n" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
53 |
by (unfold add_def) (rule rec_0) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
54 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
55 |
lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
56 |
by (unfold add_def) (rule rec_Suc) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
57 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
58 |
lemma add_assoc: "(k + m) + n = k + (m + n)" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
59 |
by (induct k) simp_all |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
60 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
61 |
lemma add_0_right: "m + 0 = m" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
62 |
by (induct m) simp_all |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
63 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
64 |
lemma add_Suc_right: "m + Suc(n) = Suc(m + n)" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
65 |
by (induct m) simp_all |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
66 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
67 |
lemma "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i + j) = i + f(j)" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
68 |
proof - |
11726 | 69 |
assume "!!n. f(Suc(n)) = Suc(f(n))" |
70 |
thus ?thesis by (induct i) simp_all |
|
11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
71 |
qed |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
72 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
73 |
end |