Hi Felix,
>From what I understand "by REWRITE_TAC[FUN_EQ_THM],2" and "by FUN_EQ_THM,2"
>do very different things: "by FUN_EQ_THM,2" runs the HOL_BY tactic, whereas
>"by REWRITE_TAC[FUN_EQ_THM],2" runs REWRITE_TAC, but not HOL_BY. Or does
>the second option run first REWRITE_TAC and then HOL_BY?
No, only "REWRITE_TAC[FUN_EQ_THM]" will be run.
In fact, I would write it myself "REWRITE_TAC,FUN_EQ_THM,2".
The "tactic" in the list after the "by" can have type "thm
list -> tactic" (in fact, that's the basic ocaml type that
I designed the thing for, a plain tactic is a derived thing.)
>I'd find it helpful to have some more verbose error reporting for inference
>errors. [...]
>If I wanted to implement something like this, where would I start?
Ouch! I wrote that code some years ago, and would have a
hard time myself doing something like this. Basically you'd
need to tinker with the whole chain of things:
- think of some syntax for what you want
- adapt the data structures for the proofs to know about
that syntax
- handle the extra possibilities in the data structures
when processing the proofs
So the syntax I was thinking about myself was something
like
... by #SOME_TACTIC#,...;
for when you don't want to "grow" the proof already by
running SOME_TACTIC, but only want to get the subgoals that
get produced by SOME_TACTIC as the current goals in your
HOL session. To get the goal for a given justification
for working on it then would be
... by ##,...;
I guess. But I don't know whether I would like something
like this if I tried it. Maybe I'd hate it :-)
Slightly related: the tactic "GOAL_TAC" sets the current goal
to the first subgoal produced at a certain point in a proof.
So already you can say things like
... by #SOME_TACTIC THEN GOAL_TAC,...;
or (as a separate proof step)
exec GOAL_TAC;
And then if you in the HOL session do
p();;
you'll see the goal there.
You can even have "GOAL_TAC"s in the middle of a complicated
traditional proof:
... THENL
[...;
... THEN GOAL_TAC;
...] THEN
...
Sometimes I find that convenient.
Freek
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
