Email Gateway (Aug 22 2022 at 17:09): Email Gateway (Aug 22 2022 at 17:09):From: Dominique Unruh <unruh@ut.ee>
Hello,
I have a case where the combination of Rewrite and Adhoc_Overloading breaks
the subst tactic. It is probably simplest to just show the minimal example:
theory Test3
imports "HOL-Library.Rewrite" Main
begin
end
theory Test
imports "HOL-Library.Adhoc_Overloading" Main Test3
begin
lemma a: "x+(x::nat) = 2*x" by auto
lemma b: "(1::nat)+(1::nat) = 2"
apply (subst a)
by simp
end
(It has two be split into two theory files.)
If I remove the imports for Rewrite or Adhoc_Overloading, the subst method
works as expected. If I move the import for Adhoc_Overloading to Test3, the
subst method works as well. But with this specific theory graph, subst does
not work.
What is happening?
And can this be fixed without adding Adhoc_Overloading as a dependency to
Test3?
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:09):From: Lars Hupel <hupel@in.tum.de>
Dear Dominique,
the problem is actually independent of "Test3". Instead, it is based on
the import order.
Namely, "Adhoc_Overloading" is itself based on "Pure", not "Main". That
means the import order matters.
This one works:
theory Test
imports Main "HOL-Library.Adhoc_Overloading"
begin
That one doesn't:
theory Test
imports "HOL-Library.Adhoc_Overloading" Main
begin
As to why exactly the order wrt "Pure"/"Main" is relevant, I don't know.
But I've seen this in the past:
<https://github.com/larsrh/libisabelle/commit/eaafee24a46dc9a99de75bcf55b7d3c8d27f71ca>.
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:13):From: Makarius <makarius@sketis.net>
Theory "HOL-Library.Adhoc_Overloading" extends Pure, so in a merge where
it is coming first, non-mergeable data components will have preference
over those from Main HOL -- notably operations from the Simplifier setup.
The "subst" method uses Simplifier.mksimps here:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Tools/eqsubst.ML#l53
-- with the Pure version it cannot work with HOL equalities.
Consequently, the following variation of the example works:
theory Test
imports "HOL-Library.Adhoc_Overloading" Main Test3
begin
lemma a: "x+(x::nat) ≡ 2*x" by (rule eq_reflection) auto
lemma b: "(1::nat)+(1::nat) = 2"
apply (subst a)
by simp
end
The session-qualified theory naming in Isabelle2017 causes some
confusion here: ~~/src/Tools/Adhoc_Overloading.thy becomes
"HOL-Library.Adhoc_Overloading", so it appears like it should be based
on Main HOL, but it isn't.
Anything not based on theory Main (or Complex_Main) is subject to the
rather complex HOL bootstrap process, and should normally not occur in
user-space -- it provokes surprises as shown here.
It is probably better to move Adhoc_Overloading.thy to
~~/src/HOL/Library and make it import Main. (I am in the process to try
this change of Isabelle + AFP.)
At some later stage, it should all be assimilated into Pure -- this
would solve other known problems of the current setup, especially in
conjunction with abbreviations.
Makarius
Email Gateway (Aug 22 2022 at 17:14):From: Lars Hupel <hupel@in.tum.de>
This change (Isabelle/81d90f830f99) broke HOLCF-Prelude in the AFP (see
attachment).
Email Gateway (Aug 22 2022 at 17:15):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
The easy fix would be to add (but I didn't do anything in the repo,
because I wanted to avoid potential clashes with others).
hide_const (open) List.nth
at the top of Definedness.thy. The problem was just that we define our
own "nth" (in Data_List) function but since "nth" is also defined in
Main and Definedness imports Adhoc_Overloading after Data_List. No
suddenly "nth" referred to List.nth instead of Data_List.nth.
cheers
chris
Email Gateway (Aug 22 2022 at 17:18):From: Makarius <makarius@sketis.net>
There are further hide commands that getoverridden by the merge with
Main from the right. This is another example of merge fragility.
I have now clarified the imports as in the included changeset.
Makarius
ch
Last updated: Apr 24 2024 at 01:07 UTC