Theory BitRing

theory BitRing
imports BooleanAlgebra BinInduct
begin

subsection {* Syntactic class for bitwise operations *}

axclass bit ⊆ type

consts
  bitNOT  :: "'a::bit => 'a"       ("NOT _" [81] 80)
  bitAND  :: "'a::bit => 'a => 'a" (infixr "AND" 70)
  bitOR   :: "'a::bit => 'a => 'a" (infixr "OR"  65)
  bitXOR  :: "'a::bit => 'a => 'a" (infixr "XOR" 65)
  testbit :: "'a::bit => nat => bool"
  shiftL  :: "'a::bit => nat => 'a" (* infixl "<<<" *)
  shiftR  :: "'a::bit => nat => 'a" (* infixr ">>>" *)

syntax (xsymbols)
  bitNOT :: "'a::bit => 'a"       ("¬b _" [81] 80)
  bitAND :: "'a::bit => 'a => 'a" (infixr "∧b" 70)
  bitOR  :: "'a::bit => 'a => 'a" (infixr "∨b" 65)
  bitXOR :: "'a::bit => 'a => 'a" (infixr "⊕b" 65)

syntax (HTML output)
  bitNOT :: "'a::bit => 'a"       ("¬b _" [81] 80)
  bitAND :: "'a::bit => 'a => 'a" (infixr "∧b" 70)
  bitOR  :: "'a::bit => 'a => 'a" (infixr "∨b" 65)
  bitXOR :: "'a::bit => 'a => 'a" (infixr "⊕b" 65)

subsection {* Bitwise operations on type @{typ bit} *}

instance bit :: bit ..

defs (overloaded)
  NOT_bit_def: "NOT x ≡ case x of bit.B0 => bit.B1 | bit.B1 => bit.B0"
  AND_bit_def: "x AND y ≡ case x of bit.B0 => bit.B0 | bit.B1 => y"
  OR_bit_def: "x OR y :: bit ≡ NOT (NOT x AND NOT y)"
  XOR_bit_def: "x XOR y :: bit ≡ (x AND NOT y) OR (NOT x AND y)"

lemma bit_simps [simp]:
  "NOT bit.B0 = bit.B1"
  "NOT bit.B1 = bit.B0"
  "bit.B0 AND y = bit.B0"
  "bit.B1 AND y = y"
  "bit.B0 OR y = y"
  "bit.B1 OR y = bit.B1"
  "bit.B0 XOR y = y"
  "bit.B1 XOR y = NOT y"
by (simp_all add: NOT_bit_def AND_bit_def OR_bit_def
                  XOR_bit_def split: bit.split)

lemma bit_NOT_NOT: "NOT (NOT (b::bit)) = b"
by (induct b) simp_all

subsection {* Bitwise operations on type @{typ int} *}

instance int :: bit ..

consts intAND :: "int => int => int"

defs (overloaded)
  NOT_int_def: "NOT (x::int) ≡ - (x + 1)"
  AND_int_def: "x AND y ≡ intAND x y"
  OR_int_def: "x OR y :: int ≡ NOT (NOT x AND NOT y)"
  XOR_int_def: "x XOR y :: int ≡ (x AND NOT y) OR (NOT x AND y)"

lemma NOT_int_pred: "NOT x = Numeral.pred (- x)"
by (simp add: NOT_int_def pred_def)

lemma NOT_int_succ: "NOT x = - Numeral.succ x"
by (simp add: NOT_int_def succ_def)

lemma NOT_Pls: "NOT Numeral.Pls = Numeral.Min"
by (simp add: NOT_int_succ)

lemma NOT_Min: "NOT Numeral.Min = Numeral.Pls"
by (simp add: NOT_int_succ)

lemma NOT_BIT_0: "NOT (w BIT bit.B0) = (NOT w) BIT bit.B1"
by (simp add: NOT_int_pred)

lemma NOT_BIT_1: "NOT (w BIT bit.B1) = (NOT w) BIT bit.B0"
by (simp add: NOT_int_succ)

lemma NOT_BIT: "NOT (x BIT b) = (NOT x) BIT (NOT b)"
by (induct b) (simp_all add: NOT_BIT_0 NOT_BIT_1)

