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_inline]: |
30 "0 = (Numeral0 :: nat)" |
30 "0 = (Numeral0 :: nat)" |
31 by simp |
31 by simp |
32 lemmas [code post] = zero_nat_code [symmetric] |
32 lemmas [code_post] = zero_nat_code [symmetric] |
33 |
33 |
34 lemma one_nat_code [code, code inline]: |
34 lemma one_nat_code [code, code_inline]: |
35 "1 = (Numeral1 :: nat)" |
35 "1 = (Numeral1 :: nat)" |
36 by simp |
36 by simp |
37 lemmas [code post] = one_nat_code [symmetric] |
37 lemmas [code_post] = one_nat_code [symmetric] |
38 |
38 |
39 lemma Suc_code [code]: |
39 lemma Suc_code [code]: |
40 "Suc n = n + 1" |
40 "Suc n = n + 1" |
41 by simp |
41 by simp |
42 |
42 |
87 text {* |
87 text {* |
88 Case analysis on natural numbers is rephrased using a conditional |
88 Case analysis on natural numbers is rephrased using a conditional |
89 expression: |
89 expression: |
90 *} |
90 *} |
91 |
91 |
92 lemma [code, code unfold]: |
92 lemma [code, code_unfold]: |
93 "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
93 "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
94 by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc) |
94 by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc) |
95 |
95 |
96 |
96 |
97 subsection {* Preprocessors *} |
97 subsection {* Preprocessors *} |
300 |
300 |
301 text {* |
301 text {* |
302 Natural numerals. |
302 Natural numerals. |
303 *} |
303 *} |
304 |
304 |
305 lemma [code inline, symmetric, code post]: |
305 lemma [code_inline, symmetric, code_post]: |
306 "nat (number_of i) = number_nat_inst.number_of_nat i" |
306 "nat (number_of i) = number_nat_inst.number_of_nat i" |
307 -- {* this interacts as desired with @{thm nat_number_of_def} *} |
307 -- {* this interacts as desired with @{thm nat_number_of_def} *} |
308 by (simp add: number_nat_inst.number_of_nat) |
308 by (simp add: number_nat_inst.number_of_nat) |
309 |
309 |
310 setup {* |
310 setup {* |
333 |
333 |
334 lemma nat_code' [code]: |
334 lemma nat_code' [code]: |
335 "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)" |
335 "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 |
336 unfolding nat_number_of_def number_of_is_id neg_def by simp |
337 |
337 |
338 lemma of_nat_int [code unfold]: |
338 lemma of_nat_int [code_unfold]: |
339 "of_nat = int" by (simp add: int_def) |
339 "of_nat = int" by (simp add: int_def) |
340 declare of_nat_int [symmetric, code post] |
340 declare of_nat_int [symmetric, code_post] |
341 |
341 |
342 code_const int |
342 code_const int |
343 (SML "_") |
343 (SML "_") |
344 (OCaml "_") |
344 (OCaml "_") |
345 |
345 |