*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Splitting case-expressions automatically*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 30 Jun 2008 18:48:09 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4868FB57.7010404@uni-muenster.de>*References*: <4868FB57.7010404@uni-muenster.de>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

lemma [rule_format]: "[| !t. x:(case t of A => s1 | B => s2 | C => s3) --> P; x:s2 |] ==> P" by(auto split: test.splits) Tobias Peter Lammich wrote:

Hi all, given the following datatype datatype test = A | B | Chow can I prove the following subgoal automatically with one (or a few)apply statements. I want to avoid to make the proof explicit in Isar,because of the writing overhead."[| !!t. x:(case t of A => s1 | B => s2 | C => s3) ==> P; x:s2 |] ==> P"something like (auto split: test.splits) does not work, am I missingsome lemmas or is there a way to explicitly instantiating t ?Thanks for any hints in advance, Peter

**Follow-Ups**:**Re: [isabelle] Splitting case-expressions automatically***From:*Brian Huffman

**References**:**[isabelle] Splitting case-expressions automatically***From:*Peter Lammich

- Previous by Date: [isabelle] Splitting case-expressions automatically
- Next by Date: Re: [isabelle] Splitting case-expressions automatically
- Previous by Thread: [isabelle] Splitting case-expressions automatically
- Next by Thread: Re: [isabelle] Splitting case-expressions automatically
- Cl-isabelle-users June 2008 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