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

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')

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

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
qed