On 27/09/17 05:29, Chun Tian (binghe) wrote: > Honestly speaking, I like those abbreviated “power” tactics, such that "fs" > for FULL_SIMP_TAC, "rfs" for REV_FULL_SIMP_TAC, etc., but using all tactics > in smaller cases (e.g. strip_tac/STRIP_TAC) doesn't make much sense to me, > because it makes me harder to distinguish between the "inner" and "outer" > languages in HOL proof scripts...
Yes. I use an explicit chain of “GEN_TAC”, “DISCH_TAC”, “EQ_TAC” and/or “CONJ_TAC” when the first step (which is most of the time) is to strip the original goal. After that, I declare what the resulting goal is with a trivial tactic I wrote: “must_prove:(term quotation -> tactic -> tactic)”. “must_prove” checks that the goal is alpha-equivalent to the quotation and then applies the user-provided tactic (it must completely solve the goal). Of course, taking a tactic as an argument is just for syntactic convenience, as the same could be done with “THEN1”/“>-”. I was going to put here the code of “must_prove”, but I just realized how ugly my implementation is. Instead I am going to rewrite it. P.S.: I wrote this message yesterday (UTC—05) but source forge rejected my message. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
