Email Gateway (Aug 18 2022 at 18:51): Email Gateway (Aug 18 2022 at 18:51):From: Lars Hupel <hupel@in.tum.de>
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?
Email Gateway (Aug 18 2022 at 18:52):From: Peter Lammich <lammich@in.tum.de>
lemma empty_unaccepted[simp]: "¬ (accepted prods nt [])"
The following should work:
apply (rule)
apply (drule empty_unaccepted_helper)
by auto
Peter
Email Gateway (Aug 18 2022 at 18:52):From: René Neumann <rene.neumann@in.tum.de>
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
Email Gateway (Aug 18 2022 at 18:52):From: Lars Hupel <hupel@in.tum.de>
Thanks. I used a slightly modified version of that where I didn't need
empty_unaccepted_helper, but rather proved the lemma directly in a
sub-proof.
Last updated: Nov 21 2024 at 12:39 UTC