# Re: [isabelle] On Recursion Induction

```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

which is short for

theorem "valbool b e = valbool (NNF b) e"
apply (induction b rule: NNF.induct)
apply (auto)
done

```
The resulting thm is "valbool ?b ?e = valbool (NNF ?b) ?e" (note the question marks which mark schematic variables, i.e., variables that can be instantiated arbitrarily according to their type). Your original version results in "ALL b e. valbool b e = valbool (NNF b) e" (which is equivalent, but not so nice to use, since you cannot directly instantiate it).
```
hope this helps

chris

```

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