Re: [isabelle] On Recursion Induction
On Wed, 9 May 2012, Jasmin Blanchette wrote:
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,
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
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
It is probably both the inclination and the date.
Many years ago, Larry Paulson invented a very nice natural deduction rule
framework called Isabelle/Pure with one main composition principle called
"RS" (now visible in Isar as "rule" method or "OF" attribute). For
various technical reasons he also added erule/drule/frule variants, and
some means for explicit instantiations under a local quantifier
10 years later I came up with a natural deduction proof framework called
Isabelle/Isar. It worked out just with the original Pure principles, the
add-on zoo was not required. The isar-ref manual explains this Pure style
of structured natural deduction in chapter 1 and 2.
Later I also re-integrated all the old stuff into the Isabelle/Isar
infrastructure, so that existing material could be converted to Isar
syntax in a superficial sense, without rewriting things deeply. Someone
(not me) invented the name "apply style" for this guest mode of
Isabelle/Isar. This is the class of "improper language elements" within
proper Isar turned out quite succesful, so that its guest status is
Concerning rule_tac in particular: it is already mostly obsolete in ML
because the FOCUS combinators address the the demand for working under
local quantifiers more directly. It is a re-use of Isar proof contexts
for ML tactic programming.
This archive was generated by a fusion of
Pipermail (Mailman edition) and