How can I properly import the definition of bit_nat from HOL.Bit_Operations?
Working code, with copying the definition into current theory:
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
Tried adding import HOL.Bit_Operations, code does not work:
theory Scratch
imports Main HOL.Bit_Operations
begin
value "bit_nat 5 0"
(* "bit_nat (1 + 1 + (1 + 1) + 1) 0" :: "'c" *)
end
A close look into HOL.Bit_Operations reveals that bit_nat is defined in the context of instantiating type class semiring_bits with type nat. (For background on type classes, see: Haskell-style type classes with Isabelle/Isar.)
instantiation nat :: semiring_bits
begin (* !!! *)
definition bit_nat :: ‹nat ⇒ nat ⇒ bool›
where ‹bit_nat m n ⟷ odd (m div 2 ^ n)›
[...]
end
This leads to the function being accessible by the name provided in the type class, which is bit:
class semiring_bits = semiring_parity +
[...]
fixes bit :: ‹'a ⇒ nat ⇒ bool›
Accordingly, your importing theory can use the desired function like this:
value ‹bit (5::nat) 0›
(* "True" :: "bool" *)
(In order to resolve the function correctly, we have to provide a type, because bit (5::int) 0 would be another option.)