Re: [isabelle] a question of formalization of parameterized-word (bit-vector)



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.