Hi,

`We use Isabelle/HOL in a compiler runtime verification environment. The
``verification process comprises "lookup operations" in lists, function
``updates and sets, i.e. proving lemmata of the following form:
`
lemma "a mem [...,a,...]"
lemma "f (...,a:= b,...) a = b"
lemma "a : {...,a,...}"

`If the lists, function updates, and sets grow large, these lookups take
``up almost all of the time of a verification run. In our current version
``we instantiate Isabelle's simplifier with some simple rules like
`
"x = a | x : A ==> x : insert a A"

`to achieve time linear to the size of the underlying structure the
``lookup is conducted on.
``However a lookup still takes quite long: several minutes for a list of a
``few thousand elements. For the verification of some relatively small
``programs thousands of lookups are needed in structures containing
``thousands of elements.
`
Is anyone aware of a technique to do this faster?

`What do you think of "bypassing" Isabelle's simplifier to make such
``lookups faster? One problem is probably that we would "spoil" the
``Isabelle implementation and the "trusted computing base" would grow larger.
`
Regards
Jan Olaf Blech