[isabelle-dev] warnings from "algebra" method

[Brian Huffman]

Nevermind, I managed to fix this one myself. It turns out that lemmas
Nat_Numeral.semiring_norm included iszero_simps twice (once directly,
and once via rel_simps). It appears that it has always had the
duplicate lemmas (ever since it was Groebner_Basis.norm_arith) but the
warning message must have been suppressed somehow until recently.

- Brian

On Tue, May 11, 2010 at 6:23 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:
> The following proof from Parity.thy:
>
> lemma even_times_anything: "even (x::int) ==> even (x * y)"
>  by algebra
>
> yields the following output:
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (0::?'a1) == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero Numeral0 == True
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (-1::?'a1) == False
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit0 ?w1)) == iszero (number_of ?w1)
>
> ### Ignoring duplicate rewrite rule:
> ### iszero (number_of (Int.Bit1 ?w1)) == False
>
> lemma even_times_anything: even ?x ==> even (?x * ?y)
>
>
> Similarly numerous warnings are produced by every other use of the
> "algebra" method I've come across.
>
> Hopefully someone will take care of this before the upcoming release.
>
> - Brian
>