[isabelle] Introducing a variable from a constant



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?






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