Re: [isabelle] Applying elimination rules
On Thu, 21 Sep 2006, Vaidas Gasiunas wrote:
> 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)
That's adequate. Also note the canonical pattern ``by (cases set: myrel)
auto'' or just ``by cases auto''. This assumes that the frist 'from' fact
is the relation you intend to eliminate.
Recall that 'by' abbreviates 'proof ... qed ...', with both an initial
method and an optional terminal one. Facts are passed to the initial
method expression, but are reset afterwards ('apply' also resets facts).
This means that the 'cases' above will eliminate the primary myrel
judgment and insert all the remaining facts; then auto operates on the
remaining goal state alone.
> 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.
The following transformation is valid in general (modulo backtracking):
by meth1 meth2
So ``by - (erule myrule, auto)'' would do the job,
but ``by (rule myrule) auto'' is slightly more appropriate.
This archive was generated by a fusion of
Pipermail (Mailman edition) and