Re: [isabelle] Transitivity reasoning and eta-expansion

On Wed, 14 Nov 2007, Peter Lammich wrote:

> I want to do transitivity reasoning. So I declare the transitivity lemma 
> as [trans]. The problem is now, that everything works until I have a 
> reflexivity step. In this case, the goal gets eta-expanded at the next 
> 'also', causing the transitivity reasoner to fail.

Eta-expansion should not be a problem here, because higher-order 
unifications works module eta (and alpha and beta).  You should be able to 
compose these facts manually, using something like

  thm ah_leq.trans [OF fact1 fact2]

The reason why 'also' fails is different: due to the reflexivity step in 
the chain, there is no progress in the calculation.  Such facts are 
filtered out from the sequence of possible results -- an empty sequence is 
left over.

The deeper reason why this is done is higher-order unification again: 
certain pathological cases of substitution result in no-progress steps.  
The filtering scheme nicely circumvents this.  So you merely loose 
reflexivity (which is not very interesting anyway), but gain many useful 
applications of substitution (of equalities or inequalities).


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