Re: [isabelle] simprocs for transitive closures of finite relations

> And a more general question: Are methods (tactics, simprocs, ...) that
> use "eval" in some way or another to be avoided? (I can't quite recall
> whether "regexp" relies on "eval".)

From my point of view, proof devices should never rely on the
(accidental) code setup at the time of their actual invocation but use a
fixed setup as present at their time of creation (»static evaluation«).
 The tutorial on code generation gives some further hints.

The other question is indeed how much you want your proof procedure be
hardwired against code generation.  I have no strict answer.  NBE could
be an alternative to allow free variables also.  The simplifier would
even be LCF-style.  Depends on the kind and size of problems you want to



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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