Stream: Beginner Questions

Topic: induction rule for odd numbers

ee (Apr 11 2024 at 17:20):

Is there an induction rule for odd nats somewhere?

Mathias Fleury (Apr 11 2024 at 17:33):

have you searched for it
find_theorems odd name:induct?

Mathias Fleury (Apr 11 2024 at 17:34):

I do not think that it exists, but it is also very trivial to prove

lemma odd_induct[consumes 1, case_names 1 Suc]:
  fixes n :: nat
  assumes ‹odd n› and
   ‹P 1›
   ‹⋀n. P n ⟹ P (n+2)›
 shows ‹P n›
proof -
  obtain k ::nat where k: ‹n = 2*k+1›
    using assms(1) oddE by blast
  show ‹P n›
    unfolding k
    apply (induction k)
    subgoal using assms(2) by auto
    subgoal using assms(3) by auto
    done
qed

Mathias Fleury (Apr 11 2024 at 17:36):

(and the proof works exactly like you would expect from doing it on paper)

Last updated: May 07 2024 at 01:07 UTC