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)›
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
