# Re: [isabelle] Cannot solve all subgoals

Hi Christoph,
> Where did I go wrong? Is this the expected behavior?
the short answer: yes, this is expected behaviour.
The longer answer: The statement
show "P â Q"
doesn't do what you think it does. Let's say, your goal state looks like
this:
1. P â Q
When you prove something with "show", then the goal state gets
*resolved* against what you proved. This allows you e.g. to prove
something more general than what the subgoal says.
In this particular case, you would end up with the new subgoal
1. P â P
However, you can easily avoid that behaviour. You can structure your
proof as follows:
proof -
assume assm: P
show Q
using assm ...
next
assume assm: Q
show P
using assm ...
qed
By explicitly stating "P" as an assumption, the system knows â sloppily
speaking â that it should solve the whole subgoal.
The whole situation is a little bit more complex and it's going to
change (it has already changed in the development version), but the
above is how you would generally structure your proof.
Cheers
Lars

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