Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Applying elimination rules

view this post on Zulip Email Gateway (Aug 18 2022 at 09:41):

From: Vaidas Gasiunas <gasiunas@informatik.tu-darmstadt.de>
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
smime.p7s

view this post on Zulip Email Gateway (Aug 18 2022 at 09:41):

From: Makarius <makarius@sketis.net>
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

==

apply meth1
apply meth2
apply (assumption+)?
done

So by - (erule myrule, auto)'' would do the job, but by (rule myrule) auto'' is slightly more appropriate.

Makarius

Last updated: May 03 2024 at 12:27 UTC