Re: [isabelle] Question about attribute annotations: [trans], [sym], [elim], [intro] etc. (Isabelle/Isar)



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.