Re: [Hol-info] Learning HOL Light

[Ramana K. <Ram...@cl...>]

On Thu, Jan 3, 2013 at 6:06 PM, Bill Richter
<ri...@ma...>wrote:

> Thanks, Petros!  It will take me a while to digest your post.  BTW I was
> wrong about the HOL Light reference manual treatment of STRIP_TAC, which is
> fine.
>
>    > BTW how does HOL and Informatics fit together?
>
>    How do they not? :) They are connected in so many ways...
>
> I think hol-info ought to have much more info about how HOL is used in the
> real world.  Why not more details!
>

I agree. Perhaps you can write some of your notes on the HOL4 wiki?
https://github.com/mn200/HOL/wiki


>
>    (Note how DISCH_TAC is *roughly* equivalent to DISCH_THEN ASSUME_TAC.)
>
> Michael posted that too, and I'm confused.  I think DISCH_TAC is exactly
> DISCH_THEN ASSUME_TAC.
>

In HOL4, you are right: they are exactly the same.
(The only difference I see is that DISCH_TAC will re-raise any exceptions
as having originated with DISCH_TAC rather than with DISCH_THEN).


>
>    A thm_tactic roughly corresponds to a forward reasoning step,
>    whereas a tactic roughly corresponds to a backwards step.
>
> I'm missing the boat about forward & backwards.  I don't know how to prove
> anything except as one does in miz3, and as John (and maybe I) showed, it
> only takes a few lines of code to write up the miz3 reasoning cleanly in
> HOL tactics.
>
>    A thm_tactic expects a theorem (often one of the assumptions) as an
>    argument, and does something with it (its conclusion to be more
>    precise).
>
> I would say that's true for ASSUME_TAC, MP_TAC and DISCH_TAC, but they're
> described differently in manual:
>
> FIRST_ASSUM : thm_tactic -> tactic
> DISCH_THEN : thm_tactic -> tactic
> SUBGOAL_THEN : term -> thm_tactic -> tactic
> ASSUME_TAC : thm_tactic
> MP_TAC : thm_tactic
> DISCH_TAC : tactic
>
> Seems to me that thm_tactic means something that can't begin a command,
> but can be the argument of something like
> FIRST_ASSUM, DISCH_THEN or SUBGOAL_THEN `t`, while a tactic can begin a
> command.  I'll go read your post more carefully!
>

To keep things really simple: thm_tactic is just an abbreviation for (thm
-> tactic). That is, a thm_tactic is any function that takes a theorem and
returns a tactic. They happen to be used in certain idiomatic ways like as
arguments to FIRST_ASSUM, or DISCH_THEN, but they can be used anywhere a
"theorem-parameterised tactic" is required.

E.g. with FIRST_ASSUM ttac, you can think of ttac as being a
theorem-parameterised tactic; then FIRST_ASSUM says to provide the first
assumption in the current goal as the theorem that makes ttac into a tactic.

--
> Best,
> Bill
>
>
> ------------------------------------------------------------------------------
> Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
> MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
> with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
> MVPs and experts. ON SALE this month only -- learn more at:
> http://p.sf.net/sfu/learnmore_122712
> _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>