[isabelle-dev] Additional lemma for Bool_List_Representation

[C. Diekmann]

Hi,

in HOL/Word/Bool_List_Representation.thy, there is the lemma bl_to_bin_lt2p:
  "bl_to_bin bs < (2 ^ length bs)"

I would like to add a stronger version. The stronger version states
that we can ignore the leading zeros of a bit list.

lemma bl_to_bin_lt2p_dropNot: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
  unfolding bl_to_bin_def
  proof(induction bs)
  case(Cons b bs)
    with bl_to_bin_lt2p_aux[where w=1] show ?case by simp
  qed(simp)

I'm not an Isabelle developer nor do I have push rights. If someone
approves of this lemma, I would be happy if it would make its way into
the default distribution. Also, I would be very interested in a name
for that lemma that is consistent with the Isabelle naming convention
for lemmas about words (if such a thing exists).

Best,
  Cornelius