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


In the afp entry native words, theory uint, we did such a setup. We define a len-type dflt_size (your k) which is only known to be positive.

Hope this helps

-------- Originalnachricht --------
Betreff: [isabelle] a question of formalization of parameterized-word (bit-vector)
Von: Li Yongjian
An: isabelle-users

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.


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