Re: [isabelle] writing an Isar proof for multiple subgoals

Lars Noschinski wrote:
>   show "eqvt simple4_graph_aux" ...
> next
>   fix x y assume "simple4_graph x y" show True ...
> next
>    fix P y assume "!!x. y = x ==> P" show P ...
> ...

I know this is trivial with automatic methods but I need to learn Isar.

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


No subgoals! 
Failed to apply initial proof method:
goal (1 subgoal):
 1. P
  P :: bool


Why is this an error when it says

  No subgoals!


Isabelle/jEdit does not let me finish the proof with qed.

- Gergely

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