[STATEMENT]
lemma integer_of_num [code]:
  "integer_of_num Num.One = 1"
  "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)"
  "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integer_of_num num.One = 1 &&& integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k) &&& integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)
[PROOF STEP]
by (simp_all only: integer_of_num_def numeral.simps Let_def)