Re: [isabelle] Confusing behavior of a paired set comprehension



On Wed, 4 Apr 2012, Jonas Wagner wrote:

No, a feature. Patterns may not contain repeated variables.

+1 vote for "bug".

The fact that Patterns may not contain repeated variables is perfectly fine. The fact that the first occurrence of a repeated variable is silently replaced by another variables is not fine.

But that's just the option of an Isabelle Newbie who got his proof wrong due to a surprising feature ;)

This thread got split over two isabelle mailing lists for unknown reasons, so I repeat my answer from isabelle-dev here once more:

  Things like %x x x x. x and fix x fix x fix x have "x = x" are perfectly
  legal and behave quite uniformly for many years, i.e. with little
  surprise to people who have got acquainted with Isabelle scoping rules.

  To make things even more simple for beginners, the Prover IDE markup
  protocol already indicates the internal scopes in the source text.  E.g.
  when using CONTROL/COMMAND with mouse clicks, one can explore the
  internal bindings.  It is only a small addition to the display engine to
  make variable scopes immediately visible in the source text, like
  Netbeans would do for Java for example when the user moves or hovers
  over the text.

  In contrast, lots of warning messages are old-school TTY technology, and
  in Proof General the channel for that gets easily overloaded so that the
  user is switching into SPAM mode.


Jonas, since you are from EPFL you are probably familier with the Scala scoping, which is often more harsh in forbidding plain nesting of scopes that would be just fine in the ML, HOL, Haskell tradition. I find the Scala behaviour quite confusing at times.

Anyway the IDE solution sketched above will make things easier for beginners without having to reconsider traditions that are established for decades in certain communities.


	Makarius






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