Re: [isabelle] Remaining Cases in Induction Proofs



Hi Patrick,

I believe that you are looking for the following pattern:

proof (induct v and p and d and r and l)
 case A: … next
 case B: … next
 case C: … next
qed auto

That is, you give a final proof method after "qed" to solve the remaining cases.

- Brian

On Mon, Jun 18, 2012 at 10:06 AM, Patrick Michel <uni at pbmichel.de> wrote:
> 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.