Re: [isabelle] On Recursion Induction



On 08.05.2012 21:40, Alfio Martini wrote:
I looked at section 9.2.3 in the reference manual and did not find
"induct_tac" in the list of improper proof methods. But assuming it
is, I think that the tutorial, for instance, Chapter 2, should be updated,
shouldn´t it?

This tutorial is a bit dated (but still very useful). I think Tobias Nipkow is working on a newer version.

But at the "playing level" I prefer to proceed like in a hand-made proof,
first stripping off all the quantifiers and then applying induction. In this
kind of exercise I can use this theorem further by applying rule allE and
so on. So, I assume that this kind of approach can be only done
with Isar and the fix command, as pointed out by Brian, which I usually
do.

If you really want to do step-by-step application of natural deduction rules, you might want to use the old-style rule_tac and erule_tac methods, because they allow you to instantiate meta-quantified variable (syntax is "rule_tac x=... in exI").

  -- Lars





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