author | wenzelm |
Thu, 22 Apr 2004 11:01:34 +0200 | |
changeset 14651 | 02b8f3bcf7fe |
parent 12371 | 80ca9058db95 |
child 14981 | e73f8140af78 |
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 |
12371 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
5 |
*) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
6 |
|
12371 | 7 |
header {* Natural numbers *} |
8 |
||
11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
9 |
theory Natural_Numbers = FOL: |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
10 |
|
12371 | 11 |
text {* |
12 |
Theory of the natural numbers: Peano's axioms, primitive recursion. |
|
13 |
(Modernized version of Larry Paulson's theory "Nat".) \medskip |
|
14 |
*} |
|
15 |
||
11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
16 |
typedecl nat |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
17 |
arities nat :: "term" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
18 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
19 |
consts |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
20 |
Zero :: nat ("0") |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
21 |
Suc :: "nat => nat" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
22 |
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
23 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
24 |
axioms |
11789 | 25 |
induct [case_names 0 Suc, induct type: nat]: |
11679 | 26 |
"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
|
27 |
Suc_inject: "Suc(m) = Suc(n) ==> m = n" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
28 |
Suc_neq_0: "Suc(m) = 0 ==> R" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
29 |
rec_0: "rec(0, a, f) = a" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
30 |
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
|
31 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
32 |
lemma Suc_n_not_n: "Suc(k) \<noteq> k" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
33 |
proof (induct k) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
34 |
show "Suc(0) \<noteq> 0" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
35 |
proof |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
36 |
assume "Suc(0) = 0" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
37 |
thus False by (rule Suc_neq_0) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
38 |
qed |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
39 |
fix n assume hyp: "Suc(n) \<noteq> n" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
40 |
show "Suc(Suc(n)) \<noteq> Suc(n)" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
41 |
proof |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
42 |
assume "Suc(Suc(n)) = Suc(n)" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
43 |
hence "Suc(n) = n" by (rule Suc_inject) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
44 |
with hyp show False by contradiction |
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 |
qed |
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 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
49 |
constdefs |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
50 |
add :: "[nat, nat] => nat" (infixl "+" 60) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
51 |
"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
|
52 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
53 |
lemma add_0 [simp]: "0 + n = n" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
54 |
by (unfold add_def) (rule rec_0) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
55 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
56 |
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
|
57 |
by (unfold add_def) (rule rec_Suc) |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
58 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
59 |
lemma add_assoc: "(k + m) + n = k + (m + n)" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
60 |
by (induct k) simp_all |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
61 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
62 |
lemma add_0_right: "m + 0 = m" |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
63 |
by (induct m) simp_all |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
64 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
65 |
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
|
66 |
by (induct m) simp_all |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
67 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
68 |
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
|
69 |
proof - |
11726 | 70 |
assume "!!n. f(Suc(n)) = Suc(f(n))" |
71 |
thus ?thesis by (induct i) simp_all |
|
11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
72 |
qed |
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
73 |
|
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset
|
74 |
end |