Re: [isabelle] Efficient Lookups in Lists



A good solution might be to write a simplification procedure (or simproc) to 
solve these kinds of subgoals. A simproc is an ML function that takes a term 
t as an argument, and optionally returns a theorem of the form t == t'. You 
can learn more about them in the Isabelle reference manual.

For example, you could write some ML code that examines terms of the form x : 
A, checking to see whether term x occurs explicitly in the term A. If so, it 
could then build theorem of the form "x : A == True" using Eq_TrueI, insertI1 
and insertI2 together with some simple theorem combinators. If term x is not 
found in the term A, the simproc would just fail and do nothing (hopefully 
this is not the common case).

Note that since a simproc builds an actual theorem that proves the equality, 
you aren't adding anything to the trusted code base. You should still get a 
significant speedup, because the ML code would be much faster than making 
hundreds of recursive calls to the simplifier.

Hope this helps,
- Brian

On Tuesday 10 October 2006 04:57, Jan Olaf Blech wrote:
> 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.