See this for a better guide by Magnus: http://www.cl.cam.ac.uk/~mom22/HOL-interaction.pdf
On Sun, Nov 15, 2015 at 5:55 PM, Yong Kiam <[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]> > wrote: > >> Use Tactical.THEN (or lcsymtacs.>>, which is the same). >> >> On 15 November 2015 at 09:03, shengyu shen <[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] >>> 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
