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:
>   Pâbool

This tells you that the show statement can discharge one of the subgoals ...
>
> goal:
> No subgoals! 
> Failed to apply initial proof method:
> goal (1 subgoal):
>  1. P
> variables:
>   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").

 -- Lars




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