Email Gateway (Aug 18 2022 at 20:18): Email Gateway (Aug 18 2022 at 20:18):From: Patrick Michel <uni@pbmichel.de>
Hi!
While updating my theories to Isabelle/HOL 2012 (worked like a charm) I was also trying out PIDE.
I am quite happy with the IDE so far, once I figured out how to search for theorems, etc.
At the moment, however, the curried notation of the meta implication drives me crazy :-)
My current subgoal structurally looks like this:
(A ⟹ B ⟹ C) ⟹ (D ⟹ F) ⟹ G ⟹ H ⟹ I ⟹ J
and I'd rather have it like this again:
[[A; B] ⟹ C; D ⟹ F; G; H; I] ⟹ J
Is there a display option for this?
Thanks,
Patrick Michel
Software Technology Group
University of Kaiserslautern
Email Gateway (Aug 18 2022 at 20:18):From: Makarius <makarius@sketis.net>
On Fri, 29 Jun 2012, Patrick Michel wrote:
While updating my theories to Isabelle/HOL 2012 (worked like a charm) I
was also trying out PIDE. I am quite happy with the IDE so far, once I
figured out how to search for theorems, etc.
See the isar-ref manual for all commands. The 'help' command also gives
you a complete list. These things were well-known before Proof General
introduced some menus for some commands > 10 years ago.
What you want here is 'find_theorems'. Apart from the full syntax the
manual also gives you 'find_consts', which Proof General does not know
because that command is younger than 5 years.
At the moment, however, the curried notation of the meta implication drives me crazy :-)
My current subgoal structurally looks like this:(A ⟹ B ⟹ C) ⟹ (D ⟹ F) ⟹ G ⟹ H ⟹ I ⟹ J
and I'd rather have it like this again:
[[A; B] ⟹ C; D ⟹ F; G; H; I] ⟹ J
Is there a display option for this?
This is called "print mode" in Isabelle terminology. E.g.
isabelle jedit -m brackets
will recover the above special Isabelle syntax for nested implications.
Historically, Larry Paulson introduced the brackets notation both for ==>
and => and used it mainly in Isabelle/ZF. Later Isabelle/HOL became more
popular, and the custom to use brackets for ==> but not for =>.
When I was exposed to this for the first time in 1993, I made sure that
brackets do work uniformly as expected, because the pretty printer was not
working in all situations at that time. Around 1998 I then learned how to
make Isabelle/Pure rules nest properly (which was not possible before),
and found the brackets very difficult to read. E.g. in your example
above, the first two goal premises are nested ==> which you see
immediately from the parentheses in the first output, but not in the
second.
Anyway, print modes like "brackets", "no_brackets", "type_brackets",
"no_type_brackets" are there to make output more interesting by
individualizing it. There is also a mode "iff" for boolean equality as
double arrow, which is off by default.
Makarius
Email Gateway (Aug 18 2022 at 20:18):From: Tobias Nipkow <nipkow@in.tum.de>
A similar decline in culture set in when assembly language arrived and you no
longer had to remember opcodes.
Tobias
Email Gateway (Aug 18 2022 at 20:19):From: Makarius <makarius@sketis.net>
Where is the problem remembering the 'help' command, and looking things up
in the fine manual?
In the meantime some volunteers can clean up the find_theorems
implementation, and make a Scala/Swing wrapper form for its command line.
Some other volunteers can step forward and maintain Isabelle Proof General
4.x, until that has become fully obsolete, which is not the case right
now. At the moment it is unmaintained, so it will decay within 1-2 years.
Makarius
Email Gateway (Aug 18 2022 at 20:19):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 20:19):From: Makarius <makarius@sketis.net>
Even more obvious: use the command completion. You type "find" and wait
300ms and get a selection of find commands. Same for "print" or whatever
you please, e.g. "sl" for "sledgehammer".
You can also modify the reactivity of the completion popup in the Plugin
Options for SideKick in jEdit. (In Isabelle2012 it is a bit more
ambitious than in Isabelle2011-1, but still not as aggressive as it can
be for full virtuosity of jEdit experts.)
Makarius
Email Gateway (Aug 18 2022 at 20:19):From: Patrick Michel <uni@pbmichel.de>
Well thanks for all the advice, but as I said; I had already figured that out.
I wouldn't have used PIDE for more than 5 minutes otherwise (which happened in the past).
Last updated: Apr 30 2024 at 16:19 UTC