Theory Digit_Expansions.Binary_Operations

theory Binary_Operations
  imports Bits_Digits Carries
begin

section ‹Digit-wise Operations›

subsection ‹Binary AND›

fun bitAND_nat :: "nat ⇒ nat ⇒ nat" (infix "&&" 64) where
  "0 && _ = 0" |
  "m && n = 2 * ((m div 2) && (n div 2)) + (m mod 2) * (n mod 2)"

lemma bitAND_zero[simp]: "n = 0 ⟹ m && n = 0"
  by (induct m n rule:bitAND_nat.induct, auto)

lemma bitAND_1: "a && 1 = (a mod 2)"
  by (induction a; auto)

lemma bitAND_rec: "m && n = 2 * ((m div 2) && (n div 2)) + (m mod 2) * (n mod 2)"
  by (cases m; simp_all)

lemma bitAND_commutes:"m && n = n && m"
  by (induct m n rule: bitAND_nat.induct, simp) (metis bitAND_rec mult.commute)

lemma nth_digit_0: "x ≤ 1 ⟹ nth_bit x 0 = x" by (simp add: nth_bit_def)

lemma bitAND_zeroone: "a ≤ 1 ⟹ b ≤ 1 ⟹ a && b ≤ 1"
  using nth_bit_def nth_digit_0 nat_le_linear bitAND_nat.elims
  by (metis (no_types, lifting) One_nat_def add.left_neutral bitAND_zero div_less le_zero_eq lessI
             mult.right_neutral mult_0_right not_mod2_eq_Suc_0_eq_0 numeral_2_eq_2)

lemma aux1_bitAND_digit_mult:
  fixes a b c :: nat
  shows "k > 0 ∧ a mod 2 = 0 ∧ b ≤ 1 ⟹ (a + b) div 2^k = a div 2^k"
  by (induction k, auto)
     (metis One_nat_def add_cancel_left_right div_mult2_eq even_succ_div_two le_0_eq le_Suc_eq)

lemma bitAND_digit_mult:"(nth_bit (a && b) k) = (nth_bit a k) * (nth_bit b k)"
proof(induction k arbitrary: a b)
  case 0
  show ?case
    using nth_bit_def
    by auto (metis (no_types, opaque_lifting) Groups.add_ac(2) bitAND_rec mod_mod_trivial
              mod_mult_self2 mult_numeral_1_right mult_zero_right not_mod_2_eq_1_eq_0 numeral_One)
next
  case (Suc k)
  have "nth_bit (a && b) (Suc k)
        = (2 * (a div 2 && b div 2) + a mod 2 * (b mod 2)) div 2 ^(Suc k) mod 2"
    using bitAND_rec by (metis nth_bit_def)

  moreover have "(a mod 2) * (b mod 2) < (2 ^ Suc(k))"
    by (metis One_nat_def lessI mult_numeral_1_right mult_zero_right not_mod_2_eq_1_eq_0
              numeral_2_eq_2 numeral_One power_gt1 zero_less_numeral zero_less_power)

  ultimately have "nth_bit (a && b) (Suc k) = (2 * (a div 2 && b div 2)) div 2 ^(Suc k) mod 2"
    using aux1_bitAND_digit_mult
    by (metis le_numeral_extra(1) le_numeral_extra(4) mod_mult_self1_is_0 mult_numeral_1_right
              mult_zero_right not_mod_2_eq_1_eq_0 numeral_One zero_less_Suc)

  then have "nth_bit (a && b) (Suc k) = (nth_bit (a div 2 && b div 2) k)"
    by (auto simp add: nth_bit_def)

  then have "nth_bit (a && b) (Suc k) = (nth_bit (a div 2) k) * (nth_bit (b div 2) k)"
    using Suc
    by presburger

  then show ?case
    by (metis div_mult2_eq nth_bit_def power_Suc)
qed

lemma bitAND_single_bit_mult_equiv: "a ≤ 1 ⟹ b ≤ 1 ⟹ a * b = a && b"
  using bitAND_digit_mult[of a b 0] bitAND_zeroone by (auto simp: nth_digit_0)

lemma bitAND_mult_equiv:
  "(∀k. (nth_bit c k) = (nth_bit a k) * (nth_bit b k)) ⟷ c = a && b" (is "?P ⟷ ?Q")
