Stream: Beginner Questions

Topic: ✔ Strong induction in Isabelle

Lekhani Ray (Jul 19 2022 at 20:55):

Is there a way to perform strong induction in Isabelle? I cannot find too many working examples on it yet?

Lukas Stevens (Jul 19 2022 at 21:04):

proof(induction n rule: less_induct)

Jonathan Julian Huerta y Munive (Jul 20 2022 at 08:09):

You can search for induction principles with command find_theorems. You can use keywords induct and nat, for example find_theorems name: induct name: nat.

Alternatively, you can prove induction principles yourself. For strong induction:

lemma nat_strong_induct[case_names zero induct]:
  assumes "P 0"
    and "(⋀n. (⋀m. m ≤ n ⟹ P m) ⟹ P (Suc n))"
  shows "P n"
  using assms
  apply (induct n rule: full_nat_induct)
  by simp (metis Suc_le_mono not0_implies_Suc)

Then you can use it as shown below:

lemma "∃m::nat. m > n"
  by (induct n rule: nat_strong_induct)
    auto

Notification Bot (Jul 21 2022 at 12:23):

Lekhani Ray has marked this topic as resolved.

Lekhani Ray (Jul 21 2022 at 12:23):

Jonathan Julian Huerta y Munive said:

You can search for induction principles with command find_theorems. You can use keywords induct and nat, for example find_theorems name: induct name: nat.

Alternatively, you can prove induction principles yourself. For strong induction:

lemma nat_strong_induct[case_names zero induct]:
  assumes "P 0"
    and "(⋀n. (⋀m. m ≤ n ⟹ P m) ⟹ P (Suc n))"
  shows "P n"
  using assms
  apply (induct n rule: full_nat_induct)
  by simp (metis Suc_le_mono not0_implies_Suc)

Then you can use it as shown below:

lemma "∃m::nat. m > n"
  by (induct n rule: nat_strong_induct)
    auto

Thank you Jonathan! That really helped!

Last updated: Dec 21 2024 at 16:20 UTC