Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Hannes Verlinde <Hannes.Verlinde@UGent.be>
I am experimenting in Isabelle/Isar with an object-logic that represents
equational propositional logic (using the calculational patterns provided by
Isar). In the theory, there are just a few inference rules (meta-level
axioms):
Leibniz [intro] : “P = Q ==> E P = E Q”
Transitivity [trans] : “[P = Q; Q = R] ==> P = R”
Equanimity [trans] : “[P = Q; Q] ==> P”
There are also a few derived inference rules (meta-level theorems) that are
simple variations of the rules above. By annotating the rules with the
attributes [intro] and [trans], I don’t have to mention them explicitly in
the Isar proofs. Writing “by rule” will make the system pick a rule
annotated with [intro] and the rules annotated with [trans] will be used
implicitly when chaining calculations with “also” and “finally”.
All of this works fine but it does feel a bit strange to label rule Leibniz
as an introduction rule (or as an elimination rule, or as a symmetry rule).
Note that I don’t really use classical reasoning in my theory. Is it ok to
somewhat “abuse” these attributes in order to obtain the effect of the rules
being automatically selected by the system? I would expect that there is
some annotation like [standard] that simply declares a rule to be a
“standard” rule without forcing the user to classify it as an introduction
or elimination rule. Is there any source that explains clearly which
attributes should be used for which kind of rules and what the consequences
are exactly?
Thanks in advance for any help or comments.
Hannes Verlinde
Ghent University
Email Gateway (Aug 17 2022 at 13:27):From: Makarius <makarius@sketis.net>
On Wed, 19 Oct 2005, Hannes Verlinde wrote:
Leibniz [intro] : "P = Q ==> E P = E Q"
Transitivity [trans] : "[P = Q; Q = R] ==> P = R"
Equanimity [trans] : "[P = Q; Q] ==> P"
By annotating the rules with the attributes [intro] and [trans], I don't
have to mention them explicitly in the Isar proofs. Writing "by rule"
will make the system pick a rule annotated with [intro]
Just note that ..'' abbreviates by rule'' (more precisely `by
default'' which includes the rule method as well). Also, the system will
pick elim rules in the same manner if you are using' suitable facts to be
eliminated.
All of this works fine but it does feel a bit strange to label rule Leibniz
as an introduction rule (or as an elimination rule, or as a symmetry rule).
The conclusion of Leibniz is indeed rather general, and apt to cause
pathological cases for higher-order unification. If you always provide
the left equality first the situation will be much more predictable. So
maybe declare it as elim, then the system will only try to use it if there
are any facts being used, but not in a purely backward proof step.
Note that I don't really use classical reasoning in my theory. Is it ok
to somewhat "abuse" these attributes in order to obtain the effect of
the rules being automatically selected by the system?
It is basically OK, but may prevent you from using the automated classical
proof tools as expected later on. Alternatively, you may use Pure.intro
or intro? instead, which do not affect the classical proof tools. See
also appendix A of the isar-ref manual for a table of rule declarations
and methods.
Makarius
Last updated: May 03 2024 at 08:18 UTC