*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Remaining Cases in Induction Proofs*From*: Patrick Michel <uni at pbmichel.de>*Date*: Mon, 18 Jun 2012 10:06:13 +0200

Hi! I am working with a five-way mutual recursive set of datatypes, that have a combined count of 27 constructors. For induction proofs over these datatypes this means proving 27 cases at minimum, sometimes more, as I often have multiple properties to prove for one of the types at once. Many of these proofs can be done "by (induct v and p and d and r and l) auto", provided I have good lemmas and auto doesn't choke. In other proofs I cam fine with listing all the cases and doing the "proof (induct v and p and d and r and l)", as many cases need different tactics. What I am worried about are the cases in between. Sometimes there really are only three interesting cases, the rest works "by auto". If auto doesn't choke on these three, I can do the proofs in apply style of course, but I try to avoid apply proofs. So with "proof" these proofs look like this: proof (induct v and p and d and r and l) case A: … next case B: … next case C: … next case rest1 thus ?case by auto next case rest2 thus ?case by auto next case rest3 thus ?case by auto next … qed Where "restX" goes up to 27, as said, or even worse these cases can have sub cases, etc. pp. The same situation arises with induction theorems from complex functions that match more than one parameter. The way Isabelle disambiguates the equations is to unfold all combinations. In a recent proof I had to proof the cases 1 to 7, 8_1 to 8_3 and 9_1 to 9_27. Thereof only 1 to 8_3 where interesting and were followed by 27 lines of boilerplate cases :-) Now I know some possible ways to get out of this mess: 1) pick another induction scheme 2) if necessary, define one via a terminating function 3) in the case of the function example above: change the definition by avoiding to match another parameter (which can complicate things and in general makes the function harder to read) 4) find more lemmas so the proof works "by (induct v and p and d and r and l) auto" again, or something comparable in size In the past weeks, however, I found myself in several situation where I could not come up with a good solution. Which brings me to my original point :-D I would love to just rewrite the above proof to something like: proof (induct v and p and d and r and l) case A: … next case B: … next case C: … next remaining_cases by auto qed Where "remaining_cases" presents me with the exact proof state I see after the last next. I.e., I can pick all the "cherries" from the cases, proof them nicely, and dispose of the rest. That would be incredibly useful to me. So has this been considered? Is it easy/hard to implement? Is it already possible and I missed it? Thanks in advance, Patrick Michel Software Technology Group University of Kaiserslautern, Germany

**Follow-Ups**:**Re: [isabelle] Remaining Cases in Induction Proofs***From:*Brian Huffman

**Re: [isabelle] Remaining Cases in Induction Proofs***From:*René Thiemann

- Previous by Date: Re: [isabelle] Enabling unification tracing in Isabelle/jEdit.
- Next by Date: Re: [isabelle] Remaining Cases in Induction Proofs
- Previous by Thread: Re: [isabelle] Enabling unification tracing in Isabelle/jEdit.
- Next by Thread: Re: [isabelle] Remaining Cases in Induction Proofs
- Cl-isabelle-users June 2012 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