mn200/HOL — pull request #110 by aravantv (2013-02-18 19:04:13+00:00)
Title: HINT_EXISTS_TAC

I added the tactic at the end of the src/1/Tactic.sml.

A few remarks:

- Michael mentionned something about writing a selftest but I did not see any part of 1/selftest.ml dedicated to the test of tactics
=> what would be the ideal place for this?

- I wrote a short Doc file: help/Docfiles/Tactic.HINT_EXISTS_TAC.doc

- To make it compile I had to do a slight change to the tactic's behaviour. For clarity, I recall this behaviour briefly.
Given a goal of the form:

?x. P x /\ Q x /\ R x
=============
1. ...
2. ...
3. Q t
4. ....

Applying HINT_EXISTS_TAC yields:

P t /\ Q t /\ R t
=============
1. ...
2. ...
3. Q t
4. ....

Now the change is as follows: In my original code, I was calling ASM_REWRITE_TAC in order to simplify the goal further as follows:

P t /\ R t
=============
1. ...
2. ...
3. Q t
4. ....

However, this introduces a dependency on Rewrite.sml (which itself depends on Tactic.sml), so I removed it.

Comments:
* this is actually probably a good thing since the ASM_REWRITE_TAC could have induced rewrites that were not wanted by the user
* in addition I don't think that HINT_EXISTS_TAC had anything to do in Rewrite.sml
* this is easily circumvented at the user level by defining a tactic which calls both tactics sequentially

-- Vincent Aravantinos