*To*: Li Yongjian <lyj238 at gmail.com>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] a question of formalization of parameterized-word (bit-vector)*From*: Peter Lammich <lammich at in.tum.de>*Date*: Sun, 11 Sep 2016 09:20:38 +0200

Hi

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

Peter

-------- Originalnachricht --------

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

Von: Li Yongjian

An: isabelle-users

Cc:

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!

- Previous by Date: [isabelle] a question of formalization of parameterized-word (bit-vector)
- Next by Date: Re: [isabelle] a question of formalization of parameterized-word (bit-vector)
- Previous by Thread: Re: [isabelle] a question of formalization of parameterized-word (bit-vector)
- Next by Thread: [isabelle] Problems on auto solving in some basic arithmetic simplication
- 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