Re: [isabelle] On Recursion Induction

On Tue, May 8, 2012 at 7:13 AM, Christian Sternagel
<c-sterna at> 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
>> use
>> 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
>> Tobias
>> 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
> follows:
>  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)
  fix b
  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)".)

- Brian

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