equal
deleted
inserted
replaced
24 using their counterparts on the integers: |
24 using their counterparts on the integers: |
25 *} |
25 *} |
26 |
26 |
27 code_datatype number_nat_inst.number_of_nat |
27 code_datatype number_nat_inst.number_of_nat |
28 |
28 |
29 lemma zero_nat_code [code, code_inline]: |
29 lemma zero_nat_code [code, code_unfold_post]: |
30 "0 = (Numeral0 :: nat)" |
30 "0 = (Numeral0 :: nat)" |
31 by simp |
31 by simp |
32 lemmas [code_post] = zero_nat_code [symmetric] |
32 |
33 |
33 lemma one_nat_code [code, code_unfold_post]: |
34 lemma one_nat_code [code, code_inline]: |
|
35 "1 = (Numeral1 :: nat)" |
34 "1 = (Numeral1 :: nat)" |
36 by simp |
35 by simp |
37 lemmas [code_post] = one_nat_code [symmetric] |
|
38 |
36 |
39 lemma Suc_code [code]: |
37 lemma Suc_code [code]: |
40 "Suc n = n + 1" |
38 "Suc n = n + 1" |
41 by simp |
39 by simp |
42 |
40 |
300 |
298 |
301 text {* |
299 text {* |
302 Natural numerals. |
300 Natural numerals. |
303 *} |
301 *} |
304 |
302 |
305 lemma [code_inline, symmetric, code_post]: |
303 lemma [code_unfold_post]: |
306 "nat (number_of i) = number_nat_inst.number_of_nat i" |
304 "nat (number_of i) = number_nat_inst.number_of_nat i" |
307 -- {* this interacts as desired with @{thm nat_number_of_def} *} |
305 -- {* this interacts as desired with @{thm nat_number_of_def} *} |
308 by (simp add: number_nat_inst.number_of_nat) |
306 by (simp add: number_nat_inst.number_of_nat) |
309 |
307 |
310 setup {* |
308 setup {* |
333 |
331 |
334 lemma nat_code' [code]: |
332 lemma nat_code' [code]: |
335 "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)" |
333 "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)" |
336 unfolding nat_number_of_def number_of_is_id neg_def by simp |
334 unfolding nat_number_of_def number_of_is_id neg_def by simp |
337 |
335 |
338 lemma of_nat_int [code_unfold]: |
336 lemma of_nat_int [code_unfold_post]: |
339 "of_nat = int" by (simp add: int_def) |
337 "of_nat = int" by (simp add: int_def) |
340 declare of_nat_int [symmetric, code_post] |
|
341 |
338 |
342 code_const int |
339 code_const int |
343 (SML "_") |
340 (SML "_") |
344 (OCaml "_") |
341 (OCaml "_") |
345 |
342 |