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

this:
  Pâbool

goal:
No subgoals! 
Failed to apply initial proof method:
goal (1 subgoal):
 1. P
variables:
  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.