Re: [isabelle] Strange interaction between Rewrite and Adhoc_Overloading



On 29/04/18 14:12, Dominique Unruh wrote:
> 
> That is:
> 
>   imports Main "HOL-Library.Adhoc_Overloading" Test3
> 
> does not work. But
> 
>   imports Main Test3 "HOL-Library.Adhoc_Overloading"
> 
> does. (Probably because of the Main.)
> 
> I guess as a rule of thumb, one should import Adhoc_Overloading always last.
> 
> But I would still be curious what actually happens here.

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.