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

[Traytel Dmitriy]

Hi Makarius,

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.

Another datapoint: if I omit the locale interpretation or add some definition (e.g., "foo = True") or some datatype declaration after the locale interpretation but before the offending local_setup, the CONTEXT exception disappears.

Cheers,
Dmitriy

typedef 'a x = "UNIV :: 'a set" by blast

locale A begin setup_lifting type_definition_x end

ML ‹val Qt_thm = @{thm Quotient_transp}›

context begin
interpretation A .

local_setup ‹fn lthy =>
  (Lifting_Info.lookup_quotients lthy @{type_name x} |> the |> #quot_thm |> Thm.transfer' lthy
  |> (fn thm => thm RS Qt_thm) |> @{print};
  lthy)›

local_setup ‹fn lthy =>
  (Lifting_Info.lookup_quotients lthy @{type_name x} |> the |> #quot_thm
  |> (fn thm => thm RS (Qt_thm |> Thm.transfer' lthy)) |> @{print};
  lthy)›

local_setup ‹fn lthy =>
  (Lifting_Info.lookup_quotients lthy @{type_name x} |> the |> #quot_thm
  |> (fn thm => thm RS Qt_thm) |> @{print};
  lthy)›
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200228/601e6394/attachment.html>