Dear Michael,
On 05/01/2018 18:18, Michael Beeson wrote:
But, we have to rewrite ONLY that term, and not the other tarea terms.
We can do that kind of thing with PAT_CONV, but it only works on
conversions, and SIMP isn't a conversion, hence the convoluted code
above that makes REWRITE into a conversion, then uses PAT_CONV, and
that makes that back into a tactic. Sheesh, does it really have to
be like this?
That actually doesn't sound too complicated (at least for HOL Light
standards)!
You can always create your own tactic from this code if you are using it
often.
In particular, in a FORWARDS proof is there any way to direct SIMP or
REWRITE to work only on certain subterms?
As far as I know (though I could be wrong), subterm selection is
non-trivial and most theorem provers would have you use substitution
instead.
This might be easier in your particular case as well.
but why
didn't the following work?
[...]
# e (ACCEPT_TAC (SPEC_ALL tadditive1));;
Exception: Failure "ACCEPT_TAC".
The most likely cause is a type mismatch. I'm guessing a, b, c, and d
have variable types that don't match, whereas ACCEPT_TAC requires
perfect matching.
"MATCH_ACCEPT_TAC tadditive1" should work.
Hope this helps!
Regards,
Petros
--
Dr Petros Papapanagiotou
CISA, School of Informatics
The University of Edinburgh
Website: http://homepages.inf.ed.ac.uk/ppapapan/
Email: p...@ed.ac.uk
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
