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.