Nested cases Isar

Question

I'm having some issues trying to do exercise 4.5 of 'Concrete Semantics' in Isar:

inductive S :: "alpha list ⇒ bool" where
 Sε : "S []" |
 aSb : "S m ⟹ S (a#m @ [b])" |
 SS : "S l ⟹ S r ⟹ S (l @ r)"

inductive T :: "alpha list ⇒ bool" where
 Tε : "T []" |
 TaTb : "T l ⟹ T r ⟹ T (l @ a#(r @ [b]))"

lemma TS: "T w ⟹ S w"
proof (induction w rule: T.induct)
  case Tε 
  show ?case by (simp add:Sε)
  case (TaTb l r) show ?case using TaTb.IH(1) (* This being S l, which allows us to case-split on l using S.induct *)
  proof (cases "l" rule: S.induct)
    case Sε
    then show ?case by (simp add: TaTb.IH(2) aSb)
  next case (aSb m)

I'm getting Illegal schematic variable(s) in case "aSb"⌂ Also I find suspicious that in Sε I cannot refer to ?case, I get Unbound schematic variable: ?case. I'm thinking that maybe the problem is that I have a cases in an induction?

Answer 1

As summarized by the comments, you have two problems:

1. cases "l" rule: S.induct makes little sense and you should either use a nested induction induction l rule: S.induct or a case distinction cases l rule: S.cases

2. In cases you should use ?thesis instead of cases as the Isabelle/jEdit outline tells you (you can click on that thing to insert it into the buffer!). That way you would also have given a name to all variable in the case TaTb.

So you probably want something like:

lemma TS: "T w ⟹ S w"
proof (induction w rule: T.induct)
  case Tε 
  show ?case by (simp add:Sε)
next
  case (TaTb l r a b) show ?case using TaTb.IH(1)
  proof (cases "l" rule: S.cases)
    case Sε
    then show ?thesis sorry
  next
    case (aSb m a b)
    then show ?thesis sorry
  next
    case (SS l r)
    then show ?thesis sorry
  qed
qed