*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Splitting case-expressions automatically*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 30 Jun 2008 15:46:52 -0700*In-reply-to*: <48690E49.5040301@in.tum.de>*References*: <4868FB57.7010404@uni-muenster.de> <48690E49.5040301@in.tum.de>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

lemma "[| !!t. x:(case t of A => s1 | B => s2 | C => s3) ==> P; x:s2 |] ==> P" by (atomize, auto split: test.splits)

lemma "[| !!t. x:(case t of A => s1 | B => s2 | C => s3) ==> P; x:s2 |] ==> P" by (drule meta_spec [where x=B], simp) - Brian Quoting Tobias Nipkow <nipkow at in.tum.de>:

The problem are the deeply nested meta-logical symbols that the split facility seems unable to cope with. If you reformulate it a bit, it works: 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 afew) apply statements. I want to avoid to make the proof explicitin 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 Imissing some lemmas or is there a way to explicitly instantiating t ?Thanks for any hints in advance, Peter

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

**Re: [isabelle] Splitting case-expressions automatically***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Splitting case-expressions automatically
- Previous 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