[isabelle] Remaining Cases in Induction Proofs



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





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