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(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.

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.


	Makarius





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