[isabelle-dev] Function package produces "duplicate rewrite rule" warnings

[Alexander Krauss]

Hi Brian,

Thanks for bisecting this, I'll have a look.

Alex

Brian Huffman wrote:
> Recent versions of the function package produce some unhelpful warning
> messages about duplicate rewrite rules:
> 
> ### Ignoring duplicate rewrite rule:
> ### Sum_Type.Projl (Inl ?y) == ?y
> 
> ### Ignoring duplicate rewrite rule:
> ### Sum_Type.Projr (Inr ?y) == ?y
> 
> I discovered the warnings when using Library/Nat_Bijection.thy, but as
> far as I can tell, every invocation of the "fun" command now produces
> a similar warning.
> 
> I did a search using "hg bisect" and identified the following revision
> as the source of the problem:
> 
> The first bad revision is:
> changeset:   36594:5c5b5c7f1157
> parent:      36560:8da6846b87d9
> user:        wenzelm
> date:        Fri Apr 30 17:18:29 2010 +0200
> summary:     conditional warnings: explicitly observe context
> visibility flag, not just accidental presence of a context;
> 
> http://isabelle.in.tum.de/repos/isabelle/rev/5c5b5c7f1157
> 
> The specific rules mentioned in the warning message are used in
> HOL/Tools/Function/sum_tree.ML:
> 
> val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}]
> 
> In turn, "proj_in_rules" is used in HOL/Tools/Function/mutual.ML as
> part of function "recover_mutual_psimp", where those rules are
> explicitly added to a simpset. Since the rules are (usually) already
> in the simpset, it produces a warning. Prior to revision 5c5b5c7f1157,
> that warning was suppressed (as it should be), but that is no longer
> the case.
> 
> I suppose that fixing this would require modifying the function
> package to set the "context visibility flag" correctly, but I don't
> know how to do that -- hopefully someone else does?
> 
> - Brian
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev