Re: [isabelle] Transfer: types in skeleton are too specific
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".
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and