Theory Additional_Lemmas

theory Additional_Lemmas

imports 
  Main
  infnorm
  Partition
  Lattice_int
  Digits_int
begin

section ‹Additional Lemmas›

text ‹Lemma about length and concat.›
lemma length_concat_map_5: 
  "length (concat (map (λi. [f1 i, f2 i, f3 i, f4 i, f5 i]) xs)) = length xs * 5" 
by (induct xs, auto)

text ‹Lemma about splitting the index of sums.›
lemma sum_split_idx_prod:
  "(∑i=0..<k*l::nat. f i) = (∑i=0..<k. (∑j=0..<l. f (i*l+j)))"
proof -
  have set_rew: "{0..<k*l} = (λ(i,j). i*l+j) ` ({0..<k} × {0..<l})"
  proof (safe, goal_cases)
    case (1 x)
    have "x = (λ(i,j). i*l+j) (x div l, x mod l)" by auto
    moreover have "(x div l, x mod l)∈{0..<k} × {0..<l}" using 1 less_mult_imp_div_less
      by (metis le_less_trans lessThan_atLeast0 lessThan_iff mem_Sigma_iff
        mod_less_divisor mult_zero_right neq0_conv zero_le)
    ultimately show ?case by blast
  next
    case (2 x i j)
    then show ?case 
    by (auto, metis less_nat_zero_code linorder_neqE_nat mod_lemma mult.commute nat_mod_lem)
  qed
  have inj: "inj_on (λ(i, y). i * l + y) ({0..<k} × {0..<l})" 
    unfolding inj_on_def by (auto) 
      (metis add.commute add_right_imp_eq linorder_neqE_nat mod_mult_self2 mult.commute 
        mult_cancel_right nat_mod_lem not_less_zero, 
       metis add.commute le0 le_less_trans mod_mult_self2 mult.commute nat_mod_lem)
  have "(∑ i∈{0..<k*l}. f i) = (∑(i,j)∈{0..<k}×{0..<l}. f (i*l+j))" 
    unfolding set_rew using inj
    by (subst sum.reindex[of "(λ(i, j). i * l + j)" "({0..<k} × {0..<l})" f])
       (auto simp add: prod.case_distrib)
  also have "… = (∑i∈{0..<k}. (∑j∈{0..<l}. f (i*l+j)))"
    using sum.cartesian_product[of "(λi j. f (i*l+j))" "{0..<l}" "{0..<k}", symmetric]
    by auto
  finally show ?thesis by auto
qed

text ‹Helping lemma to split sums.›

lemma lt_M:
  assumes "M > (∑i<(n::nat). ¦b i¦::int)"
          "∀i<n. ¦x i¦ ≤ 1" 
  shows "¦(∑i<n. x i * b i)¦ < M"
proof - 
  have "¦(∑i<(n::nat). x i * b i)::int¦ ≤ (∑i<n. ¦x i * b i¦)" using sum_abs by auto
  moreover have "… = (∑i<n. ¦x i¦ * ¦b i¦)" using abs_mult by metis
  moreover have "… ≤ (∑i<n. ¦b i¦)" using assms 
    by (smt (verit, best) lessThan_iff mult_cancel_right2 sum_mono zero_less_mult_iff)
  moreover have "… = (∑i<n. ¦b i¦)" using sum_distrib_left by metis
  ultimately have "¦(∑i<n. x i * b i)¦ ≤ (∑i<n. ¦b i¦)" by linarith
  then show ?thesis using assms by auto
qed



lemma split_sum:
  "(∑i<(n::nat). x i * (a i + M * b i)::int) = (∑i<n. x i * a i) + M * (∑i<n. x i * b i)"
proof -
  have "(∑i<(n::nat). x i * (a i + M * b i)) = (∑i<n. x i * a i) + (∑i<n. M * x i * b i)"
    by (simp add: distrib_left mult.commute mult.left_commute)
  also have "… = (∑i<n. x i * a i) + M * (∑i<n. x i * b i)"
    using sum_distrib_left[symmetric, where r=M and f="(λi. x i*b i)" and A = "{0..<n}"]  
    by (metis (no_types, lifting) lessThan_atLeast0 mult.assoc sum.cong)
  finally show ?thesis by blast
qed



lemma split_eq_system:
  assumes "M > (∑i<n::nat. ¦a i¦::int)"
          "∀i<n. ¦x i¦ ≤ 1" 
          "(∑i<n. x i * (a i + M * b i)) = 0" 
  shows   "(∑i<n. x i * a i) = 0 ∧ (∑i<n. x i * b i) = 0"
