Theory Digit_Expansions.Carries

theory Carries
  imports Bits_Digits
begin

section ‹Carries in base-b expansions›

text ‹Some auxiliary lemmas›
lemma rev_induct[consumes 1, case_names base step]:
  fixes i k :: nat
  assumes le: "i  k"
    and base: "P k"
    and step: "i. i  k  P i  P (i - 1)"
  shows "P i"
proof -
  have "i::nat. n = k-i  i  k  P i" for n
  proof (induct n)
    case 0
    then have "i = k" by arith
    with base show "P i" by simp
  next
    case (Suc n)
    then have "n = (k - (i + 1))" by arith
    moreover have k: "i + 1  k" using Suc.prems by arith
    ultimately have "P (i + 1)" by (rule Suc.hyps)
    from step[OF k this] show ?case by simp
  qed
  with le show ?thesis by fast
qed

subsection ‹Definition of carry received at position k›
text ‹When adding two numbers m and n, the carry is \emph{introduced}
      at position 1 but is \emph{received} at position 2. The function below
      accounts for the latter case. 

\begin{center} \begin{verbatim}
        k: 6 5 4 3 2 1 0
        c:         1
   - - - - - - - - - - - -
        m:   1 0 1 0 1 0
        n:           1 1
    ----------------------
    m + n: 0 1 0 1 1 0 0
\end{verbatim} \end{center} ›

definition bin_carry :: "nat  nat  nat  nat" where
  "bin_carry a b k = (a mod 2^k + b mod 2^k) div 2^k"

text ‹Carry in the subtraction of two natural numbers›

definition bin_narry :: "nat  nat  nat  nat" where
  "bin_narry a b k = (if b mod 2^k > a mod 2^k then 1 else 0)"

text ‹Equivalent definition›
definition bin_narry2 :: "nat  nat  nat  nat" where
  "bin_narry2 a b k = ((2^k + a mod 2^k - b mod 2^k) div 2^k + 1) mod 2"

lemma bin_narry_equiv: "bin_narry a b c = bin_narry2 a b c"
  apply (auto simp add: bin_narry_def bin_narry2_def)
  subgoal by (smt (verit) add.commute div_less dvd_0_right even_Suc le_add_diff_inverse2 less_add_eq_less 
        mod_greater_zero_iff_not_dvd neq0_conv not_mod2_eq_Suc_0_eq_0 order_le_less zero_less_diff 
        zero_less_numeral zero_less_power)
  subgoal by (simp add: le_div_geq less_imp_diff_less)
  done

subsection ‹Properties of carries›

lemma div_sub:
  fixes a b c :: nat
  shows "(a - b) div c = (if(a mod c < b mod c) then a div c - b div c - 1 else  a div c - b div c)"
proof-
  consider (alb) "a<b" | (ageb) "ab" by linarith
  then show ?thesis
  proof cases
    case alb
    then show ?thesis using div_le_mono by auto
  next
    case ageb
    obtain a1 a2 where a1_def: "a1 = a div c" and a2_def: "a2 = a mod c" and a_def: "a=a1*c+a2" 
      using mod_div_decomp by blast
    obtain b1 b2 where b1_def: "b1 = b div c" and b2_def: "b2 = b mod c" and b_def: "b=b1*c+b2" 
      using mod_div_decomp by blast
    have a1geb1: "a1b1" using ageb a1_def b1_def using div_le_mono by blast
    show ?thesis
    proof(cases "c=0")
      assume "c=0"
      then show ?thesis by simp
    next
      assume cneq0: "c  0"
      then show ?thesis
      proof(cases "a2 < b2")
        assume a2lb2: "a2 < b2"
        then show ?thesis 
        proof(cases "a1=b1")
          case True
          then show ?thesis using ageb a2lb2 a_def b_def by force 
        next
          assume "¬(a1=b1)"
          hence a1gb1: "a1>b1" using a1geb1 by auto
          have boundc: "a2+c-b2<c" using a2lb2 cneq0 by linarith
          have "a-b = (a1 - b1) * c + a2 - b2"
            using a_def b_def a1geb1 nat_diff_add_eq1[of b1 a1 c a2 b2] by auto
          also have "... = (a1 - b1-1+1) * c + a2 - b2"
            using a1gb1 Suc_diff_Suc[of b1 a1] by auto
          also have "... = (a1 - b1 - 1) * c + (a2 + c - b2)" 
            using div_eq_0_iff[of b2 c] mod_div_trivial[of b c] b2_def by force
          finally have "(a-b) div c = a1 - b1 - 1 + (a2 + c - b2) div c"
            using a_def b_def cneq0 by auto
          then show ?thesis 
            using boundc div_less by (simp add: a1_def a2_def b1_def b2_def)
        qed
      next
        assume a2geb2: "¬ a2 < b2"
        then have "(a - b) div c = ((a1 - b1) * c + (a2 - b2)) div c" 
          using a1geb1 a_def b_def nat_diff_add_eq1 by auto
        then show ?thesis using a2geb2 div_add1_eq[of "(a1-b1)*c" "a2-b2" c]
          by(auto simp add: b2_def a2_def a1_def b1_def less_imp_diff_less)
      qed
    qed
  qed
