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.