# [isabelle] Efficient Lookups in Lists

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

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