Email Gateway (Aug 18 2022 at 16:05): Email Gateway (Aug 18 2022 at 16:05):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,
do I understand correctly that a lemma declared as [iff] is added as
simplification rule (from left to right) as well as intro/elim rule?
What happens with equations? What kind of intro/elim rules do I get from
a lemma "A = B". More importantly, is it safe to declare a rule as [iff]
(e.g., if I had two different characterizations of A, namely B and C,
would it be safe to add [iff]: "A = B" and [iff]: "A = C" or does it
depend on the weather afterwards, whether automation does still what I
want)?
best regards
chris
Email Gateway (Aug 18 2022 at 16:05):From: Lawrence Paulson <lp15@cam.ac.uk>
The attribute [iff] attempts to transform the supplied theorems into introduction and elimination rules sensibly. If the supplied theorem is a non-boolean equality (or other atomic formula), then there is no elimination rule, and the theorem is given the attribute [intro!].
Larry Paulson
Last updated: Apr 20 2024 at 12:26 UTC