rule1: "I x"
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'')"
我以为这样就够了 但Isabelle却向我抱怨说:
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 在定义中？如果我不这样做会怎样？