Email Gateway (Aug 22 2022 at 14:05): Email Gateway (Aug 22 2022 at 14:05):From: Li Yongjian <lyj238@gmail.com>
Dear experts:
Now I meet a problem of formalization of a parameterized bit-vector.
Here a parameterized bit-vector. means that the width of the bit vector is
a parmeterize, for instance a variable in a program (hardware design) is a
word of some length k. I want to prove that some property P on the varaible
is correct for any k.
I notice that the examples usually are on a fixed-length word such as 32
word, 8 word. For instance, a lemma
lemma "0b110 AND 0b101 = (0b100 :: 5 word)" by simp
I want to have a lemma such as
lemma lemmaTest: "0b110 AND 0b101 = (0b100 :: k word)" by simp, where k is
any natural number which is greater than or equal to 3.
But obviously lemmaTest is not allowed in Isabelle.
How to formalize such a lemma? Or I can be shown some examples which
formalize the parameterized-word problems.
regards!
Email Gateway (Aug 22 2022 at 14:05):From: "C. Diekmann" <diekmann@in.tum.de>
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:
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
Last updated: Apr 20 2024 at 08:16 UTC