*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Introducing a variable from a constant*From*: Lars Hupel <hupel at in.tum.de>*Date*: Tue, 27 Dec 2011 19:03:12 +0100*In-reply-to*: <4EF7B08D.3050402@in.tum.de>*References*: <jd7si9$6uc$1@dough.gmane.org> <4EF7B08D.3050402@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:9.0) Gecko/20111224 Thunderbird/9.0.1

> lemma empty_unaccepted[simp]: "¬ (accepted prods nt [])" > proof (rule notI) > assume "accepted prods nt []" > with empty_unaccepted_helper[OF this] show "False" by simp > qed Thanks. I used a slightly modified version of that where I didn't need `empty_unaccepted_helper`, but rather proved the lemma directly in a sub-proof.

**References**:**[isabelle] Introducing a variable from a constant***From:*Lars Hupel

**Re: [isabelle] Introducing a variable from a constant***From:*René Neumann

- Previous by Date: Re: [isabelle] Introducing a variable from a constant
- Next by Date: [isabelle] Induction over n for a proposition ALL k <= n
- Previous by Thread: Re: [isabelle] Introducing a variable from a constant
- Next by Thread: [isabelle] Induction over n for a proposition ALL k <= n
- Cl-isabelle-users December 2011 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