One possible variation on your must_prove might be the following:
qmatch_rename_tac {term quotation} >- {tactic}
On 28 September 2017 at 18:28, Mario Castelán Castro <marioxcc...@yandex.com
> wrote:
> 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
>
>
> ------------------------------------------------------------
> ------------------
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
