[isabelle-dev] Arith fails with a "Type error in application"

[Dennis Walter]

Hi there,

I just discovered a probably undesired behaviour of the arith proof method:

The following proof works fine if "Quick&Dirty" is enabled, i.e. in
interactive mode. But if this proof is re-run with Q&D turned off
(e.g. in batch mode), the proof fails, because arith yields the error
displayed below.

lemma "[| 1 <= (a::int); 1 <= (b::int) |] ==> 1 <= a * b"
  apply (subgoal_tac " EX a' b'. a = 1 + a' & b = 1 + b' & 0 <= a' & 0 <= b'")
  apply (clarsimp simp add: ring_simps add_nonneg_nonneg mult_nonneg_nonneg)
  apply arith
done

*** Type error in application: Incompatible operand type
***
*** Operator:  (op * 1) :: int => int
*** Operand:   {1} :: int => bool
***
*** The error(s) above occurred for the goal statement:
*** (1 : {1}) = (0 : 1 * {1} + -1)
*** At command "apply".

The problem is not very urgent (for me), since simp can solve it, too,
if I provide the necessary instantiations "a - 1" and "b - 1", but I
thought I'd let you know about it.

Regards,
  Dennis