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

I looked at the procedure again and here is a more detailed description:

R <= R' ==> list_all R <= list_all R' (monotonicity of list_all).

R >= R' ==> S <= S' ==> (R ===> S) <= (R' ===> S') Thus, we are suddenly proving the other direction R >= R'. This is how it happens that we need neg_fun_distr1 and and neg_fun_distr2.

Ondrej On 06/14/2016 09:40 AM, Andreas Lochbihler wrote:

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. The problem is that the function relator rel_fun does not distribute over relation composition op OO. The comment in Lifting.thy indicates that the theorems pos_fun_distr, neg_fun_distr1, and neg_fun_distr2 take the role of distributivity for functions. It seems as if the latter two are used only for higher-order arguments, but it is not yet clear to me which of the two covers which cases. They have preconditions on the relations like left_unique and right_total. How do you make sure that they can be used for the relations? neg_fun_distr2 only has assumptions about the relations on the right hand side of OO, so this will affect only the correspondence relation, so lift_definition has some control over this. But what about neg_fun_distr1 and its assumptions on relations on the left? Also, one could prove two more rules of the kind of neg_fun_distr1 and neg_fun_distr2. For example, 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:*Andreas Lochbihler

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

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

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

- Previous by Date: Re: [isabelle] Parametricity for functions which ignore arguments
- Next by Date: [isabelle] ITP 2016: Call for participation
- 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