lemma int_NOT_NOT: "NOT (NOT (x::int)) = x"
apply (induct x rule: BIT_induct)
apply (simp_all add: NOT_Pls NOT_Min NOT_BIT)
done

recdef intAND "{(div2 w, w) |w. w ≠ Numeral.Pls ∧ w ≠ Numeral.Min}"
  "intAND x = (λy.
    if x = Numeral.Pls then Numeral.Pls else
    if x = Numeral.Min then y else
    (intAND (div2 x) (div2 y) BIT (lsb x AND lsb y)))"
  (hints recdef_wf: wf_div2)

declare intAND.simps [simp del]

lemma intAND_Pls: "intAND Numeral.Pls y = Numeral.Pls"
by (subst intAND.simps) simp

lemma intAND_Min: "intAND Numeral.Min y = y"
by (subst intAND.simps) simp

lemma intAND_BIT_BIT:
  "intAND (x BIT a) (y BIT b) = (intAND x y) BIT (a AND b)"
apply (subst intAND.simps)
apply (simp add: intAND_Pls intAND_Min)
done

lemma AND_Pls: "Numeral.Pls AND x = Numeral.Pls"
by (simp add: AND_int_def intAND_Pls)

lemma AND_Min: "Numeral.Min AND x = x"
by (simp add: AND_int_def intAND_Min)

lemma AND_BIT_0: "x BIT bit.B0 AND y BIT b = (x AND y) BIT bit.B0"
by (simp add: AND_int_def intAND_BIT_BIT)

lemma AND_BIT_1: "x BIT bit.B1 AND y BIT b = (x AND y) BIT b"
by (simp add: AND_int_def intAND_BIT_BIT)

lemma AND_Pls_right: "x AND Numeral.Pls = Numeral.Pls"
apply (induct x rule: BIT_induct)
apply (rule AND_Pls)
apply (rule AND_Min)
apply (subst Pls_0_eq [symmetric], subst AND_BIT_0, simp)
apply (subst Pls_0_eq [symmetric], subst AND_BIT_1, simp)
done

lemma AND_Min_right: "x AND Numeral.Min = x"
apply (induct x rule: BIT_induct)
apply (rule AND_Pls)
apply (rule AND_Min)
apply (subst Min_1_eq [symmetric], subst AND_BIT_0, simp)
apply (subst Min_1_eq [symmetric], subst AND_BIT_1, simp)
done

lemma OR_Pls: "Numeral.Pls OR x = x"
by (simp add: OR_int_def NOT_Pls NOT_Min AND_Min int_NOT_NOT)

lemma OR_Min: "Numeral.Min OR x = Numeral.Min"
by (simp add: OR_int_def NOT_Pls NOT_Min AND_Pls)

lemma OR_BIT_0: "x BIT bit.B0 OR y BIT b = (x OR y) BIT b"
by (simp add: OR_int_def NOT_BIT AND_BIT_1 bit_NOT_NOT)

lemma OR_BIT_1: "x BIT bit.B1 OR y BIT b = (x OR y) BIT bit.B1"
by (simp add: OR_int_def NOT_BIT AND_BIT_0)

lemma OR_Pls_right: "x OR Numeral.Pls = x"
by (simp add: OR_int_def NOT_Pls AND_Min_right int_NOT_NOT)

lemma OR_Min_right: "x OR Numeral.Min = Numeral.Min"
by (simp add: OR_int_def NOT_Min AND_Pls_right NOT_Pls)

lemma XOR_Pls: "Numeral.Pls XOR x = x"
by (simp add: XOR_int_def AND_Pls AND_Min OR_Pls NOT_Pls)

lemma XOR_Min: "Numeral.Min XOR x = NOT x"
by (simp add: XOR_int_def AND_Pls AND_Min NOT_Min OR_Pls_right)

lemma XOR_BIT_0: "x BIT bit.B0 XOR y BIT b = (x XOR y) BIT b"
by (simp add: XOR_int_def NOT_BIT AND_BIT_0 AND_BIT_1 OR_BIT_0)

lemma XOR_BIT_10: "x BIT bit.B1 XOR y BIT bit.B0 = (x XOR y) BIT bit.B1"
by (simp add: XOR_int_def NOT_BIT AND_BIT_0 AND_BIT_1 OR_BIT_1)

