# [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
### 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.