Re: [isabelle] Transfer: types in skeleton are too specific



Hi Ondrej,

Thanks for digging into this. I'll live with the workaround until the bug is resolved.

Best,
Andreas

On 18/10/16 16:50, OndÅej KunÄar wrote:
Hi Andreas,
this is a bug in the procedure that tries to preinstantiate some of the schematic
variables to cut down the search space. The procedure got confused because part of your
term got eta contracted after transfer internally universally quantified over the free
variables.

A possible workaround:
Quantify explicitly over n: "ân. foo c (f2 i) n".

Ondrej

On 10/17/2016 01:30 PM, Andreas Lochbihler wrote:
Dear experts of the transfer package,

I have a problem with the transfer method (theory attached,
Isabelle2016). In the lemma, transfer is supposed to replace the
function f2 with the function f1 using the parametricity theorem for the
operator foo (and thereby replace the natural number i with an integer i
in the domain of cr).

However, the proof does not go through, because the expected transfer
relation for foo (second goal after transfer_start) has a too specific
type. In detail, the relation ?Rg12 has type "bool â (nat â bool) â
bool", but it should be something like "(nat â bool) â (nat â bool) â
bool" or "?'a â (nat â bool) â bool".

Where does this restricted type come from? And how can I make transfer
work for this example?

Thanks,
Andreas






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