[isabelle] Structured induction with custom tactics



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.
Any pointers on how this might be achieved, if it is possible?

Best Regards,
Palle Raabjerg





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.