*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Efficient Lookups in Lists*From*: Brian Huffman <brianh at csee.ogi.edu>*Date*: Wed, 11 Oct 2006 14:23:07 -0700*Cc*: Jan Olaf Blech <blech at informatik.uni-kl.de>*In-reply-to*: <web-32417524@uni-kl.de>*References*: <web-32417524@uni-kl.de>*User-agent*: KMail/1.8

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

**References**:**[isabelle] Efficient Lookups in Lists***From:*Jan Olaf Blech

- Previous by Date: Re: [isabelle] Efficient Lookups in Lists
- Next by Date: [isabelle] Fun in the Afternoon: Thurs 16th Nov in Oxford
- Previous by Thread: Re: [isabelle] Efficient Lookups in Lists
- Next by Thread: [isabelle] monotonicity lemmas for embedded lists
- Cl-isabelle-users October 2006 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