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.