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