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```