Theory Coding_Theorem
theory Coding_Theorem
imports Coding_Theorem_Definitions "../Coding/Tau_Reduction" "../Coding/Masking"
"../Coding/Lemma_1_8"
begin
lemma digit_sum_bound_int:
fixes f::"nat ⇒ int"
assumes "1 < b" and "∀i∈{0..q}. f i < b"
shows "(∑i=0..q. f i * b^i) < b^(Suc q)"
using assms(2)
proof (induct q)
case 0 thus ?case by simp
next
case (Suc q)
have "(∑i=0..Suc q. f i * b^i) = (∑i=0..q. f i * b^i) + f (Suc q) * b^(Suc q)"
by simp
also have "... < b^(Suc q) + f (Suc q) * b^(Suc q)"
using Suc by auto
also have "... ≤ b^(Suc q) + (b-1) * b^(Suc q)"
using Suc.prems assms(1) by auto
also have "... = b^(Suc (Suc q))"
by (metis add.commute add_diff_eq cancel_comm_monoid_add_class.diff_cancel group_cancel.rule0
int_distrib(1) lambda_one power_Suc)
finally show ?case .
qed
subsection ‹Proof›
locale coding_theorem = coding_variables +
assumes a_nonneg: "a ≥ 0"
and f_pos: "f > 0"
and b_power2: "is_power2 b"
and δ_pos: "δ > 0"
begin
text ‹b being a power of 2 implies that the following are also powers of 2: ›
lemma ℬ_power2: "is_power2 ℬ"
unfolding ℬ_def β_def using b_power2 by simp
lemma N0_power2: "is_power2 N0"
unfolding N0_def using ℬ_power2 by simp
lemma N1_power2: "is_power2 N1"
unfolding N1_def using ℬ_power2 by simp
lemma N_power2: "is_power2 N"
unfolding N_def using N0_power2 N1_power2 by simp
lemma Ng_power2: "is_power2 N"
by (simp add: N_power2)
lemma ℬ_ge_2: "ℬ ≥ 2"
unfolding ℬ_def β_def using r_pos[OF δ_pos] is_power2_ge1[OF b_power2] apply simp
by (smt (verit, best) mult_pos_pos one_le_power pos_zmult_eq_1_iff self_le_power)
lemma ℬ_even: "2 dvd ℬ"
using ℬ_power2 unfolding is_power2_def using ℬ_ge_2
by (metis Suc_eq_plus1 dvd_refl even_power mult_cancel_left1 not_gr_zero numeral_le_iff
numerals(1) of_nat_1 of_nat_numeral plus_nat.add_0 power.simps(2) power_one_right
semiring_norm(69) zero_neq_numeral)
lemma b_le_ℬ: "b ≤ ℬ"
unfolding ℬ_def β_def apply simp
using δ_pos is_power2_ge1[OF b_power2]
by (smt (verit) mult_le_cancel_right1 self_le_power zero_less_power)
lemma M_bound: "0 ≤ M ∧ M < N0"
proof
show "0 ≤ M"
proof -
have "m i ≥ 0" for i
unfolding m_def using b_le_ℬ is_power2_ge1[OF ℬ_power2] by simp
hence "m i * ℬ^i ≥ 0" for i
using is_power2_ge1[OF ℬ_power2] by simp
thus ?thesis
unfolding M_def by (meson sum_nonneg)
qed
show "M < N0"
proof -
have "m i < ℬ" for i
unfolding m_def using is_power2_ge1[OF b_power2] by simp
thus ?thesis
unfolding M_def N0_def n_def using digit_sum_bound_int ℬ_ge_2 by simp
qed
qed
context
fixes g::int
assumes g_lower_bound: "0 ≤ g"
and g_upper_bound: "g < 2 * b * ℬ^(n ν)"
begin
lemma g_lt_N0: "g < N0"
proof -
have "g < 2 * b * ℬ^(n ν)"
using g_upper_bound by simp
also have "... ≤ ℬ * ℬ^(n ν)"
proof -
have "2 ≤ β"
by (metis β_def add_leE numeral_Bit0 one_le_numeral r_pos[OF δ_pos] self_le_power)
hence "2 * b ≤ ℬ"
unfolding ℬ_def using is_power2_ge1[OF b_power2] δ_pos
by (metis int_nat_eq int_one_le_iff_zero_less less_irrefl_nat mult_mono' of_nat_0_le_iff
of_nat_le_iff of_nat_numeral self_le_power zless_nat_eq_int_zless)
thus ?thesis
using is_power2_ge1[OF ℬ_power2] by simp
qed
also have "... = N0"
unfolding N0_def n_def
using power_add N0_def by simp
finally show ?thesis .
qed
lemma c_bound: "abs (c g) < 3 * b * ℬ^(n ν)"
proof -
have "a ≤ 6*a+3"
using a_nonneg by auto
also have "... ≤ (6*a+3) * f"
using f_pos a_nonneg by auto
finally have 0: "1 + a ≤ b"
unfolding b_def by simp
have "abs (c g) = abs (1 + a * ℬ + g)"
using c_def by simp
also have "... = 1 + a * ℬ + g"
using is_power2_ge1[OF ℬ_power2] g_lower_bound a_nonneg by auto
also have "... ≤ (1 + a) * ℬ + g"
using is_power2_ge1[OF ℬ_power2]
by (smt (verit, ccfv_SIG) mult_right_cancel mult_right_mono)
also have "... ≤ b * ℬ + g"
by (smt (verit, best) 0 ℬ_power2 is_power2_ge1 mult_right_mono)
also have "... ≤ b * ℬ^(n ν) + g"
unfolding n_def using is_power2_ge1 ℬ_power2 "0" a_nonneg self_le_power
by fastforce
finally show ?thesis
using g_upper_bound by auto
qed
lemma D_bound: "abs D ≤ fact δ * ℒ * ℬ^(n (ν+1))"
proof -
have 0: "i∈δ_tuples ⟹ D_precoeff i ≤ int (fact δ)" for i
unfolding D_precoeff_def δ_tuples_def using mchoose_le of_nat_mono by fastforce
have "D_exponent i ≤ n (ν+1)" for i
unfolding D_exponent_def by simp
hence 1: "ℬ^(D_exponent i) ≤ ℬ^(n (ν+1))" for i
using is_power2_ge1[OF ℬ_power2] power_increasing by blast
have "abs D ≤ (∑i∈δ_tuples. abs (D_precoeff i * P_coeff i * ℬ^(D_exponent i)))"
using D_def δ_tuples_finite by simp
also have "... = (∑i∈δ_tuples. abs (D_precoeff i) * abs (P_coeff i) * (abs ℬ)^(D_exponent i))"
using abs_mult by (metis (no_types, opaque_lifting) power_abs)
also have "... = (∑i∈δ_tuples. D_precoeff i * abs (P_coeff i) * ℬ^(D_exponent i))"
using is_power2_ge1[OF ℬ_power2] D_precoeff_def by auto
also have "... ≤ (∑i∈δ_tuples. fact δ * abs (P_coeff i) * ℬ^(n (ν+1)))"
proof -
{ fix i assume assm: "i∈δ_tuples"
have "0 ≤ ℬ^(D_exponent i)"
using is_power2_ge1[OF ℬ_power2] by auto
moreover have "0 ≤ D_precoeff i"
using D_precoeff_def by auto
ultimately have "D_precoeff i * abs (P_coeff i) * ℬ^(D_exponent i) ≤
fact δ * abs (P_coeff i) * ℬ^(n (ν+1))"
using "0"[OF assm] 1 by (simp add: mult_mono') }
thus ?thesis
using sum_mono by meson
qed
also have "... = fact δ * (∑i∈δ_tuples. abs (P_coeff i)) * ℬ^(n (ν+1))"
using sum_distrib_left sum_distrib_right by metis
finally show ?thesis
unfolding ℒ_def by simp
qed
lemma c_δ_D_bound: "2 * abs ((c g)^δ * D) ≤ ℬ^((2*δ+1)*n ν + 1)"
proof -
have 0: "β > int (2 * fact δ * ℒ * 3^δ)"
proof -
have "3^δ ≤ (ν+3)^δ"
by (simp add: power_mono)
thus ?thesis
using β_lower_bound
by (smt (verit, best) nat_less_as_int nat_mult_less_cancel_disj not_less)
qed
have "2 * abs ((c g)^δ * D) = 2 * (abs (c g))^δ * abs D"
by (simp add: abs_mult power_abs)
also have "... ≤ 2 * (3 * b * ℬ^(n ν))^δ * (fact δ * ℒ * ℬ^(n (ν+1)))"
using D_bound c_bound by (simp add: δ_pos mult_mono)
also have "... = 2 * (3^δ * b^δ * ℬ^(n ν * δ)) * (fact δ * ℒ * ℬ^(n (ν+1)))"
using power_mult power_mult_distrib by (metis (no_types, opaque_lifting))
also have "... = (2 * fact δ * ℒ * 3^δ) * (b^δ * ℬ^((2*δ+1) * n ν))"
proof -
have "X^(n ν * δ) * X^(n (ν+1)) = X^((2*δ+1) * n ν)" for X::int
using power_add n_def
by (smt (verit) add_mult_distrib2 left_add_twice mult.commute power_one_right)
thus ?thesis
by simp
qed
also have "... ≤ β * (b^δ * ℬ^((2*δ+1) * n ν))"
using 0 is_power2_ge1 b_power2 ℬ_power2
by (smt (verit, del_insts) mult_le_0_iff mult_right_mono zero_less_power)
also have "... = ℬ * ℬ^((2*δ+1) * n ν)"
using ℬ_def by simp
finally show ?thesis
using power_add by simp
qed
lemma K_bound: "0 ≤ K g ∧ 2 * K g < 3 * ℬ^((2*δ+1)*n ν + 1)"
proof
define K2 :: int where "K2 ≡ (∑i=0..(2*δ+1)*n ν. of_nat (β div 2) * b^δ * ℬ^i)"
have K_def_alt: "K g = (c g)^δ * D + K2"
using K2_def K_def by simp
have K2_def_alt: "K2 = (∑i=0..(2*δ+1)*n ν. (ℬ div 2) * ℬ^i)"
proof -
have "K2 = (∑i=0..(2*δ+1)*n ν. (β div 2) * b^δ * ℬ^i)"
using K2_def by simp
also have "... = (∑i=0..(2*δ+1)*n ν. (ℬ div 2) * ℬ^i)"
proof -
have "2 dvd β"
unfolding β_def using r_pos[OF δ_pos] by simp
hence "(β div 2) * b^δ = ℬ div 2"
by (simp add: ℬ_def dvd_div_mult zdiv_int)
thus ?thesis
using sum.cong by auto
qed
finally show ?thesis .
qed
have K2_bound: "ℬ^((2*δ+1) * n ν + 1) ≤ 2 * K2 ∧ K2 < ℬ^((2*δ+1) * n ν + 1)"
proof
have "K2 = (∑i=0..<(2*δ+1)*n ν. (ℬ div 2) * ℬ^i) + (ℬ div 2) * ℬ^((2*δ+1) * n ν)"
unfolding K2_def_alt using n_def
by (smt (verit) atLeastLessThanSuc_atLeastAtMost sum.atLeast0_lessThan_Suc)
also have "... ≥ (ℬ div 2) * ℬ^((2*δ+1) * n ν)"
proof -
have "(ℬ div 2) * ℬ^i ≥ 0" for i
using is_power2_ge1[OF ℬ_power2] by auto
thus ?thesis
using sum_nonneg by (smt (verit, ccfv_threshold))
qed
finally have "2 * K2 ≥ 2 * (ℬ div 2) * ℬ^((2*δ+1) * n ν)"
by simp
thus "2 * K2 ≥ ℬ^((2*δ+1) * n ν + 1)"
using ℬ_even power_add by simp
show "K2 < ℬ^((2*δ+1)*n ν + 1)"
proof -
have "ℬ div 2 < ℬ"
using ℬ_ge_2 by simp
thus ?thesis
unfolding K2_def_alt using digit_sum_bound_int ℬ_ge_2 by simp
qed
qed
show "0 ≤ K g"
unfolding K_def_alt using c_δ_D_bound K2_bound by simp linarith
show "2 * (K g) < 3 * ℬ^((2*δ+1)*n ν + 1)"
unfolding K_def_alt using c_δ_D_bound K2_bound by simp linarith
qed
text ‹technical condition 2.7, first part›
lemma T_bound: "0 ≤ T ∧ T < N"
proof
show "0 ≤ T"
proof -
have "T = M + (ℬ - 2) * ℬ^(n (ν+1)) * N0"
using T_def n_def by simp
thus ?thesis
using M_bound ℬ_ge_2 is_power2_ge1[OF N0_power2] by auto
qed
have 0: "1 + (ℬ - 2) * ℬ^(n (ν+1)) ≤ N1"
proof -
have "1 + (ℬ - 2) * ℬ^(n (ν+1)) ≤ 2 * ℬ^(n (ν+1)) + (ℬ - 2) * ℬ^(n (ν+1))"
using is_power2_ge1[OF ℬ_power2] by (smt (z3) one_le_power)
also have "... = ℬ^(n (ν+1) + 1)"
using ℬ_ge_2 by (metis add.commute diff_add_cancel int_distrib(1) power_add power_one_right)
also have "... ≤ 4 * ℬ^((2*δ+1) * n ν + 1)"
proof -
have "n (ν+1) + 1 ≤ (2*δ+1) * n ν + 1"
unfolding n_def by simp
thus ?thesis
using is_power2_ge1[OF ℬ_power2] power_increasing by (smt (verit, ccfv_SIG) K_bound)
qed
also have "... = N1"
using N1_def n_def by simp
finally show ?thesis .
qed
show "T < N"
proof -
have "T < N0 + (ℬ - 2) * ℬ^(n (ν+1)) * N0"
using T_def M_bound n_def by simp
also have "... = (1 + (ℬ - 2) * ℬ^(n (ν+1))) * N0"
by (simp add: algebra_simps)
also have "... ≤ N1 * N0"
using 0 is_power2_ge1[OF N0_power2] by simp
also have "... = N"
using N_def by simp
finally show ?thesis .
qed
qed
text ‹technical condition 2.7, second part›
lemma S_bound: "0 ≤ S g ∧ S g < N"
proof
show "0 ≤ S g"
proof -
have "S g = g + 2 * K g * N0"
using S_def by simp
thus ?thesis
using K_bound g_lower_bound is_power2_ge1[OF N0_power2] by simp
qed
have 0: "g < ℬ^((2*δ+1)*n ν + 1)"
proof -
have "g < ℬ^(n ν + 1)"
using g_lt_N0 N0_def n_def by simp
also have "... ≤ ℬ^((2*δ+1)*n ν + 1)"
proof -
have "n ν + 1 ≤ (2*δ+1)*n ν + 1"
unfolding n_def by simp
thus ?thesis
using is_power2_ge1[OF ℬ_power2] power_increasing by blast
qed
finally show ?thesis .
qed
show "S g < N"
proof -
have "S g = g + 2 * K g * N0"
using S_def by simp
also have "... ≤ (g + 2 * K g) * N0"
proof -
have "g ≤ g * N0"
using g_lower_bound is_power2_ge1[OF N0_power2]
by (simp add: mult_le_cancel_left1)
thus ?thesis
by (simp add: algebra_simps)
qed
also have "... < N1 * N0"
proof -
have "g + 2 * K g < N1"
unfolding N1_def using 0 K_bound n_def by simp
thus ?thesis
using is_power2_ge1[OF N0_power2] by auto
qed
also have "... = N"
using N_def by simp
finally show ?thesis .
qed
qed
text ‹Technical condition 2.8›
lemma tau_S_T_decomp: "τ (nat (S g)) (nat (T)) =
τ (nat g) (nat (M)) + τ (nat (2 * K g)) (nat ((ℬ - 2) * ℬ^(n (ν+1))))"
proof -
have 0: "nat (S g) = nat g + nat (K g) * nat (2 * N0)"
proof -
have "nat (S g) = nat (g + 2 * K g * N0)"
using S_def by simp
also have "... = nat g + 2 * nat (K g) * nat (N0)"
using g_lower_bound K_bound is_power2_ge1[OF N0_power2]
by (simp add: nat_add_distrib nat_mult_distrib)
finally show ?thesis
by auto
qed
have 1: "nat (T) = nat (M) + nat ((ℬ div 2 - 1) * ℬ^(n (ν+1))) * nat (2 * N0)"
proof -
have "nat (T) = nat (M + (ℬ - 2) * ℬ^(n (ν+1)) * N0)"
using T_def n_def by simp
also have "... = nat (M + 2 * (ℬ div 2 - 1) * ℬ^(n (ν+1)) * N0)"
using ℬ_even by simp
also have "... = nat (M) + nat ((ℬ div 2 - 1) * ℬ^(n (ν+1))) * nat (2 * N0)"
using ℬ_ge_2 M_bound is_power2_ge1[OF N0_power2]
by (simp add: nat_power_eq nat_add_distrib nat_mult_distrib)
finally show ?thesis .
qed
have "τ (nat (S g)) (nat (T)) =
τ (nat g + nat (K g) * nat (2 * N0))
(nat (M) + nat ((ℬ div 2 - 1) * ℬ^(n (ν+1))) * nat (2 * N0))"
using 0 1 by metis
also have "... = τ (nat g) (nat (M)) + τ (nat (K g)) (nat ((ℬ div 2 - 1) * ℬ^(n (ν+1))))"
proof -
obtain k where k_def: "nat (2 * N0) = 2^k"
using N0_power2 is_power2_def by fastforce
have "nat g + nat (M) < nat (2 * N0)"
using M_bound g_lt_N0 by auto
thus ?thesis
using count_carries_add_shift_no_overflow k_def by metis
qed
also have "... = τ (nat g) (nat (M)) + τ (nat (2 * K g)) (nat ((ℬ - 2) * ℬ^(n (ν+1))))"
proof -
have 0: "2 * nat (K g) = nat (2 * K g)"
by simp
have 1: "ℬ - 2 = 2 * (ℬ div 2 - 1)"
using ℬ_even by simp
have 2: "2 * nat ((ℬ div 2 - 1) * ℬ^(n (ν+1))) = nat ((ℬ - 2) * ℬ^(n (ν+1)))"
unfolding 1 by linarith
show ?thesis
using count_carries_even_even 0 2 by metis
qed
finally show ?thesis .
qed
end
text ‹Helper lemmas for masking›
lemma n_masking_lemma[simp]:
assumes "masking_lemma δ ν (nat ℬ) (nat b) C"
shows "masking_lemma.n δ = n"
unfolding n_def using masking_lemma.n_def assms by auto
lemma m_masking_lemma[simp]:
assumes "masking_lemma δ ν (nat ℬ) (nat b) C"
shows "masking_lemma.m δ ν (nat ℬ) (nat b) j = m j"
proof -
have 0: "int (nat ℬ) = ℬ"
using is_power2_ge1[OF ℬ_power2] by simp
have 1: "int (nat b) = b"
using is_power2_ge1[OF b_power2] by simp
have 2: "int (nat ℬ - nat b) = (ℬ - b)"
proof -
have "int (nat ℬ - nat b) = int (nat ℬ) - int (nat b)"
using b_le_ℬ by auto
thus ?thesis
using 0 1 by simp
qed
have 3: "int (nat ℬ - 1) = (ℬ - 1)"
proof -
have "1 ≤ nat ℬ"
using is_power2_ge1[OF ℬ_power2] by auto
thus ?thesis
using 0 by simp
qed
have "masking_lemma.m δ ν (nat ℬ) (nat b) j =
(if j ∈ n ` {1..ν} then int (nat ℬ - nat b) else int (nat ℬ - 1))"
unfolding masking_lemma.m_def[OF assms] n_masking_lemma[OF assms] by auto
also have "... = (if j ∈ n ` {1..ν} then (ℬ - b) else (ℬ - 1))"
using 2 3 by simp
also have "... = m j"
using m_def by simp
finally show ?thesis .
qed
lemma M_masking_lemma[simp]:
assumes "masking_lemma δ ν (nat ℬ) (nat b) C"
shows "masking_lemma.M δ ν (nat ℬ) (nat b) = nat M"
proof -
have "masking_lemma.M δ ν (nat ℬ) (nat b) = (∑j=0..n ν. m j * ℬ^j)"
unfolding masking_lemma.M_def[OF assms] using is_power2_ge1[OF ℬ_power2]
unfolding n_masking_lemma[OF assms] m_masking_lemma[OF assms, symmetric] by auto
thus ?thesis
using M_def by auto
qed
text ‹Helper lemmas to apply Lemma 1.8›
text ‹We can only apply Lemma 1.8 when g can be decomposed in base ‹ℬ› with digits ‹<b››
context
fixes g :: int
and z :: "nat ⇒ int"
assumes g_sum: "g = (∑i=1..ν. z i * ℬ^(n i))"
and z_bound: "∀i. 0 ≤ z i ∧ z i < b"
begin
text ‹This is quite verbose but justified by the following lemma›
definition z_list :: "nat list" where
"z_list ≡ nat a # map (nat ∘ z ∘ nat) [1..ν]"
lemma z_list_nth_head: "z_list!0 = nat a"
unfolding z_list_def by simp
lemma z_list_nth_tail: "1 ≤ i ⟹ i ≤ ν ⟹ z_list!i = nat (z i)"
proof -
assume "1 ≤ i" and "i ≤ ν"
then obtain j where j_def: "i = j + 1" and "j < ν"
using nat_le_iff_add by fastforce
have "z_list!i = (map (nat ∘ z ∘ nat) [1..ν])!j"
unfolding z_list_def j_def by simp
also have "... = (nat ∘ z ∘ nat) ([1..ν]!j)"
using List.nth_map ‹j < ν› by simp
also have "... = nat (z (j+1))"
by (metis Suc_eq_plus1 ‹i ≤ ν› add.commute comp_apply int_ops(4) j_def nat_int nth_upto
of_nat_mono)
finally show ?thesis
using j_def by simp
qed
lemma length_z_list[simp]: "length z_list = ν+1"
unfolding z_list_def by auto
lemma δ_lemma_1_8[simp]: "Lemma_1_8_Defs.δ P = δ"
using Lemma_1_8_Defs.δ_def δ_def by simp
lemma ν_lemma_1_8[simp]: "Lemma_1_8_Defs.ν P = ν"
using Lemma_1_8_Defs.ν_def ν_def by simp
lemma n_lemma_1_8[simp]: "Lemma_1_8_Defs.n P = n"
using Lemma_1_8_Defs.n_def n_def δ_lemma_1_8 by auto
lemma insertion_z_assign[simp]:
"insertion (Lemma_1_8_Defs.z_assign z_list) P = insertion (z(0 := a)) P"
proof -
have "i∈vars P ⟹ Lemma_1_8_Defs.z_assign z_list i = (z(0 := a)) i" for i
proof -
assume "i∈vars P"
hence i_bound: "i ≤ ν"
unfolding ν_def max_vars_def by (simp add: vars_finite)
have "Lemma_1_8_Defs.z_assign z_list i = int (z_list !⇩0 i)"
unfolding Lemma_1_8_Defs.z_assign_def
by (metis Suc_eq_plus1 i_bound le_imp_less_Suc length_map length_z_list nth0_nth nth_map)
also have "... = int (z_list ! i)"
using length_z_list i_bound by (simp add: nth0_nth)
also have "... = int (if i = 0 then nat a else nat (z i))"
using z_list_nth_head z_list_nth_tail i_bound by auto
also have "... = (if i = 0 then a else z i)"
using a_nonneg z_bound by auto
also have "... = (z(0 := a)) i"
by auto
finally show ?thesis .
qed
thus ?thesis
using insertion_irrelevant_vars by metis
qed
lemma S_lemma_1_8[simp]:
"int (Lemma_1_8_Defs.S P (nat ℬ)) = (∑i=0..(2*δ+1)*n ν. int (β div 2) * b^δ * ℬ^i)"
proof -
have "int (Lemma_1_8_Defs.S P (nat ℬ)) =
(∑i≤(2*δ+1) * n ν. int (((nat ℬ) div 2) * (nat ℬ)^i))"
unfolding Lemma_1_8_Defs.S_def Lemma_1_8_Defs.b_def δ_lemma_1_8 n_lemma_1_8 ν_lemma_1_8 by simp
also have "... = (∑i≤(2*δ+1) * n ν. (ℬ div 2) * ℬ^i)"
proof -
have "(nat ℬ) div 2 = nat (ℬ div 2)"
using ℬ_even by auto
thus ?thesis
using is_power2_ge1[OF ℬ_power2] by auto
qed
also have "... = (∑i=0..(2*δ+1) * n ν. (ℬ div 2) * ℬ^i)"
using atLeast0AtMost by presburger
also have "... = (∑i=0..(2*δ+1)*n ν. int (β div 2) * b^δ * ℬ^i)"
proof -
have "ℬ div 2 = int (β div 2) * b^δ"
unfolding ℬ_def β_def by (simp add: dvd_div_mult r_pos[OF δ_pos] zdiv_int)
thus ?thesis
by auto
qed
finally show ?thesis .
qed
lemma c_lemma_1_8[simp]:
"insertion (Lemma_1_8_Defs.ℬ_assign (nat ℬ)) (Lemma_1_8_Defs.c P z_list) = a * ℬ + g"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∑i≤ν. int (z_list!i) * (Lemma_1_8_Defs.ℬ_assign (nat ℬ) (0::nat))^(n i))"
unfolding Lemma_1_8_Defs.c_def Lemma_1_8_Defs.X_def n_lemma_1_8 ν_lemma_1_8
by simp
also have "... = (∑i≤ν. int (z_list!i) * ℬ^(n i))"
unfolding Lemma_1_8_Defs.ℬ_assign_def using ℬ_ge_2 by simp
also have "... = int (z_list!0) * ℬ^(n 0) + (∑i=1..ν. int (z_list!i) * ℬ^(n i))"
by (simp add: atLeastSucAtMost_greaterThanAtMost atMost_atLeast0 sum.head)
also have "... = a * ℬ + (∑i=1..ν. int (z_list!i) * ℬ^(n i))"
using n_def z_list_def a_nonneg by auto
also have "... = a * ℬ + g"
unfolding g_sum using z_bound z_list_nth_tail by auto
finally show ?thesis .
qed
lemma D_lemma_1_8[simp]:
"insertion (Lemma_1_8_Defs.ℬ_assign (nat ℬ)) (Lemma_1_8_Defs.D P) = D"
(is "?lhs = ?rhs")
proof -
have 0: "Lemma_1_8_Defs.D_precoeff P i = D_precoeff i" for i
unfolding Lemma_1_8_Defs.D_precoeff_def D_precoeff_def by simp
have 1: "Lemma_1_8_Defs.P_coeff P i = P_coeff i" for i
unfolding Lemma_1_8_Defs.P_coeff_def P_coeff_def by simp
have 2: "Lemma_1_8_Defs.D_exponent P i = D_exponent i" for i
unfolding Lemma_1_8_Defs.D_exponent_def D_exponent_def by simp
have 3: "Lemma_1_8_Defs.δ_tuples P = δ_tuples"
unfolding Lemma_1_8_Defs.δ_tuples_def δ_tuples_def by simp
have "?lhs = (∑i∈δ_tuples. D_precoeff i * P_coeff i * (Lemma_1_8_Defs.ℬ_assign (nat ℬ) (0::nat))^(D_exponent i))"
unfolding Lemma_1_8_Defs.D_def Lemma_1_8_Defs.X_def by (simp add: 0 1 2 3)
also have "... = D"
unfolding D_def Lemma_1_8_Defs.ℬ_assign_def using ℬ_ge_2 by simp
finally show ?thesis .
qed
lemma R_lemma_1_8[simp]:
"insertion (Lemma_1_8_Defs.ℬ_assign (nat ℬ)) (Lemma_1_8_Defs.R P z_list) = (c g)^δ * D"
(is "?lhs = ?rhs")
proof -
have "?lhs = (1 + a * ℬ + g)^δ * D"
unfolding Lemma_1_8_Defs.R_def by (simp add: algebra_simps)
also have "... = (c g)^δ * D"
unfolding c_def by simp
finally show ?thesis .
qed
lemma K_lemma_1_8[simp]:
"Lemma_1_8_Defs.K P (nat ℬ) z_list = K g"
unfolding Lemma_1_8_Defs.K_def K_def by simp
lemma lemma_1_8_helper:
shows "insertion (z(0 := a)) P = 0 ⟷ τ (nat (2 * K g)) (nat ((ℬ - 2) * ℬ^(n (ν+1)))) = 0"
and "K g > ℬ^((2*δ+1) * n ν)"
and "K g < ℬ^((2*δ+1) * n ν + 1)"
proof -
have z_sum_bound: "sum_list z_list < (ν+1) * nat b"
proof -
have "sum_list z_list = (∑i=0..ν. z_list!i)"
using sum_list_sum_nth length_z_list
by (metis Suc_eq_plus1 atLeastLessThanSuc_atLeastAtMost)
also have "... = z_list!0 + (∑i=1..ν. z_list!i)"
by (simp add: atLeastSucAtMost_greaterThanAtMost sum.head)
also have "... = nat a + (∑i=1..ν. nat (z i))"
using z_list_nth_head z_list_nth_tail by auto
also have "... ≤ nat a + (∑i=1..ν. nat b)"
using z_bound by (smt (verit, del_insts) add_left_mono nat_le_eq_zle sum_mono)
also have "... = nat a + card {1..ν} * nat b"
using sum_constant by auto
also have "... = nat a + ν * nat b"
by auto
also have "... < nat b + ν * nat b"
unfolding b_def by simp (smt (verit) mult_less_cancel_left2 a_nonneg f_pos)
finally show ?thesis
by auto
qed
have ℬ_lower_bound: "2 * fact δ * ℒ * (sum_list z_list + 1)^δ < nat ℬ"
proof -
have 0: "(sum_list z_list + 1)^δ < (ν+3)^δ * (nat b)^δ"
proof -
have "sum_list z_list + 1 ≤ (ν+1) * nat b"
using z_sum_bound by auto
also have "... < (ν+3) * nat b"
using is_power2_ge1[OF b_power2]
by (smt (verit, ccfv_threshold) add_less_cancel_left mult.commute nat_mult_less_cancel_disj
one_less_numeral_iff semiring_norm(77) zero_less_nat_eq)
finally show ?thesis
using power_mult_distrib zero_le by (metis δ_pos power_strict_mono)
qed
have "2 * fact δ * ℒ * (sum_list z_list + 1)^δ < 2 * fact δ * ℒ * (ν+3)^δ * (nat b)^δ"
using 0 fact_ge_1 ℒ_pos[OF δ_pos] by auto
also have "... ≤ β * (nat b)^δ"
using β_lower_bound by auto
also have "... = nat ℬ"
unfolding ℬ_def using is_power2_ge1[OF b_power2] by (simp add: nat_mult_distrib nat_power_eq)
finally show ?thesis .
qed
have 0: "Lemma_1_8 P (nat ℬ) (int ℒ) z_list"
unfolding Lemma_1_8_def K_Nonnegative_def
using ℬ_power2 is_power2_ge1 ℒ_ge_max_coeff[OF δ_pos] δ_pos ℒ_pos[OF δ_pos]
ℬ_lower_bound Lemma_1_8_axioms.intro ℬ_even even_nat_iff by auto
show "K g > ℬ^((2*δ+1) * n ν)"
using Lemma_1_8.lemma_1_8(2)[OF 0] ℬ_ge_2 by simp
show "K g < ℬ^((2*δ+1) * n ν + 1)"
using Lemma_1_8.lemma_1_8(3)[OF 0] ℬ_ge_2 by simp
show "insertion (z(0 := a)) P = 0 ⟷ τ (nat (2 * K g)) (nat ((ℬ - 2) * ℬ^(n (ν+1)))) = 0"
using Lemma_1_8.lemma_1_8(1)[OF 0] ℬ_ge_2 nat_diff_distrib nat_mult_distrib nat_power_eq
by auto
qed
end
lemma aux_sum_bound_reindex_n:
"0 ≤ (x::int) ⟹ (∑i=0..q. x^(n i)) ≤ (∑i=0..n q. x^i)"
proof (induct q)
case 0 thus ?case apply simp
by (metis member_le_sum atLeastAtMost_iff dual_order.refl finite_atLeastAtMost zero_le
zero_le_power)
next
case (Suc q)
have 0: "Suc (n q) ≤ n (Suc q)"
unfolding n_def using δ_pos by auto
have "(∑i=0..Suc q. x^(n i)) = (∑i=0..q. x^(n i)) + x^(n (Suc q))"
by simp
also have "... ≤ (∑i=0..n q. x^i) + x^(n (Suc q))"
using Suc by simp
also have "... ≤ (∑i=0..n q. x^i) + (∑i=Suc(n q)..n (Suc q). x^i)"
using 0 Suc.prems member_le_sum
by (metis add.commute add_le_cancel_right atLeastAtMost_iff finite_atLeastAtMost order.refl
zero_le_power)
also have "... = (∑i=0..n (Suc q). x^i)"
proof -
have "{0..n q} ∪ {Suc (n q)..n (Suc q)} = {0..n (Suc q)}"
using 0 by auto
moreover have "{0..n q} ∩ {Suc (n q)..n (Suc q)} = {}"
by auto
ultimately show ?thesis
using sum.union_disjoint by (metis finite_atLeastAtMost)
qed
finally show ?case .
qed
lemma coding_theorem_direct:
"statement1_strong y ⟹ (∃g. statement2_strong g)"
proof
assume assm: "statement1_strong y"
have "1 < b"
using assm unfolding statement1_strong_def statement1_weak_def
by (smt (verit, del_insts))
have y_bound: "0 ≤ y i ∧ y i < b" for i
using assm unfolding statement1_strong_def statement1_weak_def by auto
define g where "g ≡ (∑i=1..ν. y i * ℬ^(n i))"
have g_lower_bound: "b ≤ g"
proof -
from assm obtain j where 0: "y j > 0" and j_1ν: "j ∈ {1..ν}"
unfolding statement1_strong_def statement1_weak_def
by (meson leD linorder_neqE_linordered_idom)
have "g ≥ y j * ℬ^(n j)"
using assm member_le_sum[OF j_1ν] unfolding statement1_strong_def statement1_weak_def
by (smt (verit, del_insts) b_le_ℬ finite_atLeastAtMost g_def mult_nonneg_nonneg mult_zero_left zero_le_power)
hence "g ≥ ℬ^(n j)" using 0 is_power2_ge1[OF ℬ_power2]
by (smt (verit, ccfv_SIG) mult_le_cancel_right1 zero_less_power)
hence "g ≥ ℬ"
unfolding n_def using is_power2_ge1[OF ℬ_power2]
by (smt (verit, ccfv_SIG) δ_pos add_gr_0 self_le_power zero_less_power)
thus "g ≥ b"
using b_le_ℬ by simp
qed
have g_upper_bound: "g < b * ℬ^(n ν)"
proof -
have 0: "y i * ℬ^(n i) ≤ (b - 1) * ℬ^(n i)" for i
using y_bound is_power2_ge1[OF ℬ_power2] by auto
have "g = (∑i∈{0<..ν}. y i * ℬ^(n i))"
unfolding g_def by (simp add: atLeastSucAtMost_greaterThanAtMost)
also have "... ≤ y 0 * ℬ^(n 0) + (∑i∈{0<..ν}. y i * ℬ^(n i))"
using is_power2_ge1 ℬ_power2 b_power2 y_bound
by (smt (verit, del_insts) mult_nonneg_nonneg zero_le_power)
also have "... = (∑i∈{0..ν}. y i * ℬ^(n i))"
using sum.head[of "0" "ν"] by (smt (verit) zero_le)
also have "... ≤ (∑i∈{0..ν}. (b - 1) * ℬ^(n i))"
using 0 sum_mono by meson
also have "... = (b - 1) * (∑i=0..ν. ℬ^(n i))"
using sum_distrib_left by metis
also have "... ≤ (b - 1) * (∑i=0..n ν. ℬ^i)"
using aux_sum_bound_reindex_n is_power2_ge1[OF b_power2] ℬ_ge_2 by (simp add: mult_left_mono)
also have "... ≤ (b - 1) * (∑i=0..<n ν. ℬ^i) + (b - 1) * ℬ^(n ν)"
by (metis atLeastLessThanSuc_atLeastAtMost distrib_left order_refl sum.atLeast0_lessThan_Suc)
also have "... ≤ (ℬ - 1) * (∑i=0..<n ν. ℬ^i) + (b - 1) * ℬ^(n ν)"
by (smt (verit, ccfv_SIG) b_le_ℬ ℬ_power2 is_power2_ge1 mult_right_mono sum_nonneg
zero_le_power)
also have "... = ℬ^(n ν) - 1 + (b - 1) * ℬ^(n ν)"
by (simp add: ℬ_ge_2 atLeast0LessThan power_diff_1_eq)
also have "... = b * ℬ^(n ν) - 1"
by (simp add: algebra_simps)
also have "... < b * ℬ^(n ν)"
by auto
finally show ?thesis .
qed
have tau_KB: "τ (nat (2 * K g)) (nat ((ℬ - 2) * ℬ^(n (ν+1)))) = 0"
proof -
have "insertion (y(0 := a)) P = 0"
using assm unfolding statement1_strong_def statement1_weak_def by auto
thus ?thesis
using lemma_1_8_helper(1) g_def y_bound by auto
qed
have tau_gM: "τ (nat g) (nat (M)) = 0"
proof -
define C where "C ≡ b * ℬ^(n ν)"
interpret masking: masking_lemma δ ν "(nat ℬ)" "(nat b)" "(nat C)"
unfolding masking_lemma_def C_def n_def using δ_pos ℬ_power2 b_power2 ℬ_ge_2 b_le_ℬ is_power2_ge1
by (smt (verit, ccfv_SIG) ℬ_even dvd_imp_le even_nat_iff mult_le_mono1 nat_eq_iff2
nat_less_eq_zless nat_mult_distrib nat_power_eq order_le_less zero_less_nat_eq)
have 1: "nat g = (∑i=1..ν. nat (y i) * (nat ℬ)^(n i))"
proof -
have "0 ≤ y i * ℬ^(n i)" for i
using y_bound is_power2_ge1[OF ℬ_power2] by auto
hence "nat g = (∑i=1..ν. nat (y i * ℬ^(n i)))"
unfolding g_def using nat_sum_distrib by auto
also have "... = (∑i=1..ν. nat (y i) * (nat ℬ)^(n i))"
using y_bound is_power2_ge1[OF ℬ_power2] nat_mult_distrib nat_power_eq by auto
finally show ?thesis .
qed
show ?thesis
using masking.masking_lemma 1 y_bound
unfolding n_masking_lemma[OF masking.masking_lemma_axioms]
M_masking_lemma[OF masking.masking_lemma_axioms]
by (meson nat_less_eq_zless)
qed
have tau_ST: "τ (nat (S g)) (nat (T)) = 0"
using tau_S_T_decomp g_lower_bound g_upper_bound is_power2_ge1[OF b_power2] tau_KB tau_gM
by auto
have dvd_XY: "Y dvd (2 * nat (X g) choose nat (X g))"
proof -
have 0: "0 ≤ T ∧ T < N"
using T_bound g_lower_bound g_upper_bound is_power2_ge1[OF b_power2] by force
have 1: "0 ≤ S g ∧ S g < N"
using S_bound g_lower_bound g_upper_bound is_power2_ge1[OF b_power2] by force
have 2: "Tau_Reduction (nat (N)) (nat (S g)) (nat (T))"
unfolding Tau_Reduction_def using N_power2 0 1
by (metis int_one_le_iff_zero_less is_power2_ge1 nat_0_le order_le_less zless_nat_conj)
have 3: "Tau_Reduction.R (nat (N)) (nat (S g)) (nat (T)) = nat (R g)" (is "?lhs = ?rhs")
proof -
have "?lhs = nat ((S g + T + 1) * N + T + 1)"
unfolding Tau_Reduction.R_def[OF 2] using 0 1 by (simp add: nat_add_distrib nat_mult_distrib)
also have "... = nat (R g)"
unfolding R_def by simp
finally show ?thesis unfolding Tau_Reduction.R_def[OF 2] by simp
qed
have "(nat N)^2 dvd (2 * (nat N - 1) * (nat (R g)) choose (nat N - 1) * nat (R g))"
using Tau_Reduction.tau_as_binomial_coefficient[OF 2] 3 tau_ST by presburger
hence "nat ((N)^2) dvd (2 * nat ((N - 1) * R g) choose nat ((N - 1) * R g))"
using is_power2_ge1[OF N_power2]
by (simp add: ab_semigroup_mult_class.mult_ac(1) nat_diff_distrib nat_mult_distrib nat_power_eq)
hence "nat (Y) dvd (2 * nat (X g) choose nat (X g))"
unfolding X_def Y_def by simp
thus ?thesis
by auto
qed
have "b * ℬ^(n ν) = (int γ) * b^α"
unfolding ℬ_def α_def γ_def by (simp add: power_mult power_mult_distrib)
thus "statement2_strong g"
unfolding statement2_strong_def using g_lower_bound g_upper_bound dvd_XY by auto
qed
lemma coding_theorem_reverse:
"statement2_weak g ⟹ (∃y. statement1_weak y)"
proof -
assume assm: "statement2_weak g"
have g_bound: "0 ≤ g ∧ g < 2 * b * ℬ^(n ν)"
proof -
have "b * ℬ^(n ν) = (int γ) * b^α"
unfolding ℬ_def γ_def α_def by (simp add: power_mult power_mult_distrib)
thus ?thesis
using assm unfolding statement2_weak_def by auto
qed
have tau_ST: "τ (nat (S g)) (nat (T)) = 0"
proof -
have 0: "0 ≤ T ∧ T < N"
using T_bound g_bound is_power2_ge1[OF b_power2] by force
have 1: "0 ≤ S g ∧ S g < N"
using S_bound g_bound is_power2_ge1[OF b_power2] by force
have 2: "Tau_Reduction (nat (N)) (nat (S g)) (nat (T))"
unfolding Tau_Reduction_def using N_power2 0 1
by (metis int_one_le_iff_zero_less is_power2_ge1 nat_0_le order_le_less zless_nat_conj)
have 3: "Tau_Reduction.R (nat (N)) (nat (S g)) (nat (T)) = nat (R g)" (is "?lhs = ?rhs")
proof -
have "?lhs = nat ((S g + T + 1) * N + T + 1)"
unfolding Tau_Reduction.R_def[OF 2] using 0 1 by (simp add: nat_add_distrib nat_mult_distrib)
also have "... = nat (R g)"
unfolding R_def by simp
finally show ?thesis .
qed
have "nat Y = (nat N)⇧2"
unfolding Y_def using is_power2_ge1[OF N_power2] by (simp add: nat_power_eq)
moreover have "2 * nat (X g) = 2 * (nat N - 1) * nat (R g)"
unfolding X_def using is_power2_ge1[OF N_power2]
by simp (smt (verit, best) nat_1 nat_diff_distrib nat_mult_distrib)
moreover have "nat (X g) = (nat N - 1) * nat (R g)"
unfolding X_def using is_power2_ge1[OF N_power2]
by simp (smt (verit, best) nat_1 nat_diff_distrib nat_mult_distrib)
ultimately show ?thesis
using Tau_Reduction.tau_as_binomial_coefficient[OF 2] 3 assm unfolding statement2_weak_def
by (metis "0" bot_nat_0.extremum_strict nat_dvd_iff nat_eq_iff2
nat_less_eq_zless zero_eq_power2)
qed
have tau_gM: "τ (nat g) (nat (M)) = 0"
and tau_KB: "τ (nat (2 * K g)) (nat ((ℬ - 2) * ℬ^(n (ν+1)))) = 0"
using tau_S_T_decomp g_bound tau_ST by simp_all
define C :: int where "C ≡ ℬ * ℬ^(n ν)"
interpret masking: masking_lemma δ ν "(nat ℬ)" "(nat b)" "(nat C)"
unfolding masking_lemma_def C_def n_def using δ_pos ℬ_power2 b_power2 ℬ_ge_2 b_le_ℬ is_power2_ge1
by (smt (verit, ccfv_SIG) ℬ_even dvd_imp_le even_nat_iff mult_le_mono1 nat_eq_iff2
nat_less_eq_zless nat_mult_distrib nat_power_eq order_le_less zero_less_nat_eq)
have 1: "nat g < nat C"
unfolding C_def using g_bound N0_def g_lt_N0 n_def by force
obtain y::"nat⇒nat"
where g_sum_y: "nat g = (∑i=1..ν. y i * (nat ℬ)^(n i))"
and y_bound: "∀i. y i < nat b"
using masking.masking_lemma 1 tau_gM
unfolding n_masking_lemma[OF masking.masking_lemma_axioms] M_masking_lemma[OF masking.masking_lemma_axioms]
by blast
define z::"nat⇒int" where "z ≡ (λi. if i = 0 then a else int (y i))"
have g_sum: "g = (∑i=1..ν. z i * ℬ^(n i))"
proof -
have "i∈{1..ν} ⟹ z i * ℬ^(n i) = int (y i * (nat ℬ)^(n i))" for i
using ℬ_ge_2 z_def by auto
hence "(∑i=1..ν. z i * ℬ^(n i)) = (∑i=1..ν. int (y i * (nat ℬ)^(n i)))"
by simp
also have "... = int (∑i=1..ν. y i * (nat ℬ)^(n i))"
by simp
also have "... = int (nat g)"
using g_sum_y by simp
also have "... = g"
using g_bound by auto
finally show ?thesis
by auto
qed
have z_bound: "0 ≤ z i ∧ z i < b" for i
proof (cases "i = 0")
case True thus ?thesis
unfolding z_def b_def using a_nonneg f_pos
by simp (smt (verit, ccfv_SIG) mult_less_cancel_left2)
next
case False thus ?thesis
unfolding z_def apply simp using y_bound zless_nat_eq_int_zless by blast
qed
have z_0: "z 0 = a"
unfolding z_def by simp
have "insertion z P = 0"
using lemma_1_8_helper(1)[OF g_sum] z_bound tau_KB z_0 by auto
thus ?thesis
unfolding statement1_weak_def using z_bound z_0 by auto
qed
lemma coding_theorem_reverse':
assumes "∃g. 0 ≤ g ∧ g < 2 * (int γ) * b^α ∧ Y dvd (2 * nat (X g) choose nat (X g))"
shows "∃z. (z 0 = a) ∧ (∀i. 0 ≤ z i ∧ z i < b) ∧ insertion z P = 0"
using coding_theorem_reverse[unfolded statement2_weak_def statement1_weak_def]
using assms by auto
end
end