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
