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

    ==

  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





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