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
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