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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.