isabelleisar

Induction introduces 'bad name'


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?


Solution

  • 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__.