isabelle

Cannot access definition in HOL.Bit_Operations


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 

Solution

  • 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.)