Email Gateway (Aug 18 2022 at 14:17): Email Gateway (Aug 18 2022 at 14:17):From: René Thiemann <rene.thiemann@uibk.ac.at>
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"
Counterexample (possibly spurious):
a = 0, a * b = 0, b = 1
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é
Email Gateway (Aug 18 2022 at 14:17):From: Makarius <makarius@sketis.net>
Batch mode is a bit more thorough by default, in particular
quick_and_dirty is disabled. Apparently the crash is caused by the full
version of the Cooper procedure, not the oracle version.
It seems that Sasche Böhme has already fixed the problem recently: see
http://isabelle.in.tum.de/repos/isabelle/raw-rev/40a0760a00ea
You can direct paste this text into stdin of "patch -p 1", to modify
Isabelle2009 accordingly.
Alternatively you can make yourself an alpha/beta tester of the next
release, and use one of the many development snapshots. (We are
approaching the next official release already.)
Makarius
Email Gateway (Aug 18 2022 at 14:18):From: Sascha Boehme <boehmes@in.tum.de>
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:
Last updated: Nov 21 2024 at 12:39 UTC