[isabelle] I need some help with a theory



Dear Isabelle users,

I'm using Isabelle to prove theories that are automatically generated
by HETS tool and I'm still learning Isabelle. I'm not using Isar
because when I started I though it should be easier to use the apply
method, so I still didn't learn Isar.

I've been trying to prove Theorem01 inside the attached theory
Prelude_SortingPrograms_E1.thy, but I have no idea how to go further
from the line "thm GenSortT1".
I think I should make Isabelle match this rule (GenSortT1) with the
goal, but I could not do it. I've tried apply(case_tac Lista) to check
if this way I could use the rule GenSortT1, but I had no success.

If you can give me any ideas of how to go any further, I'll be very thankful.

Yours,
Glauber

Attachment: email.zip
Description: Zip archive



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