# [isabelle] Defining an operation on a particular set and arguments of the definition command

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: [isabelle] Defining an operation on a particular set and arguments of the definition command
*From*: "J.V. Paiva-Miranda-De-Siqueira" <jvp27 at cam.ac.uk>
*Date*: Sun, 24 Jul 2016 10:28:13 +0100
*User-agent*: Roundcube Webmail/1.0.2

Dear Isabelle Users,

`I'm a mathematician recently introduced to Isabelle, and am working on a
``certain theory
``requiring the usage of locales. I ran into a problem while trying to
``define operations on
``a certain set, which I want to be recognized as an instance of a locale
``"Ring" of an imported
`theory.

`This set is named "stalk x", where x is a parameter, i.e, I have stalk::
``"'a â( ('a set Ã 'a) set) set"
``where "stalk x = {germ x U s |U s. (U,s) â prestalk x}" (here prestalk
``is of type "'a â('a set Ã 'a) set"
`and germ is of type "'a â 'a set â 'a â ('a set Ã 'a) set").

`I'm trying to have stalk x as the carrier of a ring, so I need to define
``operations and thus
`attempted the following:
definition stalk_pop :: "'a â [('a set Ã 'a) set , ('a set Ã 'a) set]
â ('a set Ã 'a) set " where
"stalk_pop x (germ x U s) (germ x V t) = germ x (UâV)
( (restrictionsmap (U, UâV) s)Ââobjectsmap (UâV)â
(restrictionsmap (V, UâV) t)) "

`The RHS seems to be correct, but the definition command complains about
``the arguments on the LHS
``(the germs, namely). I can't define this operation for everything of
``type [('a set Ã 'a) set , ('a set Ã 'a) set]
``in a way it reduces to what I want (the RHS) over stalk x and nothing
``here is recursively defined.
``Is there a good way to define this operation strictly over ('a set Ã 'a)
``sets of the form germ x U s?
`
Thanks for your time and pardon the potentially silly question.
Sincerely,
JosÃ Siqueira

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