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