isabelle - 嵌套案例 Isar

Answer 1

正如评论所总结的，您有两个问题：

1. cases "l" rule: S.induct没有什么意义，您应该使用嵌套归纳induction l rule: S.induct或区分大小写cases l rule: S.cases

2. 如果您应该使用?thesisIsabelle/jEdit 大纲告诉您的 case 而不是 case（您可以单击那个东西将其插入缓冲区！）。这样，您还可以为 case 中的所有变量命名TaTb。

所以你可能想要这样的东西：

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