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:
> 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
Institut für Informatik (I7)
Technische Universität München
85748 Garching b. München
Office: MI 03.11.055
This archive was generated by a fusion of
Pipermail (Mailman edition) and