*To*: Dominik Luecke <luecke at informatik.uni-bremen.de>*Subject*: Re: [isabelle] Extensive case splits*From*: Paul Graunke <paul.graunke at galois.com>*Date*: Thu, 09 Aug 2007 08:21:07 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1186579046.30076.18.camel@feuerbach>*References*: <1186417659.18971.5.camel@feuerbach> <34A92F7E-CDC4-43ED-B24F-66389CEAF573@cam.ac.uk> <1186579046.30076.18.camel@feuerbach>*User-agent*: Mozilla-Thunderbird 2.0.0.4 (X11/20070622)

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. Regards, Paul Dominik Luecke wrote:

Hello, 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(in)-equations.I have added a sample goal of the proof to this mail, to make thedescription of this Isabelle problem less abstract.Regards, Dominik On Wed, 2007-08-08 at 12:22 +0100, Lawrence Paulson wrote:This sort of case-splitting easily gives rise to huge numbers ofgoals, but this is best done internally. I assume you have alreadytried 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 thatneed to besplit up into about 23k cases to solve them.

**References**:**[isabelle] Extensive case splits***From:*Dominik Luecke

**Re: [isabelle] Extensive case splits***From:*Lawrence Paulson

**Re: [isabelle] Extensive case splits***From:*Dominik Luecke

- Previous by Date: Re: [isabelle] Strange simplification
- Next by Date: [isabelle] Isabelle version for tutorial?
- Previous by Thread: Re: [isabelle] Extensive case splits
- Next by Thread: [isabelle] Position in Computer Science at The Australian National University
- Cl-isabelle-users August 2007 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