<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">
<span class="">Hi Makarius,<br class="">
</span><span class=""><br class="">
</span><span class="">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. </span><span style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);" class="">All three local_setup's work in Isabelle2019. </span><span class="">If
I were to guess, I believe this has to do with the commit </span><span class="">c82f59c47aaf, which changes the meaning of </span><span style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);" class="">Morphism.t</span><span class="">ransfer_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.</span>
<div class=""><span class=""><br class="">
</span></div>
<div class=""><span class="">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.</span></div>
<div class=""><span class=""><br class="">
</span></div>
<div class=""><span class="">Cheers,</span></div>
<div class=""><span class="">Dmitriy<br class="">
</span><span class=""><br class="">
</span>
<div class=""><font face="monospace" class="">typedef 'a x = "UNIV :: 'a set" by blast</font></div>
<div class=""><font face="monospace" class=""><br class="">
</font></div>
<div class=""><font face="monospace" class="">locale A begin setup_lifting type_definition_x end</font></div>
<div class=""><font face="monospace" class=""><br class="">
</font></div>
<div class=""><font face="monospace" class="">ML ‹val Qt_thm = @{thm Quotient_transp}›</font></div>
<div class=""><font face="monospace" class=""><br class="">
</font></div>
<div class=""><font face="monospace" class="">context begin</font></div>
<div class=""><font face="monospace" class="">interpretation A .</font></div>
<div class=""><font face="monospace" class=""><br class="">
</font></div>
<div class=""><font face="monospace" class="">local_setup ‹fn lthy =></font></div>
<div class=""><font face="monospace" class=""> (Lifting_Info.lookup_quotients lthy @{type_name x} |> the |> #quot_thm |> Thm.transfer' lthy</font></div>
<div class=""><font face="monospace" class=""> |> (fn thm => thm RS Qt_thm) |> @{print};</font></div>
<div class=""><font face="monospace" class=""> lthy)›</font></div>
<div class=""><font face="monospace" class=""><br class="">
</font></div>
<div class=""><font face="monospace" class="">local_setup ‹fn lthy =></font></div>
<div class=""><font face="monospace" class=""> (Lifting_Info.lookup_quotients lthy @{type_name x} |> the |> #quot_thm</font></div>
<div class=""><font face="monospace" class=""> |> (fn thm => thm RS (Qt_thm |> Thm.transfer' lthy)) |> @{print};</font></div>
<div class=""><font face="monospace" class=""> lthy)›</font></div>
<div class=""><font face="monospace" class=""><br class="">
</font></div>
<div class=""><font face="monospace" class="">local_setup ‹fn lthy =></font></div>
<div class=""><font face="monospace" class=""> (Lifting_Info.lookup_quotients lthy @{type_name x} |> the |> #quot_thm</font></div>
<div class=""><font face="monospace" class=""> |> (fn thm => thm RS Qt_thm) |> @{print};</font></div>
<div class=""><font face="monospace" class=""> lthy)›</font></div>
</div>
</body>
</html>