[isabelle-dev] warnings from "algebra" method

[Brian Huffman]

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