using assms proof (safe, goal_cases)
  case 1
  then show ?case 
  proof (cases "(∑i<n. x i * b i) = 0")
    case True
    then show ?thesis using assms(3) split_sum[of x a M b n] by auto
  next
    case False
    then have "¦(∑i<n. x i * a i)¦ < M * ¦(∑i<n. x i * b i)¦" 
      using lt_M[OF assms(1) assms(2)] False
      by (smt (verit, best) mult_less_cancel_left2)
    moreover have "¦(∑i<n. x i * a i)¦ = M * ¦(∑i<n. x i * b i)¦" 
      using assms(3) split_sum[of x a M b n] calculation by linarith
    ultimately have False by linarith 
    then show ?thesis by auto
  qed
next
  case 2
  then show ?case 
  proof (cases "(∑i<n. x i * b i) = 0")
    case True
    then show ?thesis using split_sum 2 using lt_M[OF assms(1) assms(2)]
       by auto
  next
    case False
    then have "¦(∑i<n. x i * a i)¦ < M * ¦(∑i<n. x i * b i)¦" 
      using lt_M[OF assms(1) assms(2)] False
      by (smt (verit, best) mult_less_cancel_left2)
    moreover have "¦(∑i<n. x i * a i)¦ = M * ¦(∑i<n. x i * b i)¦" 
      using split_sum[of x a M b n] assms calculation by linarith
    ultimately have False by linarith 
    then show ?thesis by auto
  qed
qed


text ‹Lemmas about splitting into 4 or 5 cases.›
text ‹Split into $4$ modulo classes›
lemma lt_4_split: "(i::nat) < 4 ⟶ i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3"
by auto 

lemma mod_exhaust_less_4_int: "(i::int) mod 4 = 0 ∨ i mod 4 = 1 ∨ i mod 4 = 2 ∨ i mod 4 = 3"
using MacLaurin.mod_exhaust_less_4 by auto

lemma mod_4_choices:
  assumes "i mod 4 = 0 ⟶ P i"
          "i mod 4 = 1 ⟶ P i"
          "i mod 4 = 2 ⟶ P i"
          "i mod 4 = 3 ⟶ P i"
  shows "P (i::nat)"
using assms mod_exhaust_less_4 by auto

lemma mod_4_if_split:
  assumes "i mod 4 = 0 ⟶ P = P0 i"
          "i mod 4 = 1 ⟶ P = P1 i"
          "i mod 4 = 2 ⟶ P = P2 i"
          "i mod 4 = 3 ⟶ P = P3 i"
  shows "P = (if i mod 4 = 0 then P0 i else
               (if i mod 4 = 1 then P1 i else
               (if i mod 4 = 2 then P2 i else P3 (i::nat))))" (is "?P i")
using mod_exhaust_less_4  by (auto simp add: assms)

text ‹Split into $5$ modulo classes›

lemma lt_5_split: "(i::nat) < 5 ⟶ i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4"
by auto

lemma mod_exhaust_less_5_int: 
  "(i::int) mod 5 = 0 ∨ i mod 5 = 1 ∨ i mod 5 = 2 ∨ i mod 5 = 3 ∨ i mod 5 = 4"
using lt_5_split by linarith

lemma mod_exhaust_less_5: 
  "(i::nat) mod 5 = 0 ∨ i mod 5 = 1 ∨ i mod 5 = 2 ∨ i mod 5 = 3 ∨ i mod 5 = 4"
using lt_5_split by linarith

lemma mod_5_choices:
  assumes "i mod 5 = 0 ⟶ P i"
          "i mod 5 = 1 ⟶ P i"
          "i mod 5 = 2 ⟶ P i"
          "i mod 5 = 3 ⟶ P i"
          "i mod 5 = 4 ⟶ P i"
  shows "P (i::nat)"
using assms mod_exhaust_less_5 by auto

lemma mod_5_if_split:
  assumes "i mod 5 = 0 ⟶ P = P0 i"
          "i mod 5 = 1 ⟶ P = P1 i"
          "i mod 5 = 2 ⟶ P = P2 i"
          "i mod 5 = 3 ⟶ P = P3 i"
          "i mod 5 = 4 ⟶ P = P4 i"
  shows "P = (if i mod 5 = 0 then P0 i else
               (if i mod 5 = 1 then P1 i else
               (if i mod 5 = 2 then P2 i else
               (if i mod 5 = 3 then P3 i else
                                    P4 (i::nat)))))" (is "?P i")
using mod_exhaust_less_5  by (auto simp add: assms)

text ‹Representation of natural number in interval using lower bound.›

lemma split_lower_plus_diff:
  assumes "s ∈ {n..<m::nat}"
  obtains j where "s = n+j" and "j<m-n"
using assms 
by (metis atLeastLessThan_iff diff_diff_left le_Suc_ex zero_less_diff)


end