如何在 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 语法修复它，这是建议。虽然这不是我最初的意图，但我很想看看我的归纳谓词的更一般定义，看看它会产生什么归纳定理。

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

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

感谢曼努埃尔·埃伯尔！