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.