2 |
2 |
3 theory Peano_Axioms |
3 theory Peano_Axioms |
4 imports Main |
4 imports Main |
5 begin |
5 begin |
6 |
6 |
7 locale peano = |
7 locale peano = \<comment> \<open>or: \<^theory_text>\<open>class\<close>\<close> |
8 fixes zero :: 'n |
8 fixes zero :: 'a |
9 fixes succ :: "'n \<Rightarrow> 'n" |
9 fixes succ :: "'a \<Rightarrow> 'a" |
10 assumes succ_neq_zero [simp]: "succ m \<noteq> zero" |
10 assumes succ_neq_zero [simp]: "succ m \<noteq> zero" |
11 assumes succ_inject [simp]: "succ m = succ n \<longleftrightarrow> m = n" |
11 assumes succ_inject [simp]: "succ m = succ n \<longleftrightarrow> m = n" |
12 assumes induct [case_names zero succ, induct type: 'n]: |
12 assumes induct [case_names zero succ, induct type: 'a]: |
13 "P zero \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (succ n)) \<Longrightarrow> P n" |
13 "P zero \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (succ n)) \<Longrightarrow> P n" |
14 begin |
14 begin |
15 |
15 |
16 lemma zero_neq_succ [simp]: "zero \<noteq> succ m" |
16 lemma zero_neq_succ [simp]: "zero \<noteq> succ m" |
17 by (rule succ_neq_zero [symmetric]) |
17 by (rule succ_neq_zero [symmetric]) |
18 |
18 |
19 |
19 |
20 text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close> |
20 text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close> |
21 |
21 |
22 inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool" |
22 inductive Rec :: "'b \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
23 for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a" |
23 for e :: 'b and r :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" |
24 where |
24 where |
25 Rec_zero: "Rec e r zero e" |
25 Rec_zero: "Rec e r zero e" |
26 | Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)" |
26 | Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)" |
27 |
27 |
28 lemma Rec_functional: "\<exists>!y::'a. Rec e r x y" for x :: 'n |
28 lemma Rec_functional: "\<exists>!y::'b. Rec e r x y" for x :: 'a |
29 proof - |
29 proof - |
30 let ?R = "Rec e r" |
30 let ?R = "Rec e r" |
31 show ?thesis |
31 show ?thesis |
32 proof (induct x) |
32 proof (induct x) |
33 case zero |
33 case zero |
82 qed |
82 qed |
83 |
83 |
84 |
84 |
85 text \<open>\<^medskip> Example: addition (monomorphic)\<close> |
85 text \<open>\<^medskip> Example: addition (monomorphic)\<close> |
86 |
86 |
87 definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n" |
87 definition add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
88 where "add m n = rec n (\<lambda>_ k. succ k) m" |
88 where "add m n = rec n (\<lambda>_ k. succ k) m" |
89 |
89 |
90 lemma add_zero [simp]: "add zero n = n" |
90 lemma add_zero [simp]: "add zero n = n" |
91 and add_succ [simp]: "add (succ m) n = succ (add m n)" |
91 and add_succ [simp]: "add (succ m) n = succ (add m n)" |
92 unfolding add_def by simp_all |
92 unfolding add_def by simp_all |
105 by simp |
105 by simp |
106 |
106 |
107 |
107 |
108 text \<open>\<^medskip> Example: replication (polymorphic)\<close> |
108 text \<open>\<^medskip> Example: replication (polymorphic)\<close> |
109 |
109 |
110 definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list" |
110 definition repl :: "'a \<Rightarrow> 'b \<Rightarrow> 'b list" |
111 where "repl n x = rec [] (\<lambda>_ xs. x # xs) n" |
111 where "repl n x = rec [] (\<lambda>_ xs. x # xs) n" |
112 |
112 |
113 lemma repl_zero [simp]: "repl zero x = []" |
113 lemma repl_zero [simp]: "repl zero x = []" |
114 and repl_succ [simp]: "repl (succ n) x = x # repl n x" |
114 and repl_succ [simp]: "repl (succ n) x = x # repl n x" |
115 unfolding repl_def by simp_all |
115 unfolding repl_def by simp_all |