[isabelle] Fighting with apply


I'm currently working through isabelle tutorial, and while all
definition stuff is quite understandable, there's one area which is a
complete magic for me: choosing what to type in "apply (<tac>)" to
prove the theorem. Are there better texts to grasp this? Or should I
read the tutorial and fight with my theorems till I win?

Right now I'm trying to prove some basic facts about graphs and it's
really, really painful to move forward. Is it possible for some more
advanced users of isabelle to take a look at what I'm doing and push
me in the right direction? Can same things be expressed more easily in
isabelle? I'm attaching the file I'm working on.


Attachment: graph2.thy
Description: Binary data

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