Re: [isabelle] Extensive case splits

I've also had issues with large terms, say a list of nats, and just performing a single call to subst, let alone simp. I would guess that using unification for
the P in the conclusion of ssubst, checking equality of terms (like the two
instances of P in the premise of ssubst), and implementing beta reduction
via explicit substitution all contribute.  I'm only guessing though.


Dominik Luecke wrote:

first of all... Thanks for all the answers.

I did try that, but after several hours of no real life-sign of Isabelle
I got bored and stopped the process. I thought that it might be an idea,
to somehow break down the stuff to smaller steps, so that you can at
least see if anything is really happening, or if Isabelle is just doing
something stupid for hours. The main problem is that the proof goal is
very, very big (already considered in the number of involved
I have added a sample goal of the proof to this mail, to make the
description of this Isabelle problem less abstract.

On Wed, 2007-08-08 at 12:22 +0100, Lawrence Paulson wrote:
This sort of case-splitting easily gives rise to huge numbers of goals, but this is best done internally. I assume you have already tried auto and force on them?
Larry Paulson

On 6 Aug 2007, at 17:27, Dominik Luecke wrote:

I am currently trying to prove a theorems that involve lots of case
splits in the proof process. I mean the single sub-goals a solvable by

  apply (erule disjE)+
  apply (simp)
  apply (simp)

... Any speedup would help, especially since there are goals that need to be
split up into about 23k cases to solve them.

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