Primitive recursive binary operations

Primitive recursion certificates for exponentiation, bit inspection, the increasing list of set bits, and binary bitwise operations. These certificates allow finite sets represented by binary natural numbers to be used in effective constructions.

theorem Primrec.nat_pow : Primrec₂ fun (x1 x2 : ℕ) => x1 ^ x2

Natural-number exponentiation is primitive recursive.

theorem Primrec.nat_testBit : Primrec₂ Nat.testBit

Inspecting a binary digit is primitive recursive.

theorem Primrec.nat_bitIndices : Primrec Nat.bitIndices

The increasing list of set bits is primitive recursive.

theorem Primrec.nat_bitwise (f : Bool → Bool → Bool) (hf : f false false = false) : Primrec₂ (Nat.bitwise f)

Binary bitwise operations that send two zero bits to zero are primitive recursive.

theorem Primrec.nat_lor : Primrec₂ Nat.lor

Binary union is primitive recursive.

theorem Primrec.nat_land : Primrec₂ Nat.land

Binary intersection is primitive recursive.

theorem Primrec.nat_ldiff : Primrec₂ Nat.ldiff

Binary difference is primitive recursive.