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