Documentation

Mathlib.Data.Int.Bitwise

Bitwise operations on integers #

Possibly only of archaeological significance.

Recursors #

def Int.div2 :

div2 n = n/2

Equations
Instances For
    def Int.bodd :
    Bool

    bodd n returns true if n is odd

    Equations
    Instances For
      def Int.bit (b : Bool) :

      bit b appends the digit b to the binary representation of its integer input.

      Equations
      Instances For
        def Int.testBit :
        Bool

        testBit m n returns whether the (n+1)ˢᵗ least significant bit is 1 or 0

        Equations
        Instances For
          def Int.natBitwise (f : BoolBoolBool) (m : ) (n : ) :

          Int.natBitwise is an auxiliary definition for Int.bitwise.

          Equations
          Instances For
            def Int.bitwise (f : BoolBoolBool) :

            Int.bitwise applies the function f to pairs of bits in the same position in the binary representations of its inputs.

            Equations
            Instances For
              def Int.lnot :

              lnot flips all the bits in the binary representation of its input

              Equations
              Instances For
                def Int.lor :

                lor takes two integers and returns their bitwise or

                Equations
                Instances For
                  def Int.land :

                  land takes two integers and returns their bitwise and

                  Equations
                  Instances For
                    def Int.ldiff :

                    ldiff a b performs bitwise set difference. For each corresponding pair of bits taken as booleans, say aᵢ and bᵢ, it applies the boolean operation aᵢ ∧ bᵢ to obtain the iᵗʰ bit of the result.

                    Equations
                    Instances For
                      def Int.xor :

                      xor computes the bitwise xor of two natural numbers

                      Equations
                      Instances For

                        m <<< n produces an integer whose binary representation is obtained by left-shifting the binary representation of m by n places

                        Equations
                        • One or more equations did not get rendered due to their size.

                        m >>> n produces an integer whose binary representation is obtained by right-shifting the binary representation of m by n places

                        Equations

                        bitwise ops #

                        @[simp]
                        @[simp]
                        @[simp]
                        theorem Int.bodd_coe (n : ) :
                        (↑n).bodd = n.bodd
                        @[simp]
                        theorem Int.bodd_subNatNat (m : ) (n : ) :
                        (Int.subNatNat m n).bodd = (m.bodd ^^ n.bodd)
                        @[simp]
                        theorem Int.bodd_negOfNat (n : ) :
                        (Int.negOfNat n).bodd = n.bodd
                        @[simp]
                        theorem Int.bodd_neg (n : ) :
                        (-n).bodd = n.bodd
                        @[simp]
                        theorem Int.bodd_add (m : ) (n : ) :
                        (m + n).bodd = (m.bodd ^^ n.bodd)
                        @[simp]
                        theorem Int.bodd_mul (m : ) (n : ) :
                        (m * n).bodd = (m.bodd && n.bodd)
                        theorem Int.bodd_add_div2 (n : ) :
                        (bif n.bodd then 1 else 0) + 2 * n.div2 = n
                        theorem Int.div2_val (n : ) :
                        n.div2 = n / 2
                        theorem Int.bit_val (b : Bool) (n : ) :
                        Int.bit b n = 2 * n + bif b then 1 else 0
                        theorem Int.bit_decomp (n : ) :
                        Int.bit n.bodd n.div2 = n
                        def Int.bitCasesOn {C : Sort u} (n : ) (h : (b : Bool) → (n : ) → C (Int.bit b n)) :
                        C n

                        Defines a function from conditionally, if it is defined for odd and even integers separately using bit.

                        Equations
                        • n.bitCasesOn h = .mpr (h n.bodd n.div2)
                        Instances For
                          @[simp]
                          @[simp]
                          theorem Int.bit_coe_nat (b : Bool) (n : ) :
                          Int.bit b n = (Nat.bit b n)
                          @[simp]
                          theorem Int.bit_negSucc (b : Bool) (n : ) :
                          @[simp]
                          theorem Int.bodd_bit (b : Bool) (n : ) :
                          (Int.bit b n).bodd = b
                          @[simp]
                          theorem Int.testBit_bit_zero (b : Bool) (n : ) :
                          (Int.bit b n).testBit 0 = b
                          @[simp]
                          theorem Int.testBit_bit_succ (m : ) (b : Bool) (n : ) :
                          (Int.bit b n).testBit m.succ = n.testBit m
                          theorem Int.bitwise_diff :
                          (Int.bitwise fun (a b : Bool) => a && !b) = Int.ldiff
                          @[simp]
                          theorem Int.bitwise_bit (f : BoolBoolBool) (a : Bool) (m : ) (b : Bool) (n : ) :
                          Int.bitwise f (Int.bit a m) (Int.bit b n) = Int.bit (f a b) (Int.bitwise f m n)
                          @[simp]
                          theorem Int.lor_bit (a : Bool) (m : ) (b : Bool) (n : ) :
                          (Int.bit a m).lor (Int.bit b n) = Int.bit (a || b) (m.lor n)
                          @[simp]
                          theorem Int.land_bit (a : Bool) (m : ) (b : Bool) (n : ) :
                          (Int.bit a m).land (Int.bit b n) = Int.bit (a && b) (m.land n)
                          @[simp]
                          theorem Int.ldiff_bit (a : Bool) (m : ) (b : Bool) (n : ) :
                          (Int.bit a m).ldiff (Int.bit b n) = Int.bit (a && !b) (m.ldiff n)
                          @[simp]
                          theorem Int.lxor_bit (a : Bool) (m : ) (b : Bool) (n : ) :
                          (Int.bit a m).xor (Int.bit b n) = Int.bit (a ^^ b) (m.xor n)
                          @[simp]
                          theorem Int.lnot_bit (b : Bool) (n : ) :
                          (Int.bit b n).lnot = Int.bit (!b) n.lnot
                          @[simp]
                          theorem Int.testBit_bitwise (f : BoolBoolBool) (m : ) (n : ) (k : ) :
                          (Int.bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)
                          @[simp]
                          theorem Int.testBit_lor (m : ) (n : ) (k : ) :
                          (m.lor n).testBit k = (m.testBit k || n.testBit k)
                          @[simp]
                          theorem Int.testBit_land (m : ) (n : ) (k : ) :
                          (m.land n).testBit k = (m.testBit k && n.testBit k)
                          @[simp]
                          theorem Int.testBit_ldiff (m : ) (n : ) (k : ) :
                          (m.ldiff n).testBit k = (m.testBit k && !n.testBit k)
                          @[simp]
                          theorem Int.testBit_lxor (m : ) (n : ) (k : ) :
                          (m.xor n).testBit k = (m.testBit k ^^ n.testBit k)
                          @[simp]
                          theorem Int.testBit_lnot (n : ) (k : ) :
                          n.lnot.testBit k = !n.testBit k
                          @[simp]
                          theorem Int.shiftLeft_neg (m : ) (n : ) :
                          m <<< (-n) = m >>> n
                          @[simp]
                          theorem Int.shiftRight_neg (m : ) (n : ) :
                          m >>> (-n) = m <<< n
                          @[simp]
                          theorem Int.shiftLeft_coe_nat (m : ) (n : ) :
                          m <<< n = (m <<< n)
                          @[simp]
                          theorem Int.shiftRight_coe_nat (m : ) (n : ) :
                          m >>> n = (m >>> n)
                          @[simp]
                          theorem Int.shiftRight_negSucc (m : ) (n : ) :
                          theorem Int.shiftRight_add' (m : ) (n : ) (k : ) :
                          m >>> (n + k) = m >>> n >>> k

                          Compare with Int.shiftRight_add, which doesn't have the coercions ℕ → ℤ.

                          bitwise ops #

                          theorem Int.shiftLeft_add (m : ) (n : ) (k : ) :
                          m <<< (n + k) = m <<< n <<< k
                          theorem Int.shiftLeft_sub (m : ) (n : ) (k : ) :
                          m <<< (n - k) = m <<< n >>> k
                          theorem Int.shiftLeft_eq_mul_pow (m : ) (n : ) :
                          m <<< n = m * (2 ^ n)
                          theorem Int.one_shiftLeft (n : ) :
                          1 <<< n = (2 ^ n)
                          @[simp]
                          theorem Int.zero_shiftLeft (n : ) :
                          0 <<< n = 0
                          @[simp]
                          theorem Int.zero_shiftRight' (n : ) :
                          0 >>> n = 0

                          Compare with Int.zero_shiftRight, which has n : ℕ.