lemma XOR_BIT_11: "x BIT bit.B1 XOR y BIT bit.B1 = (x XOR y) BIT bit.B0"
by (simp add: XOR_int_def NOT_BIT AND_BIT_0 AND_BIT_1 OR_BIT_0)

lemma XOR_Pls_right: "x XOR Numeral.Pls = x"
by (simp add: XOR_int_def NOT_Pls AND_Min_right AND_Pls_right OR_Pls_right)

lemma XOR_Min_right: "x XOR Numeral.Min = NOT x"
by (simp add: XOR_int_def NOT_Min AND_Pls_right AND_Min_right OR_Pls)

lemmas bitwise_arith_simps [simp] =
  NOT_Pls NOT_Min NOT_BIT_0 NOT_BIT_1
  AND_Pls AND_Min AND_BIT_0 AND_BIT_1
  AND_Pls_right AND_Min_right
  OR_Pls OR_Min OR_BIT_0 OR_BIT_1
  OR_Pls_right OR_Min_right
  XOR_Pls XOR_Min XOR_BIT_0 XOR_BIT_10 XOR_BIT_11
  XOR_Pls_right XOR_Min_right

subsection {* Bitwise ops with getbit, lsb, div2 *}

lemma lsb_NOT: "lsb (NOT x) = NOT (lsb x)"
by (induct x rule: BIT_induct) simp_all

lemma div2_NOT: "div2 (NOT x) = NOT (div2 x)"
by (induct x rule: BIT_induct) simp_all

lemma lsb_AND: "lsb (x AND y) = lsb x AND lsb y"
apply (induct x rule: BIT_induct)
apply simp
apply simp
apply (subst div2_BIT_lsb [symmetric, of y], simp)
apply (subst div2_BIT_lsb [symmetric, of y], simp)
done

lemma div2_AND: "div2 (x AND y) = div2 x AND div2 y"
apply (induct x rule: BIT_induct)
apply simp
apply simp
apply (subst div2_BIT_lsb [symmetric, of y], simp)
apply (subst div2_BIT_lsb [symmetric, of y], simp)
done

lemma lsb_OR: "lsb (x OR y) = lsb x OR lsb y"
by (simp add: OR_int_def OR_bit_def lsb_NOT lsb_AND)

lemma div2_OR: "div2 (x OR y) = div2 x OR div2 y"
by (simp add: OR_int_def div2_NOT div2_AND)

lemma lsb_XOR: "lsb (x XOR y) = lsb x XOR lsb y"
by (simp add: XOR_int_def XOR_bit_def lsb_NOT lsb_AND lsb_OR)

lemma div2_XOR: "div2 (x XOR y) = div2 x XOR div2 y"
by (simp add: XOR_int_def div2_NOT div2_AND div2_OR)

lemma getbit_NOT: "getbit (NOT x) n = NOT (getbit x n)"
by (induct n arbitrary: x, simp add: lsb_NOT, simp add: div2_NOT)

lemma getbit_AND: "getbit (x AND y) n = getbit x n AND getbit y n"
by (induct n arbitrary: x y, simp add: lsb_AND, simp add: div2_AND)

lemma getbit_OR: "getbit (x OR y) n = getbit x n OR getbit y n"
by (induct n arbitrary: x y, simp add: lsb_OR, simp add: div2_OR)

lemma getbit_XOR: "getbit (x XOR y) n = getbit x n XOR getbit y n"
by (induct n arbitrary: x y, simp add: lsb_XOR, simp add: div2_XOR)

defs (overloaded)
  testbit_int_def:
  "testbit x n ≡ case getbit x n of bit.B0 => False | bit.B1 => True"

lemma testbit_int_NOT: "testbit (NOT x::int) n = (¬ testbit x n)"
by (simp add: testbit_int_def getbit_NOT split: bit.split)

lemma testbit_int_AND:
  "testbit (x AND y::int) n = (testbit x n ∧ testbit y n)"
by (simp add: testbit_int_def getbit_AND split: bit.split)

lemma testbit_int_OR:
  "testbit (x OR y::int) n = (testbit x n ∨ testbit y n)"
by (simp add: testbit_int_def getbit_OR split: bit.split)

lemma testbit_int_XOR:
  "testbit (x XOR y::int) n = (testbit x n ≠ testbit y n)"
