# Re: [isabelle] Problem with command-line version

Dear René,
This problem has already been discovered and fixed a few months ago.
The next release will not exhibit this behaviour anymore.
Regards,
Sascha
René Thiemann wrote:
> 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.*