*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Introducing a variable from a constant*From*: Lars Hupel <hupel at in.tum.de>*Date*: Sun, 25 Dec 2011 20:12:09 +0100*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:9.0) Gecko/20111224 Thunderbird/9.0.1

I'm trying to formalize that for a particular grammar, there is no production which accepts the empty word. Thus, I wrote the following lemma: lemma empty_unaccepted_helper: "⟦ accepted prods nt bs; bs = [] ⟧ ⟹ False" by (induction rule: accepted.induct) auto Now I want to make that fact explicit: lemma empty_unaccepted[simp]: "¬ (accepted prods nt [])" My idea is the following: proof assume "accepted prods nt []" hence "accepted prods nt bs ∧ bs = []" (* and now? *) I know that this is a rather naive approach and as expected it didn't work. Any idea on how I could do that?

**Follow-Ups**:**Re: [isabelle] Introducing a variable from a constant***From:*Peter Lammich

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

- Previous by Date: [isabelle] Announcement: workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)
- Next by Date: Re: [isabelle] Introducing a variable from a constant
- Previous by Thread: [isabelle] Announcement: workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)
- Next by Thread: Re: [isabelle] Introducing a variable from a constant
- 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