Re: [isabelle] PIDE Display of Assumptions



On Fri, 29 Jun 2012, Christian Urban wrote:

Is there a way to make that printmode the default
in ones etc/settings, for example?

Following usual Isabelle conventions, src/Tools/jEdit/etc/settings defines various settings that are relavant for that tool. ISABELLE_JEDIT_OPTIONS allows to give default command line options. So you can set that accordingly somewhere in your local $ISABELLE_HOME_USER/etc/settings for example.


I have to admit I am very fond of this special syntax too and have no problem with interpreting them in my head as

[A,B]     [D]
  C        F    G   H   I
 ------------------------
             J

which is the style that usually appears in textbooks on
natural deduction. For example, the Gentzen book would
write the impI- and  orE-rules as

      [A]
       B
    -------
    A --> B


          [A] [B]
 A v B     C   C
 ---------------
       C

which is not very different from Larry's bracket notation.

That is the reason why Larry introduced that in the late 1980-ies, and why I've spent some time in 1993 to make it print realiably.

The nesting of rules does not fit very well in that notation, though, and it is absent in Gentzen's book. This is why I've introduced the plain no_brackets print mode around 1998, which now happens to be the default in Isabelle/jEdit after so many years.


There is also a broader perspective here: printing of rules can be done in a high-level fashion via 'print_statement', but likewise printing of goal states is still not available. The latter would also overcome misunderstanding how to prove "!!x. A ==> B ==> C", i.e. by saying
"fix x assume A B show C", not show "!!x. A ==> B ==> C".


	Makarius





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