Re: [isabelle] Parametrized transfer rules with lift_definition
there is a brief description of the algorithm in my thesis in Â4.3. That
description should give you a good overview how the procedure works.
I can answer additional questions if needed.
On 06/10/2016 05:32 PM, Andreas Lochbihler wrote:
Dear Lifting experts,
I am looking for some documentation on how the Lifting tool derives the
parametrised transfer rules from the parametricity theorem. In some
cases, lift_definition reports that it was not able to merge certain
terms. I'd like to understand how this works and its limitations. I have
a different application in mind (strengthening parametricity theorems
with congruence rules) and would like to understand whether the same
approach could work there.
This archive was generated by a fusion of
Pipermail (Mailman edition) and