[isabelle] Transfer: types in skeleton are too specific



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

Attachment: Scratch.thy
Description: application/example



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