Email Gateway (Aug 19 2022 at 11:04): Email Gateway (Aug 19 2022 at 11:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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).
Email Gateway (Aug 19 2022 at 11:14):From: Ondřej Kunčar <kuncar@in.tum.de>
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
Email Gateway (Aug 19 2022 at 11:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Ondřej,
Thank you for your suggestion, it works like a charm.
This only applies to the development version, e.g., 608afd26a476. As is good practice on
isabelle-users, I have back-ported my problem to Isabelle2013 where there are only
non-parametric correspondence relations. But you rightly guessed that I am actually
working with the development version.
By the way, I wrap the type "32 word" in a type of its own to do the usual code generation
refinement stuff. When I call setup_lifting with the type definition, it warns that it
cannot generate a parametrized correspondence relation failed because it could not find a
relator for the type "Numeral_Type.bit0". Honestly, I have no clue what a relator for
these numeral types should look like. Or is it OK to ignore the warning in this case?
Thanks again,
Andreas
Last updated: Apr 19 2024 at 01:05 UTC