Email Gateway (Aug 18 2022 at 12:19): Email Gateway (Aug 18 2022 at 12:19):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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 _^*)?
cheers
christian
Email Gateway (Aug 18 2022 at 12:19):From: Clemens Ballarin <ballarin@in.tum.de>
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).
Cheers,
Clemens
Last updated: May 03 2024 at 04:19 UTC