THEN applies the tactic to all subgoals, THEN1 applies it to the first one (and expects it to be solved) -- Refer to the HOL reference for a full explanation
So your final proof might look like fs[]>>rw[] (*Suppose we generated 5 subgoals*) >- (*first subgoal tactic*) ( a >> b >> c) >- (* second subgoal tactic*) ( a >> b >> e) >> (*apply same tactic to everything else*) ( a >> d) Like you said, this gives you a tree-like proof structure. If you want to do something like a "diamond" you could use TRY (making it fail on subgoals you don't want the tactic to be applied on) like: a >> TRY(b) >> c There's also THENL if you don't want to use lots of THEN1s. On Sun, Nov 15, 2015 at 7:38 PM, shengyu shen <[email protected]> wrote: > First thank you for our suggestion. > > But for your sugestion on using THEN ... THEN, sometimes there are > multiple sub goals, which leads to tree like proof structure instead of > linear one. > > So some THEN may not need. > > Shen > > 2015年11月15日 上午01:55，Yong Kiam <[email protected]> 写道： > > 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
