[isabelle] Cannot solve all subgoals



Hi,

sometimes when I prove a lemma with multiple subgoals one after the
other, the number of subgoals does not shrink and in the end there are
unsolved subgoals that I don't understand.

The following is a minimal example of what happened:

theory Test imports Main begin
lemma foo:
  assumes "R = {}"
  shows "âx y. (x, y) â R â x = y" "âx y. (y, x) â R â (x, y) â R" proof-
  show "âx y. (x, y) â R â x = y" sorry
  show "âx y. (y, x) â R â (x, y) â R" sorry
  (* 2 remaining subgoals at this point:
     1. âx y. (x, y) â R â (y, x) â R
     2. âx y. (y, x) â R â (x, y) â R
  *)
qed
(*
Failed to finish proof:
  goal (2 subgoals):
   1. âx y. (x, y) â R â (y, x) â R
   2. âx y. (y, x) â R â (x, y) â R
*)
end

In the lemma, after positioning the cursor in jedit behind proof-, it
shows me the two subgoals I expect.  After solving these two subgoals,
there are now still 2 goals remaining and the proof fails.

The last unsolved subgoal looks to me exactly like the one I proved
explicitly with the second show line, so I am somewhat puzzled as to why
it remains.

Where did I go wrong?  Is this the expected behavior?

(In case it is relevant, I work with Isabelle2015.)

Thanks,
Christoph




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.