Re: [isabelle] how to set "brackets" mode



On 20/12/16 12:52, Lawrence Paulson wrote:
> People often ask how to enable the [| ... |] ==> output, which many find more readable than the default. Itâs certainly my preference.

Can you explain this? Or is it just due to habits and nostalgy?


The uniform notation of nested ==> goes back to 1998, when Isar concepts
were emerging, with some consequences on Pure. E.g. it became possible
to work with nested rules routinely. Before, rules were mostly flat and
the bracketed notation was adequate. Afterwards, I found nested rules
with brackets very cumbersome to read and to write, and eventually
stopped doing that. Since Isabelle/jEdit is shipped with defaults for
Isar, this print mode also changed approx. 5 years ago.

Note that plain currying (for => and ==>) without any special notational
tricks has the advantage that the depth of nesting is immediately
visible by the parentheses around complex items. This visual clue is
absent in bracket notation (which is better for long lists of flat items).

Moreover, typing [| |] is almost impossible on a non-English keyboard. I
usually prefer input and output to coincide as much as feasible. I
cannot imagine anybody with a German keyword to prefer these special
brackets.


Another reason from 1998: many people not familiar with Isabelle asking
in presentations "What are these semantic brackets? What are these
semicolons?" Any also: What are these question-mark variables?".

Typical introductions to Isabelle talk about programming language
semantics (even until today, e.g. the "Concrete Semantics" book), so it
looks very odd to me to construct an artificial conflict with standard
notation of semantic brackets and sequential composition. Such
applications then require double semicolons (Or maybe bold ones?). We
have managed to get rid of semicolons in outer syntax some years ago
(making them free for sequential composition of proof methods), so maybe
we can one day do the same for inner syntax.

I have actually started using "if" and "for" notation for the clauses in
inductive definitions, especially in introductions to Isabelle. The
postfix notation is like in Prolog (what most people already know) and
the keywords "if" and "for" look self-explanatory. That Isar rule
notation with semantic brackets and semicolons in their conventional
meaning could make a difference for didactic purposes.


Back to occasional complaints about iterated ==> in output. My
impression is that most people talk about goal state output, not rule
output. Today, there is no particular reason why the outer subgoal
structure should be printed with !! / ==> at all. It could be done in
some Isar notation, either fix/assume/show or show/if/for. Moreover it
could be done in a way that makes it easy to copy-paste (or "sendback")
the result into the emerging Isar proof text.

Also note that the ASCII notation of ==> used to have special
line-breaks for pretty printing, maybe to require less space when it is
iterated. Just as historic accident, the symbolic notation â was lacking
that: it was introduced as plain infixr in
http://isabelle.in.tum.de/repos/isabelle/rev/9dd06eeda95c -- maybe by
accident.

When the default officially changed from ASCII to symbols recently, I
also changed the special formatting of ==> to plain infixr (see
http://isabelle.in.tum.de/repos/isabelle/rev/301833d9013a#l3.77). I
simply did not dare to ask what is the *right* way to print the long
arrow notation, after everybody got used to the presumably wrong way in
so many years of Isabelle symbols usage (both in the user interface and
in LaTeX output).

Maybe we should just recover that line-breaking for both the ASCII and
symbolic double-arrow? It could make a difference for screen display,
but also cause surprises in LaTeX documents that are tweaked for a
particular layout.


	Makarius





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