# Re: [isabelle] Introducing a variable from a constant

Am 25.12.2011 20:12, schrieb Lars Hupel:
> 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?
>
>
>
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
- René
--
René Neumann
Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München
Tel: +49-89-289-17232
Office: MI 03.11.055

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*