Tactic merger

[m-fleury]

This is discussion on what new feature could do.

It would be cool to have a "tactic merger" that transforms two applies in a single by:

apply rule
apply (auto simp: XXX)

into

by rule (auto simp: XXX)

Some possible variants:

• The auto/simp merger:

apply (auto simp: XXX)
apply (auto simp: YYY)

into

apply (auto simp: XXX YYY)

or by?

• The force merger:

apply (auto simp: XXX)
apply (force simp: YYY)

into

by (force simp: XXX YYY)

In the examples above, the second call might have been generated by Sledgehammer and this would clean up the file. It will not always work, but can be useful still.

Questions:

• can this be useful?
• what kind of interesting other interesting cases are needed?

[halbGefressen]

The auto/simp merger and the force merger do not work all the time. I encountered multiple cases in which auto simp: XXX, auto simp: YYY worked, but auto simp: XXX YYY didn't terminate because simplifying with rule YYY on the first goal led to non-termination, but on the simplified goal didn't. Also since auto may create multiple subgoals, the auto/force merger may sometimes produce unexpected behaviour.

We could instead create a tactic combinator, merging apply (a) apply (b) into apply (a,b). This would make proofs shorter, too.