[STATEMENT]
lemma digit_7_code [code]:
  \<open>digit7 c \<longleftrightarrow> bit (integer_of_char c) 7\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit7 c = bit (integer_of_char c) 7
[PROOF STEP]
by (cases c) (simp add: integer_of_char_def)