Theory Lemma_1_8

theory Lemma_1_8                                 
  imports Lemma_1_8_Coding
begin

subsubsection ‹Proof of the equivalence›

locale Lemma_1_8 = K_Nonnegative +
  assumes ℬ_power2: "is_power2 (int ℬ)"
begin

lemma b_power2: "is_power2 (int b)" 
  using b_def int_ops is_power2_div2 ℬ_power2 ℬ_gt_2
  by (smt (verit) Suc_1 of_nat_less_iff)

(* K lower bound is shown previously in K_Nonnegative *)

lemma K_upper_bound: "K < int ℬ^((2*δ+1) * n ν + 1)"
proof -
  have "j ∈ {..(2*δ+1) * n ν} ⟹ e j + b ≤ ℬ - 1" for j
    using e_b_bound ℬ_ge_1 by (simp add: of_nat_diff) 
  hence 0: "j ∈ {..(2*δ+1) * n ν} ⟹ (e j + b) * ℬ^j ≤ (ℬ - 1) * ℬ^j" for j
    using ℬ_ge_1 by simp

  have 1: "(ℬ - 1) * (∑i≤n. ℬ^i) = ℬ^(n+1) - 1" for n
  proof (induction n)
    case 0 show ?case by simp
  next 
    case (Suc n)
    have "int ((ℬ - 1) * (∑i≤Suc n. ℬ^i)) = 
      int ((ℬ - 1) * (∑i≤n. ℬ^i) + (ℬ - 1) * ℬ^(Suc n))"
      by (auto simp add: algebra_simps)
    also have "... = int ℬ^(Suc n) - (1::int) + (ℬ - (1::int)) * int ℬ^(Suc n)"
      using int_ops Suc.IH ℬ_ge_1 by simp
    also have "... = int ℬ * ℬ^(Suc n) - 1"
      using int_ops by (simp add: algebra_simps)
    also have "... = int (ℬ^(Suc (Suc n)) - 1)"
      using ℬ_ge_1 int_ops by simp
    finally show ?case
      by (metis Suc_eq_plus1 of_nat_eq_iff)
  qed

  have "K ≤ (∑i≤(2*δ+1) * n ν. (ℬ - 1) * int ℬ^i)"
    unfolding K_def using sum_mono 0
    by (metis (no_types, lifting) K_def K_expression of_nat_mult of_nat_power)
  also have "... = int ((ℬ - 1) * (∑i≤(2*δ+1) * n ν. ℬ^i))" 
    by (simp add: sum_distrib_left)
  also have "... = int (ℬ^((2*δ+1) * n ν + 1) - 1)"
    using 1 by simp
  also have "... = ℬ^((2*δ+1) * n ν + 1) - (1::int)"
    using ℬ_ge_1 int_ops(6) by auto
  also have "... < int ℬ^((2*δ+1) * n ν + 1)" by auto
  finally show ?thesis .
qed

lemma direct_implication: 
  "insertion z_assign P = 0 ⟹ τ (nat K) ((b-1) * ℬ^(n (ν+1))) = 0"
