Re: [isabelle] a question of formalization of parameterized-word (bit-vector)
> How to formalize such a lemma? Or I can be shown some examples which
> formalize the parameterized-word problems.
We did something quite similar:
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and