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.