equal
deleted
inserted
replaced
18 *} |
18 *} |
19 |
19 |
20 subsection {* Representation *} |
20 subsection {* Representation *} |
21 |
21 |
22 code_datatype "0::nat" nat_of_num |
22 code_datatype "0::nat" nat_of_num |
23 |
|
24 lemma [code_abbrev]: |
|
25 "nat_of_num = numeral" |
|
26 by (fact nat_of_num_numeral) |
|
27 |
23 |
28 lemma [code]: |
24 lemma [code]: |
29 "num_of_nat 0 = Num.One" |
25 "num_of_nat 0 = Num.One" |
30 "num_of_nat (nat_of_num k) = k" |
26 "num_of_nat (nat_of_num k) = k" |
31 by (simp_all add: nat_of_num_inverse) |
27 by (simp_all add: nat_of_num_inverse) |