In the below code:
inductive T :: "alpha list ⇒ bool" where
Tε : "T []" |
TaTb : "T l ⟹ T r ⟹ T (l @ a#(r @ [b]))"
lemma Tapp: "⟦T l; T r⟧ ⟹ T (l@r)"
proof (induction l arbitrary: r rule: T.induct)
case Tε
then show ?case by (simp add: Tε)
next
case (TaTb l r) then show ?case
I am in the state:
proof (prove)
using this:
T l
T ra__
T ?r ⟹ T (l @ ?r)
T ?r ⟹ T (ra__ @ ?r)
T r
goal (1 subgoal):
1. T ((l @ a # ra__ @ [b]) @ r)
However, I cannot reference this ra__
, getting Bad name: "ra__"⌂
, however, I need to reference it. How do I bind it?
Your proof text is trying to give two different variables the name r
. For your case pattern try a different name, e.g. case(TaTb l r')
. You will get the same proof state except r'
instead of ra__
.