Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] I need some help with a theory

Email Gateway (Aug 18 2022 at 12:37):

From: Glauber Cabral <glauber.sp@gmail.com>
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
email.zip

Last updated: May 03 2024 at 04:19 UTC