Re: [isabelle] proof dags?
On Sat, 2 Jun 2012, John Wickerson wrote:
It seems to me that proving a lemma in Isabelle is much like building a
dag, where the facts are nodes and the implications between facts are
arrows. When several nodes "line up" in a simple chain we can use the
Isar construction "hence"; and for some other dag shapes the
"moreover/ultimately" pattern works. But in general, one needs to invent
names sometimes when the underlying proof dag doesn't conform to one of
I was wondering: has there been any work on a UI that lets the user
construct this dag *directly*? I'm imagining a sort of drag-and-drop
interface that lets me drag arrows between boxes and move boxes around a
canvas, and so on.
I have occasionally pondered the question how the implicit dependency
structure and the primary Isar text can be linked in a user interface.
This means some kind of augmented text editing as in Isabelle/jEdit with a
bit more than just a boring tree view on the side. jEdit also has notions
for drag-and-drop of text pieces and various operations on collections of
So one mainly needs to link existing concepts for plain text with the
structural information of the semantic document model. Advanced IDEs for
programming languages probably have something to offer here already, but I
don't know anything from first sight.
If anybody can point to examples from Eclipse, Netbeans, IntelliJ IDEA, or
even Visiual Studio, I would be interested to study them to learn how it
fits into the proof document model.
This archive was generated by a fusion of
Pipermail (Mailman edition) and