[isabelle-dev] Additional lemma for Bool_List_Representation
Gerwin.Klein at nicta.com.au
Tue Mar 22 23:13:50 CET 2016
I’ll transform the proof slightly and add it.
Names are hard ;-) I’d call it just bl_to_bin_lt2p_drop.
> On 23.03.2016, at 02:48, C. Diekmann <diekmann at in.tum.de> wrote:
> 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
> 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).
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
More information about the isabelle-dev