*To*: Li Yongjian <lyj238 at gmail.com>*Subject*: Re: [isabelle] a question of formalization of parameterized-word (bit-vector)*From*: "C. Diekmann" <diekmann at in.tum.de>*Date*: Sun, 11 Sep 2016 12:34:20 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CABCjkDpmTa-R+kmg1Q9vXFRLj_hnLw1eVLDuNwypS3sqXr5Sgg@mail.gmail.com>*References*: <CABCjkDpmTa-R+kmg1Q9vXFRLj_hnLw1eVLDuNwypS3sqXr5Sgg@mail.gmail.com>*Sender*: c.diekmann at googlemail.com

Hi, > How to formalize such a lemma? Or I can be shown some examples which > formalize the parameterized-word problems. We did something quite similar: https://github.com/diekmann/Iptables_Semantics/blob/master/thy/IP_Addresses/Lib_Word_toString.thy#L100 But once you have an assumption, in your case "len_of TYPE('k) >= 3", proofs get really hard because Word_Lib cannot help you much. Those restrictions about a minimum length for a word probably only come from hard-coded constants, maybe you can rephrase the complicated lemma without the use of hard-coded constants? Best, Cornelius

**References**:

- Previous by Date: Re: [isabelle] a question of formalization of parameterized-word (bit-vector)
- Next by Date: [isabelle] Problems on auto solving in some basic arithmetic simplication
- Previous by Thread: [isabelle] a question of formalization of parameterized-word (bit-vector)
- Next by Thread: Re: [isabelle] a question of formalization of parameterized-word (bit-vector)
- Cl-isabelle-users September 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list