proof -
  assume "insertion z_assign P = 0"
  hence assm: "e (n (ν+1)) = 0" using e_n_ν1_expression by simp
   
  define deg where "deg = (2*δ+1) * n ν"
  define x where "x = (λi. nat (e i + int b))"
  define y where "y = (λi. if i = n (ν+1) then b-1 else 0)"

  have x_sum: "nat K = (∑i<deg+1. x i * ℬ^i)"
  proof -
    have 0: "(e i + int b) * ℬ^i ≥ 0" for i
      using e_b_bound(1) by (simp add: dual_order.strict_implies_order)

    have "nat K = nat (∑i≤deg. (e i + int b) * ℬ^i)"
      unfolding K_expression deg_def by auto
    also have "... = (∑i≤deg. nat ((e i + int b) * ℬ^i))"
      using nat_sum_distrib 0 by auto
    also have "... = (∑i≤deg. x i * ℬ^i)"
      unfolding x_def
      by (metis (no_types, opaque_lifting) dual_order.strict_implies_order 
        e_b_bound(1) int_ops(7) nat_0_le nat_int)
    finally show ?thesis
      using Suc_eq_plus1 lessThan_Suc_atMost by presburger
  qed

  have y_sum: "(b-1) * ℬ^(n (ν+1)) = (∑i<deg+1. y i * ℬ^i)"
  proof -
    have 0: "n (ν+1) ≤ deg" unfolding deg_def n_def by auto

    have "(∑i∈{..deg}. y i * ℬ^i) = 
      (∑i∈{..deg} - {n (ν+1)}. y i * ℬ^i) + (∑i∈{n (ν+1)}. y i * ℬ^i)"
      by (meson "0" atMost_iff empty_subsetI finite_atMost insert_subset sum.subset_diff)
    also have "... = (∑i∈{n (ν+1)}. y i * ℬ^i)"
      unfolding y_def by simp
    also have "... = y (n (ν+1)) * ℬ^(n (ν+1))"
      by simp
    also have "... = (b-1) * ℬ^(n (ν+1))"
      unfolding y_def by simp
    finally show ?thesis
      using Suc_eq_plus1 lessThan_Suc_atMost by presburger
  qed

  have digit_cond: "x i + y i < ℬ" for i
  proof cases
    assume "i = n (ν+1)" 
    hence "x i + y i ≤ b + (b - 1)"
      unfolding x_def y_def using assm by auto
    also have "... = ℬ - 1" 
      using b_def_reverse by auto
    also have "... < ℬ" 
      using ℬ_ge_1 by auto
    finally show ?thesis .
  next 
    assume "i ≠ n (ν+1)"
    hence "x i + y i ≤ nat (e i + int b)"
      unfolding x_def y_def by auto
    also have "... < ℬ"
      using e_b_bound by (smt (verit) nat_less_iff)
    finally show ?thesis .
  qed
  
  have τ_digits: "τ (x i) (y i) = 0" for i
  proof cases 
    assume i_def: "i = n (ν+1)" 
    obtain k where "b = 2^k" using b_power2 is_power2_def by auto
    thus ?thesis using assm unfolding x_def y_def i_def
      using nat_int plus_int_code(2) count_carries_pow2_block_ones count_carries_0n by presburger
  next 
    assume "i ≠ n (ν+1)"
    thus ?thesis unfolding y_def by simp
  qed

  obtain k where k_def: "ℬ = 2^k"
    using ℬ_power2 is_power2_def by auto
  have k_ge_1: "1 ≤ k"
    using k_def ℬ_ge_2
    by (metis ℬ_gt_2 antisym linorder_linear one_le_numeral order_less_le 
        power_increasing power_one_right)

  have "τ (nat K) ((b-1) * ℬ^(n (ν+1))) = (∑i<deg+1. τ (x i) (y i))"
    using count_carries_digitwise_no_overflow[OF k_ge_1] digit_cond k_def 
    unfolding x_sum y_sum by blast
  also have "... = 0" 
    using τ_digits by simp
  finally show ?thesis .
qed

 
lemma reverse_implication:
  "τ (nat K) ((b-1) * ℬ^(n (ν+1))) = 0 ⟹ insertion z_assign P = 0"
