Re: [isabelle] On Recursion Induction
On Tue, May 8, 2012 at 7:13 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
> Dear Alfio,
> On 05/08/2012 01:03 PM, Alfio Martini wrote:
>> 1) In the proof of the theorem, below in the file (and in the image), I
>> recursion induction together
>> with "induct_tac" (as taught in the tutorial) and everything works as
>> expected. However, If I try to use
>> apply (induction b rule: NNF.induct) as suggested by the new tutorial from
>> Nipkow (e.g., section 2.3, page 15) , I get the following error message:
>> ill-typed instantiation: b :; 'a.
>> Why this is so?
> "induct"/"induction" is not the same as "induct_tac" (all methods with a
> "_tac" suffix are emulations for traditional tactics (as used in apply-style
> proofs) and are considered "improper" by isar-ref p. 173. One difference is
> that with traditional tactics case-analysis (case_tac) and induction
> (induct_tac) is possible over meta-bound variables, for "induct"/"induction"
> however, you need free variables (I guess in reality the difference is more
> subtle, so please Isabelle-gurus, correct me). Moreover your statement
> theorem "∀b. ∀e. valbool b e = valbool (NNF b) e"
> is a bit strange since by-default all variables are (meta-)all-quantified
> after a successful proof. With proper methods you can proof the statement as
> theorem "valbool b e = valbool (NNF b) e"
> by (induction b rule: NNF.induct) auto
I was about to suggest the same thing.
Another standard idiom is to use "fix" to introduce a new free
variable, which can then be used with "induct":
theorem "\<forall>b. \<forall>e. valbool b e = valbool (NNF b) e"
proof (rule allI)
show "\<forall>e. valbool b e = valbool (NNF b) e"
by (induction b rule:NNF.induct) auto
(Note that simply "proof", which applies a default intro rule, would
also work in place of "proof (rule allI)".)
This archive was generated by a fusion of
Pipermail (Mailman edition) and