1 (* Title: HOL/ex/Abstract_NAT.thy |
|
2 Author: Makarius |
|
3 *) |
|
4 |
|
5 section \<open>Abstract Natural Numbers primitive recursion\<close> |
|
6 |
|
7 theory Abstract_NAT |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 text \<open>Axiomatic Natural Numbers (Peano) -- a monomorphic theory.\<close> |
|
12 |
|
13 locale NAT = |
|
14 fixes zero :: 'n |
|
15 and succ :: "'n \<Rightarrow> 'n" |
|
16 assumes succ_inject [simp]: "succ m = succ n \<longleftrightarrow> m = n" |
|
17 and succ_neq_zero [simp]: "succ m \<noteq> zero" |
|
18 and induct [case_names zero succ, induct type: 'n]: |
|
19 "P zero \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (succ n)) \<Longrightarrow> P n" |
|
20 begin |
|
21 |
|
22 lemma zero_neq_succ [simp]: "zero \<noteq> succ m" |
|
23 by (rule succ_neq_zero [symmetric]) |
|
24 |
|
25 |
|
26 text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close> |
|
27 |
|
28 inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool" |
|
29 for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a" |
|
30 where |
|
31 Rec_zero: "Rec e r zero e" |
|
32 | Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)" |
|
33 |
|
34 lemma Rec_functional: |
|
35 fixes x :: 'n |
|
36 shows "\<exists>!y::'a. Rec e r x y" |
|
37 proof - |
|
38 let ?R = "Rec e r" |
|
39 show ?thesis |
|
40 proof (induct x) |
|
41 case zero |
|
42 show "\<exists>!y. ?R zero y" |
|
43 proof |
|
44 show "?R zero e" .. |
|
45 show "y = e" if "?R zero y" for y |
|
46 using that by cases simp_all |
|
47 qed |
|
48 next |
|
49 case (succ m) |
|
50 from \<open>\<exists>!y. ?R m y\<close> |
|
51 obtain y where y: "?R m y" and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" |
|
52 by blast |
|
53 show "\<exists>!z. ?R (succ m) z" |
|
54 proof |
|
55 from y show "?R (succ m) (r m y)" .. |
|
56 next |
|
57 fix z |
|
58 assume "?R (succ m) z" |
|
59 then obtain u where "z = r m u" and "?R m u" |
|
60 by cases simp_all |
|
61 with yy' show "z = r m y" |
|
62 by (simp only:) |
|
63 qed |
|
64 qed |
|
65 qed |
|
66 |
|
67 |
|
68 text \<open>\<^medskip> The recursion operator -- polymorphic!\<close> |
|
69 |
|
70 definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a" |
|
71 where "rec e r x = (THE y. Rec e r x y)" |
|
72 |
|
73 lemma rec_eval: |
|
74 assumes Rec: "Rec e r x y" |
|
75 shows "rec e r x = y" |
|
76 unfolding rec_def |
|
77 using Rec_functional and Rec by (rule the1_equality) |
|
78 |
|
79 lemma rec_zero [simp]: "rec e r zero = e" |
|
80 proof (rule rec_eval) |
|
81 show "Rec e r zero e" .. |
|
82 qed |
|
83 |
|
84 lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)" |
|
85 proof (rule rec_eval) |
|
86 let ?R = "Rec e r" |
|
87 have "?R m (rec e r m)" |
|
88 unfolding rec_def using Rec_functional by (rule theI') |
|
89 then show "?R (succ m) (r m (rec e r m))" .. |
|
90 qed |
|
91 |
|
92 |
|
93 text \<open>\<^medskip> Example: addition (monomorphic)\<close> |
|
94 |
|
95 definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n" |
|
96 where "add m n = rec n (\<lambda>_ k. succ k) m" |
|
97 |
|
98 lemma add_zero [simp]: "add zero n = n" |
|
99 and add_succ [simp]: "add (succ m) n = succ (add m n)" |
|
100 unfolding add_def by simp_all |
|
101 |
|
102 lemma add_assoc: "add (add k m) n = add k (add m n)" |
|
103 by (induct k) simp_all |
|
104 |
|
105 lemma add_zero_right: "add m zero = m" |
|
106 by (induct m) simp_all |
|
107 |
|
108 lemma add_succ_right: "add m (succ n) = succ (add m n)" |
|
109 by (induct m) simp_all |
|
110 |
|
111 lemma "add (succ (succ (succ zero))) (succ (succ zero)) = |
|
112 succ (succ (succ (succ (succ zero))))" |
|
113 by simp |
|
114 |
|
115 |
|
116 text \<open>\<^medskip> Example: replication (polymorphic)\<close> |
|
117 |
|
118 definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list" |
|
119 where "repl n x = rec [] (\<lambda>_ xs. x # xs) n" |
|
120 |
|
121 lemma repl_zero [simp]: "repl zero x = []" |
|
122 and repl_succ [simp]: "repl (succ n) x = x # repl n x" |
|
123 unfolding repl_def by simp_all |
|
124 |
|
125 lemma "repl (succ (succ (succ zero))) True = [True, True, True]" |
|
126 by simp |
|
127 |
|
128 end |
|
129 |
|
130 |
|
131 text \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close> |
|
132 |
|
133 interpretation NAT 0 Suc |
|
134 proof (rule NAT.intro) |
|
135 fix m n |
|
136 show "Suc m = Suc n \<longleftrightarrow> m = n" by simp |
|
137 show "Suc m \<noteq> 0" by simp |
|
138 show "P n" |
|
139 if zero: "P 0" |
|
140 and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)" |
|
141 for P |
|
142 proof (induct n) |
|
143 case 0 |
|
144 show ?case by (rule zero) |
|
145 next |
|
146 case Suc |
|
147 then show ?case by (rule succ) |
|
148 qed |
|
149 qed |
|
150 |
|
151 end |
|