嵌套案例 Isar

Question

我在 Isar 中尝试做 'Concrete Semantics' 的练习 4.5 时遇到了一些问题：

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)

我正在 Illegal schematic variable(s) in case "aSb"⌂ 我也怀疑在 Sε 中我不能引用 ?case，我得到 Unbound schematic variable: ?case。我在想，也许问题是我在入职培训中有案例？

Answer 1

根据评论总结，你有两个问题：

cases "l" rule: S.induct 毫无意义，您应该使用嵌套归纳 induction l rule: S.induct 或区分大小写 cases l rule: S.cases
在案例中，您应该使用 ?thesis 而不是 Isabelle/jEdit 大纲告诉您的案例（您可以单击那个东西将其插入缓冲区！）。这样你也可以在 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

嵌套案例 Isar

Nested cases Isar

isabelle

isar