qed

lemma dif_digit_formula:"a  b  (a - b)¡k = (a¡k + b¡k + bin_narry a b k) mod 2"
proof -
  {
    presume asm: "ab" "a mod 2 ^ k < b mod 2 ^ k"
    then have "Suc((a - b) div 2 ^ k) = a div 2 ^ k - b div 2 ^ k"
      by (smt (verit) Nat.add_diff_assoc One_nat_def Suc_pred add.commute diff_is_0_eq div_add_self1 
          div_le_mono div_sub mod_add_self1 nat_le_linear neq0_conv plus_1_eq_Suc power_not_zero 
          zero_neq_numeral) 
    then have "(a - b) div 2 ^ k mod 2 = Suc (a div 2 ^ k mod 2 + b div 2 ^ k mod 2) mod 2"
      by (smt (verit) diff_is_0_eq even_Suc even_diff_nat even_iff_mod_2_eq_zero le_less mod_add_eq 
          nat.simps(3) not_mod_2_eq_1_eq_0)
  }
  moreover
  {
    presume asm2: "¬ a mod 2 ^ k < b mod 2 ^ k" "b  a"
    then have "(a - b) div 2 ^ k mod 2 = (a div 2 ^ k mod 2 + b div 2 ^ k mod 2) mod 2"
      using div_sub[of b "2^k" a] div_le_mono even_add even_iff_mod_2_eq_zero 
        le_add_diff_inverse2[of "b div 2 ^ k" "a div 2 ^ k"] mod_mod_trivial[of _ 2] 
        not_less[of "a mod 2 ^ k" "b mod 2 ^ k"] not_mod_2_eq_1_eq_0 div_sub by (smt (verit))
  }
  ultimately show ?thesis
    by (auto simp add: bin_narry_def nth_bit_def) 
qed


lemma dif_narry_formula: 
  "ab  bin_narry a b (k + 1) = (if (a¡k < b¡k + bin_narry a b k) then 1 else 0)"
