*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Question about attribute annotations: [trans], [sym], [elim], [intro] etc. (Isabelle/Isar)*From*: "Hannes Verlinde" <Hannes.Verlinde at UGent.be>*Date*: Wed, 19 Oct 2005 14:25:25 +0200*Importance*: Normal*Organization*: Ghent University*Reply-to*: Hannes.Verlinde at 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 -- |

**Follow-Ups**:

- Previous by Date: Re: [isabelle] Metalogical "spec" not resolved automatically
- Next by Date: [isabelle] segmentation fault solution
- Previous by Thread: Re: [isabelle] Metalogical "spec" not resolved automatically
- Next by Thread: Re: [isabelle] Question about attribute annotations: [trans], [sym], [elim], [intro] etc. (Isabelle/Isar)
- Cl-isabelle-users October 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list