26 |
26 |
27 definition |
27 definition |
28 nat_of_int :: "int \<Rightarrow> nat" |
28 nat_of_int :: "int \<Rightarrow> nat" |
29 "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k" |
29 "k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k" |
30 |
30 |
|
31 lemma nat_of_int_int: |
|
32 "nat_of_int (int n) = n" |
|
33 using zero_zle_int nat_of_int_def by simp |
|
34 |
31 code_constname |
35 code_constname |
32 nat_of_int "IntDef.nat_of_int" |
36 nat_of_int "IntDef.nat_of_int" |
33 |
37 |
34 text {* |
38 text {* |
35 Case analysis on natural numbers is rephrased using a conditional |
39 Case analysis on natural numbers is rephrased using a conditional |
36 expression: |
40 expression: |
37 *} |
41 *} |
38 |
42 |
39 lemma [code unfold]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
43 lemma [code unfold, code noinline]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
40 proof - |
44 proof - |
41 have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))" |
45 have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))" |
42 proof - |
46 proof - |
43 fix f g n |
47 fix f g n |
44 show "nat_case f g n = (if n = 0 then f else g (n - 1))" |
48 show "nat_case f g n = (if n = 0 then f else g (n - 1))" |
45 by (cases n) simp_all |
49 by (cases n) simp_all |
46 qed |
50 qed |
47 show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
51 show "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
48 by (rule eq_reflection ext rewrite)+ |
52 by (rule eq_reflection ext rewrite)+ |
49 qed |
53 qed |
|
54 |
|
55 lemma [code inline]: |
|
56 "nat_case f g n = (if OperationalEquality.eq n 0 then f else g (nat_of_int (int n - 1)))" |
|
57 by (cases n) (simp_all add: eq_def nat_of_int_int) |
50 |
58 |
51 text {* |
59 text {* |
52 Most standard arithmetic functions on natural numbers are implemented |
60 Most standard arithmetic functions on natural numbers are implemented |
53 using their counterparts on the integers: |
61 using their counterparts on the integers: |
54 *} |
62 *} |