Search code examples
isabelletheorem-provinginduction

Isabelle induction, custom base case

I'm currently trying to proof the following lemma in isabelle:

lemma helper:
  fixes n :: nat
  assumes "n ≥ 5"
  shows "(n * n > 2*n + 1)"

proof (induction n)
qed

However the induction proof tactic forces me to show the following two cases:

 1. 2 * 0 + 1 < 0 * 0
 2. ⋀n. 2 * n + 1 < n * n ⟹ 2 * Suc n + 1 < Suc n * Suc n

With the first one obviously being wrong. However since my lemma states that it assumes n >= 5 I'm wondering why exactly it's not starting its induction for the base case n = 5? And since it doesn't do that, would also be interested in how I could get it to start induction at n = 5 instead of 0.

Solution

  • You can use the dec_induct induction rule as follows:

    lemma helper:
  fixes n :: nat
  assumes "n ≥ 5"
  shows "(n * n > 2*n + 1)"
  using assms
proof (induction rule: dec_induct)
  case base ― ‹n = 5›
  then show ?case by simp
next
  case (step m) ― ‹5 ≤ m < n›
  then show ?case by simp
qed