Re: [isabelle] writing an Isar proof for multiple subgoals
On 14.07.2015 11:19, Buday Gergely wrote:
> I have a problem proving the third subgoal:
> lemma "â (P::bool) (x::lam). (â xa. x = xa â P) â P"
> proof -
> fix P x assume "â xa. x = xa â P" show P by auto
> Isabelle tells me
> show Pâbool
> Successful attempt to solve goal by exported rule:
> (âxaâ?'aâtype. (?x2â?'aâtype) = xa â ?P2âbool) â ?P2
> proof (state): depth 0
This tells you that the show statement can discharge one of the subgoals ...
> No subgoals!
> Failed to apply initial proof method:
> goal (1 subgoal):
> 1. P
> P :: bool
... but auto failed to solve it. Notice the suspicious lack of "!!xa. x
= xa" in the second part? That is because you did not feed the
assumption into the show statement (which you could do e.g. using "then").
This archive was generated by a fusion of
Pipermail (Mailman edition) and