[isabelle] Problem with implicit structure argument



Hi,

I'm new to Isabelle and I need help with a problem regarding implicit
structure arguments.

To learn Isabelle and since I would be interested in developing some
category theory in Isabelle, I'm trying to make some modifications to Greg
O'Keefe's AFP entry "Category theory using Isar and Locales" (the one
called "Category", not "Category2").

The essential modifications so far are related to two locales:
one_cat (in Functor.thy) and
into_set (in HomFunctor.thy).

In the original O'Keefe's code, these two locales introduce some kind of
"artificial" equations.  E.g., the locale "one_cat" is obtained from
"two_cat" by adding an equation "BB = AA":

locale one_cat = two_cats +
  assumes endo: "BB = AA"

I suspect that this approach was the only one available with some old
implementation of the locales machineries, but now we can do something
better by passing the appropriate parameters to the locale.  This is what I
did

locale one_cat =
  endo: two_cats AA AA
    for AA :: "('o1,'a1,'m1) category_scheme" (structure)

Of course, the rest of the code has to be modified accordingly.  I did part
of the work, but I'm now blocked by the following problem.

In the locale Yoneda (Yoneda.thy) the implicit structure argument is not
recognised anymore.  For instance, I have to write ObâAAâ instead of simply
Ob.  I do not understand why.

My code is available here
https://www.dropbox.com/s/pp3jdd45checg27/Category.tar.gz?dl=0

Thank you for you help,
Marco



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