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



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.