Stream: Beginner Questions

Topic: ✔ How can I invoke Sledgehammer to finish an induction pr...

Mathias Fleury (Mar 21 2026 at 12:55):

by is closing goals. Sledgehammer works on open goals

Mathias Fleury (Mar 21 2026 at 12:55):

So either:

   apply (induction x)
   sledgehammer

Mathias Fleury (Mar 21 2026 at 12:56):

or:

proof (induction x)
  (*click on the skeleton produced by Isabelle/jEdit*)
   case 0
  then show ?case
    sledgehammer
   sorry
next
  case (Suc n)
  then show ?case
    sledgehammer
   sorry
qed

Adam Dingle (Mar 21 2026 at 12:57):

Great, thanks!

Notification Bot (Mar 21 2026 at 12:57):

Adam Dingle has marked this topic as resolved.

Last updated: Mar 25 2026 at 02:29 UTC