*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Explanation of induction rules for inductive predicates?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 23 Jan 2013 22:01:20 +0100*In-reply-to*: <CACcJPQqEMmXSUueM=c4Os+3kLaLkJVx0QNv5qo+R1SuyuRvaJw@mail.gmail.com>*References*: <CACcJPQpuQy8BSJnVLy1oac_cx4Z878M=VBjizQUFoW9Si2v23g@mail.gmail.com> <50FFD240.4090604@inf.ethz.ch> <CACcJPQqEMmXSUueM=c4Os+3kLaLkJVx0QNv5qo+R1SuyuRvaJw@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130107 Thunderbird/17.0.2

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 >

**References**:**[isabelle] Explanation of induction rules for inductive predicates?***From:*James Cooper

**Re: [isabelle] Explanation of induction rules for inductive predicates?***From:*Andreas Lochbihler

**Re: [isabelle] Explanation of induction rules for inductive predicates?***From:*James Cooper

- Previous by Date: Re: [isabelle] Explanation of induction rules for inductive predicates?
- Next by Date: Re: [isabelle] Isabelle2013-RC1 available for testing
- Previous by Thread: Re: [isabelle] Explanation of induction rules for inductive predicates?
- Next by Thread: Re: [isabelle] Explanation of induction rules for inductive predicates?
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list