*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Transfer rule for undefined*From*: Ondřej Kunčar <kuncar at in.tum.de>*Date*: Thu, 06 Jun 2013 14:35:15 +0200*In-reply-to*: <51A7674E.1040103@inf.ethz.ch>*References*: <51A7674E.1040103@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130329 Thunderbird/17.0.5

Hi Andreas,

OK, how to make your example working:

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).

**Follow-Ups**:**Re: [isabelle] Transfer rule for undefined***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Custom Haskell serialisation for datatype constructors
- Next by Date: Re: [isabelle] Transfer rule for undefined
- Previous by Thread: Re: [isabelle] No code equations for explode on String.literal
- Next by Thread: Re: [isabelle] Transfer rule for undefined
- Cl-isabelle-users June 2013 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