Re: [isabelle] writing an Isar proof for multiple subgoals
Lars Noschinski wrote:
> show "eqvt simple4_graph_aux" ...
> fix x y assume "simple4_graph x y" show True ...
> 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"
fix P x assume "â xa. x = xa â P" show P by auto
Isabelle tells me
Successful attempt to solve goal by exported rule:
(âxaâ?'aâtype. (?x2â?'aâtype) = xa â ?P2âbool) â ?P2
proof (state): depth 0
Failed to apply initial proof method:
goal (1 subgoal):
P :: bool
Why is this an error when it says
Isabelle/jEdit does not let me finish the proof with qed.
This archive was generated by a fusion of
Pipermail (Mailman edition) and