Hi Petros/Joe,
I must admit that I'm not particularly familiar with any of these Emacs/etc
modes for HOL Light and HOL4, although I have seen Proof General, and
ProofTree that interacts with it. How do these other facilities compare?
> Tactician is more general and gives you a full breakdown of the
> packaged proof in interactive steps (and vice-versa), at the cost
> of having to reconstruct core HOL Light data structures. Of course
> Mark would be much better at explaining more details.
That's right, a goal tree is maintained as a tactic proof executes, with
each node storing a goal and a description of the tactic used on it. Goals
are adjusted to carry a pointer to their tree node, and tactics are adjusted
to work with these goals and update the tree. Theorems are also adjusted,
to enable them to be described if they occur as tactic arguments. This all
enables a flattened ("g" and "e" style) or packaged "prove" style) version
of a tactic proof script to be outputted upon user request. A goal tree
graph, with tactics as the nodes, can also be outputted as a .dot file. A
planned enhancement is to output graphs that also show the goal sequent as
you hover the mouse over a node.
So I suppose one could envisage an Emacs mode where the user selected a
packaged proof script to result in a window showing the flattened proof
script and/or the goal tree graph, which would be suitable for stepping
through interactively. The user could edit the proof in this window and
then the packaged proof would get updated accordingly. I think generally
users would be more comfortable editing flattened proof scripts rather than
packaged up ones.
> One advantage that I can think of is when you wish to go through the
> proof of one particular subgoal. This may be confusing if you are
> executing packaged proof steps (e.g. if other subgoals are proven
> simultaneously).
Yes, if the user just sees/edits the packaged proof script, there is the
challenge of how to design a GUI for stepping through this. I suppose the
goal tree graph could highlight the set of nodes that correspond to a given
highlighted tactic in the script, and the graph could be automatically
recalculated as the user edits the script.
Mark.
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
