Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] programming an instance proof in HOL

Email Gateway (Aug 18 2022 at 10:40):

From: Michael Norrish <michael.norrish@nicta.com.au>
I wish to do the equivalent of

instance tyop :: (class1) class2
...

I hoped that it would be enough to have (a certified term version of)

Logic.mk_inclass (Type(tyop, [TFree("'a", [class1])]), class2)

as my goal. Though I am able to prove this goal, I get an exception
when I attempt to add my new theorem as an arity (using
AxClass.add_arity)

Exception-
THM
("add_arity: malformed type arity",
0,
["OFCLASS('a bit0, asz2_class)"]) raised

What then should be the form of my theorem?

(I also tried using AxClass.add_classrel, but this fails with a
similar message.)

Michael.

Last updated: May 03 2024 at 08:18 UTC