Re: [isabelle] Parametrized transfer rules with lift_definition

Hi Andreas,
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 MHonArc.