Re: [isabelle] Efficient Lookups in Lists
There is one more solution possibility, you could use the compute oracle
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
and then each time you simplify a term by
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and