[isabelle] Applying elimination rules



Hello,

I work with inductively defined relations and often have a case when I 
need get conditions for some specific case of the relation. This can be 
done with elimination rule, which is automatically generated for the 
relation. Usually I apply the rule in such pattern:

from ... obtain ... where ... by (auto elim: myrel.elims)

However, in some cases this pattern does not work; then I apply another 
pattern, which succeeds more often:

from ... obtain ... where ... apply - apply(erule myrel.elims) 
apply(auto) done

It seems that the second pattern should be equivalent to "by (-, erule 
myrule, auto)", but the latter does not work. Is there any way to 
express the second pattern compactly in a "by" clause?

Greetings,
Vaidas 

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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