equal
deleted
inserted
replaced
23 A int-to-nat conversion with domain |
23 A int-to-nat conversion with domain |
24 restricted to non-negative ints (in contrast to @{const nat}). |
24 restricted to non-negative ints (in contrast to @{const nat}). |
25 *} |
25 *} |
26 |
26 |
27 definition |
27 definition |
28 nat_of_int :: "int \<Rightarrow> nat" |
28 nat_of_int :: "int \<Rightarrow> nat" where |
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: |
31 lemma nat_of_int_int: |
32 "nat_of_int (int n) = n" |
32 "nat_of_int (int n) = n" |
33 using zero_zle_int nat_of_int_def by simp |
33 using zero_zle_int nat_of_int_def by simp |