by (simp add: testbit_int_def getbit_XOR split: bit.split)

lemma testbit_int_0: "testbit (0::int) n = False"
by (simp add: Pls_def [symmetric] testbit_int_def getbit_Pls) 

lemma testbit_int_1: "testbit (-1::int) n = True"
by (simp add: number_of_is_id testbit_int_def getbit_Min)

lemmas testbit_int_simps =
   testbit_int_NOT testbit_int_AND
   testbit_int_OR testbit_int_XOR
   testbit_int_0 testbit_int_1

lemma testbit_expand_int_eq:
  "((x::int) = y) = (∀n. testbit x n = testbit y n)"
apply (safe intro!: getbit_ext)
apply (drule_tac x="n" in spec)
apply (simp add: testbit_int_def split: bit.splits)
done


subsection {* Axiomatic Class for Bit-Vector Types *}

text {*
The following class includes boolean algebra types where
we can compute bitwise operations on numbers as if they
were integers.
*}

axclass bit_ring ⊆ bit, number_ring
  of_int_NOT: "of_int (NOT a) = NOT (of_int a)"
  of_int_AND: "of_int (a AND b) = of_int a AND of_int b"
  AND_assoc: "(x AND y) AND z = x AND (y AND z)"
  OR_assoc: "(x OR y) OR z = x OR (y OR z)"
  AND_commute: "x AND y = y AND x"
  OR_commute: "x OR y = y OR x"
  AND_OR_distrib: "x AND (y OR z) = (x AND y) OR (x AND z)"
  OR_AND_distrib: "x OR (y AND z) = (x OR y) AND (x OR z)"
  AND_1_right [simp]: "x AND -1 = x"
  OR_0_right [simp]: "x OR 0 = x"
  AND_cancel_right [simp]: "x AND NOT x = 0"
  OR_cancel_right [simp]: "x OR NOT x = -1"
  XOR_def: "x XOR y = x AND NOT y OR NOT x AND y"

instance int :: bit_ring
apply (intro_classes, simp, simp)
apply (auto simp add: testbit_expand_int_eq testbit_int_simps)
done

interpretation bit_ring:
  boolean_xor [bitAND bitOR bitNOT "0::'a::bit_ring" "-1" bitXOR]
by unfold_locales (rule bit_ring_class.axioms)+

lemmas NOT_0 [simp] = bit_ring.compl_zero
lemmas NOT_1 [simp] = bit_ring.compl_one
lemmas AND_0_right [simp] = bit_ring.conj_zero_right
lemmas AND_0_left  [simp] = bit_ring.conj_zero_left
lemmas AND_1_left  [simp] = bit_ring.conj_one_left
lemmas OR_0_left  [simp] = bit_ring.disj_zero_left
lemmas OR_1_right [simp] = bit_ring.disj_one_right
lemmas OR_1_left  [simp] = bit_ring.disj_one_left
lemmas XOR_0_right [simp] = bit_ring.xor_zero_right
lemmas XOR_0_left  [simp] = bit_ring.xor_zero_left
lemmas XOR_1_right [simp] = bit_ring.xor_one_right
lemmas XOR_1_left  [simp] = bit_ring.xor_one_left

lemmas NOT_unique = bit_ring.compl_unique
lemmas double_NOT [simp] = bit_ring.double_compl
lemmas NOT_eq_NOT_iff [iff] = bit_ring.compl_eq_compl_iff

lemmas AND_absorb [simp] = bit_ring.conj_absorb
lemmas AND_left_absorb [simp] = bit_ring.conj_left_absorb
lemmas AND_cancel_left [simp] = bit_ring.conj_cancel_left
lemmas AND_ac = bit_ring.conj_ac
lemmas AND_OR_distrib2 = bit_ring.conj_disj_distrib2
lemmas AND_OR_distribs = bit_ring.conj_disj_distribs
lemmas de_Morgan_AND = bit_ring.de_Morgan_conj

lemmas OR_absorb [simp] = bit_ring.disj_absorb
lemmas OR_left_absorb [simp] = bit_ring.disj_left_absorb
lemmas OR_cancel_left [simp] = bit_ring.disj_cancel_left
lemmas OR_ac = bit_ring.disj_ac
lemmas OR_AND_distrib2 = bit_ring.disj_conj_distrib2
lemmas OR_AND_distribs = bit_ring.disj_conj_distribs
lemmas de_Morgan_OR = bit_ring.de_Morgan_disj

