Re: [isabelle] Parametrized transfer rules with lift_definition
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
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 (subst all_comm)
apply (subst all_conj_distrib[symmetric])
apply (intro choice)
Why are these rules not needed?
On 13/06/16 20:08, OndÅej KunÄar wrote:
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