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

Ah, thank you both very much. The "induct env e ≡ "NumExpr n" t rule:
typecheck.induct" approach seems to be just what I wanted (and I had been
using the two-level-proof-with-a-def-inside approach elsewhere, so it's
good to know there's a way to automate that).

The inductive_cases thing Tobias mentioned

inductive_cases xyz[elim!]: "typecheck env (NumExpr n) t"

also seems interesting, and shorter, but I'm not sure I understand what
it's doing exactly. If I stick the above line in my code, the lemma follows
"by auto", but I'm not really sure what the exact elimination rule being
added is. It's... sort of an inversion rule? but how does it know t =
NumType? (and, it seems it's not really the inversion rule I was thinking
of, since when I try to add the inverse of the Var typing rule,

inductive_cases checkVar[elim!]: "typecheck env (Var v) t ==> lookup env v
= Some t"

the system complains "Proposition not an inductive predicate".)

Again, thanks for your fast and insightful responses, and any further help
you have would be much appreciated.


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