theory Scratch
imports Main
begin

lemma strong_induction_helper: 
  assumes step: "\<forall> n. (\<forall> m<n. P m) \<longrightarrow> P n"
  shows "\<forall> m<(k::nat). P m"
  using step
proof (induct k)
  show "\<forall> m<0. P m" by simp
next
  fix k assume ih: "\<forall>n. (\<forall>m<n. P m) \<longrightarrow> P n \<Longrightarrow> \<forall> m<k. P m"
    and step: "\<forall>n. (\<forall>m<n. P m) \<longrightarrow> P n"
  show "\<forall> m < Suc k. P m"
  proof clarify
    fix m assume msk: "m < Suc k"
    from step ih have pm: "\<forall> m<k. P m" by blast
    from msk have "m < k \<or> 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: "\<forall> n. (\<forall> m<n. P m) \<longrightarrow> P n"
  shows "P (k::nat)"
proof -
  from step have "\<forall> m< Suc k. P m" by (rule strong_induction_helper)
  thus ?thesis by blast
qed

end