theory Scratch
imports Main
begin
lemma strong_induction_helper:
assumes step: "\ n. (\ m P n"
shows "\ m<(k::nat). P m"
using step
proof (induct k)
show "\ m<0. P m" by simp
next
fix k assume ih: "\n. (\m P n \ \ mn. (\m P n"
show "\ m < Suc k. P m"
proof clarify
fix m assume msk: "m < Suc k"
from step ih have pm: "\ m m = k" by arith
thus "P m"
proof
assume "m < k" with pm show ?thesis by blast
next
assume m: "m = k"
from pm step have "P k" by blast
with m show "P m" by blast
qed
qed
qed
theorem strong_induction:
assumes step: "\ n. (\ m P n"
shows "P (k::nat)"
proof -
from step have "\ m< Suc k. P m" by (rule strong_induction_helper)
thus ?thesis by blast
qed
end