[isabelle-dev] Additional lemma for Bool_List_Representation

[Gerwin Klein]

I’ll transform the proof slightly and add it.

Names are hard ;-) I’d call it just bl_to_bin_lt2p_drop.

Cheers,
Gerwin



> On 23.03.2016, at 02:48, C. Diekmann <diekmann at in.tum.de> wrote:
>
> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


________________________________

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.