Can erule produce erroneous subgoals?

Question

I have the following grammar defined in Isabelle:

inductive S where
  S_empty: "S []" |
  S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
  S_paren: "S xs ⟹ S (Open # xs @ [Close])"

Then I define a gramar T that conceptually only adds the following rule:

  T_left: "T xs ⟹ T (Open # xs)"

Then I tried to proof the following theorem:

theorem T_S:
  "T xs ⟹ count xs Open = count xs Close ⟹ S xs"
  apply(erule T.induct)
  apply(simp add: S_empty)
  apply(simp add: S_append)
  apply(simp add: S_paren)
  oops

To my surprise the final goal seems to be false:

⋀xsa. count xs Open = count xs Close ⟹ T xsa ⟹ S xsa ⟹ S (Open # xsa)

So here S (Open # xsa) cannot hold because there is no such production in the grammar assuming S xsa.

This situation makes no-sense to me? Is erule producing goals that are false?

Answer 1

Induction rules like T.induct should usually be used with the induction proof method rather than erule. The induction method ensures that the whole statement becomes part of the inductive statements whereas with erule only the conclusion is part of the inductive argument; other assumptions are basically ignored for the induction. This can be seen in the last goal state where the inductive statement involves the goal parameter xsa whereas the crucial assumption count xs Open = count xs Close still talks about the variable xs. So, the proof step should be apply(induction rule: T.induct). Then there is a chance to prove this statement.