# [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.*