# Re: [isabelle] Explanation of induction rules for inductive predicates?

Dear James,

`as you have observed, the standard induction rule assumes that none of
``the parameters is specialised. If you want to keep specialised terms,
``you must tell Isabelle explicitly. Formally, you can prove something
``like this (not tested):
`
lemma
assumes "typecheck env (NumExpr n) T"
shows "T = NumType"
proof -
def e == "NumExpr n"
from assms have "typecheck env e T" by(simp add: e_def)
then have "e = NumExpr n --> T = NumType"
by induct simp_all
then show "T = NumType" by(simp add: e_def)
qed

`As such manual instantiations of terms occur frequently, the induct
``proof method can do the transformation for you:
`
lemma
assumes "typecheck env (NumExpr n) T"
shows "T = NumType"
using assms
apply(induct env e=="NumExpr n" T rule: typecheck.induct)
apply simp_all
done

`inductive also generates a case analysis rule typecheck.cases, which
``does not throw away instantiated parameters, but does not give any
``induction hypothesis. For proving inversion lemmas, this is probably the
``best way to go:
`
lemma "typecheck env (NumExpr n) T ==> T = NumType"
apply(cases rule: typecheck.cases)
apply simp_all
done
Hope this helps,
Andreas

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