# [isabelle] Problem with command-line version

Dear all,
consider the following easy proof:
theory Scratch imports Rational
begin
lemma True
proof -
{
fix a :: int
have "∃ b. a = a * b ∧ b > 0" by auto
then obtain b where "a = a * b" and "b > 0" by auto
hence "∃ c. b = c + (1 :: int) ∧ c ≥ 0" by arith
hence True by simp
}
thus ?thesis .
qed
end
When stepping through the proof interactively, everything works fine.

`However, when using isabelle-process (Isabelle 2009), I get the
``following error message
`for the proof step where arith is applied.
> val it = () : unit
val commit = fn : unit -> bool
Loading theory "Scratch"
### Trying linear arithmetic...
### Linear arithmetic failed - see trace for a counterexample.
Counterexample (possibly spurious):
a = 0, a * b = 0, b = 1
### Trying Presburger arithmetic...
Search depth = 0
*** 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)
*** (line 10 of "/Users/rene/Scratch.thy")
Is this a known phenomena with arith?

`(I rewrote the proof to use exI instead of arith, then both command-
``line and
`interactive version are happy.)
Best regards,
René

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*