Re: [isabelle] Automatic heuristic simplifier setup
Till Mossakowski schrieb:
Is there a general heuristic (perhaps even implemented) what should
be put into the Isabelle simplifier? Of course, this cannot replace
manual adpations; however, it could at least provide a good
Certainly nothing automated. And I would even have a hard time
describing my intuition.
A related question is: which kinds of loops are automatically
detected by the simplifier already?
The loop test works on a rule by rule basis. Given P ==> l = r it
rejects this orientation of the rule if
- there are extra variables in r not in l or P, or
- the head of l is a variable, or
- l occurs in r or P, or
- P is empty and l matches r, or
- l is a constant but r is not
If the opposite orientation also fails, P ==> (l=r) = True is added.
Is there work on using termination proof tools in this
context? Probably, commutativity rules would need to be
excluded when fedding a termination checker, because Isabelle
can handle them.
There is no such work. I suspect that trying to prove termination is
extremely hard and Isabelle specific. Detecting loops on the other hand
may be valuable, in particular for novices.
This archive was generated by a fusion of
Pipermail (Mailman edition) and