Re: [isabelle] attribute 'standard'
transitivity is dealt with in the simplifier by a solver. The set up
is at the end of ~~/src/HOL/Transitive_Closure.thy. The solver is
needed since transitivity rules normally make the simplifier loop.
In order to configure it for your own closure operation, you need to
supply the right lemmas and a function decomp, which identifies
suitable assumptions in the subgoal. Follow the instructions in ~~/
src/Provers/trancl.ML. Get in touch if there are questions (or if
your transitivity hold relative to a locale).
On 19 Aug 2008, at 10:36, Christian Sternagel wrote:
from the ISAR reference manual I do not really get the meaning of
the attribute 'standard'... the reason why I'm asking is the
I observed that transitivity of _^* is applied automatically, but I
didn't find any [simp] declaration that would explain this to me.
No I have my own closure operation on sets that is also transitive
and I would like transitivity to be applied automatically to. So
how do I set up a corresponding lemma (and how was it down for _^*)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and