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

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 ...
  assume assm: Q
  show P
    using assm ...

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.


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