[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:
"⟦ 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and