嵌套案例Isar

Question

我在Isar:中尝试"具体语义"的练习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

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

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

2. 在某些情况下，您应该使用?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