Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
On Mon, 8 Feb 2010, Florian Haftmann wrote:
The "prems" are, roughly, the accumulated facts within a proof, which as
a historical accident have been used implicitly by certain proof methods
-- which, following the rule of thumb "explicit is better than
implicit", turned out as a bad idea. You can recover this behaviour by
using prems explicitly, e.g. "using prems by ..." or "by (auto simp add:
prems)" etc. Best practice is to refer to used facts implicitly; recall
that you can quote facts by proposition using backticks ``.
Many years ago (around 1999) the "prems" were indeed somehow correlated to
local facts within a proof, in emulation of the old-style goal
representation that lacks genuine facts (cf. the "insert" method).
Later (still in 1999, or maybe in 2000) the distinction between a proof
context and a goal state became much clearer, and also more scalable --
both for users who need to read state information and tools that need to
operate on them. Ever since, local facts required for a proof step should
have been indicated explicitly, but only in recent years I've made some
effort to remove these early mistakes from the system.
Further note that the later introduction of locales (and arbitrary target
contexts), as well as derived assumption elements such as 'obtain'
rendered the "prems" register of the Isar machinery just an arbitrary
collection of theorems that happen to have a certain foundational role.
In user space it is meaningless and should not be used anymore -- the
Proof General hilighting scheme also indicates this.
This archive was generated by a fusion of
Pipermail (Mailman edition) and