equal
deleted
inserted
replaced
12 |
12 |
13 definition Nat :: "integer \<Rightarrow> nat" |
13 definition Nat :: "integer \<Rightarrow> nat" |
14 where |
14 where |
15 "Nat = nat_of_integer" |
15 "Nat = nat_of_integer" |
16 |
16 |
17 definition integer_of_nat :: "nat \<Rightarrow> integer" |
17 lemma [code_post]: |
18 where |
18 "Nat 0 = 0" |
19 [code_abbrev]: "integer_of_nat = of_nat" |
19 "Nat 1 = 1" |
|
20 "Nat (numeral k) = numeral k" |
|
21 by (simp_all add: Nat_def nat_of_integer_def) |
20 |
22 |
21 lemma int_of_integer_integer_of_nat [simp]: |
23 lemma [code_abbrev]: |
22 "int_of_integer (integer_of_nat n) = of_nat n" |
24 "integer_of_nat = of_nat" |
23 by (simp add: integer_of_nat_def) |
25 by (fact integer_of_nat_def) |
24 |
26 |
25 lemma [code_unfold]: |
27 lemma [code_unfold]: |
26 "Int.nat (int_of_integer k) = nat_of_integer k" |
28 "Int.nat (int_of_integer k) = nat_of_integer k" |
27 by (simp add: nat_of_integer_def) |
29 by (simp add: nat_of_integer_def) |
28 |
30 |
33 lemma [code abstract]: |
35 lemma [code abstract]: |
34 "integer_of_nat (nat_of_integer k) = max 0 k" |
36 "integer_of_nat (nat_of_integer k) = max 0 k" |
35 by (simp add: integer_of_nat_def) |
37 by (simp add: integer_of_nat_def) |
36 |
38 |
37 lemma [code_abbrev]: |
39 lemma [code_abbrev]: |
38 "nat_of_integer (Code_Numeral_Types.Pos k) = nat_of_num k" |
40 "nat_of_integer (numeral k) = nat_of_num k" |
39 by (simp add: nat_of_integer_def nat_of_num_numeral) |
41 by (simp add: nat_of_integer_def nat_of_num_numeral) |
40 |
42 |
41 lemma [code abstract]: |
43 lemma [code abstract]: |
42 "integer_of_nat (nat_of_num n) = integer_of_num n" |
44 "integer_of_nat (nat_of_num n) = integer_of_num n" |
43 by (simp add: integer_eq_iff integer_of_num_def nat_of_num_numeral) |
45 by (simp add: integer_eq_iff integer_of_num_def nat_of_num_numeral) |