Proof by induction with three base cases (Isabelle)

Question

I want to be able to prove a statement by induction on n (of type nat). It consists of a conditional whose antecedent is only true for n >= 2. A conditional whose antecedent is false is always true. So I'd like to prove the cases n=0, n=1 and n=2 all separately from the main inductive step. Is it possible to do a proof by induction with three base cases like the following:

  lemma "P (n::nat) --> Q"
  proof (induct n)
    case 0
    show ?case sorry
  next
    case 1
    show ?case sorry
  next 
    case 2
    show ?case sorry
  next
    case (Suc n)
    show ?case sorry
  qed

As it stands, this doesn't seem to work. I could prove "P (n+2) --> Q" by induction instead, but it wouldn't be as strong a statement. I'm considering a case split into "n=0","n=1" and "n>=2", and proving only the last case by induction.

Answer 1

The cleanest way is probably to prove a custom induction rule for the kind of induction that you want, like this:

lemma nat_0_1_2_induct [case_names 0 1 2 step]:
  assumes "P 0" "P 1" "P 2" "⋀n. n ≥ 2 ⟹ P n ⟹ P (Suc n)"
  shows   "P n"
proof (induction n rule: less_induct)
  case (less n)
  show ?case using assms(4)[OF _ less.IH[of "n - 1"]]
    by (cases "n ≤ 2") (insert assms(1-3), auto simp: eval_nat_numeral le_Suc_eq)
qed

lemma "P (n::nat) ⟶ Q"
proof (induction n rule: nat_0_1_2_induct)

In theory, the induction_schema method is also very useful to prove such custom induction rules, but in this case, it doesn't help a lot:

lemma nat_0_1_2_induct [case_names 0 1 2 step]:
  "P 0 ⟹ P 1 ⟹ P 2 ⟹ (⋀n. n ≥ 2 ⟹ P n ⟹ P (Suc n)) ⟹ P n"
proof (induction_schema, goal_cases complete wf terminate)
  case (complete P n)
  thus ?case by (cases n) force+
next
  show "wf (Wellfounded.measure id)" by (rule wf_measure)
qed simp_all

You could also use less_induct directly and then do a case distinction within the induction step for the base cases.