proof
  assume "?Q"
  then show "?P" using bitAND_digit_mult by simp
next
  assume "?P"
  then show "?Q" using bitAND_digit_mult digit_wise_equiv by presburger
qed

lemma bitAND_linear:
  fixes k::nat
  shows "(b < 2^k) ∧ (d < 2^k) ⟹ (a * 2^k + b) && (c * 2^k + d) = (a && c) * 2^k + (b && d)"
proof(induction k arbitrary: a b c d)
  case 0
  then show ?case by simp
next
  case (Suc k)
  define m where "m = a * 2^(Suc k) + b"
  define n where "n = c * 2^(Suc k) + d"

  have "m && n = 2 * (bitAND_nat (m div 2) (n div 2)) + (m mod 2) * (n mod 2)"
    using bitAND_rec
    by blast

  moreover have "d mod 2 = n mod 2 ∧ b mod 2 = m mod 2"
    by (metis m_def n_def add.commute mod_mult_self2 power_Suc semiring_normalization_rules(19))

  ultimately have f0:"m && n
                      = 2 * ((a * 2^k + (b div 2)) && (c * 2^k + (d div 2))) + (b mod 2)*(d mod 2)"
    by (metis add.commute div_mult_self2 m_def n_def power_Suc semiring_normalization_rules(19)
              zero_neq_numeral)

  have "b div 2 < (2 ^ k) ∧ d div 2 < (2 ^ k)"
    using Suc.prems
    by auto

  then have f1:"m && n
                = ((a && c) * 2^(Suc k)) + 2 * ((b div 2) && (d div 2)) + (b mod 2) * (d mod 2)"
    using f0 Suc.IH
    by simp

  have "b && d = 2 * ((b div 2) && (d div 2)) + (b mod 2) * (d mod 2)"
    using bitAND_rec
    by blast

  then show ?case
    using f1
    by (auto simp add: m_def n_def)
qed

subsection ‹Binary orthogonality›
text ‹cf. \<^cite>‹h10lecturenotes› section 2.6.1 on "Binary orthogonality"›
text ‹The following definition differs slightly from the one in the paper. However, we later prove the 
     equivalence of the two definitions.›

fun orthogonal :: "nat => nat => bool" (infix "⊥" 49) where
  "(orthogonal a b) = (a && b = 0)"

lemma ortho_mult_equiv: "a ⊥ b ⟷ (∀k. (nth_bit a k) * (nth_bit b k) = 0)" (is "?P ⟷ ?Q")
proof
  assume "?P"
  then show "?Q" using bitAND_digit_mult nth_bit_def by (metis div_0 mod_0 orthogonal.simps)
next
  assume "?Q"
  then show "?P" using bitAND_mult_equiv nth_bit_def by (metis div_0 mod_0 orthogonal.simps)
qed

lemma aux1_1_digit_lt_linear:
  assumes "b < 2^r" "k ≥ r"
  shows  "bin_carry (a*2^r) b k = 0"
proof-
  have "b < 2^r ⟶(a*2^r) ⊥ b"
  proof(induct a  b rule: bitAND_nat.induct)
    case (1 uu)
    then show ?case by simp
  next
    case (2 v n)
    show ?case apply auto using bitAND_linear[of n r 0 0 "Suc(v)"] bitAND_commutes by auto
  qed
  then show ?thesis using ortho_mult_equiv no_carry_mult_equiv assms(1) by auto
qed

lemma aux1_digit_lt_linear:
  assumes "b < 2^r" and "k ≥ r"
  shows "(a*2^r + b) ¡ k = (a*2^r) ¡ k"
proof-
  have "b div 2 ^ k = 0" using assms by (simp add: order.strict_trans2)
  moreover have "(a * 2 ^ r mod 2 ^ k +  b mod 2 ^ k) div 2 ^ k = 0" using assms
  proof-
    have "bin_carry (a*2^r) b k = 0" using assms aux1_1_digit_lt_linear by auto
    then show ?thesis using assms by (auto simp add: bin_carry_def)
  qed
  ultimately show ?thesis
    by (auto simp add: nth_bit_def div_add1_eq[of "a*2^r" "b" "2^k"])
qed

