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 _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
