*To*: OndÅej KunÄar <kuncar at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Parametrized transfer rules with lift_definition*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 14 Jun 2016 09:40:03 +0200*In-reply-to*: <dfe427b1-3f6a-384f-5cc0-fdae36ef69e6@in.tum.de>*References*: <575ADD90.5030305@inf.ethz.ch> <dfe427b1-3f6a-384f-5cc0-fdae36ef69e6@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

Dear Ondrej, Thanks for the pointer. The last sentence of this section is what I am wondering about: I implemented a procedure that can do all of those steps automatically.

lemma neg_fun_distr3: assumes 1: "left_unique R" "right_total R" and 2: "right_unique S" "left_total S" shows "R OO R' ===> S OO S' â (R ===> S) OO (R' ===> S')" using functional_converse_relation[OF 1] functional_relation[OF 2] unfolding rel_fun_def OO_def apply clarify apply (subst all_comm) apply (subst all_conj_distrib[symmetric]) apply (intro choice) by metis Why are these rules not needed? Best, Andreas On 13/06/16 20:08, OndÅej KunÄar wrote:

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. Bests, Ondrej 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. Best, Andreas

**Follow-Ups**:**Re: [isabelle] Parametrized transfer rules with lift_definition***From:*OndÅej KunÄar

**References**:**[isabelle] Parametrized transfer rules with lift_definition***From:*Andreas Lochbihler

**Re: [isabelle] Parametrized transfer rules with lift_definition***From:*OndÅej KunÄar

- Previous by Date: Re: [isabelle] Parametrized transfer rules with lift_definition
- Next by Date: Re: [isabelle] Opaque ascription for SML code generation
- Previous by Thread: Re: [isabelle] Parametrized transfer rules with lift_definition
- Next by Thread: Re: [isabelle] Parametrized transfer rules with lift_definition
- Cl-isabelle-users June 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list