lemma aux_digit_shift: "(a * 2^t) ¡ (l+t) = a ¡ l"
  using nth_bit_def
  by (induct l; auto)
     (smt (verit) div_mult2_eq mult.commute nonzero_mult_div_cancel_right power_add power_not_zero zero_neq_numeral)

lemma aux_digit_lt_linear:
  assumes b: "b < (2::nat)^t"
  assumes d: "d < (2::nat)^t"
  shows "(a * 2^t + b) ¡ k ≤ (c * 2^t + d) ¡ k ⟷ ((a * 2^t) ¡ k ≤ (c * 2^t) ¡ k ∧ b ¡ k ≤ d ¡ k)"
proof (cases "k < t")
  case True
  from True have "(a * 2^t + b) ¡ k = b ¡ k"
    using aux2_digit_sum_repr assms(1) by auto
  moreover from True have "(c * 2^t + d) ¡ k = d ¡ k"
    using aux2_digit_sum_repr assms(2) by auto
  moreover from True have "(a * 2^t) ¡ k = 0"
    using aux2_digit_sum_repr[of "0"] nth_bit_def by auto
  ultimately show ?thesis
    using aux2_digit_sum_repr assms by auto
next
  case False
  from False have "(a * 2^t + b) ¡ k = (a * 2^t) ¡ k"
    using aux1_digit_lt_linear assms(1) by auto
  moreover from False have "(c * 2^t + d) ¡ k = (c * 2^t) ¡ k" using aux1_digit_lt_linear assms(2) by auto
  moreover from False have "b ¡ k = 0"
    using aux1_digit_lt_linear[of _ _ _ "0"] nth_bit_def assms(1) by auto
  ultimately show ?thesis by auto
qed

lemma aux2_digit_lt_linear:
  fixes a b c d t l :: nat
  shows "∃k. (a * 2^t) ¡ k ≤ (c * 2^t) ¡ k ⟶ a ¡ l ≤ c ¡ l"
proof -
  define k where "k = l + t"
  have "(a * 2^t) ¡ k = a ¡ l" using nth_bit_def k_def
    using aux_digit_shift by auto
  moreover have "(c * 2^t) ¡ k = c ¡ l" using nth_bit_def k_def
    using aux_digit_shift by auto
  ultimately show ?thesis by metis
qed

lemma aux3_digit_lt_linear:
  fixes a b c d t k :: nat
  shows "∃l. a ¡ l ≤ c ¡ l ⟶ (a * 2^t) ¡ k ≤ (c * 2^t) ¡ k"
proof (cases "k < t")
  case True
  hence "(a * 2^t) ¡ k = 0"
    using aux2_digit_sum_repr[of "0"] nth_bit_def by auto
  then show ?thesis by auto
next
  case False
  define l where "l = k - t"
  hence k: "k = l + t" using False by auto
  have "(a * 2^t) ¡ k = a ¡ l" using nth_bit_def l_def
    using aux_digit_shift k by auto
  moreover have "(c * 2^t) ¡ k = c ¡ l" using nth_bit_def l_def
    using aux_digit_shift k by auto
  ultimately show ?thesis by auto
qed

lemma digit_lt_linear:
  fixes a b c d t :: nat
  assumes b: "b < (2::nat)^t"
  assumes d: "d < (2::nat)^t"
  shows "(∀k. (a * 2^t + b) ¡ k ≤ (c * 2^t + d) ¡ k) ⟷ (∀l. a ¡ l ≤ c ¡ l ∧ b ¡ l ≤ d ¡ l)"
proof -
  have shift: "(∀k. (a * 2^t) ¡ k ≤ (c * 2^t) ¡ k) ⟷ (∀l. a ¡ l ≤ c ¡ l)" (is "?P ⟷ ?Q")
  proof
    assume P: ?P
    show ?Q using P aux2_digit_lt_linear by auto
  next
    assume Q: ?Q
    show ?P using Q aux3_digit_lt_linear by auto
  qed

  have main: "(∀k. (a * 2^t + b) ¡ k ≤ (c * 2^t + d) ¡ k ⟷ ((a * 2^t) ¡ k ≤ (c * 2^t) ¡ k ∧ b ¡ k ≤ d ¡ k))"
    using aux_digit_lt_linear b d by auto

  from main shift show ?thesis by auto
qed

text ‹Sufficient bitwise (digitwise) condition for the non-strict standard order of natural numbers›

