Search code examples
proofisabelletheorem-provingisar

Skip a subgoal while proving in Isabelle

I am trying to prove a theorem but got stuck at a subgoal (that I prefer to skip and prove later). How can I skip this and prove the others ?

First, I tried oops and sorry but they both abort the entire proof (instead of the only subgoal). I also tried to put the subgoal into a dummy lemma (assuming proven with sorry) then using it (apply (rule [my dummy lemma])) but it applies the dummy lemma to every other subgoals (not only the first one).

Solution

  • It mostly depends on whether you are using the archaic (sorry for that ;)) apply-style or proper structured Isar for proving. I will give a small example to cover both styles. Assume you wanted to prove

    lemma "A & B"

    Where A and B just serve as placeholders for potentially huge formulas.

    As structured proof you would do something like:

    proof
  show "A" sorry
next
  show "B" sorry
qed

    I.e., in this style you can use sorry to omit proofs for subgoals.

    In apply-style you could do

    apply (rule conjI)
defer -- "moves the first subgoal to the last position"
apply (*proof for subgoal "B"*)
apply (*proof for subgoal "A"*)

    There is also the apply-style command prefer n which moves subgoal n to the front.