29752
|
1 |
(* Title: FOL/ex/Nat_Class.thy
|
1246
|
2 |
Author: Markus Wenzel, TU Muenchen
|
|
3 |
*)
|
|
4 |
|
69866
|
5 |
section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
|
|
6 |
|
29752
|
7 |
theory Nat_Class
|
69866
|
8 |
imports FOL
|
17245
|
9 |
begin
|
|
10 |
|
60770
|
11 |
text \<open>
|
69866
|
12 |
This is an abstract version of \<^file>\<open>Nat.thy\<close>. Instead of axiomatizing a
|
|
13 |
single type \<open>nat\<close>, it defines the class of all these types (up to
|
69581
|
14 |
isomorphism).
|
17245
|
15 |
|
69866
|
16 |
Note: The \<open>rec\<close> operator has been made \<^emph>\<open>monomorphic\<close>, because class
|
|
17 |
axioms cannot contain more than one type variable.
|
60770
|
18 |
\<close>
|
1246
|
19 |
|
29751
|
20 |
class nat =
|
69590
|
21 |
fixes Zero :: \<open>'a\<close> (\<open>0\<close>)
|
|
22 |
and Suc :: \<open>'a \<Rightarrow> 'a\<close>
|
|
23 |
and rec :: \<open>'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a\<close>
|
|
24 |
assumes induct: \<open>P(0) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)\<close>
|
|
25 |
and Suc_inject: \<open>Suc(m) = Suc(n) \<Longrightarrow> m = n\<close>
|
|
26 |
and Suc_neq_Zero: \<open>Suc(m) = 0 \<Longrightarrow> R\<close>
|
|
27 |
and rec_Zero: \<open>rec(0, a, f) = a\<close>
|
|
28 |
and rec_Suc: \<open>rec(Suc(m), a, f) = f(m, rec(m, a, f))\<close>
|
29751
|
29 |
begin
|
1246
|
30 |
|
69590
|
31 |
definition add :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>+\<close> 60)
|
|
32 |
where \<open>m + n = rec(m, n, \<lambda>x y. Suc(y))\<close>
|
19819
|
33 |
|
69590
|
34 |
lemma Suc_n_not_n: \<open>Suc(k) \<noteq> (k::'a)\<close>
|
|
35 |
apply (rule_tac n = \<open>k\<close> in induct)
|
29751
|
36 |
apply (rule notI)
|
|
37 |
apply (erule Suc_neq_Zero)
|
|
38 |
apply (rule notI)
|
|
39 |
apply (erule notE)
|
|
40 |
apply (erule Suc_inject)
|
|
41 |
done
|
19819
|
42 |
|
69590
|
43 |
lemma \<open>(k + m) + n = k + (m + n)\<close>
|
29751
|
44 |
apply (rule induct)
|
|
45 |
back
|
|
46 |
back
|
|
47 |
back
|
|
48 |
back
|
|
49 |
back
|
|
50 |
oops
|
19819
|
51 |
|
69590
|
52 |
lemma add_Zero [simp]: \<open>0 + n = n\<close>
|
29751
|
53 |
apply (unfold add_def)
|
|
54 |
apply (rule rec_Zero)
|
|
55 |
done
|
1246
|
56 |
|
69590
|
57 |
lemma add_Suc [simp]: \<open>Suc(m) + n = Suc(m + n)\<close>
|
29751
|
58 |
apply (unfold add_def)
|
|
59 |
apply (rule rec_Suc)
|
|
60 |
done
|
19819
|
61 |
|
69590
|
62 |
lemma add_assoc: \<open>(k + m) + n = k + (m + n)\<close>
|
|
63 |
apply (rule_tac n = \<open>k\<close> in induct)
|
29751
|
64 |
apply simp
|
|
65 |
apply simp
|
|
66 |
done
|
19819
|
67 |
|
69590
|
68 |
lemma add_Zero_right: \<open>m + 0 = m\<close>
|
|
69 |
apply (rule_tac n = \<open>m\<close> in induct)
|
29751
|
70 |
apply simp
|
|
71 |
apply simp
|
|
72 |
done
|
19819
|
73 |
|
69590
|
74 |
lemma add_Suc_right: \<open>m + Suc(n) = Suc(m + n)\<close>
|
|
75 |
apply (rule_tac n = \<open>m\<close> in induct)
|
29751
|
76 |
apply simp_all
|
|
77 |
done
|
19819
|
78 |
|
|
79 |
lemma
|
69590
|
80 |
assumes prem: \<open>\<And>n. f(Suc(n)) = Suc(f(n))\<close>
|
|
81 |
shows \<open>f(i + j) = i + f(j)\<close>
|
|
82 |
apply (rule_tac n = \<open>i\<close> in induct)
|
29751
|
83 |
apply simp
|
|
84 |
apply (simp add: prem)
|
|
85 |
done
|
1246
|
86 |
|
|
87 |
end
|
29751
|
88 |
|
|
89 |
end
|