lemma digitwise_leq: 
  assumes "b>1"
  shows "∀t. nth_digit x t b ≤ nth_digit y t b ⟹ x ≤ y"
proof -
  assume asm: "∀t. nth_digit x t b ≤ nth_digit y t b"
  define r where "r ≡(if x>y then x else y)"
  have "x = (∑k<x. (nth_digit x k b) * b ^ k)" 
    using digit_gen_sum_repr_variant ‹b>1› by auto
  hence x: "x = (∑k=0..<r. (nth_digit x k b) * b ^ k)" 
    using atLeast0LessThan r_def digit_gen_sum_index_variant ‹b>1› 
    by (metis (full_types) linorder_neqE_nat)
  have "y = (∑k<y. (nth_digit y k b) * b ^ k)" 
    using digit_gen_sum_repr_variant ‹b>1› by auto
  hence y: "y = (∑k=0..<r. (nth_digit y k b) * b ^ k)"
    using atLeast0LessThan r_def digit_gen_sum_index_variant ‹b>1› by auto
  show ?thesis using asm x y 
    sum_mono[of "{0..<r}" "λk. nth_digit x k b * b^k" "λk. nth_digit y k b * b^k"] 
    by auto
qed

subsection ‹Binary masking›

text ‹Preliminary result on the standard non-strict of natural numbers›

lemma bitwise_leq: "(∀k. a ¡ k ≤  b ¡ k) ⟶ a ≤ b"
  using digitwise_leq[of 2] by (simp add: nth_digit_base2_equiv)

text ‹cf. \<^cite>‹h10lecturenotes› section 2.6.2 on "Binary Masking"›
text ‹Again, the equivalence to the definition there will be proved in a later lemma.›

fun masks :: "nat => nat => bool" (infix "≼" 49) where
  "masks 0 _ = True" |
  "masks a b = ((a div 2 ≼ b div 2) ∧ (a mod 2 ≤ b mod 2))"

lemma masks_substr: "a ≼ b ⟹ (a div (2^k) ≼ b div (2^k))"
proof (induction k)
  case 0
  then show ?case by simp
next
  case (Suc k)
  moreover
  {
    fix ka :: nat
    assume a1: "a div 2 ^ ka ≼ b div 2 ^ ka"

    have f2: "∀n na nb. (nb::nat) div na div n = nb div n div na"
      by (metis (no_types) div_mult2_eq semiring_normalization_rules(7))

    then have f3: "∀n na nb nc.
                    (nc div nb = 0 ∨ nc div 2 div nb ≼ na div 2 div n) ∨ ¬ nc div nb ≼ na div n"
      by (metis (no_types) masks.elims(2))

    {
      assume "∃n. a div n div 2 ^ ka ≠ 0" then have "a div 2 ^ ka ≠ 0" using f2 by (metis div_0)
      then have "a div 2 div 2 ^ ka ≼ b div 2 div 2 ^ ka" using f3 a1 by meson
    }
    then have "a div (2 * 2 ^ ka) ≼ b div (2 * 2 ^ ka)"
      by (metis (no_types) div_mult2_eq masks.simps(1))
  }
  ultimately show ?case by simp
qed

lemma masks_digit_leq:"(a ≼ b) ⟹ (nth_bit a k) ≤ (nth_bit b k)"
proof (induction k arbitrary: a b)
  case 0
  then show ?case
    by (metis add_cancel_left_right bitAND_nat.elims div_by_1 le0 masks.simps(2) power_0
              mod_mult_self1_is_0 mod_mult_self4 nth_bit_def)
next
  case (Suc k)
  then show ?case
    by (simp add: nth_bit_def)
       (metis div_mult2_eq masks_substr nth_bit_def pow.simps(1) power_numeral)
qed

lemma masks_leq_equiv:"(a ≼ b) ⟷ (∀k. (nth_bit a k) ≤ (nth_bit b k))" (is "?P ⟷ ?Q")
proof
  assume "?P"
  then show "?Q" using masks_digit_leq by auto
next
  assume "?Q"
  then show "?P" using nth_bit_def
  proof (induct a b rule: masks.induct)
    case (1 uu)
    then show ?case by simp
  next
    case (2 v b)
    then show ?case by simp (metis drop_bit_Suc drop_bit_eq_div div_by_1 power.simps(1))
  qed
