Isabelle/HOL中bool类型无法使用xor操作的报错原因咨询

问题原因 #

你使用的xor操作符是Isabelle/HOL中属于semiring_bit_operations类型类的通用位操作函数，该类针对具备环结构的数值类型（比如整数、位向量等）设计，而bool类型默认并未被纳入这个类型类范畴，因此直接调用xor处理bool值会触发类型不匹配错误。

解决办法 #

方法1：用布尔逻辑等价式替代 #

布尔类型的异或逻辑完全等价于两个值不相等，可以直接用a ≠ b替换xor a b，修改后的代码如下：

fun halfadder :: "bool * bool ⇒ bool * bool"
where
  "halfadder (a,b) = (
     let s = a ≠ b in
     let cout = a ∧ b in
     (cout,s))"

方法2：导入布尔专用的异或操作 #

若你更倾向于使用xor符号，可以导入HOL.Bool理论中定义的布尔专属xor操作（该操作仅针对bool类型，和通用位操作的xor并非同一符号），修改后的代码需先添加导入声明：

theory HalfAdder
imports HOL.Bool
begin

fun halfadder :: "bool * bool ⇒ bool * bool"
where
  "halfadder (a,b) = (
     let s = xor a b in
     let cout = a ∧ b in
     (cout,s))"

end

补充说明 #

你提到用xor处理其他数据类型也报错，大概率是因为未导入对应类型的位操作理论库。比如处理整数需导入HOL-Library.Bit_Operations，处理位向量需导入HOL-Word.Word，同时要确保目标类型属于semiring_bit_operations类范畴。

内容的提问来源于stack exchange，提问作者fred