Theory IMO2019_Q1

(*
  File:    IMO2019_Q1.thy
  Author:  Manuel Eberl, TU München
*)
section ‹Q1›
theory IMO2019_Q1
  imports Main
begin

text ‹
  Consider a function ‹f : ℤ → ℤ› that fulfils the functional equation
  ‹f(2a) + 2f(b) = f(f(a+b))› for all ‹a, b ∈ ℤ›.

  Then ‹f› is either identically 0 or of the form ‹f(x) = 2x + c› for some constant ‹c ∈ ℤ›.
›

context
  fixes f :: "int ⇒ int" and m :: int
  assumes f_eq: "f (2 * a) + 2 * f b = f (f (a + b))"
  defines "m ≡ (f 0 - f (-2)) div 2"
begin

text ‹
  We first show that ‹f› is affine with slope ‹(f(0) - f(-2)) / 2›.
  This follows from plugging in ‹(0, b)› and ‹(-1, b + 1)› into the functional equation.
›
lemma f_eq': "f x = m * x + f 0"
proof -
  have rec: "f (b + 1) = f b + m" for b
    using f_eq[of 0 b] f_eq[of "-1" "b + 1"] by (simp add: m_def)
  moreover have "f (b - 1) = f b - m" for b
    using rec[of "b - 1"] by simp
  ultimately show ?thesis
    by (induction x rule: int_induct[of _ 0]) (auto simp: algebra_simps)
qed

text ‹
  This version is better for the simplifier because it prevents it from looping.
›
lemma f_eq'_aux [simp]: "NO_MATCH 0 x ⟹ f x = m * x + f 0"
  by (rule f_eq')

text ‹
  Plugging in ‹(0, 0)› and ‹(0, 1)›.
›
lemma f_classification: "(∀x. f x = 0) ∨ (∀x. f x = 2 * x + f 0)"
  using f_eq[of 0 0] f_eq[of 0 1] by auto

end

text ‹
  It is now easy to derive the full characterisation of the functions we considered:
›
theorem
  fixes f :: "int ⇒ int"
  shows "(∀a b. f (2 * a) + 2 * f b = f (f (a + b))) ⟷
           (∀x. f x = 0) ∨ (∀x. f x = 2 * x + f 0)" (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  thus ?rhs using f_classification[of f] by blast
next
  assume ?rhs
  thus ?lhs by (smt (verit, ccfv_threshold) mult_2)
qed

end