Sorry, I got the semantics of FIRST_ASSUM wrong: it's more subtle (but
irrelevant to the point I was making); it says to provide the first
assumption that makes the resulting tactic succeed (i.e. it will backtrack
and try each assumption in turn until the constructed tactic doesn't fail).
On Thu, Jan 3, 2013 at 7:07 PM, Ramana Kumar <[email protected]>wrote:
> 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
