1 (* Title: HOL/Library/Code_Binary_Nat.thy |
1 (* Title: HOL/Library/Code_Binary_Nat.thy |
2 Author: Stefan Berghofer, Florian Haftmann, TU Muenchen |
2 Author: Florian Haftmann, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 header {* Implementation of natural numbers as binary numerals *} |
5 header {* Implementation of natural numbers as binary numerals *} |
6 |
6 |
7 theory Code_Binary_Nat |
7 theory Code_Binary_Nat |
8 imports Main |
8 imports Code_Abstract_Nat |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 When generating code for functions on natural numbers, the |
12 When generating code for functions on natural numbers, the |
13 canonical representation using @{term "0::nat"} and |
13 canonical representation using @{term "0::nat"} and |
144 "of_nat 0 = 0" |
144 "of_nat 0 = 0" |
145 "of_nat (nat_of_num k) = numeral k" |
145 "of_nat (nat_of_num k) = numeral k" |
146 by (simp_all add: nat_of_num_numeral) |
146 by (simp_all add: nat_of_num_numeral) |
147 |
147 |
148 |
148 |
149 subsection {* Case analysis *} |
|
150 |
|
151 text {* |
|
152 Case analysis on natural numbers is rephrased using a conditional |
|
153 expression: |
|
154 *} |
|
155 |
|
156 lemma [code, code_unfold]: |
|
157 "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
|
158 by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc) |
|
159 |
|
160 |
|
161 subsection {* Preprocessors *} |
|
162 |
|
163 text {* |
|
164 The term @{term "Suc n"} is no longer a valid pattern. |
|
165 Therefore, all occurrences of this term in a position |
|
166 where a pattern is expected (i.e.~on the left-hand side of a recursion |
|
167 equation) must be eliminated. |
|
168 This can be accomplished by applying the following transformation rules: |
|
169 *} |
|
170 |
|
171 lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow> |
|
172 f n \<equiv> if n = 0 then g else h (n - 1)" |
|
173 by (rule eq_reflection) (cases n, simp_all) |
|
174 |
|
175 text {* |
|
176 The rules above are built into a preprocessor that is plugged into |
|
177 the code generator. Since the preprocessor for introduction rules |
|
178 does not know anything about modes, some of the modes that worked |
|
179 for the canonical representation of natural numbers may no longer work. |
|
180 *} |
|
181 |
|
182 (*<*) |
|
183 setup {* |
|
184 let |
|
185 |
|
186 fun remove_suc thy thms = |
|
187 let |
|
188 val vname = singleton (Name.variant_list (map fst |
|
189 (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; |
|
190 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
|
191 fun lhs_of th = snd (Thm.dest_comb |
|
192 (fst (Thm.dest_comb (cprop_of th)))); |
|
193 fun rhs_of th = snd (Thm.dest_comb (cprop_of th)); |
|
194 fun find_vars ct = (case term_of ct of |
|
195 (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] |
|
196 | _ $ _ => |
|
197 let val (ct1, ct2) = Thm.dest_comb ct |
|
198 in |
|
199 map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @ |
|
200 map (apfst (Thm.apply ct1)) (find_vars ct2) |
|
201 end |
|
202 | _ => []); |
|
203 val eqs = maps |
|
204 (fn th => map (pair th) (find_vars (lhs_of th))) thms; |
|
205 fun mk_thms (th, (ct, cv')) = |
|
206 let |
|
207 val th' = |
|
208 Thm.implies_elim |
|
209 (Conv.fconv_rule (Thm.beta_conversion true) |
|
210 (Drule.instantiate' |
|
211 [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct), |
|
212 SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv'] |
|
213 @{thm Suc_if_eq})) (Thm.forall_intr cv' th) |
|
214 in |
|
215 case map_filter (fn th'' => |
|
216 SOME (th'', singleton |
|
217 (Variable.trade (K (fn [th'''] => [th''' RS th'])) |
|
218 (Variable.global_thm_context th'')) th'') |
|
219 handle THM _ => NONE) thms of |
|
220 [] => NONE |
|
221 | thps => |
|
222 let val (ths1, ths2) = split_list thps |
|
223 in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end |
|
224 end |
|
225 in get_first mk_thms eqs end; |
|
226 |
|
227 fun eqn_suc_base_preproc thy thms = |
|
228 let |
|
229 val dest = fst o Logic.dest_equals o prop_of; |
|
230 val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); |
|
231 in |
|
232 if forall (can dest) thms andalso exists (contains_suc o dest) thms |
|
233 then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes |
|
234 else NONE |
|
235 end; |
|
236 |
|
237 val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc; |
|
238 |
|
239 in |
|
240 |
|
241 Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc) |
|
242 |
|
243 end; |
|
244 *} |
|
245 (*>*) |
|
246 |
|
247 code_modulename SML |
149 code_modulename SML |
248 Code_Binary_Nat Arith |
150 Code_Binary_Nat Arith |
249 |
151 |
250 code_modulename OCaml |
152 code_modulename OCaml |
251 Code_Binary_Nat Arith |
153 Code_Binary_Nat Arith |