Improve speed of `xcf`, `xfun_spec` etc.

[xrchz]

These tactics use the stateful simplifier and can become rather inefficient. This issue is to minimise the use of the simplifier in cfTacticsLib.sml, using lower-level/more specific proof tools instead. For example, something like

rpt(CHANGED_TAC (disch_then (mp_tac o CONV_RULE reduce_conv o PURE_ONCE_REWRITE_RULE[cf_def])))

might do better than

disch_then(mp_tac o CONV_RULE reduce_conv o simp_rule [cf_def])

Although this can probably be improved further.

If everything in examples builds and there is any noticeable speed increase, this issue can be closed. (Or if there's an argument put forward for why better speed of xcf is impossible.)

[xrchz]

@Armael thoughts?

[Armael]

Indeed, I would not be surprised that the various xtactics use the simplifier too much, and could be implemented more efficiently. We have a relatively big base of examples at hand, so as you illustrate, I think it is safe to try to rewrite the bits that look costly to something more efficient that looks equivalent: if all proofs still pass then it should be good.

[xrchz]

Won't fix: Superseded by #813