On Thu, Jan 3, 2013 at 6:06 PM, Bill Richter
<[email protected]>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
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
