src/HOL/Integ/NatBin.thy
changeset 17550 9bcd6ea262b8
parent 17085 5b57f995a179
child 17668 8ef257366a0c
equal deleted inserted replaced
17549:ee4408eac12c 17550:9bcd6ea262b8
    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]
    30 
    32 
    31 lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
    33 lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
    32 by (simp add: nat_number_of_def)
    34 by (simp add: nat_number_of_def)
    33 
    35 
    34 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
    36 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"