[isabelle-dev] Additional lemma for Bool_List_Representation
diekmann at in.tum.de
Tue Mar 22 16:48:40 CET 2016
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)"
case(Cons b bs)
with bl_to_bin_lt2p_aux[where w=1] show ?case by 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).
More information about the isabelle-dev