Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Improper proof command 'guess' provi...

Email Gateway (Sep 27 2021 at 15:17):

From: Makarius <makarius@sketis.net>
* Isar *

• The improper proof command 'guess' is no longer part of by Pure, but
  provided by the separate theory "Pure-ex.Guess". INCOMPATIBILITY,
  existing applications need to import session "Pure-ex" and theory
  "Pure-ex.Guess". Afterwards it is usually better eliminate the 'guess'
  command, using explicit 'obtain' instead.

This refers to Isabelle/b49bd5d9041f and AFP/2056abab0dd6. The AFP changeset
is representative for the kind of (non-)applications of 'guess'. It originally
stems from a discussion about improper Isar add-ons in 2006. In the 10 years
later so many better ways to mix structured and unstructured proofs emerged,
e.g. the 'subgoal' command. So today, there would be no point to introduce
such a command at all.

In the above AFP change, I have either turned the non-Isar "wild guesses" into
proper 'obtain', or rephrased the proofs slightly to avoid the awkward
situation in the first place. In a few cases, left things unchanged and did
import "Pure-ex.Guess" as explained above.

This is in contrast to the Isabelle distribution where all guesses within Isar
proofs are already gone --- mostly derived from Robert Himmelmann's initial
work on HOL-Analysis n years ago.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Sep 27 2021 at 15:23):

From: Lawrence Paulson <lp15@cam.ac.uk>
And good riddance to it!

Larry

Last updated: Jul 15 2022 at 23:21 UTC