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

[Tjark Weber]

On Fri, 2009-08-21 at 19:19 +0200, Dennis Walter wrote:
> 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

With Toplevel.debug set, I get the following exception trace, which
leads me to suspect that the problem is somewhere in "presburger".

Regards,
Tjark

========== 8< ==========

Exception trace for exception - ERROR
Goal.prove_common(6)err(1)
List.map(2)
Goal.prove_common(6)
Cooper.provelin(2)
Cooper.linearize_conv(3)/3
Cooper.linearize_conv(3)
Conv.combination_conv(3)
Conv.combination_conv(3)
Conv.combination_conv(3)
Conv.then_conv(3)
Conv.then_conv(3)
Qelim.gen_qelim_conv(8)conv(2)
Conv.combination_conv(3)
Conv.combination_conv(3)
Conv.then_conv(3)
Qelim.gen_qelim_conv(8)conv(2)
Conv.combination_conv(3)
Conv.combination_conv(3)
Conv.combination_conv(3)
Conv.then_conv(3)
Qelim.gen_qelim_conv(8)conv(2)
Conv.combination_conv(3)
Conv.then_conv(3)
Conv.then_conv(3)
Cooper.conv(2)
Conv.combination_conv(3)
Presburger.core_cooper_tac(1)(2)
Tactical.CSUBGOAL(3)
Tactical.CSUBGOAL(3)
Tactical.CSUBGOAL(3)
Seq.INTERVAL(4)
Seq.map(2)(1)
Seq.flat(1)(1)
Seq.map(2)(1)
Seq.flat(1)(1)
Tactical.ORELSE(1)(1)
Seq.map(2)(1)
Seq.flat(1)(1)
Seq.append(2)copy(1)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Toplevel.proofs'(1)(1)(1)
Runtime.debugging(2)(1)
End of trace