无法访问 HOL.Bit_Operations 中的定义

Question

如何从 HOL.Bit_Operations 正确导入

bit_nat

的定义？

工作代码，将定义复制到当前理论中：

theory Scratch
imports Main 
begin

definition bit_nat :: ‹nat ⇒ nat ⇒ bool›
  where ‹bit_nat m n ⟷ odd (m div 2 ^ n)›

value "bit_nat 5 0" 
(* "True" :: "bool" *)

end 

尝试添加 import HOL.Bit_Operations，代码不起作用：

theory Scratch
imports Main HOL.Bit_Operations
begin

value "bit_nat 5 0" 
(* "bit_nat (1 + 1 + (1 + 1) + 1) 0" :: "'c" *)

end 

Answer 1

仔细研究

HOL.Bit_Operations

会发现，

bit_nat

是在使用类型 semiring_bits 实例化类型类

nat

的上下文中定义的。 （有关类型类的背景，请参阅：Isabelle/Isar 的 Haskell 风格类型类。）

instantiation nat :: semiring_bits
begin (* !!! *)

definition bit_nat :: ‹nat ⇒ nat ⇒ bool›
  where ‹bit_nat m n ⟷ odd (m div 2 ^ n)›

[...]

end

这导致可以通过类型类中提供的名称来访问该函数，即

bit

:

class semiring_bits = semiring_parity +
  [...]
  fixes bit :: ‹'a ⇒ nat ⇒ bool›

因此，您的导入理论可以使用所需的函数，如下所示：

value ‹bit (5::nat) 0›
(* "True" :: "bool" *)

（为了正确解析函数，我们必须提供一个类型，因为

bit (5::int) 0

将是另一种选择。）