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



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.