Re: [isabelle] Structured induction with custom tactics
On Tue, 9 Feb 2010, Palle Raabjerg wrote:
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(Pair N M)
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
Fine-grained control over the "structure" of proof states is usually very
delicate, but it can be done. The proof methods "induct" and
"nominal_induct" are the most sophisticated examples for that.
As a starting point, I recommend looking at the relatively new FOCUS
combinators in Isabelle2009-1/src/Pure/subgoal.ML -- the plain
Subgoal.focus versions together with Isar.goal() in interactive mode
should give you some idea how to get hold of the basic fix/assume/show
layout of a goal state.
This archive was generated by a fusion of
Pipermail (Mailman edition) and