isabelle - 如何在 Isabelle 的归纳类型规范中添加其他类型变量？

Question

我定义了一个这样的归纳类型：

inductive I :: "tau ⇒ bool" where
rule0: "I C0" |
rule1: "I x" |
rule2: "Q x ⟹ I x" |
rule3: "Q x ⟹ I x'" |
rule4: "Q x ⟹ I (C1 x)" |
rule5: "Q (C1 x) ⟹ I x" |
rule6: "Q (C1 x) ⟹ I x'" |
rule7: "Q x ⟹ I (C2 x' x'')"

我认为这就足够了，但伊莎贝尔抱怨/警告我：

Additional type variable(s) in specification of "I": 'a, 'b 

我不明白这是什么意思。我知道这是说我应该把归纳谓词放在某个地方接受任何两种类型（如类型变量'a和所示'b）。但这不是我想做的。我只希望输入始终是以下类型tau：

datatype tau = 
C0 |
C1 tau |
C2 tau tau

显然，这些定义是虚构的，并不是真的要证明什么。我只是好奇地检查它使用这些定义生成的定理（特别是归纳法）。

1）我如何让它停止抱怨我的变量是任意类型并让它们始终是类型tau？

---

另外，我真的很好奇投诉的含义以及如何使用它是建议的语法来解决'a它'b。虽然这不是我最初的意图，但我很想看到我的归纳谓词的更一般定义，并看看它会产生什么 iduct 定理。

2) 如何用 Isabelle 想要的任意类型定义我的归纳谓词？我在哪里'a和'b定义？如果我不这样做会发生什么？

标签： isabelletheorem-proving

Answer 1

为了限制我的规则中的类型，我可以修饰归纳定义中的类型I：

inductive I :: "tau ⇒ bool"  where
rule0: "I C0" |
rule1: "I x" |
rule2: "Q x ⟹ I x" |
rule3: "Q (x::tau) ⟹ I x'" |
rule4: "Q x ⟹ I (C1 x)" |
rule5: "Q (C1 x) ⟹ I x" |
rule6: "Q (C1 x) ⟹ I x'" |
rule7: "Q (x::tau) ⟹ I (C2 x' x'')"

现在的定理是这样的：

thm I.induct

⟦I ?x; ?P C0; ⋀x. ?P x; ⋀Q x. Q x ⟹ ?P x; ⋀Q x x'. Q x ⟹ ?P x'; ⋀Q x. Q x ⟹ ?P (C1 x); ⋀Q x. Q (C1 x) ⟹ ?P x; ⋀Q x x'. Q (C1 x) ⟹ ?P x'; ⋀Q x x' x''. Q x ⟹ ?P (C2 x' x'')⟧ ⟹ ?P ?x

谢谢曼努埃尔·埃伯尔！