Re: [isabelle] Parametrized transfer rules with lift_definition

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?


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.


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.