Re: [isabelle] attribute 'standard'

Hi Christian,

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:

Hi there,

from the ISAR reference manual I do not really get the meaning of the attribute 'standard'... the reason why I'm asking is the following:

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 MHonArc.