proof -
  {
    presume a1: "a mod (2 * 2 ^ k) < b mod (2 * 2 ^ k)"
    presume a2: "¬ a div 2 ^ k mod 2 < Suc (b div 2 ^ k mod 2)"
    have f3: "2 ^ k  (0::nat)"
      by simp
    have f4: "a div 2 ^ k mod 2 = 1"
      using a2 by (meson le_less_trans mod2_eq_if mod_greater_zero_iff_not_dvd not_less 
          zero_less_Suc)
    then have "b mod (2 * 2 ^ k) = b mod 2 ^ k"
      using a2 by (metis (no_types) One_nat_def le_simps(3) mod_less_divisor mod_mult2_eq 
          mult.left_neutral neq0_conv not_less semiring_normalization_rules(7))
    then have "False"
      using f4 f3 a1 by (metis One_nat_def add.commute div_add_self1 div_le_mono less_imp_le 
          mod_div_trivial mod_mult2_eq mult.left_neutral not_less plus_1_eq_Suc 
          semiring_normalization_rules(7) zero_less_Suc)
  }
  moreover
  {
    presume a1: "¬ a mod 2 ^ k < b mod 2 ^ k"
    presume a2: "a mod (2 * 2 ^ k) < b mod (2 * 2 ^ k)"
    presume a3: "¬ a div 2 ^ k mod 2 < b div 2 ^ k mod 2"
    presume a4: "b  a"
    have f6: "a mod 2 ^ Suc k < b mod 2 ^ Suc k"
    using a2 by simp
    obtain nn :: "nat  nat  nat" where f7: "b + nn a b = a" using a4 le_add_diff_inverse by auto
    have "(a div 2 ^ k - b div 2 ^ k) div 2 = a div 2 ^ k div 2 - b div 2 ^ k div 2"
    using a3 div_sub by presburger
      then have f8: "(a - b) div 2 ^ Suc k = a div 2 ^ Suc k - b div 2 ^ Suc k"
        using a1 by (metis (no_types) div_mult2_eq div_sub power_Suc power_commutes)
      have f9: "n na. Suc (na div n) = (n + na) div n  0 = n"
        by (metis (no_types) add_Suc_right add_cancel_left_right div_add_self1 lessI 
            less_Suc_eq_0_disj less_one zero_neq_one)
      then have "n na nb. (na + nb - n) div na = Suc (nb div na) - n div na - 1 
         ¬ (na + nb) mod na < n mod na  0 = na" by (metis (no_types) div_sub)
      then have f10: "n na nb. ¬ (nb::nat) mod na < n mod na  nb div na - n div na 
          = (na + nb - n) div na  0 = na"
        by (metis (no_types) diff_Suc_Suc diff_commute diff_diff_left mod_add_self1 plus_1_eq_Suc)
      have "n. Suc n  n" by linarith
    then have "(0::nat) = 2 ^ Suc k"
      using f10 f9 f8 f7 f6 a4 by (metis add_diff_cancel_left' add_diff_assoc)
    then have "False"
      by simp
  }

  ultimately show ?thesis
    apply (auto simp add: nth_bit_def not_less bin_narry_def)
    subgoal by (smt (verit) add_0_left add_less_cancel_left Divides.divmod_digit_0(2) le_less_trans mod_less_divisor
        mod_mult2_eq mult_zero_right nat_neq_iff not_less not_mod2_eq_Suc_0_eq_0 
        semiring_normalization_rules(7) zero_less_numeral zero_less_power)
    subgoal by (smt (verit) One_nat_def add.left_neutral Divides.divmod_digit_0(1) le_less_trans less_imp_le
          mod_less_divisor mod_mult2_eq mod_mult_self1_is_0 mult_zero_right not_less
          not_mod2_eq_Suc_0_eq_0 not_one_le_zero semiring_normalization_rules(7) zero_less_numeral 
          zero_less_power)
    done
qed
 
lemma sum_digit_formula:"(a + b)¡k =(a¡k + b¡k + bin_carry a b k) mod 2"
  by (simp add: bin_carry_def nth_bit_def) (metis div_add1_eq mod_add_eq)

lemma sum_carry_formula:"bin_carry a b (k + 1) =(a¡k + b¡k + bin_carry a b k) div 2"
  by (simp add: bin_carry_def nth_bit_def)
     (smt (verit) div_mult2_eq div_mult_self4 mod_mult2_eq power_not_zero semiring_normalization_rules(20)
          semiring_normalization_rules(34) semiring_normalization_rules(7) zero_neq_numeral)

lemma bin_carry_bounded:
  shows "bin_carry a b k = bin_carry a b k mod 2"
proof-
  have "a mod 2 ^ k <  2 ^k" by simp
  moreover have "b mod 2 ^ k < 2 ^ k" by simp
  ultimately have "(a mod 2 ^ k + b mod 2 ^ k) <  2 ^(Suc k)" by (simp add: mult_2 add_strict_mono)
  then have "(a mod 2 ^ k + b mod 2 ^ k) div 2^k   1" using less_mult_imp_div_less by force
  then have "bin_carry a b k  1" using div_le_mono bin_carry_def by fastforce
  then show ?thesis by auto
qed

lemma carry_bounded: "bin_carry a b k  1"
  using bin_carry_bounded not_mod_2_eq_1_eq_0[of "bin_carry a b k"] by auto

lemma no_carry:
  "(r< n.((nth_bit a r) + (nth_bit b r)  1)) 
          (nth_bit (a + b) n) = (nth_bit a n + nth_bit b n) mod 2"
  (is "?P  ?Q n")
proof (rule ccontr)
  assume p: "?P"
  assume nq: "¬?Q n"
  then obtain k where k1:"¬?Q k" and k2:"r<k. ?Q r" by (auto dest: obtain_smallest)

  have c1: "bin_carry a b k = 1"
    using k1 sum_digit_formula bin_carry_bounded
    by auto (metis add.commute not_mod2_eq_Suc_0_eq_0 plus_nat.add_0)

  have c0: "bin_carry a b (k-1) = 0" using sum_digit_formula
    by (metis bin_carry_bounded bin_carry_def diff_is_0_eq' diff_less div_by_1 even_add
              even_iff_mod_2_eq_zero k2 less_numeral_extra(1) mod_by_1 neq0_conv nth_bit_bounded
              power_0)

  with c1 have "a ¡ (k-1) + b ¡ (k-1) < 1"
    by (smt (verit, ccfv_threshold) Suc_leI add.commute add.left_commute add_0 add_cancel_right_left add_diff_cancel_left' add_diff_cancel_right' add_diff_inverse_nat add_lessD1 add_mono_thms_linordered_field(4) bin_carry_bounded bot_nat_0.not_eq_extremum choose_two diff_add_zero diff_diff_left diff_le_self div_add1_eq dual_order.refl gr0_conv_Suc k2 le_add1 le_antisym le_neq_implies_less lessI less_diff_conv less_diff_conv2 less_eq_iff_succ_less less_imp_add_positive less_imp_diff_less less_nat_zero_code less_one linorder_not_less mult.commute mult_1 nat.simps(3) nat_add_left_cancel_less nat_arith.rule0 nat_diff_split nonzero_mult_div_cancel_left not_add_less1 not_add_less2 nq one_add_one order_le_less_trans order_less_irrefl order_less_le_trans p sum_carry_formula trans_less_add1 zero_diff zero_less_Suc zero_less_diff zero_neq_one)

  with c0 have "0 = bin_carry a b k" using k2 sum_carry_formula
    by auto (metis Suc_eq_plus1_left add_diff_inverse_nat less_imp_diff_less mod_0 mod_Suc
              mod_add_self1 mod_div_trivial mod_less n_not_Suc_n plus_nat.add_0)

  then show False using c1 by auto
qed

lemma no_carry_mult_equiv:"(k. nth_bit a k * nth_bit b k = 0)  (k. bin_carry a b k = 0)"
  (is "?P  ?Q")
proof
  assume P: ?P 
  {
    fix k
    from P have "bin_carry a b k = 0"
    proof (induction k)
      case 0
      then show ?case using bin_carry_def by (simp)
    next
      case (Suc k)
      then show ?case using sum_carry_formula P
        by (metis One_nat_def Suc_eq_plus1 add.right_neutral div_less lessI
        mult_is_0 not_mod_2_eq_0_eq_1 nth_bit_def numeral_2_eq_2 zero_less_Suc)
    qed
  }
  then show ?Q by auto
next
  assume Q: ?Q
  {
    fix k
    from Q have "a ¡ k * b ¡ k = 0"
    proof (induction k)
      case 0
      then show ?case using bin_carry_def nth_bit_def
        by simp (metis add_self_div_2 not_mod2_eq_Suc_0_eq_0 power_one_right)
    next
      case (Suc k)
      then show ?case
        using nth_bit_def  sum_carry_formula
        by simp (metis One_nat_def add.right_neutral add_self_div_2 not_mod_2_eq_1_eq_0 power_Suc)+
    qed
  }
  then show ?P by auto 
qed


(* NEW LEMMAS FROM DIGIT COMPARISON *)

lemma carry_digit_impl: "bin_carry a b k  0  r<k. a ¡ r + b ¡ r = 2"
proof(rule ccontr)
  assume "¬ (r<k. a ¡ r + b ¡ r = 2)"
  hence bound: "r<k. a ¡ r + b ¡ r  1" using nth_bit_def by auto
  assume bk:"bin_carry a b k  0"
  hence base: "bin_carry a b k = 1" using carry_bounded le_less[of "bin_carry a b k" 1] by auto
  have step: "i  k  bin_carry a b i = 1  bin_carry a b (i - 1) = 1" for i
    proof(rule ccontr)
      assume ik: "i  k"
      assume carry: "bin_carry a b i = 1"
      assume "bin_carry a b (i- 1)  1"
      hence "bin_carry a b (i - 1) = 0" using bin_carry_bounded not_mod_2_eq_1_eq_0[of "bin_carry a b (i - 1)"] by auto
      then show False using ik carry bound sum_carry_formula[of a b "i-1"] 
        apply simp
        by (metis Suc_eq_plus1 Suc_pred add_lessD1 bot_nat_0.not_eq_extremum carry diff_is_0_eq' div_le_mono le_eq_less_or_eq less_add_one one_div_two_eq_zero)
    qed 
  have "ik. bin_carry a b i = 1" using rev_induct[where ?P="λc.(bin_carry a b c = 1)"] step base by blast
  moreover have "bin_carry a b 0 = 0" using bin_carry_def by simp
  ultimately show False by auto
qed


end