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

Sascha Boehme boehmes at in.tum.de
Wed Aug 26 13:31:20 CEST 2009


This bug has already been fixed, see

  http://isabelle.in.tum.de/repos/isabelle/rev/40a0760a00ea

Regards,
Sascha


Tjark Weber wrote:
> 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
> 
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



More information about the isabelle-dev mailing list