Re: [Hol-info] Learning HOL Light

[Bill R. <ri...@ma...>]

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! 

   (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.  

   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!

-- 
Best,
Bill