author | wenzelm |
Sat, 22 Oct 2016 20:09:30 +0200 | |
changeset 64349 | 26bc905be09d |
parent 61489 | b8d375aee0df |
child 69587 | 53982d5ec0bb |
permissions | -rw-r--r-- |
3115 | 1 |
(* Title: FOL/ex/Nat.thy |
1473 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1992 University of Cambridge |
4 |
*) |
|
5 |
||
60770 | 6 |
section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close> |
17245 | 7 |
|
8 |
theory Nat |
|
9 |
imports FOL |
|
10 |
begin |
|
11 |
||
12 |
typedecl nat |
|
55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
41779
diff
changeset
|
13 |
instance nat :: "term" .. |
17245 | 14 |
|
41779 | 15 |
axiomatization |
16 |
Zero :: nat ("0") and |
|
17 |
Suc :: "nat => nat" and |
|
25989 | 18 |
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" |
41779 | 19 |
where |
20 |
induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" and |
|
21 |
Suc_inject: "Suc(m)=Suc(n) ==> m=n" and |
|
22 |
Suc_neq_0: "Suc(m)=0 ==> R" and |
|
23 |
rec_0: "rec(0,a,f) = a" and |
|
24 |
rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))" |
|
17245 | 25 |
|
41779 | 26 |
definition add :: "[nat, nat] => nat" (infixl "+" 60) |
27 |
where "m + n == rec(m, n, %x y. Suc(y))" |
|
17245 | 28 |
|
19819 | 29 |
|
60770 | 30 |
subsection \<open>Proofs about the natural numbers\<close> |
19819 | 31 |
|
61489 | 32 |
lemma Suc_n_not_n: "Suc(k) \<noteq> k" |
19819 | 33 |
apply (rule_tac n = k in induct) |
34 |
apply (rule notI) |
|
35 |
apply (erule Suc_neq_0) |
|
36 |
apply (rule notI) |
|
37 |
apply (erule notE) |
|
38 |
apply (erule Suc_inject) |
|
39 |
done |
|
40 |
||
41 |
lemma "(k+m)+n = k+(m+n)" |
|
42 |
apply (rule induct) |
|
43 |
back |
|
44 |
back |
|
45 |
back |
|
46 |
back |
|
47 |
back |
|
48 |
back |
|
49 |
oops |
|
50 |
||
51 |
lemma add_0 [simp]: "0+n = n" |
|
52 |
apply (unfold add_def) |
|
53 |
apply (rule rec_0) |
|
54 |
done |
|
55 |
||
56 |
lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)" |
|
57 |
apply (unfold add_def) |
|
58 |
apply (rule rec_Suc) |
|
59 |
done |
|
60 |
||
61 |
lemma add_assoc: "(k+m)+n = k+(m+n)" |
|
62 |
apply (rule_tac n = k in induct) |
|
63 |
apply simp |
|
64 |
apply simp |
|
65 |
done |
|
66 |
||
67 |
lemma add_0_right: "m+0 = m" |
|
68 |
apply (rule_tac n = m in induct) |
|
69 |
apply simp |
|
70 |
apply simp |
|
71 |
done |
|
72 |
||
73 |
lemma add_Suc_right: "m+Suc(n) = Suc(m+n)" |
|
74 |
apply (rule_tac n = m in induct) |
|
75 |
apply simp_all |
|
76 |
done |
|
77 |
||
78 |
lemma |
|
79 |
assumes prem: "!!n. f(Suc(n)) = Suc(f(n))" |
|
80 |
shows "f(i+j) = i+f(j)" |
|
81 |
apply (rule_tac n = i in induct) |
|
82 |
apply simp |
|
83 |
apply (simp add: prem) |
|
84 |
done |
|
17245 | 85 |
|
0 | 86 |
end |