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

[Stefan Berghofer]

On 03/05/10 22:34, Brian Huffman wrote:
> The datatype package produces some extra warning messages now too:
> 
> ### Ignoring duplicate rewrite rule:
> ### True == induct_true
> 
> ### Ignoring duplicate rewrite rule:
> ### False == induct_false
> 
> I haven't checked, but I would be willing to bet that this behavior
> was introduced by the same changeset as the function package warning
> messages. I wouldn't be surprised if warnings pop up in other packages
> as well.

Hi Brian,

no, these warning messages had a different reason. I introduced this
problem when adding new infrastructure for the pre-simplification of
goals produced by the induct and cases methods. These methods now
delete trivial goals (corresponding to cases that cannot occur)
and simplify non-trivial goals using injectivity and distinctness
theorems for datatypes (as well as other rules that can be declared
by the user). The above warning was generated by the code for
preprocessing these simplification rules. It should no longer
occur in the current repository version of Isabelle.

Greetings,
Stefan

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe