equal
deleted
inserted
replaced
25 |
25 |
26 declare nat_0 [simp] nat_1 [simp] |
26 declare nat_0 [simp] nat_1 [simp] |
27 |
27 |
28 lemma nat_number_of [simp]: "nat (number_of w) = number_of w" |
28 lemma nat_number_of [simp]: "nat (number_of w) = number_of w" |
29 by (simp add: nat_number_of_def) |
29 by (simp add: nat_number_of_def) |
30 |
|
31 declare nat_number_of [symmetric, THEN eq_reflection, code unfold] |
|
32 |
30 |
33 lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)" |
31 lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)" |
34 by (simp add: nat_number_of_def) |
32 by (simp add: nat_number_of_def) |
35 |
33 |
36 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)" |
34 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)" |