Re: [isabelle] Transfer rule for undefined



Hi Andreas,
the issue with undefined is on my to-do list. I think your solution is on the right track. When I have more time, I will make something more robust to deal with undefined.

OK, how to make your example working:
1) Quotient_my_int and Quotient_my_nat uses non-parametric correspondence relation cr_my_int and cr_my_nat, whereas the transfer rules uses pcr_my_int and pcr_my_nat. In this case you can just use my_int.pcr_cr_eq and my_nat.pcr_cr_eq to change the former relations to the latter ones. 2) identity_quotient should be always before all rules for other types, thus it is used at the very end. 3) I think this theorem should be enough to generate transfer rules for undefined on the fly:
lemma undefined_transfer_better:
  assumes "Quotient R Abs Rep T"
  shows "T (Rep undefined) undefined"
using assms unfolding Quotient_alt_def by blast

Thus the result is:
lemmas [transfer_rule] = identity_quotient fun_quotient
  Quotient_my_int[unfolded my_int.pcr_cr_eq[symmetric]]
  Quotient_my_nat[unfolded my_nat.pcr_cr_eq[symmetric]]
  undefined_transfer_better

Ondrej

On 05/30/2013 04:50 PM, Andreas Lochbihler wrote:
Dear developers of lifting/transfer,

First of all, I'd like to thank all of you for this great tool, I am now
using it all the time. Unfortunately, I keep proving different transfer
rules for the constant undefined over and over again, although they all
have the same shape.

The following example illustrates my setting:

typedef my_int = "UNIV :: int set" .. setup_lifting type_definition_my_int
typedef my_nat = "UNIV :: nat set" .. setup_lifting type_definition_my_nat

lift_definition P :: "my_int => bool" is "op > 0" .
lift_definition foo :: "my_int => bool => my_nat" is "%i _. nat i" .
lift_definition my_int_of_my_nat :: "my_nat => my_int" is int .

definition bar :: "my_int => bool => my_nat"
   where "bar i b = (if P i then undefined i b else foo i b)"

lemma "foo (my_int_of_my_nat n) b = bar (my_int_of_my_nat n) b"
   unfolding bar_def
   apply transfer

This gives me the following second subgoal for undefined:

   Transfer.Rel (fun_rel cr_my_int (fun_rel op = cr_my_nat)) ?ah23
undefined

So far, I just proved this transfer rule for an appropriate
instantiation of ?ah23, but I have to prove similar goals with different
combinations of fun_rel, cr_... etc. So I tried to prove a generic
transfer lemma for quotients:

lemma undefined_transfer:
   assumes Q1: "Quotient A Abs1 Rep1 cr1"
   and Q2: "Quotient B Abs2 Rep2 cr2"
   shows "(fun_rel cr2 cr1) (Rep1 o undefined o Abs2) undefined"
by(auto dest!: Q2[unfolded Quotient_alt_def, THEN conjunct1, rule_format]
      intro!: Q1[unfolded Quotient_alt_def, THEN conjunct2, THEN
conjunct1, rule_format])

With this lemma, I can prove all these rules for undefined -- in the
running example:

apply(unfold Rel_def)
apply(rule undefined_transfer fun_quotient identity_quotient
         Quotient_my_nat Quotient_my_int)+

Unfortunately, I did not manage to have transfer prove these rules on
the fly. How can I get there? The following declarations do not suffice:

lemmas [transfer_rule] =
   undefined_transfer Quotient_my_int Quotient_my_nat fun_quotient
identity_quotient

Thanks in advance for any help,
Andreas

PS: The example is from Isabelle2013, but it is similar in the
development version (id 13171b27eaca).





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.