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



Am 23/01/2013 20:50, schrieb James Cooper:
> 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.

You can look at the thm xyz to see what it is. Instead of P ==> Q, what you
wanted, it is "P ==> (Q ==> R) ==> R", which is logically equivalent (but is
what the elim attribute expects.)

> It's... sort of an inversion rule? but how does it know t =
> NumType?

It follows from your rules in the same way that you proved it. There is no
creativity involved, just distinctness of constructurs.

> (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".)

That's because it ain't. It's an implication. You wrote too much. Compare with
the line I had sent you.

Tobias

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





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