`I am currently trying to write custom tactics to resolve different
``instances of some induction proofs. With some help from Christian Urban
``on [nominal-isabelle], I found out how to invoke nominal_induct_tac from
``the ML level, which has been a great help so far (thanks Christian!).
`
But while it is possible to do much simply by combining an induction
tactic with a number of other tactics, I increasingly find that it would
be useful (possibly even necessary) in many cases to be able to
structure the tactics so that
1. The base case and the inductive cases are separated, such that
different tactics can be used for each.
2. We have access to the induction term in each case.
Example. If we have the following datatype:
nominal_datatype trm = Name name | Pair trm trm
The Isar-proof might be structured like this:
proof(induct T rule: trm.strong_inducts)
case(Name a)
...
case(Pair N M)
...
qed
So we want to keep the cases separate in the tactic, or at least the
base case separate from the inductive steps.
And whenever we do a nested proof in the base case, for instance, we can
refer directly to 'a' as the induction term. This might not work well in
general in a tactic if we cannot assume knowledge about the datatype we
do the induction on, but in most cases at least, the base case would be
the same.