qed

lemma masks_leq:"a ≼ b ⟶ a ≤ b"
  using masks_leq_equiv bitwise_leq by simp

lemma mask_linear:
  fixes a b c d t :: nat
  assumes b: "b < (2::nat)^t"
  assumes d: "d < (2::nat)^t"
  shows "((a * 2^t + b ≼ c * 2^t + d) ⟷ (a ≼ c ∧ b ≼ d))" (is "?P ⟷ ?Q")
proof -
  have "?P ⟷ (∀k. (a * 2^t + b) ¡ k ≤ (c * 2^t + d) ¡ k)" using masks_leq_equiv by auto
  also have "... ⟷ (∀k. a ¡ k ≤ c ¡ k ∧ b ¡ k ≤ d ¡ k)" using b d digit_lt_linear by auto
  also have "... ⟷ a ≼ c ∧ b ≼ d" using masks_leq_equiv by auto
  finally show ?thesis by auto
qed

lemma aux1_lm0241_pow2_up_bound:"(∃(p::nat). (a::nat) < 2^(Suc p))"
  by (induction a) (use less_exp in fastforce)+

lemma aux2_lm0241_single_digit_binom:
  assumes "1 ≥ (a::nat)"
  assumes "1 ≥ (b::nat)"
  shows "¬(a = 1 ∧ b = 1) ⟷ ((a + b) choose b) = 1" (is "?P ⟷ ?Q")
  using assms(1) assms(2)
  by (metis Suc_eq_plus1 add.commute add_cancel_right_left add_eq_if
              binomial_n_0 choose_one le_add2 le_antisym zero_neq_one)

lemma aux3_lm0241_binom_bounds:
  assumes "1 ≥ (m::nat)"
  assumes "1 ≥ (n::nat)"
  shows "1 ≥ m choose n"
  using assms(1) assms(2) le_Suc_eq by auto

lemma aux4_lm0241_prod_one:
  fixes f::"(nat ⇒ nat)"
  assumes "(∀x. (1 ≥ f x))"
  shows "(∏k ≤ n. (f k)) = 1 ⟶ (∀k. k ≤ n ⟶ f k = 1)" (is "?P ⟶ ?Q")
proof(rule ccontr)
  assume assm:"¬(?P ⟶ ?Q)"
  hence f_zero:"∃r. r ≤ n ∧ f r ≠ 1" by simp
  then obtain r where "f r ≠ 1"  and "r ≤ n" by blast
  hence "f r = 0" using assms le_antisym not_less by blast
  hence contr:"(∏k ≤ n. f k) = 0" using ‹r ≤ n› by auto
  then show False using assm contr by simp
qed

lemma aux5_lm0241:
  "(∀i. (nth_bit (a + b) i) choose (nth_bit b i) = 1) ⟶
   ¬(nth_bit a i = 1 ∧ nth_bit b i = 1)"
   (is "?P ⟶ ?Q i")
proof(rule ccontr)
  assume assm:"¬(?P ⟶ ?Q i)"
  hence "(∃i. ¬?Q i)" by blast
  then obtain i where contr:"¬?Q i" and i_minimal:"(∀j < i. ?Q j)" 
    using obtain_smallest[of ‹λi. ¬?Q i›] by auto
  hence "∀j. j < i ⟶ nth_bit a j * nth_bit b j = 0" by (simp add: nth_bit_def)
  hence "∀j. j < i ⟶ ((nth_bit a j = 0 ∧ nth_bit b j = 1) ∨
                            (nth_bit a j = 1 ∧ nth_bit b j = 0) ∨
                            (nth_bit a j = 0 ∧ nth_bit b j = 0))"
      by (auto simp add: nth_bit_def)
  hence "∀j. j < i ⟶ nth_bit a j + nth_bit b j ≤ 1" by auto
  hence "bin_carry a b i = 0"
    using no_carry by (metis contr add_self_mod_2 assm choose_one one_neq_zero)
  hence f0:"nth_bit (a + b) i = (nth_bit a i + nth_bit b i) mod 2"
    by(auto simp add:sum_digit_formula)
  have "... = 0" using contr by auto
  hence "(nth_bit (a + b) i) choose (nth_bit b i) = 0" using f0 contr by auto
  then show False using assm by fastforce
qed

end