[isabelle] programming an instance proof in HOL



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.





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