Theory Arithmetical_Hints

(*  Title:      CoW/Arithmetical_Hints.thy
    Author:     Štěpán Holub, Charles University
    Author:     Martin Raška, Charles University
    Author:     Štěpán Starosta, CTU in Prague

Part of Combinatorics on Words Formalized. See https://gitlab.com/formalcow/combinatorics-on-words-formalized/
*)

theory Arithmetical_Hints
  imports Main
begin

section "Arithmetical hints"

text‹In this section we give some specific auxiliary lemmas on natural numbers.›

lemma zero_diff_eq: "i ≤ j ⟹ (0::nat) = j - i  ⟹ j = i"
  by simp

lemma zero_less_diff': "i < j ⟹ j - i ≠ (0::nat)"
   by simp

lemma nat_prod_le: "m ≠ (0 :: nat) ⟹ m*n ≤ k ⟹ n ≤ k"
  using le_trans[of n "m*n" k] by auto

lemma get_div: "(p :: nat) < a ⟹ m = (m * a + p) div a"
  by simp

lemma get_mod: "(p :: nat) < a ⟹ p = (m * a + p) mod a"
  by simp

lemma plus_one_between:  "(a :: nat) < b ⟹ ¬ b < a + 1"
  by auto

lemma quotient_smaller: "k ≠ (0 :: nat) ⟹  b ≤ k * b"
  by simp

lemma mult_cancel_le: "b ≠ 0 ⟹ a*b ≤ c*b ⟹ a ≤ (c::nat)"
  by simp

lemma add_lessD2: "k + m < (n::nat) ⟹ m < n"
unfolding add.commute[of k] using add_lessD1.

lemma mod_offset:  assumes "M ≠ (0 :: nat)"
  obtains k where "n mod M = (l + k) mod M"
proof-
  have "(l + (M - l mod M)) mod M = 0"
    using mod_add_left_eq[of l M "(M - l mod M)", unfolded le_add_diff_inverse[OF mod_le_divisor[OF assms[unfolded neq0_conv]], of l] mod_self, symmetric].
  from mod_add_left_eq[of "(l + (M - l mod M))" M n, symmetric, unfolded this add.commute[of 0] add.comm_neutral]
  have "((l + (M - l mod M)) + n) mod M = n mod M".
  from that[OF this[unfolded add.assoc, symmetric]]
  show thesis.
qed

lemma assumes "q ≠ (0::nat)" shows "p ≤ p + q - gcd p q"
  using gcd_le2_nat[OF ‹q ≠ 0›, of p]
  by linarith

lemma less_mult_one: assumes "(m-1)*k < k" obtains "m = 0" | "m = (1::nat)"
  using assms by fastforce

lemmas gcd_le2_pos = gcd_le2_nat[folded zero_order(4)] and
       gcd_le1_pos = gcd_le1_nat[folded zero_order(4)]

lemma ge1_pos_conv: "1 ≤ k ⟷ 0 < (k::nat)"
  by linarith

lemma per_lemma_len_le: assumes le: "p + q - gcd p q ≤ (n :: nat)" and "0 < q" shows "p ≤ n"
  using le unfolding add_diff_assoc[OF gcd_le2_pos[OF ‹0 < q›], symmetric] by (rule add_leD1)

lemma Suc_less_iff_Suc_le: "Suc n < k ⟷ Suc n ≤ k - 1"
   by auto

lemma nat_induct_pair: "P 0 0 ⟹ (⋀ m n. P m n ⟹ P m (Suc n)) ⟹ (⋀ m n. P m n ⟹ P (Suc m) n) ⟹ P m n"
  by (induction m arbitrary: n) (metis nat_induct, simp)

lemma One_less_Two_le_iff: "1 < k ⟷ 2 ≤ (k :: nat)"
  by fastforce

lemma at_least2_Suc: assumes "2 ≤ k"
  obtains k' where "k = Suc(Suc k')"
  using Suc3_eq_add_3  less_eqE[OF assms] by auto

lemma at_least3_Suc: assumes "3 ≤ k"
  obtains k' where "k = Suc(Suc(Suc k'))"
  using Suc3_eq_add_3  less_eqE[OF assms] by auto

lemmas not0_SucE[elim] = not0_implies_Suc[THEN exE]

lemma le1_SucE: assumes "1 ≤ n"
  obtains k where "n = Suc k" using Suc_le_D[OF assms[unfolded One_nat_def]] by blast

lemma Suc_minus:  "k ≠ 0 ⟹ Suc (k - 1) = k"
   by simp

lemma Suc_minus': "1 ≤ k ⟹ Suc(k - 1) = k"
  by simp

lemmas Suc_minus_pos = Suc_diff_1

lemma Suc_minus2: "2 ≤ k ⟹ Suc (Suc(k - 2)) = k"
  by auto

lemma Suc_leE: assumes "Suc k ≤ n" obtains m where "n = Suc m" and "k ≤ m"
using Suc_le_D assms by blast

lemma two_three_add_le_mult: "2 ≤ (l::nat) ⟹ 3 ≤ k ⟹ k + l + 1 ≤ k*l"
  unfolding numeral_nat
  by (elim Suc_leE)  simp

lemma almost_equal_equal: assumes "(a:: nat) ≠ 0" and "b ≠ 0" and eq: "k*(a+b) + a = m*(a+b) + b"
  shows "k = m" and "a = b"
proof-
  show "k = m"
  proof (rule linorder_cases[of k m])
    assume "k < m"
    from add_le_mono1[OF mult_le_mono1[OF Suc_leI[OF this]]]
    have "(Suc k)*(a + b) + b ≤ m*(a+b) + b".
    hence False
      using  ‹b ≠ 0› unfolding mult_Suc eq[symmetric] by force
    thus ?thesis by blast
  next
    assume "m < k"
    from add_le_mono1[OF mult_le_mono1[OF Suc_leI[OF this]]]
    have "(Suc m)*(a + b) + a ≤ k*(a+b) + a".
    hence False
      using  ‹a ≠ 0› unfolding mult_Suc eq by force
    thus ?thesis by blast
  qed (simp)
  thus "a = b"
    using eq by auto
qed

lemma crossproduct_le: assumes "(a::nat) ≤ b" and "c ≤ d"
  shows "a*d + b*c ≤ a*c + b*d"
proof-
  have "b * c ≤ b * d  + a * c"
    using assms by (simp add: trans_le_add1)
  note mult_le_mono[OF assms]
  have "a * (d - c) ≤ b * (d - c)"
    using mult_le_mono1[OF ‹a ≤ b›].
  hence "a * d - a * c ≤ b * d - b * c"
    using diff_mult_distrib2 by metis
  hence "a * d ≤ b * d - b * c + a * c"
    using le_diff_conv by blast
  hence "a * d ≤ (b * d  + a * c) - b * c"
    by (simp add: ‹c ≤ d›)
  hence "a * d + b * c ≤ (b * d  + a * c) - b * c + b * c"
    by simp
  thus ?thesis
    using ‹b * c ≤ b * d  + a * c› by force
qed

lemma (in linorder) le_less_cases: "(a ≤ b ⟹ P) ⟹ (b < a ⟹ P) ⟹ P"
  by (metis local.not_less)

end