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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev