# Re: [isabelle] Efficient Lookups in Lists

`There is one more solution possibility, you could use the compute oracle
``in Pure/Tools/compute.ML.
``It is already included in your Isabelle build (so it is somewhere
``between the "trusted base" and the rest :-)),
`you can invoke it by calling once
Compute.basic_make ....
and then each time you simplify a term by
Compute.rewrite ...
There are two major drawbacks to this method:
1. You can only simplify terms which contain no type variables.

`2. You have to configure the rewrite by calling Compute.basic_make and
``give it ALL the theorems used for rewriting;
` these theorems must not contain type variables, either;

`The no-type-variables limitation in 2) is not so bad if you know what
``types you can possibly have in your terms; you can just instantiate the
``polymorphic rewrite theorems with all types you need and give these to
``Compute.basic_make.
`

`I have used above technique successfully for fast matrix multiplication,
``gaining a speed-up-factor comparable to compilation.
``It is more trustworthy than compilation, though, because it builds
``directly on Pure and makes no additional assumptions.
`
Steven

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