[isabelle-dev] CONTEXT exception after locale interpretation with setup_lifting

[Traytel Dmitriy]

Hi Makarius,

> On 14 Mar 2020, at 22:25, Makarius <makarius at sketis.net> wrote:
> 
> On 28/02/2020 17:44, Traytel Dmitriy wrote:
>> 
>> I found the following interaction of setup_lifting and locale interpretations
>> surprising. In the below example, the first two local_setup's succeed, whereas
>> the third one fails with a CONTEXT exception in Isabelle/b94053ca8d77. And
>> this failure occurs despite the fact that Lifting_Info.lookup_quotients
>> already invokes Morphism.transfer_morphism. All three local_setup's work in
>> Isabelle2019. If I were to guess, I believe this has to do with the
>> commit c82f59c47aaf, which changes the meaning of Morphism.transfer_morphism.
>> But I have to admit that I don't understand the Context.subthy_id check in the
>> Thm.join_transfer function that is introduced there.
> 
> Bisection yields the following result:
> 
> changeset:   70472:9179e7a98196
> user:        wenzelm
> date:        Tue Aug 06 17:26:40 2019 +0200
> files:       src/HOL/Tools/Lifting/lifting_def.ML
> src/HOL/Tools/Lifting/lifting_info.ML src/HOL/Tools/Lifting/lifting_setup.ML
> src/HOL/Tools/Transfer/transfer.ML
> description:
> clarified signature;
> more careful treatment of implicit context;
> 
> The problem is in Thm.join_transfer from here:
> changeset:   70310:c82f59c47aaf
> user:        wenzelm
> date:        Mon Jun 03 20:09:43 2019 +0200
> files:       src/Pure/morphism.ML src/Pure/thm.ML
> description:
> clarified transfer_morphism: implicit join_certificate, e.g. relevant for
> complex cascades of morphisms such as class locale interpretation;
> 
> I have now amended that here:
> changeset:   71553:cf2406e654cf
> tag:         tip
> user:        wenzelm
> date:        Sat Mar 14 21:58:29 2020 +0100
> files:       src/Pure/thm.ML
> description:
> more robust: proper transfer if Context.eq_thy_id;
> 
> 
> Thus it also fits better to Thm.join_transfer_context.

Great, thanks! Your change allowed me to remove a workaround of an additional Thm.transfer in lift_bnf (c.f. isabelle/1cf958713cf7).

I pushed this to the post-release dev-repository. I don't think that this changes anything observable for users. So it is probably fine if the release still includes the workaround.

Dmitriy