proof -
  assume assm: "τ (nat K) ((b-1) * ℬ^(n (ν+1))) = 0"
  
  define deg where "deg = (2*δ+1) * n ν"
  define x where "x = (λi. nat (e i + int b))"
  define y where "y = (λi. if i = n (ν+1) then b-1 else 0)"
  
  have x_sum: "nat K = (∑i<deg+1. x i * ℬ^i)"
  proof -
    have 0: "(e i + int b) * ℬ^i ≥ 0" for i
      using e_b_bound(1) by (simp add: dual_order.strict_implies_order)

    have "nat K = nat (∑i≤deg. (e i + int b) * ℬ^i)"
      unfolding K_expression deg_def by auto
    also have "... = (∑i≤deg. nat ((e i + int b) * ℬ^i))"
      using nat_sum_distrib 0 by auto
    also have "... = (∑i≤deg. x i * ℬ^i)"
      unfolding x_def
      by (metis (no_types, opaque_lifting) dual_order.strict_implies_order 
        e_b_bound(1) int_ops(7) nat_0_le nat_int)
    finally show ?thesis
      using Suc_eq_plus1 lessThan_Suc_atMost by presburger
  qed

  have y_sum: "(b-1) * ℬ^(n (ν+1)) = (∑i<deg+1. y i * ℬ^i)"
  proof -
    have 0: "n (ν+1) ≤ deg" unfolding deg_def n_def by auto

    have "(∑i∈{..deg}. y i * ℬ^i) = 
      (∑i∈{..deg} - {n (ν+1)}. y i * ℬ^i) + (∑i∈{n (ν+1)}. y i * ℬ^i)"
      by (meson "0" atMost_iff empty_subsetI finite_atMost insert_subset sum.subset_diff)
    also have "... = (∑i∈{n (ν+1)}. y i * ℬ^i)"
      unfolding y_def by simp
    also have "... = y (n (ν+1)) * ℬ^(n (ν+1))"
      by simp
    also have "... = (b-1) * ℬ^(n (ν+1))"
      unfolding y_def by simp
    finally show ?thesis
      using Suc_eq_plus1 lessThan_Suc_atMost by presburger
  qed

  have xy_bound: "x i < ℬ ∧ y i < ℬ" for i
    unfolding x_def y_def using e_b_bound b_def
    by (smt (verit, best) ℬ_ge_1 div_less_dividend less_imp_diff_less less_numeral_extra(1) 
        nat_less_iff one_less_numeral_iff order_less_le_trans semiring_norm(76))

  obtain k where k_def: "ℬ = 2^k"
    using ℬ_power2 is_power2_def by auto
  have k_ge_1: "1 ≤ k"
    using k_def ℬ_ge_2
    by (metis ℬ_gt_2 antisym linorder_linear one_le_numeral order_less_le 
        power_increasing power_one_right)

  have "n (ν+1) < deg+1"
    unfolding deg_def n_def by auto
  hence "τ (x (n (ν+1))) (y (n (ν+1))) ≤ τ (∑i<deg+1. x i * ℬ^i) (∑i<deg+1. y i * ℬ^i)"
    using count_carries_digitwise_specific[OF k_ge_1] xy_bound 
    unfolding k_def by meson
  hence "τ (x (n (ν+1))) (y (n (ν+1))) = 0"
    using x_sum y_sum assm by auto
  hence "τ (b-1) (nat (e (n (ν+1)) + int b)) = 0"
    using x_def y_def n_def deg_def count_carries_sym by simp
  hence "b dvd nat (e (n (ν+1)) + int b)"
    using count_carries_divisibility_pow2 b_power2 unfolding is_power2_def by force
  hence "(int b) dvd (e (n (ν+1)) + int b)"
    by (metis dual_order.strict_iff_not e_b_bound(1) nat_0_le of_nat_dvd_iff)
  hence b_dvd_e: "b dvd e (n (ν+1))"
    by auto
  hence "e (n (ν+1)) = 0"
  proof cases
    assume "e (n (ν+1)) = 0" thus ?thesis .
  next 
    assume "e (n (ν+1)) ≠ 0"
    hence "b ≤ abs (e (n (ν+1)))"
      using b_dvd_e by (simp add: zdvd_imp_le) 
    hence "ℬ ≤ 2 * abs (e (n (ν+1)))"
      using b_def_reverse by auto
    hence "fact δ * (nat L) * (1 + sum_list z)^δ < abs (e (n (ν+1)))"
      using ℬ_lower_bound by linarith
    thus ?thesis
      using e_upper_bound L_pos dual_order.strict_iff_not
      by fastforce
  qed
  thus ?thesis using e_n_ν1_expression by auto
qed

lemma tau_rewrite: 
  "τ (2 * nat K) ((ℬ-2) * ℬ^(n (ν+1))) = τ (nat K) ((b-1) * ℬ^(n (ν+1)))"
  using count_carries_even_even b_def_reverse
  by (smt (verit, best) ab_semigroup_mult_class.mult_ac(1) mult_numeral_1_right numerals(1) 
      right_diff_distrib')
 
lemma lemma_1_8: 
  shows "insertion z_assign P = 0 ⟷ τ (2 * nat K) ((ℬ-2) * ℬ^(n (ν+1))) = 0"
    and "K > int ℬ^((2*δ+1) * n ν)" 
    and "K < int ℬ^((2*δ+1) * n ν + 1)"
  using K_lower_bound K_upper_bound direct_implication reverse_implication n_def tau_rewrite
  by simp_all blast

end

end