Hi,
there is also the GoalTree library. In contrast to the GoalStack one,
expanding a tactic gets the tactic twice. Once as a string and once as a
ML function. This allows the GoalTree to keep track of the proof
stucture and print the tactics used for the proof using THEN, THENL,
etc. at the end. There is a bit of support of sending the string
automaticallz in the HolMode of emacs (I don't know about the vim
bindings).
I prefer the wrinting my proofs manually. I believe it gives you more
flexibility and there is better support for the GoalStack in the Emacs
Hol Mode. However, I believe it was worth mentioning.
Best
Thomas
On 15.11.2015 11:00, Yong Kiam wrote:
See this for a better guide by Magnus:
http://www.cl.cam.ac.uk/~mom22/HOL-interaction.pdf
<http://www.cl.cam.ac.uk/%7Emom22/HOL-interaction.pdf>
On Sun, Nov 15, 2015 at 5:55 PM, Yong Kiam <[email protected]
<mailto:[email protected]>> wrote:
This may not be directly relevant to your question but you could
consider developing your proofs interactively in an editor (Vim or
Emacs) and saving the scripts instead of using the HOL4 REPL
directly (see the various proof scripts in src/ and examples/).
I use the Vim bindings:
https://github.com/HOL-Theorem-Prover/HOL/tree/master/tools/vim
and others may be able to tell you more about the emacs ones.
Usual development (for me in Vim):
1) State the goal in your proof script like:
val foo = prove (``g``,
2) Highlight ``g`` and send it to the theorem prover as a goal
(h-t , h-g)
3) Start writing and trying tactics (h-e sends the tactic to the
prover, see the README for other things you could do)
val foo = prove(``g``,
fs[] >> rw[] >> blabla...
(>> is THEN, >- is THEN1)
4) On a successful proof, just save whatever you wrote in the
editor into a proof file:
val foo = prove(``g``, fs[]>>rw[]>>blabla);
This is off the top of my head, there might be a better guide for
this somewhere.
On Sun, Nov 15, 2015 at 5:39 PM, Ramana Kumar
<[email protected] <mailto:[email protected]>> wrote:
Use Tactical.THEN (or lcsymtacs.>>, which is the same).
On 15 November 2015 at 09:03, shengyu shen
<[email protected] <mailto:[email protected]>> wrote:
Dear all :
Supposing I have goal G and I prove it with lots of
tactics like folowing :
g `G`;
e (t1);
e (t2);
e (t3);
So after I finished proof, I need to use store_thm to
manually collecting all t1,t2,t3... to save the proven
theorem.
Is there any way to automatically collect all these tactics?
Shen
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
<mailto:[email protected]>
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
<mailto:[email protected]>
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