lemmas XOR_def = bit_ring.xor_def
lemmas XOR_def2 = bit_ring.xor_def2
lemmas XOR_cancel_right [simp] = bit_ring.xor_cancel_right
lemmas XOR_cancel_left [simp] = bit_ring.xor_cancel_left
lemmas XOR_NOT_right = bit_ring.xor_compl_right
lemmas XOR_NOT_left = bit_ring.xor_compl_right
lemmas XOR_self [simp] = bit_ring.xor_self
lemmas XOR_left_self [simp] = bit_ring.xor_left_self
lemmas XOR_commute = bit_ring.xor_commute
lemmas XOR_assoc = bit_ring.xor_assoc
lemmas XOR_ac = bit_ring.xor_ac
lemmas AND_XOR_distrib = bit_ring.conj_xor_distrib
lemmas AND_XOR_distrib2 = bit_ring.conj_xor_distrib2
lemmas AND_XOR_distribs = bit_ring.conj_xor_distribs

lemma number_of_NOT:
  "(number_of (NOT a)::'a::bit_ring) = NOT (number_of a)"
by (simp only: number_of_eq of_int_NOT)

lemma number_of_AND:
  "(number_of (a AND b)::'a::bit_ring) = number_of a AND number_of b"
by (simp only: number_of_eq of_int_AND)

lemma number_of_OR:
  "(number_of (a OR b)::'a::bit_ring) = number_of a OR number_of b"
apply (rule NOT_eq_NOT_iff [THEN iffD1])
apply (simp only: de_Morgan_OR
                  number_of_NOT [symmetric]
                  number_of_AND [symmetric])
done

lemma number_of_XOR:
  "(number_of (a XOR b)::'a::bit_ring) = number_of a XOR number_of b"
by (simp add: XOR_def number_of_NOT number_of_AND number_of_OR)

lemmas bitwise_arith_extra_simps [simp] =
  number_of_AND [symmetric]
  number_of_OR [symmetric]
  number_of_NOT [symmetric]
  number_of_XOR [symmetric]

subsection {* Integers modulo powers of 2 *}

lemma ex_power2_eq_number:
  "∃w. (2::int) ^ n = number_of w ∧ ¬ neg (number_of w::int)"
apply (induct n)
apply (rule_tac x="Numeral.Pls BIT bit.B1" in exI, simp)
apply (erule exE, rule_tac x="w BIT bit.B0" in exI, simp)
done

lemma zmod_power2_lemma:
  "(number_of x::int) mod 2 ^ n = number_of x AND (2 ^ n - 1)"
apply (induct n arbitrary: x, simp_all)
apply (cut_tac x="x" in div2_BIT_lsb, erule subst)
apply (cut_tac n="n" in ex_power2_eq_number, erule exE)
apply (simp split: bit.split)
done

lemma zmod_power2: "(x::int) mod 2 ^ n = x AND (2 ^ n - 1)"
by (cut_tac zmod_power2_lemma, simp add: number_of_is_id)

lemma zmod_NOT: "(NOT (x mod 2^n)) mod 2^n = (NOT x::int) mod 2^n"
by (simp add: zmod_power2 de_Morgan_AND AND_OR_distribs)

lemma zmod_AND_left: "((x mod 2^n) AND y) mod 2^n = (x AND y::int) mod 2^n"
by (simp add: zmod_power2 AND_ac)

lemma zmod_AND_right: "(x AND (y mod 2^n)) mod 2^n = (x AND y::int) mod 2^n"
by (simp add: zmod_power2 AND_ac)

lemma zmod_OR_left: "((x mod 2^n) OR y) mod 2^n = (x OR y::int) mod 2^n"
by (simp add: zmod_power2 AND_OR_distribs AND_ac)

lemma zmod_OR_right: "(x OR (y mod 2^n)) mod 2^n = (x OR y::int) mod 2^n"
by (simp add: zmod_power2 AND_OR_distribs AND_ac)

lemmas zmod_bit_simps =
  zmod_NOT zmod_AND_left zmod_AND_right zmod_OR_left zmod_OR_right

end