Re: [isabelle] On Recursion Induction



Am 09.05.2012 um 09:54 schrieb Lars Noschinski:

> 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").

... both of which are definitely in the list of "harmful" proof methods of section 9.2.3.

It would seem to me that the use of tactic emulation proof methods (i.e. methods whose name end with "_tac") in one place and the warnings against their use in another place reflects more the inclinations of the respective authors of these documents than the date at which these were written.

Jasmin






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