Re: [isabelle] proving a class instantiation.



On Wed, 10 Nov 2010, Brian Huffman wrote:

On Wed, Nov 10, 2010 at 8:19 AM, Makarius <makarius at sketis.net> wrote:
On Wed, 10 Nov 2010, Lars Noschinski wrote:

My confusion stemmed from the fact that I like(d) to think of "!!x. A x
==> B x" as a convenient short-cut for the more verbose {fix x assume "A x"
show "B x"}.

It is in fact a short form of this:

 { fix x presume "A x" show "B x" ... }

So of the two possible interpretations of show "!!x. A x ==> B x", you specifically chose the version with 'presume' rather than 'assume'. Why did you think this was the right choice? Comments on the mailing list have clearly shown that users uniformly expect the 'assume' interpretation, and are thoroughly confused by the current behavior.

The behaviour of show "!!x. A x ==> B x" is a natural consequence of how rule application works in Isar, and I did not force it into another direction when it emerged many years ago. This is the same principle that made most of the language work out very well in the end. So you are asking to close a door where you have entered yourself before.

Moreover, the "expected" treatment of such inlined rules would dilute important concepts of the Isar language design, and make it harder to learn it properly later on. One such principle is that native structural language elements are preferred over logical formulae. If you take the existing fixes/assumes/shows/obtains for example, it gives the user an opportinity to add names, attributes, is patterns etc. that can be later used in the proof. It also avoids an argument, if !!/==> are just copies of !/--> in HOL, or a separete notation for rules, or whatever.

Abbreviating { fix assume "A x" show "B x" ... } as
show "!!x. A x ==> B x" looses the advantages of Isar structure.
Instead, one could support something simular to fixes/assumes/shows inside a proof, but as always it requires substantial time to study the consequences of adding new trees to the garden, and maybe removing some old ones.

This delicate process of tending the arboretum is further complicated by different traditions being present at the same time. The whole Isar framework grew out of certain ideas of tactical reasoning, natural deduction rule composition, semi-automated reasoning, and fit together so smoothly that many people still think that "apply" scripts are native to Isar (although they are only guests).


A marginal question concerning consistency and least surprise: Why do many people still indent toplevel Isar proofs differently from local ones? E.g. like this:

lemma foo
by simp

instead of the proper form according to the true logical structure of Isar:

lemma foo
  by simp

Here the "surprise" has again historical roots, because the first version is how unstructured proof scripts would look like, before they where manually converted to the new language many years ago.


	Makarius


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