equal
deleted
inserted
replaced
1 (* |
1 (* Title: HOL/ex/Abstract_NAT.thy |
2 Author: Makarius |
2 Author: Makarius |
3 *) |
3 *) |
4 |
4 |
5 header {* Abstract Natural Numbers primitive recursion *} |
5 header {* Abstract Natural Numbers primitive recursion *} |
6 |
6 |
23 by (rule succ_neq_zero [symmetric]) |
23 by (rule succ_neq_zero [symmetric]) |
24 |
24 |
25 |
25 |
26 text {* \medskip Primitive recursion as a (functional) relation -- polymorphic! *} |
26 text {* \medskip Primitive recursion as a (functional) relation -- polymorphic! *} |
27 |
27 |
28 inductive |
28 inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool" |
29 Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool" |
|
30 for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a" |
29 for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a" |
31 where |
30 where |
32 Rec_zero: "Rec e r zero e" |
31 Rec_zero: "Rec e r zero e" |
33 | Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)" |
32 | Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)" |
34 |
33 |
62 qed |
61 qed |
63 |
62 |
64 |
63 |
65 text {* \medskip The recursion operator -- polymorphic! *} |
64 text {* \medskip The recursion operator -- polymorphic! *} |
66 |
65 |
67 definition |
66 definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a" |
68 rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a" where |
67 where "rec e r x = (THE y. Rec e r x y)" |
69 "rec e r x = (THE y. Rec e r x y)" |
|
70 |
68 |
71 lemma rec_eval: |
69 lemma rec_eval: |
72 assumes Rec: "Rec e r x y" |
70 assumes Rec: "Rec e r x y" |
73 shows "rec e r x = y" |
71 shows "rec e r x = y" |
74 unfolding rec_def |
72 unfolding rec_def |
88 qed |
86 qed |
89 |
87 |
90 |
88 |
91 text {* \medskip Example: addition (monomorphic) *} |
89 text {* \medskip Example: addition (monomorphic) *} |
92 |
90 |
93 definition |
91 definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n" |
94 add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n" where |
92 where "add m n = rec n (\<lambda>_ k. succ k) m" |
95 "add m n = rec n (\<lambda>_ k. succ k) m" |
|
96 |
93 |
97 lemma add_zero [simp]: "add zero n = n" |
94 lemma add_zero [simp]: "add zero n = n" |
98 and add_succ [simp]: "add (succ m) n = succ (add m n)" |
95 and add_succ [simp]: "add (succ m) n = succ (add m n)" |
99 unfolding add_def by simp_all |
96 unfolding add_def by simp_all |
100 |
97 |
112 by simp |
109 by simp |
113 |
110 |
114 |
111 |
115 text {* \medskip Example: replication (polymorphic) *} |
112 text {* \medskip Example: replication (polymorphic) *} |
116 |
113 |
117 definition |
114 definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list" |
118 repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list" where |
115 where "repl n x = rec [] (\<lambda>_ xs. x # xs) n" |
119 "repl n x = rec [] (\<lambda>_ xs. x # xs) n" |
|
120 |
116 |
121 lemma repl_zero [simp]: "repl zero x = []" |
117 lemma repl_zero [simp]: "repl zero x = []" |
122 and repl_succ [simp]: "repl (succ n) x = x # repl n x" |
118 and repl_succ [simp]: "repl (succ n) x = x # repl n x" |
123 unfolding repl_def by simp_all |
119 unfolding repl_def by simp_all |
124 |
120 |
138 fix P |
134 fix P |
139 assume zero: "P 0" |
135 assume zero: "P 0" |
140 and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)" |
136 and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)" |
141 show "P n" |
137 show "P n" |
142 proof (induct n) |
138 proof (induct n) |
143 case 0 show ?case by (rule zero) |
139 case 0 |
|
140 show ?case by (rule zero) |
144 next |
141 next |
145 case Suc then show ?case by (rule succ) |
142 case Suc |
|
143 then show ?case by (rule succ) |
146 qed |
144 qed |
147 qed |
145 qed |
148 |
146 |
149 end |
147 end |